Invariants shape how the solver looks for a viable solution. They are statements that are either assumed to be true or that we want the solver to disprove.
Fault has a couple of temporal logic operators that create SMT rules to test conditions across time. Fault is not as good at temporal logic as other languages specifically designed for it (TLA+ comes to mind), but it can handle some basic reasoning.
| ||At some point in the model runtime this assertion will be true|| |
| ||This assertion is always true (technically the default for all assertions)|| |
| ||When this assertion becomes true it will stay true for the rest of the model runtime|| |
| ||This assertion is true no more than n times|| |
| ||This assertion is true no fewer than n times|| |