Commit 7f764497 authored by Christian Müller's avatar Christian Müller

strat files

parent 9601f1c5
......@@ -35,6 +35,7 @@ results/**/*.foltl
# Resulting invariants
results/**/*.invariants
results/**/*.strategies
results/**/*.dot
results/**/*.png
......
Strategies:
strategy for B(x1,p1): ¬ Conf(x1,p1) ∧ ∀ xat:A. ¬ Conf(xat,p1)
\ No newline at end of file
Strategies:
strategy for B(a1,b1,i1): ∀ n2:T. ((b1 = n2) ∨ ¬ Ile(b1,n2) ∨ ¬ Inext(a1,b1) ∨ ¬ (b1 = i1)) ∧ ∀ n3:T. (¬ Ibtw(b1,i1,n3) ∨ ¬ Ile(i1,n3) ∨ ¬ Inext(a1,b1))
\ No newline at end of file
Strategies:
strategy for B1(x1,p1): (∀ y:A. Conf(y,p1) ∨ ¬ Conf(x1,p1)) ∧ (Conf(x1,p1) ∨ ∀ x:A. ¬ Conf(x,p1)) ∧ (∀ y1:A. Conf(y1,p1) ∨ ¬ Conf(x1,p1))
\ No newline at end of file
Strategies:
strategy for B(a1,b1,i1): ∀ n2:T. ((b1 = n2) ∨ ¬ leq(b1,n2) ∨ ¬ next(a1,b1) ∨ ¬ (b1 = i1)) ∧ ∀ n3:T. (¬ btw(b1,i1,n3) ∨ ¬ leq(i1,n3) ∨ ¬ next(a1,b1))
\ No newline at end of file
Strategies:
strategy for B(a1,b1): ∀ n2:T. ((a1 = n2) ∨ ¬ leq(a1,n2) ∨ ¬ (a1 = b1)) ∧ ∀ n3:T. (¬ btw(b1,a1,n3) ∨ ¬ leq(a1,n3))
\ No newline at end of file
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