A model checker for the Dynamic Logic of Propositional Assignments (DL-PA) with solving and parameterized random formula generation functionalities.

A model checker for the Dynamic Logic of Propositional Assignments (DL-PA) with solving and parameterized random formula generation functionalities.

Compilation:
    make

Usage:
    ./build/dlpa {-c|-s|-g} [-v] [-f input_file_path] [-o output_file_path]

Options:
    -c check model
        Given a DL-PA formula and valuation, check if the valuation models the formula.
        Atoms not present in the valuation set are false by default.
    -s solve formula
        Given a DL-PA formula, find all valuations which model the formula.
    -g generate formula
        Given a set of parameter weights, generate a random DL-PA formula.
    -v verbose
    -f input file
        Input file contains a DL-PA formula if checking/solving, or parameter weights if generating.
        If no input file is given, read from stdin.
    -o output file
        If no output file is given, write to stdout.

Bison Grammar:   
    Valuation
        input_valuation
        : "{" valuation "}"
        |
        ;

        valuation
        : "atom" valuation 
        |
        ;
    
    Formula
        form
        : "(" form[F] ")"           
        | form[L] "\\or" form[R]    // Disjunction
        | "\\neg" form[F]           // Negation
        | "\\top"                   // True
        | "<" prog[P] ">" form[F]   // Diamond
        | "atom"                    // Atom
        ;

    Program
        prog
        : "(" prog[P] ")"           
        | "atom" "<-" form[F]       // Assignment
        | "?" form[F] "?"           // Test
        | prog[L] "\\seq" prog[R]   // Sequential composition
        | prog[L] "\\cup" prog[R]   // Non-deterministic composition
        | prog[L] "\\star"          // Finite iteration (Kleene star)
        ;

    Flex atom format:
        [a-zA-Z][a-zA-Z0-9]*"("[ ,a-zA-Z0-9]*")"
        [a-zA-Z][a-zA-Z0-9]* 

    Example:
        {atom1, atom2, atom(x,y)} <?atom1? \seq atom2 <- \neg atom2> atom2 \or atom(x,y)
    
    
Parameters input format if generating:
    9 integers for formula weights (fATOM,fOR,fNEG,fTOP,fDIAMOND,fNEGATOM,fAND,fFALSE,fBOX)
    9 integers for program weights (pGETS,pTEST,pSEQ,pCUP,pSTAR,pIFTHEN,pIFTHENELSE,pWHILEDO,pDOWHILENOT)
    1 integer for max_depth
    1 integer for max_atoms

    If all weights are 0 then set all weights to 1 by default

Testing:
    Usage:
        python3 tests/runtests.py [test_suite ...]
    If no test suites are given then all test suites are used. 
    Only model checking is checked.
Owner
Similar Resources

Adjust Cirrus Logic CL-GD542x memory clock (DOS tool)

clmclk This is a tool for DOS to adjust Cirrus Logic CL-GD542x memory clock. This tool works on ISA and VL graphics cards with the CL-GD542, CL-GD5426

Apr 6, 2022

Repository of the magnUS Snakemen team for the third project in 2022, titled Logic Game

Repository of  the <<magnUS Snakemen>> team for the third project in 2022, titled  <<Logic Game>>

ใ€Ž ๐Ÿ ใ€magnUS-Snakemenใ€Ž ๐Ÿ ใ€ ๐Ÿ“– About It's been a tough day at school. You come back home, leave your bag on your bed and sit on your desk. You think i

Nov 17, 2022

Well-organized, commented and documented sample project that shows the basic functionalities of the 42's mlx library.

miniLibX sample | slucas-s I developed this sample project to play around with the basic functionalities of the miniLibX, the simple graphics library

Jan 1, 2023

A multiplatform C++ library for common and basic system functionalities.

axl.cm A multiplatform C++ library for common and basic system functionalities. Platforms Linux Windows C++ standard minimum: C++98 target: C++11 maxi

Apr 4, 2022

USB to interfaces implementing MicroPython "machine" module functionalities on a computer.

USB to interfaces implementing MicroPython

u2if project u2if(USB to interfaces) is an attempt to implement some of the MicroPython "machine" module functionalities on a computer. The goal is to

Dec 26, 2022

ozz-animation provides runtime character animation playback functionalities (loading, sampling, blending...)

ozz-animation provides runtime character animation playback functionalities (loading, sampling, blending...)

ozz-animation open source c++ 3d skeletal animation library and toolset ozz-animation provides runtime character animation playback functionalities (l

Dec 27, 2022

It's an 90 days challenge where all important concept of DSA I will be learning and solving using C++ or Java.

#90DaysDSA It's an 90 days challenge where all important concept of DSA I will be learning and solving using C++ or Java. Day 1 & 2 - Space and Time

Dec 11, 2021

Solving Kepler's equation via contour integration, implemented in C++

Kepler's Goat Herd Code for solving Kepler's equation using contour integration, following Philcox et al. (2021, arXiv). This uses a method originally

Sep 11, 2022

Utility for testing random and pseudorandom sequences, either as bytes or bit streams, reporting entropy, mean value, serial correlation, chi square, and Monte Carlo estimate of an value, serial correlation, chi square, and Monte Carlo estimate of ฯ€.

ENT โ€” Fourmilab Random Sequence Tester The Fourmilab Random Sequence Tester, ent, applies various tests to sequences of bytes stored in files and repo

Dec 15, 2022
Related tags
ESP32-Skid-Steer - Bruder Catepillar Skid Steer model converted to RC, controlled by an ESP32 with 2 analog joysticks and a receiver that is an ESP32 on the model.
ESP32-Skid-Steer - Bruder Catepillar Skid Steer model converted to RC, controlled by an ESP32 with 2 analog joysticks and a receiver that is an ESP32 on the model.

ESP32-Skid-Steer Bruder Catepillar Skid Steer model converted to RC, controlled by an ESP32 with 2 analog joysticks and a receiver that is an ESP32 on

Oct 27, 2022
CSE-7th-Semester-IIT-KGP - Tests, programming assignments and their solution for some courses offered by Department of Computer Science and Engineering, IIT Kharagpur

CSE-7th-Semester-IIT-KGP Disclaimer: Do not copy codes though. Heavy penalization for plagiarism. Programming assignments and their solution for some

Dec 30, 2021
MDE is a model extraction tool that converts Destiny 2 dynamic models into fbx files supporting textures, skeletons, and all provided vertex data.

MDE is a model extraction tool that converts Destiny 2 dynamic models into fbx files. A dynamic model is one that is animated or is spawned in during the game.

Sep 2, 2022
Practical assignments for the XDU compiler course: The interpreter of function drawing language.

drawing-lang-interpreter Practical assignments for the XDU compiler course: The toy interpreter of function drawing language, written by XDU Zhang Yi(

Sep 30, 2022
Assignments for Operating System (CO2017) - Semester 202 - HCMUT
Assignments for Operating System (CO2017) - Semester 202 - HCMUT

VIETNAM NATIONAL UNIVERSITY, HO CHI MINH CITY UNIVERSITY OF TECHNOLOGY FACULTY OF COMPUTER SCIENCE AND ENGINEERING โ€ƒ โ€ƒ Operating System / Semester 202

Dec 23, 2021
Logic and Mechanized Reasoning

Logic and Mechanized Reasoning This repository is designed to accompany the course by the same name. See also: the textbook (in progress): https://avi

Dec 29, 2022
Stock exchange simulator made in Swing using Java with logic backend in C++ giving it faster load time and better data control

StockSimulator Stock exchange simulator made in Swing using Java with logic backend in C++ giving it faster load time and better data control Features

Mar 1, 2022
This repo contains BOTH c++ and BP examples to acheive the same logic, but in each frameworks specific ways

ApparatusCppMoveRandomly Hey there! This repo contains BOTH c++ and BP examples to acheive the same logic, but in each frameworks specific ways. I int

Jan 24, 2022
Using a RP2040 Pico as a basic logic analyzer, exporting CSV data to read in sigrok / Pulseview

rp2040-logic-analyzer This project modified the PIO logic analyzer example that that was part of the Raspberry Pi Pico examples. The example now allow

Dec 29, 2022
NAND (JEDEC / ONFI) Analyzer for Saleae Logic
NAND (JEDEC / ONFI) Analyzer for Saleae Logic

NandAnalyzer NAND (JEDEC / ONFI) Analyzer for Saleae Logic The plugin was only tested against NV-DDR3 traces (and I use the term "test" lightly). You

Dec 12, 2022