Commit bb32d548 authored by Christian Müller's avatar Christian Müller

example

parent 5cbd41fb
Signature Signature
EmptyPredicates EmptyPredicates: R(a:Ti,b:Tj), S(a:Ti, b:Tj)
R(a:T,b:T), S(a:T, b:T) AxiomPredicates: I(b:T)
AxiomPredicates As: A(b:Tj)
I(b:T) Bs: B(b:Ti)
As Constants: ca:Ti, cb:Tj
A(b:T)
Bs
B(b:T)
Constants
ca:T, cb:T
Transition System Transition System
loop { loop {
sim { sim {
R(a,b) := A(a,b) R(a,b) := A(b)
S(c,d) := R(a,b) S(c,d) := (R(ca,d) ∧ c = ca)
} }
S(a,b) := False S(a,b) := False
} }
Invariant Invariant
True ∀a:Ti,b:Tj. (R(a, b) ∧ (ca = a))
Axioms Axioms
True True
......
Signature
EmptyPredicates
R(a:R,b:S)
Constants
ca:T
Transition System
R(a,b) := R(ca,b)
Invariant
True
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment