; @author Naoki Nishida 
(format LCTRS :smtlib 2.6)

(theory FixedSizeBitVectors)

(sort Loc)
(sort State)

(fun state (-> Loc Loc Bool Bool (_ BitVec 1) State))
(fun noncrit0 Loc)
(fun wait0 Loc)
(fun crit0 Loc)
(fun noncrit1 Loc)
(fun wait1 Loc)
(fun crit1 Loc)
(fun success State)
(fun error State)

(rule (state noncrit0 p1 b0 b1 x) (state wait0 p1 b01 b1 x1)
        :guard (and b01 (= x1 #b1)) :var ((x1 (_ BitVec 1))))
(rule (state wait0 p1 b0 b1 x) (state crit0 p1 b0 b1 x)
        :guard (or (= x #b0) (not b1)) :var ((x (_ BitVec 1))))
(rule (state crit0 p1 b0 b1 x) (state noncrit0 p1 b01 b1 x)
        :guard (not b01))
(rule (state p0 noncrit1 b0 b1 x) (state p0 wait1 b0 b11 x1)
        :guard (and b11 (= x1 #b0)) :var ((x1 (_ BitVec 1))))
(rule (state p0 wait1 b0 b1 x) (state p0 crit1 b0 b1 x)
        :guard (or (= x #b1) (not b0)) :var ((x (_ BitVec 1))))
(rule (state p0 crit1 b0 b1 x) (state p0 noncrit1 b0 b11 x)
        :guard (not b11))
(rule (state p0 p1 b0 b1 x) success)
(rule (state crit0 crit1 b0 b1 x) error)