easychair_singletrace.spec 586 Bytes
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
Signature
    EmptyPredicates:    Conf(x:A, p:P), Assign(x:A,p:P), Review(x:A,p:P,r:R), Read(x:A,p:P,r:R)
    AxiomPredicates:    -
    As:                 A1(x:A,p:P), A2(x:A,p:P,r:R), A3(x:A,p:P,r:R)
    Bs:                 B1(x:A,p:P)
    Constants:          -

Transition System
	Conf(x,p) := A1(x,p)
	Assign(x,p) := B1(x,p)
	Review(x,p,r) := (Assign(x,p) ∧ ¬Conf(x,p) ∧ A2(x,p,r))
	loop {
	    Read(x,p,r) := ∃y:A. (Assign(x,p) ∧ Review(y,p,r))
	    Review(x,p,r) := (Assign(x,p) ∧ ¬Conf(x,p) ∧ A3(x,p,r))
	}

Invariant
	∀x:A,p:P,r:R. ¬(Conf(x,p) ∧ Read(x,p,r))