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.
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.