# Looping Workflows Scala Implementation of the workflow language with loops published in CSF '17. ## Parser There is a working parser that can read the ``*.spec`` files in ``/examples``. Workflows can also be specified directly in Scala by instantiating case classes. You can find implicits helping with that in ``de.tum.workflows.Implicits``. ## 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`` (You can generate an eclipse project file for use with Scala IDE by running ``sbt eclipse`` after installing the sbt eclipse plugin) ## Example File Format A readable example can be found at ``/examples/conference.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:X,y:Y may (because of easier parsing) Declassify # optional block # Declassification conditions for all Oracles. # Specify with types. # Use the first agent of the target as noninterference agent. # These are state-based, so will be evaluated on every state to find violations. # Currently, no temporal operators here are supported. 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. ``` ## Testing 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/``. ### 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. However, there should be a ready-built version at ``aalta/Aalta_v2.0/aalta``. Call it by using (for example) ``time aalta/Aalta_v2.0/aalta < results/easychair3_stubborn_size4.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.