Commit 99973a5a authored by Stefan Jaax's avatar Stefan Jaax
Browse files

Add use info to

parent 0e12ac23
......@@ -60,6 +60,53 @@ that map to true and false, respectively.
Peregrine is run from the command line.
If you save the protocol from above in the file *majority.pp* and enter:
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: 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:
peregrine --help
Supports Markdown
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