README.md 3.96 KB
Newer Older
1
# Overview
Christian Müller's avatar
Christian Müller committed
2

3 4 5 6 7 8 9 10 11 12 13 14
This repository contains an implementation of 
- First Order transition systems published in (to be published).
- the Multi-Agent Workflow Language published in CSF '17, CCS 18.


# First Order Transition Systems

## How to use (from code)

To do First Order invariant inference, have a look at ``MainInvariantsInference``. 

# Workflows
Christian Müller's avatar
Christian Müller committed
15

Christian Müller's avatar
Christian Müller committed
16
## How to use (from code)
Christian Müller's avatar
Christian Müller committed
17 18 19

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
20

Christian Müller's avatar
Christian Müller committed
21 22 23 24
## How to use (from CLI)

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

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

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

31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65
## Example Transition System File Format

A readable example can be found at ``/examples/tstests/parseTest.spec``.
The example file format consists of the following blocks:

```
Signature
    # comma-separated lists of predicates, variables with their types
    EmptyPredicates:    R(a:Ti,b:Tj), S(a:Ti, b:Tj)  # Predicates empty at the initial state
    AxiomPredicates:    I(b:T)                       # Constant, axiomatized Input Predicates
    As:                 A(b:Tj)                      # Predicates under the control of player A
    Bs:                 B(b:Ti)                      # Predicates under the control of player B
    Constants:          ca:Ti, cb:Tj                 # Constants

Transition System
    # Nondeterministic loop
    loop {
        # Simultaneous update of several relations
        sim {
            R(a,b) := A(b)
            S(c,d) := (R(ca,d) ∧ c = ca)
        }
        S(a,b) := False
    }

Invariant
    ∀a:Ti,b:Tj. (R(a, b) ∧ (ca = a))

Axioms
    # comma-separated list of axioms over the AxiomPredicates
    True
    
```

## Example Workflow File Format
Christian Müller's avatar
Christian Müller committed
66

Christian Müller's avatar
Christian Müller committed
67
A readable example can be found at ``/examples/conference.spec``.
Christian Müller's avatar
Christian Müller committed
68 69 70 71 72 73 74
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
75
# 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
76

Christian Müller's avatar
Christian Müller committed
77 78 79 80 81 82 83 84 85
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
86 87 88 89 90 91 92 93 94 95
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
96
## Building & Testing
Christian Müller's avatar
Christian Müller committed
97

Christian Müller's avatar
Christian Müller committed
98
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
99 100
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
101

102
### Aalta
103
LTL formulas resulting from the LTL encoding of the workflow languaged can be tested for satisfiability.
104 105
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
106
However, there should be a ready-built version at ``aalta/Aalta_v2.0/aalta``.
107 108

Call it by using (for example)
Christian Müller's avatar
Christian Müller committed
109
``time aalta/Aalta_v2.0/aalta < results/easychair3_stubborn_size4.ltl``
110 111 112

### 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
113 114
or at https://spot.lrde.epita.fr/trans.html.

115 116 117
### License

All code in this repository is licensed under the MIT License for Open Source Software.
118 119