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

add owl, transformers, tests

parent 7c277482
......@@ -24,6 +24,9 @@ build
.settings/
/bin/
# Idea
.idea/
# Resulting ltl formulas
results/*.ltl
results/*.ppltl
......
This diff is collapsed.
This diff is collapsed.
# Invariants Tool
This is an implementation accompanying the anonymous submission 47.
It can be used to verify and infer universal invariants for workflows.
## Prerequisites
The tool is built to be run by the JVM.
It needs an installed Z3 SMT Solver on the machine. There are bindings included for version 4.5.1, which can be replaced by specifying an additional classpath entry containing the new bindings.
## Usage
It can be called with `java -jar invariants.jar [--causal] [--elimChoice] FILE`
It will then try to parse the FILE to a workflow specification, build an equality invariant for a single relation (namely the one mentioned as TARGET in the specification) and try to infer the strongest universal invariant that implies this invariant.
When finished, all intermediate proving steps will be documented in the `results` folder and can be visualized by using the included `renderpngs.sh` script.
## Timings
The given implementation may differ from the time indicated in the paper for various reasons.
This release version will always build the invariant for just the target relation, instead of the conjunction over all relations.
The numbers in the paper have been produced by comparing the sum of all separate runtimes for all possible target relations with the invariant that is a conjunction for all target relations, choosing the minimum.
Also, depending on the workflow, the `elimChoice` configuration variable may improve runtimes significantly in some cases.
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) ∧ 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, pt:P, rt:R)
Workflow
forallmay x:A,p:P
True → Conf += (x,p)
forallmay x:A,p:P
!Conf(x,p) → Assign += (x,p)
forall x:A,y:A,p:P,q:P
(Assign(x,p) ∧ Assign(y,p) ∧ Conf(x,q) ∧ !Conf(y,q)) → Assign -= (y,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,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:X,p:P
True -> Conf += (x,p)
forallmay x:X,p:P
!Conf(x,p) -> Assign += (x,p)
forall x:X,p:P,r:R
(Assign(x,p) ∧ O(x,p,r)) -> Read += (x,p,r)
forallmay y:X,x:X,p:P
(Assign(x,p) ∧ Assign(y,p)) -> Comm += (x,y,p)
Declassify
O(x:X,p:P,r:R): ¬ Conf(a:X,p:P)
Target
Comm(a:X, b:X, pp:P)
Workflow
forallmay x:X,p:P
True -> Conf += (x,p)
forallmay x:X,p:P
!Conf(x,p) -> Assign += (x,p)
forall x:X,y:X,p:P,q:P
(Conf(x,p) ∧ ¬ Conf(y,p) ∧ Assign(x,q) ∧ Assign(y,q)) -> Assign -= (y,q)
forall x:X,p:P,r:R
(Assign(x,p) ∧ O(x,p,r)) -> Read += (x,p,r)
forallmay y:X,x:X,p:P
(Assign(x,p) ∧ Assign(y,p)) -> Comm += (x,y,p)
Declassify
O(x:X,p:P,r:R): ¬ Conf(a:X,p:P)
Target
Comm(a:X, b:X, pp:P)
Workflow
forallmay x,s
O(s) -> R += (x,s)
Target
R(x,s)
Workflow
forall x
True -> R += (x)
forall x,s
O(x,s) -> S += (x)
Declassify
O(x,s): R(xt)
Target
S(xt)
Workflow
forall x:X,s:S
O(s) -> R += (x,s)
Target
R(x:X,s:S)
Workflow
forallmay x,s O(s) -> Q += (x,s)
loop {
forall x,y,s R(y,s) -> S += (x,y,s)
forall x,s Q(x,s) -> R += (x,s)
}
Target
S(x,y,s)
Workflow
forall x,s
O(x,s) -> R += (x,s)
Target
R(x,s)
shopt -s nullglob
TIMEOUT=1m
for FILE in results/*.dot
do
NAME=$(basename ${FILE} .dot)
DIR=$(dirname "${FILE}")
PIC="${DIR}/${NAME}.png"
echo "Rendering ${FILE} to ${PIC}"
if
timeout ${TIMEOUT} time -p dot -Tpng < ${FILE} >> ${PIC}
then
echo "Finished successfully"
else
echo "Timeout after ${TIMEOUT}"
fi
done
......@@ -2,9 +2,9 @@ name := "LoopingWorkflows"
version := "0.1"
scalaVersion := "2.12.3"
scalaVersion := "2.12.6"
EclipseKeys.withBundledScalaContainers := false
// EclipseKeys.withBundledScalaContainers := false
libraryDependencies ++= Seq(
"com.typesafe.scala-logging" %% "scala-logging" % "3.5.0",
......
Workflow
forall x,s
True -> R -= (x)
forall x,s
O(x,s) -> R += (x)
......
package de.tum.workflows
import scala.io.Source
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.blocks.Spec
import java.io.File
import de.tum.workflows.foltl.Properties
import de.tum.workflows.ltl.FOTransformers
import de.tum.workflows.owl.OwlTransformer
object LTLCLI extends App with LazyLogging {
val MAXAGENTS = 8
lazy val usage = """
Usage niwo-ltl.jar [--stubborn] FILE
FILE should be a path to a Workflow Description File.
If --stubborn is given, all agents are assumed to be stubborn, regardless of the workflow specification.
"""
if (args.length == 0) {
logger.info(usage)
} else {
var stubborn = false
args.collect {
case "--stubborn" => stubborn = true
}
val file = args.last
logger.info(s"Using $file")
val source = Source.fromFile(file).mkString
val spec = WorkflowParser.parseSpec(source)
if (!spec.successful) {
logger.error(s"Parsing of $file unsuccessful: $spec")
None
} else {
if (!spec.get.checkSanity()) {
logger.error(s"Sanity check of $file failed. Skipping file.")
None
} else {
Some(spec.get)
}
}
spec.map(generate(new File(file).getName.stripSuffix(".spec"), _, stubborn))
}
def generate(name: String, spec: Spec, onlystubborn: Boolean) {
logger.info(s"Encoding Spec:\n$spec")
if (spec.w.isomitting) {
logger.info("Omitting spec - no embedding in LTL possible")
} else {
logger.info("Nonomitting spec - embedding FOLTL formula in LTL")
val foltlprop = if (onlystubborn || spec.causals.isEmpty) {
logger.info(s"Computing noninterference for target ${spec.target} using only stubborn agents")
Properties.noninterStubborn(spec)
} else {
logger.info(s"Computing noninterference for target ${spec.target} using causal agents ${spec.causals}")
Properties.noninterCausal(spec)
}
logger.info(s"Built FOLTL prop with size ${foltlprop.opsize()}")
val (agents, res) = FOTransformers.eliminateExistentials(foltlprop)
val universe = agents.map(_.withType()).mkString(", ")
logger.info(s"Using universe $universe")
if (agents.groupBy(_.typ).exists(_._2.size > MAXAGENTS)) {
logger.error(s"Universe has more than $MAXAGENTS agents for a single type. Aborting.")
return
}
val quantfree = FOTransformers.eliminateUniversals(res, agents)
val ltlprop = FOTransformers.eliminatePredicates(quantfree)
logger.info(s"Built LTL property with size ${ltlprop.opsize()}")
val owlprop = OwlTransformer.toOwl(ltlprop)
}
}
}
\ No newline at end of file
......@@ -28,7 +28,6 @@ object FormulaFunctions extends LazyLogging {
free(t, Set())
}
@tailrec
def simplify(t: Formula): Formula = {
val simp: PartialFunction[Formula, Formula] = {
// Push negation inward
......@@ -72,6 +71,13 @@ object FormulaFunctions extends LazyLogging {
case Or(t1, Or(t2, t3)) if (t1 == t2) => Or(t1, t3)
case Or(t1, Or(t2, t3)) if (t1 == t3) => Or(t1, t2)
// And Or
case And(t1, Or(t2, t3)) if (t1 == t3) => t1
case And(t1, Or(t2, t3)) if (t1 == t2) => t1
case And(Or(t2, t3), t1) if (t1 == t3) => t1
case And(Or(t2, t3), t1) if (t1 == t2) => t1
// case Or(t1, Neg(t2)) if t1 == t2 => True
// Equivalence
......@@ -107,8 +113,9 @@ object FormulaFunctions extends LazyLogging {
// make(qmake(xs, t1), t2)
}
val (changed, t1) = everywhereFP(simp, t)
if (!changed) t1 else simplify(t1)
// val (changed, t1) = everywhereFP(simp, t)
// if (!changed) t1 else simplify(t1)
everywhereBotUp(simp, t)
}
def eliminateImplication(f: Formula): Formula = {
......@@ -164,6 +171,7 @@ object FormulaFunctions extends LazyLogging {
}
def everywhereBotUp(trans: PartialFunction[Formula, Formula], t: Formula): Formula = {
// First apply trans to push negation inward etc
if (trans.isDefinedAt(t))
everywhereBotUp(trans, trans(t))
else {
......@@ -174,7 +182,11 @@ object FormulaFunctions extends LazyLogging {
case BinOp(make, t1, t2) => make(everywhereBotUp(trans, t1), everywhereBotUp(trans, t2))
case x => x
}
sub
// Applicable after inner transformation?
if (trans.isDefinedAt(sub))
trans(sub)
else
sub
}
}
......
package de.tum.workflows.owl
import scala.collection.JavaConversions._
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.foltl.FOLTL
import de.tum.workflows.foltl.FOLTL._
import owl.ltl._
object OwlTransformer extends LazyLogging {
case class IndexedVariable(v:Var, index:Int) extends FOLTL.Formula
def namemapping(f:FOLTL.Formula) = {
val names = f collect {
case Var(name, typ) => List(name)
}
val namelist = names.toSet[String].toList
val indexmap = namelist.zipWithIndex.toMap
val repl = f everywhere {
case v:Var => IndexedVariable(v, indexmap(v.name))
}
val reversemap = indexmap map { _.swap }
(reversemap, namelist, repl)
}
def toOwl(f:FOLTL.Formula): owl.ltl.LabelledFormula = {
val (reversemap, namelist, indexedformula) = namemapping(f)
val owlform = transform(indexedformula)
val named = LabelledFormula.of(owlform, namelist)
named
}
def transform(f:FOLTL.Formula): owl.ltl.Formula = {
f match {
case Fun(name, ind, params) => {
logger.error("Trying to encode function symbols into OWL Formula")
BooleanConstant.FALSE
}
case q: FOLTL.Quantifier => {
logger.error("Trying to encode quantifiers into OWL Formula")
BooleanConstant.FALSE
}
case Globally(f1) =>
GOperator.of(transform(f1))
case Finally(f1) =>
FOperator.of(transform(f1))
case Until(f1, f2) => {
val e1 = transform(f1)
val e2 = transform(f2)
UOperator.of(e1, e2)
}
case Next(f1) =>
XOperator.of(transform(f1))
case And(f1, f2) => {
val e1 = transform(f1)
val e2 = transform(f2)
Conjunction.of(e1, e2)
}
case Eq(f1, f2) => {
val e1 = transform(f1)
val e2 = transform(f2)
Biconditional.of(e1, e2).nnf()
}
case Or(f1, f2) => {
val e1 = transform(f1)
val e2 = transform(f2)
Disjunction.of(e1, e2)
}
case Implies(f1, f2) => {
val e1 = transform(f1)
val e2 = transform(f2)
// TODO: is there a better way?
Disjunction.of(e1.not(), e2)
}
case Neg(f1) =>
transform(f1).not()
case True =>
BooleanConstant.TRUE
case False =>
BooleanConstant.FALSE
case IndexedVariable(v, i) =>
Literal.of(i, false)
}
}
}
......@@ -22,7 +22,9 @@ object Test extends App {
// val easyform = And(Fun("p", List("x")), Neg(Fun("p", List("x"))))
// simp(easyform)
// simp(And(Or(Fun("a", List()), Fun("b", List())), Fun("a", List())))
val t = (And(Or(Fun("a", List()), Fun("b", List())), Fun("a", List()))).simplify()
println(t)
//
// simp(Eq(Fun("A", List("x")), Fun("A", List("y"))))
// simp(False)
......
......@@ -3,9 +3,9 @@ package de.tum.workflows.ltl.tests
import org.scalatest.FlatSpec
import org.scalatest.Matchers._
import org.scalatest.Inspectors._
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.Implicits._
import de.tum.workflows.foltl.FOLTL
class FOLTLTest extends FlatSpec {
"Formulas" should "be constructed correctly" in {
......@@ -31,11 +31,28 @@ class FOLTLTest extends FlatSpec {
val t = Forall("x", Fun("S", "x"))
And(t, t).simplify() should be (t)
}
it should "simplify double negation" in {
Neg(Neg(True)).simplify() should be(True)
}
it should "double negation inside quantification" in {
Forall("x", Neg(Neg(Var("x")))).simplify() should be (Forall("x", Var("x")))
}
it should "simplify trivial stuff" in {
And(True, Var("y")).simplify() should be (Var("y"))
}
it should "simplify more trivial stuff" in {
And(False, Var("y")).simplify() should be (False)
}
it should "simplify even more trivial stuff" in {
And(Or(False, False), Var("y")).simplify() should be (False)
}
it should "simplify quantors" in {
val f = And(Forall("x", Fun("f", "x")), Forall("x", Fun("f", "x")))
f.simplify() should be (Forall("x", Fun("f", "x")))
......
......@@ -36,16 +36,16 @@ class InvariantTest extends FlatSpec {
// safe should be(true)
// }
// "InvariantChecker" should "prove simple things safe" in {
//
// val wf = ExampleWorkflows.parseExample("tests/simpleChoiceNoOracle").get.w
//
// val inv = Forall(List("a", "b"), Eq(Fun("R", Some("t1"), List("a", "b")), Fun("R", Some("t2"), List("a", "b"))))
//
// val (safe, msg) = InvariantChecker.checkInvariantFP(wf, inv, true)
//
// safe should be(true)
// }
"InvariantChecker" should "prove simple things safe" in {
val spec = ExampleWorkflows.parseExample("tests/simpleChoiceNoOracle").get
val inv = Forall(List("a", "b"), Eq(Fun("R", Some("t1"), List("a", "b")), Fun("R", Some("t2"), List("a", "b"))))
val (safe, msg) = InvariantChecker.checkInvariantFP(spec, inv)
safe should be(true)
}
//
// it should "fail to prove unsafe workflows safe" in {
//
......
package de.tum.workflows.ltl.tests
import java.util
import java.util.EnumSet
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.owl.OwlTransformer
import org.scalatest.FlatSpec
import org.scalatest.Matchers._
import org.scalatest.Inspectors._
import owl.automaton.algorithms.{EmptinessCheck, LanguageAnalysis}
import owl.ltl.parser.LtlParser
import owl.run.{DefaultEnvironment, RunUtil}
import owl.translations.SimpleTranslations
import owl.translations.ltl2dra.LTL2DRAFunction
import owl.translations.ltl2ldba.LTL2LDBAFunction
import owl.translations.ltl2ldba.LTL2LDBAFunction.Configuration
class OwlTest extends FlatSpec with LazyLogging {
"OwlTransformer" should "go to owl formulas" in {
val tests = List(
(Next(Or(Var("x"), Var("y"))), "X(x | y)"),
(And(Var("x"), Var("y")), "(x & y)"),
(Globally(Finally(Var("y"))), "GF y"),
(Next(Finally(Eq(Var("y"), Var("z")))), "XF (y <-> z)")
)
for (t <- tests) {
val owlform = OwlTransformer.toOwl(t._1)
val parsedform = LtlParser.parse(t._2)
owlform shouldEqual (parsedform)
}
}
"OWLFormulas" should "identify satisfiability" in {
val tests = List(
(Next(Or(Var("x"), Var("y"))), false)
// (And(Var("x"), Var("y")), true),
// (Globally(Finally(Var("y"))), true),
// (Next(Finally(Eq(Var("y"), Neg(Var("y"))))), false),
// (And(Globally(Var("y")), Finally(Neg(Var("y")))), false)
)
for (t <- tests) {
val owlform = OwlTransformer.toOwl(t._1)
val env = DefaultEnvironment.of(true, false, false)
val trans = SimpleTranslations.buildSafety(owlform, env)
val empty = EmptinessCheck.isEmpty(trans)
empty should be (t._2)
}
}
}
......@@ -30,7 +30,7 @@ class InvariantCausalFilesTest extends FlatSpec {
// assert(!checkSafeCausal(name, inv))
// }
//
it should "fail to prove conference_linear alleq" in {
it should "fail to prove conference_linear alleq" ignore {
val name = "nonomitting/conference_linear"
val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
assert(!checkSafeCausalElim(name, "alleq", inv))
......
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