parseTest.spec 418 Bytes
Newer Older
1
Signature
Christian Müller's avatar
Christian Müller committed
2 3 4 5 6
    EmptyPredicates:    R(a:Ti,b:Tj), S(a:Ti, b:Tj)
    AxiomPredicates:    I(b:T)
    As:                 A(b:Tj)
    Bs:                 B(b:Ti)
    Constants:          ca:Ti, cb:Tj
7 8 9 10

Transition System
    loop {
        sim {
Christian Müller's avatar
Christian Müller committed
11 12
            R(a,b) := A(b)
            S(c,d) := (R(ca,d) ∧ c = ca)
13 14 15 16 17
        }
        S(a,b) := False
    }

Invariant
Christian Müller's avatar
Christian Müller committed
18
    ∀a:Ti,b:Tj. (R(a, b) ∧ (ca = a))
19 20 21 22

Axioms
    True