Module defs

vstd_extra::temporal_logic

Module defs 

Source

Structs§

ActionPred
Execution
StatePred
TempPred

Functions§

always
enabled
eventually
false_pred
later
lift_action
lift_state
lift_state_exists
lift_state_forall
lift_state_prime
not
stable
tla_exists
tla_forall
true_pred
valid
weak_fairness