Commit be30866a authored by Stefan Jaax's avatar Stefan Jaax
Browse files

Add description of input to README.md

parent 008172ed
Loading
Loading
Loading
Loading
+45 −0
Original line number Diff line number Diff line
@@ -12,6 +12,51 @@ In order to compile and install Peregrine, go to the project's main directory an

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 followed by the keyword *initial* specifies states that can 
belong to an initial population. 

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



Usage
-------