Invariants

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;
available	An unfunc's precondition is satisfiable from the initial state	assume f available;