README.md 2 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2 3 4 5 6 7
# Looping Workflows

Scala Implementation of the workflow language with loops.

Workflows can be written directly in Scala by instantiating case classes.
You can find implicits helping with that in ``de.tum.workflows.Implicits``.

Christian Müller's avatar
Christian Müller committed
8 9 10
## 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
11

Christian Müller's avatar
Christian Müller committed
12
(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
13

Christian Müller's avatar
Christian Müller committed
14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35
## 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.
```

Christian Müller's avatar
Christian Müller committed
36 37
## Testing

Christian Müller's avatar
Christian Müller committed
38 39
``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``
Christian Müller's avatar
Christian Müller committed
40

41 42 43 44
### 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
45
However, there should be a ready-built version at ``aalta/Aalta_v2.0/aalta``.
46 47

Call it by using (for example)
Christian Müller's avatar
Christian Müller committed
48
``time aalta/Aalta_v2.0/aalta < results/easychair3_stubborn_size4.ltl``
49 50 51

### 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
52 53
or at https://spot.lrde.epita.fr/trans.html.

54 55