Commit 26c68c19 authored by Christian Müller's avatar Christian Müller
Browse files

build file

parent 902d02c9
...@@ -38,8 +38,6 @@ packageOptions in assembly += Package.ManifestAttributes( ...@@ -38,8 +38,6 @@ packageOptions in assembly += Package.ManifestAttributes(
) )
test in assembly := {} test in assembly := {}
assemblyJarName in assembly := "niwo-ts.jar" assemblyJarName in assembly := "niwo-ts.jar"
mainClass in assembly := Some("de.tum.niwo.TSCLI") mainClass in assembly := Some("de.tum.niwo.TSCLI")
......
01:46:50.672 [ScalaTest-run-running-BarTest] INFO de.tum.niwo.foltl.FOTransformers$ -
Invariant: Only one glass(!) per person.
Allows barkeeper to hand out same glass with multiple drinks
BSFO SOQE: strategy for B1(x1,d2,g3):
∀ g1:G. (((g1 = g3) ∨ ¬ give(x1,g3) ∨ ¬ give(x1,g1)) ∧
∀ d1:D. (
((g1 = g3) ∨ ¬ give(x1,g1) ∨ ¬ pour(d2,g3)) ∧
((g1 = g3) ∨ ¬ pour(d1,g1) ∨ ¬ pour(d2,g3)) ∧
((g1 = g3) ∨ ¬ give(x1,g3) ∨ ¬ pour(d1,g1))))
Signature
EmptyPredicates: give(x:A, g:G), pour(d:D,g:G)
AxiomPredicates: -
As: A1(d:D,g:G)
Bs: B1(x:A,d:D,g:G)
Constants: -
Transition System
loop {
pour(d,g) := (pour(d,g) ∨ A1(d,g))
give(x,g) := (give(x,g) ∨ ∃d:D. (pour(d,g) ∧ B1(x,d,g)))
}
Invariant
∀x:A,g1:G,g2:G. (¬give(x,g1) ∨ ¬give(x,g2) ∨ (g1 = g2))
Signature
EmptyPredicates: give(x:A, g:G), pour(d:D,g:G)
AxiomPredicates: -
As: A1(d:D,g:G)
Bs: B1(x:A,d:D,g:G)
Constants: -
Transition System
loop {
pour(d,g) := (pour(d,g) ∨ A1(d,g))
give(x,g) := (give(x,g) ∨ ∃d:D. (pour(d,g) ∧ B1(x,d,g)))
}
Invariant
∀x:A,g1:G,g2:G. (¬give(x,g1) ∨ ¬give(x,g2) ∨ (g1 = g2))
Signature
EmptyPredicates: give(x:A, g:G), pour(d:D,g:G)
AxiomPredicates: -
As: A1(d:D,g:G)
Bs: B1(x:A,d:D,g:G)
Constants: -
Transition System
loop {
pour(d,g) := (pour(d,g) ∨ A1(d,g))
give(x,g) := (give(x,g) ∨ ∃ d:D. (pour(d,g) ∧
(∀ g1:G. ¬give(x,g1)) ∧
(∀g2:G,g3:G. ¬pour(d,g2) ∨ ¬pour(d,g3) ∨ (g2 = g3))))
}
Invariant
∀x:A,g1:G,g2:G. (¬give(x,g1) ∨ ¬give(x,g2) ∨ (g1 = g2))
(G(!p8|((((p0|p1)&Xp0)|(X!p0&!p0&!p1))&(((p6|p12)&Xp12)|(X!p12&!p6&!p12))&(((p2|p10)&Xp10)|(!p2&!p10&X!p10))&(((p5|p9)&Xp9)|(!p5&!p9&X!p9)))|X!p4)&!p0&!p3&!p4&!p7&!p9&!p10&!p11&!p12&!p13&p8&G(!p4|!p8)&F((!p9|!p13)&(p9|p13))&G(Xp4|!p8)&G(!p4|Xp4)&G(X!p4|(((Xp7&p7)|(X!p7&!p7))&((Xp3&p3)|(!p3&X!p3))&((X!p13&!p13)|(Xp13&p13))&((Xp11&p11)|(X!p11&!p11)))|!p4)&G(X!p4|(((p0&Xp0)|(!p0&X!p0))&((p10&Xp10)|(X!p10&!p10))&((p9&Xp9)|(X!p9&!p9))&((X!p12&!p12)|(Xp12&p12)))|!p4)&G(!p8|(((Xp7&(p1|p7))|(!p7&!p1&X!p7))&(((p6|p11)&Xp11)|(X!p11&!p6&!p11))&((Xp3&(p2|p3))|(X!p3&!p2&!p3))&(((p5|p13)&Xp13)|(!p5&!p13&X!p13)))|X!p4))
\ No newline at end of file
(!p4&!p2&!p1&!p0&G((((Xp4&p4)|(!p4&X!p4))&((p13&Xp13)|(!p13&X!p13))&((X!p1&!p1)|(Xp1&p1))&((p11&Xp11)|(!p11&X!p11)))|X!p2|!p2)&G((((X!p0&!p0)|(Xp0&p0))&((!p8&X!p8)|(p8&Xp8))&((p12&Xp12)|(!p12&X!p12))&((!p9&X!p9)|(p9&Xp9)))|X!p2|!p2)&(F(!p13&p8)|F(p13&!p8))&G(!p5|X!p2|((((p7|p1)&Xp1)|(!p7&X!p1&!p1))&((!p10&X!p13&!p13)|((p13|p10)&Xp13))&((!p11&!p10&X!p11)|((p11|p10)&Xp11))&((X!p4&!p4&!p7)|(Xp4&(p7|p4)))))&G(!p5|!p2)&G(!p5|X!p2|(((X!p8&!p3&!p8)|(Xp8&(p8|p3)))&((!p12&!p3&X!p12)|((p12|p3)&Xp12))&((Xp0&(p6|p0))|(!p0&!p6&X!p0))&(((p9|p6)&Xp9)|(!p6&X!p9&!p9))))&p5&G(Xp2|!p5)&!p13&!p12&!p11&G(Xp2|!p2)&!p9&!p8)
\ No newline at end of file
...@@ -114,7 +114,7 @@ object MainLTLWorkflows extends App with LazyLogging { ...@@ -114,7 +114,7 @@ object MainLTLWorkflows extends App with LazyLogging {
// clear() // clear()
// generateExample("nonomitting/conference") // generateExample("nonomitting/conference")
// generateExample("tests/declasstest") // generateExample("tests/declasstest")
generateExample("tests/simpleChoice") // generateExample("tests/simpleChoice")
// generateExample("tests/simpleChoiceNoOracle") // generateExample("tests/simpleChoiceNoOracle")
// generateAllExamples() generateAllExamples()
} }
\ No newline at end of file
import de.tum.niwo.foltl.FOLTL.Implies
import de.tum.niwo.{Examples, Utils}
import de.tum.niwo.invariants.InvProperties
import de.tum.niwo.parser.WorkflowParser
import de.tum.niwo.toz3.Z3BSFO
import org.scalatest.FlatSpec
class BarTest extends FlatSpec {
def check(name:String, properties:InvProperties):Boolean = {
val spec = Examples.parseExampleTS(name).get
Utils.check(name, "", spec, properties)
}
val properties = InvProperties(stubborn = true, eliminateA = true, eliminateB = true, approxElim = false)
"Bar example" should "be proven safe" in {
val name = "tstests/bar"
assert(check(name, properties))
}
"Bar example" should "be proven safe with strategy" in {
val name = "tstests/bar_strat"
assert(check(name, properties))
}
it should "prove strategy" in {
val strat1 = "((∀ g1:G. ¬give(x,g1)) ∧ (∀g2:G,g3:G. (¬pour(d,g1) ∨ ¬pour(d,g2) ∨ (g1 = g2))))"
val strat2 = "∀ g2:G. (((g2 = g3) ∨ ¬ give(x1,g3) ∨ ¬ give(x1,g2)) ∧ ∀ g1:G. (((g1 = g3) ∨ ¬ give(x1,g1) ∨ ¬ give(x1,g3)) ∧ ∀ d1:D. (((g2 = g3) ∨ ¬ give(x1,g3) ∨ ¬ pour(d1,g2)) ∧ ((g1 = g3) ∨ ¬ give(x1,g1) ∨ ¬ pour(d2,g3)) ∧ ((g2 = g3) ∨ ¬ give(x1,g2) ∨ ¬ pour(d2,g3)) ∧ ∀ d:D. (((g1 = g3) ∨ ¬ give(x1,g3) ∨ ¬ pour(d,g1)) ∧ ((g2 = g3) ∨ ¬ pour(d2,g3) ∨ ¬ pour(d1,g2)) ∧ ((g1 = g3) ∨ ¬ pour(d,g1) ∨ ¬ pour(d2,g3)) ∧ ((g2 = g3) ∨ ¬ give(x1,g3) ∨ ¬ give(x1,g2) ∨ ¬ pour(d1,g2)) ∧ ((g2 = g3) ∨ ¬ give(x1,g2) ∨ ¬ pour(d2,g3) ∨ ¬ pour(d1,g2)) ∧ ((g1 = g3) ∨ ¬ give(x1,g1) ∨ ¬ give(x1,g3) ∨ ¬ pour(d,g1)) ∧ ((g1 = g3) ∨ ¬ give(x1,g1) ∨ ¬ pour(d,g1) ∨ ¬ pour(d2,g3))))))"
val fstrat1 = WorkflowParser.parseFormula(strat1).get
val fstrat2 = WorkflowParser.parseFormula(strat2).get
println(Z3BSFO.checkAE(Implies(fstrat1, fstrat2)))
println(Z3BSFO.checkAE(Implies(fstrat2, fstrat1)))
}
}
\ No newline at end of file
Supports Markdown
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