In January 2021 we will introduce a 10 GB quota for project repositories. Higher limits for individual projects will be available on request. Please see https://doku.lrz.de/display/PUBLIC/GitLab for more information.

README.md 3.82 KB
Newer Older
Philipp Meyer's avatar
Philipp Meyer committed
1
Peregrine
Philipp Meyer's avatar
Philipp Meyer committed
2 3
=======

Philipp Meyer's avatar
Philipp Meyer committed
4
Tool for efficient verification of population protocols
Philipp Meyer's avatar
Philipp Meyer committed
5 6 7

Installation
-------
8 9 10 11 12 13
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/).
Philipp Meyer's avatar
Philipp Meyer committed
14

15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36
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 } 
}


```
Stefan Jaax's avatar
Stefan Jaax committed
37
* After the keyword *population protocol* the name of the protocol is given in 
38 39 40 41 42 43 44 45 46
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, 
Stefan Jaax's avatar
Stefan Jaax committed
47
each transition must be given a name after the  keyword *transitions*.
48

Stefan Jaax's avatar
Stefan Jaax committed
49
* Transitions are defined after the keyword *arcs*; there must be one definition
50 51
  for each transition name. 

Stefan Jaax's avatar
Stefan Jaax committed
52
* The set following the keyword *initial* specifies states that can 
53 54
belong to an initial population. 

Stefan Jaax's avatar
Stefan Jaax committed
55
* The sets following the keywords *true* and *false* identify the states 
56 57 58 59
that map to true and false, respectively.



Philipp Meyer's avatar
Philipp Meyer committed
60 61 62
Usage
-------

Stefan Jaax's avatar
Stefan Jaax committed
63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90
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*:

Stefan Jaax's avatar
Stefan Jaax committed
91
* Layered Termination: protocol is layered in a way that every fair run of the protocol
Stefan Jaax's avatar
Stefan Jaax committed
92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109
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
```

Philipp Meyer's avatar
Philipp Meyer committed
110 111 112
Authors
-------

Philipp Meyer's avatar
Philipp Meyer committed
113 114
* Philipp Meyer (<meyerphi@in.tum.de>)
* Stefan Jaax (<jaax@in.tum.de>)
Philipp Meyer's avatar
Philipp Meyer committed
115

Stefan Jaax's avatar
Stefan Jaax committed
116 117 118 119
References
--------
* Michael Blondin, Stefan Jaax, Javier Esparza: “Towards Efficient Verification of Population Protocols”, 2017; [http://arxiv.org/abs/1703.04367 arXiv:1703.04367].

Philipp Meyer's avatar
Philipp Meyer committed
120 121
Licence
-------
Philipp Meyer's avatar
Philipp Meyer committed
122
Peregrine is licensed under the GPLv3, see [LICENSE.md](LICENSE.md) for details.
Philipp Meyer's avatar
Philipp Meyer committed
123 124 125

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).