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

impl table:

parent bed7ccbd
......@@ -7,7 +7,7 @@ forallmay x:A,p:P
forall x:A,p:P,r:R
(Assign(x,p) ∧ Oracle(x,p,r)) → Review += (x,p,r)
loop {
forall xa:A,xb:A,p:P,r:R (Assign(xa,p) ∧ Review(xb,p,r)) → Read += (xa,r)
forall xa:A,xb:A,p:P,r:R (Assign(xa,p) ∧ Review(xb,p,r)) → Read += (xa,p,r)
forallmay x:A,p:P,r:R (Assign(x,p)) → Review += (x,p,r)
}
......@@ -17,7 +17,7 @@ Oracle(x:A,p:P,r:R): ¬ Conf(xat:A,p:P)
Target
Read(xat:A, rt:R)
Read(xat:A, p:P, rt:R)
Causality
......
Workflow
forallmay x:A,p:P
True → Conf += (x,p)
forallmay x:A,p:P
B(x,p) → Assign += (x,p)
forall x:A,p:P,r:R
(Assign(x,p) ∧ O(x,p,r)) → Review += (x,p,r)
loop {
forall x:A,y:A,p:P,r:R (Assign(x,p) ∧ Review(y,p,r)) → Read += (x,p,r)
forallmay x:A,p:P,r:R (Assign(x,p)) → Review += (x,p,r)
}
Declassify
O(x:A,p:P,r:R): ¬ Conf(xt:A,p:P)
Target
Read(xt:A, rt:R)
Workflow
forallmay x:A,p:P
True → Conf += (x,p)
forallmay x:A,p:P
B(x,p) → Assign += (x,p)
forall x:A,p:P,r:R
(Assign(x,p) ∧ Oracle(x,p,r)) → Review += (x,p,r)
forall xa:A,xb:A,p:P,r:R
(Assign(xa,p) ∧ Review(xb,p,r)) → Read += (xa,p,r)
forallmay x:A,p:P,r:R
(Assign(x,p)) → Review += (x,p,r)
forall xa:A,xb:A,p:P,r:R
(Assign(xa,p) ∧ Review(xb,p,r)) → Read += (xa,p,r)
forallmay x:A,p:P,r:R
(Assign(x,p)) → Review += (x,p,r)
Declassify
Oracle(x:A,p:P,r:R): ¬ Conf(xat:A,p:P)
Target
Read(xat:A, p:P, rt:R)
Causality
a:A
Workflow
forallmay x:A,p:P
True → Conf += (x,p)
forallmay x:A,p:P
B(x,p) → Assign += (x,p)
forall x:A,p:P,r:R
(Assign(x,p) ∧ Oracle(x,p,r)) → Review += (x,p,r)
loop {
forall xa:A,xb:A,p:P,r:R (Assign(xa,p) ∧ Review(xb,p,r)) → Read += (xa,p,r)
forallmay x:A,p:P,r:R (Assign(x,p)) → Review += (x,p,r)
}
Declassify
Oracle(x:A,p:P,r:R): ¬ Conf(xat:A,p:P)
Target
Read(xat:A, p:P, rt:R)
Causality
a:A
Signature
EmptyPredicates: Conf(x:A, p:P), Assign(x:A,p:P), Review(x:A,p:P,r:R), Read(x:A,p:P,r:R)
AxiomPredicates: -
As: A1(x:A,p:P), A2(x:A,p:P,r:R), A3(x:A,p:P,r:R)
Bs: B1(x:A,p:P)
Constants: -
Transition System
Conf(x,p) := A1(x,p)
Assign(x,p) := B1(x,p)
Review(x,p,r) := (Assign(x,p) ∧ ¬Conf(x,p) ∧ A2(x,p,r))
loop {
Read(x,p,r) := ∃y:A. (Assign(x,p) ∧ Review(y,p,r))
Review(x,p,r) := (Assign(x,p) ∧ ¬Conf(x,p) ∧ A3(x,p,r))
}
Invariant
∀x:A,p:P,r:R. ¬(Conf(x,p) ∧ Read(x,p,r))
......@@ -72,6 +72,8 @@ object FOTransformers extends LazyLogging {
if (eqs.nonEmpty) {
logger.trace(s"Introducing equalities while eliminating $AUX")
}
// TODO: add substitution for equalities
clause ++ eqs
}
......@@ -79,7 +81,7 @@ object FOTransformers extends LazyLogging {
FormulaFunctions.rewrapQuantifiers(quants, updatedcnf)
} else {
logger.debug(s"Approximating elimination of universal second order predicate $AUX")
logger.debug(s"Approximating elimination of universal second order predicate $AUX, not computing CNF")
// Saturated formula, no equalities anywhere
f
}
......
package de.tum.niwo.parser
import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.foltl.FOLTL
import de.tum.niwo.foltl.FOLTL._
import scala.util.matching.Regex
import scala.util.parsing.combinator.{PackratParsers, RegexParsers}
trait FormulaParser extends RegexParsers with PackratParsers with LazyLogging {
def IDENT = "[a-zA-Z][a-zA-Z0-9]*".r
def VAR = IDENT ^^ { str => Var(str) }
def TYPEDVAR = IDENT ~ ((":" ~> IDENT)?) ^^ { case str ~ typ => if (typ.isDefined) Var(str, typ.get) else Var(str) }
def IDENT: Regex = "[a-zA-Z][a-zA-Z0-9]*".r
def VAR: Parser[Var] = IDENT ^^ { str => Var(str) }
def TYPEDVAR: Parser[Var] = IDENT ~ ((":" ~> IDENT)?) ^^ { case str ~ typ => if (typ.isDefined) Var(str, typ.get) else Var(str) }
// logics
def tt = "True" ^^^ True
def ff = "False" ^^^ False
def AND = "(" ~> (repsep(TERM, "∧") | repsep(TERM, "&&")) <~ ")" ^^ (ts => And.make(ts))
def OR = "(" ~> (repsep(TERM, "∨") | repsep(TERM, "||")) <~ ")" ^^ (ts => Or.make(ts))
def NEG = ("¬" | "!") ~ SIMPLETERM ^^ { case _ ~ t => Neg(t) }
def IMPLIES = "(" ~> TERM ~ "⟹" ~ (TERM <~ ")") ^^ { case t1 ~ _ ~ t2 => Implies(t1, t2) }
def tt: Parser[FOLTL.True.type] = "True" ^^^ True
def ff: Parser[FOLTL.False.type] = "False" ^^^ False
def AND: Parser[Formula] = "(" ~> (repsep(TERM, "∧") | repsep(TERM, "&&")) <~ ")" ^^ (ts => And.make(ts))
def OR: Parser[Formula] = "(" ~> (repsep(TERM, "∨") | repsep(TERM, "||")) <~ ")" ^^ (ts => Or.make(ts))
def NEG: PackratParser[Neg] = ("¬" | "!") ~ TERM ^^ { case _ ~ t => Neg(t) }
def IMPLIES: Parser[Implies] = "(" ~> TERM ~ "⟹" ~ (TERM <~ ")") ^^ { case t1 ~ _ ~ t2 => Implies(t1, t2) }
// temporals
def GLOBALLY = ("G" | "☐") ~> TERM ^^ (t => Globally(t))
def FINALLY = ("F" | "♢") ~> TERM ^^ (t => Finally(t))
def GLOBALLY: Parser[Globally] = ("G" | "☐") ~> TERM ^^ (t => Globally(t))
def FINALLY: Parser[Finally] = ("F" | "♢") ~> TERM ^^ (t => Finally(t))
def TUPLE = "(" ~> repsep(TYPEDVAR, ",") <~ ")"
def FUN = VAR ~ TUPLE ^^ { case f ~ tup => Fun(f.name, tup) }
def EQ =
def TUPLE: Parser[List[Var]] = "(" ~> repsep(TYPEDVAR, ",") <~ ")"
def FUN: Parser[Fun] = VAR ~ TUPLE ^^ { case f ~ tup => Fun(f.name, tup) }
def EQ: Parser[Formula] =
(VAR <~ "=") ~ VAR ^^ { case v1 ~ v2 => Equal(v1, v2) } |
(VAR <~ "≠") ~ VAR ^^ { case v1 ~ v2 => Neg(Equal(v1, v2)) }
def EQUIV =
def EQUIV: Parser[Equiv] =
"(" ~> (SIMPLETERM <~ "<->") ~ (TERM <~ ")") ^^ { case t1 ~ t2 => Equiv(t1, t2) }
def EXISTS =
def EXISTS: Parser[Exists] =
"∃" ~> (repsep(TYPEDVAR, ",") <~ ("."?)) ~ TERM ^^ { case vs ~ t => Exists(vs, t) }
def FORALL =
def FORALL: Parser[Forall] =
"∀" ~> (repsep(TYPEDVAR, ",") <~ ("."?)) ~ TERM ^^ { case vs ~ t => Forall(vs, t) }
def QUANTIFIER:PackratParser[Formula] = EXISTS | FORALL
def SIMPLETERM = tt | ff | FUN | EQ
def SIMPLETERM: Parser[Formula] = tt | ff | FUN | EQ
lazy val TERM:PackratParser[Formula] = AND | OR | IMPLIES | NEG | SIMPLETERM | GLOBALLY | FINALLY | QUANTIFIER | EQUIV
def parseFormula(s:String) = parseAll(TERM, s)
def parseFormula(s:String): ParseResult[Formula] = parseAll(TERM, s)
}
package de.tum.niwo.tests.papertests
import de.tum.niwo.foltl.FOLTL.{Forall, Var}
import de.tum.niwo.invariants.InvariantGenerator.genEq
import de.tum.niwo.{Examples, Utils}
import de.tum.niwo.invariants.{InvProperties, InvariantGenerator}
import de.tum.niwo.tests.TestUtils.checkSafe
import org.scalatest.FlatSpec
class CCSSubmissionTest extends FlatSpec {
def checkTS(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)
"Single trace Easychair" should "be proven safe" in {
val name = "tstests/easychair_singletrace"
assert(checkTS(name, properties))
}
"Deterministic Leader election" should "be proven safe" in {
val name = "tstests/leaderelection_inductive"
assert(checkTS(name, properties))
}
it should "be proven safe with Bs" in {
val name = "tstests/leaderelection_inductive_withB"
assert(checkTS(name, properties))
}
it should "be proven safe with easier B" in {
val name = "tstests/leaderelection_inductive_withB2"
assert(checkTS(name, properties))
}
"Easychair" should "prove stubborn conference" in {
val name = "omitting/conference_stubborn"
val inv = InvariantGenerator.invariantNoninterSingleBS _
checkSafe(name, "", inv, InvProperties(
stubborn = true,
approxElim = false
))
}
it should "prove stubborn conference with B" in {
val name = "omitting/conference_stubborn_withB"
val inv = InvariantGenerator.invariantNoninterSingleBS _
checkSafe(name, "", inv, InvProperties(
stubborn = true,
approxElim = false
))
}
it should "prove linear causal stuff with B safe" in {
val name = "tests/conference_linear_small_withB"
val xt = Var("xt","X")
val yt = Var("yt","X")
val pt = Var("pt","P")
// val rt = Var("rt","R")
val inv = Forall(List(xt, pt, yt), genEq("Comm", List(xt, yt, pt)))
assert(checkSafe(name, "", _ => inv,
InvProperties(stubborn = false, approxElim = false)))
}
// it should "fail to prove causal conference with approxElim" in {
// val name = "omitting/conference"
// val inv = InvariantGenerator.invariantNoninterSingleBS _
// assert(checkSafe(name, "", inv, InvProperties(
// stubborn = false,
// approxElim = true
// )))
// }
it should "prove causal unrolled conference with approxElim" in {
val name = "omitting/conference_unrolled_withB"
val inv = InvariantGenerator.invariantNoninterSingleBS _
assert(checkSafe(name, "", inv, InvProperties(
stubborn = false,
approxElim = true
)))
}
// terminates, but gives strategy False
it should "prove causal conference with approxElim" in {
val name = "omitting/conference_withB"
val inv = InvariantGenerator.invariantNoninterSingleBS _
assert(checkSafe(name, "", inv, InvProperties(
stubborn = false,
approxElim = true
)))
}
it should "prove stubborn omitting/conference_linear_fixed" in {
val name = "omitting/conference_linear_fixed"
val inv = InvariantGenerator.invariantNoninterSingleBS _
assert(checkSafe(name, "", inv, InvProperties(
stubborn = true,
approxElim = false
)))
}
it should "prove causal omitting/conference_linear_fixed" in {
val name = "omitting/conference_linear_fixed"
val inv = InvariantGenerator.invariantNoninterSingleBS _
assert(checkSafe(name, "", inv, InvProperties(
stubborn = false,
approxElim = false
)))
}
}
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