diff --git a/spot/twaalgos/cleanacc.cc b/spot/twaalgos/cleanacc.cc index 685507112..87a42917c 100644 --- a/spot/twaalgos/cleanacc.cc +++ b/spot/twaalgos/cleanacc.cc @@ -617,20 +617,20 @@ namespace spot twa_graph_ptr simplify_acceptance_here(twa_graph_ptr aut) { - cleanup_acceptance_here(aut, false); - merge_identical_marks_here(aut); - if (!aut->acc().is_generalized_buchi()) + for (;;) { + cleanup_acceptance_here(aut, false); + merge_identical_marks_here(aut); + if (aut->acc().is_generalized_buchi()) + break; + acc_cond::acc_code old = aut->get_acceptance(); simplify_complementary_marks_here(aut); fuse_marks_here(aut); + aut->set_acceptance(aut->acc().unit_propagation()); + if (old == aut->get_acceptance()) + break; } cleanup_acceptance_here(aut, true); - auto prop_cond = aut->acc().unit_propagation(); - if (prop_cond != aut->acc()) - { - aut->set_acceptance(prop_cond); - cleanup_acceptance_here(aut, true); - } return aut; } diff --git a/tests/core/accsimpl.test b/tests/core/accsimpl.test index 17404023f..1dbf06095 100755 --- a/tests/core/accsimpl.test +++ b/tests/core/accsimpl.test @@ -72,4 +72,4 @@ State: 0 --END-- EOF autcross --language-preserved 'autfilt --simplify-acc' -F frenkin -test 1,4,2 = "`autfilt --simplify-acc frenkin --stats=%s,%e,%a`" +test 1,4,1 = "`autfilt --simplify-acc frenkin --stats=%s,%e,%a`" diff --git a/tests/core/remfin.test b/tests/core/remfin.test index 0b387d8e0..c8b1eb670 100755 --- a/tests/core/remfin.test +++ b/tests/core/remfin.test @@ -313,27 +313,25 @@ State: 2 {0} [!1] 2 --END-- HOA: v1 -States: 4 +States: 3 Start: 0 AP: 2 "a" "b" -Acceptance: 4 Inf(0) | Inf(3) | (Inf(1)&Inf(2)) +acc-name: Buchi +Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 -[t] 0 {2 3} -[0] 1 {2 3} -[!0] 2 {2 3} +[t] 0 {0} +[0] 1 {0} +[!0] 2 {0} State: 1 -[1] 0 {2} -[0&1] 1 {2} -[!0&1] 2 {1 2} +[1] 0 {0} +[0&1] 1 {0} +[!0&1] 2 {0} State: 2 [!1] 0 -[0&!1] 1 -[!0&!1] 2 -[!0&!1] 3 -State: 3 -[!0&!1] 3 {0} +[0&!1] 1 {0} +[!0&!1] 2 {0} --END-- HOA: v1 States: 3 @@ -915,7 +913,7 @@ State: 2 {0} [!1] 2 --END-- HOA: v1 -States: 4 +States: 3 Start: 0 AP: 2 "a" "b" acc-name: Buchi @@ -927,16 +925,13 @@ State: 0 [0] 1 {0} [!0] 2 {0} State: 1 -[1] 0 -[0&1] 1 +[1] 0 {0} +[0&1] 1 {0} [!0&1] 2 {0} State: 2 [!1] 0 -[0&!1] 1 -[!0&!1] 2 -[!0&!1] 3 -State: 3 -[!0&!1] 3 {0} +[0&!1] 1 {0} +[!0&!1] 2 {0} --END-- HOA: v1 States: 3 diff --git a/tests/python/automata.ipynb b/tests/python/automata.ipynb index 07eda5fcb..09ecfe0be 100644 --- a/tests/python/automata.ipynb +++ b/tests/python/automata.ipynb @@ -30,155 +30,155 @@ "\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b & c & d\n", + "\n", + "\n", + "b & c & d\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "b & !d\n", + "\n", + "\n", + "b & !d\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "b & !c & d\n", + "\n", + "\n", + "b & !c & d\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "\n", + "c & d\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "!d\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "!c & d\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "\n", + "c & d\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "!d\n", "\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "!c & d\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", "\n", "3->1\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "!c\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f83440499f0> >" + " *' at 0x7fc938228a20> >" ] }, "execution_count": 2, @@ -208,149 +208,149 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b & c & d\n", + "\n", + "\n", + "b & c & d\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "b & !d\n", + "\n", + "\n", + "b & !d\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "b & !c & d\n", + "\n", + "\n", + "b & !c & d\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "\n", + "c & d\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "!d\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "!c & d\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "\n", + "c & d\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "!d\n", "\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "!c & d\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", "\n", "3->1\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "!c\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" @@ -386,166 +386,166 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "cluster_0\n", - "\n", + "\n", "\n", "\n", "cluster_1\n", - "\n", + "\n", "\n", "\n", "cluster_2\n", - "\n", + "\n", "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b & c & d\n", + "\n", + "\n", + "b & c & d\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "b & !d\n", + "\n", + "\n", + "b & !d\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "b & !c & d\n", + "\n", + "\n", + "b & !c & d\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "c & d\n", - "\n", + "\n", + "\n", + "c & d\n", + "\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!d\n", - "\n", + "\n", + "\n", + "!d\n", + "\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "!c & d\n", - "\n", + "\n", + "\n", + "!c & d\n", + "\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "\n", + "c & d\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "!d\n", "\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "!c & d\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", "\n", "3->1\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "!c\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" @@ -604,60 +604,60 @@ "\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "I->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "0\n", - "\n", - "\n", - "0\n", + "\n", + "\n", + "0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f83440567b0> >" + " *' at 0x7fc938233060> >" ] }, "execution_count": 6, @@ -680,60 +680,60 @@ "\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "I->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "0\n", - "\n", - "\n", - "0\n", + "\n", + "\n", + "0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f8344056b10> >" + " *' at 0x7fc938233960> >" ] }, "execution_count": 7, @@ -763,60 +763,60 @@ "\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "I->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f8344049d20> >" + " *' at 0x7fc938238660> >" ] }, "execution_count": 8, @@ -869,89 +869,89 @@ "\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "3\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", "\n" @@ -980,202 +980,202 @@ "\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", "6\n", - "\n", - "\n", - "6\n", + "\n", + "\n", + "6\n", "\n", "\n", "\n", "I->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "6->6\n", - "\n", - "\n", - "a & b & c\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", "\n", "0\n", - "\n", - "\n", - "0\n", + "\n", + "\n", + "0\n", "\n", "\n", "\n", "6->0\n", - "\n", - "\n", - "!a & !b & c\n", + "\n", + "\n", + "!a & !b & c\n", "\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "6->1\n", - "\n", - "\n", - "a & !b & !c\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", "\n", "2\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "2\n", "\n", "\n", "\n", "6->2\n", - "\n", - "\n", - "!a & b & !c\n", + "\n", + "\n", + "!a & b & !c\n", "\n", "\n", "\n", "3\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "3\n", "\n", "\n", "\n", "6->3\n", - "\n", - "\n", - "!a & b & c\n", + "\n", + "\n", + "!a & b & c\n", "\n", "\n", "\n", "4\n", - "\n", - "\n", - "4\n", + "\n", + "\n", + "4\n", "\n", "\n", "\n", "6->4\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", "\n", "5\n", - "\n", - "\n", - "5\n", + "\n", + "\n", + "5\n", "\n", "\n", "\n", "6->5\n", - "\n", - "\n", - "a & b & !c\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "3->0\n", - "\n", - "\n", - "!b & c\n", + "\n", + "\n", + "!b & c\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", - "b & !c\n", + "\n", + "\n", + "b & !c\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "b & c\n", + "\n", + "\n", + "b & c\n", "\n", "\n", "\n", "4->0\n", - "\n", - "\n", - "!a & c\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", "\n", "4->1\n", - "\n", - "\n", - "a & !c\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "a & c\n", + "\n", + "\n", + "a & c\n", "\n", "\n", "\n", "5->1\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "5->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n", "5->5\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n" @@ -1211,145 +1211,145 @@ "\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "a | b\n", + "\n", + "\n", + "a | b\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "b\n", + "\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "a | b\n", + "\n", + "\n", + "a | b\n", "\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "2->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", - "a | b\n", + "\n", + "\n", + "a | b\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "!a & !b\n", - "\n", + "\n", + "\n", + "!a & !b\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f8344056f90> >" + " *' at 0x7fc9382462d0> >" ] }, "execution_count": 12, @@ -1379,91 +1379,91 @@ "\n", "\n", - "\n", "\n", "\n", "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f83440651e0> >" + " *' at 0x7fc938246c60> >" ] }, "execution_count": 13, @@ -1493,108 +1493,108 @@ "\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "2\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "3->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f83440652d0> >" + " *' at 0x7fc93824d4b0> >" ] }, "execution_count": 14, @@ -1661,20 +1661,20 @@ "Start: 0\n", "AP: 2 \"a\" \"b\"\n", "acc-name: Buchi\n", - "Acceptance: 4 Inf(0)&Fin(1)&Fin(3) | Inf(2)&Inf(3) | Inf(1)\n", + "Acceptance: 5 Inf(0)&Fin(1)&Fin(4) | Inf(2)&Inf(3) | Inf(1)\n", "--BODY--\n", "State: 0 {3}\n", "[t] 0\n", "[0] 1 {1}\n", - "[!0] 2 {0}\n", + "[!0] 2 {0 4}\n", "State: 1 {3}\n", "[1] 0\n", "[0&1] 1 {0}\n", - "[!0&1] 2 {2}\n", - "State: 2\n", + "[!0&1] 2 {2 4}\n", + "State: 2 \n", "[!1] 0\n", "[0&!1] 1 {0}\n", - "[!0&!1] 2 {0}\n", + "[!0&!1] 2 {0 4}\n", "--END--" ] }, @@ -1689,131 +1689,134 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "(Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ") & Fin(\n", - "\n", - ")) | (Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")) | Inf(\n", - "\n", - ")\n", + "\n", + "\n", + "\n", + "(Inf(\n", + "\n", + ") & Fin(\n", + "\n", + ") & Fin(\n", + "\n", + ")) | (Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")) | Inf(\n", + "\n", + ")\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", - "\n", - "\n", + "\n", + "\n", + "a\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "b\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "2->0\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a & !b\n", - "\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f8344056ab0> >" + " *' at 0x7fc93824d060> >" ] }, "metadata": {}, @@ -1825,125 +1828,372 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Inf(\n", - "\n", - ") | Inf(\n", - "\n", - ")\n", - "[Fin-less 3]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") | Inf(\n", + "\n", + ") | (Inf(\n", + "\n", + ")&Inf(\n", + "\n", + "))\n", + "[Fin-less 4]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", - "\n", - "\n", + "\n", + "\n", + "a\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fc938253e40> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a & b\n", - "\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "!b\n", "\n", "\n", - "\n", + "\n", "2->0\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", - "\n", + "\n", "2->1\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", - "\n", + "\n", "2->2\n", - "\n", - "\n", - "!a & !b\n", - "\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "!a | !b\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f83440566c0> >" + " *' at 0x7fc93824dbd0> >" ] }, "metadata": {}, @@ -1955,88 +2205,143 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f8344056060> >" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "image/svg+xml": [ - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n" - ], - "text/plain": [ - " *' at 0x7f8344056cc0> >" + " *' at 0x7fc938253510> >" ] }, "metadata": {}, @@ -2071,158 +2376,161 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "(Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ") & Fin(\n", - "\n", - ")) | (Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")) | Inf(\n", - "\n", - ")\n", + "\n", + "\n", + "\n", + "(Inf(\n", + "\n", + ") & Fin(\n", + "\n", + ") & Fin(\n", + "\n", + ")) | (Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")) | Inf(\n", + "\n", + ")\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", - "\n", - "\n", + "\n", + "\n", + "a\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "b\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "2->0\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a & !b\n", - "\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", "\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f83440659c0> >" + " *' at 0x7fc93825d930> >" ] }, "execution_count": 19, @@ -2245,60 +2553,60 @@ "\n", "\n", - "\n", "\n", "\n", "\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "\n", - "0\n", + "\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f83440654b0> >" + " *' at 0x7fc93825dab0> >" ] }, "execution_count": 20, @@ -2348,129 +2656,129 @@ "
\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + " viewBox=\"0.00 0.00 165.00 130.42\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "!c\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "c\n", - "\n", + "\n", + "\n", + "c\n", + "\n", "\n", "\n", "\n", @@ -2489,269 +2797,269 @@ "
\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 2]\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 2]\n", "\n", "\n", "\n", "0\n", - "\n", - "0,0\n", + "\n", + "0,0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "\n", "1\n", - "\n", - "0,1\n", + "\n", + "0,1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a & b\n", - "\n", + "\n", + "\n", + "a & b\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "1,1\n", + "\n", + "1,1\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & !c\n", - "\n", + "\n", + "\n", + "a & !c\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & c\n", - "\n", - "\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a & !c\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a & c\n", - "\n", + "\n", + "\n", + "!a & c\n", + "\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "a & !c\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "a & c\n", - "\n", + "\n", + "\n", + "a & c\n", + "\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a & !c\n", - "\n", + "\n", + "\n", + "!a & !c\n", + "\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a & c\n", - "\n", - "\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 2]\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 2]\n", "\n", "\n", "\n", "0\n", "\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "\n", "1\n", "\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a & b\n", - "\n", + "\n", + "\n", + "a & b\n", + "\n", "\n", "\n", "\n", "2\n", "\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & !c\n", - "\n", + "\n", + "\n", + "a & !c\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & c\n", - "\n", - "\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a & !c\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a & c\n", - "\n", + "\n", + "\n", + "!a & c\n", + "\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "a & !c\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "a & c\n", - "\n", + "\n", + "\n", + "a & c\n", + "\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a & !c\n", - "\n", + "\n", + "\n", + "!a & !c\n", + "\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a & c\n", - "\n", - "\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", "\n", "\n", "\n", @@ -2795,60 +3103,60 @@ "\n", "\n", - "\n", "\n", "\n", "\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f8344049990> >" + " *' at 0x7fc93825d6c0> >" ] }, "metadata": {}, @@ -2881,74 +3189,74 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f8344101660> >" + " *' at 0x7fc9381e31b0> >" ] }, "execution_count": 24, @@ -2978,50 +3286,50 @@ "\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Fin(\n", - "\n", - ")\n", - "[co-Büchi]\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f83441014e0> >" + " *' at 0x7fc9381e9bd0> >" ] }, "execution_count": 25, @@ -3051,64 +3359,64 @@ "\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "Fin(\n", - "\n", - ")\n", - "[co-Büchi]\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", - "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "I->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n" @@ -3144,55 +3452,55 @@ "\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Fin(\n", - "\n", - ") & (Inf(\n", - "\n", - ") | Fin(\n", - "\n", - "))\n", - "[parity max odd 3]\n", + "\n", + "Fin(\n", + "\n", + ") & (Inf(\n", + "\n", + ") | Fin(\n", + "\n", + "))\n", + "[parity max odd 3]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f8344056cf0> >" + " *' at 0x7fc9381ee750> >" ] }, "execution_count": 27, @@ -3222,60 +3530,60 @@ "\n", "\n", - "\n", "\n", "\n", "\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f8344049990> >" + " *' at 0x7fc93825d6c0> >" ] }, "metadata": {}, @@ -3287,60 +3595,60 @@ "\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f8344049990> >" + " *' at 0x7fc93825d6c0> >" ] }, "metadata": {}, @@ -3374,60 +3682,60 @@ "\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a & b & c\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f8344049990> >" + " *' at 0x7fc93825d6c0> >" ] }, "execution_count": 29, @@ -3460,7 +3768,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.7.3" + "version": "3.8.2" } }, "nbformat": 4, diff --git a/tests/python/merge.py b/tests/python/merge.py index a33a2774f..7fa888859 100644 --- a/tests/python/merge.py +++ b/tests/python/merge.py @@ -1,6 +1,6 @@ #!/usr/bin/python3 # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017 Laboratoire de Recherche et Développement de +# Copyright (C) 2017, 2020 Laboratoire de Recherche et Développement de # l'EPITA. # # This file is part of Spot, a model checking library. @@ -78,8 +78,7 @@ assert hoa == """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" -acc-name: parity min even 2 -Acceptance: 2 Inf(0) | Fin(1) +Acceptance: 2 Fin(1) | Inf(0) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 diff --git a/tests/python/simplacc.py b/tests/python/simplacc.py index af8cb9298..024bccd56 100644 --- a/tests/python/simplacc.py +++ b/tests/python/simplacc.py @@ -57,23 +57,28 @@ for a in auts: b = spot.simplify_acceptance(a) assert b.equivalent_to(a) res.append(str(b.get_acceptance())) + c = spot.simplify_acceptance(b) + assert b.get_acceptance() == c.get_acceptance() a.set_acceptance(a.num_sets(), a.get_acceptance().complement()) b = spot.simplify_acceptance(a) assert b.equivalent_to(a) res.append(str(b.get_acceptance())) + c = spot.simplify_acceptance(b) + assert b.get_acceptance() == c.get_acceptance() + assert res == [ 'Inf(0)', 'Fin(0)', - 'Inf(1) & Fin(0)', + 'Fin(0) & Inf(1)', 'Fin(1) | Inf(0)', - 'Inf(1) & (Fin(0) | Inf(2))', + '(Fin(0) | Inf(2)) & Inf(1)', 'Fin(1) | (Fin(2) & Inf(0))', '(Fin(1) | Inf(2)) & Inf(0)', 'Fin(0) | (Fin(2) & Inf(1))', '((Fin(1) | Inf(2)) & Inf(5)) | (Fin(0) & (Fin(1) | (Fin(3) & Inf(4))))', '(Fin(5) | (Fin(2) & Inf(1))) & (Inf(0) | ((Fin(4) | Inf(3)) & Inf(1)))', - 'Inf(1) | Inf(0)', - 'Fin(1) & Fin(0)', + 'Inf(0)', + 'Fin(0)', ] diff --git a/tests/python/toparity.py b/tests/python/toparity.py index 8301789b3..9ebaabc14 100644 --- a/tests/python/toparity.py +++ b/tests/python/toparity.py @@ -288,7 +288,7 @@ State: 4 [0&!1] 4 [0&1] 4 {1 2 4} --END-- -"""), [9, 6, 7, 7, 6, 6, 6]) +"""), [9, 6, 6, 6, 7, 6, 6]) test(spot.automaton(""" HOA: v1