README.md 1.44 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1
2
3
4
5
6
7
8
9
10
11
# 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``.

For now, it is possible to generate the LTL formula for a workflow using
``Encoding.toFOLTL(w)``
and translate it to pure LTL that can be parsed by Spot.

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

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

## Testing

Christian Müller's avatar
Christian Müller committed
20
An example can be found at ``de.tum.workflows.Main``
Christian Müller's avatar
Christian Müller committed
21
It can be run using ``sbt run`` and logs the resulting LTL formulas for the example workflows to results/.
Christian Müller's avatar
Christian Müller committed
22

Christian Müller's avatar
Christian Müller committed
23
24
25
26
27
28
29
30
31
32
### 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.

Call it by using (for example)
``time aalta/Aalta_v2.0/aalta < results/prevexampleNoOracle_stubborn_3agents.ltl``

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

Christian Müller's avatar
Christian Müller committed
35
36