smcdel alternatives and similar packages
Based on the "Logic" category
* Code Quality Rankings and insights are calculated and provided by Lumnify.
They vary from L1 to L5 with "L5" being the highest. Visit our partner's website for more details.
Do you think we are missing an alternative of smcdel or a related project?
A symbolic model checker for Dynamic Epistemic Logic.
You can find a complete literate Haskell documentation in the file SMCDEL.pdf.
Johan van Benthem, Jan van Eijck, Malvin Gattinger, and Kaile Su: Symbolic Model Checking for Dynamic Epistemic Logic. In: Proceedings of The Fifth International Conference on Logic, Rationality and Interaction (LORI-V), 2015.
You can try SMCDEL online here: https://w4eg.de/malvin/illc/smcdelweb/
On Debian, just do
sudo apt install graphviz dot2tex.
1) Use stack from https://www.stackage.org
stack buildwill compile everything. This might fail if one of the BDD packages written in C and C++ is missing. In this case, install those manually and then try
stack installwill put two executables
smcdel-webinto ~/.local/bin which should be in your
2) Create a text file
MuddyShort.smcdel.txt which describes the knowledge structure and the formulas you want to check for truth or validity:
``` -- Three Muddy Children in SMCDEL VARS 1,2,3 LAW Top OBS alice: 2,3 bob: 1,3 carol: 1,2 WHERE? [ ! (1|2|3) ] alice knows whether 1 VALID? [ ! (1|2|3) ] [ ! ((~ (alice knows whether 1)) & (~ (bob knows whether 2)) & (~ (carol knows whether 3))) ] [ ! ((~ (alice knows whether 1)) & (~ (bob knows whether 2)) & (~ (carol knows whether 3))) ] (alice,bob,carol) comknow that (1 & 2 & 3) ```
smcdel MuddyShort.smcdel.txt resulting in:
``` >> smcdel MuddyShort.smcdel.txt SMCDEL 1.0 by Malvin Gattinger -- https://github.com/jrclogic/SMCDEL At which states is ... true?   Is ... valid on the given structure? True ```
More example files are in the folder Examples.
To deal with more complex models and formulas, use SMCDEL as a Haskell module.
Used BDD packages
SMCDEL can be used with different BDD packages. To compile and run the benchmarks you will have to install all of them.