Commit 0e12ac23 authored by Stefan Jaax's avatar Stefan Jaax
Browse files

Merge branch 'master' of gitlab.lrz.de:i7/peregrine

parents d78627b5 5bb2dea2
Loading
Loading
Loading
Loading
+51 −0
Original line number Diff line number Diff line
@@ -5,6 +5,57 @@ Tool for efficient verification of population protocols

Installation
-------
In order to compile and install Peregrine, go to the project's main directory and enter
```bash
    sudo make install
```

Compilation requires the Glasgow Haskell Compiler [ghc >= 7.8.1](https://www.haskell.org/ghc/)  and the build system [cabal >= 1.22](https://www.haskell.org/cabal/).

Input
------

Peregrine takes a single population protocol as input.
The following example shows how a protocol is encoded:

```
population protocol "Majority Protocol" {
    states { a b a_small b_small}
    transitions { t1 t2 t3 t4 }
    arcs { { a, b } -> t1 -> { a_small, b_small }
           { b, a_small } -> t2 -> { b, b_small }
           { a, b_small } -> t3 -> { a, a_small }
           { a_small, b_small } -> t4 -> { a_small, a_small }
         }
    initial { a b }
    true { a a_small }
    false { b b_small } 
}


```
* After the key word *population protocol* the name of the protocol is given in 
quotes. 

* Finite sets are specified in braces 
through space- or comma-separated lists of  names. 
Names consist of alphanumerical characters or underscores. 

* The set of states is given after the identifier *states*. 

* In order to make transitions identifiable, 
each transition must be given a name after the  key word *transitions*.

* Transitions are defined after the key word *arcs*; there must be one definition
  for each transition name. 

* The set following the keyword *initial* specifies states that can 
belong to an initial population. 

* The sets following the keywords *true* and *false* identify the states 
that map to true and false, respectively.



Usage
-------