Commit 8a956206 authored by Christian Müller's avatar Christian Müller

move aalta, update readme

parent d362f152
......@@ -18,8 +18,19 @@ To get sbt to build the project properly, you have to add the Supersafe Compiler
## Testing
An example can be found at ``de.tum.workflows.Main``
It can be run using ``sbt run`` and logs the resulting LTL formulas for the example workflow to the console.
It can be run using ``sbt run`` and logs the resulting LTL formulas for the example workflows to results/.
Generating an accepting run can be done by locally installing Spot (https://spot.lrde.epita.fr),
### 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),
or at https://spot.lrde.epita.fr/trans.html.
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