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

cleanup

parent 8d467f41
......@@ -2,11 +2,15 @@
Scala Implementation of the workflow language with loops published in CSF '17, CCS 18.
## How to use
## How to use (from code)
To generate LTL formulas from non-omitting workflows, have a look at ``MainLTL``.
To do First Order invariant inference, have a look at ``MainInvariantsInference``.
## How to use (from CLI)
Have a look at ``LTLCLI`` and ``InvariantCLI``.
## Parser
There is a working parser that can read the ``*.spec`` files in ``/examples``.
......
......@@ -19,6 +19,7 @@ object InvariantCLI extends App with LazyLogging {
FILE should be a path to a Workflow Description File.
If --causal is given, all agents are assumed to be causal, otherwise 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 (args.length == 0) {
......
......@@ -118,17 +118,11 @@ object Preconditions extends LazyLogging {
def weakestPrecondition(post: Formula, outerb: SimpleBlock, spec: Spec, properties: InvProperties) = {
val steps = elaborate(outerb, spec, properties)
// TODO: Make 2-trace elaboration optional
// elaborate only if non-stubborn
// val steps = if (!properties.stubborn) elaborateSteps(outerb, spec) else List(outerb)
val steps = elaborate(outerb, spec, properties)
val precond = steps.foldRight(post)((b, f) => {
// val innerb = if (b.isoracly) {
// elaborateOraclyBlock(b, spec)
// } else {
// b
// }
val innerprecond = weakestPreconditionSingle(f, b, spec, properties)
innerprecond
})
......@@ -157,14 +151,6 @@ object Preconditions extends LazyLogging {
def abstractedPrecondition(f: Formula, b: SimpleBlock, s: Spec, properties: InvProperties) = {
val precond = weakestPrecondition(f, b, s, properties)
// Stubborn agents -> remove trace variable from choice predicate
// Not neccessary anymore
// val stubprecond = if (stubborn) {
// precond.everywhere {
// case Fun(f, i, p) if b.may && f == b.pred.get => Fun(f, p)
// }
// } else precond
// Abstract away inner existentials - always if causal agents
val universalinv = if (!properties.stubborn || b.isomitting) {
FOTransformers.abstractExistentials(precond)
......@@ -181,10 +167,9 @@ object Preconditions extends LazyLogging {
// Win game
val bless = if (properties.eliminateB) {
val bs = (auxless.collect {
// FIXME: better recognition of Bs
case Fun(name, _, _) if name.startsWith("B") => List(name)
}).toSet
val bs = auxless.collect {
case f:Fun if f.isB() => List(f.name)
}.toSet
val eliminv = bs.foldRight(auxless)((b, inv) => FOTransformers.eliminateBPredicate(inv, b)._1)
eliminv
} else {
......
......@@ -127,6 +127,8 @@ object FOLTL {
def updatedParams(list: List[Var]) = Fun(name, ind, list)
def isOracle() = name.startsWith("O")
def isAux() = name.startsWith("choice")
def isB() = name.startsWith("B")
def encodeToVar() = {
val pi = if (ind.isDefined) "#" + ind.get else ""
......
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