specification sorts state; constants S0 : state; variables s, s0, s1, s2, s11, s22 : state; end specification