diff --git a/examples/broadcast.pp b/examples/broadcast.pp index 79d61a2a83899f20b94f5bb241b1c0f1126c1939..1370c73737d8c37e2e4e6d8b21486f9caeca114e 100644 --- a/examples/broadcast.pp +++ b/examples/broadcast.pp @@ -1,10 +1,10 @@ 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 } } diff --git a/examples/majority.pp b/examples/majority.pp index dc90c0f5f1e22a3c6587ff53fcf51321666c3c89..0e82267570201444422f0437c9dfdb43a54c25ec 100644 --- a/examples/majority.pp +++ b/examples/majority.pp @@ -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 } } diff --git a/examples/threshold_l3_c1.pnet b/examples/threshold_l3_c1.pnet new file mode 100644 index 0000000000000000000000000000000000000000..ce57c83bb546419d6bf5f78615d15ff4912d2734 --- /dev/null +++ b/examples/threshold_l3_c1.pnet @@ -0,0 +1,297 @@ +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} +} diff --git a/src/Main.hs b/src/Main.hs index eb4836f9786e23b1f0dbf7786beeed0452582f38..9e591f9f0934f2509e843a06755b3d55accd327c 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -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 (yesStates pp)) - verbosePut 0 $ "No states : " ++ show (length (noStates pp)) + verbosePut 0 $ "Yes states : " ++ show (length (trueStates pp)) + verbosePut 0 $ "No states : " ++ show (length (falseStates pp)) checkFile :: String -> OptIO PropResult checkFile file = do diff --git a/src/Parser/PP.hs b/src/Parser/PP.hs index 3587d87bff75bc96e6218396bdbbc7fdefaeba0f..c720cfb90c0caed27a3a17a8768fbb6a7565e741 100644 --- a/src/Parser/PP.hs +++ b/src/Parser/PP.hs @@ -77,11 +77,11 @@ transitions = reserved "transitions" *> identList initial :: Parser [String] initial = reserved "initial" *> identList -yesStates :: Parser [String] -yesStates = reserved "yes" *> identList +trueStates :: Parser [String] +trueStates = reserved "true" *> identList -noStates :: Parser [String] -noStates = reserved "no" *> identList +falseStates :: 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] - | YesStatement [String] - | NoStatement [String] + | TrueStatement [String] + | FalseStatement [String] | Arcs [(String,String,Integer)] statement :: Parser Statement @@ -114,8 +114,8 @@ statement = States <$> states <|> Transitions <$> transitions <|> Arcs <$> arcs <|> Initial <$> initial <|> - YesStatement <$> yesStates <|> - NoStatement <$> noStates + TrueStatement <$> trueStates <|> + FalseStatement <$> falseStates 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 ) diff --git a/src/PopulationProtocol.hs b/src/PopulationProtocol.hs index dd6363b713a119d39fdc5228c5457e57689bada8..1f53006c9c02f629bc4e1d156254d8de124227d3 100644 --- a/src/PopulationProtocol.hs +++ b/src/PopulationProtocol.hs @@ -5,7 +5,7 @@ module PopulationProtocol (PopulationProtocol,State(..),Transition(..), Configuration,FlowVector,RConfiguration,RFlowVector, renameState,renameTransition,renameStatesAndTransitions, - name,showNetName,states,transitions,initialStates,yesStates,noStates, + name,showNetName,states,transitions,initialStates,trueStates,falseStates, pre,lpre,post,lpost,mpre,mpost,context, makePopulationProtocol,makePopulationProtocolWithTrans, makePopulationProtocolFromStrings,makePopulationProtocolWithTransFromStrings, @@ -72,8 +72,8 @@ data PopulationProtocol = PopulationProtocol { states :: [State], transitions :: [Transition], initialStates :: [State], - yesStates :: [State], - noStates :: [State], + trueStates :: [State], + falseStates :: [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 ++ - "\nStates: " ++ show (states pp) ++ - "\nTransitions: " ++ show (transitions pp) ++ - "\nInitial states: " ++ show (initialStates pp) ++ - "\nYes states: " ++ show (yesStates pp) ++ - "\nNo states: " ++ show (noStates pp) ++ - "\nState arcs:\n" ++ unlines + "\nStates : " ++ show (states pp) ++ + "\nTransitions : " ++ show (transitions pp) ++ + "\nInitial states : " ++ show (initialStates pp) ++ + "\nTrue states : " ++ show (trueStates pp) ++ + "\nFalse states : " ++ show (falseStates pp) ++ + "\nState arcs :\n" ++ unlines (map showContext (M.toList (adjacencyQ pp))) ++ "\nTransition 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, - yesStates = - listSet $ map (renameState f) $ yesStates pp, - noStates = - listSet $ map (renameState f) $ noStates pp, + trueStates = + listSet $ map (renameState f) $ trueStates pp, + falseStates = + listSet $ map (renameState f) $ falseStates 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 noStates arcs = +makePopulationProtocol name states transitions initialStates trueStates falseStates arcs = PopulationProtocol { name = name, states = listSet states, transitions = listSet transitions, initialStates = listSet initialStates, - yesStates = listSet yesStates, - noStates = listSet noStates, + trueStates = listSet trueStates, + falseStates = listSet falseStates, 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 noStates arcs = +makePopulationProtocolFromStrings name states transitions initialStates trueStates falseStates arcs = makePopulationProtocol name (map State (S.toAscList stateSet)) (map Transition (S.toAscList transitionSet)) (map State initialStates) - (map State yesStates) - (map State noStates) + (map State trueStates) + (map State falseStates) (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 noStates ts = - makePopulationProtocol name states (map fst ts) initialStates yesStates noStates arcs +makePopulationProtocolWithTrans name states initialStates trueStates falseStates ts = + makePopulationProtocol name states (map fst ts) initialStates trueStates falseStates 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 noStates arcs = +makePopulationProtocolWithTransFromStrings name states initialStates trueStates falseStates arcs = makePopulationProtocolWithTrans name (map State states) (map State initialStates) - (map State yesStates) - (map State noStates) + (map State trueStates) + (map State falseStates) (map toTArc arcs) where toTArc (t, (iq, oq)) = diff --git a/src/Solver/StrongConsensus.hs b/src/Solver/StrongConsensus.hs index fd8db4560fb318d10bff70fbb3af3866263292db..49ff89e4116e50d7702c823ecc84631c85198991 100644 --- a/src/Solver/StrongConsensus.hs +++ b/src/Solver/StrongConsensus.hs @@ -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 (noStates pp)) .> 0) + (sum (mval m1 (trueStates pp)) .> 0 &&& sum (mval m2 (falseStates pp)) .> 0) unmarkedByConfiguration :: [State] -> SIMap State -> SBool unmarkedByConfiguration r m = sum (mval m r) .== 0