Commit 6abb5138 authored by Philipp Meyer's avatar Philipp Meyer

Update README with section on benchmarks

parent f1028e57
......@@ -10,7 +10,8 @@ In order to compile and install Peregrine, go to the project's main directory an
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/).
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
------
......@@ -29,30 +30,30 @@ population protocol "Majority Protocol" {
}
initial { a b }
true { a a_small }
false { b b_small }
false { b b_small }
}
```
* After the keyword *population protocol* the name of the protocol is given in
quotes.
* 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.
* 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*.
* The set of states is given after the identifier *states*.
* In order to make transitions identifiable,
* 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.
for each transition name.
* The set following the keyword *initial* specifies states that can
belong to an initial population.
* 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
* The sets following the keywords *true* and *false* identify the states
that map to true and false, respectively.
......@@ -60,7 +61,7 @@ that map to true and false, respectively.
Usage
-------
Peregrine is run from the command line.
Peregrine is run from the command line.
If you save the protocol from above in the file *majority.pp* and enter:
```bash
......@@ -85,13 +86,13 @@ strong consensus satisfied
All properties satisfied
```
As seen in the output, Peregrine by default checks two properties:
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
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
......@@ -100,13 +101,37 @@ 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
Peregrine offers fine-grained control over the solution methods and the
verbosity of the output.
To see all options, enter:
```bash
peregrine --help
```
Benchmarks
-------
In the `benchmarks` directory, scripts and tools to generate protocols
and evaluate Peregrine on these benchmarks can be found.
To run the benchmarks, Peregrine needs to be installed.
To compile the table to display the results, additionally
[Python 3](https://www.python.org/) with the [pandas](http://pandas.pydata.org/) library and
[LaTeX](https://www.latex-project.org/) are required.
In order to reproduce the results from the paper
"Towards Efficient Verification of Population Protocols",
go to the folder `benchmarks` and run
```bash
make podc
```
The results are then compiled to the file `results-podc.pdf`.
In order to run all benchmarks, go to the folder `benchmarks` and run
```bash
make
```
The results are then compiled to the file `results-complete.pdf`.
Authors
-------
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment