Peregrine
=======

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 keyword *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  keyword *transitions*.

* Transitions are defined after the keyword *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
-------

Peregrine is run from the command line. 

If you save the protocol from above in the file *majority.pp* and enter:
```bash
    peregrine majority.pp
```

You obtain the following output:
```
Peregrine - Efficient Verification of Population Protocols

Reading "majority.pp"
Analyzing Population protocol "Majority Protocol"

Checking layered termination
Checking layered termination with at most 1 layers
Checking layered termination with at most 2 layers
layered termination satisfied

Checking strong consensus
strong consensus satisfied

All properties satisfied
```

As seen in the output, Peregrine by default checks two properties: 
*Layered Termination* and *Strong Consensus*:

* Layered Termination: protocol is layered in a way that every fair run of the protocol
will eventually reach a terminal population where no more change occurs.
* Strong Consensus: every terminal population reachable from an initial population
  forms a consensus. Moreover, the boolean value of the consensus must be unique 
  for a given initial population.

If both Layered Termination and Strong Consensus are satsified, then the protocol
is *well-specified*, i.e. the protocol robustly computes a predicate defined
by the mapping from input population to its unique consensus value.
Note that the converse direction need not hold: there are well-specified protocols
that violate the conjunction of Strong Consensus and Layered Termination.

Peregrine offers fine-grained control over the solution methods and the 
verbosity of the output.
To see all options, enter:
```bash
    peregrine --help
```

Authors
-------

* Philipp Meyer (<meyerphi@in.tum.de>)
* Stefan Jaax (<jaax@in.tum.de>)

References
--------
* Michael Blondin, Javier Esparza, Stefan Jaax, Philipp J. Meyer: “Towards Efficient Verification of Population Protocols”, 2017; [http://arxiv.org/abs/1703.04367 arXiv:1703.04367].

Licence
-------
Peregrine is licensed under the GPLv3, see [LICENSE.md](LICENSE.md) for details.

Logo by [Juan Lacruz](https://commons.wikimedia.org/wiki/User:Juan_lacruz), [Peregrine Falcon La Cañada](https://commons.wikimedia.org/wiki/File:Peregrine_Falcon_La_Cañada.jpg), [CC BY-SA 3.0](https://creativecommons.org/licenses/by-sa/3.0/legalcode).