Commit 9a6fc60c authored by Christian Müller's avatar Christian Müller

improve readme

parent a45f9930
# Looping Workflows
Scala Implementation of the workflow language with loops.
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.
......@@ -14,7 +16,7 @@ To get sbt to build the project properly, you have to add the Supersafe Compiler
## Example File Format
A readable example can be found at ``/examples/easychair.spec``.
A readable example can be found at ``/examples/conference.spec``.
The example file format consists of the following blocks:
```
......@@ -24,6 +26,15 @@ 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.
......
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