Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Menu
9.2.2023: Due to updates GitLab will be unavailable for some minutes between 9:00 and 11:00.
Open sidebar
i7
peregrine
Commits
c1c7e6b2
Commit
c1c7e6b2
authored
Nov 29, 2017
by
Stefan Jaax
Browse files
Change readme
parent
a58acf69
Changes
1
Hide whitespace changes
Inline
Side-by-side
README.md
View file @
c1c7e6b2
...
...
@@ -16,47 +16,39 @@ 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
:
Peregrine takes a single population protocol as
JSON-encoded
input.
The following example shows
the input format
:
```
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 }
{
"title": "Majority Protocol",
"states": ["A", "a", "B", "b"],
"transitions": [
{ "name": "t1",
"pre": ["A", "B"],
"post": ["a", "b"]
},
{ "name": "t2",
"pre": ["B", "a"],
"post": ["B", "b"]
},
{ "name": "t3",
"pre": ["A", "b"],
"post": ["A", "a"]
},
{ "name": "t4",
"pre": ["a", "b"],
"post": ["a", "a"]
}
],
initialStates: ["A", "B"],
trueStates: ["A", "a"],
predicate: "A >= B",
description: "This protocol computes whether there are more B-states than A-states"
}
```
*
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
-------
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment