A model checker for the Dynamic Logic of Propositional Assignments (DLPA) with solving and parameterized random formula generation functionalities.
Compilation:
make
Usage:
./build/dlpa {csg} [v] [f input_file_path] [o output_file_path]
Options:
c check model
Given a DLPA 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 DLPA formula, find all valuations which model the formula.
g generate formula
Given a set of parameter weights, generate a random DLPA formula.
v verbose
f input file
Input file contains a DLPA 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] // Nondeterministic composition
 prog[L] "\\star" // Finite iteration (Kleene star)
;
Flex atom format:
[azAZ][azAZ09]*"("[ ,azAZ09]*")"
[azAZ][azAZ09]*
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.
A model checker for the Dynamic Logic of Propositional Assignments (DLPA) with solving and parameterized random formula generation functionalities.
Owner
Jeffrey Yang
Similar Resources
Adjust Cirrus Logic CLGD542x memory clock (DOS tool)
clmclk This is a tool for DOS to adjust Cirrus Logic CLGD542x memory clock. This tool works on ISA and VL graphics cards with the CLGD542, CLGD5426
Repository of the magnUS Snakemen team for the third project in 2022, titled Logic Game
ใ ๐ ใmagnUSSnakemenใ ๐ ใ ๐ 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
Wellorganized, commented and documented sample project that shows the basic functionalities of the 42's mlx library.
miniLibX sample  slucass I developed this sample project to play around with the basic functionalities of the miniLibX, the simple graphics library
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
USB to interfaces implementing MicroPython "machine" module functionalities on a computer.
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
ozzanimation provides runtime character animation playback functionalities (loading, sampling, blending...)
ozzanimation open source c++ 3d skeletal animation library and toolset ozzanimation provides runtime character animation playback functionalities (l
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
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
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
Related tags
ESP32SkidSteer  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.
ESP32SkidSteer Bruder Catepillar Skid Steer model converted to RC, controlled by an ESP32 with 2 analog joysticks and a receiver that is an ESP32 on
CSE7thSemesterIITKGP  Tests, programming assignments and their solution for some courses offered by Department of Computer Science and Engineering, IIT Kharagpur
CSE7thSemesterIITKGP Disclaimer: Do not copy codes though. Heavy penalization for plagiarism. Programming assignments and their solution for some
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.
Practical assignments for the XDU compiler course: The interpreter of function drawing language.
drawinglanginterpreter Practical assignments for the XDU compiler course: The toy interpreter of function drawing language, written by XDU Zhang Yi(
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
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
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
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
Using a RP2040 Pico as a basic logic analyzer, exporting CSV data to read in sigrok / Pulseview
rp2040logicanalyzer This project modified the PIO logic analyzer example that that was part of the Raspberry Pi Pico examples. The example now allow
NAND (JEDEC / ONFI) Analyzer for Saleae Logic
NandAnalyzer NAND (JEDEC / ONFI) Analyzer for Saleae Logic The plugin was only tested against NVDDR3 traces (and I use the term "test" lightly). You