smcdel: Symbolic Model Checking for Dynamic Epistemic Logic

[ gpl, library, logic ] [ Propose Tags ]

See README.md for references and documentation.


[Skip to Readme]

Flags

Manual Flags

NameDescriptionDefault
cliEnabled
webDisabled
with-cuddDisabled

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 1.0.0, 1.1.0, 1.2.0, 1.3.0
Change log CHANGELOG.md
Dependencies ansi-terminal (>=0.11.5 && <1.2), array (>=0.5.4 && <0.6), base (>=4.8 && <5), containers (>=0.6.7 && <0.7), decision-diagrams (>=0.2.0 && <0.3), directory (>=1.3.7 && <1.4), filepath (>=1.4.2 && <1.5), graphviz (>=2999.20.2 && <2999.21), HasCacBDD (>=0.2.0.0 && <0.3), process (>=1.6.18 && <1.7), QuickCheck (>=2.14.3 && <2.15), smcdel, tagged (>=0.8.0 && <0.9), temporary (>=1.3 && <1.4), text (>=2.0.2 && <2.1), time (>=1.12.2 && <1.13) [details]
License GPL-2.0-only
Author
Maintainer Malvin Gattinger <malvin@w4eg.eu>
Category Logic
Home page https://github.com/jrclogic/SMCDEL#readme
Bug tracker https://github.com/jrclogic/SMCDEL/issues
Source repo head: git clone https://github.com/jrclogic/SMCDEL
Uploaded by m4lvin at 2024-04-24T17:13:30Z
Distributions
Executables smcdel-web, smcdel
Downloads 1232 total (16 in the last 30 days)
Rating 2.0 (votes: 1) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs uploaded by user
Build status unknown [no reports yet]

Readme for smcdel-1.3.0

[back to package description]

SMCDEL

Release Hackage GitLab CI Test Coverage DOI

A symbolic model checker for Dynamic Epistemic Logic.

Online

You can try SMCDEL online here: https://w4eg.de/malvin/illc/smcdelweb/

Basic usage

  1. Use stack from https://www.stackage.org
  • stack install will build and install an executable smcdel into ~/.local/bin which should be in your PATH variable.
  1. 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)
    
  2. Run 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?
    []
    [1]
    
    Is ... valid on the given structure?
    True
    

    More example files are in the folder Examples.

  3. To also build and install the web interface, run stack install --flag smcdel:web Then you can run smcdel-web and open http://localhost:3000.

Advanced usage

The executables only provide model checking for S5 with public announcements. For K and to define more complex models and updates, SMCDEL should be used as a Haskell library. Please refer to the Haddock documentation for each module.

Examples can be found in the folders src/SMCDEL/Examples and bench.

Dependencies: To get all visualisation functions working, graphviz, dot2tex and some LaTeX packages should be installed. On Debian, please do sudo apt install graphviz dot2tex libtinfo5 texlive-latex-base poppler-utils preview-latex-style texlive-pstricks.

Used BDD packages

SMCDEL uses different BDD packages.

  • Data.HasCacBDD which runs CacBDD from http://kailesu.net/CacBDD/. This is the default choice used by the executables and the modules Symbolic.S5 and Symbolic.K.

  • The pure Haskell library decision-diagrams. It is used by the module Symbolic.S5_DD.

  • Optionally, Cudd (with some patches) which uses the CUDD library. To obtain the modules SMCDEL.Symbolic.S5_CUDD, SMCDEL.Symbolic.S5_K, SMCDEL.Symbolic.S5_Ki you should compile with stack build --flag smcdel:with-cudd.

References

Main reference for the theory behind the implementation, also containing benchmarks:

Additional publications: