Skip to main content Link Menu Expand (external link) Document Search Copy Copied


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.

Temporal Logic

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.

Operator Definition Use
eventually At some point in the model runtime this assertion will be true assert x eventually;
always This assertion is always true (technically the default for all assertions) assert x always;
eventually-always When this assertion becomes true it will stay true for the rest of the model runtime assert x eventually-always;
nmt n This assertion is true no more than n times assert x nmt 2;
nft n This assertion is true no fewer than n times assert x nft 2;

Table of contents