diff --git a/NEWS b/NEWS index 4b2fc5add..08f1c74a3 100644 --- a/NEWS +++ b/NEWS @@ -10,6 +10,14 @@ New in spot 1.99.4a (not yet released) are declared as weak. This code was previously in dtgba_complement(). + * scc_filter_states() has learnt to remove useless acceptance marks + that are on transitions between SCCs, while preserving state-based + acceptance. The most visible effect is in the output of "ltl2tgba + -s XXXa": it used to have 5 accepting states, it now has only one. + (Changing removing acceptance of those 4 states has no effect on + the language, but it speedup some algorithms like NDFS-based + emptiness checks, as discussed in our Spin'15 paper.) + Python: * Add bindings for complete() and dtwa_complement() diff --git a/src/tests/dstar.test b/src/tests/dstar.test index fcc7fde77..7e161739a 100755 --- a/src/tests/dstar.test +++ b/src/tests/dstar.test @@ -244,7 +244,7 @@ digraph G { node [shape="circle"] I [label="", style=invis, width=0] I -> 0 - 0 [label="0", peripheries=2] + 0 [label="0"] 0 -> 1 [label="!a & !b"] 0 -> 2 [label="a & !b"] 1 [label="1", peripheries=2] diff --git a/src/tests/prodor.test b/src/tests/prodor.test index d5528ccee..605d16223 100755 --- a/src/tests/prodor.test +++ b/src/tests/prodor.test @@ -96,15 +96,15 @@ Acceptance: 2 Inf(0) | Inf(1) properties: trans-labels explicit-labels state-acc complete properties: deterministic --BODY-- -State: 0 {0 1} +State: 0 {1} [0] 1 [!0] 2 -State: 1 {0 1} +State: 1 {1} [0&1] 3 [!0&1] 4 [0&!1] 5 [!0&!1] 6 -State: 2 {0} +State: 2 [0&1] 3 [!0&1] 4 [0&!1] 5 diff --git a/src/tests/readsave.test b/src/tests/readsave.test index 9c562935e..01912d4ab 100755 --- a/src/tests/readsave.test +++ b/src/tests/readsave.test @@ -700,3 +700,40 @@ diff output3 expect3 $autfilt -Hk input 2>stderr && exit 1 grep 'print_hoa.*k' stderr + +cat >input4 <output4 +cat output4 + +cat >expect4<has_state_based_acc()) - return scc_filter_states(a); + // If the automaton is weak, using transition-based acceptance + // won't help, so let's preserve it. + if ((state_based_ || a->is_inherently_weak()) && a->has_state_based_acc()) + return scc_filter_states(a, arg); else return scc_filter(a, arg); } @@ -186,7 +188,7 @@ namespace spot || (type_ == Monitor && a->num_sets() == 0)) { if (tgb_used) - a = do_scc_filter(a); + a = do_scc_filter(a, true); if (COMP_) a = complete(a); if (SBACC_) @@ -202,7 +204,7 @@ namespace spot // ignored. a = scc_filter_states(a); else - a = do_scc_filter(a); + a = do_scc_filter(a, (PREF_ == Any)); if (type_ == Monitor) { @@ -445,10 +447,12 @@ namespace spot sim = nullptr; } - if (type_ == TGBA && level_ == High && scc_filter_ != 0) + if (level_ == High && scc_filter_ != 0) { - if (dba && !dba_is_minimal) // WDBA is already clean. + if (dba) { + // Do that even for WDBA, to remove marks from transitions + // leaving trivial SCCs. dba = do_scc_filter(dba, true); assert(!sim); } diff --git a/src/twaalgos/sccfilter.cc b/src/twaalgos/sccfilter.cc index c1b15fa38..098b8a2ee 100644 --- a/src/twaalgos/sccfilter.cc +++ b/src/twaalgos/sccfilter.cc @@ -126,8 +126,10 @@ namespace spot // Remove acceptance conditions from all edges outside of // non-accepting SCCs. If "RemoveAll" is false, keep those on - // transitions entering accepting SCCs. - template + // transitions entering accepting SCCs. If "PreserveSBA", is set + // only touch a transition if all its neighbor siblings can be + // touched as well. + template struct acc_filter_mask: next_filter { acc_cond::mark_t accmask; @@ -154,16 +156,47 @@ namespace spot if (keep) { - unsigned u = this->si->scc_of(dst); - // If the edge is between two SCCs, we can simplify - // remove the acceptance sets. If the SCC is non-accepting, - // we can only remove the Inf sets. - if (RemoveAll && u != this->si->scc_of(src)) - acc = 0U; - else if (this->si->is_rejecting_scc(u)) - acc &= accmask; + unsigned u = this->si->scc_of(src); + unsigned v = this->si->scc_of(dst); + // The basic rules are as follows: + // + // - If an edge is between two SCCs, is OK to remove + // all acceptance sets, as this edge cannot be part + // of any loop. + // - If an edge is in an non-accepting SCC, we can only + // remove the Inf sets, as removinf the Fin sets + // might make the SCC accepting. + // + // The above rules are made more complex with two flags: + // + // - If PreserveSBA is set, we have to tree a transition + // leaving an SCC as other transitions inside the SCC, + // otherwise we will break the property that all + // transitions leaving the same state have identical set + // membership. + // - If RemoveAll is false, we like to keep the membership + // of transitions entering an SCC. This can only be + // done if PreserveSBA is unset, unfortunately. + if (u == v) + { + if (this->si->is_rejecting_scc(u)) + acc &= accmask; + } + else if (PreserveSBA && this->si->is_rejecting_scc(u)) + { + if (!this->si->is_trivial(u)) + acc &= accmask; // No choice. + else if (RemoveAll) + acc = 0U; + } + else if (!PreserveSBA) + { + if (RemoveAll) + acc = 0U; + else if (this->si->is_rejecting_scc(v)) + acc &= accmask; + } } - return filtered_trans(keep, cond, acc); } }; @@ -186,7 +219,7 @@ namespace spot auto& acc = this->si->get_aut()->acc(); if (!acc.is_generalized_buchi()) throw std::runtime_error - ("simplification of SCC acceptance work only with " + ("simplification of SCC acceptance works only with " "generalized Büchi acceptance"); unsigned scc_count = this->si->scc_count(); @@ -243,10 +276,11 @@ namespace spot twa_graph_ptr scc_filter_apply(const_twa_graph_ptr aut, scc_info* given_si, Args&&... args) { + unsigned in_n = aut->num_states(); + if (in_n == 0) // nothing to filter. + return make_twa_graph(aut, twa::prop_set::all()); + twa_graph_ptr filtered = make_twa_graph(aut->get_dict()); - unsigned in_n = aut->num_states(); // Number of input states. - if (in_n == 0) // Nothing to filter. - return filtered; filtered->copy_ap_of(aut); // Compute scc_info if not supplied. @@ -302,9 +336,16 @@ namespace spot } twa_graph_ptr - scc_filter_states(const const_twa_graph_ptr& aut, scc_info* given_si) + scc_filter_states(const const_twa_graph_ptr& aut, bool remove_all_useless, + scc_info* given_si) { - auto res = scc_filter_apply>(aut, given_si); + twa_graph_ptr res; + if (remove_all_useless) + res = scc_filter_apply>>(aut, given_si); + else + res = scc_filter_apply>>(aut, given_si); res->prop_copy(aut, { true, true, true, true }); return res; } @@ -321,21 +362,25 @@ namespace spot res = scc_filter_apply>>>(aut, given_si); + >>>(aut, given_si); else res = scc_filter_apply>>>(aut, given_si); + >>>(aut, given_si); } else { if (remove_all_useless) res = scc_filter_apply>>(aut, given_si); + >>(aut, given_si); else res = scc_filter_apply>>(aut, given_si); + >>(aut, given_si); } res->merge_edges(); res->prop_copy(aut, @@ -357,18 +402,20 @@ namespace spot res = scc_filter_apply>>>>(aut, given_si, - suspvars, - ignoredvars, - early_susp); + >>>>(aut, given_si, + suspvars, + ignoredvars, + early_susp); else res = scc_filter_apply>>>>(aut, given_si, - suspvars, - ignoredvars, - early_susp); + >>>>(aut, given_si, + suspvars, + ignoredvars, + early_susp); res->merge_edges(); res->prop_copy(aut, { false, // state-based acceptance is not preserved diff --git a/src/twaalgos/sccfilter.hh b/src/twaalgos/sccfilter.hh index ff6e44c4c..162e715d9 100644 --- a/src/twaalgos/sccfilter.hh +++ b/src/twaalgos/sccfilter.hh @@ -63,14 +63,14 @@ namespace spot /// \brief Prune unaccepting SCCs. /// - /// This is an abridged version of scc_filter(), that only removes - /// useless states, without touching at the acceptance conditions. - /// - /// Especially, if the input TωA has the SBA property, (i.e., - /// transitions leaving accepting states are all marked as - /// accepting), then the output TGBA will also have that property. + /// This is an abridged version of scc_filter(), that preserves + /// state-based acceptance. I.e., if the input TωA has the SBA + /// property, (i.e., transitions leaving accepting states are all + /// marked as accepting), then the output TωA will also have that + /// property. SPOT_API twa_graph_ptr scc_filter_states(const const_twa_graph_ptr& aut, + bool remove_all_useless = false, scc_info* given_si = nullptr); /// \brief Prune unaccepting SCCs, superfluous acceptance diff --git a/src/twaalgos/simulation.cc b/src/twaalgos/simulation.cc index ce32de1e4..966e8343b 100644 --- a/src/twaalgos/simulation.cc +++ b/src/twaalgos/simulation.cc @@ -777,7 +777,7 @@ namespace spot res = cosimul.run(); if (Sba) - res = scc_filter_states(res); + res = scc_filter_states(res, false); else res = scc_filter(res, false); diff --git a/wrap/python/tests/automata.ipynb b/wrap/python/tests/automata.ipynb index d863de9a5..4617f3847 100644 --- a/wrap/python/tests/automata.ipynb +++ b/wrap/python/tests/automata.ipynb @@ -17,8 +17,7 @@ "pygments_lexer": "ipython3", "version": "3.4.3+" }, - "name": "", - "signature": "sha256:6b034a8346695a3f327fd50e8c768209ea3d931598b99d5d80508685976c255e" + "name": "" }, "nbformat": 3, "nbformat_minor": 0, @@ -177,7 +176,7 @@ "\n" ], "text": [ - " *' at 0x7f2998ab6540> >" + " *' at 0x7f2e58013ea0> >" ] } ], @@ -316,7 +315,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -469,7 +468,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -569,7 +568,7 @@ "\n" ], "text": [ - " *' at 0x7f2998a8be40> >" + " *' at 0x7f2e4afe6720> >" ] } ], @@ -639,7 +638,7 @@ "\n" ], "text": [ - " *' at 0x7f2998a8bed0> >" + " *' at 0x7f2e4afe6870> >" ] } ], @@ -715,7 +714,7 @@ "\n" ], "text": [ - " *' at 0x7f2998a8b840> >" + " *' at 0x7f2e4afe6600> >" ] } ], @@ -838,7 +837,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -1028,7 +1027,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -1175,7 +1174,7 @@ "\n" ], "text": [ - " *' at 0x7f2998a280f0> >" + " *' at 0x7f2e4afe6180> >" ] } ], @@ -1276,7 +1275,7 @@ "\n" ], "text": [ - " *' at 0x7f2998a28120> >" + " *' at 0x7f2e4afe6330> >" ] } ], @@ -1394,7 +1393,7 @@ "\n" ], "text": [ - " *' at 0x7f2998a28150> >" + " *' at 0x7f2e4afe66c0> >" ] } ], @@ -1427,11 +1426,11 @@ "\n", "\n", - "\n", + "\n", "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", @@ -1473,28 +1472,27 @@ "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "b\n", - "\u24ff\n", + "\n", + "\n", + "b\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "1\n", - "\u24ff\n", + "\n", + "\n", + "1\n", + "\u24ff\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f2998a28180> >" + " *' at 0x7f2e4afe6de0> >" ] } ], @@ -1571,13 +1569,13 @@ "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "0->4\n", - "\n", - "\n", + "\n", + "\n", "!a & !b\n", "\n", "\n", @@ -1593,13 +1591,13 @@ "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "0->6\n", - "\n", - "\n", + "\n", + "\n", "a & !b\n", "\n", "\n", @@ -1622,8 +1620,8 @@ "\n", "\n", "1->4\n", - "\n", - "\n", + "\n", + "\n", "!a & !b\n", "\n", "\n", @@ -1634,9 +1632,9 @@ "\n", "\n", "1->6\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "2->1\n", @@ -1658,9 +1656,9 @@ "\n", "\n", "2->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "2->5\n", @@ -1670,9 +1668,9 @@ "\n", "\n", "2->6\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "3->1\n", @@ -1694,8 +1692,8 @@ "\n", "\n", "3->4\n", - "\n", - "\n", + "\n", + "\n", "!a & !b\n", "\n", "\n", @@ -1706,45 +1704,45 @@ "\n", "\n", "3->6\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "4->1\n", - "\n", + "\n", "\n", - "a & b\n", + "a & b\n", "\n", "\n", "4->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "4->3\n", - "\n", - "\n", + "\n", + "\n", "a & !b\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "4->5\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "4->6\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "5->5\n", @@ -1754,221 +1752,217 @@ "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "5->7\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "5->8\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "6->6\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "6->7\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "6->8\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "7->7\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "9\n", - "\n", - "9\n", + "\n", + "9\n", "\n", "\n", "7->9\n", - "\n", - "\n", - "a & b\n", - "\u24ff\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "7->10\n", - "\n", - "\n", - "!a & b\n", - "\u24ff\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "8->8\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "8->9\n", - "\n", - "\n", - "a & b\n", - "\u24ff\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "8->10\n", - "\n", - "\n", - "!a & b\n", - "\u24ff\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "9->9\n", - "\n", - "\n", - "a & b\n", - "\u24ff\n", + "\n", + "\n", + "a & b\n", + "\u24ff\n", "\n", "\n", "9->10\n", - "\n", - "\n", - "!a & b\n", - "\u24ff\n", + "\n", + "\n", + "!a & b\n", + "\u24ff\n", "\n", "\n", "11\n", - "\n", - "11\n", + "\n", + "11\n", "\n", "\n", "9->11\n", - "\n", - "\n", - "a & !b\n", - "\u24ff\n", + "\n", + "\n", + "a & !b\n", + "\u24ff\n", "\n", "\n", "12\n", - "\n", - "12\n", + "\n", + "12\n", "\n", "\n", "9->12\n", - "\n", - "\n", - "!a & !b\n", - "\u24ff\n", + "\n", + "\n", + "!a & !b\n", + "\u24ff\n", "\n", "\n", "10->9\n", - "\n", - "\n", - "a & b\n", - "\u24ff\n", + "\n", + "\n", + "a & b\n", + "\u24ff\n", "\n", "\n", "10->10\n", - "\n", - "\n", - "!a & b\n", - "\u24ff\n", + "\n", + "\n", + "!a & b\n", + "\u24ff\n", "\n", "\n", "10->11\n", - "\n", - "\n", - "a & !b\n", - "\u24ff\n", + "\n", + "\n", + "a & !b\n", + "\u24ff\n", "\n", "\n", "10->12\n", - "\n", - "\n", - "!a & !b\n", - "\u24ff\n", + "\n", + "\n", + "!a & !b\n", + "\u24ff\n", "\n", "\n", "11->9\n", - "\n", - "\n", - "a & b\n", - "\u24ff\n", + "\n", + "\n", + "a & b\n", + "\u24ff\n", "\n", "\n", "11->10\n", - "\n", - "\n", - "!a & b\n", - "\u24ff\n", + "\n", + "\n", + "!a & b\n", + "\u24ff\n", "\n", "\n", "11->11\n", - "\n", - "\n", - "a & !b\n", - "\u24ff\n", + "\n", + "\n", + "a & !b\n", + "\u24ff\n", "\n", "\n", "11->12\n", - "\n", - "\n", - "!a & !b\n", - "\u24ff\n", + "\n", + "\n", + "!a & !b\n", + "\u24ff\n", "\n", "\n", "12->9\n", - "\n", - "\n", - "a & b\n", - "\u24ff\n", + "\n", + "\n", + "a & b\n", + "\u24ff\n", "\n", "\n", "12->10\n", - "\n", - "\n", - "!a & b\n", - "\u24ff\n", + "\n", + "\n", + "!a & b\n", + "\u24ff\n", "\n", "\n", "12->11\n", - "\n", - "\n", - "a & !b\n", - "\u24ff\n", + "\n", + "\n", + "a & !b\n", + "\u24ff\n", "\n", "\n", "12->12\n", - "\n", - "\n", - "!a & !b\n", - "\u24ff\n", + "\n", + "\n", + "!a & !b\n", + "\u24ff\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f2998a8bde0> >" + " *' at 0x7f2e4afe6d20> >" ] } ], @@ -2171,7 +2165,7 @@ "\n" ], "text": [ - " *' at 0x7f2998a8bfc0> >" + " *' at 0x7f2e4afe66f0> >" ] } ], @@ -2327,7 +2321,7 @@ "\n" ], "text": [ - " *' at 0x7f2998a8bea0> >" + " *' at 0x7f2e4afe6e70> >" ] } ], @@ -2397,7 +2391,7 @@ "\n" ], "text": [ - " *' at 0x7f2998a281e0> >" + " *' at 0x7f2e4afe6660> >" ] } ], diff --git a/wrap/python/tests/piperead.ipynb b/wrap/python/tests/piperead.ipynb index caf78463d..959790d2d 100644 --- a/wrap/python/tests/piperead.ipynb +++ b/wrap/python/tests/piperead.ipynb @@ -43,7 +43,7 @@ "source": [ "# Reading automata output from processes\n", "\n", - "If an argument of `spot.automata` ends with `|`, then it is interpreted as a shell command that outputs and automaton." + "If an argument of `spot.automata` ends with `|`, then it is interpreted as a shell command that outputs one automaton or more." ] }, { @@ -110,7 +110,7 @@ "\n" ], "text": [ - " *' at 0x7faffcc25750> >" + " *' at 0x7f3fa02ed390> >" ] }, { @@ -123,46 +123,45 @@ "\n", "\n", - "\n", + "\n", "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", - "\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7faffcc257e0> >" + " *' at 0x7f3fa02ed420> >" ] }, { @@ -208,7 +207,7 @@ "\n" ], "text": [ - " *' at 0x7faffcc257b0> >" + " *' at 0x7f3fa02ed3f0> >" ] }, { @@ -265,7 +264,7 @@ "\n" ], "text": [ - " *' at 0x7faffcc25750> >" + " *' at 0x7f3fa02ed390> >" ] } ], @@ -342,7 +341,7 @@ "\n" ], "text": [ - " *' at 0x7faffcc25f60> >" + " *' at 0x7f3fa02ed480> >" ] } ], @@ -374,8 +373,8 @@ "\u001b[1;31m---------------------------------------------------------------------------\u001b[0m", "\u001b[1;31mRuntimeError\u001b[0m Traceback (most recent call last)", "\u001b[1;32m\u001b[0m in \u001b[0;36m\u001b[1;34m()\u001b[0m\n\u001b[1;32m----> 1\u001b[1;33m \u001b[0mspot\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mautomaton\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'non-existing-command|'\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m", - "\u001b[1;32m/home-ssd/adl/git/spot/wrap/python/spot.py\u001b[0m in \u001b[0;36mautomaton\u001b[1;34m(filename)\u001b[0m\n\u001b[0;32m 216\u001b[0m See `spot.automata()` for a list of supported formats.\"\"\"\n\u001b[0;32m 217\u001b[0m \u001b[1;32mtry\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 218\u001b[1;33m \u001b[1;32mreturn\u001b[0m \u001b[0mnext\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mautomata\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m 219\u001b[0m \u001b[1;32mexcept\u001b[0m \u001b[0mStopIteration\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 220\u001b[0m \u001b[1;32mraise\u001b[0m \u001b[0mRuntimeError\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m\"Failed to read automaton from {}\"\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mformat\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n", - "\u001b[1;32m/home-ssd/adl/git/spot/wrap/python/spot.py\u001b[0m in \u001b[0;36mautomata\u001b[1;34m(*filenames)\u001b[0m\n\u001b[0;32m 208\u001b[0m \u001b[1;32mif\u001b[0m \u001b[0mret\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 209\u001b[0m raise RuntimeError(\"Command {} exited with exit status {}\"\n\u001b[1;32m--> 210\u001b[1;33m .format(filename[:-1], ret))\n\u001b[0m\u001b[0;32m 211\u001b[0m \u001b[1;32mreturn\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 212\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n", + "\u001b[1;32m/home-ssd/adl/git/spot/wrap/python/spot.py\u001b[0m in \u001b[0;36mautomaton\u001b[1;34m(filename)\u001b[0m\n\u001b[0;32m 369\u001b[0m See `spot.automata` for a list of supported formats.\"\"\"\n\u001b[0;32m 370\u001b[0m \u001b[1;32mtry\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 371\u001b[1;33m \u001b[1;32mreturn\u001b[0m \u001b[0mnext\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mautomata\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m 372\u001b[0m \u001b[1;32mexcept\u001b[0m \u001b[0mStopIteration\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 373\u001b[0m \u001b[1;32mraise\u001b[0m \u001b[0mRuntimeError\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m\"Failed to read automaton from {}\"\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mformat\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n", + "\u001b[1;32m/home-ssd/adl/git/spot/wrap/python/spot.py\u001b[0m in \u001b[0;36mautomata\u001b[1;34m(*filenames)\u001b[0m\n\u001b[0;32m 360\u001b[0m \u001b[1;32mif\u001b[0m \u001b[0mret\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 361\u001b[0m raise RuntimeError(\"Command {} exited with exit status {}\"\n\u001b[1;32m--> 362\u001b[1;33m .format(filename[:-1], ret))\n\u001b[0m\u001b[0;32m 363\u001b[0m \u001b[1;32mreturn\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 364\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n", "\u001b[1;31mRuntimeError\u001b[0m: Command non-existing-command exited with exit status 127" ] } @@ -446,7 +445,7 @@ "\n" ], "text": [ - " *' at 0x7faffcc25720> >" + " *' at 0x7f3fa02edea0> >" ] }, { @@ -457,7 +456,7 @@ "\u001b[1;31m---------------------------------------------------------------------------\u001b[0m", "\u001b[1;31mRuntimeError\u001b[0m Traceback (most recent call last)", "\u001b[1;32m\u001b[0m in \u001b[0;36m\u001b[1;34m()\u001b[0m\n\u001b[1;32m----> 1\u001b[1;33m \u001b[1;32mfor\u001b[0m \u001b[0ma\u001b[0m \u001b[1;32min\u001b[0m \u001b[0mspot\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mautomata\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m\"ltl2tgba -H 'a U b'|\"\u001b[0m\u001b[1;33m,\u001b[0m \u001b[1;34m'ltl2tgba -f \"syntax U U error\"|'\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m 2\u001b[0m \u001b[0mdisplay\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0ma\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n", - "\u001b[1;32m/home-ssd/adl/git/spot/wrap/python/spot.py\u001b[0m in \u001b[0;36mautomata\u001b[1;34m(*filenames)\u001b[0m\n\u001b[0;32m 208\u001b[0m \u001b[1;32mif\u001b[0m \u001b[0mret\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 209\u001b[0m raise RuntimeError(\"Command {} exited with exit status {}\"\n\u001b[1;32m--> 210\u001b[1;33m .format(filename[:-1], ret))\n\u001b[0m\u001b[0;32m 211\u001b[0m \u001b[1;32mreturn\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 212\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n", + "\u001b[1;32m/home-ssd/adl/git/spot/wrap/python/spot.py\u001b[0m in \u001b[0;36mautomata\u001b[1;34m(*filenames)\u001b[0m\n\u001b[0;32m 360\u001b[0m \u001b[1;32mif\u001b[0m \u001b[0mret\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 361\u001b[0m raise RuntimeError(\"Command {} exited with exit status {}\"\n\u001b[1;32m--> 362\u001b[1;33m .format(filename[:-1], ret))\n\u001b[0m\u001b[0;32m 363\u001b[0m \u001b[1;32mreturn\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 364\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n", "\u001b[1;31mRuntimeError\u001b[0m: Command ltl2tgba -f \"syntax U U error\" exited with exit status 2" ] } @@ -488,8 +487,8 @@ "\u001b[1;31m---------------------------------------------------------------------------\u001b[0m", "\u001b[1;31mRuntimeError\u001b[0m Traceback (most recent call last)", "\u001b[1;32m\u001b[0m in \u001b[0;36m\u001b[1;34m()\u001b[0m\n\u001b[1;32m----> 1\u001b[1;33m \u001b[0mspot\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mautomaton\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'false|'\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m", - "\u001b[1;32m/home-ssd/adl/git/spot/wrap/python/spot.py\u001b[0m in \u001b[0;36mautomaton\u001b[1;34m(filename)\u001b[0m\n\u001b[0;32m 216\u001b[0m See `spot.automata()` for a list of supported formats.\"\"\"\n\u001b[0;32m 217\u001b[0m \u001b[1;32mtry\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 218\u001b[1;33m \u001b[1;32mreturn\u001b[0m \u001b[0mnext\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mautomata\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m 219\u001b[0m \u001b[1;32mexcept\u001b[0m \u001b[0mStopIteration\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 220\u001b[0m \u001b[1;32mraise\u001b[0m \u001b[0mRuntimeError\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m\"Failed to read automaton from {}\"\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mformat\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n", - "\u001b[1;32m/home-ssd/adl/git/spot/wrap/python/spot.py\u001b[0m in \u001b[0;36mautomata\u001b[1;34m(*filenames)\u001b[0m\n\u001b[0;32m 208\u001b[0m \u001b[1;32mif\u001b[0m \u001b[0mret\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 209\u001b[0m raise RuntimeError(\"Command {} exited with exit status {}\"\n\u001b[1;32m--> 210\u001b[1;33m .format(filename[:-1], ret))\n\u001b[0m\u001b[0;32m 211\u001b[0m \u001b[1;32mreturn\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 212\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n", + "\u001b[1;32m/home-ssd/adl/git/spot/wrap/python/spot.py\u001b[0m in \u001b[0;36mautomaton\u001b[1;34m(filename)\u001b[0m\n\u001b[0;32m 369\u001b[0m See `spot.automata` for a list of supported formats.\"\"\"\n\u001b[0;32m 370\u001b[0m \u001b[1;32mtry\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 371\u001b[1;33m \u001b[1;32mreturn\u001b[0m \u001b[0mnext\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mautomata\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m 372\u001b[0m \u001b[1;32mexcept\u001b[0m \u001b[0mStopIteration\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 373\u001b[0m \u001b[1;32mraise\u001b[0m \u001b[0mRuntimeError\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m\"Failed to read automaton from {}\"\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mformat\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n", + "\u001b[1;32m/home-ssd/adl/git/spot/wrap/python/spot.py\u001b[0m in \u001b[0;36mautomata\u001b[1;34m(*filenames)\u001b[0m\n\u001b[0;32m 360\u001b[0m \u001b[1;32mif\u001b[0m \u001b[0mret\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 361\u001b[0m raise RuntimeError(\"Command {} exited with exit status {}\"\n\u001b[1;32m--> 362\u001b[1;33m .format(filename[:-1], ret))\n\u001b[0m\u001b[0;32m 363\u001b[0m \u001b[1;32mreturn\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 364\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n", "\u001b[1;31mRuntimeError\u001b[0m: Command false exited with exit status 1" ] }