This is a program that implements the LTL model checking algorithm which can be found in the book "Principles of Model Checking".
This is a project for the course "model checking" in Shanghai Jiao Tong University. The code can pass the basic benchmark test, but is not guaranteed to be correct.
Detailed explanation can be found in the document.md.