README.md 2.52 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2
# Looping Workflows

Christian Müller's avatar
Christian Müller committed
3 4
Scala Implementation of the workflow language with loops published in CSF '17, CCS 18.

Christian Müller's avatar
Christian Müller committed
5
## How to use (from code)
Christian Müller's avatar
Christian Müller committed
6 7 8

To generate LTL formulas from non-omitting workflows, have a look at ``MainLTL``.
To do First Order invariant inference, have a look at ``MainInvariantsInference``. 
Christian Müller's avatar
Christian Müller committed
9

Christian Müller's avatar
Christian Müller committed
10 11 12 13
## How to use (from CLI)

Have a look at ``LTLCLI`` and ``InvariantCLI``.

Christian Müller's avatar
Christian Müller committed
14
## Parser 
Christian Müller's avatar
Christian Müller committed
15
There is a working parser that can read the ``*.spec`` files in ``/examples``.
Christian Müller's avatar
Christian Müller committed
16

Christian Müller's avatar
Christian Müller committed
17
Workflows can also be specified directly in Scala by instantiating case classes.
Christian Müller's avatar
Christian Müller committed
18 19
You can find implicits helping with that in ``de.tum.workflows.Implicits``.

Christian Müller's avatar
Christian Müller committed
20 21
## Example File Format

Christian Müller's avatar
Christian Müller committed
22
A readable example can be found at ``/examples/conference.spec``.
Christian Müller's avatar
Christian Müller committed
23 24 25 26 27 28 29
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
Christian Müller's avatar
Christian Müller committed
30
# Please use forallmay x:X,y:Y instead of forall x:X,y:Y may (because of easier parsing)
Christian Müller's avatar
Christian Müller committed
31

Christian Müller's avatar
Christian Müller committed
32 33 34 35 36 37 38 39 40
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.

Christian Müller's avatar
Christian Müller committed
41 42 43 44 45 46 47 48 49 50
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.
```

Christian Müller's avatar
Christian Müller committed
51
## Building & Testing
Christian Müller's avatar
Christian Müller committed
52

Christian Müller's avatar
Christian Müller committed
53
The project is built with ``sbt``. To run one of the executable main classes, use ``sbt run``.
Christian Müller's avatar
Christian Müller committed
54 55
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/``.
Christian Müller's avatar
Christian Müller committed
56

57 58 59 60
### 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.
Christian Müller's avatar
Christian Müller committed
61
However, there should be a ready-built version at ``aalta/Aalta_v2.0/aalta``.
62 63

Call it by using (for example)
Christian Müller's avatar
Christian Müller committed
64
``time aalta/Aalta_v2.0/aalta < results/easychair3_stubborn_size4.ltl``
65 66 67

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

70 71