Wizard for specifying fairness assumptions in temporal verification

[vkhomenko]

Liveness properties of async systems typically require fairness assumptions. It would be useful to help users to specify such assumptions:

• one can scan the temporal formula to get the list of atomic propositions, which usually correspond to signal values or enabledness of signal edges;
• one can check (via Spot) if the property is a safety property (that does not require fairness assumptions) or a liveness property (that is likely to need fairness assumptions);
• one can often assume weak fairness for outputs;
• one can select / check whether the fairness should be weak or strong depending on whether there is a choice for the signal in question.