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 PR replaces the DNF based approach to translating flyvy modules to imperative programs with a pattern-matching based approach. This makes translation significantly faster; however, it comes at the cost of not being able to translate as many programs. This is worth it for now, as it lets us support running the paxos example.
@tchajed This PR will be hard to review, because there are a lot of changes. However, a lot of the lines of diffs come from reordering the things inside the file, which I have split off into it's own commit. You should verify that the first commit is just moving things around, and make your actual review using the rest of the commits. If the second commit is too large to review, let me know and I'll try to split it up.
This PR replaces the DNF based approach to translating flyvy modules to imperative programs with a pattern-matching based approach. This makes translation significantly faster; however, it comes at the cost of not being able to translate as many programs. This is worth it for now, as it lets us support running the paxos example.
@tchajed This PR will be hard to review, because there are a lot of changes. However, a lot of the lines of diffs come from reordering the things inside the file, which I have split off into it's own commit. You should verify that the first commit is just moving things around, and make your actual review using the rest of the commits. If the second commit is too large to review, let me know and I'll try to split it up.