A CTL (Computation Tree Logic) model checker having as input a file containing a textual description of a Kripke structure and a file containing a CTL formula.

• The first line of input contains a single integer, n (the number of states).
• The next line contains n space-separated strings describing the respective designations for states.
• The next line contains a single integer, m (the number of initial states).
• The next line contains m space-separated strings describing the respective designations for initial states.
• The next line contains a single integer, x (the number of transitions).
• Each line i of the x subsequent lines contains two space-separated integers describing the respective designations of source state and destination state for the transition i.
• The next line contains a single integer, y (the number of states that have interpretations).
• Each line j of the y subsequent lines describes interpretations for state j as a space-separated tokens. Each line takes the following form:
  • The first token denotes the designation for state j.
  • The second token, z, denotes the number of propositions for state j.
  • The rest of the line contains z space-separated strings describing the respective designations of propositions for state j.

Check grammar file.

A single line that contains space-separated strings describing the respective designations for states that satisfies the CTL formula.

• Gradle: for building the jar file.
• Java: for executing the jar file.

1- Clone this repository:

git clone [email protected]:iahmedbacha/ctl-model-checker.git

2- At the root of the project, build the jar file:

gradle build

3- Find the generated jar file in:

./app/build/libs/app-all.jar

4- Assuming app-all.jar, kripke.txt and formula.txt are in the same folder, execute:

java -jar app-all.jar kripke.txt formula.txt output.txt

5- Find the result in output.txt.

Find examples of a Kripke structure and CTL formulae here.

Contributions are always welcome!

• Add tests.