specification sorts systemstate comment: Rushby's state;; constants initialstate : systemstate; comment: Rushby's s0; variables sys, sys0, sys1 : systemstate; end specification