| 23 | | The |
| | 23 | * `civl verify` should return a value in the command line based on the error found (or 0 if no error was found). |
| | 24 | * Command line option to generate certain stats about a run (i.e. how many symbolic states occurred at each program location, how much branching occurred at each location, etc). |
| | 25 | * Be able to save states to memory (perhaps just at specific program points or when specific conditions hold) and later start CIVL back up from those intermediate states. That way issues that don't occur until deep into the state exploration (perhaps minutes or hours into a search) can be quickly returned to. |
| | 26 | * Tool for viewing and filtering explored state space: |
| | 27 | * `civl verify` would generate a state space file containing all states and transitions it explored (similar to how `-showStates` and `-showTransitions` works but just more compactly stored and with some extra metadata). |
| | 28 | * File can be "filtered" to only show states and transitions which reach (or are reachable from) some set of states. |
| | 29 | * Would either be implemented as a GUI for viewing and filtering these files or as a command line tool which takes as input a results file and parameters specifying how to filter the space, and then prints the filtered results. |
| | 49 | * No more dependent types in SARL. SARL will only support unbounded arrays. CIVL will simply encode bounded arrays as an unbounded array paired with an integer representing the arrays size. In other words, move the state out of the type and into the value. |
| | 50 | * Alternatively, SARL will only have bounded arrays with a concrete bound. However, I think you lose flexibility this way. |
| | 51 | * Prefer using static methods and variables over factory objects for object creation and manipulation. Less cruft this way (don't have to pass factories all over the place) and also discourages relying on stateful implementations which are more error prone and harder to debug. |
| | 52 | * Easier construction and manipulation of ASTs: |
| | 53 | * All new `ASTNode`s require a `Source` object which is very tedious to construct meaningfully. Most of the meaningful info (when creating new `ASTNode`s in a transformer) is in the `String` it is constructed with which could just be deduced from the `ASTNode` itself. |
| | 54 | * `ASTNode`s are immutable but the structure of an `AST` overall is not though, requiring the need to manage ownership of `ASTNode`s which can be hard to get right. |
| | 55 | |
