Commit 4efe503d authored by Christian Müller's avatar Christian Müller

add license, update readme, fix tests, find bugs in converter

parent 64ee83d6
......@@ -28,14 +28,19 @@ build
.idea/
# Resulting ltl formulas
results/*.ltl
results/*.ppltl
results/*.foltl
results/*.png
results/*.metrics
results/**/*.ltl
results/**/*.ppltl
results/**/*.metrics
results/**/*.foltl
# Resulting invariants
results/**/*.invariants
results/**/*.dot
results/**/*.png
# aalta
cnf.dimacs
# Z3
lib/com.microsoft.z3.jar
Copyright 2019 Christian Müller.
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"),
to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense,
and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
# Looping Workflows
# Overview
Scala Implementation of the workflow language with loops published in CSF '17, CCS 18.
This repository contains an implementation of
- First Order transition systems published in (to be published).
- the Multi-Agent Workflow Language published in CSF '17, CCS 18.
# First Order Transition Systems
## How to use (from code)
To do First Order invariant inference, have a look at ``MainInvariantsInference``.
# Workflows
## How to use (from code)
......@@ -17,7 +28,41 @@ There is a working parser that can read the ``*.spec`` files in ``/examples``.
Workflows can also be specified directly in Scala by instantiating case classes.
You can find implicits helping with that in ``de.tum.workflows.Implicits``.
## Example File Format
## Example Transition System File Format
A readable example can be found at ``/examples/tstests/parseTest.spec``.
The example file format consists of the following blocks:
```
Signature
# comma-separated lists of predicates, variables with their types
EmptyPredicates: R(a:Ti,b:Tj), S(a:Ti, b:Tj) # Predicates empty at the initial state
AxiomPredicates: I(b:T) # Constant, axiomatized Input Predicates
As: A(b:Tj) # Predicates under the control of player A
Bs: B(b:Ti) # Predicates under the control of player B
Constants: ca:Ti, cb:Tj # Constants
Transition System
# Nondeterministic loop
loop {
# Simultaneous update of several relations
sim {
R(a,b) := A(b)
S(c,d) := (R(ca,d) ∧ c = ca)
}
S(a,b) := False
}
Invariant
∀a:Ti,b:Tj. (R(a, b) ∧ (ca = a))
Axioms
# comma-separated list of axioms over the AxiomPredicates
True
```
## Example Workflow File Format
A readable example can be found at ``/examples/conference.spec``.
The example file format consists of the following blocks:
......@@ -55,7 +100,7 @@ To run the unit tests, you can run ``sbt test``. You can find all the unit tests
To test your own examples, run ``de.tum.workflows.Main`` by using ``sbt run``. This will parse all ``.spec`` files in ``/examples/`` and will log the resulting LTL formulas to ``results/``.
### Aalta
The resulting LTL formulas can be tested for satisfiability.
LTL formulas resulting from the LTL encoding of the workflow languaged can be tested for satisfiability.
We recommend to use Aalta for this. It has been bundled with this software and resides in ``aalta``.
It can be built by issuing ``make`` in ``aalta/Aalta_v2.0/``. To do this, ``bison`` and ``flex`` must be installed.
However, there should be a ready-built version at ``aalta/Aalta_v2.0/aalta``.
......@@ -67,5 +112,8 @@ Call it by using (for example)
Generating an accepting run can also be done by locally installing Spot (https://spot.lrde.epita.fr),
or at https://spot.lrde.epita.fr/trans.html.
### License
All code in this repository is licensed under the MIT License for Open Source Software.
......@@ -2,13 +2,13 @@ name := "loopingWorkflows"
version := "0.1"
scalaVersion := "2.12.6"
scalaVersion := "2.12.8"
// EclipseKeys.withBundledScalaContainers := false
libraryDependencies ++= Seq(
"com.typesafe.scala-logging" %% "scala-logging" % "3.5.0",
"ch.qos.logback" % "logback-classic" % "1.1.7",
"com.typesafe.scala-logging" %% "scala-logging" % "3.9.2",
"ch.qos.logback" % "logback-classic" % "1.2.3",
"org.scalactic" %% "scalactic" % "3.0.4" % "test",
"org.scalatest" %% "scalatest" % "3.0.4" % "test",
"org.scala-graph" %% "graph-core" % "1.12.5",
......
Workflow
forallmay i,j O(i,j) -> A += (i,j)
forall i,j A(i,j) -> B += (i,j)
forall i,j B(i,j) -> C += (i,j)
forall i,j O(i,j) -> A += (i,j)
forall i,j A(i,j) -> RB += (i,j)
forall i,j RB(i,j) -> C += (i,j)
forall i,j C(i,j) -> D += (i,j)
forall i,j D(i,j) -> E += (i,j)
forall i,j E(i,j) -> F += (i,j)
forall i,j F(i,j) -> G += (i,j)
forall i,j G(i,j) -> H += (i,j)
forall i,j H(i,j) -> I += (i,j)
forall i,j I(i,j) -> J += (i,j)
forall i,j H(i,j) -> HI += (i,j)
forall i,j HI(i,j) -> J += (i,j)
Target
......
Workflow
forallmay i,j True -> A += (i,j)
forall i,j A(i,j) -> B += (i,j)
forall i,j B(i,j) -> C += (i,j)
forall i,j A(i,j) -> RB += (i,j)
forall i,j RB(i,j) -> C += (i,j)
forall i,j C(i,j) -> D += (i,j)
forall i,j D(i,j) -> E += (i,j)
forall i,j E(i,j) -> F += (i,j)
forall i,j F(i,j) -> G += (i,j)
forall i,j G(i,j) -> H += (i,j)
forall i,j H(i,j) -> I += (i,j)
forall i,j I(i,j) -> J += (i,j)
forall i,j H(i,j) -> HI += (i,j)
forall i,j HI(i,j) -> J += (i,j)
Target
......
Workflow
forallmay i,j O(i,j) -> A += (i,j)
forall i,j A(i,j) -> B += (i,j)
forall i,j B(i,j) -> C += (i,j)
forall i,j O(i,j) -> A += (i,j)
forall i,j A(i,j) -> RB += (i,j)
forall i,j RB(i,j) -> C += (i,j)
forall i,j C(i,j) -> D += (i,j)
forall i,j D(i,j) -> E += (i,j)
forall i,j E(i,j) -> F += (i,j)
forall i,j F(i,j) -> G += (i,j)
forall i,j G(i,j) -> H += (i,j)
forall i,j H(i,j) -> I += (i,j)
forall i,j I(i,j) -> J += (i,j)
forall i,j H(i,j) -> HI += (i,j)
forall i,j HI(i,j) -> J += (i,j)
forall i,j J(i,j) -> K += (i,j)
forall i,j K(i,j) -> L += (i,j)
forall i,j L(i,j) -> M += (i,j)
......
Workflow
forallmay i,j True -> A += (i,j)
forall i,j A(i,j) -> B += (i,j)
forall i,j B(i,j) -> C += (i,j)
forall i,j A(i,j) -> RB += (i,j)
forall i,j RB(i,j) -> C += (i,j)
forall i,j C(i,j) -> D += (i,j)
forall i,j D(i,j) -> E += (i,j)
forall i,j E(i,j) -> F += (i,j)
forall i,j F(i,j) -> G += (i,j)
forall i,j G(i,j) -> H += (i,j)
forall i,j H(i,j) -> I += (i,j)
forall i,j I(i,j) -> J += (i,j)
forall i,j H(i,j) -> HI += (i,j)
forall i,j HI(i,j) -> J += (i,j)
forall i,j J(i,j) -> K += (i,j)
forall i,j K(i,j) -> L += (i,j)
forall i,j L(i,j) -> M += (i,j)
......
Workflow
forallmay i,j O(i,j) -> A += (i,j)
forall i,j A(i,j) -> B += (i,j)
forall i,j B(i,j) -> C += (i,j)
forall i,j O(i,j) -> A += (i,j)
forall i,j A(i,j) -> RB += (i,j)
forall i,j RB(i,j) -> C += (i,j)
forall i,j C(i,j) -> D += (i,j)
forall i,j D(i,j) -> E += (i,j)
forall i,j E(i,j) -> F += (i,j)
forall i,j F(i,j) -> G += (i,j)
forall i,j G(i,j) -> H += (i,j)
forall i,j H(i,j) -> I += (i,j)
forall i,j I(i,j) -> J += (i,j)
forall i,j H(i,j) -> HI += (i,j)
forall i,j HI(i,j) -> J += (i,j)
forall i,j J(i,j) -> K += (i,j)
forall i,j K(i,j) -> L += (i,j)
forall i,j L(i,j) -> M += (i,j)
......
Workflow
forallmay i,j True -> A += (i,j)
forall i,j A(i,j) -> B += (i,j)
forall i,j B(i,j) -> C += (i,j)
forall i,j A(i,j) -> RB += (i,j)
forall i,j RB(i,j) -> C += (i,j)
forall i,j C(i,j) -> D += (i,j)
forall i,j D(i,j) -> E += (i,j)
forall i,j E(i,j) -> F += (i,j)
forall i,j F(i,j) -> G += (i,j)
forall i,j G(i,j) -> H += (i,j)
forall i,j H(i,j) -> I += (i,j)
forall i,j I(i,j) -> J += (i,j)
forall i,j H(i,j) -> HI += (i,j)
forall i,j HI(i,j) -> J += (i,j)
forall i,j J(i,j) -> K += (i,j)
forall i,j K(i,j) -> L += (i,j)
forall i,j L(i,j) -> M += (i,j)
......
......@@ -2,7 +2,7 @@ Workflow
forallmay x:X,p:P
True -> Conf += (x,p)
forallmay x:x,p: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)
......
sbt.version=1.1.6
sbt.version=1.2.8
......@@ -23,7 +23,8 @@ object TSConverter extends LazyLogging {
// Map Add/Remove statements to SetStmt
val steps = elaborated.map(s => toTSBlock(s)(w.sig, properties))
// Add causals to constants, add informedness for causal agents
// Add choice predicates to As
// FIXME: Add causals to constants, add informedness for causal agents
val newsig = if (!properties.stubborn) {
w.sig.copy(
preds = w.sig.preds + Fun(INFNAME, List(spec.target.params.head)),
......
......@@ -502,7 +502,7 @@ object FormulaFunctions extends LazyLogging {
// Functions, Variables
case f => (f, bound)
}
logger.warn("Using fallback fixbindings method for general formulas.")
logger.trace("Using fallback fixbindings method for general formulas.")
fix(t, bound ++ t.freeVars)
}
......
......@@ -71,7 +71,9 @@ object Preconditions extends LazyLogging {
// removed
}
def abstractedPrecondition(f: Formula, b: SimpleTSBlock, spec: InvariantSpec, properties: InvProperties, untouched: Set[String], diverged:Boolean): Formula = {
def abstractedPrecondition(f: Formula, b: SimpleTSBlock, spec: InvariantSpec,
properties: InvProperties, untouched: Set[String], diverged:Boolean): Formula = {
val precond = weakestPrecondition(f, b, spec, properties)
// Assume untouched predicates empty
......@@ -79,6 +81,7 @@ object Preconditions extends LazyLogging {
val z3simpednewinv = Z3BSFO.simplifyBS(untouchedprecond)
// If not diverged yet, remove annotations from all predicates since all copies are equal
// TODO: this is hyperproperty-specific
val removedannotations = if (!diverged) {
val rels = spec.ts.sig.preds.map(_.name)
......
......@@ -10,6 +10,9 @@ import de.tum.niwo.foltl.{FOTransformers, FormulaFunctions}
object Z3BSFO extends LazyLogging {
var aechecks = 0
var simplifications = 0
def createContext():(Context, Solver) = {
// Set up Z3
val cfg = new util.HashMap[String, String]()
......@@ -26,7 +29,9 @@ object Z3BSFO extends LazyLogging {
}
def checkAE(f: Formula) = {
def checkAE(f: Formula): (Status, Solver) = {
aechecks += 1
logger.trace(s"Checking a formula with ${f.opsize} operators.")
val (time, res) = Utils.time {
val (ctx, s) = createContext()
......@@ -49,11 +54,15 @@ object Z3BSFO extends LazyLogging {
(c, s)
}
logger.debug(s"Z3-BSFO call took $time ms")
if (time > 1000) {
logger.debug(s"Z3-BSFO call took $time ms")
}
res
}
def simplifyBS(f: Formula) = {
def simplifyBS(f: Formula): Formula = {
simplifications += 1
logger.trace(s"Simplifying a formula with ${f.opsize} operators.")
val (ctx, _) = createContext()
......@@ -73,7 +82,7 @@ object Z3BSFO extends LazyLogging {
val ar = tactics.apply(goal)
val sub = ar.getSubgoals()
val sub = ar.getSubgoals
val mapped = if (sub.isEmpty) {
True
} else if (sub.size > 1) {
......@@ -87,7 +96,7 @@ object Z3BSFO extends LazyLogging {
mapped
}
def toCNFUniversal(f:Formula) = {
def toCNFUniversal(f:Formula): Formula = {
if (!f.isUniversal) {
logger.error("Trying to get CNF of non-universal formula via Z3")
}
......@@ -103,7 +112,7 @@ object Z3BSFO extends LazyLogging {
FormulaFunctions.pushUniversalQuantifiers(simped)
}
def toCNFClausesUniversal(f:Formula) = {
def toCNFClausesUniversal(f:Formula): (List[(Boolean, List[Var])], List[List[Formula]]) = {
if (!f.isUniversal) {
logger.error("Trying to get CNF of non-universal formula via Z3")
}
......@@ -117,7 +126,7 @@ object Z3BSFO extends LazyLogging {
(quantifiers, clauses)
}
def toCNFQFreeClauses(f: Formula) = {
def toCNFQFreeClauses(f: Formula): List[List[Formula]] = {
val (ctx, _) = createContext()
......@@ -161,7 +170,7 @@ object Z3BSFO extends LazyLogging {
// Send to z3
val c = s.check()
if (c == Status.UNKNOWN) {
logger.warn(s"Z3-BSFO: Status unknown - ${s.getReasonUnknown()}")
logger.warn(s"Z3-BSFO: Status unknown - ${s.getReasonUnknown}")
"No model found - Status unknown"
} else if (c == Status.SATISFIABLE) {
s.getModel.toString
......
......@@ -65,7 +65,7 @@ class InferenceTests extends FlatSpec {
assert(checkSafeStubborn(name, "", _ => inv))
}
it should "prove safe loopy causal stuff safe" ignore {
it should "prove safe loopy causal stuff safe" in {
val name = "tests/conference_stubborn_withB"
val xat = Var("xat","A")
val xbt = Var("xbt","A")
......
......@@ -5,7 +5,6 @@ import de.tum.niwo.invariants.InvariantGenerator
import de.tum.niwo.tests.TestUtils._
import org.scalatest.{FlatSpec, Ignore}
@Ignore
class DemoNoStrengtheningTests extends FlatSpec {
// fixed arity, nonomitting - easy
......
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