Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
peregrine
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Locked Files
Requirements
Requirements
List
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Security & Compliance
Security & Compliance
Dependency List
License Compliance
Operations
Operations
Environments
Analytics
Analytics
CI / CD
Insights
Issue
Repository
Value Stream
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Jobs
Commits
Open sidebar
i7
peregrine
Commits
430f9c2e
Commit
430f9c2e
authored
May 02, 2017
by
Philipp Meyer
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Rename yes and no states to true and false states
parent
4cdc7a42
Changes
7
Hide whitespace changes
Inline
Side-by-side
Showing
7 changed files
with
348 additions
and
51 deletions
+348
-51
examples/broadcast.pp
examples/broadcast.pp
+5
-5
examples/majority.pp
examples/majority.pp
+2
-2
examples/threshold_l3_c1.pnet
examples/threshold_l3_c1.pnet
+297
-0
src/Main.hs
src/Main.hs
+2
-2
src/Parser/PP.hs
src/Parser/PP.hs
+17
-17
src/PopulationProtocol.hs
src/PopulationProtocol.hs
+24
-24
src/Solver/StrongConsensus.hs
src/Solver/StrongConsensus.hs
+1
-1
No files found.
examples/broadcast.pp
View file @
430f9c2e
population
protocol
"Broadcast Protocol"
{
states
{
true
false
}
states
{
_true
_false
}
transitions
{
x_false_true
}
arcs
{
{
false
,
true
}
->
x_false_true
->
{
true
,
true
}
{
_false
,
_true
}
->
x_false_true
->
{
_true
,
_
true
}
}
initial
{
true
false
}
yes
{
true
}
no
{
false
}
initial
{
_true
_
false
}
true
{
_
true
}
false
{
_
false
}
}
examples/majority.pp
View file @
430f9c2e
...
...
@@ -8,6 +8,6 @@ population protocol "Majority Protocol" {
{
neutral
,
mildlybad
}
->
x_neutral_mildlybad
->
{
mildlybad
,
mildlybad
}
}
initial
{
good
bad
}
yes
{
good
neutral
}
no
{
bad
mildlybad
}
true
{
good
neutral
}
false
{
bad
mildlybad
}
}
examples/threshold_l3_c1.pnet
0 → 100644
View file @
430f9c2e
population protocol "Old Threshold Protocol with l = 3 and c = 1" {
states { _l_true_m3 _l_true_m2 _l_true_m1 _l_true_0 _l_true_p1 _l_true_p2 _l_true_p3 _l_false_m3 _l_false_m2 _l_false_m1 _l_false_0 _l_false_p1 _l_false_p2 _l_false_p3 _nl_true_m3 _nl_true_m2 _nl_true_m1 _nl_true_0 _nl_true_p1 _nl_true_p2 _nl_true_p3 _nl_false_m3 _nl_false_m2 _nl_false_m1 _nl_false_0 _nl_false_p1 _nl_false_p2 _nl_false_p3}
transitions { x__l_true_m3__l_true_m3 x__l_true_m3__l_true_m2 x__l_true_m3__l_true_m1 x__l_true_m3__l_true_0 x__l_true_m3__l_true_p1 x__l_true_m3__l_true_p2 x__l_true_m3__l_true_p3 x__l_true_m2__l_true_m2 x__l_true_m2__l_true_m1 x__l_true_m2__l_true_0 x__l_true_m2__l_true_p1 x__l_true_m2__l_true_p2 x__l_true_m2__l_true_p3 x__l_true_m1__l_true_m1 x__l_true_m1__l_true_0 x__l_true_m1__l_true_p1 x__l_true_m1__l_true_p2 x__l_true_m1__l_true_p3 x__l_true_0__l_true_0 x__l_true_0__l_true_p1 x__l_true_0__l_true_p2 x__l_true_0__l_true_p3 x__l_true_p1__l_true_p1 x__l_true_p1__l_true_p2 x__l_true_p1__l_true_p3 x__l_true_p2__l_true_p2 x__l_true_p2__l_true_p3 x__l_true_p3__l_true_p3 x__l_false_m3__l_true_m3 x__l_false_m3__l_true_m2 x__l_false_m3__l_true_m1 x__l_false_m3__l_true_0 x__l_false_m3__l_true_p1 x__l_false_m3__l_true_p2 x__l_false_m3__l_true_p3 x__l_false_m3__l_false_m3 x__l_false_m3__l_false_m2 x__l_false_m3__l_false_m1 x__l_false_m3__l_false_0 x__l_false_m3__l_false_p1 x__l_false_m3__l_false_p2 x__l_false_m3__l_false_p3 x__l_false_m2__l_true_m3 x__l_false_m2__l_true_m2 x__l_false_m2__l_true_m1 x__l_false_m2__l_true_0 x__l_false_m2__l_true_p1 x__l_false_m2__l_true_p2 x__l_false_m2__l_true_p3 x__l_false_m2__l_false_m2 x__l_false_m2__l_false_m1 x__l_false_m2__l_false_0 x__l_false_m2__l_false_p1 x__l_false_m2__l_false_p2 x__l_false_m2__l_false_p3 x__l_false_m1__l_true_m3 x__l_false_m1__l_true_m2 x__l_false_m1__l_true_m1 x__l_false_m1__l_true_0 x__l_false_m1__l_true_p1 x__l_false_m1__l_true_p2 x__l_false_m1__l_true_p3 x__l_false_m1__l_false_m1 x__l_false_m1__l_false_0 x__l_false_m1__l_false_p1 x__l_false_m1__l_false_p2 x__l_false_m1__l_false_p3 x__l_false_0__l_true_m3 x__l_false_0__l_true_m2 x__l_false_0__l_true_m1 x__l_false_0__l_true_0 x__l_false_0__l_true_p1 x__l_false_0__l_true_p2 x__l_false_0__l_true_p3 x__l_false_0__l_false_0 x__l_false_0__l_false_p1 x__l_false_0__l_false_p2 x__l_false_0__l_false_p3 x__l_false_p1__l_true_m3 x__l_false_p1__l_true_m2 x__l_false_p1__l_true_m1 x__l_false_p1__l_true_0 x__l_false_p1__l_true_p1 x__l_false_p1__l_true_p2 x__l_false_p1__l_true_p3 x__l_false_p1__l_false_p1 x__l_false_p1__l_false_p2 x__l_false_p1__l_false_p3 x__l_false_p2__l_true_m3 x__l_false_p2__l_true_m2 x__l_false_p2__l_true_m1 x__l_false_p2__l_true_0 x__l_false_p2__l_true_p1 x__l_false_p2__l_true_p2 x__l_false_p2__l_true_p3 x__l_false_p2__l_false_p2 x__l_false_p2__l_false_p3 x__l_false_p3__l_true_m3 x__l_false_p3__l_true_m2 x__l_false_p3__l_true_m1 x__l_false_p3__l_true_0 x__l_false_p3__l_true_p1 x__l_false_p3__l_true_p2 x__l_false_p3__l_true_p3 x__l_false_p3__l_false_p3 x__nl_true_m3__l_true_m2 x__nl_true_m3__l_true_m1 x__nl_true_m3__l_true_0 x__nl_true_m3__l_true_p1 x__nl_true_m3__l_true_p2 x__nl_true_m3__l_true_p3 x__nl_true_m3__l_false_m3 x__nl_true_m3__l_false_m2 x__nl_true_m3__l_false_m1 x__nl_true_m3__l_false_0 x__nl_true_m3__l_false_p1 x__nl_true_m3__l_false_p2 x__nl_true_m3__l_false_p3 x__nl_true_m2__l_true_m2 x__nl_true_m2__l_true_m1 x__nl_true_m2__l_true_0 x__nl_true_m2__l_true_p1 x__nl_true_m2__l_true_p2 x__nl_true_m2__l_true_p3 x__nl_true_m2__l_false_m3 x__nl_true_m2__l_false_m2 x__nl_true_m2__l_false_m1 x__nl_true_m2__l_false_0 x__nl_true_m2__l_false_p1 x__nl_true_m2__l_false_p2 x__nl_true_m2__l_false_p3 x__nl_true_m1__l_true_m2 x__nl_true_m1__l_true_m1 x__nl_true_m1__l_true_0 x__nl_true_m1__l_true_p1 x__nl_true_m1__l_true_p2 x__nl_true_m1__l_true_p3 x__nl_true_m1__l_false_m3 x__nl_true_m1__l_false_m2 x__nl_true_m1__l_false_m1 x__nl_true_m1__l_false_0 x__nl_true_m1__l_false_p1 x__nl_true_m1__l_false_p2 x__nl_true_m1__l_false_p3 x__nl_true_0__l_true_p1 x__nl_true_0__l_true_p2 x__nl_true_0__l_true_p3 x__nl_true_0__l_false_m3 x__nl_true_0__l_false_m2 x__nl_true_0__l_false_m1 x__nl_true_0__l_false_0 x__nl_true_0__l_false_p1 x__nl_true_0__l_false_p2 x__nl_true_0__l_false_p3 x__nl_true_p1__l_true_m3 x__nl_true_p1__l_true_m2 x__nl_true_p1__l_true_m1 x__nl_true_p1__l_true_0 x__nl_true_p1__l_true_p1 x__nl_true_p1__l_true_p2 x__nl_true_p1__l_true_p3 x__nl_true_p1__l_false_m3 x__nl_true_p1__l_false_m2 x__nl_true_p1__l_false_m1 x__nl_true_p1__l_false_0 x__nl_true_p1__l_false_p1 x__nl_true_p1__l_false_p2 x__nl_true_p1__l_false_p3 x__nl_true_p2__l_true_m3 x__nl_true_p2__l_true_m2 x__nl_true_p2__l_true_m1 x__nl_true_p2__l_true_0 x__nl_true_p2__l_true_p1 x__nl_true_p2__l_true_p2 x__nl_true_p2__l_true_p3 x__nl_true_p2__l_false_m3 x__nl_true_p2__l_false_m2 x__nl_true_p2__l_false_m1 x__nl_true_p2__l_false_0 x__nl_true_p2__l_false_p1 x__nl_true_p2__l_false_p2 x__nl_true_p2__l_false_p3 x__nl_true_p3__l_true_m3 x__nl_true_p3__l_true_m2 x__nl_true_p3__l_true_m1 x__nl_true_p3__l_true_0 x__nl_true_p3__l_true_p1 x__nl_true_p3__l_true_p2 x__nl_true_p3__l_true_p3 x__nl_true_p3__l_false_m3 x__nl_true_p3__l_false_m2 x__nl_true_p3__l_false_m1 x__nl_true_p3__l_false_0 x__nl_true_p3__l_false_p1 x__nl_true_p3__l_false_p2 x__nl_true_p3__l_false_p3 x__nl_false_m3__l_true_m3 x__nl_false_m3__l_true_m2 x__nl_false_m3__l_true_m1 x__nl_false_m3__l_true_0 x__nl_false_m3__l_true_p1 x__nl_false_m3__l_true_p2 x__nl_false_m3__l_true_p3 x__nl_false_m3__l_false_m3 x__nl_false_m3__l_false_m2 x__nl_false_m3__l_false_m1 x__nl_false_m3__l_false_0 x__nl_false_m3__l_false_p1 x__nl_false_m3__l_false_p2 x__nl_false_m3__l_false_p3 x__nl_false_m2__l_true_m3 x__nl_false_m2__l_true_m2 x__nl_false_m2__l_true_m1 x__nl_false_m2__l_true_0 x__nl_false_m2__l_true_p1 x__nl_false_m2__l_true_p2 x__nl_false_m2__l_true_p3 x__nl_false_m2__l_false_m3 x__nl_false_m2__l_false_m2 x__nl_false_m2__l_false_m1 x__nl_false_m2__l_false_0 x__nl_false_m2__l_false_p1 x__nl_false_m2__l_false_p2 x__nl_false_m2__l_false_p3 x__nl_false_m1__l_true_m3 x__nl_false_m1__l_true_m2 x__nl_false_m1__l_true_m1 x__nl_false_m1__l_true_0 x__nl_false_m1__l_true_p1 x__nl_false_m1__l_true_p2 x__nl_false_m1__l_true_p3 x__nl_false_m1__l_false_m3 x__nl_false_m1__l_false_m2 x__nl_false_m1__l_false_m1 x__nl_false_m1__l_false_0 x__nl_false_m1__l_false_p1 x__nl_false_m1__l_false_p2 x__nl_false_m1__l_false_p3 x__nl_false_0__l_true_m3 x__nl_false_0__l_true_m2 x__nl_false_0__l_true_m1 x__nl_false_0__l_true_0 x__nl_false_0__l_true_p1 x__nl_false_0__l_true_p2 x__nl_false_0__l_true_p3 x__nl_false_0__l_false_m3 x__nl_false_0__l_false_m2 x__nl_false_0__l_false_m1 x__nl_false_0__l_false_0 x__nl_false_p1__l_true_m3 x__nl_false_p1__l_true_m2 x__nl_false_p1__l_true_m1 x__nl_false_p1__l_true_0 x__nl_false_p1__l_true_p1 x__nl_false_p1__l_true_p2 x__nl_false_p1__l_true_p3 x__nl_false_p1__l_false_m3 x__nl_false_p1__l_false_m2 x__nl_false_p1__l_false_m1 x__nl_false_p1__l_false_0 x__nl_false_p1__l_false_p1 x__nl_false_p1__l_false_p2 x__nl_false_p2__l_true_m3 x__nl_false_p2__l_true_m2 x__nl_false_p2__l_true_m1 x__nl_false_p2__l_true_0 x__nl_false_p2__l_true_p1 x__nl_false_p2__l_true_p2 x__nl_false_p2__l_true_p3 x__nl_false_p2__l_false_m3 x__nl_false_p2__l_false_m2 x__nl_false_p2__l_false_m1 x__nl_false_p2__l_false_0 x__nl_false_p2__l_false_p1 x__nl_false_p2__l_false_p2 x__nl_false_p3__l_true_m3 x__nl_false_p3__l_true_m2 x__nl_false_p3__l_true_m1 x__nl_false_p3__l_true_0 x__nl_false_p3__l_true_p1 x__nl_false_p3__l_true_p2 x__nl_false_p3__l_true_p3 x__nl_false_p3__l_false_m3 x__nl_false_p3__l_false_m2 x__nl_false_p3__l_false_m1 x__nl_false_p3__l_false_0 x__nl_false_p3__l_false_p1 x__nl_false_p3__l_false_p2 }
arcs {
{ _l_true_m3, _l_true_m3 } -> x__l_true_m3__l_true_m3 -> { _l_true_m3, _nl_true_m3 }
{ _l_true_m3, _l_true_m2 } -> x__l_true_m3__l_true_m2 -> { _l_true_m3, _nl_true_m2 }
{ _l_true_m3, _l_true_m1 } -> x__l_true_m3__l_true_m1 -> { _l_true_m3, _nl_true_m1 }
{ _l_true_m3, _l_true_0 } -> x__l_true_m3__l_true_0 -> { _l_true_m3, _nl_true_0 }
{ _l_true_m3, _l_true_p1 } -> x__l_true_m3__l_true_p1 -> { _l_true_m2, _nl_true_0 }
{ _l_true_m3, _l_true_p2 } -> x__l_true_m3__l_true_p2 -> { _l_true_m1, _nl_true_0 }
{ _l_true_m3, _l_true_p3 } -> x__l_true_m3__l_true_p3 -> { _l_true_0, _nl_true_0 }
{ _l_true_m2, _l_true_m2 } -> x__l_true_m2__l_true_m2 -> { _l_true_m3, _nl_true_m1 }
{ _l_true_m2, _l_true_m1 } -> x__l_true_m2__l_true_m1 -> { _l_true_m3, _nl_true_0 }
{ _l_true_m2, _l_true_0 } -> x__l_true_m2__l_true_0 -> { _l_true_m2, _nl_true_0 }
{ _l_true_m2, _l_true_p1 } -> x__l_true_m2__l_true_p1 -> { _l_true_m1, _nl_true_0 }
{ _l_true_m2, _l_true_p2 } -> x__l_true_m2__l_true_p2 -> { _l_true_0, _nl_true_0 }
{ _l_true_m2, _l_true_p3 } -> x__l_true_m2__l_true_p3 -> { _l_false_p1, _nl_false_0 }
{ _l_true_m1, _l_true_m1 } -> x__l_true_m1__l_true_m1 -> { _l_true_m2, _nl_true_0 }
{ _l_true_m1, _l_true_0 } -> x__l_true_m1__l_true_0 -> { _l_true_m1, _nl_true_0 }
{ _l_true_m1, _l_true_p1 } -> x__l_true_m1__l_true_p1 -> { _l_true_0, _nl_true_0 }
{ _l_true_m1, _l_true_p2 } -> x__l_true_m1__l_true_p2 -> { _l_false_p1, _nl_false_0 }
{ _l_true_m1, _l_true_p3 } -> x__l_true_m1__l_true_p3 -> { _l_false_p2, _nl_false_0 }
{ _l_true_0, _l_true_0 } -> x__l_true_0__l_true_0 -> { _l_true_0, _nl_true_0 }
{ _l_true_0, _l_true_p1 } -> x__l_true_0__l_true_p1 -> { _l_false_p1, _nl_false_0 }
{ _l_true_0, _l_true_p2 } -> x__l_true_0__l_true_p2 -> { _l_false_p2, _nl_false_0 }
{ _l_true_0, _l_true_p3 } -> x__l_true_0__l_true_p3 -> { _l_false_p3, _nl_false_0 }
{ _l_true_p1, _l_true_p1 } -> x__l_true_p1__l_true_p1 -> { _l_false_p2, _nl_false_0 }
{ _l_true_p1, _l_true_p2 } -> x__l_true_p1__l_true_p2 -> { _l_false_p3, _nl_false_0 }
{ _l_true_p1, _l_true_p3 } -> x__l_true_p1__l_true_p3 -> { _l_false_p3, _nl_false_p1 }
{ _l_true_p2, _l_true_p2 } -> x__l_true_p2__l_true_p2 -> { _l_false_p3, _nl_false_p1 }
{ _l_true_p2, _l_true_p3 } -> x__l_true_p2__l_true_p3 -> { _l_false_p3, _nl_false_p2 }
{ _l_true_p3, _l_true_p3 } -> x__l_true_p3__l_true_p3 -> { _l_false_p3, _nl_false_p3 }
{ _l_false_m3, _l_true_m3 } -> x__l_false_m3__l_true_m3 -> { _l_true_m3, _nl_true_m3 }
{ _l_false_m3, _l_true_m2 } -> x__l_false_m3__l_true_m2 -> { _l_true_m3, _nl_true_m2 }
{ _l_false_m3, _l_true_m1 } -> x__l_false_m3__l_true_m1 -> { _l_true_m3, _nl_true_m1 }
{ _l_false_m3, _l_true_0 } -> x__l_false_m3__l_true_0 -> { _l_true_m3, _nl_true_0 }
{ _l_false_m3, _l_true_p1 } -> x__l_false_m3__l_true_p1 -> { _l_true_m2, _nl_true_0 }
{ _l_false_m3, _l_true_p2 } -> x__l_false_m3__l_true_p2 -> { _l_true_m1, _nl_true_0 }
{ _l_false_m3, _l_true_p3 } -> x__l_false_m3__l_true_p3 -> { _l_true_0, _nl_true_0 }
{ _l_false_m3, _l_false_m3 } -> x__l_false_m3__l_false_m3 -> { _l_true_m3, _nl_true_m3 }
{ _l_false_m3, _l_false_m2 } -> x__l_false_m3__l_false_m2 -> { _l_true_m3, _nl_true_m2 }
{ _l_false_m3, _l_false_m1 } -> x__l_false_m3__l_false_m1 -> { _l_true_m3, _nl_true_m1 }
{ _l_false_m3, _l_false_0 } -> x__l_false_m3__l_false_0 -> { _l_true_m3, _nl_true_0 }
{ _l_false_m3, _l_false_p1 } -> x__l_false_m3__l_false_p1 -> { _l_true_m2, _nl_true_0 }
{ _l_false_m3, _l_false_p2 } -> x__l_false_m3__l_false_p2 -> { _l_true_m1, _nl_true_0 }
{ _l_false_m3, _l_false_p3 } -> x__l_false_m3__l_false_p3 -> { _l_true_0, _nl_true_0 }
{ _l_false_m2, _l_true_m3 } -> x__l_false_m2__l_true_m3 -> { _l_true_m3, _nl_true_m2 }
{ _l_false_m2, _l_true_m2 } -> x__l_false_m2__l_true_m2 -> { _l_true_m3, _nl_true_m1 }
{ _l_false_m2, _l_true_m1 } -> x__l_false_m2__l_true_m1 -> { _l_true_m3, _nl_true_0 }
{ _l_false_m2, _l_true_0 } -> x__l_false_m2__l_true_0 -> { _l_true_m2, _nl_true_0 }
{ _l_false_m2, _l_true_p1 } -> x__l_false_m2__l_true_p1 -> { _l_true_m1, _nl_true_0 }
{ _l_false_m2, _l_true_p2 } -> x__l_false_m2__l_true_p2 -> { _l_true_0, _nl_true_0 }
{ _l_false_m2, _l_true_p3 } -> x__l_false_m2__l_true_p3 -> { _l_false_p1, _nl_false_0 }
{ _l_false_m2, _l_false_m2 } -> x__l_false_m2__l_false_m2 -> { _l_true_m3, _nl_true_m1 }
{ _l_false_m2, _l_false_m1 } -> x__l_false_m2__l_false_m1 -> { _l_true_m3, _nl_true_0 }
{ _l_false_m2, _l_false_0 } -> x__l_false_m2__l_false_0 -> { _l_true_m2, _nl_true_0 }
{ _l_false_m2, _l_false_p1 } -> x__l_false_m2__l_false_p1 -> { _l_true_m1, _nl_true_0 }
{ _l_false_m2, _l_false_p2 } -> x__l_false_m2__l_false_p2 -> { _l_true_0, _nl_true_0 }
{ _l_false_m2, _l_false_p3 } -> x__l_false_m2__l_false_p3 -> { _l_false_p1, _nl_false_0 }
{ _l_false_m1, _l_true_m3 } -> x__l_false_m1__l_true_m3 -> { _l_true_m3, _nl_true_m1 }
{ _l_false_m1, _l_true_m2 } -> x__l_false_m1__l_true_m2 -> { _l_true_m3, _nl_true_0 }
{ _l_false_m1, _l_true_m1 } -> x__l_false_m1__l_true_m1 -> { _l_true_m2, _nl_true_0 }
{ _l_false_m1, _l_true_0 } -> x__l_false_m1__l_true_0 -> { _l_true_m1, _nl_true_0 }
{ _l_false_m1, _l_true_p1 } -> x__l_false_m1__l_true_p1 -> { _l_true_0, _nl_true_0 }
{ _l_false_m1, _l_true_p2 } -> x__l_false_m1__l_true_p2 -> { _l_false_p1, _nl_false_0 }
{ _l_false_m1, _l_true_p3 } -> x__l_false_m1__l_true_p3 -> { _l_false_p2, _nl_false_0 }
{ _l_false_m1, _l_false_m1 } -> x__l_false_m1__l_false_m1 -> { _l_true_m2, _nl_true_0 }
{ _l_false_m1, _l_false_0 } -> x__l_false_m1__l_false_0 -> { _l_true_m1, _nl_true_0 }
{ _l_false_m1, _l_false_p1 } -> x__l_false_m1__l_false_p1 -> { _l_true_0, _nl_true_0 }
{ _l_false_m1, _l_false_p2 } -> x__l_false_m1__l_false_p2 -> { _l_false_p1, _nl_false_0 }
{ _l_false_m1, _l_false_p3 } -> x__l_false_m1__l_false_p3 -> { _l_false_p2, _nl_false_0 }
{ _l_false_0, _l_true_m3 } -> x__l_false_0__l_true_m3 -> { _l_true_m3, _nl_true_0 }
{ _l_false_0, _l_true_m2 } -> x__l_false_0__l_true_m2 -> { _l_true_m2, _nl_true_0 }
{ _l_false_0, _l_true_m1 } -> x__l_false_0__l_true_m1 -> { _l_true_m1, _nl_true_0 }
{ _l_false_0, _l_true_0 } -> x__l_false_0__l_true_0 -> { _l_true_0, _nl_true_0 }
{ _l_false_0, _l_true_p1 } -> x__l_false_0__l_true_p1 -> { _l_false_p1, _nl_false_0 }
{ _l_false_0, _l_true_p2 } -> x__l_false_0__l_true_p2 -> { _l_false_p2, _nl_false_0 }
{ _l_false_0, _l_true_p3 } -> x__l_false_0__l_true_p3 -> { _l_false_p3, _nl_false_0 }
{ _l_false_0, _l_false_0 } -> x__l_false_0__l_false_0 -> { _l_true_0, _nl_true_0 }
{ _l_false_0, _l_false_p1 } -> x__l_false_0__l_false_p1 -> { _l_false_p1, _nl_false_0 }
{ _l_false_0, _l_false_p2 } -> x__l_false_0__l_false_p2 -> { _l_false_p2, _nl_false_0 }
{ _l_false_0, _l_false_p3 } -> x__l_false_0__l_false_p3 -> { _l_false_p3, _nl_false_0 }
{ _l_false_p1, _l_true_m3 } -> x__l_false_p1__l_true_m3 -> { _l_true_m2, _nl_true_0 }
{ _l_false_p1, _l_true_m2 } -> x__l_false_p1__l_true_m2 -> { _l_true_m1, _nl_true_0 }
{ _l_false_p1, _l_true_m1 } -> x__l_false_p1__l_true_m1 -> { _l_true_0, _nl_true_0 }
{ _l_false_p1, _l_true_0 } -> x__l_false_p1__l_true_0 -> { _l_false_p1, _nl_false_0 }
{ _l_false_p1, _l_true_p1 } -> x__l_false_p1__l_true_p1 -> { _l_false_p2, _nl_false_0 }
{ _l_false_p1, _l_true_p2 } -> x__l_false_p1__l_true_p2 -> { _l_false_p3, _nl_false_0 }
{ _l_false_p1, _l_true_p3 } -> x__l_false_p1__l_true_p3 -> { _l_false_p3, _nl_false_p1 }
{ _l_false_p1, _l_false_p1 } -> x__l_false_p1__l_false_p1 -> { _l_false_p2, _nl_false_0 }
{ _l_false_p1, _l_false_p2 } -> x__l_false_p1__l_false_p2 -> { _l_false_p3, _nl_false_0 }
{ _l_false_p1, _l_false_p3 } -> x__l_false_p1__l_false_p3 -> { _l_false_p3, _nl_false_p1 }
{ _l_false_p2, _l_true_m3 } -> x__l_false_p2__l_true_m3 -> { _l_true_m1, _nl_true_0 }
{ _l_false_p2, _l_true_m2 } -> x__l_false_p2__l_true_m2 -> { _l_true_0, _nl_true_0 }
{ _l_false_p2, _l_true_m1 } -> x__l_false_p2__l_true_m1 -> { _l_false_p1, _nl_false_0 }
{ _l_false_p2, _l_true_0 } -> x__l_false_p2__l_true_0 -> { _l_false_p2, _nl_false_0 }
{ _l_false_p2, _l_true_p1 } -> x__l_false_p2__l_true_p1 -> { _l_false_p3, _nl_false_0 }
{ _l_false_p2, _l_true_p2 } -> x__l_false_p2__l_true_p2 -> { _l_false_p3, _nl_false_p1 }
{ _l_false_p2, _l_true_p3 } -> x__l_false_p2__l_true_p3 -> { _l_false_p3, _nl_false_p2 }
{ _l_false_p2, _l_false_p2 } -> x__l_false_p2__l_false_p2 -> { _l_false_p3, _nl_false_p1 }
{ _l_false_p2, _l_false_p3 } -> x__l_false_p2__l_false_p3 -> { _l_false_p3, _nl_false_p2 }
{ _l_false_p3, _l_true_m3 } -> x__l_false_p3__l_true_m3 -> { _l_true_0, _nl_true_0 }
{ _l_false_p3, _l_true_m2 } -> x__l_false_p3__l_true_m2 -> { _l_false_p1, _nl_false_0 }
{ _l_false_p3, _l_true_m1 } -> x__l_false_p3__l_true_m1 -> { _l_false_p2, _nl_false_0 }
{ _l_false_p3, _l_true_0 } -> x__l_false_p3__l_true_0 -> { _l_false_p3, _nl_false_0 }
{ _l_false_p3, _l_true_p1 } -> x__l_false_p3__l_true_p1 -> { _l_false_p3, _nl_false_p1 }
{ _l_false_p3, _l_true_p2 } -> x__l_false_p3__l_true_p2 -> { _l_false_p3, _nl_false_p2 }
{ _l_false_p3, _l_true_p3 } -> x__l_false_p3__l_true_p3 -> { _l_false_p3, _nl_false_p3 }
{ _l_false_p3, _l_false_p3 } -> x__l_false_p3__l_false_p3 -> { _l_false_p3, _nl_false_p3 }
{ _nl_true_m3, _l_true_m2 } -> x__nl_true_m3__l_true_m2 -> { _l_true_m3, _nl_true_m2 }
{ _nl_true_m3, _l_true_m1 } -> x__nl_true_m3__l_true_m1 -> { _l_true_m3, _nl_true_m1 }
{ _nl_true_m3, _l_true_0 } -> x__nl_true_m3__l_true_0 -> { _l_true_m3, _nl_true_0 }
{ _nl_true_m3, _l_true_p1 } -> x__nl_true_m3__l_true_p1 -> { _l_true_m2, _nl_true_0 }
{ _nl_true_m3, _l_true_p2 } -> x__nl_true_m3__l_true_p2 -> { _l_true_m1, _nl_true_0 }
{ _nl_true_m3, _l_true_p3 } -> x__nl_true_m3__l_true_p3 -> { _l_true_0, _nl_true_0 }
{ _nl_true_m3, _l_false_m3 } -> x__nl_true_m3__l_false_m3 -> { _l_true_m3, _nl_true_m3 }
{ _nl_true_m3, _l_false_m2 } -> x__nl_true_m3__l_false_m2 -> { _l_true_m3, _nl_true_m2 }
{ _nl_true_m3, _l_false_m1 } -> x__nl_true_m3__l_false_m1 -> { _l_true_m3, _nl_true_m1 }
{ _nl_true_m3, _l_false_0 } -> x__nl_true_m3__l_false_0 -> { _l_true_m3, _nl_true_0 }
{ _nl_true_m3, _l_false_p1 } -> x__nl_true_m3__l_false_p1 -> { _l_true_m2, _nl_true_0 }
{ _nl_true_m3, _l_false_p2 } -> x__nl_true_m3__l_false_p2 -> { _l_true_m1, _nl_true_0 }
{ _nl_true_m3, _l_false_p3 } -> x__nl_true_m3__l_false_p3 -> { _l_true_0, _nl_true_0 }
{ _nl_true_m2, _l_true_m2 } -> x__nl_true_m2__l_true_m2 -> { _l_true_m3, _nl_true_m1 }
{ _nl_true_m2, _l_true_m1 } -> x__nl_true_m2__l_true_m1 -> { _l_true_m3, _nl_true_0 }
{ _nl_true_m2, _l_true_0 } -> x__nl_true_m2__l_true_0 -> { _l_true_m2, _nl_true_0 }
{ _nl_true_m2, _l_true_p1 } -> x__nl_true_m2__l_true_p1 -> { _l_true_m1, _nl_true_0 }
{ _nl_true_m2, _l_true_p2 } -> x__nl_true_m2__l_true_p2 -> { _l_true_0, _nl_true_0 }
{ _nl_true_m2, _l_true_p3 } -> x__nl_true_m2__l_true_p3 -> { _l_false_p1, _nl_false_0 }
{ _nl_true_m2, _l_false_m3 } -> x__nl_true_m2__l_false_m3 -> { _l_true_m3, _nl_true_m2 }
{ _nl_true_m2, _l_false_m2 } -> x__nl_true_m2__l_false_m2 -> { _l_true_m3, _nl_true_m1 }
{ _nl_true_m2, _l_false_m1 } -> x__nl_true_m2__l_false_m1 -> { _l_true_m3, _nl_true_0 }
{ _nl_true_m2, _l_false_0 } -> x__nl_true_m2__l_false_0 -> { _l_true_m2, _nl_true_0 }
{ _nl_true_m2, _l_false_p1 } -> x__nl_true_m2__l_false_p1 -> { _l_true_m1, _nl_true_0 }
{ _nl_true_m2, _l_false_p2 } -> x__nl_true_m2__l_false_p2 -> { _l_true_0, _nl_true_0 }
{ _nl_true_m2, _l_false_p3 } -> x__nl_true_m2__l_false_p3 -> { _l_false_p1, _nl_false_0 }
{ _nl_true_m1, _l_true_m2 } -> x__nl_true_m1__l_true_m2 -> { _l_true_m3, _nl_true_0 }
{ _nl_true_m1, _l_true_m1 } -> x__nl_true_m1__l_true_m1 -> { _l_true_m2, _nl_true_0 }
{ _nl_true_m1, _l_true_0 } -> x__nl_true_m1__l_true_0 -> { _l_true_m1, _nl_true_0 }
{ _nl_true_m1, _l_true_p1 } -> x__nl_true_m1__l_true_p1 -> { _l_true_0, _nl_true_0 }
{ _nl_true_m1, _l_true_p2 } -> x__nl_true_m1__l_true_p2 -> { _l_false_p1, _nl_false_0 }
{ _nl_true_m1, _l_true_p3 } -> x__nl_true_m1__l_true_p3 -> { _l_false_p2, _nl_false_0 }
{ _nl_true_m1, _l_false_m3 } -> x__nl_true_m1__l_false_m3 -> { _l_true_m3, _nl_true_m1 }
{ _nl_true_m1, _l_false_m2 } -> x__nl_true_m1__l_false_m2 -> { _l_true_m3, _nl_true_0 }
{ _nl_true_m1, _l_false_m1 } -> x__nl_true_m1__l_false_m1 -> { _l_true_m2, _nl_true_0 }
{ _nl_true_m1, _l_false_0 } -> x__nl_true_m1__l_false_0 -> { _l_true_m1, _nl_true_0 }
{ _nl_true_m1, _l_false_p1 } -> x__nl_true_m1__l_false_p1 -> { _l_true_0, _nl_true_0 }
{ _nl_true_m1, _l_false_p2 } -> x__nl_true_m1__l_false_p2 -> { _l_false_p1, _nl_false_0 }
{ _nl_true_m1, _l_false_p3 } -> x__nl_true_m1__l_false_p3 -> { _l_false_p2, _nl_false_0 }
{ _nl_true_0, _l_true_p1 } -> x__nl_true_0__l_true_p1 -> { _l_false_p1, _nl_false_0 }
{ _nl_true_0, _l_true_p2 } -> x__nl_true_0__l_true_p2 -> { _l_false_p2, _nl_false_0 }
{ _nl_true_0, _l_true_p3 } -> x__nl_true_0__l_true_p3 -> { _l_false_p3, _nl_false_0 }
{ _nl_true_0, _l_false_m3 } -> x__nl_true_0__l_false_m3 -> { _l_true_m3, _nl_true_0 }
{ _nl_true_0, _l_false_m2 } -> x__nl_true_0__l_false_m2 -> { _l_true_m2, _nl_true_0 }
{ _nl_true_0, _l_false_m1 } -> x__nl_true_0__l_false_m1 -> { _l_true_m1, _nl_true_0 }
{ _nl_true_0, _l_false_0 } -> x__nl_true_0__l_false_0 -> { _l_true_0, _nl_true_0 }
{ _nl_true_0, _l_false_p1 } -> x__nl_true_0__l_false_p1 -> { _l_false_p1, _nl_false_0 }
{ _nl_true_0, _l_false_p2 } -> x__nl_true_0__l_false_p2 -> { _l_false_p2, _nl_false_0 }
{ _nl_true_0, _l_false_p3 } -> x__nl_true_0__l_false_p3 -> { _l_false_p3, _nl_false_0 }
{ _nl_true_p1, _l_true_m3 } -> x__nl_true_p1__l_true_m3 -> { _l_true_m2, _nl_true_0 }
{ _nl_true_p1, _l_true_m2 } -> x__nl_true_p1__l_true_m2 -> { _l_true_m1, _nl_true_0 }
{ _nl_true_p1, _l_true_m1 } -> x__nl_true_p1__l_true_m1 -> { _l_true_0, _nl_true_0 }
{ _nl_true_p1, _l_true_0 } -> x__nl_true_p1__l_true_0 -> { _l_false_p1, _nl_false_0 }
{ _nl_true_p1, _l_true_p1 } -> x__nl_true_p1__l_true_p1 -> { _l_false_p2, _nl_false_0 }
{ _nl_true_p1, _l_true_p2 } -> x__nl_true_p1__l_true_p2 -> { _l_false_p3, _nl_false_0 }
{ _nl_true_p1, _l_true_p3 } -> x__nl_true_p1__l_true_p3 -> { _l_false_p3, _nl_false_p1 }
{ _nl_true_p1, _l_false_m3 } -> x__nl_true_p1__l_false_m3 -> { _l_true_m2, _nl_true_0 }
{ _nl_true_p1, _l_false_m2 } -> x__nl_true_p1__l_false_m2 -> { _l_true_m1, _nl_true_0 }
{ _nl_true_p1, _l_false_m1 } -> x__nl_true_p1__l_false_m1 -> { _l_true_0, _nl_true_0 }
{ _nl_true_p1, _l_false_0 } -> x__nl_true_p1__l_false_0 -> { _l_false_p1, _nl_false_0 }
{ _nl_true_p1, _l_false_p1 } -> x__nl_true_p1__l_false_p1 -> { _l_false_p2, _nl_false_0 }
{ _nl_true_p1, _l_false_p2 } -> x__nl_true_p1__l_false_p2 -> { _l_false_p3, _nl_false_0 }
{ _nl_true_p1, _l_false_p3 } -> x__nl_true_p1__l_false_p3 -> { _l_false_p3, _nl_false_p1 }
{ _nl_true_p2, _l_true_m3 } -> x__nl_true_p2__l_true_m3 -> { _l_true_m1, _nl_true_0 }
{ _nl_true_p2, _l_true_m2 } -> x__nl_true_p2__l_true_m2 -> { _l_true_0, _nl_true_0 }
{ _nl_true_p2, _l_true_m1 } -> x__nl_true_p2__l_true_m1 -> { _l_false_p1, _nl_false_0 }
{ _nl_true_p2, _l_true_0 } -> x__nl_true_p2__l_true_0 -> { _l_false_p2, _nl_false_0 }
{ _nl_true_p2, _l_true_p1 } -> x__nl_true_p2__l_true_p1 -> { _l_false_p3, _nl_false_0 }
{ _nl_true_p2, _l_true_p2 } -> x__nl_true_p2__l_true_p2 -> { _l_false_p3, _nl_false_p1 }
{ _nl_true_p2, _l_true_p3 } -> x__nl_true_p2__l_true_p3 -> { _l_false_p3, _nl_false_p2 }
{ _nl_true_p2, _l_false_m3 } -> x__nl_true_p2__l_false_m3 -> { _l_true_m1, _nl_true_0 }
{ _nl_true_p2, _l_false_m2 } -> x__nl_true_p2__l_false_m2 -> { _l_true_0, _nl_true_0 }
{ _nl_true_p2, _l_false_m1 } -> x__nl_true_p2__l_false_m1 -> { _l_false_p1, _nl_false_0 }
{ _nl_true_p2, _l_false_0 } -> x__nl_true_p2__l_false_0 -> { _l_false_p2, _nl_false_0 }
{ _nl_true_p2, _l_false_p1 } -> x__nl_true_p2__l_false_p1 -> { _l_false_p3, _nl_false_0 }
{ _nl_true_p2, _l_false_p2 } -> x__nl_true_p2__l_false_p2 -> { _l_false_p3, _nl_false_p1 }
{ _nl_true_p2, _l_false_p3 } -> x__nl_true_p2__l_false_p3 -> { _l_false_p3, _nl_false_p2 }
{ _nl_true_p3, _l_true_m3 } -> x__nl_true_p3__l_true_m3 -> { _l_true_0, _nl_true_0 }
{ _nl_true_p3, _l_true_m2 } -> x__nl_true_p3__l_true_m2 -> { _l_false_p1, _nl_false_0 }
{ _nl_true_p3, _l_true_m1 } -> x__nl_true_p3__l_true_m1 -> { _l_false_p2, _nl_false_0 }
{ _nl_true_p3, _l_true_0 } -> x__nl_true_p3__l_true_0 -> { _l_false_p3, _nl_false_0 }
{ _nl_true_p3, _l_true_p1 } -> x__nl_true_p3__l_true_p1 -> { _l_false_p3, _nl_false_p1 }
{ _nl_true_p3, _l_true_p2 } -> x__nl_true_p3__l_true_p2 -> { _l_false_p3, _nl_false_p2 }
{ _nl_true_p3, _l_true_p3 } -> x__nl_true_p3__l_true_p3 -> { _l_false_p3, _nl_false_p3 }
{ _nl_true_p3, _l_false_m3 } -> x__nl_true_p3__l_false_m3 -> { _l_true_0, _nl_true_0 }
{ _nl_true_p3, _l_false_m2 } -> x__nl_true_p3__l_false_m2 -> { _l_false_p1, _nl_false_0 }
{ _nl_true_p3, _l_false_m1 } -> x__nl_true_p3__l_false_m1 -> { _l_false_p2, _nl_false_0 }
{ _nl_true_p3, _l_false_0 } -> x__nl_true_p3__l_false_0 -> { _l_false_p3, _nl_false_0 }
{ _nl_true_p3, _l_false_p1 } -> x__nl_true_p3__l_false_p1 -> { _l_false_p3, _nl_false_p1 }
{ _nl_true_p3, _l_false_p2 } -> x__nl_true_p3__l_false_p2 -> { _l_false_p3, _nl_false_p2 }
{ _nl_true_p3, _l_false_p3 } -> x__nl_true_p3__l_false_p3 -> { _l_false_p3, _nl_false_p3 }
{ _nl_false_m3, _l_true_m3 } -> x__nl_false_m3__l_true_m3 -> { _l_true_m3, _nl_true_m3 }
{ _nl_false_m3, _l_true_m2 } -> x__nl_false_m3__l_true_m2 -> { _l_true_m3, _nl_true_m2 }
{ _nl_false_m3, _l_true_m1 } -> x__nl_false_m3__l_true_m1 -> { _l_true_m3, _nl_true_m1 }
{ _nl_false_m3, _l_true_0 } -> x__nl_false_m3__l_true_0 -> { _l_true_m3, _nl_true_0 }
{ _nl_false_m3, _l_true_p1 } -> x__nl_false_m3__l_true_p1 -> { _l_true_m2, _nl_true_0 }
{ _nl_false_m3, _l_true_p2 } -> x__nl_false_m3__l_true_p2 -> { _l_true_m1, _nl_true_0 }
{ _nl_false_m3, _l_true_p3 } -> x__nl_false_m3__l_true_p3 -> { _l_true_0, _nl_true_0 }
{ _nl_false_m3, _l_false_m3 } -> x__nl_false_m3__l_false_m3 -> { _l_true_m3, _nl_true_m3 }
{ _nl_false_m3, _l_false_m2 } -> x__nl_false_m3__l_false_m2 -> { _l_true_m3, _nl_true_m2 }
{ _nl_false_m3, _l_false_m1 } -> x__nl_false_m3__l_false_m1 -> { _l_true_m3, _nl_true_m1 }
{ _nl_false_m3, _l_false_0 } -> x__nl_false_m3__l_false_0 -> { _l_true_m3, _nl_true_0 }
{ _nl_false_m3, _l_false_p1 } -> x__nl_false_m3__l_false_p1 -> { _l_true_m2, _nl_true_0 }
{ _nl_false_m3, _l_false_p2 } -> x__nl_false_m3__l_false_p2 -> { _l_true_m1, _nl_true_0 }
{ _nl_false_m3, _l_false_p3 } -> x__nl_false_m3__l_false_p3 -> { _l_true_0, _nl_true_0 }
{ _nl_false_m2, _l_true_m3 } -> x__nl_false_m2__l_true_m3 -> { _l_true_m3, _nl_true_m2 }
{ _nl_false_m2, _l_true_m2 } -> x__nl_false_m2__l_true_m2 -> { _l_true_m3, _nl_true_m1 }
{ _nl_false_m2, _l_true_m1 } -> x__nl_false_m2__l_true_m1 -> { _l_true_m3, _nl_true_0 }
{ _nl_false_m2, _l_true_0 } -> x__nl_false_m2__l_true_0 -> { _l_true_m2, _nl_true_0 }
{ _nl_false_m2, _l_true_p1 } -> x__nl_false_m2__l_true_p1 -> { _l_true_m1, _nl_true_0 }
{ _nl_false_m2, _l_true_p2 } -> x__nl_false_m2__l_true_p2 -> { _l_true_0, _nl_true_0 }
{ _nl_false_m2, _l_true_p3 } -> x__nl_false_m2__l_true_p3 -> { _l_false_p1, _nl_false_0 }
{ _nl_false_m2, _l_false_m3 } -> x__nl_false_m2__l_false_m3 -> { _l_true_m3, _nl_true_m2 }
{ _nl_false_m2, _l_false_m2 } -> x__nl_false_m2__l_false_m2 -> { _l_true_m3, _nl_true_m1 }
{ _nl_false_m2, _l_false_m1 } -> x__nl_false_m2__l_false_m1 -> { _l_true_m3, _nl_true_0 }
{ _nl_false_m2, _l_false_0 } -> x__nl_false_m2__l_false_0 -> { _l_true_m2, _nl_true_0 }
{ _nl_false_m2, _l_false_p1 } -> x__nl_false_m2__l_false_p1 -> { _l_true_m1, _nl_true_0 }
{ _nl_false_m2, _l_false_p2 } -> x__nl_false_m2__l_false_p2 -> { _l_true_0, _nl_true_0 }
{ _nl_false_m2, _l_false_p3 } -> x__nl_false_m2__l_false_p3 -> { _l_false_p1, _nl_false_0 }
{ _nl_false_m1, _l_true_m3 } -> x__nl_false_m1__l_true_m3 -> { _l_true_m3, _nl_true_m1 }
{ _nl_false_m1, _l_true_m2 } -> x__nl_false_m1__l_true_m2 -> { _l_true_m3, _nl_true_0 }
{ _nl_false_m1, _l_true_m1 } -> x__nl_false_m1__l_true_m1 -> { _l_true_m2, _nl_true_0 }
{ _nl_false_m1, _l_true_0 } -> x__nl_false_m1__l_true_0 -> { _l_true_m1, _nl_true_0 }
{ _nl_false_m1, _l_true_p1 } -> x__nl_false_m1__l_true_p1 -> { _l_true_0, _nl_true_0 }
{ _nl_false_m1, _l_true_p2 } -> x__nl_false_m1__l_true_p2 -> { _l_false_p1, _nl_false_0 }
{ _nl_false_m1, _l_true_p3 } -> x__nl_false_m1__l_true_p3 -> { _l_false_p2, _nl_false_0 }
{ _nl_false_m1, _l_false_m3 } -> x__nl_false_m1__l_false_m3 -> { _l_true_m3, _nl_true_m1 }
{ _nl_false_m1, _l_false_m2 } -> x__nl_false_m1__l_false_m2 -> { _l_true_m3, _nl_true_0 }
{ _nl_false_m1, _l_false_m1 } -> x__nl_false_m1__l_false_m1 -> { _l_true_m2, _nl_true_0 }
{ _nl_false_m1, _l_false_0 } -> x__nl_false_m1__l_false_0 -> { _l_true_m1, _nl_true_0 }
{ _nl_false_m1, _l_false_p1 } -> x__nl_false_m1__l_false_p1 -> { _l_true_0, _nl_true_0 }
{ _nl_false_m1, _l_false_p2 } -> x__nl_false_m1__l_false_p2 -> { _l_false_p1, _nl_false_0 }
{ _nl_false_m1, _l_false_p3 } -> x__nl_false_m1__l_false_p3 -> { _l_false_p2, _nl_false_0 }
{ _nl_false_0, _l_true_m3 } -> x__nl_false_0__l_true_m3 -> { _l_true_m3, _nl_true_0 }
{ _nl_false_0, _l_true_m2 } -> x__nl_false_0__l_true_m2 -> { _l_true_m2, _nl_true_0 }
{ _nl_false_0, _l_true_m1 } -> x__nl_false_0__l_true_m1 -> { _l_true_m1, _nl_true_0 }
{ _nl_false_0, _l_true_0 } -> x__nl_false_0__l_true_0 -> { _l_true_0, _nl_true_0 }
{ _nl_false_0, _l_true_p1 } -> x__nl_false_0__l_true_p1 -> { _l_false_p1, _nl_false_0 }
{ _nl_false_0, _l_true_p2 } -> x__nl_false_0__l_true_p2 -> { _l_false_p2, _nl_false_0 }
{ _nl_false_0, _l_true_p3 } -> x__nl_false_0__l_true_p3 -> { _l_false_p3, _nl_false_0 }
{ _nl_false_0, _l_false_m3 } -> x__nl_false_0__l_false_m3 -> { _l_true_m3, _nl_true_0 }
{ _nl_false_0, _l_false_m2 } -> x__nl_false_0__l_false_m2 -> { _l_true_m2, _nl_true_0 }
{ _nl_false_0, _l_false_m1 } -> x__nl_false_0__l_false_m1 -> { _l_true_m1, _nl_true_0 }
{ _nl_false_0, _l_false_0 } -> x__nl_false_0__l_false_0 -> { _l_true_0, _nl_true_0 }
{ _nl_false_p1, _l_true_m3 } -> x__nl_false_p1__l_true_m3 -> { _l_true_m2, _nl_true_0 }
{ _nl_false_p1, _l_true_m2 } -> x__nl_false_p1__l_true_m2 -> { _l_true_m1, _nl_true_0 }
{ _nl_false_p1, _l_true_m1 } -> x__nl_false_p1__l_true_m1 -> { _l_true_0, _nl_true_0 }
{ _nl_false_p1, _l_true_0 } -> x__nl_false_p1__l_true_0 -> { _l_false_p1, _nl_false_0 }
{ _nl_false_p1, _l_true_p1 } -> x__nl_false_p1__l_true_p1 -> { _l_false_p2, _nl_false_0 }
{ _nl_false_p1, _l_true_p2 } -> x__nl_false_p1__l_true_p2 -> { _l_false_p3, _nl_false_0 }
{ _nl_false_p1, _l_true_p3 } -> x__nl_false_p1__l_true_p3 -> { _l_false_p3, _nl_false_p1 }
{ _nl_false_p1, _l_false_m3 } -> x__nl_false_p1__l_false_m3 -> { _l_true_m2, _nl_true_0 }
{ _nl_false_p1, _l_false_m2 } -> x__nl_false_p1__l_false_m2 -> { _l_true_m1, _nl_true_0 }
{ _nl_false_p1, _l_false_m1 } -> x__nl_false_p1__l_false_m1 -> { _l_true_0, _nl_true_0 }
{ _nl_false_p1, _l_false_0 } -> x__nl_false_p1__l_false_0 -> { _l_false_p1, _nl_false_0 }
{ _nl_false_p1, _l_false_p1 } -> x__nl_false_p1__l_false_p1 -> { _l_false_p2, _nl_false_0 }
{ _nl_false_p1, _l_false_p2 } -> x__nl_false_p1__l_false_p2 -> { _l_false_p3, _nl_false_0 }
{ _nl_false_p2, _l_true_m3 } -> x__nl_false_p2__l_true_m3 -> { _l_true_m1, _nl_true_0 }
{ _nl_false_p2, _l_true_m2 } -> x__nl_false_p2__l_true_m2 -> { _l_true_0, _nl_true_0 }
{ _nl_false_p2, _l_true_m1 } -> x__nl_false_p2__l_true_m1 -> { _l_false_p1, _nl_false_0 }
{ _nl_false_p2, _l_true_0 } -> x__nl_false_p2__l_true_0 -> { _l_false_p2, _nl_false_0 }
{ _nl_false_p2, _l_true_p1 } -> x__nl_false_p2__l_true_p1 -> { _l_false_p3, _nl_false_0 }
{ _nl_false_p2, _l_true_p2 } -> x__nl_false_p2__l_true_p2 -> { _l_false_p3, _nl_false_p1 }
{ _nl_false_p2, _l_true_p3 } -> x__nl_false_p2__l_true_p3 -> { _l_false_p3, _nl_false_p2 }
{ _nl_false_p2, _l_false_m3 } -> x__nl_false_p2__l_false_m3 -> { _l_true_m1, _nl_true_0 }
{ _nl_false_p2, _l_false_m2 } -> x__nl_false_p2__l_false_m2 -> { _l_true_0, _nl_true_0 }
{ _nl_false_p2, _l_false_m1 } -> x__nl_false_p2__l_false_m1 -> { _l_false_p1, _nl_false_0 }
{ _nl_false_p2, _l_false_0 } -> x__nl_false_p2__l_false_0 -> { _l_false_p2, _nl_false_0 }
{ _nl_false_p2, _l_false_p1 } -> x__nl_false_p2__l_false_p1 -> { _l_false_p3, _nl_false_0 }
{ _nl_false_p2, _l_false_p2 } -> x__nl_false_p2__l_false_p2 -> { _l_false_p3, _nl_false_p1 }
{ _nl_false_p3, _l_true_m3 } -> x__nl_false_p3__l_true_m3 -> { _l_true_0, _nl_true_0 }
{ _nl_false_p3, _l_true_m2 } -> x__nl_false_p3__l_true_m2 -> { _l_false_p1, _nl_false_0 }
{ _nl_false_p3, _l_true_m1 } -> x__nl_false_p3__l_true_m1 -> { _l_false_p2, _nl_false_0 }
{ _nl_false_p3, _l_true_0 } -> x__nl_false_p3__l_true_0 -> { _l_false_p3, _nl_false_0 }
{ _nl_false_p3, _l_true_p1 } -> x__nl_false_p3__l_true_p1 -> { _l_false_p3, _nl_false_p1 }
{ _nl_false_p3, _l_true_p2 } -> x__nl_false_p3__l_true_p2 -> { _l_false_p3, _nl_false_p2 }
{ _nl_false_p3, _l_true_p3 } -> x__nl_false_p3__l_true_p3 -> { _l_false_p3, _nl_false_p3 }
{ _nl_false_p3, _l_false_m3 } -> x__nl_false_p3__l_false_m3 -> { _l_true_0, _nl_true_0 }
{ _nl_false_p3, _l_false_m2 } -> x__nl_false_p3__l_false_m2 -> { _l_false_p1, _nl_false_0 }
{ _nl_false_p3, _l_false_m1 } -> x__nl_false_p3__l_false_m1 -> { _l_false_p2, _nl_false_0 }
{ _nl_false_p3, _l_false_0 } -> x__nl_false_p3__l_false_0 -> { _l_false_p3, _nl_false_0 }
{ _nl_false_p3, _l_false_p1 } -> x__nl_false_p3__l_false_p1 -> { _l_false_p3, _nl_false_p1 }
{ _nl_false_p3, _l_false_p2 } -> x__nl_false_p3__l_false_p2 -> { _l_false_p3, _nl_false_p2 }
}
initial {_l_true_m3 _l_true_m2 _l_true_m1 _l_true_0 _l_true_p1 _l_true_p2 _l_true_p3 _l_false_m3 _l_false_m2 _l_false_m1 _l_false_0 _l_false_p1 _l_false_p2 _l_false_p3}
true {_l_true_m3 _l_true_m2 _l_true_m1 _l_true_0 _l_true_p1 _l_true_p2 _l_true_p3 _nl_true_m3 _nl_true_m2 _nl_true_m1 _nl_true_0 _nl_true_p1 _nl_true_p2 _nl_true_p3}
false {_l_false_m3 _l_false_m2 _l_false_m1 _l_false_0 _l_false_p1 _l_false_p2 _l_false_p3 _nl_false_m3 _nl_false_m2 _nl_false_m1 _nl_false_0 _nl_false_p1 _nl_false_p2 _nl_false_p3}
}
src/Main.hs
View file @
430f9c2e
...
...
@@ -38,8 +38,8 @@ structuralAnalysis pp = do
verbosePut
0
$
"States : "
++
show
(
length
(
states
pp
))
verbosePut
0
$
"Transitions : "
++
show
(
length
(
transitions
pp
))
verbosePut
0
$
"Initial states : "
++
show
(
length
(
initialStates
pp
))
verbosePut
0
$
"Yes states : "
++
show
(
length
(
yes
States
pp
))
verbosePut
0
$
"No states : "
++
show
(
length
(
no
States
pp
))
verbosePut
0
$
"Yes states : "
++
show
(
length
(
true
States
pp
))
verbosePut
0
$
"No states : "
++
show
(
length
(
false
States
pp
))
checkFile
::
String
->
OptIO
PropResult
checkFile
file
=
do
...
...
src/Parser/PP.hs
View file @
430f9c2e
...
...
@@ -77,11 +77,11 @@ transitions = reserved "transitions" *> identList
initial
::
Parser
[
String
]
initial
=
reserved
"initial"
*>
identList
yes
States
::
Parser
[
String
]
yesStates
=
reserved
"yes
"
*>
identList
true
States
::
Parser
[
String
]
trueStates
=
reserved
"true
"
*>
identList
no
States
::
Parser
[
String
]
noStates
=
reserved
"no
"
*>
identList
false
States
::
Parser
[
String
]
falseStates
=
reserved
"false
"
*>
identList
arc
::
Parser
[(
String
,
String
,
Integer
)]
arc
=
do
...
...
@@ -105,8 +105,8 @@ arcs = do
data
Statement
=
States
[
String
]
|
Transitions
[
String
]
|
Initial
[
String
]
|
Yes
Statement
[
String
]
|
No
Statement
[
String
]
|
True
Statement
[
String
]
|
False
Statement
[
String
]
|
Arcs
[(
String
,
String
,
Integer
)]
statement
::
Parser
Statement
...
...
@@ -114,8 +114,8 @@ statement = States <$> states <|>
Transitions
<$>
transitions
<|>
Arcs
<$>
arcs
<|>
Initial
<$>
initial
<|>
YesStatement
<$>
yes
States
<|>
NoStatement
<$>
no
States
TrueStatement
<$>
true
States
<|>
FalseStatement
<$>
false
States
populationProtocol
::
Parser
PopulationProtocol
populationProtocol
=
do
...
...
@@ -123,16 +123,16 @@ populationProtocol = do
reserved
"protocol"
name
<-
option
""
ident
statements
<-
braces
(
many
statement
)
let
(
qs
,
ts
,
is
,
ys
,
ns
,
as
)
=
foldl
splitStatement
(
[]
,
[]
,
[]
,
[]
,
[]
,
[]
)
statements
return
$
makePopulationProtocolFromStrings
name
qs
ts
is
ys
ns
as
let
(
qs
,
ts
,
qinitial
,
qtrue
,
qfalse
,
as
)
=
foldl
splitStatement
(
[]
,
[]
,
[]
,
[]
,
[]
,
[]
)
statements
return
$
makePopulationProtocolFromStrings
name
qs
ts
qinitial
qtrue
qfalse
as
where
splitStatement
(
qs
,
ts
,
is
,
ys
,
ns
,
as
)
stmnt
=
case
stmnt
of
States
q
->
(
q
++
qs
,
ts
,
is
,
ys
,
ns
,
as
)
Transitions
t
->
(
qs
,
t
++
ts
,
is
,
ys
,
ns
,
as
)
Initial
i
->
(
qs
,
ts
,
i
++
is
,
ys
,
ns
,
as
)
YesStatement
y
->
(
qs
,
ts
,
is
,
y
++
ys
,
ns
,
as
)
NoStatement
n
->
(
qs
,
ts
,
is
,
ys
,
n
++
ns
,
as
)
Arcs
a
->
(
qs
,
ts
,
is
,
ys
,
ns
,
a
++
as
)
splitStatement
(
qs
,
ts
,
qinitial
,
qtrue
,
qfalse
,
as
)
stmnt
=
case
stmnt
of
States
q
->
(
q
++
qs
,
ts
,
qinitial
,
qtrue
,
qfalse
,
as
)
Transitions
t
->
(
qs
,
t
++
ts
,
qinitial
,
qtrue
,
qfalse
,
as
)
Initial
q
->
(
qs
,
ts
,
q
++
qinitial
,
qtrue
,
qfalse
,
as
)
TrueStatement
q
->
(
qs
,
ts
,
qinitial
,
q
++
qtrue
,
qfalse
,
as
)
FalseStatement
q
->
(
qs
,
ts
,
qinitial
,
qtrue
,
q
++
qfalse
,
as
)
Arcs
a
->
(
qs
,
ts
,
qinitial
,
qtrue
,
qfalse
,
a
++
as
)
binary
::
String
->
(
a
->
a
->
a
)
->
Assoc
->
Operator
String
()
Identity
a
binary
name
fun
=
Infix
(
reservedOp
name
*>
return
fun
)
...
...
src/PopulationProtocol.hs
View file @
430f9c2e
...
...
@@ -5,7 +5,7 @@ module PopulationProtocol
(
PopulationProtocol
,
State
(
..
),
Transition
(
..
),
Configuration
,
FlowVector
,
RConfiguration
,
RFlowVector
,
renameState
,
renameTransition
,
renameStatesAndTransitions
,
name
,
showNetName
,
states
,
transitions
,
initialStates
,
yesStates
,
no
States
,
name
,
showNetName
,
states
,
transitions
,
initialStates
,
trueStates
,
false
States
,
pre
,
lpre
,
post
,
lpost
,
mpre
,
mpost
,
context
,
makePopulationProtocol
,
makePopulationProtocolWithTrans
,
makePopulationProtocolFromStrings
,
makePopulationProtocolWithTransFromStrings
,
...
...
@@ -72,8 +72,8 @@ data PopulationProtocol = PopulationProtocol {
states
::
[
State
],
transitions
::
[
Transition
],
initialStates
::
[
State
],
yes
States
::
[
State
],
no
States
::
[
State
],
true
States
::
[
State
],
false
States
::
[
State
],
adjacencyQ
::
M
.
Map
State
([(
Transition
,
Integer
)],
[(
Transition
,
Integer
)]),
adjacencyT
::
M
.
Map
Transition
([(
State
,
Integer
)],
[(
State
,
Integer
)])
}
...
...
@@ -84,12 +84,12 @@ showNetName pp = "Population protocol" ++
instance
Show
PopulationProtocol
where
show
pp
=
showNetName
pp
++
"
\n
States: "
++
show
(
states
pp
)
++
"
\n
Transitions: "
++
show
(
transitions
pp
)
++
"
\n
Initial states: "
++
show
(
initialStates
pp
)
++
"
\n
Yes states: "
++
show
(
yes
States
pp
)
++
"
\n
No states: "
++
show
(
no
States
pp
)
++
"
\n
State arcs:
\n
"
++
unlines
"
\n
States
: "
++
show
(
states
pp
)
++
"
\n
Transitions
: "
++
show
(
transitions
pp
)
++
"
\n
Initial states
: "
++
show
(
initialStates
pp
)
++
"
\n
True states : "
++
show
(
true
States
pp
)
++
"
\n
False states : "
++
show
(
false
States
pp
)
++
"
\n
State arcs
:
\n
"
++
unlines
(
map
showContext
(
M
.
toList
(
adjacencyQ
pp
)))
++
"
\n
Transition arcs:
\n
"
++
unlines
(
map
showContext
(
M
.
toList
(
adjacencyT
pp
)))
...
...
@@ -112,10 +112,10 @@ renameStatesAndTransitions f pp =
listSet
$
map
(
renameTransition
f
)
$
transitions
pp
,
initialStates
=
listSet
$
map
(
renameState
f
)
$
initialStates
pp
,
yes
States
=
listSet
$
map
(
renameState
f
)
$
yes
States
pp
,
no
States
=
listSet
$
map
(
renameState
f
)
$
no
States
pp
,
true
States
=
listSet
$
map
(
renameState
f
)
$
true
States
pp
,
false
States
=
listSet
$
map
(
renameState
f
)
$
false
States
pp
,
adjacencyQ
=
mapAdjacency
(
renameState
f
)
(
renameTransition
f
)
$
adjacencyQ
pp
,
adjacencyT
=
mapAdjacency
(
renameTransition
f
)
(
renameState
f
)
$
...
...
@@ -129,14 +129,14 @@ makePopulationProtocol :: String -> [State] -> [Transition] ->
[
State
]
->
[
State
]
->
[
State
]
->
[
Either
(
Transition
,
State
,
Integer
)
(
State
,
Transition
,
Integer
)]
->
PopulationProtocol
makePopulationProtocol
name
states
transitions
initialStates
yesStates
no
States
arcs
=
makePopulationProtocol
name
states
transitions
initialStates
trueStates
false
States
arcs
=
PopulationProtocol
{
name
=
name
,
states
=
listSet
states
,
transitions
=
listSet
transitions
,
initialStates
=
listSet
initialStates
,
yesStates
=
listSet
yes
States
,
noStates
=
listSet
no
States
,
trueStates
=
listSet
true
States
,
falseStates
=
listSet
false
States
,
adjacencyQ
=
M
.
map
(
listMap
***
listMap
)
adQ
,
adjacencyT
=
M
.
map
(
listMap
***
listMap
)
adT
}
...
...
@@ -160,14 +160,14 @@ makePopulationProtocol name states transitions initialStates yesStates noStates
makePopulationProtocolFromStrings
::
String
->
[
String
]
->
[
String
]
->
[
String
]
->
[
String
]
->
[
String
]
->
[(
String
,
String
,
Integer
)]
->
PopulationProtocol
makePopulationProtocolFromStrings
name
states
transitions
initialStates
yesStates
no
States
arcs
=
makePopulationProtocolFromStrings
name
states
transitions
initialStates
trueStates
false
States
arcs
=
makePopulationProtocol
name
(
map
State
(
S
.
toAscList
stateSet
))
(
map
Transition
(
S
.
toAscList
transitionSet
))
(
map
State
initialStates
)
(
map
State
yes
States
)
(
map
State
no
States
)
(
map
State
true
States
)
(
map
State
false
States
)
(
map
toEitherArc
arcs
)
where
stateSet
=
S
.
fromList
states
...
...
@@ -194,8 +194,8 @@ makePopulationProtocolFromStrings name states transitions initialStates yesState
makePopulationProtocolWithTrans
::
String
->
[
State
]
->
[
State
]
->
[
State
]
->
[
State
]
->
[(
Transition
,
([(
State
,
Integer
)],
[(
State
,
Integer
)]))]
->
PopulationProtocol
makePopulationProtocolWithTrans
name
states
initialStates
yesStates
no
States
ts
=
makePopulationProtocol
name
states
(
map
fst
ts
)
initialStates
yesStates
no
States
arcs
makePopulationProtocolWithTrans
name
states
initialStates
trueStates
false
States
ts
=
makePopulationProtocol
name
states
(
map
fst
ts
)
initialStates
trueStates
false
States
arcs
where
arcs
=
[
Right
(
q
,
t
,
w
)
|
(
t
,(
is
,
_
))
<-
ts
,
(
q
,
w
)
<-
is
]
++
[
Left
(
t
,
q
,
w
)
|
(
t
,(
_
,
os
))
<-
ts
,
(
q
,
w
)
<-
os
]
...
...
@@ -203,13 +203,13 @@ makePopulationProtocolWithTrans name states initialStates yesStates noStates ts
makePopulationProtocolWithTransFromStrings
::
String
->
[
String
]
->
[
String
]
->
[
String
]
->
[
String
]
->
[(
String
,
([(
String
,
Integer
)],
[(
String
,
Integer
)]))]
->
PopulationProtocol
makePopulationProtocolWithTransFromStrings
name
states
initialStates
yesStates
no
States
arcs
=
makePopulationProtocolWithTransFromStrings
name
states
initialStates
trueStates
false
States
arcs
=
makePopulationProtocolWithTrans
name
(
map
State
states
)
(
map
State
initialStates
)
(
map
State
yes
States
)
(
map
State
no
States
)
(
map
State
true
States
)
(
map
State
false
States
)
(
map
toTArc
arcs
)
where
toTArc
(
t
,
(
iq
,
oq
))
=
...
...
src/Solver/StrongConsensus.hs
View file @
430f9c2e
...
...
@@ -49,7 +49,7 @@ initialConfiguration pp m0 =
differentConsensusConstraints
::
PopulationProtocol
->
SIMap
State
->
SIMap
State
->
SBool
differentConsensusConstraints
pp
m1
m2
=
(
sum
(
mval
m1
(
yesStates
pp
))
.>
0
&&&
sum
(
mval
m2
(
no
States
pp
))
.>
0
)
(
sum
(
mval
m1
(
trueStates
pp
))
.>
0
&&&
sum
(
mval
m2
(
false
States
pp
))
.>
0
)
unmarkedByConfiguration
::
[
State
]
->
SIMap
State
->
SBool
unmarkedByConfiguration
r
m
=
sum
(
mval
m
r
)
.==
0
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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