Fair Transition Systems
A fair transition system is given by a set of transitions; each is a
first-order relation between the set of sytem variables and the
next-state system variables, indicating how the system can move from one
state to the next.
The next-state variables are the primed version of the system variables;
thus, for example, x' = x + 1 indicates that the value of the
system variable x is incremented by the transition.
For convenience, STeP provides a structured representation for
transitions with the following components:
- Enable: This is the enabling condition of the transition, a
state-formula that must be true in order for the transition to be
taken. It may not contain primed variables, and is by default "true".
- Assign: This lists the next-state values for variables that can be
given as an assignment, in the straightworward way.
- Modrel: The modifying relation.
This field is intended for those components of the
transition relation that cannot be expressed by any of the above.
It is an arbitrary relation (a first-order formula) over primed and
unprimed system variables, which is conjoined with the constraints
implied by the other fields.
Thus, it is expected to be consistent with those: for example,
variables that appear in the left-hand side of an assignment should not
appear primed in the modifying relation.
- Preloc, postloc: When parsing SPL programs, STeP adds
prelocation and postlocation fields to each transition, which indicate
how control is changed by the transition.
A transition that has more than one set of fields is taken to be the
disjunction of the constituent sub-transitions.
For instance, a while and if-then-else statements are
parsed into a transition with two sub-components,
corresponding to the truth-value of the
condition.
Fairness: Justice and Compassion
Transitions can be optionally marked as just or
compassionate.
A just transition cannot be continuously enabled without ever being
taken; compassionate transitions have the stronger requirement, that
they not be enabled infinitely often (but not necessarily continously)
without being taken.
These fairness requirements are not relevant when proving safety
properties, such as invariants, but have to be taken into account when
proving response or liveness properties.
By default, transitions have no fairness requirements.
Note that the SPL noncritical statetement has no fairness
requirements, while the critical statement is just.
step-comments@CS.Stanford.EDU