jlhsmall/LTL

#LTL Model Checking The big assignment of CS3959: Model Checking.

This project is programmed in Java, and uses ANTLR 4 parser generator. It checks whether a transition system or a certain state of it satisfies some LTL formulae. ##How to run Write the input to input.txt, and run Main.java, then the result will be presented in the system output.

If you want to know the formula's elementary set, as well as the construction of GNBA, NBA and transition system, undo the comments in line 23 (GNBA), 25 (NBA), 27 (transition system) of Main.java.

##Project Structure

###Main.java The main function void main(String[] args) process the input. For each query, it writes the formula in formula.txt, and calls void solve(TransitionSystem TS), which checks whether the transition system satisfies the formula in formula.txt. For the queries of a certain state $s$, we modify the transition system's set of initial states to ${s}$, and call void solve(TransitionSystem TS).

The void solve(TransitionSystem TS) first builds an AST according to the formula (using the parser in src/AST, generated by LTL.g4). Here, assume the formula in formula.txt is #\varphi#, then the AST we build will be one denoting $\neg\varphi$. After that, we use the AST to build the GNBA, the NBA, and do the product construction and persistence checking.

###MyInput.java This class is created to make inputting easier. ArrayList<Integer> ReadIntegerLine(BufferedReader br) reads a line of integers, and ArrayList<String> ReadStringLine(BufferedReader br) reads a line of strings.

###Abstract Syntax Tree Task 1. The Abstract Syntax Tree (AST) is stored in src/AST. We use ASTBuilder.java to build the tree, and define the class of tree node in ASTNode, each of which represents a sub-formula of $\neg\varphi$. The rest classes each represents a certain type of formula, and is derived from ASTNode.

###GNBA.java Task 2. The GNBA can be constructed from an LTL formula (here an AST) according to the textbook.

###NBA.java Task 3. The NBA can be constructed from a GNBA according to the textbook.

###TransitionSystem.java The transition system can be constructed from a file input, which is realized in TransitionSystem(String file); or we can do the product construction (Task 4), which is realized in TransitionSystem(TransitionSystem TS, NBA A, ASTNode root). To do persistence checking (Task 5), just call boolean hasFSCC(), and reverse the result.