diff --git a/spot/twaalgos/stutter.cc b/spot/twaalgos/stutter.cc index 579651738..1af7880f2 100644 --- a/spot/twaalgos/stutter.cc +++ b/spot/twaalgos/stutter.cc @@ -869,4 +869,123 @@ namespace spot { highlight_vector(pos, stutter_invariant_states(pos, neg), color); } + + + namespace + { + [[noreturn]] static void sistates_has_wrong_size(const char* fun) + { + throw std::runtime_error(std::string(fun) + + "(): vector size should match " + "the number of states"); + } + } + + int + is_stutter_invariant_forward_closed(twa_graph_ptr aut, + const std::vector& sistates) + { + unsigned ns = aut->num_states(); + if (SPOT_UNLIKELY(sistates.size() != ns)) + sistates_has_wrong_size("is_stutter_invariant_forward_closed"); + for (unsigned s = 0; s < ns; ++s) + { + if (!sistates[s]) + continue; + for (auto& e : aut->out(s)) + { + if (!sistates[e.dst]) + return e.dst; + } + } + return -1; + } + + std::vector + make_stutter_invariant_forward_closed_inplace + (twa_graph_ptr aut, const std::vector& sistates) + { + unsigned ns = aut->num_states(); + if (SPOT_UNLIKELY(sistates.size() != ns)) + sistates_has_wrong_size("make_stutter_invariant_forward_closed_inplace"); + // Find the set of SI states that can jump into non-SI states. + std::vector seed_states; + bool pb = false; + for (unsigned s = 0; s < ns; ++s) + { + if (!sistates[s]) + continue; + for (auto& e : aut->out(s)) + if (!sistates[e.dst]) + { + seed_states.push_back(s); + pb = true; + break; + } + } + if (!pb) // Nothing to change + return sistates; + + // Find the set of non-SI states that are reachable from a seed + // state, and give each of them a new number. + std::vector new_number(ns, 0); + std::vector prob_states; + prob_states.reserve(ns); + unsigned base = ns; + std::vector dfs; + dfs.reserve(ns); + for (unsigned pb: seed_states) + { + dfs.push_back(pb); + while (!dfs.empty()) + { + unsigned src = dfs.back(); + dfs.pop_back(); + for (auto& e: aut->out(src)) + { + unsigned dst = e.dst; + if (sistates[dst] || new_number[dst]) + continue; + new_number[dst] = base++; + dfs.push_back(dst); + prob_states.push_back(dst); + } + } + } + + // Actually duplicate the problematic states + assert(base > ns); + aut->new_states(base - ns); + assert(aut->num_states() == base); + for (unsigned ds: prob_states) + { + unsigned new_src = new_number[ds]; + assert(new_src > 0); + for (auto& e: aut->out(ds)) + { + unsigned dst = new_number[e.dst]; + if (!dst) + dst = e.dst; + aut->new_edge(new_src, dst, e.cond, e.acc); + } + } + + // Redirect the transition coming out of the seed states + // to the duplicate state. + for (unsigned pb: seed_states) + for (auto& e: aut->out(pb)) + { + unsigned ndst = new_number[e.dst]; + if (ndst) + e.dst = ndst; + } + + // Create a new SI-state vector. + std::vector new_sistates; + new_sistates.reserve(base); + new_sistates.insert(new_sistates.end(), sistates.begin(), sistates.end()); + new_sistates.insert(new_sistates.end(), base - ns, true); + return new_sistates; + } + } diff --git a/spot/twaalgos/stutter.hh b/spot/twaalgos/stutter.hh index f8576ec9b..cbb40c6b6 100644 --- a/spot/twaalgos/stutter.hh +++ b/spot/twaalgos/stutter.hh @@ -270,4 +270,43 @@ namespace spot SPOT_API std::vector stutter_invariant_letters(const_twa_graph_ptr pos, formula f_pos); /// @} + + + /// \ingroup stutter_inv + /// \brief Test if the set of stutter-invariant states is + /// forward-closed. + /// + /// Test if the set of states returned by + /// spot::stutter_invariant_states() is closed by the successor + /// relation. I.e., the successor of an SI-state is an SI-state. + /// + /// This function returns -1 is \a sistates is forward closed, or it + /// will return the number of a state that is not an SI-state but + /// has a predecessor that is an SI-state. + /// + /// The \a sistate vector should be a vector computed for \a aut + /// using spot::stutter_invariant_states(). + SPOT_API int + is_stutter_invariant_forward_closed(twa_graph_ptr aut, + const std::vector& sistates); + + /// \ingroup stutter_inv + /// \brief Change the automaton so its set of stutter-invariant + /// state is forward-closed. + /// + /// \see spot::is_stutter_invariant_forward_closed() + /// + /// The \a sistate vector should be a vector computed for \a aut + /// using spot::stutter_invariant_states(). The automaton \a aut + /// will be fixed in place by duplicating problematic states, and an + /// updated copy of the \a sistates vector will be returned. + /// + /// This function will detect the cases where not change to \a aut + /// is necessary at a cost that is very close to + /// spot::is_stutter_invariant_forward_closed(), so calling this last + /// function first is useless. + SPOT_API std::vector + make_stutter_invariant_forward_closed_inplace + (twa_graph_ptr aut, const std::vector& sistates); + } diff --git a/tests/python/stutter-inv.ipynb b/tests/python/stutter-inv.ipynb index b1373a9db..756baf59f 100644 --- a/tests/python/stutter-inv.ipynb +++ b/tests/python/stutter-inv.ipynb @@ -15,7 +15,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.3" + "version": "3.6.4rc1" }, "name": "" }, @@ -354,7 +354,7 @@ "\n" ], "text": [ - " *' at 0x7f399007b4b0> >" + " *' at 0x7fc79ce55870> >" ] }, { @@ -626,7 +626,7 @@ "\n" ], "text": [ - " *' at 0x7f399007b660> >" + " *' at 0x7fc79ce2e900> >" ] } ], @@ -638,7 +638,7 @@ "source": [ "While the automaton as a whole is stutter-sensitive, we can see that eventually we will enter a sub-automaton that is stutter-invariant.\n", "\n", - "The `stutter_invariant_states()` function returns a Boolean vector indiced by the state number. A state is marked as `True` if either its language is stutter-invariant, or if it appear below a stutter-invariant state (see the second example later). As always, the second argument, `f`, can be omitted (pass `None`) if the formula is unknown, or it can be replaced by a negated automaton if it is known. " + "The `stutter_invariant_states()` function returns a Boolean vector indiced by the state number. A state is marked as `True` if either its language is stutter-invariant, or if it can only be reached via a stutter-invariant state (see the second example later). As always, the second argument, `f`, can be omitted (pass `None`) if the formula is unknown, or it can be replaced by a negated automaton if it is known. " ] }, { @@ -816,7 +816,7 @@ "\n" ], "text": [ - " *' at 0x7f399007b660> >" + " *' at 0x7fc79ce2e900> >" ] } ], @@ -979,7 +979,7 @@ "\n" ], "text": [ - " *' at 0x7f3981fdfab0> >" + " *' at 0x7fc79ce2e8d0> >" ] }, { @@ -1066,7 +1066,7 @@ "\n" ], "text": [ - " *' at 0x7f3981fdfa20> >" + " *' at 0x7fc79ce61d50> >" ] } ], @@ -1076,7 +1076,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "Now we build the sum of these to automata. The stutter-invariance check detects that the initial state is stutter-invariant (i.e., the entire language is stutter-invariant) so all states below it are marked despite the fact that the language recognized from these individual states would not be stutter-invariant." + "Now we build the sum of these two automata. The stutter-invariance check detects that the initial state is stutter-invariant (i.e., the entire language is stutter-invariant) so all states below it are marked despite the fact that the language recognized from these individual states would not be stutter-invariant." ] }, { @@ -1090,7 +1090,9 @@ "display(aut)\n", "# The stutter_invariant property is set on AUT as a side effect\n", "# of calling sutter_invariant_states() or any variant of it.\n", - "assert(aut.prop_stutter_invariant().is_true())" + "assert(aut.prop_stutter_invariant().is_true())\n", + "\n", + "print(aut.to_str())" ], "language": "python", "metadata": {}, @@ -1260,7 +1262,43 @@ "\n" ], "text": [ - " *' at 0x7f3981fdfba0> >" + " *' at 0x7fc79ce2ea50> >" + ] + }, + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "HOA: v1\n", + "States: 6\n", + "Start: 5\n", + "AP: 1 \"a\"\n", + "Acceptance: 3 (Inf(0)&Inf(1)) | Inf(2)\n", + "properties: trans-labels explicit-labels trans-acc stutter-invariant\n", + "--BODY--\n", + "State: 0\n", + "[!0] 0 {1}\n", + "[0] 0\n", + "[0] 1 {0}\n", + "State: 1\n", + "[0] 0\n", + "[0] 1 {0}\n", + "State: 2\n", + "[t] 2\n", + "[!0] 3\n", + "[0] 4\n", + "State: 3\n", + "[!0] 3 {2}\n", + "[0] 4 {2}\n", + "State: 4\n", + "[!0] 3 {2}\n", + "State: 5\n", + "[!0] 3\n", + "[0] 1\n", + "[0] 4\n", + "[t] 0\n", + "[t] 2\n", + "--END--\n" ] } ], @@ -1374,7 +1412,7 @@ "\n" ], "text": [ - " *' at 0x7f3981fdf390> >" + " *' at 0x7fc79ce2e960> >" ] } ], @@ -1497,7 +1535,7 @@ "\n" ], "text": [ - " *' at 0x7f3981fdfa80> >" + " *' at 0x7fc79ce55e10> >" ] } ], @@ -1535,6 +1573,1235 @@ } ], "prompt_number": 23 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## The set of stutter-invariant states is not always forward closed\n", + "\n", + "Consider the following automaton, which is a variant of our second example above. \n", + "\n", + "The language accepted from state (2) is `!GF(a & Xa) & GF!a` (this can be simplified to `FG(!a | X!a)`), while the language accepted from state (0) is `GF(a & Xa) & GF!a`. Therefore. the language accepted from state (5) is `a & X(GF!a)`. Since this is equivalent to `a & GF(!a)` state (5) recognizes stutter-invariant language, but as we can see, it is not the case that all states below (5) are also marked. In fact, states (0) can also be reached via states (7) and (6), recognizing respectively `(a & X(a & GF!a)) | (!a & X(!a & GF(a & Xa) & GF!a))` and `!a & GF(a & Xa) & GF!a))`, i.e., two stutter-sentive languages." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "ex1 = spot.automaton(\"\"\"HOA: v1 \n", + "States: 8 Start: 7 AP: 1 \"a\" Acceptance: 2 (Inf(0)&Inf(1))\n", + "--BODY--\n", + "State: 0 [!0] 0 {1} [0] 0 [0] 1 {0}\n", + "State: 1 [0] 0 [0] 1 {0}\n", + "State: 2 [t] 2 [!0] 3 [0] 4\n", + "State: 3 [!0] 3 {0 1} [0] 4 {0 1}\n", + "State: 4 [!0] 3 {0 1}\n", + "State: 5 [0] 0 [0] 2\n", + "State: 6 [!0] 0\n", + "State: 7 [!0] 6 [0] 5\n", + "--END--\"\"\")\n", + "spot.highlight_stutter_invariant_states(ex1,None, 5)\n", + "display(ex1)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")&Inf(\n", + "\u2776\n", + ")\n", + "[gen. B\u00fcchi 2]\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "I->7\n", + "\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "7->5\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "7->6\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a\n", + "\u2776\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\u24ff\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", + "\u24ff\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "a\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "5->0\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "5->2\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "6->0\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7fc79cdf1ba0> >" + ] + } + ], + "prompt_number": 24 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "This situation can be tested with `spot.is_stutter_invariant_forward_closed()`. The function returns `-1` if the successor of any stutter-invariant state is it is also a stutter-invariant state, otherwise it return the number of one stutter-sensitive state that has a stutter-invariant state as predecessor." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "sistates = spot.stutter_invariant_states(ex1)\n", + "spot.is_stutter_invariant_forward_closed(ex1, sistates)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 25, + "text": [ + "0" + ] + } + ], + "prompt_number": 25 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "In cases where we prefer to have a forward-closed set of stutter-invariant states, it is always possible to duplicate\n", + "the problematic states. The `make_stutter_invariant_foward_closed_inplace()` modifies the automaton in place, and also returns an updated copie of the vector of stutter-invariant states." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "sistates2 = spot.make_stutter_invariant_forward_closed_inplace(ex1, sistates)\n", + "spot.highlight_stutter_invariant_states(ex1, None, 5)\n", + "display(ex1)\n", + "print(sistates2)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")&Inf(\n", + "\u2776\n", + ")\n", + "[gen. B\u00fcchi 2]\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "I->7\n", + "\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "7->5\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "7->6\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a\n", + "\u2776\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\u24ff\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", + "\u24ff\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "a\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "5->2\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "8\n", + "\n", + "8\n", + "\n", + "\n", + "5->8\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "8->8\n", + "\n", + "\n", + "!a\n", + "\u2776\n", + "\n", + "\n", + "8->8\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "9\n", + "\n", + "9\n", + "\n", + "\n", + "8->9\n", + "\n", + "\n", + "a\n", + "\u24ff\n", + "\n", + "\n", + "6->0\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "9->8\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "9->9\n", + "\n", + "\n", + "a\n", + "\u24ff\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7fc79cdf1ba0> >" + ] + }, + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "(False, False, True, True, True, True, False, False, True, True)\n" + ] + } + ], + "prompt_number": 26 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Now, state 0 is no longuer a problem." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "spot.is_stutter_invariant_forward_closed(ex1, sistates2)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 27, + "text": [ + "-1" + ] + } + ], + "prompt_number": 27 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Let's see how infrequently the set of stutter-invarant states is not closed." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "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" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 28 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "# Let's consider the LTL formula from the following 5 sources,\n", + "# and restrict ourselves to formulas that are not stutter-invariant.\n", + "formulas = [ f for f in gen.ltl_patterns(gen.LTL_DAC_PATTERNS, \n", + " gen.LTL_EH_PATTERNS, \n", + " gen.LTL_HKRSS_PATTERNS, \n", + " gen.LTL_P_PATTERNS, \n", + " 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", + "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)" + ], + "language": "python", + "metadata": { + "scrolled": false + }, + "outputs": [ + { + "html": [ + "
\n", + "\n", + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
formulastatesSIstatesfwd_closed
0Fp0 -> (!p0 U (!p0 & p1 & X(!p0 U p2)))32True
1Fp0 -> (!p1 U (p0 | (!p1 & p2 & X(!p1 U p3))))43True
2G!p0 | (!p0 U ((p0 & Fp1) -> (!p1 U (!p1 & p2 ...42True
3G((p0 & Fp1) -> (!p2 U (p1 | (!p2 & p3 & X(!p2...41True
4G(p0 -> (Fp1 -> (!p1 U (p2 | (!p1 & p3 & X(!p1...30True
5F(p0 & XFp1) -> (!p0 U p2)32True
6Fp0 -> (!(!p0 & p1 & X(!p0 U (!p0 & p2))) U (p...43True
7G!p0 | (!p0 U (p0 & (F(p1 & XFp2) -> (!p1 U p3...42True
8G((p0 & Fp1) -> (!(!p1 & p2 & X(!p1 U (!p1 & p...41True
9G(p0 -> ((!(!p1 & p2 & X(!p1 U (!p1 & p3))) U ...30True
10G((p0 & XFp1) -> XF(p1 & Fp2))61True
11Fp0 -> (((p1 & X(!p0 U p2)) -> X(!p0 U (p2 & F...62True
12G(p0 -> G((p1 & XFp2) -> X(!p2 U (p2 & Fp3))))50True
13G((p0 & Fp1) -> (((p2 & X(!p1 U p3)) -> X(!p1 ...102True
14G(p0 -> (((p1 & X(!p2 U p3)) -> X(!p2 U (p3 & ...100True
15G(p0 -> F(p1 & XFp2))40True
16Fp0 -> ((p1 -> (!p0 U (!p0 & p2 & X(!p0 U p3))...41True
17G(p0 -> G(p1 -> (p2 & XFp3)))33True
18G((p0 & Fp1) -> ((p2 -> (!p1 U (!p1 & p3 & X(!...40True
19G(p0 -> ((p1 -> (!p2 U (!p2 & p3 & X(!p2 U p4)...62True
20G(p0 -> F(p1 & !p2 & X(!p2 U p3)))40True
21Fp0 -> ((p1 -> (!p0 U (!p0 & p2 & !p3 & X((!p0...41True
22G(p0 -> G(p1 -> (p2 & !p3 & X(!p3 U p4))))33True
23G((p0 & Fp1) -> ((p2 -> (!p1 U (!p1 & p3 & !p4...40True
24G(p0 -> ((p1 -> (!p2 U (!p2 & p3 & !p4 & X((!p...62True
25p0 U (p1 & X(p2 U p3))32True
26p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6)...72True
27F(p0 & XGp1)22True
28F(p0 & X(p1 & XFp2))42True
29F(p0 & X(p1 U p2))31True
...............
33G((p0 & p1 & !p2 & Xp2) -> X(p3 | X(!p1 | p3)))30True
34G((p0 & p1 & !p2 & Xp2) -> X(X!p1 | (p2 U (!p2...55True
35G(p0 & p1 & !p2 & Xp2) -> X(X!p1 | (p2 U (!p2 ...11True
36G((!p0 & p1) -> Xp2)20True
37G(p0 -> X(p0 | p1))22True
38G((!(p1 <-> Xp1) | !(p0 <-> Xp0) | !(p2 <-> Xp...3434True
39G((p0 & !p1 & Xp1 & Xp0) -> (p2 -> Xp3))22True
40G(p0 -> X(!p0 U p1))20True
41G((!p0 & Xp0) -> X((p0 U p1) | Gp0))33True
42G((!p0 & Xp0) -> X(p0 U (p0 & !p1 & X(p0 & p1))))44True
43G((!p0 & Xp0) -> X(p0 U (p0 & !p1 & X(p0 & p1 ...66True
44G((p0 & X!p0) -> X(!p0 U (!p0 & !p1 & X(!p0 & ...66True
45G((p0 & X!p0) -> X(!p0 U (!p0 & !p1 & X(!p0 & ...88True
46G((!p0 & Xp0) -> X(!(!p0 & Xp0) U (!p1 & Xp1)))66True
47G(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 ...120True
48G((Xp0 -> p0) -> (p1 <-> Xp1))44True
49G((Xp0 -> p0) -> ((p1 -> Xp1) & (!p1 -> X!p1)))44True
50p0 & XG!p021True
51XG(p0 -> (G!p1 | (!Xp1 U p2)))41True
52XG((p0 & !p1) -> (G!p1 | (!p1 U p2)))32True
53XG((p0 & p1) -> (Gp1 | (p1 U p2)))32True
54Xp0 & G((!p0 & Xp0) -> XXp0)50True
55(Xp0 U Xp1) | !X(p0 U p1)11True
56(Xp0 U p1) | !X(p0 U (p0 & p1))11True
57((Xp0 U p1) | !X(p0 U (p0 & p1))) & G(p0 -> Fp1)22True
58((Xp0 U Xp1) | !X(p0 U p1)) & G(p0 -> Fp1)22True
59!G(p0 -> X(p1 R p2))31True
60(p0 & Xp1) R X(((p2 U p3) R p0) U (p2 R p0))53True
61G(p0 | XGp1) & G(p2 | XG!p1)32True
62G(p0 | (Xp1 & X!p1))11True
\n", + "

63 rows \u00d7 4 columns

\n", + "
" + ], + "metadata": {}, + "output_type": "display_data", + "text": [ + " 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]" + ] + } + ], + "prompt_number": 29 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "There is no instance of set of stutter-invariant states that is not closed in these example formulas." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "sum(fwd_closed), len(fwd_closed)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 30, + "text": [ + "(63, 63)" + ] + } + ], + "prompt_number": 30 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Here is the percentage of stutter-invarant states." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "100*sum(sistates_size)/sum(aut_size)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 31, + "text": [ + "55.90277777777778" + ] + } + ], + "prompt_number": 31 } ], "metadata": {}