Commit 902d02c9 authored by Christian Müller's avatar Christian Müller

add universe

parent 44acea29
Workflow
forallmay x:A,p:P
True → Conf += (x,p)
forallmay x:A,p:P
!Conf(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)
Universe
a1:A,a2:A,p1:P,p2:P,r1:R
Target
Read(xat:A, pt:P, rt:R)
Causality
a:A
......@@ -14,9 +14,13 @@ object TSCLI extends App with LazyLogging {
FILE should be a path to a FO Safety Game Description File.
If --elimChoice is given, all A predicates are immediately eliminated, while otherwise they will be eliminated after termination of the fixpoint algorithm. (may affect performance)
With elimChoice turned off, that corresponds to A predicates not changing over time.
If --approxElim is given, second order quantifier elimination is further approximated by not computing CNF for formulas that are too large.
By default all A predicates are immediately eliminated from the precondition.
If --approxChoice is given, they will instead be eliminated only after termination
of the fixpoint algorithm. (may sometimes improve performance)
Turning approxChoice on corresponds to A predicates not changing over time
and being part of the AxiomPredicates.
If --approxElim is given, second order quantifier elimination is
further approximated by not computing CNF for formulas that are too large.
This achieves a tremendous speed boost at the cost of accuracy.
"""
......@@ -24,13 +28,13 @@ object TSCLI extends App with LazyLogging {
logger.info(usage)
} else {
var elim = false
var elimA = true
var approxelim = false
args.collect {
case "--elimChoice" => elim = true
case "--approxChoice" => elimA = false
case "--approxElim" => approxelim = true
}
val properties = InvProperties(stubborn = true, eliminateA = elim, approxElim = approxelim)
val properties = InvProperties(stubborn = true, eliminateA = elimA, approxElim = approxelim)
val file = args.last
......
......@@ -100,7 +100,6 @@ object Utils extends LazyLogging {
val elabdot = WFGraphEncoding.toDot(graph)(Map(), Set())
Utils.write(name, s"${filenames}_workflow.dot", elabdot)
val invspec = TSConverter.toInvariantSpec(spec, properties, inv)
val tsgraph = TSGraphEncoding.toGraph(invspec.ts)
val elabtsdot = TSGraphEncoding.toDot(tsgraph)(Map(), Set())
......@@ -114,9 +113,12 @@ object Utils extends LazyLogging {
val basename = name.split("/").last
val filenames = s"${basename}_$model${if (desc.isEmpty) "" else s"_$desc"}"
val fixspec = properties.universe.map(u =>
InvSpecInstantiator.instantiate(spec, u)
).getOrElse(spec)
val fixspec = spec.universe.map(u => {
val m = u.groupBy(_.typ)
logger.info(s"Instantiating spec for universe $m")
InvSpecInstantiator.instantiate(spec, m)
}).getOrElse(spec)
val (res, graph, labelling, provens, strategies, dot, time) =
InvariantChecker.checkInvariantFPLabelling(fixspec, properties)
......
......@@ -17,8 +17,10 @@ object WFCLI extends App with LazyLogging {
FILE should be a path to a Workflow Description File.
If --stubborn is given, all agents are assumed to be stubborn.
If --elimChoice is given, all choice predicates are immediately eliminated, while otherwise they will be eliminated after termination of the fixpoint algorithm. (may affect performance)
With elimChoice turned off, that corresponds to choice predicates not changing over time.
If --approxChoice is given, all A predicates will be eliminated only after termination
of the fixpoint algorithm. (may sometimes improve performance)
immediately eliminated from the precondition.
Turning approxChoice on corresponds to A predicates not changing over time.
If --approxElim is given, second order quantifier elimination is further approximated by not computing CNF for formulas that are too large.
This achieves a tremendous speed boost at the cost of accuracy.
"""
......@@ -28,14 +30,14 @@ object WFCLI extends App with LazyLogging {
} else {
var causal = true
var elim = false
var elimA = true
var approxelim = false
args.collect {
case "--stubborn" => causal = false
case "--elimChoice" => elim = true
case "--approxChoice" => elimA = false
case "--approxElim" => approxelim = true
}
val properties = InvProperties(stubborn = !causal, eliminateA = elim, approxElim = approxelim)
val properties = InvProperties(stubborn = !causal, eliminateA = elimA, approxElim = approxelim)
val file = args.last
......
......@@ -40,7 +40,7 @@ object TSConverter extends LazyLogging {
val ts = TransitionSystem(newsig, steps)
InvariantSpec(ts, spec.axioms, invgen(spec))
InvariantSpec(ts, spec.axioms, invgen(spec), spec.universe)
}
def everywhere(list: List[WFBlock],
......
......@@ -46,7 +46,10 @@ trait Spec {
def axioms: Formula
}
case class InvariantSpec(ts:TransitionSystem, axioms:Formula, inv:Formula) extends Spec {
case class InvariantSpec(ts:TransitionSystem,
axioms:Formula,
inv:Formula,
universe:Option[List[Var]] = None) extends Spec {
override def toString: String = {
s"InvSpec\n$ts\n\nAxioms\n${Utils.indentLines(axioms.toString)}\n\nInvariant\n${Utils.indentLines(inv.toString)}\n"
}
......
......@@ -22,7 +22,14 @@ object Workflow {
}
// TODO: make causals a set;
case class NISpec(w: Workflow, declass: Map[String, (List[Var], Formula)], axioms: Formula, target: Fun, causals:List[Var], inv: Option[Formula] = None) extends Spec with LazyLogging {
case class NISpec(
w: Workflow,
declass: Map[String, (List[Var], Formula)],
axioms: Formula,
target: Fun,
causals:List[Var],
inv: Option[Formula] = None,
universe:Option[List[Var]] = None) extends Spec with LazyLogging {
override def toString: String = {
s"NISpec\nWorkflow:\n$w\nDeclass:$declass\nTarget:$target"
}
......
......@@ -16,11 +16,10 @@ import scala.annotation.tailrec
case class InvProperties(stubborn:Boolean,
eliminateA:Boolean = true,
eliminateB:Boolean = true,
approxElim:Boolean = true,
universe:Option[Map[String, List[Var]]] = None) {
approxElim:Boolean = true) {
override def toString: String = {
s"InvProperties(stubborn=$stubborn, eliminateA=$eliminateA, eliminateB=$eliminateB," +
s"approxElim=$approxElim,universe:$universe)"
s"approxElim=$approxElim)"
}
}
object InvProperties {
......@@ -86,7 +85,7 @@ object InvariantChecker extends LazyLogging {
// take the edge with a minimum of following unproven edges excluding selfloops
// val next = toProve.minBy(edge => ((edge.target.outgoing.filter(t => t.target != t.source) -- proven).size))
// take the edge with maximum source node first
val nextEdge = if (properties.universe.isDefined) {
val nextEdge = if (spec.universe.isDefined) {
// counterexample mode: try to go to source
toProve.minBy(edge => edge.source.value)
} else {
......
......@@ -5,6 +5,7 @@ import de.tum.niwo.blocks._
import de.tum.niwo.foltl.FOLTL._
import ParserUtils._
import de.tum.niwo.parser.TransitionSystemParser.repsep
import de.tum.niwo.parser.WorkflowParser.{TYPEDVAR, repsep}
import scala.util.parsing.combinator.{PackratParsers, RegexParsers}
......@@ -44,8 +45,9 @@ object TransitionSystemParser extends RegexParsers
("Signature" ~> SIG) ~
("Transition System" ~> BLOCKLIST) ~
("Invariant" ~> repsep(TERM, ",")) ~
(("Universe" ~> repsep(TYPEDVAR, ","))?) ~
(("Axioms" ~> repsep(TERM, ","))?)^? {
case sig ~ blocks ~ invariants ~ axioms if {
case sig ~ blocks ~ invariants ~ universe ~ axioms if {
val infered = blocks.map(ParserUtils.inferBlockTypeFromSig(sig, _))
val predicates = allpredicates(infered)
......@@ -65,7 +67,7 @@ object TransitionSystemParser extends RegexParsers
val ts = TransitionSystem(sig, infered)
InvariantSpec(
ts, And.make(inferedaxioms), And.make(inferedinvs)
ts, And.make(inferedaxioms), And.make(inferedinvs), universe
)
}
}
......
......@@ -93,16 +93,17 @@ object WorkflowParser extends RegexParsers with PackratParsers with FormulaParse
"Workflow" ~! WORKFLOW ~
(("Declassify" ~> DECLASS)?) ~
(("Invariant" ~> repsep(TERM, ","))?) ~
(("Universe" ~> repsep(TYPEDVAR, ","))?) ~
("Target" ~> FUN) ~
(("Causality" ~> repsep(TYPEDVAR, ","))?) ^^ {
case _ ~ w ~ decl ~ inv ~ tar ~ causals => {
case _ ~ w ~ decl ~ inv ~ uni ~ tar ~ causals => {
// temporary typing sig
val sig = w.sig.copy(w.sig.as,
w.sig.constas,
w.sig.bs,
w.sig.preds,
w.sig.constants ++ tar.params ++ causals.toList.flatten)
NISpec(w, toMap(decl.toList), True, tar, causals.getOrElse(List()), inv.map(list => And.make(list.map(inferFormulaTypes(sig, _)))))
w.sig.constants ++ tar.params ++ causals.toList.flatten ++ uni.toList.flatten)
NISpec(w, toMap(decl.toList), True, tar, causals.getOrElse(List()), inv.map(list => And.make(list.map(inferFormulaTypes(sig, _)))), uni)
}
}
......
......@@ -139,7 +139,7 @@ class CCSSubmissionTest extends FlatSpec with LazyLogging {
}
it should "prove counterexample for conference" in {
val name = "omitting/conference"
val name = "omitting/conference_fixeduniverse"
val inv = (spec:NISpec) => {
val i = InvariantGenerator.invariantNoninterSingleBS(spec)
......@@ -147,17 +147,18 @@ class CCSSubmissionTest extends FlatSpec with LazyLogging {
FormulaFunctions.eliminateEq(reninv)
}
// universe = Some(
// Map(
// "A" -> List(Var("a1", "A"), Var("a2", "A")),
// "P" -> List(Var("p1", "P"), Var("p2", "P")),
// "R" -> List(Var("r1", "R"))
// )
// )
assert(!checkSafe(name, "", inv, InvProperties(
stubborn = false,
approxElim = false,
eliminateA = true,
universe = Some(
Map(
"A" -> List(Var("a1", "A"), Var("a2", "A")),
"P" -> List(Var("p1", "P"), Var("p2", "P")),
"R" -> List(Var("r1", "R"))
)
)
eliminateA = 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