diff --git a/.github/workflows/run_docs.yaml b/.github/workflows/run_docs.yaml index fede9c5..0b8b3c6 100644 --- a/.github/workflows/run_docs.yaml +++ b/.github/workflows/run_docs.yaml @@ -18,7 +18,6 @@ jobs: - name: Install dependencies run: | python -m pip install --upgrade pip - pip install -r requirements.txt pip install -e . - name: Install and Build 🔧 # This example project is built using npm and outputs the result to the 'build' folder. Replace with the commands required to build your project, or remove this step entirely if your site is pre-built. run: | diff --git a/.github/workflows/run_tests.yaml b/.github/workflows/run_tests.yaml index 1dcc31d..b551861 100644 --- a/.github/workflows/run_tests.yaml +++ b/.github/workflows/run_tests.yaml @@ -18,7 +18,6 @@ - name: Install dependencies run: | python -m pip install --upgrade pip - pip install -r requirements.txt pip install -e . - name: Run tests with pytest run: pytest \ No newline at end of file diff --git a/notebooks/demo.ipynb b/notebooks/demo.ipynb index 2253c47..3457a52 100644 --- a/notebooks/demo.ipynb +++ b/notebooks/demo.ipynb @@ -3,45 +3,156 @@ { "cell_type": "code", "execution_count": 1, - "metadata": { - "collapsed": true - }, + "metadata": {}, "outputs": [], "source": [ - "from austr.buildin.presentations import buechi_arithmetic\n", + "from autstr.buildin.presentations import buechi_arithmetic\n", "from visual_automata.fa.dfa import VisualDFA\n", - "from austr.utils.automata_tools import iterate_language" + "from autstr.utils.automata_tools import iterate_language" ] }, { "cell_type": "code", "execution_count": 2, - "outputs": [], - "source": [ - "ba = buechi_arithmetic()" - ], "metadata": { "collapsed": false, + "jupyter": { + "outputs_hidden": false + }, "pycharm": { "name": "#%%\n" } - } + }, + "outputs": [], + "source": [ + "ba = buechi_arithmetic()" + ] }, { "cell_type": "code", "execution_count": 3, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "A(x,x,x): 3 states\n" - ] + "metadata": { + "collapsed": false, + "jupyter": { + "outputs_hidden": false }, + "pycharm": { + "name": "#%%\n" + } + }, + "outputs": [ { "data": { - "image/svg+xml": "\n\n\n\n\n\n\n\n\nInitial\n\n\n\n\n0\n\n0\n\n\n\nInitial->0\n\n\n\n\n\n1\n\n1\n\n\n\n0->1\n\n\n ('*',) \n\n\n\n0->1\n\n\n ('1',) \n\n\n\n2\n\n\n2\n\n\n\n0->2\n\n\n ('0',) \n\n\n\n1->1\n\n\n ('0',) \n\n\n\n1->1\n\n\n ('*',) \n\n\n\n1->1\n\n\n ('1',) \n\n\n\n2->1\n\n\n ('0',) \n\n\n\n2->1\n\n\n ('1',) \n\n\n\n2->2\n\n\n ('*',) \n\n\n\n", - "text/plain": "" + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Initial\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "Initial->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + " ('0',) \n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + " ('1',) \n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + " ('*',) \n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + " ('1',) \n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + " ('*',) \n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + " ('0',) \n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + " ('0',) \n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + " ('1',) \n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + " ('*',) \n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] }, "execution_count": 3, "metadata": {}, @@ -52,41 +163,133 @@ "# Define zero\n", "ba.update(O='A(x,x,x)')\n", "VisualDFA(ba.automata['O']).show_diagram()" - ], + ] + }, + { + "cell_type": "code", + "execution_count": 4, "metadata": { "collapsed": false, + "jupyter": { + "outputs_hidden": false + }, "pycharm": { "name": "#%%\n" } - } - }, - { - "cell_type": "code", - "execution_count": 4, + }, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "O(x): 3 states\n", - "-O(x): 4 states\n", - "O(y): 3 states\n", - "O(z): 3 states\n", - "(O(y) | O(z)): 5 states\n", - "A(y,z,x): 16 states\n", - "-A(y,z,x): 46 states\n", - "(O(y) | O(z) | -A(y,z,x)): 54 states\n", - "-(O(y) | O(z) | -A(y,z,x)): 14 states\n", - "all z.(O(y) | O(z) | -A(y,z,x)): 13 states\n", - "-all z.(O(y) | O(z) | -A(y,z,x)): 8 states\n", - "all y z.(O(y) | O(z) | -A(y,z,x)): 3 states\n", - "(-O(x) & all y z.(O(y) | O(z) | -A(y,z,x))): 3 states\n" - ] - }, { "data": { - "image/svg+xml": "\n\n\n\n\n\n\n\n\nInitial\n\n\n\n\n2\n\n2\n\n\n\nInitial->2\n\n\n\n\n\n0\n\n\n0\n\n\n\n0->0\n\n\n ('*',) \n\n\n\n1\n\n1\n\n\n\n0->1\n\n\n ('0',) \n\n\n\n0->1\n\n\n ('1',) \n\n\n\n1->1\n\n\n ('0',) \n\n\n\n1->1\n\n\n ('*',) \n\n\n\n1->1\n\n\n ('1',) \n\n\n\n2->0\n\n\n ('1',) \n\n\n\n2->1\n\n\n ('0',) \n\n\n\n2->1\n\n\n ('*',) \n\n\n\n", - "text/plain": "" + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Initial\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "Initial->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + " ('0',) \n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + " ('1',) \n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + " ('*',) \n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + " ('0',) \n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + " ('1',) \n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + " ('*',) \n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + " ('0',) \n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + " ('*',) \n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + " ('1',) \n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] }, "execution_count": 4, "metadata": {}, @@ -97,32 +300,467 @@ "# Define one\n", "ba.update(I='not O(x) and forall y z.(O(y) or O(z) or not A(y, z, x))')\n", "VisualDFA(ba.automata['I']).show_diagram()" - ], + ] + }, + { + "cell_type": "code", + "execution_count": 5, "metadata": { "collapsed": false, + "jupyter": { + "outputs_hidden": false + }, "pycharm": { "name": "#%%\n" } - } - }, - { - "cell_type": "code", - "execution_count": 5, + }, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "I(x): 3 states\n", - "A(u,x,v): 16 states\n", - "(I(x) & A(u,x,v)): 6 states\n", - "exists x.(I(x) & A(u,x,v)): 6 states\n" - ] - }, { "data": { - "image/svg+xml": "\n\n\n\n\n\n\n\n\nInitial\n\n\n\n\n0\n\n0\n\n\n\nInitial->0\n\n\n\n\n\n1\n\n1\n\n\n\n0->1\n\n\n ('*', '1') \n\n\n\n0->1\n\n\n ('1', '1') \n\n\n\n0->1\n\n\n ('*', '*') \n\n\n\n0->1\n\n\n ('1', '*') \n\n\n\n0->1\n\n\n ('0', '*') \n\n\n\n0->1\n\n\n ('0', '0') \n\n\n\n0->1\n\n\n ('*', '0') \n\n\n\n3\n\n3\n\n\n\n0->3\n\n\n ('1', '0') \n\n\n\n4\n\n\n4\n\n\n\n0->4\n\n\n ('0', '1') \n\n\n\n1->1\n\n\n ('*', '1') \n\n\n\n1->1\n\n\n ('1', '1') \n\n\n\n1->1\n\n\n ('*', '*') \n\n\n\n1->1\n\n\n ('1', '*') \n\n\n\n1->1\n\n\n ('0', '*') \n\n\n\n1->1\n\n\n ('0', '0') \n\n\n\n1->1\n\n\n ('*', '0') \n\n\n\n1->1\n\n\n ('0', '1') \n\n\n\n1->1\n\n\n ('1', '0') \n\n\n\n2\n\n2\n\n\n\n2->1\n\n\n ('*', '1') \n\n\n\n2->1\n\n\n ('*', '*') \n\n\n\n2->1\n\n\n ('1', '*') \n\n\n\n2->1\n\n\n ('0', '*') \n\n\n\n2->1\n\n\n ('*', '0') \n\n\n\n2->1\n\n\n ('0', '1') \n\n\n\n2->1\n\n\n ('1', '0') \n\n\n\n2->2\n\n\n ('0', '0') \n\n\n\n2->4\n\n\n ('1', '1') \n\n\n\n3->1\n\n\n ('1', '1') \n\n\n\n3->1\n\n\n ('*', '*') \n\n\n\n3->1\n\n\n ('1', '*') \n\n\n\n3->1\n\n\n ('0', '*') \n\n\n\n3->1\n\n\n ('0', '0') \n\n\n\n3->1\n\n\n ('*', '0') \n\n\n\n3->2\n\n\n ('0', '1') \n\n\n\n3->3\n\n\n ('1', '0') \n\n\n\n5\n\n\n5\n\n\n\n3->5\n\n\n ('*', '1') \n\n\n\n4->1\n\n\n ('*', '1') \n\n\n\n4->1\n\n\n ('1', '*') \n\n\n\n4->1\n\n\n ('0', '*') \n\n\n\n4->1\n\n\n ('*', '0') \n\n\n\n4->1\n\n\n ('0', '1') \n\n\n\n4->1\n\n\n ('1', '0') \n\n\n\n4->2\n\n\n ('0', '0') \n\n\n\n4->4\n\n\n ('1', '1') \n\n\n\n4->5\n\n\n ('*', '*') \n\n\n\n5->1\n\n\n ('*', '1') \n\n\n\n5->1\n\n\n ('1', '1') \n\n\n\n5->1\n\n\n ('1', '*') \n\n\n\n5->1\n\n\n ('0', '*') \n\n\n\n5->1\n\n\n ('0', '0') \n\n\n\n5->1\n\n\n ('*', '0') \n\n\n\n5->1\n\n\n ('0', '1') \n\n\n\n5->1\n\n\n ('1', '0') \n\n\n\n5->5\n\n\n ('*', '*') \n\n\n\n", - "text/plain": "" + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Initial\n", + "\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "Initial->4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + " ('1', '1') \n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + " ('*', '*') \n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + " ('*', '1') \n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + " ('0', '1') \n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + " ('1', '*') \n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + " ('0', '*') \n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + " ('1', '0') \n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + " ('*', '0') \n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "0->5\n", + "\n", + "\n", + " ('0', '0') \n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + " ('1', '0') \n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + " ('*', '1') \n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + " ('1', '1') \n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + " ('0', '0') \n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + " ('1', '*') \n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + " ('*', '*') \n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + " ('0', '*') \n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + " ('*', '0') \n", + "\n", + "\n", + "\n", + "1->5\n", + "\n", + "\n", + " ('0', '1') \n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + " ('*', '*') \n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + " ('1', '1') \n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + " ('*', '1') \n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + " ('0', '1') \n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + " ('0', '0') \n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + " ('1', '*') \n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + " ('0', '*') \n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + " ('1', '0') \n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + " ('*', '0') \n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + " ('1', '1') \n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + " ('*', '1') \n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + " ('0', '1') \n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + " ('0', '0') \n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + " ('1', '*') \n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + " ('*', '*') \n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + " ('0', '*') \n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + " ('1', '0') \n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + " ('*', '0') \n", + "\n", + "\n", + "\n", + "4->0\n", + "\n", + "\n", + " ('0', '1') \n", + "\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + " ('1', '0') \n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + " ('1', '1') \n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + " ('*', '1') \n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + " ('0', '0') \n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + " ('1', '*') \n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + " ('*', '*') \n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + " ('0', '*') \n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + " ('*', '0') \n", + "\n", + "\n", + "\n", + "5->0\n", + "\n", + "\n", + " ('1', '1') \n", + "\n", + "\n", + "\n", + "5->3\n", + "\n", + "\n", + " ('*', '1') \n", + "\n", + "\n", + "\n", + "5->3\n", + "\n", + "\n", + " ('0', '1') \n", + "\n", + "\n", + "\n", + "5->3\n", + "\n", + "\n", + " ('1', '*') \n", + "\n", + "\n", + "\n", + "5->3\n", + "\n", + "\n", + " ('*', '*') \n", + "\n", + "\n", + "\n", + "5->3\n", + "\n", + "\n", + " ('0', '*') \n", + "\n", + "\n", + "\n", + "5->3\n", + "\n", + "\n", + " ('1', '0') \n", + "\n", + "\n", + "\n", + "5->3\n", + "\n", + "\n", + " ('*', '0') \n", + "\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + " ('0', '0') \n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] }, "execution_count": 5, "metadata": {}, @@ -133,29 +771,133 @@ "# Define successor\n", "ba.update(S='exists x.(I(x) and A(u, x, v))')\n", "VisualDFA(ba.automata['S']).show_diagram()" - ], + ] + }, + { + "cell_type": "code", + "execution_count": 6, "metadata": { "collapsed": false, + "jupyter": { + "outputs_hidden": false + }, "pycharm": { "name": "#%%\n" } - } - }, - { - "cell_type": "code", - "execution_count": 6, + }, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "B(x,x): 3 states\n" - ] - }, { "data": { - "image/svg+xml": "\n\n\n\n\n\n\n\n\nInitial\n\n\n\n\n0\n\n0\n\n\n\nInitial->0\n\n\n\n\n\n0->0\n\n\n ('0',) \n\n\n\n1\n\n\n1\n\n\n\n0->1\n\n\n ('1',) \n\n\n\n2\n\n2\n\n\n\n0->2\n\n\n ('*',) \n\n\n\n1->1\n\n\n ('*',) \n\n\n\n1->2\n\n\n ('0',) \n\n\n\n1->2\n\n\n ('1',) \n\n\n\n2->2\n\n\n ('0',) \n\n\n\n2->2\n\n\n ('*',) \n\n\n\n2->2\n\n\n ('1',) \n\n\n\n", - "text/plain": "" + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Initial\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "Initial->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + " ('*',) \n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + " ('0',) \n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + " ('1',) \n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + " ('1',) \n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + " ('0',) \n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + " ('*',) \n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + " ('0',) \n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + " ('1',) \n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + " ('*',) \n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] }, "execution_count": 6, "metadata": {}, @@ -166,33 +908,675 @@ "# Define powers of two\n", "ba.update(P='B(x,x)')\n", "VisualDFA(ba.automata['P']).show_diagram()" - ], + ] + }, + { + "cell_type": "code", + "execution_count": 7, "metadata": { "collapsed": false, + "jupyter": { + "outputs_hidden": false + }, "pycharm": { "name": "#%%\n" } - } - }, - { - "cell_type": "code", - "execution_count": 7, + }, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "O(z): 3 states\n", - "-O(z): 4 states\n", - "A(x,z,y): 16 states\n", - "(-O(z) & A(x,z,y)): 16 states\n", - "exists z.(-O(z) & A(x,z,y)): 9 states\n" - ] - }, { "data": { - "image/svg+xml": "\n\n\n\n\n\n\n\n\nInitial\n\n\n\n\n1\n\n1\n\n\n\nInitial->1\n\n\n\n\n\n0\n\n0\n\n\n\n0->0\n\n\n ('0', '0') \n\n\n\n0->0\n\n\n ('0', '1') \n\n\n\n4\n\n\n4\n\n\n\n0->4\n\n\n ('1', '1') \n\n\n\n5\n\n5\n\n\n\n0->5\n\n\n ('1', '0') \n\n\n\n6\n\n6\n\n\n\n0->6\n\n\n ('*', '1') \n\n\n\n0->6\n\n\n ('*', '*') \n\n\n\n0->6\n\n\n ('1', '*') \n\n\n\n0->6\n\n\n ('0', '*') \n\n\n\n0->6\n\n\n ('*', '0') \n\n\n\n1->4\n\n\n ('0', '1') \n\n\n\n1->5\n\n\n ('1', '1') \n\n\n\n1->5\n\n\n ('0', '0') \n\n\n\n1->5\n\n\n ('1', '0') \n\n\n\n1->6\n\n\n ('*', '1') \n\n\n\n1->6\n\n\n ('*', '*') \n\n\n\n1->6\n\n\n ('1', '*') \n\n\n\n1->6\n\n\n ('0', '*') \n\n\n\n1->6\n\n\n ('*', '0') \n\n\n\n2\n\n2\n\n\n\n2->2\n\n\n ('*', '0') \n\n\n\n2->6\n\n\n ('1', '1') \n\n\n\n2->6\n\n\n ('*', '*') \n\n\n\n2->6\n\n\n ('1', '*') \n\n\n\n2->6\n\n\n ('0', '*') \n\n\n\n2->6\n\n\n ('0', '0') \n\n\n\n2->6\n\n\n ('0', '1') \n\n\n\n2->6\n\n\n ('1', '0') \n\n\n\n7\n\n\n7\n\n\n\n2->7\n\n\n ('*', '1') \n\n\n\n3\n\n3\n\n\n\n3->0\n\n\n ('0', '1') \n\n\n\n3->3\n\n\n ('0', '0') \n\n\n\n3->5\n\n\n ('1', '1') \n\n\n\n3->5\n\n\n ('1', '0') \n\n\n\n3->6\n\n\n ('*', '1') \n\n\n\n3->6\n\n\n ('*', '*') \n\n\n\n3->6\n\n\n ('1', '*') \n\n\n\n3->6\n\n\n ('0', '*') \n\n\n\n3->6\n\n\n ('*', '0') \n\n\n\n4->0\n\n\n ('0', '0') \n\n\n\n4->0\n\n\n ('0', '1') \n\n\n\n4->2\n\n\n ('*', '0') \n\n\n\n4->4\n\n\n ('1', '1') \n\n\n\n4->5\n\n\n ('1', '0') \n\n\n\n4->6\n\n\n ('1', '*') \n\n\n\n4->6\n\n\n ('0', '*') \n\n\n\n4->7\n\n\n ('*', '1') \n\n\n\n8\n\n\n8\n\n\n\n4->8\n\n\n ('*', '*') \n\n\n\n5->0\n\n\n ('0', '1') \n\n\n\n5->2\n\n\n ('*', '0') \n\n\n\n5->3\n\n\n ('0', '0') \n\n\n\n5->5\n\n\n ('1', '1') \n\n\n\n5->5\n\n\n ('1', '0') \n\n\n\n5->6\n\n\n ('*', '*') \n\n\n\n5->6\n\n\n ('1', '*') \n\n\n\n5->6\n\n\n ('0', '*') \n\n\n\n5->7\n\n\n ('*', '1') \n\n\n\n6->6\n\n\n ('*', '1') \n\n\n\n6->6\n\n\n ('1', '1') \n\n\n\n6->6\n\n\n ('*', '*') \n\n\n\n6->6\n\n\n ('1', '*') \n\n\n\n6->6\n\n\n ('0', '*') \n\n\n\n6->6\n\n\n ('0', '0') \n\n\n\n6->6\n\n\n ('*', '0') \n\n\n\n6->6\n\n\n ('0', '1') \n\n\n\n6->6\n\n\n ('1', '0') \n\n\n\n7->2\n\n\n ('*', '0') \n\n\n\n7->6\n\n\n ('1', '1') \n\n\n\n7->6\n\n\n ('1', '*') \n\n\n\n7->6\n\n\n ('0', '*') \n\n\n\n7->6\n\n\n ('0', '0') \n\n\n\n7->6\n\n\n ('0', '1') \n\n\n\n7->6\n\n\n ('1', '0') \n\n\n\n7->7\n\n\n ('*', '1') \n\n\n\n7->8\n\n\n ('*', '*') \n\n\n\n8->6\n\n\n ('*', '1') \n\n\n\n8->6\n\n\n ('1', '1') \n\n\n\n8->6\n\n\n ('1', '*') \n\n\n\n8->6\n\n\n ('0', '*') \n\n\n\n8->6\n\n\n ('0', '0') \n\n\n\n8->6\n\n\n ('*', '0') \n\n\n\n8->6\n\n\n ('0', '1') \n\n\n\n8->6\n\n\n ('1', '0') \n\n\n\n8->8\n\n\n ('*', '*') \n\n\n\n", - "text/plain": "" + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Initial\n", + "\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "Initial->5\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + " ('0', '1') \n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + " ('0', '0') \n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + " ('1', '0') \n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + " ('1', '1') \n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "0->6\n", + "\n", + "\n", + " ('*', '1') \n", + "\n", + "\n", + "\n", + "0->6\n", + "\n", + "\n", + " ('1', '*') \n", + "\n", + "\n", + "\n", + "0->6\n", + "\n", + "\n", + " ('*', '*') \n", + "\n", + "\n", + "\n", + "0->6\n", + "\n", + "\n", + " ('0', '*') \n", + "\n", + "\n", + "\n", + "0->6\n", + "\n", + "\n", + " ('*', '0') \n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + " ('*', '0') \n", + "\n", + "\n", + "\n", + "1->6\n", + "\n", + "\n", + " ('1', '1') \n", + "\n", + "\n", + "\n", + "1->6\n", + "\n", + "\n", + " ('0', '1') \n", + "\n", + "\n", + "\n", + "1->6\n", + "\n", + "\n", + " ('0', '0') \n", + "\n", + "\n", + "\n", + "1->6\n", + "\n", + "\n", + " ('1', '*') \n", + "\n", + "\n", + "\n", + "1->6\n", + "\n", + "\n", + " ('*', '*') \n", + "\n", + "\n", + "\n", + "1->6\n", + "\n", + "\n", + " ('0', '*') \n", + "\n", + "\n", + "\n", + "1->6\n", + "\n", + "\n", + " ('1', '0') \n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "1->7\n", + "\n", + "\n", + " ('*', '1') \n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + " ('0', '1') \n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + " ('*', '0') \n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + " ('1', '1') \n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + " ('1', '0') \n", + "\n", + "\n", + "\n", + "2->6\n", + "\n", + "\n", + " ('1', '*') \n", + "\n", + "\n", + "\n", + "2->6\n", + "\n", + "\n", + " ('*', '*') \n", + "\n", + "\n", + "\n", + "2->6\n", + "\n", + "\n", + " ('0', '*') \n", + "\n", + "\n", + "\n", + "2->7\n", + "\n", + "\n", + " ('*', '1') \n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "2->8\n", + "\n", + "\n", + " ('0', '0') \n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + " ('0', '1') \n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + " ('0', '0') \n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + " ('*', '0') \n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + " ('1', '0') \n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + " ('1', '1') \n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + " ('*', '*') \n", + "\n", + "\n", + "\n", + "3->6\n", + "\n", + "\n", + " ('1', '*') \n", + "\n", + "\n", + "\n", + "3->6\n", + "\n", + "\n", + " ('0', '*') \n", + "\n", + "\n", + "\n", + "3->7\n", + "\n", + "\n", + " ('*', '1') \n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + " ('*', '*') \n", + "\n", + "\n", + "\n", + "4->6\n", + "\n", + "\n", + " ('1', '1') \n", + "\n", + "\n", + "\n", + "4->6\n", + "\n", + "\n", + " ('*', '1') \n", + "\n", + "\n", + "\n", + "4->6\n", + "\n", + "\n", + " ('0', '1') \n", + "\n", + "\n", + "\n", + "4->6\n", + "\n", + "\n", + " ('0', '0') \n", + "\n", + "\n", + "\n", + "4->6\n", + "\n", + "\n", + " ('1', '*') \n", + "\n", + "\n", + "\n", + "4->6\n", + "\n", + "\n", + " ('0', '*') \n", + "\n", + "\n", + "\n", + "4->6\n", + "\n", + "\n", + " ('1', '0') \n", + "\n", + "\n", + "\n", + "4->6\n", + "\n", + "\n", + " ('*', '0') \n", + "\n", + "\n", + "\n", + "5->2\n", + "\n", + "\n", + " ('1', '1') \n", + "\n", + "\n", + "\n", + "5->2\n", + "\n", + "\n", + " ('0', '0') \n", + "\n", + "\n", + "\n", + "5->2\n", + "\n", + "\n", + " ('1', '0') \n", + "\n", + "\n", + "\n", + "5->3\n", + "\n", + "\n", + " ('0', '1') \n", + "\n", + "\n", + "\n", + "5->6\n", + "\n", + "\n", + " ('*', '1') \n", + "\n", + "\n", + "\n", + "5->6\n", + "\n", + "\n", + " ('1', '*') \n", + "\n", + "\n", + "\n", + "5->6\n", + "\n", + "\n", + " ('*', '*') \n", + "\n", + "\n", + "\n", + "5->6\n", + "\n", + "\n", + " ('0', '*') \n", + "\n", + "\n", + "\n", + "5->6\n", + "\n", + "\n", + " ('*', '0') \n", + "\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + " ('1', '1') \n", + "\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + " ('*', '1') \n", + "\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + " ('0', '1') \n", + "\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + " ('0', '0') \n", + "\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + " ('1', '*') \n", + "\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + " ('*', '*') \n", + "\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + " ('0', '*') \n", + "\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + " ('1', '0') \n", + "\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + " ('*', '0') \n", + "\n", + "\n", + "\n", + "7->1\n", + "\n", + "\n", + " ('*', '0') \n", + "\n", + "\n", + "\n", + "7->4\n", + "\n", + "\n", + " ('*', '*') \n", + "\n", + "\n", + "\n", + "7->6\n", + "\n", + "\n", + " ('1', '1') \n", + "\n", + "\n", + "\n", + "7->6\n", + "\n", + "\n", + " ('0', '1') \n", + "\n", + "\n", + "\n", + "7->6\n", + "\n", + "\n", + " ('0', '0') \n", + "\n", + "\n", + "\n", + "7->6\n", + "\n", + "\n", + " ('1', '*') \n", + "\n", + "\n", + "\n", + "7->6\n", + "\n", + "\n", + " ('0', '*') \n", + "\n", + "\n", + "\n", + "7->6\n", + "\n", + "\n", + " ('1', '0') \n", + "\n", + "\n", + "\n", + "7->7\n", + "\n", + "\n", + " ('*', '1') \n", + "\n", + "\n", + "\n", + "8->0\n", + "\n", + "\n", + " ('0', '1') \n", + "\n", + "\n", + "\n", + "8->2\n", + "\n", + "\n", + " ('1', '1') \n", + "\n", + "\n", + "\n", + "8->2\n", + "\n", + "\n", + " ('1', '0') \n", + "\n", + "\n", + "\n", + "8->6\n", + "\n", + "\n", + " ('*', '1') \n", + "\n", + "\n", + "\n", + "8->6\n", + "\n", + "\n", + " ('1', '*') \n", + "\n", + "\n", + "\n", + "8->6\n", + "\n", + "\n", + " ('*', '*') \n", + "\n", + "\n", + "\n", + "8->6\n", + "\n", + "\n", + " ('0', '*') \n", + "\n", + "\n", + "\n", + "8->6\n", + "\n", + "\n", + " ('*', '0') \n", + "\n", + "\n", + "\n", + "8->8\n", + "\n", + "\n", + " ('0', '0') \n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] }, "execution_count": 7, "metadata": {}, @@ -203,43 +1587,467 @@ "# Define linear order\n", "ba.update(Smaller='exist z.(not O(z) and A(x, z, y))')\n", "VisualDFA(ba.automata['Smaller']).show_diagram()" - ], + ] + }, + { + "cell_type": "code", + "execution_count": 8, "metadata": { "collapsed": false, + "jupyter": { + "outputs_hidden": false + }, "pycharm": { "name": "#%%\n" } - } - }, - { - "cell_type": "code", - "execution_count": 8, + }, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "P(y): 3 states\n", - "Smaller(x0,y): 9 states\n", - "(P(y) & Smaller(x0,y)): 6 states\n", - "A(x0,x1,x): 16 states\n", - "(P(y) & Smaller(x0,y) & A(x0,x1,x)): 20 states\n", - "B(x1,y): 6 states\n", - "(P(y) & Smaller(x0,y) & A(x0,x1,x) & B(x1,y)): 8 states\n", - "Smaller(y,y1): 9 states\n", - "B(x1,y1): 6 states\n", - "(Smaller(y,y1) & B(x1,y1)): 8 states\n", - "exists y1.(Smaller(y,y1) & B(x1,y1)): 8 states\n", - "-exists y1.(Smaller(y,y1) & B(x1,y1)): 14 states\n", - "(P(y) & Smaller(x0,y) & A(x0,x1,x) & B(x1,y) & -exists y1.(Smaller(y,y1) & B(x1,y1))): 8 states\n", - "exists x1.(P(y) & Smaller(x0,y) & A(x0,x1,x) & B(x1,y) & -exists y1.(Smaller(y,y1) & B(x1,y1))): 8 states\n", - "exists x0 x1.(P(y) & Smaller(x0,y) & A(x0,x1,x) & B(x1,y) & -exists y1.(Smaller(y,y1) & B(x1,y1))): 6 states\n" - ] - }, { "data": { - "image/svg+xml": "\n\n\n\n\n\n\n\n\nInitial\n\n\n\n\n1\n\n1\n\n\n\nInitial->1\n\n\n\n\n\n0\n\n\n0\n\n\n\n0->0\n\n\n ('*', '*') \n\n\n\n4\n\n4\n\n\n\n0->4\n\n\n ('*', '1') \n\n\n\n0->4\n\n\n ('1', '1') \n\n\n\n0->4\n\n\n ('1', '*') \n\n\n\n0->4\n\n\n ('0', '*') \n\n\n\n0->4\n\n\n ('0', '0') \n\n\n\n0->4\n\n\n ('*', '0') \n\n\n\n0->4\n\n\n ('0', '1') \n\n\n\n0->4\n\n\n ('1', '0') \n\n\n\n1->0\n\n\n ('0', '1') \n\n\n\n3\n\n3\n\n\n\n1->3\n\n\n ('0', '0') \n\n\n\n1->3\n\n\n ('1', '0') \n\n\n\n1->4\n\n\n ('*', '1') \n\n\n\n1->4\n\n\n ('*', '*') \n\n\n\n1->4\n\n\n ('1', '*') \n\n\n\n1->4\n\n\n ('0', '*') \n\n\n\n1->4\n\n\n ('*', '0') \n\n\n\n5\n\n\n5\n\n\n\n1->5\n\n\n ('1', '1') \n\n\n\n2\n\n2\n\n\n\n2->2\n\n\n ('0', '*') \n\n\n\n2->4\n\n\n ('*', '1') \n\n\n\n2->4\n\n\n ('1', '1') \n\n\n\n2->4\n\n\n ('*', '*') \n\n\n\n2->4\n\n\n ('0', '0') \n\n\n\n2->4\n\n\n ('*', '0') \n\n\n\n2->4\n\n\n ('0', '1') \n\n\n\n2->4\n\n\n ('1', '0') \n\n\n\n2->5\n\n\n ('1', '*') \n\n\n\n3->3\n\n\n ('0', '0') \n\n\n\n3->3\n\n\n ('1', '0') \n\n\n\n3->4\n\n\n ('*', '1') \n\n\n\n3->4\n\n\n ('*', '*') \n\n\n\n3->4\n\n\n ('1', '*') \n\n\n\n3->4\n\n\n ('0', '*') \n\n\n\n3->4\n\n\n ('*', '0') \n\n\n\n3->4\n\n\n ('0', '1') \n\n\n\n3->5\n\n\n ('1', '1') \n\n\n\n4->4\n\n\n ('*', '1') \n\n\n\n4->4\n\n\n ('1', '1') \n\n\n\n4->4\n\n\n ('*', '*') \n\n\n\n4->4\n\n\n ('1', '*') \n\n\n\n4->4\n\n\n ('0', '*') \n\n\n\n4->4\n\n\n ('0', '0') \n\n\n\n4->4\n\n\n ('*', '0') \n\n\n\n4->4\n\n\n ('0', '1') \n\n\n\n4->4\n\n\n ('1', '0') \n\n\n\n5->0\n\n\n ('*', '*') \n\n\n\n5->2\n\n\n ('0', '*') \n\n\n\n5->4\n\n\n ('*', '1') \n\n\n\n5->4\n\n\n ('1', '1') \n\n\n\n5->4\n\n\n ('0', '0') \n\n\n\n5->4\n\n\n ('*', '0') \n\n\n\n5->4\n\n\n ('0', '1') \n\n\n\n5->4\n\n\n ('1', '0') \n\n\n\n5->5\n\n\n ('1', '*') \n\n\n\n", - "text/plain": "" + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Initial\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "Initial->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + " ('1', '1') \n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + " ('0', '1') \n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + " ('*', '1') \n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + " ('1', '*') \n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + " ('*', '*') \n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + " ('0', '*') \n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + " ('*', '0') \n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "0->5\n", + "\n", + "\n", + " ('0', '0') \n", + "\n", + "\n", + "\n", + "0->5\n", + "\n", + "\n", + " ('1', '0') \n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + " ('1', '*') \n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + " ('0', '*') \n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + " ('*', '*') \n", + "\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + " ('1', '1') \n", + "\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + " ('*', '1') \n", + "\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + " ('0', '1') \n", + "\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + " ('0', '0') \n", + "\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + " ('1', '0') \n", + "\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + " ('*', '0') \n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + " ('1', '*') \n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + " ('0', '*') \n", + "\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + " ('1', '1') \n", + "\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + " ('*', '1') \n", + "\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + " ('0', '1') \n", + "\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + " ('0', '0') \n", + "\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + " ('*', '*') \n", + "\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + " ('1', '0') \n", + "\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + " ('*', '0') \n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + " ('*', '*') \n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + " ('1', '1') \n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + " ('*', '1') \n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + " ('0', '1') \n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + " ('0', '0') \n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + " ('1', '*') \n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + " ('0', '*') \n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + " ('1', '0') \n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + " ('*', '0') \n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + " ('1', '1') \n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + " ('*', '1') \n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + " ('0', '1') \n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + " ('0', '0') \n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + " ('1', '*') \n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + " ('*', '*') \n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + " ('0', '*') \n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + " ('1', '0') \n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + " ('*', '0') \n", + "\n", + "\n", + "\n", + "5->1\n", + "\n", + "\n", + " ('1', '1') \n", + "\n", + "\n", + "\n", + "5->4\n", + "\n", + "\n", + " ('*', '1') \n", + "\n", + "\n", + "\n", + "5->4\n", + "\n", + "\n", + " ('0', '1') \n", + "\n", + "\n", + "\n", + "5->4\n", + "\n", + "\n", + " ('1', '*') \n", + "\n", + "\n", + "\n", + "5->4\n", + "\n", + "\n", + " ('*', '*') \n", + "\n", + "\n", + "\n", + "5->4\n", + "\n", + "\n", + " ('0', '*') \n", + "\n", + "\n", + "\n", + "5->4\n", + "\n", + "\n", + " ('*', '0') \n", + "\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + " ('0', '0') \n", + "\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + " ('1', '0') \n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] }, "execution_count": 8, "metadata": {}, @@ -252,106 +2060,90 @@ " E='exists x0 x1.(P(y) and Smaller(x0, y) and A(x0, x1, x) and B(x1, y) and not exists y1.(Smaller(y, y1) and B(x1, y1)))'\n", ")\n", "VisualDFA(ba.automata['E']).show_diagram()" - ], - "metadata": { - "collapsed": false, - "pycharm": { - "name": "#%%\n" - } - } + ] }, { "cell_type": "code", "execution_count": 9, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "O(x): 3 states\n", - "A(x,x,y): 6 states\n", - "A(x,u,v): 16 states\n", - "(A(x,x,y) & A(x,u,v)): 17 states\n", - "P(v): 3 states\n", - "(A(x,x,y) & A(x,u,v) & P(v)): 13 states\n", - "A(v,w,y): 16 states\n", - "(A(x,x,y) & A(x,u,v) & P(v) & A(v,w,y)): 17 states\n", - "exists w.(A(x,x,y) & A(x,u,v) & P(v) & A(v,w,y)): 11 states\n", - "exists v w.(A(x,x,y) & A(x,u,v) & P(v) & A(v,w,y)): 11 states\n", - "exists u v w.(A(x,x,y) & A(x,u,v) & P(v) & A(v,w,y)): 4 states\n", - "exists y u v w.(A(x,x,y) & A(x,u,v) & P(v) & A(v,w,y)): 4 states\n", - "(O(x) | exists y u v w.(A(x,x,y) & A(x,u,v) & P(v) & A(v,w,y))): 5 states\n", - "-(O(x) | exists y u v w.(A(x,x,y) & A(x,u,v) & P(v) & A(v,w,y))): 1 states\n", - "all x.(O(x) | exists y u v w.(A(x,x,y) & A(x,u,v) & P(v) & A(v,w,y))): 1 states\n" - ] - }, - { - "data": { - "image/svg+xml": "\n\n\n\n\n\n\n\n\nInitial\n\n\n\n\n0\n\n\n0\n\n\n\nInitial->0\n\n\n\n\n\n", - "text/plain": "" - }, - "execution_count": 9, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - "# Evaluate 'between a number x>0 and its double lies a power of 2'\n", - "a = ba.evaluate('forall x.(O(x) or exists y u v w.(A(x, x, y) and A(x, u, v) and P(v) and A(v, w, y)))')\n", - "VisualDFA(a).show_diagram()" - ], "metadata": { "collapsed": false, + "jupyter": { + "outputs_hidden": false + }, "pycharm": { "name": "#%%\n" } - } - }, - { - "cell_type": "code", - "execution_count": 11, + }, "outputs": [ { "data": { - "text/plain": "" + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Initial\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "Initial->0\n", + "\n", + "\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] }, - "execution_count": 11, + "execution_count": 9, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "from functools import cmp_to_key\n", - "\n", - "list(map(cmp_to_key(lambda x:x[0]), [(0, 'a'), (1, 'b')]))[" - ], - "metadata": { - "collapsed": false, - "pycharm": { - "name": "#%%\n" - } - } + "# Evaluate 'between a number x>0 and its double lies a power of 2'\n", + "a = ba.evaluate('forall x.(O(x) or exists y u v w.(A(x, x, y) and A(x, u, v) and P(v) and A(v, w, y)))')\n", + "VisualDFA(a).show_diagram()" + ] } ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" }, "language_info": { "codemirror_mode": { "name": "ipython", - "version": 2 + "version": 3 }, "file_extension": ".py", "mimetype": "text/x-python", "name": "python", "nbconvert_exporter": "python", - "pygments_lexer": "ipython2", - "version": "2.7.6" + "pygments_lexer": "ipython3", + "version": "3.12.0" } }, "nbformat": 4, - "nbformat_minor": 0 -} \ No newline at end of file + "nbformat_minor": 4 +} diff --git a/pyproject.toml b/pyproject.toml new file mode 100644 index 0000000..7731bd8 --- /dev/null +++ b/pyproject.toml @@ -0,0 +1,31 @@ +[project] +name = "autstr" +version = "0.1" +description = "Library for working with finitely presentable infinite structures" +authors = [ + { name = "Faried Abu Zaid", email = "fariedaz@gmail.com" } +] +license = { text = "GPL v3.0" } +dependencies = [ + "nltk~=3.7", + "automata-lib~=5.0.0", + "sphinx-autodoc-typehints~=1.19.2", + "ipykernel>=6.29.5", + "jupyter (>=1.1.1,<2.0.0)", + "visual-automata (>=1.1.1,<2.0.0)", +] +requires-python = ">=3.8,<=3.12" + +[project.optional-dependencies] +docs = [ + "sphinxcontrib-applehelp~=1.0.2", + "sphinxcontrib-devhelp~=1.0.2", + "sphinxcontrib-htmlhelp~=2.0.0", + "sphinxcontrib-jsmath~=1.0.1", + "sphinxcontrib-qthelp~=1.0.3", + "sphinxcontrib-serializinghtml~=1.1.5" +] + +[tool.uv] +build-system = "setuptools" +packages = ["autstr", "autstr.utils"] diff --git a/requirements.txt b/requirements.txt deleted file mode 100644 index ca4b8f3..0000000 --- a/requirements.txt +++ /dev/null @@ -1,12 +0,0 @@ -nltk~=3.7 -automata-lib~=5.0.0 -# Doc and testing -pytest~= 7.1.2 -sphinx-autodoc-typehints~=1.19.2 -sphinxcontrib-applehelp~=1.0.2 -sphinxcontrib-devhelp~=1.0.2 -sphinxcontrib-htmlhelp~=2.0.0 -sphinxcontrib-jsmath~=1.0.1 -sphinxcontrib-qthelp~=1.0.3 -sphinxcontrib-serializinghtml~=1.1.5 -cloud-sptheme~=1.10.1.post20200504175005 diff --git a/setup.py b/setup.py deleted file mode 100644 index d8ccae7..0000000 --- a/setup.py +++ /dev/null @@ -1,12 +0,0 @@ -from setuptools import setup - -setup( - name='AuStr', - version='0.1', - packages=['autstr', 'autstr.utils'], - url='https://github.com/fariedabuzaid/AuStr/edit/main/README.md', - license='GPL v3.0', - author='Faried Abu Zaid', - author_email='fariedaz@gmail.com', - description='Library for working finitely presentable structures' -)