README.md 2.5 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2
# Looping Workflows

Christian Müller's avatar
Christian Müller committed
3 4 5
Scala Implementation of the workflow language with loops published in CSF '17.

## Parser 
Christian Müller's avatar
Christian Müller committed
6
There is a working parser that can read the ``*.spec`` files in ``/examples``.
Christian Müller's avatar
Christian Müller committed
7

Christian Müller's avatar
Christian Müller committed
8
Workflows can also be specified directly in Scala by instantiating case classes.
Christian Müller's avatar
Christian Müller committed
9 10
You can find implicits helping with that in ``de.tum.workflows.Implicits``.

Christian Müller's avatar
Christian Müller committed
11 12 13
## 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``
Christian Müller's avatar
Christian Müller committed
14

Christian Müller's avatar
Christian Müller committed
15
(You can generate an eclipse project file for use with Scala IDE by running ``sbt eclipse`` after installing the sbt eclipse plugin)
Christian Müller's avatar
Christian Müller committed
16

Christian Müller's avatar
Christian Müller committed
17 18
## Example File Format

Christian Müller's avatar
Christian Müller committed
19
A readable example can be found at ``/examples/conference.spec``.
Christian Müller's avatar
Christian Müller committed
20 21 22 23 24 25 26
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
Christian Müller's avatar
Christian Müller committed
27
# Please use forallmay x:X,y:Y instead of forall x:X,y:Y may (because of easier parsing)
Christian Müller's avatar
Christian Müller committed
28

Christian Müller's avatar
Christian Müller committed
29 30 31 32 33 34 35 36 37
Declassify

# optional block
# Declassification conditions for all Oracles.
# Specify with types.
# Use the first agent of the target as noninterference agent.
# These are state-based, so will be evaluated on every state to find violations.
# Currently, no temporal operators here are supported.

Christian Müller's avatar
Christian Müller committed
38 39 40 41 42 43 44 45 46 47
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.
```

Christian Müller's avatar
Christian Müller committed
48 49
## Testing

Christian Müller's avatar
Christian Müller committed
50 51
To run the unit tests, you can run ``sbt test``. You can find all the unit tests in ``src/test/scala``.
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/``.
Christian Müller's avatar
Christian Müller committed
52

53 54 55 56
### 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.
Christian Müller's avatar
Christian Müller committed
57
However, there should be a ready-built version at ``aalta/Aalta_v2.0/aalta``.
58 59

Call it by using (for example)
Christian Müller's avatar
Christian Müller committed
60
``time aalta/Aalta_v2.0/aalta < results/easychair3_stubborn_size4.ltl``
61 62 63

### Spot
Generating an accepting run can also be done by locally installing Spot (https://spot.lrde.epita.fr),
Christian Müller's avatar
Christian Müller committed
64 65
or at https://spot.lrde.epita.fr/trans.html.

66 67