Commit 24497f1d authored by Christian Müller's avatar Christian Müller

Merge branch 'master' of versioncontrolseidl.in.tum.de:mueller/loopingworkflows

parents b254c88c 1d772124
# Looping Workflows
Scala Implementation of the workflow language with loops.
There is a working parser that can read the ``*.spec`` files in ``/examples``.
Workflows can be written directly in Scala by instantiating case classes.
Workflows can also be specified directly in Scala by instantiating case classes.
You can find implicits helping with that in ``de.tum.workflows.Implicits``.
## Building
To get sbt to build the project properly, you have to add the Supersafe Compiler plugin by adding
``resolvers += "Artima Maven Repository" at "http://repo.artima.com/releases"`` to ``~/.sbt/0.13/global.sbt``
(You can generate an eclipse project file for use with Scala IDE by running ``sbt eclipse`` after installing the sbt plugin)
(You can generate an eclipse project file for use with Scala IDE by running ``sbt eclipse`` after installing the sbt eclipse plugin)
## Example File Format
A readable example can be found at ``/examples/easychair.spec``.
The example file format consists of the following blocks:
```
Workflow
# a workflow
# If types are omitted, everything is of type T, types can be given while binding the variables with the forall x:X
# Please use forallmay x:X,y:Y instead of forall x,y may (because of easier parsing)
Target
# the relation where the noninterference counterexample should be found. Make sure the types match.
Causality
# optional block
# Gives a list of typed causal agents that will be instantiated and added to the universe.
```
## Testing
An example can be found in ``de.tum.workflows.Main`` and many tests in ``src/test/scala``
It can be run using ``sbt run`` and logs the resulting LTL formulas for the example workflows to results/.
``de.tum.workflows.Main`` will use any ``.spec`` files in ``/examples/`` and logs the resulting LTL formulas for the example workflows to results/.
To get a feel for the code, see the tests in ``src/test/scala``
### Aalta
The resulting LTL formulas 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``.
Call it by using (for example)
``time aalta/Aalta_v2.0/aalta < results/prevexampleNoOracle_stubborn_3agents.ltl``
``time aalta/Aalta_v2.0/aalta < results/easychair3_stubborn_size4.ltl``
### Spot
Generating an accepting run can also be done by locally installing Spot (https://spot.lrde.epita.fr),
......
p cnf 107 116
31 0
p cnf 83 92
23 0
-23 24 0
-23 31 0
-24 25 0
-24 26 0
-25 -1 2 0
-26 27 0
-26 28 0
-27 -3 4 0
-28 29 0
-28 30 0
-29 1 -2 0
-30 3 -4 0
-31 32 0
-31 39 0
-32 33 0
-32 34 0
-33 -1 2 0
-33 -5 6 0
-34 35 0
-34 36 0
-35 -3 4 0
-35 -7 8 0
-36 37 0
-36 38 0
-37 1 -2 0
-38 3 -4 0
-37 5 -6 0
-38 7 -8 0
-39 40 0
-39 47 0
-40 41 0
-40 42 0
-41 -5 6 0
-41 -9 10 0
-42 43 0
-42 44 0
-43 -7 8 0
-43 -11 12 0
-44 45 0
-44 46 0
-45 5 -6 0
-46 7 -8 0
-45 9 -10 0
-46 11 -12 0
-47 48 0
-47 63 0
-47 55 0
-48 49 0
-48 50 0
-49 -9 10 0
-49 -13 14 0
-50 51 0
-50 52 0
-51 -11 12 0
-51 -15 16 0
-52 53 0
-52 54 0
-53 -13 14 0
-54 55 0
-54 56 0
-55 -15 16 0
-56 57 0
-56 58 0
-57 9 -10 0
-58 59 0
-58 60 0
-59 13 -14 0
-60 61 0
-60 62 0
-61 11 -12 0
-62 15 -16 0
-53 13 -14 0
-54 15 -16 0
-55 56 0
-55 57 0
-56 -17 -18 0
-57 58 0
-57 59 0
-58 -17 -19 0
-59 60 0
-59 61 0
-60 -20 -17 0
-61 62 0
-61 63 0
-62 -20 -21 0
-63 64 0
-63 79 0
-64 65 0
-64 66 0
-65 -17 18 0
-66 67 0
-66 68 0
-67 -19 20 0
-68 69 0
-68 70 0
-69 -21 22 0
-70 71 0
-70 72 0
-71 -23 24 0
-72 73 0
-72 74 0
-73 17 -18 0
-74 75 0
-74 76 0
-75 21 -22 0
-76 77 0
-76 78 0
-77 19 -20 0
-78 23 -24 0
-63 65 0
-64 -20 -18 0
-65 66 0
-65 67 0
-66 -20 -19 0
-67 68 0
-67 69 0
-68 -17 -21 0
-69 70 0
-69 71 0
-70 -18 -19 0
-71 72 0
-71 73 0
-72 -22 -21 0
-73 74 0
-73 75 0
-74 -22 -19 0
-75 76 0
-75 77 0
-76 -21 -19 0
-77 78 0
-77 79 0
-78 -22 -18 0
-79 80 0
-79 81 0
-80 -25 -26 0
-80 -21 -18 0
-81 82 0
-81 83 0
-82 -25 -27 0
-83 84 0
-83 85 0
-84 -28 -25 0
-85 86 0
-85 87 0
-86 -28 -29 0
-87 88 0
-87 89 0
-88 -28 -26 0
-89 90 0
-89 91 0
-90 -28 -27 0
-91 92 0
-91 93 0
-92 -25 -29 0
-93 94 0
-93 95 0
-94 -26 -27 0
-95 96 0
-95 97 0
-96 -30 -29 0
-97 98 0
-97 99 0
-98 -30 -27 0
-99 100 0
-99 101 0
-100 -29 -27 0
-101 102 0
-101 103 0
-102 -30 -26 0
-103 104 0
-103 105 0
-104 -29 -26 0
-105 106 0
-105 107 0
-106 -30 -25 0
-107 -30 -28 0
-82 -22 -17 0
-83 -22 -20 0
......@@ -3,12 +3,12 @@ Workflow
forallmay x:A,p:P
True → Conf += (x,p)
forallmay x:A,p:P
!Conf(x,p) → Ass += (x,p)
!Conf(x,p) → Assign += (x,p)
forallmay x:A,p:P,r:R
(Ass(x,p) ∧ O(x,p,r)) → Review += (x,p,r)
(Assign(x,p) ∧ O(x,p,r)) → Review += (x,p,r)
loop {
forall xa:A,xb:A,p:P,r:R (A(xa,p) ∧ Review(xb,p,r)) → Read += (xa,xb,p,r)
forallmay x:A,p:P,r:R (A(x,p) ∧ O(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,xb,p,r)
forallmay x:A,p:P,r:R (Assign(x,p) ∧ O(x,p,r)) → Review += (x,p,r)
}
Declassify
......
......@@ -7,8 +7,8 @@ forallmay x:A,p:P
forallmay x:A,p:P
(Ass(x,p) ∧ O(x,p)) -> Acc += (x,p)
loop {
forall xa:A,xb:A,p:P (A(xa,p) ∧ Acc(xb,p)) -> Read += (xa,xb,p)
forallmay x:A,p:P (A(x,p) ∧ O(x,p)) -> Acc += (x,p)
forall xa:A,xb:A,p:P (Ass(xa,p) ∧ Acc(xb,p)) -> Read += (xa,xb,p)
forallmay x:A,p:P (Ass(x,p) ∧ O(x,p)) -> Acc += (x,p)
}
Declassify
......@@ -18,3 +18,7 @@ O(x:A,p:P,r:R): G ¬ Conf(x:A,p:P)
Target
Read(xa:A,xb:A,p:P)
Causality
a:A
......@@ -3,11 +3,11 @@ Workflow
forallmay x:X,p:P
True -> Conf += (x,p)
forallmay x:X,p:P
!Conf(x,p) -> Ass += (x,p)
!Conf(x,p) -> Assign += (x,p)
forall x:X,p:P,r:R
(Ass(x,p) ∧ O(x,p,r)) -> Read += (x,p,r)
(Assign(x,p) ∧ O(x,p,r)) -> Read += (x,p,r)
forallmay y:X,x:X,p:P
(Ass(x,p) ∧ Ass(y,p)) -> Comm += (x,y,p)
(Assign(x,p) ∧ Assign(y,p)) -> Comm += (x,y,p)
Declassify
......
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