diff --git a/spot/twaalgos/toparity.cc b/spot/twaalgos/toparity.cc index 056daaf40..32f5c7570 100644 --- a/spot/twaalgos/toparity.cc +++ b/spot/twaalgos/toparity.cc @@ -1684,7 +1684,7 @@ run() res_->set_named_prop("state-names", names); reduce_parity_here(res_); res_->purge_unreachable_states(); - res_->merge_states(); + // res_->merge_states(); return res_; } diff --git a/tests/python/automata.ipynb b/tests/python/automata.ipynb index 61971c52e..07eda5fcb 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 0x7fa0443228a0> >" + " *' at 0x7f83440499f0> >" ] }, "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 0x7fa044322570> >" + " *' at 0x7f83440567b0> >" ] }, "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 0x7fa0443309c0> >" + " *' at 0x7f8344056b10> >" ] }, "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 0x7fa044330ab0> >" + " *' at 0x7f8344049d20> >" ] }, "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 0x7fa044336bd0> >" + " *' at 0x7f8344056f90> >" ] }, "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 0x7fa0443364e0> >" + " *' at 0x7f83440651e0> >" ] }, "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 0x7fa044336e70> >" + " *' at 0x7f83440652d0> >" ] }, "execution_count": 14, @@ -1689,131 +1689,131 @@ "\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", "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", "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" ], "text/plain": [ - " *' at 0x7fa0442cea20> >" + " *' at 0x7f8344056ab0> >" ] }, "metadata": {}, @@ -1825,125 +1825,125 @@ "\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", + ")\n", + "[Fin-less 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", - "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", "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", + "!a & b\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" ], "text/plain": [ - " *' at 0x7fa0442ce9c0> >" + " *' at 0x7f83440566c0> >" ] }, "metadata": {}, @@ -1955,135 +1955,43 @@ "\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", "\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", - "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", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "!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", - "\n", - "2->2\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "\n", - "2->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fa0442ce1e0> >" + " *' at 0x7f8344056060> >" ] }, "metadata": {}, @@ -2095,102 +2003,40 @@ "\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", + "\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", - "1\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "2\n", - "\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", - "1->1\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", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fa0442ceb70> >" + " *' at 0x7f8344056cc0> >" ] }, "metadata": {}, @@ -2225,158 +2071,158 @@ "\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", "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", "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", "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 0x7fa0442c6360> >" + " *' at 0x7f83440659c0> >" ] }, "execution_count": 19, @@ -2399,60 +2245,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 0x7fa0442c69c0> >" + " *' at 0x7f83440654b0> >" ] }, "execution_count": 20, @@ -2502,129 +2348,129 @@ "
\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + " viewBox=\"0.00 0.00 165.00 130.40\" 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", @@ -2643,269 +2489,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", @@ -2949,60 +2795,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 0x7fa0442e1e40> >" + " *' at 0x7f8344049990> >" ] }, "metadata": {}, @@ -3035,74 +2881,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 0x7fa0442c64e0> >" + " *' at 0x7f8344101660> >" ] }, "execution_count": 24, @@ -3132,50 +2978,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 0x7fa0442e9960> >" + " *' at 0x7f83441014e0> >" ] }, "execution_count": 25, @@ -3205,64 +3051,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" @@ -3298,55 +3144,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 0x7fa0442f2540> >" + " *' at 0x7f8344056cf0> >" ] }, "execution_count": 27, @@ -3376,60 +3222,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 0x7fa0442e1e40> >" + " *' at 0x7f8344049990> >" ] }, "metadata": {}, @@ -3441,60 +3287,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 0x7fa0442e1e40> >" + " *' at 0x7f8344049990> >" ] }, "metadata": {}, @@ -3528,60 +3374,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 0x7fa0442e1e40> >" + " *' at 0x7f8344049990> >" ] }, "execution_count": 29, @@ -3614,7 +3460,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.8.2" + "version": "3.7.3" } }, "nbformat": 4, diff --git a/tests/python/toparity.py b/tests/python/toparity.py index 237dacb05..91732922e 100644 --- a/tests/python/toparity.py +++ b/tests/python/toparity.py @@ -195,7 +195,7 @@ State: 13 [0&1] 5 [!0&!1] 10 {0 1 3 5} [0&!1] 13 {1 3} ---END--"""), [31, 27, 23, 28, 28, 24, 22]) +--END--"""), [35, 30, 23, 30, 34, 27, 22]) test(spot.automaton(""" HOA: v1 @@ -213,7 +213,7 @@ State: 1 [0&!1] 1 {4} [!0&1] 1 {0 1 2 3} [!0&!1] 1 {0 3} ---END--"""), [7, 5, 3, 6, 5, 5, 3]) +--END--"""), [7, 7, 3, 6, 10, 5, 3]) for i,f in enumerate(spot.randltl(10, 400)): @@ -288,7 +288,7 @@ State: 4 [0&!1] 4 [0&1] 4 {1 2 4} --END-- -"""), [8, 6, 7, 7, 6, 6, 6]) +"""), [9, 9, 8, 7, 9, 9, 6]) test(spot.automaton(""" HOA: v1 @@ -310,7 +310,7 @@ State: 1 [0&!1] 1 {2 3} [0&1] 1 {1 2 4} --END-- -"""), [11, 6, 3, 7, 7, 4, 3]) +"""), [11, 6, 4, 7, 11, 6, 3]) # Tests both the old and new version of to_parity @@ -341,7 +341,7 @@ explicit-labels trans-acc --BODY-- State: 0 [0&1] 2 {4 5} [0&1] 4 {0 4} p = spot.to_parity_old(a, True) assert p.num_states() == 22 assert spot.are_equivalent(a, p) -test(a, [6, 6, 6, 6, 6, 6, 6]) +test(a, [8, 7, 8, 8, 8, 7, 6]) # Force a few edges to false, to make sure to_parity() is OK with that. for e in a.out(2): @@ -355,7 +355,7 @@ for e in a.out(3): p = spot.to_parity_old(a, True) assert p.num_states() == 22 assert spot.are_equivalent(a, p) -test(a, [7, 6, 7, 7, 6, 6, 6]) +test(a, [7, 6, 7, 7, 7, 6, 6]) for f in spot.randltl(4, 400): d = spot.translate(f, "det", "G") @@ -371,4 +371,4 @@ for f in spot.randltl(5, 2000): a = spot.translate('!(GFa -> (GFb & GF(!b & !Xb)))', 'gen', 'det') b = spot.to_parity_old(a, True) assert a.equivalent_to(b) -test(a, [6, 6, 3, 6, 7, 6, 3]) +test(a, [7, 7, 3, 7, 8, 7, 3])