README.md 2.09 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
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
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.



Philipp Meyer's avatar
Philipp Meyer committed
60
61
62
63
64
65
Usage
-------

Authors
-------

Philipp Meyer's avatar
Philipp Meyer committed
66
67
* Philipp Meyer (<meyerphi@in.tum.de>)
* Stefan Jaax (<jaax@in.tum.de>)
Philipp Meyer's avatar
Philipp Meyer committed
68
69
70

Licence
-------
Philipp Meyer's avatar
Philipp Meyer committed
71
Peregrine is licensed under the GPLv3, see [LICENSE.md](LICENSE.md) for details.
Philipp Meyer's avatar
Philipp Meyer committed
72
73
74

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