Skip to content
/ ctlmc Public

CTL model checker, implemented using BDDs (JavaBDD library)

License

Notifications You must be signed in to change notification settings

fpoli/ctlmc

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

14 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

CTL model checking

CTL model checking, implemented using BDDs (JavaBDD library).

Build Status

Usage

Usage: program (CTL specification) (path to model file)
e.g.: program 'AG(Not(And("c1"="T", "c2"="T")))' "model.fsm"

Arguments:

  1. CTL specification (e.g. Imply(AG("t1"="T"), AF("c1"="T")));
  2. path to model file, in the FSM format with the following restriction:
    • all the states must be univocally identified by the value of their atomic propositions.

Quick start

  1. Install Scala and sbt
  2. Run tests with make test
  3. Prepare jar package with make package
  4. Run demo with java -jar /path/to/ctl-model-checking.jar 'AG(Not(And("c1"="T", "c2"="T")))' ./src/test/resources/mutual-exclusion.fsm

Example (output)

=== CTL Model Checking ===
(*) Parsing CTL specification AG(Not(And("c1"="T", "c2"="T"))) ...
(*) Parsing FSM model ./src/test/resources/mutual-exclusion.fsm ...
 - 9 atomic propositions
 - 9 states
 - 14 transitions
(*) Model checking...
[OK] The model satisfies the specification

License

Copyright (C) 2015 Federico Poli federpoli@gmail.com

Released under the GNU General Public License, version 3

About

CTL model checker, implemented using BDDs (JavaBDD library)

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published