Commit 115f9c07 authored by Christian Müller's avatar Christian Müller

fix tests, fix in/equalities, fix saturator

parent 6e31cd1c
Signature
EmptyPredicates: msg(a, b), leader(a)
AxiomPredicates: next(a, b), leq(a, b), btw(a, b, c)
As: -
Bs: -
Constants: -
Transition System
msg(a,b) := next(a,b)
loop {
leader(a) := msg(a, a)
msg(a,c) := ∃b. (next(b, c) ∧ msg(a, b) ∧ leq(b, a))
}
Invariant
∀n1,n2. (¬leader(n1) ∨ ¬leader(n2) ∨ n1 = n2),
∀n1,n2. (n1 = n2 ∨ ¬leader(n1) ∨ ¬leq(n1, n2)),
∀n1,n2. (n1 = n2 ∨ ¬msg(n1, n1) ∨ ¬leq(n1, n2)),
∀n1,n2,n3. (¬btw(n1,n2,n3) ∨ ¬msg(n2,n1) ∨ ¬leq(n2,n3))
Axioms
∀x. leq(x,x),
∀x,y,z. (¬leq(x,y) ∨ ¬leq(y,z) ∨ leq(x,z)),
∀x,y. (¬leq(x,y) ∨ ¬leq(y,x) ∨ x = y),
∀x,y. (leq(x,y) ∨ leq(y,x)),
∀x,y,z. (¬btw(x,y,z) ∨ btw(y,z,x)),
∀w,x,y,z. (¬btw(w,x,y) ∨ ¬btw(w,y,z) ∨ btw(w,x,z)),
∀w,x,y. (¬btw(w,x,y) ∨ ¬btw(w,y,x)),
∀w,x,y. (w = x ∨ w = y ∨ x = y ∨ btw(w, x, y) ∨ btw(w, y, x)),
∀a,b. (¬next(a,b) ∨ ∀x. (x = a ∨ x = b ∨ btw(a,b,x)))
Signature
EmptyPredicates: msg(a, b), leader(a)
AxiomPredicates: next(a, b), leq(a, b), btw(a, b, c)
As: -
Bs: B(a,b,i)
Constants: -
Transition System
msg(i,b) := ∃a. (next(a,b) ∧ B(a,b,i))
loop {
leader(a) := msg(a, a)
msg(a,c) := ∃b. (next(b, c) ∧ msg(a, b) ∧ leq(b, a))
}
Invariant
∀n1,n2. (¬leader(n1) ∨ ¬leader(n2) ∨ n1 = n2),
∀n1,n2. (n1 = n2 ∨ ¬leader(n1) ∨ ¬leq(n1, n2)),
∀n1,n2. (n1 = n2 ∨ ¬msg(n1, n1) ∨ ¬leq(n1, n2)),
∀n1,n2,n3. (¬btw(n1,n2,n3) ∨ ¬msg(n2,n1) ∨ ¬leq(n2,n3))
Axioms
∀x. leq(x,x),
∀x,y,z. (¬leq(x,y) ∨ ¬leq(y,z) ∨ leq(x,z)),
∀x,y. (¬leq(x,y) ∨ ¬leq(y,x) ∨ x = y),
∀x,y. (leq(x,y) ∨ leq(y,x)),
∀x,y,z. (¬btw(x,y,z) ∨ btw(y,z,x)),
∀w,x,y,z. (¬btw(w,x,y) ∨ ¬btw(w,y,z) ∨ btw(w,x,z)),
∀w,x,y. (¬btw(w,x,y) ∨ ¬btw(w,y,x)),
∀w,x,y. (w = x ∨ w = y ∨ x = y ∨ btw(w, x, y) ∨ btw(w, y, x)),
∀a,b. (¬next(a,b) ∨ ∀x. (x = a ∨ x = b ∨ btw(a,b,x)))
Signature
EmptyPredicates: msg(a, b), leader(a)
AxiomPredicates: next(a, b), leq(a, b), btw(a, b, c)
As: -
Bs: B(a,b)
Constants: -
Transition System
msg(a,b) := B(a,b)
loop {
leader(a) := msg(a, a)
msg(a,c) := ∃b. (next(b, c) ∧ msg(a, b) ∧ leq(b, a))
}
Invariant
∀n1,n2. (¬leader(n1) ∨ ¬leader(n2) ∨ n1 = n2),
∀n1,n2. (n1 = n2 ∨ ¬leader(n1) ∨ ¬leq(n1, n2)),
∀n1,n2. (n1 = n2 ∨ ¬msg(n1, n1) ∨ ¬leq(n1, n2)),
∀n1,n2,n3. (¬btw(n1,n2,n3) ∨ ¬msg(n2,n1) ∨ ¬leq(n2,n3))
Axioms
∀x. leq(x,x),
∀x,y,z. (¬leq(x,y) ∨ ¬leq(y,z) ∨ leq(x,z)),
∀x,y. (¬leq(x,y) ∨ ¬leq(y,x) ∨ x = y),
∀x,y. (leq(x,y) ∨ leq(y,x)),
∀x,y,z. (¬btw(x,y,z) ∨ btw(y,z,x)),
∀w,x,y,z. (¬btw(w,x,y) ∨ ¬btw(w,y,z) ∨ btw(w,x,z)),
∀w,x,y. (¬btw(w,x,y) ∨ ¬btw(w,y,x)),
∀w,x,y. (w = x ∨ w = y ∨ x = y ∨ btw(w, x, y) ∨ btw(w, y, x)),
∀a,b. (¬next(a,b) ∨ ∀x. (x = a ∨ x = b ∨ btw(a,b,x)))
...@@ -14,6 +14,7 @@ object Utils extends LazyLogging { ...@@ -14,6 +14,7 @@ object Utils extends LazyLogging {
val RESULTSFOLDER = "results" val RESULTSFOLDER = "results"
val DEBUG_MODE = true val DEBUG_MODE = true
val Z3CONTEXTELIM = false
def mkString[T](string: Iterable[T], start: String, mid: String, end: String): String = { def mkString[T](string: Iterable[T], start: String, mid: String, end: String): String = {
if (string.isEmpty) "" else string.mkString(start, mid, end) if (string.isEmpty) "" else string.mkString(start, mid, end)
...@@ -97,7 +98,7 @@ object Utils extends LazyLogging { ...@@ -97,7 +98,7 @@ object Utils extends LazyLogging {
Utils.write(name, s"${filenames}_workflow.dot", elabdot) Utils.write(name, s"${filenames}_workflow.dot", elabdot)
val invspec = TSConverter.toInvariantSpec(spec, properties, inv) val invspec = TSConverter.toInvariantSpec(spec, properties, inv)
check(name, desc, invspec, properties) infer(name, desc, invspec, properties)
} }
private def infer(name:String, desc:String, spec:InvariantSpec, properties:InvProperties):Boolean = { private def infer(name:String, desc:String, spec:InvariantSpec, properties:InvProperties):Boolean = {
......
package de.tum.niwo.blocks package de.tum.niwo.blocks
import de.tum.niwo.foltl.FOLTL.{And, Formula, Or} import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.Utils
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.foltl.FormulaFunctions import de.tum.niwo.foltl.FormulaFunctions
import de.tum.niwo.toz3.Z3BSFO
object Saturator { object Saturator extends LazyLogging {
def saturate(ts:TransitionSystem): TransitionSystem = { def saturate(ts:TransitionSystem): TransitionSystem = {
...@@ -25,6 +28,10 @@ object Saturator { ...@@ -25,6 +28,10 @@ object Saturator {
c ++ ineqs c ++ ineqs
} }
if (witheqs != clauses) {
logger.info(s"Saturation introduced equalities in CNF for guard $f")
}
// do not rewrap quantifiers here // do not rewrap quantifiers here
val cnfwitheqs = And.make(witheqs.map(Or.make)) val cnfwitheqs = And.make(witheqs.map(Or.make))
...@@ -40,12 +47,17 @@ object Saturator { ...@@ -40,12 +47,17 @@ object Saturator {
} }
c ++ ineqs c ++ ineqs
} }
val dnfwithineqs = Z3BSFO.simplifyBS(Or.make(withineqs.map(And.make)))
// val theta = dnfwithineqs.toCNF
val result = if (dnfclauses != withineqs) {
logger.warn(s"Saturation introduces inequalities for guard $f")
dnfwithineqs.toCNF
} else {
cnfwitheqs
}
val dnfwithineqs = Or.make(withineqs.map(And.make)) val newform = FormulaFunctions.rewrapQuantifiers(quantifiers, result).simplify
// val theta = dnfwithineqs.toCNF
// FIXME this should use theta if equalities would actually be introduced
val newform = FormulaFunctions.rewrapQuantifiers(quantifiers, cnfwitheqs).simplify
newform newform
} }
......
...@@ -8,6 +8,7 @@ import de.tum.niwo.invariants.{InvProperties, InvariantGenerator} ...@@ -8,6 +8,7 @@ import de.tum.niwo.invariants.{InvProperties, InvariantGenerator}
object TSConverter extends LazyLogging { object TSConverter extends LazyLogging {
// TODO: introduce more than one informedness depending on type?
// TODO: move stubbornness flag out of properties // TODO: move stubbornness flag out of properties
def toInvariantSpec(spec:NISpec, def toInvariantSpec(spec:NISpec,
properties:InvProperties, properties:InvProperties,
...@@ -19,14 +20,17 @@ object TSConverter extends LazyLogging { ...@@ -19,14 +20,17 @@ object TSConverter extends LazyLogging {
val elaboratefun = (b:SimpleWFBlock[_]) => elaborate(b, spec, properties) val elaboratefun = (b:SimpleWFBlock[_]) => elaborate(b, spec, properties)
val elaborated = everywhere(w.steps, elaboratefun) val elaborated = everywhere(w.steps, elaboratefun)
// FIXME: Add causals to constants, add informedness for causal agents
// Add causals to constants, add informedness for causal agents
val newsig = if (!properties.stubborn) { val newsig = if (!properties.stubborn) {
w.sig.copy( w.sig.copy(
preds = w.sig.preds + Fun(INFNAME, List(spec.target.params.head)), preds = w.sig.preds + Fun(INFNAME, List(spec.target.params.head)),
constants = spec.causals.toSet ++ spec.constants ++ w.sig.constants constants = spec.causals.toSet union spec.constants union w.sig.constants
) )
} else { } else {
w.sig w.sig.copy (
constants = spec.constants union w.sig.constants
)
} }
// Map WFLoop/Nondet to TSLoop/TSNondet // Map WFLoop/Nondet to TSLoop/TSNondet
...@@ -93,7 +97,9 @@ object TSConverter extends LazyLogging { ...@@ -93,7 +97,9 @@ object TSConverter extends LazyLogging {
val choice = Fun(b.pred.get, b.agents) val choice = Fun(b.pred.get, b.agents)
val first = b.agents.head val first = b.agents.head
if (first.typ == spec.target.params.head.typ) { val informableTypes = spec.target.params.head.typ :: spec.causals.map(_.typ)
if (informableTypes.contains(first.typ)) {
for (s <- b.steps) yield { for (s <- b.steps) yield {
val inner = if (properties.stubborn) { val inner = if (properties.stubborn) {
choice.in(T1) choice.in(T1)
......
...@@ -146,11 +146,14 @@ object FOTransformers extends LazyLogging { ...@@ -146,11 +146,14 @@ object FOTransformers extends LazyLogging {
val freeparams = B.params.map(p => FormulaFunctions.generateName(p, bounds.toSet)) val freeparams = B.params.map(p => FormulaFunctions.generateName(p, bounds.toSet))
val gkineq = for ((gk, gargs) <- gks.zip(Gargs); garg <- gargs) yield { val gkineq = for ((gk, gargs) <- gks.zip(Gargs); garg <- gargs) yield {
// Or.make(gk, ineq(garg, freeparams)) Or.make(gk, FormulaFunctions.ineq(garg, freeparams))
gk.parallelRename(garg, freeparams)
} }
val fsol:Formula = And.make(gkineq) // Simplify equalities
val boundvars = quantifiers.flatMap(_._2)
val simpler = for (clause <- gkineq) yield FormulaFunctions.simplifyInequalitiesFromCNFClause(boundvars, clause)
val fsol:Formula = And.make(simpler)
val fsolq = FormulaFunctions.rewrapQuantifiers(quantifiers, fsol) val fsolq = FormulaFunctions.rewrapQuantifiers(quantifiers, fsol)
val z3fsolq = Z3BSFO.simplifyBS(fsolq) val z3fsolq = Z3BSFO.simplifyBS(fsolq)
......
...@@ -90,10 +90,14 @@ object FormulaFunctions extends LazyLogging { ...@@ -90,10 +90,14 @@ object FormulaFunctions extends LazyLogging {
// case Or(t1, Neg(t2)) if t1 == t2 => True // case Or(t1, Neg(t2)) if t1 == t2 => True
// Equivalence // Equivalence <->
case Equiv(t1, t2) if t1 == t2 => True case Equiv(t1, t2) if t1 == t2 => True
case Equiv(v1:Var, v2:Var) if v1.name > v2.name => Equiv(v2, v1) case Equiv(v1:Var, v2:Var) if v1.name > v2.name => Equiv(v2, v1)
// Equality =
case Equal(t1, t2) if t1 == t2 => True
case Equal(v1:Var, v2:Var) if v1.name > v2.name => Equal(v2, v1)
// Double Temporals // Double Temporals
case Finally(Finally(t)) => Finally(t) case Finally(Finally(t)) => Finally(t)
case Globally(Globally(t)) => Globally(t) case Globally(Globally(t)) => Globally(t)
...@@ -723,4 +727,31 @@ object FormulaFunctions extends LazyLogging { ...@@ -723,4 +727,31 @@ object FormulaFunctions extends LazyLogging {
}.toSet }.toSet
And.make(eqs.toList) And.make(eqs.toList)
} }
def simplifyInequalitiesFromCNFClause(univ:List[Var], clause:Formula): Formula = {
@tailrec
def simp(f: Formula): Formula = {
// get equalities - second is always universally quantified
val ineqs = f.collect {
case Neg(Equal(v1: Var, v2: Var)) if univ.contains(v1) => List((v2, v1))
case Neg(Equal(v1: Var, v2: Var)) if univ.contains(v2) => List((v1, v2))
}
if (ineqs.nonEmpty) {
// pick the first one, replace v2 by v1
val (v1, v2) = ineqs.head
val repl = f.parallelRename(List(v2), List(v1))
// after renaming, remove the inequalities
val withouteq = repl.simplify
// continue
simp(withouteq)
} else {
f
}
}
simp(clause)
}
} }
\ No newline at end of file
...@@ -79,13 +79,13 @@ object Preconditions extends LazyLogging { ...@@ -79,13 +79,13 @@ object Preconditions extends LazyLogging {
// Assume untouched predicates empty // Assume untouched predicates empty
val untouchedprecond = precond.assumeEmpty(untouched.toList) val untouchedprecond = precond.assumeEmpty(untouched.toList)
val z3simpednewinv = Z3BSFO.simplifyBS(untouchedprecond) val z3simpednewinv = Z3BSFO.simplifyAE(untouchedprecond)
// If not diverged yet, remove annotations from all predicates since all copies are equal // If not diverged yet, remove annotations from all predicates since all copies are equal
// TODO: this is hyperproperty-specific // TODO: this is hyperproperty-specific
val removedannotations = if (!diverged) { val removedannotations = if (!diverged) {
val rels = spec.ts.sig.preds.map(_.name) val rels = spec.ts.sig.preds.map(_.name)
rels.foldRight(z3simpednewinv)((r, f) => Z3BSFO.simplifyBS(FormulaFunctions.removeAnnotation(f, r))) rels.foldRight(z3simpednewinv)((r, f) => Z3BSFO.simplifyAE(FormulaFunctions.removeAnnotation(f, r)))
} else { } else {
z3simpednewinv z3simpednewinv
} }
......
...@@ -28,6 +28,11 @@ object ParserUtils extends LazyLogging { ...@@ -28,6 +28,11 @@ object ParserUtils extends LazyLogging {
// Check arities and types // Check arities and types
val checks = for ((k, list) <- grouped) yield { val checks = for ((k, list) <- grouped) yield {
if (!sigtypes.isDefinedAt(k)) {
logger.error(s"Predicate $k not defined in the signature")
}
val sigtype = sigtypes(k) val sigtype = sigtypes(k)
val variables = list.map(_.params) val variables = list.map(_.params)
val types = variables.map(_.map(_.typ)) val types = variables.map(_.map(_.typ))
...@@ -138,7 +143,8 @@ object ParserUtils extends LazyLogging { ...@@ -138,7 +143,8 @@ object ParserUtils extends LazyLogging {
val map = predtypeMap(sig.preds ++ sig.as ++ sig.constas ++ sig.bs) val map = predtypeMap(sig.preds ++ sig.as ++ sig.constas ++ sig.bs)
val repl = (stmt.tuple.map(_.name).zip(map(stmt.fun)) ++ sig.constants.map(v => (v.name, v.typ))).toMap val repl = (stmt.tuple.map(_.name).zip(map(stmt.fun)) ++ sig.constants.map(v => (v.name, v.typ))).toMap ++
stmt.guard.boundVars.map(v => (v.name, v.typ)).toMap
def addTypes(tuple: List[Var]): List[Var] = { def addTypes(tuple: List[Var]): List[Var] = {
if (tuple.exists(v => !repl.isDefinedAt(v.name))) { if (tuple.exists(v => !repl.isDefinedAt(v.name))) {
......
...@@ -4,6 +4,7 @@ import com.typesafe.scalalogging.LazyLogging ...@@ -4,6 +4,7 @@ import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.blocks._ import de.tum.niwo.blocks._
import de.tum.niwo.foltl.FOLTL._ import de.tum.niwo.foltl.FOLTL._
import ParserUtils._ import ParserUtils._
import de.tum.niwo.parser.TransitionSystemParser.repsep
import scala.util.parsing.combinator.{PackratParsers, RegexParsers} import scala.util.parsing.combinator.{PackratParsers, RegexParsers}
...@@ -27,18 +28,19 @@ object TransitionSystemParser extends RegexParsers ...@@ -27,18 +28,19 @@ object TransitionSystemParser extends RegexParsers
stmt => SimpleTSBlock(List(stmt)) stmt => SimpleTSBlock(List(stmt))
} }
private def PREDLIST: Parser[Set[Fun]] = repsep(FUN,",") ^^ { l => l.toSet } private def PREDLIST: PackratParser[Set[Fun]] = rep1sep(FUN,",") ^^ { l => l.toSet } | "-" ^^^ {Set[Fun]()}
private def VARLIST: PackratParser[Set[Var]] = rep1sep(TYPEDVAR, ",") ^^ { l => l.toSet } | "-" ^^^ {Set[Var]()}
private def SIG:Parser[Signature] = private lazy val SIG:PackratParser[Signature] =
("EmptyPredicates:" ~> PREDLIST) ~ ("EmptyPredicates:" ~> PREDLIST) ~
("AxiomPredicates:" ~> PREDLIST) ~ ("AxiomPredicates:" ~> PREDLIST) ~
("As:" ~> PREDLIST) ~ ("As:" ~> PREDLIST) ~
("Bs:" ~> PREDLIST) ~ ("Bs:" ~> PREDLIST) ~
("Constants:" ~> repsep(TYPEDVAR, ",")) ^^ { ("Constants:" ~> VARLIST) ^^ {
case preds ~ constas ~ as ~ bs ~ consts => Signature(as, constas, bs, preds, consts.toSet) case preds ~ constas ~ as ~ bs ~ consts => Signature(as, constas, bs, preds, consts)
} }
private def SPEC: Parser[InvariantSpec] = private def SPEC: PackratParser[InvariantSpec] =
("Signature" ~> SIG) ~ ("Signature" ~> SIG) ~
("Transition System" ~> BLOCKLIST) ~ ("Transition System" ~> BLOCKLIST) ~
("Invariant" ~> repsep(TERM, ",")) ~ ("Invariant" ~> repsep(TERM, ",")) ~
...@@ -68,5 +70,5 @@ object TransitionSystemParser extends RegexParsers ...@@ -68,5 +70,5 @@ object TransitionSystemParser extends RegexParsers
} }
} }
def parseSpec(s: String): ParseResult[InvariantSpec] = parseAll(SPEC, s) def parseSpec(s: String): ParseResult[InvariantSpec] = parseAll(phrase(SPEC), s)
} }
...@@ -38,7 +38,7 @@ object Z3BSFO extends LazyLogging { ...@@ -38,7 +38,7 @@ object Z3BSFO extends LazyLogging {
val neg = Neg(f).simplify val neg = Neg(f).simplify
// Can only check universal things // Can only check AE things
if (!neg.isBS) { if (!neg.isBS) {
logger.error("Z3-BSFO: Trying to encode formula not in Bernays-Schönfinkel") logger.error("Z3-BSFO: Trying to encode formula not in Bernays-Schönfinkel")
} }
...@@ -60,20 +60,33 @@ object Z3BSFO extends LazyLogging { ...@@ -60,20 +60,33 @@ object Z3BSFO extends LazyLogging {
res res
} }
def simplifyAE(f: Formula): Formula = {
Neg(simplifyBS(Neg(f))).simplify
}
def simplifyBS(f: Formula): Formula = { def simplifyBS(f: Formula): Formula = {
simplifications += 1 simplifications += 1
logger.trace(s"Simplifying a formula with ${f.opsize} operators.") logger.trace(s"Simplifying a formula with ${f.opsize} operators.")
// Can only simplify BS things
if (!f.isBS) {
logger.error("Z3-BSFO: Trying to simplify formula not in Bernays-Schönfinkel")
}
val (ctx, _) = createContext() val (ctx, _) = createContext()
val tactics = if (Utils.Z3CONTEXTELIM) {
val simp = ctx.mkTactic("ctx-solver-simplify") val simp = ctx.mkTactic("ctx-solver-simplify")
val simp2 = ctx.mkTactic("simplify") val simp2 = ctx.mkTactic("simplify")
val params = ctx.mkParams() val params = ctx.mkParams()
params.add("mbqi", true) params.add("mbqi", true)
// params.add("mbqi.trace", true) params.add("mbqi.trace", true)
val tactics = ctx.andThen(simp, simp2)
simp.getSolver.setParameters(params) simp.getSolver.setParameters(params)
ctx.andThen(simp, simp2)
} else {
ctx.mkTactic("simplify")
}
// mkGoal (produce models, produce unsat cores, produce proofs) // mkGoal (produce models, produce unsat cores, produce proofs)
val goal = ctx.mkGoal(false, false, false) val goal = ctx.mkGoal(false, false, false)
......
...@@ -8,7 +8,7 @@ import de.tum.niwo.foltl.FOLTL._ ...@@ -8,7 +8,7 @@ import de.tum.niwo.foltl.FOLTL._
object Z3FOEncoding extends LazyLogging { object Z3FOEncoding extends LazyLogging {
val TIMEOUT = 60000 // in milliseconds val TIMEOUT = 10000 // in milliseconds
def translate(f: Formula, ctx: Context) = { def translate(f: Formula, ctx: Context) = {
// logger.info(s"Using formula:\n$f") // logger.info(s"Using formula:\n$f")
......
...@@ -20,8 +20,7 @@ class DemoNotebookTest extends FlatSpec { ...@@ -20,8 +20,7 @@ class DemoNotebookTest extends FlatSpec {
// assert(checkSafeCausal(name, "", inv)) // assert(checkSafeCausal(name, "", inv))
// } // }
// Last state: 24s, working it should "prove nonomitting/notebook causal elim with cnf building" in {
it should "prove nonomitting/notebook causal elim with cnf building" ignore {
val name = "nonomitting/notebook" val name = "nonomitting/notebook"
val inv = InvariantGenerator.invariantNoninterSingleBS _ val inv = InvariantGenerator.invariantNoninterSingleBS _
assert(checkSafe(name, "elim", inv, assert(checkSafe(name, "elim", inv,
...@@ -39,11 +38,17 @@ class DemoNotebookTest extends FlatSpec { ...@@ -39,11 +38,17 @@ class DemoNotebookTest extends FlatSpec {
it should "prove omitting/notebook_unsafe stubborn elim alleq" in { it should "prove omitting/notebook_unsafe stubborn elim alleq" in {
val name = "omitting/notebook_unsafe" val name = "omitting/notebook_unsafe"
val inv = InvariantGenerator.invariantAllEqual _ val inv = InvariantGenerator.invariantAllEqual _
assert(!checkSafeStubborn(name, "elim", inv)) assert(!checkSafe(name, "", inv, InvProperties(
stubborn = true,
approxElim = true
)))
} }
it should "prove omitting/notebook_unsafe causal elim alleq" in { it should "fail to prove omitting/notebook_unsafe causal elim alleq" in {
val name = "omitting/notebook_unsafe" val name = "omitting/notebook_unsafe"
val inv = InvariantGenerator.invariantNoninterSingleBS _ val inv = InvariantGenerator.invariantNoninterSingleBS _
assert(!checkSafeStubborn(name, "elim", inv)) assert(checkSafe(name, "", inv, InvProperties(
stubborn = false,
approxElim = true
)))
} }
} }
...@@ -11,22 +11,24 @@ import de.tum.niwo.Examples ...@@ -11,22 +11,24 @@ import de.tum.niwo.Examples
import de.tum.niwo.graphs.WFGraphEncoding._ import de.tum.niwo.graphs.WFGraphEncoding._
import de.tum.niwo.Utils import de.tum.niwo.Utils
import de.tum.niwo.graphs.WFGraphEncoding import de.tum.niwo.graphs.WFGraphEncoding
import de.tum.niwo.invariants.{InvariantChecker, InvariantGenerator, Preconditions} import de.tum.niwo.invariants.{InvProperties, InvariantChecker, InvariantGenerator, Preconditions}
import de.tum.niwo.tests.TestUtils._ import de.tum.niwo.tests.TestUtils._
@Ignore
class DemoUniversityTest extends FlatSpec { class DemoUniversityTest extends FlatSpec {
it should "prove nonomitting/university alleq" in { "Inference" should "prove nonomitting/university alleq" in {
val name = "nonomitting/university" val name = "nonomitting/university"
val inv = InvariantGenerator.invariantAllEqual _ val inv = InvariantGenerator.invariantAllEqual _
assert(checkSafeStubbornNoElim(name, inv)) assert(checkSafeStubborn(name, inv))
} }
it should "prove nonomitting/university causal alleq" in { it should "prove nonomitting/university causal" in {
val name = "nonomitting/university" val name = "nonomitting/university"
val inv = InvariantGenerator.invariantNoninterSingleBS _ val inv = InvariantGenerator.invariantNoninterSingleBS _
assert(!checkSafeCausalNoElim(name, "alleq", inv)) assert(!checkSafe(name, "", inv, InvProperties(
stubborn = false,
approxElim = true
)))
} }
} }
package de.tum.niwo.tests package de.tum.niwo.tests.papertests
import de.tum.niwo.foltl.FOLTL._ import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.invariants.InvProperties import de.tum.niwo.invariants.InvProperties
import de.tum.niwo.invariants.InvariantGenerator._
import de.tum.niwo.tests.TestUtils._ import de.tum.niwo.tests.TestUtils._
import org.scalatest.FlatSpec import org.scalatest.FlatSpec
import org.scalatest.Matchers._ import org.scalatest.Matchers._
import de.tum.niwo.invariants.InvariantGenerator._
class InferenceTests extends FlatSpec { class InferenceTests extends FlatSpec {
......
...@@ -54,19 +54,20 @@ class InvariantEasychairTest extends FlatSpec { ...@@ -54,19 +54,20 @@ class InvariantEasychairTest extends FlatSpec {
))) )))
} }
it should "prove causal conference accept without approxElim" in { // heap space
it should "fail to prove causal conference accept without approxElim" ignore {
val name = "nonomitting/conference-acceptance" val name = "nonomitting/conference-acceptance"
val inv = InvariantGenerator.invariantNoninterSingleBS _ val inv = InvariantGenerator.invariantNoninterSingleBS _
assert(checkSafe(name, "", inv, InvProperties( assert(!checkSafe(name, "", inv, InvProperties(
stubborn = false, stubborn = false,
approxElim = false approxElim = false
))) )))
} }
it should "prove causal conference accept with approxElim" in { it should "fail to prove causal conference accept with approxElim" in {
val name = "nonomitting/conference-acceptance" val name = "nonomitting/conference-acceptance"
val inv = InvariantGenerator.invariantNoninterSingleBS _ val inv = InvariantGenerator.invariantNoninterSingleBS _
assert(checkSafe(name, "", inv, InvProperties( assert(!checkSafe(name, "", inv, InvProperties(
stubborn = true, stubborn = true,
approxElim = true approxElim = true
))) )))
...@@ -93,14 +94,35 @@ class InvariantEasychairTest extends FlatSpec { ...@@ -93,14 +94,35 @@ class InvariantEasychairTest extends FlatSpec {
// assert(checkSafeStubborn(name, "with_elim", inv)) // assert(checkSafeStubborn(name, "with_elim", inv))
// } // }
// it should "prove omitting/conference_fixed" in { it should "prove omitting/conference_fixed without eliminating Aux" in {
// val name = "omitting/conference_fixed_stubborn" val name = "omitting/conference_fixed_stubborn"
// val xt = Var("xt", "A") val inv = InvariantGenerator.invariantNoninterSingleBS _
// val pt = Var("rt", "R") assert(checkSafe(name, "", inv, InvProperties(
// val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get) stubborn = true,
// assert(checkSafeStubbornNoElim(name, inv)) eliminateA = false,
// } approxElim = false
)))
}
// HEAP SPACE
it should "prove omitting/conference_fixed" ignore {
val name = "omitting/conference_fixed_stubborn"
val inv = InvariantGenerator.invariantNoninterSingleBS _
assert(checkSafe(name, "", inv, InvProperties(
stubborn = true,
approxElim = false