An experimental framework for temporal verification based on first-order linear-time temporal logic. Our goal is to express transition systems in first-order logic and verify temporal correctness properties, including safety and liveness.
This adds a source-to-source translation that removes all non-boolean-returning relations. It also changes the todo!s in the checkers to panic!s and updates the checker code paths in command.rs.
This adds a source-to-source translation that removes all non-boolean-returning relations. It also changes the todo!s in the checkers to panic!s and updates the checker code paths in command.rs.