Any model for sequential programming that contains both (demonic) nondeterminism and probabilism
must reveal the difference between these two well-known programs: the first assigns to some variable a
nondeterministic choice between Booleans and then assigns to a different variable a fair choice between
Booleans, whilst the second reverses the order by making the fair choice before the nondeterministic one.
The interest and subtlety of those programs lies in the fact that without probability, disjoint assignments
commute and so those programs might naively have been expected to be indistinguishable. Previous
relational models separate them by exploiting a complex definition of sequential composition. This
paper provides an alternative approach in which sequential composition is instead standard relational
composition. The technical contribution that enables that to be achieved expands the binary (initial-final)
state view of computation to incorporate a third state, the ‘original’ state which checkpoints the most
recent nondeterministic choice. That enables a nondeterministic choice to be made on the basis of past
probabilistic choices and so facilitates independent nondeterministic combinations to be chosen against
them. The resulting model has the standard relational model embedded in it by a Galois connection.