README.md

# Looping Workflows

Scala Implementation of the workflow language with loops published in CSF '17, CCS 18.

## How to use

To generate LTL formulas from non-omitting workflows, have a look at ``MainLTL``.
To do First Order invariant inference, have a look at ``MainInvariantsInference``. 

## 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.