Commit edd626c5 authored by Christian Müller's avatar Christian Müller

readme

parent 6673eed6
......@@ -11,6 +11,28 @@ To get sbt to build the project properly, you have to add the Supersafe Compiler
(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/easychair.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,y may (because of easier parsing)
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
``de.tum.workflows.Main`` will use any ``.spec`` files in ``/examples/`` and logs the resulting LTL formulas for the example workflows to results/.
......
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