UNCONSPROP
(d)
CONSPROP
(m1, i1, s1, w, r, t, m2, i2, s2,  m3, i3, s3,  m4, i4, s4, m5, i5, s5, m6, i6, s6, a1, a2, a3, a4, a5, a6)
CONSTRAINT
(= 1)+(m1, i1, s1)
(= 1)+(m2, i2, s2)
(= 1)+(m3, i3, s3)
(= 1)+(m4, i4, s4)
(= 1)+(m5, i5, s5)
(= 1)+(m6, i6, s6)
(= 1)+(w, r, t)
(= 1)+(a1, a2, a3, a4, a5, a6)
INIT
(i1)
(!i1 | !a1 | w | r)
(!s1 | !a1 | w | t)
(!m1 | !a1 | t)
(i2)
(!i2 | !a2 | w | r)
(!s2 | !a2 | w | t)
(!m2 | !a2 | t)
(i3)
(!i3 | !a3 | w | r)
(!s3 | !a3 | w | t)
(!m3 | !a3 | t)
(i4)
(!i4 | !a4 | w | r)
(!s4 | !a4 | w | t)
(!m4 | !a4 | t)
(i5)
(!i5 | !a5 | w | r)
(!s5 | !a5 | w | t)
(!m5 | !a5 | t)
(i6)
(!i6 | !a6 | w | r)
(!s6 | !a6 | w | t)
(!m6 | !a6 | t)
(!d | m1 | m2 | m3 | m4 | m5)
(!d | m1 | m2 | m3 | m4 | m6)
(!d | m1 | m2 | m3 | m5 | m6)
(!d | m1 | m2 | m4 | m5 | m6)
(!d | m1 | m3 | m4 | m5 | m6)
(!d | m2 | m3 | m4 | m5 | m6)
STEP
true => X (!d | m1 | m2 | m3 | m4 | m5)
true => X (!d | m1 | m2 | m3 | m4 | m6)
true => X (!d | m1 | m2 | m3 | m5 | m6)
true => X (!d | m1 | m2 | m4 | m5 | m6)
true => X (!d | m1 | m3 | m4 | m5 | m6)
true => X (!d | m2 | m3 | m4 | m5 | m6)
true => X(!i1 | !a1 | w | r)
true => X(!s1 | !a1 | w | t)
true => X(!m1 | !a1 | t)
(i1 & a1 & w) => X(m1)
(i1 & a1 & r) => X(s1)
(s1 & a1 & w) => X(m1)
(s1 & a1 & t) => X(s1)
(m1 & a1 & t) => X(m1)
true => X(!i2 | !a2 | w | r)
true => X(!s2 | !a2 | w | t)
true => X(!m2 | !a2 | t)
(i2 & a2 & w) => X(m2)
(i2 & a2 & r) => X(s2)
(s2 & a2 & w) => X(m2)
(s2 & a2 & t) => X(s2)
(m2 & a2 & t) => X(m2)
true => X(!i3 | !a3 | w | r)
true => X(!s3 | !a3 | w | t)
true => X(!m3 | !a3 | t)
(i3 & a3 & w) => X(m3)
(i3 & a3 & r) => X(s3)
(s3 & a3 & w) => X(m3)
(s3 & a3 & t) => X(s3)
(m3 & a3 & t) => X(m3)
true => X(!i4 | !a4 | w | r)
true => X(!s4 | !a4 | w | t)
true => X(!m4 | !a4 | t)
(i4 & a4 & w) => X(m4)
(i4 & a4 & r) => X(s4)
(s4 & a4 & w) => X(m4)
(s4 & a4 & t) => X(s4)
(m4 & a4 & t) => X(m4)
true => X(!i5 | !a5 | w | r)
true => X(!s5 | !a5 | w | t)
true => X(!m5 | !a5 | t)
(i5 & a5 & w) => X(m5)
(i5 & a5 & r) => X(s5)
(s5 & a5 & w) => X(m5)
(s5 & a5 & t) => X(s5)
(m5 & a5 & t) => X(m5)
true => X(!i6 | !a6 | w | r)
true => X(!s6 | !a6 | w | t)
true => X(!m6 | !a6 | t)
(i6 & a6 & w) => X(m6)
(i6 & a6 & r) => X(s6)
(s6 & a6 & w) => X(m6)
(s6 & a6 & t) => X(s6)
(m6 & a6 & t) => X(m6)
(i1 & !a1 & w) => X(i1)
(i1 & !a1 & r) => X(i1)
(i1 & !a1 & t) => X(i1)
(s1 & !a1 & w) => X(i1)
(s1 & !a1 & r) => X(s1)
(s1 & !a1 & t) => X(s1)
(m1 & !a1 & w) => X(i1)
(m1 & !a1 & r) => X(s1)
(m1 & !a1 & t) => X(m1)
(i2 & !a2 & w) => X(i2)
(i2 & !a2 & r) => X(i2)
(i2 & !a2 & t) => X(i2)
(s2 & !a2 & w) => X(i2)
(s2 & !a2 & r) => X(s2)
(s2 & !a2 & t) => X(s2)
(m2 & !a2 & w) => X(i2)
(m2 & !a2 & r) => X(s2)
(m2 & !a2 & t) => X(m2)
(i3 & !a3 & w) => X(i3)
(i3 & !a3 & r) => X(i3)
(i3 & !a3 & t) => X(i3)
(s3 & !a3 & w) => X(i3)
(s3 & !a3 & r) => X(s3)
(s3 & !a3 & t) => X(s3)
(m3 & !a3 & w) => X(i3)
(m3 & !a3 & r) => X(s3)
(m3 & !a3 & t) => X(m3)
(i4 & !a4 & w) => X(i4)
(i4 & !a4 & r) => X(i4)
(i4 & !a4 & t) => X(i4)
(s4 & !a4 & w) => X(i4)
(s4 & !a4 & r) => X(s4)
(s4 & !a4 & t) => X(s4)
(m4 & !a4 & w) => X(i4)
(m4 & !a4 & r) => X(s4)
(m4 & !a4 & t) => X(m4)
(i5 & !a5 & w) => X(i5)
(i5 & !a5 & r) => X(i5)
(i5 & !a5 & t) => X(i5)
(s5 & !a5 & w) => X(i5)
(s5 & !a5 & r) => X(s5)
(s5 & !a5 & t) => X(s5)
(m5 & !a5 & w) => X(i5)
(m5 & !a5 & r) => X(s5)
(m5 & !a5 & t) => X(m5)
(i6 & !a6 & w) => X(i6)
(i6 & !a6 & r) => X(i6)
(i6 & !a6 & t) => X(i6)
(s6 & !a6 & w) => X(i6)
(s6 & !a6 & r) => X(s6)
(s6 & !a6 & t) => X(s6)
(m6 & !a6 & w) => X(i6)
(m6 & !a6 & r) => X(s6)
(m6 & !a6 & t) => X(m6)
EVENTUALITY
F(d)
END