Commit 6673eed6 authored by Christian Müller's avatar Christian Müller
Browse files

extend README

parent cd87a6ce
...@@ -9,20 +9,21 @@ You can find implicits helping with that in ``de.tum.workflows.Implicits``. ...@@ -9,20 +9,21 @@ You can find implicits helping with that in ``de.tum.workflows.Implicits``.
To get sbt to build the project properly, you have to add the Supersafe Compiler plugin by adding 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`` ``resolvers += "Artima Maven Repository" at "http://repo.artima.com/releases"`` to ``~/.sbt/0.13/global.sbt``
(You can generate an eclipse project file for use with Scala IDE by running ``sbt eclipse`` after installing the sbt plugin) (You can generate an eclipse project file for use with Scala IDE by running ``sbt eclipse`` after installing the sbt eclipse plugin)
## Testing ## Testing
An example can be found in ``de.tum.workflows.Main`` and many tests in ``src/test/scala`` ``de.tum.workflows.Main`` will use any ``.spec`` files in ``/examples/`` and logs the resulting LTL formulas for the example workflows to results/.
It can be run using ``sbt run`` 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``
### Aalta ### Aalta
The resulting LTL formulas can be tested for satisfiability. 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``. 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. It can be built by issuing ``make`` in ``aalta/Aalta_v2.0/``. To do this, ``bison`` and ``flex`` must be installed.
However, there should be a ready-built version at ``aalta/Aalta_v2.0/aalta``.
Call it by using (for example) Call it by using (for example)
``time aalta/Aalta_v2.0/aalta < results/prevexampleNoOracle_stubborn_3agents.ltl`` ``time aalta/Aalta_v2.0/aalta < results/easychair3_stubborn_size4.ltl``
### Spot ### Spot
Generating an accepting run can also be done by locally installing Spot (https://spot.lrde.epita.fr), Generating an accepting run can also be done by locally installing Spot (https://spot.lrde.epita.fr),
......
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