Commit 191b586
committed
this commit restructures the interaction generation in order to have
better counterexample minimization.
- it separates interaction plans from their state of execution
- it removes closures from the property definitions, encoding properties as an enum variant, and deriving the closures from the variants.
- it adds some naive counterexample minimization capabilities to the Limbo simulator and reduces the plan sizes considerably.
- it makes small changes to various points of the simulator for better error reporting, enhancing code readability, small fixes to handle previously missed cases1 parent cc56276 commit 191b586
11 files changed
+979
-501
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
4 | 4 | | |
5 | 5 | | |
6 | 6 | | |
| 7 | + | |
7 | 8 | | |
8 | 9 | | |
9 | 10 | | |
| |||
21 | 22 | | |
22 | 23 | | |
23 | 24 | | |
24 | | - | |
| 25 | + | |
25 | 26 | | |
26 | 27 | | |
27 | 28 | | |
| |||
0 commit comments