diff --git a/wrap/python/spot.py b/wrap/python/spot.py index 1392a0285..24b5b8b1e 100644 --- a/wrap/python/spot.py +++ b/wrap/python/spot.py @@ -198,7 +198,7 @@ def translate(formula, output='tgba', pref='small', level='high', if type(formula) == str: formula = parse_formula(formula) - a = translator() + a = translator(_bdd_dict) if type(output) == str: output_ = output.lower() diff --git a/wrap/python/tests/automata.ipynb b/wrap/python/tests/automata.ipynb index 07dc0bf1a..36c30646e 100644 --- a/wrap/python/tests/automata.ipynb +++ b/wrap/python/tests/automata.ipynb @@ -18,7 +18,7 @@ "version": "3.4.2" }, "name": "", - "signature": "sha256:8277d563756e7b9333f4900705ae07524e2902b49f4c79ceb40739a865a177c4" + "signature": "sha256:7bcd29a20e60c508a998923ed5875f91f69cd4f3e77dca19795b976dab016b90" }, "nbformat": 3, "nbformat_minor": 0, @@ -60,123 +60,123 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "1\n", - "\n", - "1\n", - "\u24ff\n", + "\n", + "1\n", + "\u24ff\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "\n", + "c & d\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!c & d\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "!d\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "!c\n", "\n", "\n", "3->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "\n", + "c & d\n", "\n", "\n", "3->2\n", - "\n", - "\n", - "!c & d\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "!d\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f87301e0180> >" + " *' at 0x1052702d0> >" ] } ], @@ -196,119 +196,119 @@ "output_type": "pyout", "prompt_number": 3, "svg": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "\n", + "c & d\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!c & d\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "!d\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "!c\n", "\n", "\n", "3->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "\n", + "c & d\n", "\n", "\n", "3->2\n", - "\n", - "\n", - "!c & d\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "!d\n", "\n", "\n", "" ], "text": [ - "" + "" ] } ], @@ -328,133 +328,133 @@ "output_type": "pyout", "prompt_number": 4, "svg": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", "cluster_0\n", - "\n", + "\n", "\n", "cluster_1\n", - "\n", + "\n", "\n", "cluster_2\n", - "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "c & d\n", - "\u24ff\n", + "\n", + "\n", + "c & d\n", + "\u24ff\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "!d\n", - "\u24ff\n", + "\n", + "\n", + "!d\n", + "\u24ff\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!c & d\n", - "\u24ff\n", + "\n", + "\n", + "!c & d\n", + "\u24ff\n", "\n", "\n", "3->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "\n", + "c & d\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "!d\n", "\n", "\n", "3->2\n", - "\n", - "\n", - "!c & d\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "!c\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "" ], "text": [ - "" + "" ] } ], @@ -500,54 +500,54 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "I->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "0\n", - "\n", - "0\n", - "\u24ff\n", + "\n", + "0\n", + "\u24ff\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f87301b6990> >" + " *' at 0x106ca0060> >" ] } ], @@ -570,54 +570,54 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "I->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "0\n", - "\n", - "0\n", - "\u24ff\n", + "\n", + "0\n", + "\u24ff\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f87301b6bd0> >" + " *' at 0x106ca0120> >" ] } ], @@ -640,53 +640,53 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "I->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f87301b6a20> >" + " *' at 0x106ca0030> >" ] } ], @@ -729,80 +729,80 @@ "output_type": "pyout", "prompt_number": 10, "svg": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "1\n", "\n", "\n", - "1\n", + "1\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "a\n", "\n", "\n", "2\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "2\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "b\n", "\n", "\n", "3\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "3\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "c\n", "\n", "\n", "1->1\n", "\n", "\n", - "c\n", + "a\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "b\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "c\n", "\n", "\n", "" ], "text": [ - "" + "" ] } ], @@ -822,177 +822,177 @@ "output_type": "pyout", "prompt_number": 11, "svg": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "6\n", - "\n", - "6\n", - "\u24ff\n", + "\n", + "6\n", + "\u24ff\n", "\n", "\n", "I->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "6->6\n", - "\n", - "\n", - "a & b & c\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", "0\n", - "\n", - "0\n", - "\u24ff\n", + "\n", + "0\n", + "\u24ff\n", "\n", "\n", "6->0\n", - "\n", - "\n", - "!a & !b & c\n", + "\n", + "\n", + "!a & !b & c\n", "\n", "\n", "1\n", - "\n", - "1\n", - "\u24ff\n", + "\n", + "1\n", + "\u24ff\n", "\n", "\n", "6->1\n", - "\n", - "\n", - "!a & b & !c\n", + "\n", + "\n", + "!a & b & c\n", "\n", "\n", "2\n", - "\n", - "2\n", - "\u24ff\n", + "\n", + "2\n", + "\u24ff\n", "\n", "\n", "6->2\n", - "\n", - "\n", - "a & !b & !c\n", + "\n", + "\n", + "!a & b & !c\n", "\n", "\n", "3\n", - "\n", - "3\n", - "\u24ff\n", + "\n", + "3\n", + "\u24ff\n", "\n", "\n", "6->3\n", - "\n", - "\n", - "!a & b & c\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\u24ff\n", - "\n", - "\n", - "6->4\n", - "\n", - "\n", - "a & b & !c\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", - "5\n", - "\n", - "5\n", - "\u24ff\n", + "5\n", + "\n", + "5\n", + "\u24ff\n", "\n", "\n", "6->5\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\u24ff\n", + "\n", + "\n", + "6->4\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!b & c\n", "\n", "\n", - "1->1\n", - "\n", - "\n", - "b\n", + "1->1\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "b & !c\n", "\n", "\n", - "2->2\n", - "\n", - "\n", - "a\n", + "2->2\n", + "\n", + "\n", + "b\n", "\n", - "\n", - "3->0\n", - "\n", - "\n", - "!b & c\n", - "\n", - "\n", - "3->1\n", - "\n", - "\n", - "b & !c\n", + "\n", + "3->2\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", - "3->3\n", - "\n", - "\n", - "b & c\n", + "3->3\n", + "\n", + "\n", + "a & b\n", "\n", - "\n", - "4->1\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "4->2\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "5->0\n", - "\n", - "\n", - "!a & c\n", - "\n", - "\n", - "5->2\n", - "\n", - "\n", - "a & !c\n", + "\n", + "3->5\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "5->5\n", - "\n", - "\n", - "a & c\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "4->0\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "4->5\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a & c\n", "\n", "\n", "" ], "text": [ - "" + "" ] } ], @@ -1015,77 +1015,77 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "b\n", - "\u24ff\n", + "\n", + "\n", + "b\n", + "\u24ff\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "1\n", - "\u24ff\n", + "\n", + "\n", + "1\n", + "\u24ff\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f87301b6cc0> >" + " *' at 0x1052dcfc0> >" ] } ], @@ -1108,462 +1108,482 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "0->5\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "0->6\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "1->5\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "1->6\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "2->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "2->5\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "2->6\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "3->1\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "3->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "3->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "3->5\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "3->6\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "4->1\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "4->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "4->3\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "4->5\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "4->6\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "5->5\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "5->7\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "5->8\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "6->6\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "6->7\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "6->8\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "7->7\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "9\n", - "\n", - "9\n", + "\n", + "9\n", "\n", "\n", "7->9\n", - "\n", - "\n", - "a & b\n", - "\u24ff\n", + "\n", + "\n", + "a & b\n", + "\u24ff\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "7->10\n", - "\n", - "\n", - "!a & b\n", - "\u24ff\n", + "\n", + "\n", + "!a & b\n", + "\u24ff\n", "\n", "\n", "8->8\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "8->9\n", - "\n", - "\n", - "a & b\n", - "\u24ff\n", + "\n", + "\n", + "a & b\n", + "\u24ff\n", "\n", "\n", "8->10\n", - "\n", - "\n", - "!a & b\n", - "\u24ff\n", + "\n", + "\n", + "!a & b\n", + "\u24ff\n", "\n", "\n", "9->9\n", - "\n", - "\n", - "a & b\n", - "\u24ff\n", + "\n", + "\n", + "a & b\n", + "\u24ff\n", "\n", "\n", "9->10\n", - "\n", - "\n", - "!a & b\n", - "\u24ff\n", + "\n", + "\n", + "!a & b\n", + "\u24ff\n", "\n", "\n", "11\n", - "\n", - "11\n", + "\n", + "11\n", "\n", "\n", "9->11\n", - "\n", - "\n", - "a & !b\n", - "\u24ff\n", + "\n", + "\n", + "a & !b\n", + "\u24ff\n", "\n", "\n", "12\n", - "\n", - "12\n", + "\n", + "12\n", "\n", "\n", "9->12\n", - "\n", - "\n", - "!a & !b\n", - "\u24ff\n", + "\n", + "\n", + "!a & !b\n", + "\u24ff\n", "\n", "\n", "10->9\n", - "\n", - "\n", - "a & b\n", - "\u24ff\n", + "\n", + "\n", + "a & b\n", + "\u24ff\n", "\n", "\n", "10->10\n", - "\n", - "\n", - "!a & b\n", - "\u24ff\n", + "\n", + "\n", + "!a & b\n", + "\u24ff\n", "\n", "\n", "10->11\n", - "\n", - "\n", - "a & !b\n", - "\u24ff\n", + "\n", + "\n", + "a & !b\n", + "\u24ff\n", "\n", "\n", "10->12\n", - "\n", - "\n", - "!a & !b\n", - "\u24ff\n", + "\n", + "\n", + "!a & !b\n", + "\u24ff\n", "\n", "\n", "11->9\n", - "\n", - "\n", - "a & b\n", - "\u24ff\n", + "\n", + "\n", + "a & b\n", + "\u24ff\n", "\n", "\n", "11->10\n", - "\n", - "\n", - "!a & b\n", - "\u24ff\n", + "\n", + "\n", + "!a & b\n", + "\u24ff\n", "\n", "\n", "11->11\n", - "\n", - "\n", - "a & !b\n", - "\u24ff\n", + "\n", + "\n", + "a & !b\n", + "\u24ff\n", "\n", "\n", "11->12\n", - "\n", - "\n", - "!a & !b\n", - "\u24ff\n", + "\n", + "\n", + "!a & !b\n", + "\u24ff\n", "\n", "\n", "12->9\n", - "\n", - "\n", - "a & b\n", - "\u24ff\n", + "\n", + "\n", + "a & b\n", + "\u24ff\n", "\n", "\n", "12->10\n", - "\n", - "\n", - "!a & b\n", - "\u24ff\n", + "\n", + "\n", + "!a & b\n", + "\u24ff\n", "\n", "\n", "12->11\n", - "\n", - "\n", - "a & !b\n", - "\u24ff\n", + "\n", + "\n", + "a & !b\n", + "\u24ff\n", "\n", "\n", "12->12\n", - "\n", - "\n", - "!a & !b\n", - "\u24ff\n", + "\n", + "\n", + "!a & !b\n", + "\u24ff\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f87301b6ba0> >" + " *' at 0x1052dcba0> >" ] } ], "prompt_number": 13 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "a.is_empty()" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 14, + "text": [ + "False" + ] + } + ], + "prompt_number": 14 } ], "metadata": {}