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

Scala Implementation of the workflow language with loops.
Christian Müller's avatar
Christian Müller committed
4
There is a working parser that can read the ``*.spec`` files in ``/examples``.
Christian Müller's avatar
Christian Müller committed
5

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

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

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

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

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
37 38
## Testing

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

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

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

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

55 56