diff --git a/NEWS b/NEWS index 4e8084d4e..2b4552dc9 100644 --- a/NEWS +++ b/NEWS @@ -117,6 +117,12 @@ New in spot 2.0.3a (not yet released) the corresponding properties of the automaton as a side-effect of their check. + * the sbacc() function, used by "ltl2tgba -S" and "autfilt -S" to + convert automata to state-based acceptance, learned some tricks + (using SCCs, pulling accepting marks common to all outgoing edges, + and pushing acceptance marks common to all incoming edges) to + reduce the number of additional states needed. + * language_containment_checker now has default values for all parameters of its constructor. diff --git a/spot/twaalgos/sbacc.cc b/spot/twaalgos/sbacc.cc index 17c50a9aa..5b8039896 100644 --- a/spot/twaalgos/sbacc.cc +++ b/spot/twaalgos/sbacc.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015 Laboratoire de Recherche et Développement +// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement // de l'Epita. // // This file is part of Spot, a model checking library. @@ -21,6 +21,7 @@ #include #include #include +#include namespace spot { @@ -29,6 +30,26 @@ namespace spot if (old->prop_state_acc()) return old; + scc_info si(old); + + unsigned ns = old->num_states(); + acc_cond::mark_t all = old->acc().all_sets(); + std::vector common_in(ns, all); + std::vector common_out(ns, all); + std::vector one_in(ns, 0U); + for (auto& e: old->edges()) + if (si.scc_of(e.src) == si.scc_of(e.dst)) + { + common_in[e.dst] &= e.acc; + common_out[e.src] &= e.acc; + one_in[e.dst] = e.acc; + } + for (unsigned s = 0; s < ns; ++s) + common_out[s] |= common_in[s]; + for (auto& e: old->edges()) + if (si.scc_of(e.src) == si.scc_of(e.dst)) + one_in[e.dst] = (e.acc - common_out[e.src]); + auto res = make_twa_graph(old->get_dict()); res->copy_ap_of(old); res->copy_acceptance_of(old); @@ -54,28 +75,39 @@ namespace spot return p.first->second; }; - // Find any edge going into the initial state, and use its - // acceptance as mark. - acc_cond::mark_t init_acc = 0U; unsigned old_init = old->get_init_state_number(); - for (auto& t: old->edges()) - if (t.dst == old_init) - { - init_acc = t.acc; - break; - } + acc_cond::mark_t init_acc = 0U; + if (!si.is_rejecting_scc(si.scc_of(old_init))) + // Use any edge going into the initial state to set the first + // acceptance mark. + init_acc = one_in[old_init] | common_out[init_acc]; res->set_init_state(new_state(old_init, init_acc)); while (!todo.empty()) { auto one = todo.back(); todo.pop_back(); + unsigned scc_src = si.scc_of(one.first.first); + bool maybe_accepting = !si.is_rejecting_scc(scc_src); for (auto& t: old->out(one.first.first)) - res->new_edge(one.second, - new_state(t.dst, t.acc), - t.cond, - one.first.second); + { + unsigned scc_dst = si.scc_of(t.dst); + acc_cond::mark_t acc = 0U; + bool dst_acc = si.is_accepting_scc(scc_dst); + if (maybe_accepting && scc_src == scc_dst) + acc = t.acc - common_out[t.src]; + else if (dst_acc) + // We enter a new accepting SCC. Use any edge going into + // t.dst from this SCC to set the initial acceptance mark. + acc = one_in[t.dst]; + if (dst_acc) + acc |= common_out[t.dst]; + common_out[t.dst]; + res->new_edge(one.second, new_state(t.dst, acc), + t.cond, one.first.second); + } } + res->merge_edges(); return res; } } diff --git a/tests/core/parseaut.test b/tests/core/parseaut.test index c859adb41..665f8cc70 100755 --- a/tests/core/parseaut.test +++ b/tests/core/parseaut.test @@ -1755,14 +1755,14 @@ State: 0 1 0 2 2 1 0 2 2 1 0 2 2 1 0 2 2 State: 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 -State: 2 -2 2 2 2 3 3 3 3 4 4 4 4 5 5 5 5 -State: 3 {0} -2 2 2 2 3 3 3 3 4 4 4 4 5 5 5 5 -State: 4 {1} -2 2 2 2 3 3 3 3 4 4 4 4 5 5 5 5 -State: 5 {0 1} -2 2 2 2 3 3 3 3 4 4 4 4 5 5 5 5 +State: 2 {0 1} +3 3 3 3 4 4 4 4 5 5 5 5 2 2 2 2 +State: 3 +3 3 3 3 4 4 4 4 5 5 5 5 2 2 2 2 +State: 4 {0} +3 3 3 3 4 4 4 4 5 5 5 5 2 2 2 2 +State: 5 {1} +3 3 3 3 4 4 4 4 5 5 5 5 2 2 2 2 --END-- EOF diff --git a/tests/core/sbacc.test b/tests/core/sbacc.test index 172035781..156c2250a 100755 --- a/tests/core/sbacc.test +++ b/tests/core/sbacc.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015 Laboratoire de Recherche et Développement +# Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -37,26 +37,26 @@ Acceptance: 2 Inf(0)&Inf(1) properties: trans-labels explicit-labels state-acc complete properties: deterministic stutter-invariant --BODY-- -State: 0 {0 1} -[0&1] 0 -[!0&!1] 1 -[!0&1] 2 -[0&!1] 3 -State: 1 -[0&1] 0 -[!0&!1] 1 -[!0&1] 2 -[0&!1] 3 -State: 2 {1} -[0&1] 0 -[!0&!1] 1 -[!0&1] 2 -[0&!1] 3 -State: 3 {0} -[0&1] 0 -[!0&!1] 1 -[!0&1] 2 -[0&!1] 3 +State: 0 {0} +[0&!1] 0 +[0&1] 1 +[!0&!1] 2 +[!0&1] 3 +State: 1 {0 1} +[0&!1] 0 +[0&1] 1 +[!0&!1] 2 +[!0&1] 3 +State: 2 +[0&!1] 0 +[0&1] 1 +[!0&!1] 2 +[!0&1] 3 +State: 3 {1} +[0&!1] 0 +[0&1] 1 +[!0&!1] 2 +[!0&1] 3 --END-- EOF @@ -91,9 +91,9 @@ properties: trans-labels explicit-labels state-acc deterministic --BODY-- State: 0 {1} [0] 1 -State: 1 +State: 1 {0} [0] 2 -State: 2 {0} +State: 2 {0 1} [0] 0 --END-- EOF @@ -124,4 +124,8 @@ EOF diff out.hoa expected randltl --weak-fairness -n 20 2 | -ltlcross "$ltl2tgba -DH %f >%O" "$ltl2tgba -H %f | $autfilt -H >%O" + ltlcross "$ltl2tgba -DH %f >%O" \ + "$ltl2tgba -S %f >%O" \ + "$ltl2tgba -H %f | $autfilt -H >%O" + +test 4 = `ltl2tgba -S 'F(a & X(!a &Xb))' --any --stats=%s` diff --git a/tests/python/automata.ipynb b/tests/python/automata.ipynb index 392c35953..dec25e75f 100644 --- a/tests/python/automata.ipynb +++ b/tests/python/automata.ipynb @@ -18,7 +18,7 @@ "version": "3.4.3+" }, "name": "", - "signature": "sha256:91af67353e0a35fefd672b53bd005af28720c0c7a8dfc922ce70fa8f3ef6a42e" + "signature": "sha256:4ddb9b8fc1c41bacd7e47f70861303cde0ad425f842ade8e1f23ee74738914b0" }, "nbformat": 3, "nbformat_minor": 0, @@ -178,7 +178,7 @@ "\n" ], "text": [ - " *' at 0x7f5fc0c24900> >" + " *' at 0x7fe334de9900> >" ] } ], @@ -317,7 +317,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -470,7 +470,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -570,7 +570,7 @@ "\n" ], "text": [ - " *' at 0x7f5fc866e1b0> >" + " *' at 0x7fe33c8331b0> >" ] } ], @@ -640,7 +640,7 @@ "\n" ], "text": [ - " *' at 0x7f5fc866e060> >" + " *' at 0x7fe33c833060> >" ] } ], @@ -716,7 +716,7 @@ "\n" ], "text": [ - " *' at 0x7f5fc866e0f0> >" + " *' at 0x7fe33c8330f0> >" ] } ], @@ -839,7 +839,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -1029,7 +1029,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -1176,7 +1176,7 @@ "\n" ], "text": [ - " *' at 0x7f5fc866e300> >" + " *' at 0x7fe33c833300> >" ] } ], @@ -1277,7 +1277,7 @@ "\n" ], "text": [ - " *' at 0x7f5fc866e2d0> >" + " *' at 0x7fe33c8332d0> >" ] } ], @@ -1310,92 +1310,92 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", - "0->0\n", - "\n", - "\n", - "1\n", + "0->0\n", + "\n", + "\n", + "1\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "!a\n", + "0->1\n", + "\n", + "\n", + "!a\n", "\n", "\n", "2\n", "\n", - "\n", "2\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "\n", + "3\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "b\n", "\n", "\n", "3->2\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f5fc866e120> >" + " *' at 0x7fe33c833120> >" ] } ], @@ -1494,7 +1494,7 @@ "\n" ], "text": [ - " *' at 0x7f5fc866e330> >" + " *' at 0x7fe33c833330> >" ] } ], @@ -1964,7 +1964,7 @@ "\n" ], "text": [ - " *' at 0x7f5fc866e2a0> >" + " *' at 0x7fe33c8332a0> >" ] } ], @@ -2161,7 +2161,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -2286,7 +2286,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -2428,7 +2428,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -2579,7 +2579,7 @@ "\n" ], "text": [ - " *' at 0x7f5fc0b98ae0> >" + " *' at 0x7fe334d5cae0> >" ] } ], @@ -2735,7 +2735,7 @@ "\n" ], "text": [ - " *' at 0x7f5fc0b98fc0> >" + " *' at 0x7fe334d5cfc0> >" ] } ], @@ -2805,7 +2805,7 @@ "\n" ], "text": [ - " *' at 0x7f5fc0b98ae0> >" + " *' at 0x7fe334d5cae0> >" ] } ], @@ -2877,7 +2877,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -2930,7 +2930,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -3042,7 +3042,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -3154,7 +3154,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -3232,7 +3232,7 @@ "\n" ], "text": [ - " *' at 0x7f5fc866e390> >" + " *' at 0x7fe33c833390> >" ] }, { @@ -3315,7 +3315,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -3400,7 +3400,7 @@ "\n" ], "text": [ - " *' at 0x7f5fc85824e0> >" + " *' at 0x7fe33c747540> >" ] } ], @@ -3489,7 +3489,7 @@ "\n" ], "text": [ - " *' at 0x7f5fc85824e0> >" + " *' at 0x7fe33c747540> >" ] } ], @@ -3578,7 +3578,7 @@ "\n" ], "text": [ - " *' at 0x7f5fc85824e0> >" + " *' at 0x7fe33c747540> >" ] } ],