From 1fd0aa14a270c18028e5566ac7c20c7acf1c3930 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 20 Jan 2018 11:30:10 +0100 Subject: [PATCH] multiple adjustments for Debian stable * tests/python/ipnbdoctest.py: Adjust to Python <3.6. * tests/python/_autparserr.ipynb: Adjust to older IPython version. * tests/python/stutter-inv.ipynb: Avoid pandas because its output varies from version to version. --- tests/python/_autparserr.ipynb | 9 +- tests/python/ipnbdoctest.py | 15 +- tests/python/stutter-inv.ipynb | 832 +++++---------------------------- 3 files changed, 138 insertions(+), 718 deletions(-) diff --git a/tests/python/_autparserr.ipynb b/tests/python/_autparserr.ipynb index 2aa9b219f..7bbd51789 100644 --- a/tests/python/_autparserr.ipynb +++ b/tests/python/_autparserr.ipynb @@ -6,6 +6,7 @@ "metadata": {}, "outputs": [], "source": [ + "from IPython.display import display\n", "import spot\n", "spot.setup()" ] @@ -27,7 +28,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "Overwriting _example.aut\n" + "Writing _example.aut\n" ] } ], @@ -111,7 +112,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbec845de70> >" + " *' at 0x7f72fc2978d0> >" ] }, "metadata": {}, @@ -183,7 +184,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbec846c5a0> >" + " *' at 0x7f72fc2ce090> >" ] }, "execution_count": 4, @@ -309,7 +310,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbec846c570> >" + " *' at 0x7f72fc2ce5a0> >" ] }, "metadata": {}, diff --git a/tests/python/ipnbdoctest.py b/tests/python/ipnbdoctest.py index ae68deb10..307cfccf1 100755 --- a/tests/python/ipnbdoctest.py +++ b/tests/python/ipnbdoctest.py @@ -115,12 +115,9 @@ def canonicalize(s, type, ignores): s = re.sub(r' fill="black"', '', s) s = re.sub(r' stroke="transparent"', ' stroke="none"', s) s = re.sub(r'>', '>\n<title>', s) - # Different Pandas versions produce different CSS styles. - s = re.sub(r'<style[ a-z]*>.*</style>', - '<style>...</style>', s, flags=re.DOTALL) - - # CalledProcessError message has a final dot in Python 3.6 - s = re.sub(r"(' returned non-zero exit status \d+)\.", r'\1', s) + # Different Pandas versions produce different CSS styles (when there is a + # style). + s = re.sub(r'<style[ a-z]*>.*</style>\n', '', s, flags=re.DOTALL) for n, p in enumerate(ignores): s = re.sub(p, 'IGN{}'.format(n), s) @@ -145,6 +142,12 @@ def canonical_dict(dict, ignores): # sys.exit(77) is used to Skip the test. sys.exit(77) + if 'ename' in dict and dict['ename'] == 'CalledProcessError': + # CalledProcessError message has a final dot in Python 3.6 + dict['evalue'] = \ + re.sub(r"(' returned non-zero exit status \d+)\.", r'\1', + dict['evalue']) + if 'transient' in dict: del dict['transient'] if 'execution_count' in dict: diff --git a/tests/python/stutter-inv.ipynb b/tests/python/stutter-inv.ipynb index aa5f0ae9e..993779734 100644 --- a/tests/python/stutter-inv.ipynb +++ b/tests/python/stutter-inv.ipynb @@ -3,9 +3,7 @@ { "cell_type": "code", "execution_count": 1, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [], "source": [ "import spot\n", @@ -36,9 +34,7 @@ { "cell_type": "code", "execution_count": 2, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -56,9 +52,7 @@ { "cell_type": "code", "execution_count": 3, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -83,9 +77,7 @@ { "cell_type": "code", "execution_count": 4, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -119,9 +111,7 @@ { "cell_type": "code", "execution_count": 5, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -158,9 +148,7 @@ { "cell_type": "code", "execution_count": 6, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -185,9 +173,7 @@ { "cell_type": "code", "execution_count": 7, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -211,9 +197,7 @@ { "cell_type": "code", "execution_count": 8, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -239,9 +223,7 @@ { "cell_type": "code", "execution_count": 9, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -266,9 +248,7 @@ { "cell_type": "code", "execution_count": 10, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -318,7 +298,7 @@ "</svg>\n" ], "text/plain": [ - "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc79ce55870> >" + "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd59d1a6960> >" ] }, "metadata": {}, @@ -365,9 +345,7 @@ { "cell_type": "code", "execution_count": 11, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [], "source": [ "def explain_stut(f):\n", @@ -394,9 +372,7 @@ { "cell_type": "code", "execution_count": 12, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -433,9 +409,7 @@ { "cell_type": "code", "execution_count": 13, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -460,9 +434,7 @@ { "cell_type": "code", "execution_count": 14, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -600,7 +572,7 @@ "</svg>\n" ], "text/plain": [ - "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc79ce2e900> >" + "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd59c941e40> >" ] }, "metadata": {}, @@ -624,9 +596,7 @@ { "cell_type": "code", "execution_count": 15, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -654,9 +624,7 @@ { "cell_type": "code", "execution_count": 16, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -794,7 +762,7 @@ "</svg>\n" ], "text/plain": [ - "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc79ce2e900> >" + "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd59c941e40> >" ] }, "metadata": {}, @@ -830,9 +798,7 @@ { "cell_type": "code", "execution_count": 17, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [], "source": [ "g1 = spot.formula('GF(a & Xa) & GF!a')\n", @@ -843,9 +809,7 @@ { "cell_type": "code", "execution_count": 18, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -873,9 +837,7 @@ { "cell_type": "code", "execution_count": 19, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -951,7 +913,7 @@ "</svg>\n" ], "text/plain": [ - "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc79ce2e8d0> >" + "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd59d1a6ab0> >" ] }, "metadata": {}, @@ -1040,7 +1002,7 @@ "</svg>\n" ], "text/plain": [ - "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc79ce61d50> >" + "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd59c919a80> >" ] }, "metadata": {}, @@ -1069,9 +1031,7 @@ { "cell_type": "code", "execution_count": 20, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -1237,7 +1197,7 @@ "</svg>\n" ], "text/plain": [ - "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc79ce2ea50> >" + "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd59c919930> >" ] }, "metadata": {}, @@ -1307,9 +1267,7 @@ { "cell_type": "code", "execution_count": 21, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -1396,7 +1354,7 @@ "</svg>\n" ], "text/plain": [ - "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc79ce2e960> >" + "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd59c919ae0> >" ] }, "metadata": {}, @@ -1436,9 +1394,7 @@ { "cell_type": "code", "execution_count": 22, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -1520,7 +1476,7 @@ "</svg>\n" ], "text/plain": [ - "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc79ce55e10> >" + "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd59c951420> >" ] }, "metadata": {}, @@ -1546,9 +1502,7 @@ { "cell_type": "code", "execution_count": 23, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "name": "stdout", @@ -1581,9 +1535,7 @@ { "cell_type": "code", "execution_count": 24, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -1760,7 +1712,7 @@ "</svg>\n" ], "text/plain": [ - "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc79cdf1ba0> >" + "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd59c9199f0> >" ] }, "metadata": {}, @@ -1794,9 +1746,7 @@ { "cell_type": "code", "execution_count": 25, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -1825,9 +1775,7 @@ { "cell_type": "code", "execution_count": 26, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -2047,7 +1995,7 @@ "</svg>\n" ], "text/plain": [ - "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc79cdf1ba0> >" + "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd59c9199f0> >" ] }, "metadata": {}, @@ -2078,9 +2026,7 @@ { "cell_type": "code", "execution_count": 27, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -2107,619 +2053,88 @@ { "cell_type": "code", "execution_count": 28, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [], "source": [ - "import spot.gen as gen\n", - "\n", - "try:\n", - " import pandas\n", - "except ImportError:\n", - " import sys; sys.exit(77) # Our test suite will skip the rest if Pandas is missing" + "import spot.gen as gen" ] }, { "cell_type": "code", "execution_count": 29, "metadata": { - "collapsed": false, "scrolled": false }, "outputs": [ { - "data": { - "text/html": [ - "<div>\n", - "<style>\n", - " .dataframe thead tr:only-child th {\n", - " text-align: right;\n", - " }\n", - "\n", - " .dataframe thead th {\n", - " text-align: left;\n", - " }\n", - "\n", - " .dataframe tbody tr th {\n", - " vertical-align: top;\n", - " }\n", - "</style>\n", - "<table border=\"1\" class=\"dataframe\">\n", - " <thead>\n", - " <tr style=\"text-align: right;\">\n", - " <th></th>\n", - " <th>formula</th>\n", - " <th>states</th>\n", - " <th>SIstates</th>\n", - " <th>fwd_closed</th>\n", - " </tr>\n", - " </thead>\n", - " <tbody>\n", - " <tr>\n", - " <th>0</th>\n", - " <td>Fp0 -> (!p0 U (!p0 & p1 & X(!p0 U p2)))</td>\n", - " <td>3</td>\n", - " <td>2</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>1</th>\n", - " <td>Fp0 -> (!p1 U (p0 | (!p1 & p2 & X(!p1 U p3))))</td>\n", - " <td>4</td>\n", - " <td>3</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>2</th>\n", - " <td>G!p0 | (!p0 U ((p0 & Fp1) -> (!p1 U (!p1 & p2 ...</td>\n", - " <td>4</td>\n", - " <td>2</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>3</th>\n", - " <td>G((p0 & Fp1) -> (!p2 U (p1 | (!p2 & p3 & X(!p2...</td>\n", - " <td>4</td>\n", - " <td>1</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>4</th>\n", - " <td>G(p0 -> (Fp1 -> (!p1 U (p2 | (!p1 & p3 & X(!p1...</td>\n", - " <td>3</td>\n", - " <td>0</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>5</th>\n", - " <td>F(p0 & XFp1) -> (!p0 U p2)</td>\n", - " <td>3</td>\n", - " <td>2</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>6</th>\n", - " <td>Fp0 -> (!(!p0 & p1 & X(!p0 U (!p0 & p2))) U (p...</td>\n", - " <td>4</td>\n", - " <td>3</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>7</th>\n", - " <td>G!p0 | (!p0 U (p0 & (F(p1 & XFp2) -> (!p1 U p3...</td>\n", - " <td>4</td>\n", - " <td>2</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>8</th>\n", - " <td>G((p0 & Fp1) -> (!(!p1 & p2 & X(!p1 U (!p1 & p...</td>\n", - " <td>4</td>\n", - " <td>1</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>9</th>\n", - " <td>G(p0 -> ((!(!p1 & p2 & X(!p1 U (!p1 & p3))) U ...</td>\n", - " <td>3</td>\n", - " <td>0</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>10</th>\n", - " <td>G((p0 & XFp1) -> XF(p1 & Fp2))</td>\n", - " <td>6</td>\n", - " <td>1</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>11</th>\n", - " <td>Fp0 -> (((p1 & X(!p0 U p2)) -> X(!p0 U (p2 & F...</td>\n", - " <td>6</td>\n", - " <td>2</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>12</th>\n", - " <td>G(p0 -> G((p1 & XFp2) -> X(!p2 U (p2 & Fp3))))</td>\n", - " <td>5</td>\n", - " <td>0</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>13</th>\n", - " <td>G((p0 & Fp1) -> (((p2 & X(!p1 U p3)) -> X(!p1 ...</td>\n", - " <td>10</td>\n", - " <td>2</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>14</th>\n", - " <td>G(p0 -> (((p1 & X(!p2 U p3)) -> X(!p2 U (p3 & ...</td>\n", - " <td>10</td>\n", - " <td>0</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>15</th>\n", - " <td>G(p0 -> F(p1 & XFp2))</td>\n", - " <td>4</td>\n", - " <td>0</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>16</th>\n", - " <td>Fp0 -> ((p1 -> (!p0 U (!p0 & p2 & X(!p0 U p3))...</td>\n", - " <td>4</td>\n", - " <td>1</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>17</th>\n", - " <td>G(p0 -> G(p1 -> (p2 & XFp3)))</td>\n", - " <td>3</td>\n", - " <td>3</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>18</th>\n", - " <td>G((p0 & Fp1) -> ((p2 -> (!p1 U (!p1 & p3 & X(!...</td>\n", - " <td>4</td>\n", - " <td>0</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>19</th>\n", - " <td>G(p0 -> ((p1 -> (!p2 U (!p2 & p3 & X(!p2 U p4)...</td>\n", - " <td>6</td>\n", - " <td>2</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>20</th>\n", - " <td>G(p0 -> F(p1 & !p2 & X(!p2 U p3)))</td>\n", - " <td>4</td>\n", - " <td>0</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>21</th>\n", - " <td>Fp0 -> ((p1 -> (!p0 U (!p0 & p2 & !p3 & X((!p0...</td>\n", - " <td>4</td>\n", - " <td>1</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>22</th>\n", - " <td>G(p0 -> G(p1 -> (p2 & !p3 & X(!p3 U p4))))</td>\n", - " <td>3</td>\n", - " <td>3</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>23</th>\n", - " <td>G((p0 & Fp1) -> ((p2 -> (!p1 U (!p1 & p3 & !p4...</td>\n", - " <td>4</td>\n", - " <td>0</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>24</th>\n", - " <td>G(p0 -> ((p1 -> (!p2 U (!p2 & p3 & !p4 & X((!p...</td>\n", - " <td>6</td>\n", - " <td>2</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>25</th>\n", - " <td>p0 U (p1 & X(p2 U p3))</td>\n", - " <td>3</td>\n", - " <td>2</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>26</th>\n", - " <td>p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6)...</td>\n", - " <td>7</td>\n", - " <td>2</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>27</th>\n", - " <td>F(p0 & XGp1)</td>\n", - " <td>2</td>\n", - " <td>2</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>28</th>\n", - " <td>F(p0 & X(p1 & XFp2))</td>\n", - " <td>4</td>\n", - " <td>2</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>29</th>\n", - " <td>F(p0 & X(p1 U p2))</td>\n", - " <td>3</td>\n", - " <td>1</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>...</th>\n", - " <td>...</td>\n", - " <td>...</td>\n", - " <td>...</td>\n", - " <td>...</td>\n", - " </tr>\n", - " <tr>\n", - " <th>33</th>\n", - " <td>G((p0 & p1 & !p2 & Xp2) -> X(p3 | X(!p1 | p3)))</td>\n", - " <td>3</td>\n", - " <td>0</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>34</th>\n", - " <td>G((p0 & p1 & !p2 & Xp2) -> X(X!p1 | (p2 U (!p2...</td>\n", - " <td>5</td>\n", - " <td>5</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>35</th>\n", - " <td>G(p0 & p1 & !p2 & Xp2) -> X(X!p1 | (p2 U (!p2 ...</td>\n", - " <td>1</td>\n", - " <td>1</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>36</th>\n", - " <td>G((!p0 & p1) -> Xp2)</td>\n", - " <td>2</td>\n", - " <td>0</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>37</th>\n", - " <td>G(p0 -> X(p0 | p1))</td>\n", - " <td>2</td>\n", - " <td>2</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>38</th>\n", - " <td>G((!(p1 <-> Xp1) | !(p0 <-> Xp0) | !(p2 <-> Xp...</td>\n", - " <td>34</td>\n", - " <td>34</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>39</th>\n", - " <td>G((p0 & !p1 & Xp1 & Xp0) -> (p2 -> Xp3))</td>\n", - " <td>2</td>\n", - " <td>2</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>40</th>\n", - " <td>G(p0 -> X(!p0 U p1))</td>\n", - " <td>2</td>\n", - " <td>0</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>41</th>\n", - " <td>G((!p0 & Xp0) -> X((p0 U p1) | Gp0))</td>\n", - " <td>3</td>\n", - " <td>3</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>42</th>\n", - " <td>G((!p0 & Xp0) -> X(p0 U (p0 & !p1 & X(p0 & p1))))</td>\n", - " <td>4</td>\n", - " <td>4</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>43</th>\n", - " <td>G((!p0 & Xp0) -> X(p0 U (p0 & !p1 & X(p0 & p1 ...</td>\n", - " <td>6</td>\n", - " <td>6</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>44</th>\n", - " <td>G((p0 & X!p0) -> X(!p0 U (!p0 & !p1 & X(!p0 & ...</td>\n", - " <td>6</td>\n", - " <td>6</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>45</th>\n", - " <td>G((p0 & X!p0) -> X(!p0 U (!p0 & !p1 & X(!p0 & ...</td>\n", - " <td>8</td>\n", - " <td>8</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>46</th>\n", - " <td>G((!p0 & Xp0) -> X(!(!p0 & Xp0) U (!p1 & Xp1)))</td>\n", - " <td>6</td>\n", - " <td>6</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>47</th>\n", - " <td>G(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 ...</td>\n", - " <td>12</td>\n", - " <td>0</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>48</th>\n", - " <td>G((Xp0 -> p0) -> (p1 <-> Xp1))</td>\n", - " <td>4</td>\n", - " <td>4</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>49</th>\n", - " <td>G((Xp0 -> p0) -> ((p1 -> Xp1) & (!p1 -> X!p1)))</td>\n", - " <td>4</td>\n", - " <td>4</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>50</th>\n", - " <td>p0 & XG!p0</td>\n", - " <td>2</td>\n", - " <td>1</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>51</th>\n", - " <td>XG(p0 -> (G!p1 | (!Xp1 U p2)))</td>\n", - " <td>4</td>\n", - " <td>1</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>52</th>\n", - " <td>XG((p0 & !p1) -> (G!p1 | (!p1 U p2)))</td>\n", - " <td>3</td>\n", - " <td>2</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>53</th>\n", - " <td>XG((p0 & p1) -> (Gp1 | (p1 U p2)))</td>\n", - " <td>3</td>\n", - " <td>2</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>54</th>\n", - " <td>Xp0 & G((!p0 & Xp0) -> XXp0)</td>\n", - " <td>5</td>\n", - " <td>0</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>55</th>\n", - " <td>(Xp0 U Xp1) | !X(p0 U p1)</td>\n", - " <td>1</td>\n", - " <td>1</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>56</th>\n", - " <td>(Xp0 U p1) | !X(p0 U (p0 & p1))</td>\n", - " <td>1</td>\n", - " <td>1</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>57</th>\n", - " <td>((Xp0 U p1) | !X(p0 U (p0 & p1))) & G(p0 -> Fp1)</td>\n", - " <td>2</td>\n", - " <td>2</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>58</th>\n", - " <td>((Xp0 U Xp1) | !X(p0 U p1)) & G(p0 -> Fp1)</td>\n", - " <td>2</td>\n", - " <td>2</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>59</th>\n", - " <td>!G(p0 -> X(p1 R p2))</td>\n", - " <td>3</td>\n", - " <td>1</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>60</th>\n", - " <td>(p0 & Xp1) R X(((p2 U p3) R p0) U (p2 R p0))</td>\n", - " <td>5</td>\n", - " <td>3</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>61</th>\n", - " <td>G(p0 | XGp1) & G(p2 | XG!p1)</td>\n", - " <td>3</td>\n", - " <td>2</td>\n", - " <td>True</td>\n", - " </tr>\n", - " <tr>\n", - " <th>62</th>\n", - " <td>G(p0 | (Xp1 & X!p1))</td>\n", - " <td>1</td>\n", - " <td>1</td>\n", - " <td>True</td>\n", - " </tr>\n", - " </tbody>\n", - "</table>\n", - "<p>63 rows × 4 columns</p>\n", - "</div>" - ], - "text/plain": [ - " formula states SIstates \\\n", - "0 Fp0 -> (!p0 U (!p0 & p1 & X(!p0 U p2))) 3 2 \n", - "1 Fp0 -> (!p1 U (p0 | (!p1 & p2 & X(!p1 U p3)))) 4 3 \n", - "2 G!p0 | (!p0 U ((p0 & Fp1) -> (!p1 U (!p1 & p2 ... 4 2 \n", - "3 G((p0 & Fp1) -> (!p2 U (p1 | (!p2 & p3 & X(!p2... 4 1 \n", - "4 G(p0 -> (Fp1 -> (!p1 U (p2 | (!p1 & p3 & X(!p1... 3 0 \n", - "5 F(p0 & XFp1) -> (!p0 U p2) 3 2 \n", - "6 Fp0 -> (!(!p0 & p1 & X(!p0 U (!p0 & p2))) U (p... 4 3 \n", - "7 G!p0 | (!p0 U (p0 & (F(p1 & XFp2) -> (!p1 U p3... 4 2 \n", - "8 G((p0 & Fp1) -> (!(!p1 & p2 & X(!p1 U (!p1 & p... 4 1 \n", - "9 G(p0 -> ((!(!p1 & p2 & X(!p1 U (!p1 & p3))) U ... 3 0 \n", - "10 G((p0 & XFp1) -> XF(p1 & Fp2)) 6 1 \n", - "11 Fp0 -> (((p1 & X(!p0 U p2)) -> X(!p0 U (p2 & F... 6 2 \n", - "12 G(p0 -> G((p1 & XFp2) -> X(!p2 U (p2 & Fp3)))) 5 0 \n", - "13 G((p0 & Fp1) -> (((p2 & X(!p1 U p3)) -> X(!p1 ... 10 2 \n", - "14 G(p0 -> (((p1 & X(!p2 U p3)) -> X(!p2 U (p3 & ... 10 0 \n", - "15 G(p0 -> F(p1 & XFp2)) 4 0 \n", - "16 Fp0 -> ((p1 -> (!p0 U (!p0 & p2 & X(!p0 U p3))... 4 1 \n", - "17 G(p0 -> G(p1 -> (p2 & XFp3))) 3 3 \n", - "18 G((p0 & Fp1) -> ((p2 -> (!p1 U (!p1 & p3 & X(!... 4 0 \n", - "19 G(p0 -> ((p1 -> (!p2 U (!p2 & p3 & X(!p2 U p4)... 6 2 \n", - "20 G(p0 -> F(p1 & !p2 & X(!p2 U p3))) 4 0 \n", - "21 Fp0 -> ((p1 -> (!p0 U (!p0 & p2 & !p3 & X((!p0... 4 1 \n", - "22 G(p0 -> G(p1 -> (p2 & !p3 & X(!p3 U p4)))) 3 3 \n", - "23 G((p0 & Fp1) -> ((p2 -> (!p1 U (!p1 & p3 & !p4... 4 0 \n", - "24 G(p0 -> ((p1 -> (!p2 U (!p2 & p3 & !p4 & X((!p... 6 2 \n", - "25 p0 U (p1 & X(p2 U p3)) 3 2 \n", - "26 p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6)... 7 2 \n", - "27 F(p0 & XGp1) 2 2 \n", - "28 F(p0 & X(p1 & XFp2)) 4 2 \n", - "29 F(p0 & X(p1 U p2)) 3 1 \n", - ".. ... ... ... \n", - "33 G((p0 & p1 & !p2 & Xp2) -> X(p3 | X(!p1 | p3))) 3 0 \n", - "34 G((p0 & p1 & !p2 & Xp2) -> X(X!p1 | (p2 U (!p2... 5 5 \n", - "35 G(p0 & p1 & !p2 & Xp2) -> X(X!p1 | (p2 U (!p2 ... 1 1 \n", - "36 G((!p0 & p1) -> Xp2) 2 0 \n", - "37 G(p0 -> X(p0 | p1)) 2 2 \n", - "38 G((!(p1 <-> Xp1) | !(p0 <-> Xp0) | !(p2 <-> Xp... 34 34 \n", - "39 G((p0 & !p1 & Xp1 & Xp0) -> (p2 -> Xp3)) 2 2 \n", - "40 G(p0 -> X(!p0 U p1)) 2 0 \n", - "41 G((!p0 & Xp0) -> X((p0 U p1) | Gp0)) 3 3 \n", - "42 G((!p0 & Xp0) -> X(p0 U (p0 & !p1 & X(p0 & p1)))) 4 4 \n", - "43 G((!p0 & Xp0) -> X(p0 U (p0 & !p1 & X(p0 & p1 ... 6 6 \n", - "44 G((p0 & X!p0) -> X(!p0 U (!p0 & !p1 & X(!p0 & ... 6 6 \n", - "45 G((p0 & X!p0) -> X(!p0 U (!p0 & !p1 & X(!p0 & ... 8 8 \n", - "46 G((!p0 & Xp0) -> X(!(!p0 & Xp0) U (!p1 & Xp1))) 6 6 \n", - "47 G(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 ... 12 0 \n", - "48 G((Xp0 -> p0) -> (p1 <-> Xp1)) 4 4 \n", - "49 G((Xp0 -> p0) -> ((p1 -> Xp1) & (!p1 -> X!p1))) 4 4 \n", - "50 p0 & XG!p0 2 1 \n", - "51 XG(p0 -> (G!p1 | (!Xp1 U p2))) 4 1 \n", - "52 XG((p0 & !p1) -> (G!p1 | (!p1 U p2))) 3 2 \n", - "53 XG((p0 & p1) -> (Gp1 | (p1 U p2))) 3 2 \n", - "54 Xp0 & G((!p0 & Xp0) -> XXp0) 5 0 \n", - "55 (Xp0 U Xp1) | !X(p0 U p1) 1 1 \n", - "56 (Xp0 U p1) | !X(p0 U (p0 & p1)) 1 1 \n", - "57 ((Xp0 U p1) | !X(p0 U (p0 & p1))) & G(p0 -> Fp1) 2 2 \n", - "58 ((Xp0 U Xp1) | !X(p0 U p1)) & G(p0 -> Fp1) 2 2 \n", - "59 !G(p0 -> X(p1 R p2)) 3 1 \n", - "60 (p0 & Xp1) R X(((p2 U p3) R p0) U (p2 R p0)) 5 3 \n", - "61 G(p0 | XGp1) & G(p2 | XG!p1) 3 2 \n", - "62 G(p0 | (Xp1 & X!p1)) 1 1 \n", - "\n", - " fwd_closed \n", - "0 True \n", - "1 True \n", - "2 True \n", - "3 True \n", - "4 True \n", - "5 True \n", - "6 True \n", - "7 True \n", - "8 True \n", - "9 True \n", - "10 True \n", - "11 True \n", - "12 True \n", - "13 True \n", - "14 True \n", - "15 True \n", - "16 True \n", - "17 True \n", - "18 True \n", - "19 True \n", - "20 True \n", - "21 True \n", - "22 True \n", - "23 True \n", - "24 True \n", - "25 True \n", - "26 True \n", - "27 True \n", - "28 True \n", - "29 True \n", - ".. ... \n", - "33 True \n", - "34 True \n", - "35 True \n", - "36 True \n", - "37 True \n", - "38 True \n", - "39 True \n", - "40 True \n", - "41 True \n", - "42 True \n", - "43 True \n", - "44 True \n", - "45 True \n", - "46 True \n", - "47 True \n", - "48 True \n", - "49 True \n", - "50 True \n", - "51 True \n", - "52 True \n", - "53 True \n", - "54 True \n", - "55 True \n", - "56 True \n", - "57 True \n", - "58 True \n", - "59 True \n", - "60 True \n", - "61 True \n", - "62 True \n", - "\n", - "[63 rows x 4 columns]" - ] - }, - "metadata": {}, - "output_type": "display_data" + "name": "stdout", + "output_type": "stream", + "text": [ + "formula states SIstates fwd_closed\n", + "(p1 & X(!p0 U p2)) R !p0 3 2 1\n", + "(!p1 U (p0 | (!p1 & p2 & X(!p1 U p3)))) 4 3 1\n", + "!p0 | ((p2 & X(!p1 U p3)) R !p1) 4 2 1\n", + "G(!p0 | (!p2 U (p1 | (!p2 & p3 & X(!p2 U 4 1 1\n", + "G(!p0 | (!p1 W (p2 | (!p1 & p3 & X(!p1 U 3 0 1\n", + "(!p0 U p2) | G(!p0 | XG!p1) 3 2 1\n", + "G!p0 | ((p0 | !p1 | X(!p2 W p0)) U (p0 | 4 3 1\n", + "!p0 W (p0 & ((!p1 U p3) | G(!p1 | XG!p2) 4 2 1\n", + "G(!p0 | G!p1 | ((p1 | !p2 | X(!p3 W p1)) 4 1 1\n", + "G(!p0 | ((p1 | !p2 | X(!p3 W p1)) U (p1 3 0 1\n", + "G(!p0 | X(F(p1 & Fp2) | G!p1)) 6 1 1\n", + "G!p0 | ((!p1 | X((!p0 U (p2 & Fp3)) | (p 6 2 1\n", + "G(!p0 | G(!p1 | X(!p2 W (p2 & Fp3)))) 5 0 1\n", + "G(!p0 | G!p1 | ((!p2 | X((!p1 U (p3 & Fp 10 2 1\n", + "G(!p0 | ((!p1 | X((!p2 U (p3 & Fp4)) | ( 10 0 1\n", + "G(!p0 | F(p1 & XFp2)) 4 0 1\n", + "G!p0 | ((!p1 | ((p2 & X(!p0 U p3)) M !p0 4 1 1\n", + "G(!p0 | G(!p1 | (p2 & XFp3))) 3 3 1\n", + "G(!p0 | G!p1 | ((!p2 | ((p3 & X(!p1 U p4 4 0 1\n", + "G(!p0 | ((!p1 | ((p3 & X(!p2 U p4)) M !p 6 2 1\n", + "G(!p0 | F(p1 & !p2 & X(!p2 U p3))) 4 0 1\n", + "G!p0 | ((!p1 | ((p2 & !p3 & X((!p0 & !p3 4 1 1\n", + "G(!p0 | G(!p1 | (p2 & !p3 & X(!p3 U p4)) 3 3 1\n", + "G(!p0 | G!p1 | ((!p2 | ((p3 & !p4 & X((! 4 0 1\n", + "G(!p0 | ((!p1 | ((p3 & !p4 & X((!p2 & !p 6 2 1\n", + "p0 U (p1 & X(p2 U p3)) 3 2 1\n", + "p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & 7 2 1\n", + "F(p0 & XGp1) 2 2 1\n", + "F(p0 & X(p1 & XFp2)) 4 2 1\n", + "F(p0 & X(p1 U p2)) 3 1 1\n", + "G(p0 & Fp1 & Fp2 & Fp3) 1 1 1\n", + "GF((!p0 & Xp0) | (p0 & X!p0) | (!p1 & Xp 5 5 1\n", + "GF((!p0 & Xp0) | (p0 & X!p0) | (!p1 & Xp 9 9 1\n", + "G(!p0 | !p1 | p2 | X(!p2 | p3 | X(!p1 | 3 0 1\n", + "G(!p0 | !p1 | p2 | X(!p2 | (p2 U (!p2 U 5 5 1\n", + "1 1 1 1\n", + "G(p0 | !p1 | Xp2) 2 0 1\n", + "G(!p0 | X(p0 | p1)) 2 2 1\n", + "G((((p1 & Xp1) | (!p1 & X!p1)) & ((p0 & 34 34 1\n", + "G(!p0 | p1 | !p2 | X(!p0 | !p1 | p3)) 2 2 1\n", + "G(!p0 | X(!p0 U p1)) 2 0 1\n", + "G(p0 | X(!p0 | (p0 W p1))) 3 3 1\n", + "G(p0 | X(!p0 | ((!p1 & X(p0 & p1)) M p0) 4 4 1\n", + "G(p0 | X(!p0 | ((!p1 & X(p1 & ((!p1 & X( 6 6 1\n", + "G(!p0 | X(p0 | ((!p1 & X(p1 & ((!p1 & X( 6 6 1\n", + "G(!p0 | X(p0 | ((!p1 & X(p1 & ((!p1 & X( 8 8 1\n", + "G(p0 | X(!p0 | ((p0 | X!p0) U (!p1 & Xp1 6 6 1\n", + "G(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 | 12 0 1\n", + "G((!p0 & Xp0) | (p1 & Xp1) | (!p1 & X!p1 4 4 1\n", + "G((!p0 & Xp0) | ((!p1 | Xp1) & (p1 | X!p 4 4 1\n", + "p0 & XG!p0 2 1 1\n", + "XG(!p0 | p2 | G!p1 | X(p2 M !p1)) 4 1 1\n", + "XG(!p0 | p1 | (!p1 W p2)) 3 2 1\n", + "XG(!p0 | !p1 | (p1 W p2)) 3 2 1\n", + "Xp0 & G(p0 | X(!p0 | Xp0)) 5 0 1\n", + "1 1 1 1\n", + "1 1 1 1\n", + "G(!p0 | Fp1) 2 2 1\n", + "G(!p0 | Fp1) 2 2 1\n", + "F(p0 & X(!p1 U !p2)) 3 1 1\n", + "(p0 & Xp1) R X(p2 R p0) 5 3 1\n", + "G((p0 | XGp1) & (p2 | XG!p1)) 3 2 1\n", + "Gp0 1 1 1\n" + ] } ], "source": [ @@ -2732,23 +2147,21 @@ " gen.LTL_SB_PATTERNS)\n", " if not f.is_syntactic_stutter_invariant() ]\n", "\n", - "fmt_txt = []\n", "aut_size = []\n", "sistates_size = []\n", "fwd_closed = []\n", "\n", + "fmt = \"{:40.40} {:>6} {:>8} {:>10}\"\n", + "print(fmt.format(\"formula\", \"states\", \"SIstates\", \"fwd_closed\"))\n", "for f in formulas:\n", - " fmt_txt.append(f.to_str())\n", " aut = spot.translate(f)\n", " aut_size.append(aut.num_states())\n", " sistates = spot.stutter_invariant_states(aut, f)\n", - " sistates_size.append(sum(sistates))\n", - " fwd_closed.append(spot.is_stutter_invariant_forward_closed(aut, sistates) == -1)\n", - " \n", - "# Put everything in a data frame for display.\n", - "df = pandas.DataFrame({'formula': fmt_txt, 'states': aut_size, 'SIstates': sistates_size, 'fwd_closed': fwd_closed},\n", - " columns=['formula','states','SIstates','fwd_closed'])\n", - "display(df)" + " sisz = sum(sistates)\n", + " sistates_size.append(sisz)\n", + " fc = spot.is_stutter_invariant_forward_closed(aut, sistates) == -1\n", + " fwd_closed.append(fc)\n", + " print(fmt.format(f.to_str(), aut.num_states(), sisz, fc))" ] }, { @@ -2761,9 +2174,7 @@ { "cell_type": "code", "execution_count": 30, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -2790,9 +2201,7 @@ { "cell_type": "code", "execution_count": 31, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -2808,6 +2217,13 @@ "source": [ "100*sum(sistates_size)/sum(aut_size)" ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": { @@ -2826,7 +2242,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.4rc1" + "version": "3.6.4" } }, "nbformat": 4,