From 2c764fb3c7a67a8b0e93afc19f6315c0c06bd17e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 29 Sep 2014 18:17:34 +0200 Subject: [PATCH] Store membership to acceptance sets using bitsets, not BDDs. This is a huge patch, that took over a month to complete. The bit sets are currently restricted to what 'unsigned can store', but it should be easy to extend it to 'uint64_t' should we need it. * NEWS: Update. * src/tgba/acc.hh: New file. * src/tgbatest/acc.cc, src/tgbatest/acc.test: Test it. * src/tgba/tgbakvcomplement.cc, src/tgba/tgbakvcomplement.hh, src/tgba/tgbasgba.cc, src/tgba/tgbasgba.hh: Delete. The KV complementation is too slow to be used in practice, and I somehow broke it during the conversion to bitsets. The tgba->sgba conversion was only used for the KV complementation, and should be better redone on tgba_digraph_ptr should it be needed again. * src/bin/ltlcross.cc, src/dstarparse/dra2ba.cc, src/dstarparse/nsa2tgba.cc, src/graphtest/tgbagraph.cc, src/graphtest/tgbagraph.test, src/kripke/fairkripke.cc, src/kripke/fairkripke.hh, src/kripke/kripke.cc, src/kripke/kripke.hh, src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh, src/misc/hash.hh, src/neverparse/neverclaimparse.yy, src/priv/accmap.hh, src/ta/ta.cc, src/ta/ta.hh, src/ta/taexplicit.cc, src/ta/taexplicit.hh, src/ta/taproduct.cc, src/ta/taproduct.hh, src/ta/tgta.cc, src/ta/tgta.hh, src/ta/tgtaexplicit.cc, src/ta/tgtaexplicit.hh, src/ta/tgtaproduct.cc, src/ta/tgtaproduct.hh, src/taalgos/dotty.cc, src/taalgos/emptinessta.cc, src/taalgos/minimize.cc, src/taalgos/tgba2ta.cc, src/tgba/Makefile.am, src/tgba/fwd.hh, src/tgba/taatgba.cc, src/tgba/taatgba.hh, src/tgba/tgba.cc, src/tgba/tgba.hh, src/tgba/tgbagraph.cc, src/tgba/tgbagraph.hh, src/tgba/tgbamask.cc, src/tgba/tgbamask.hh, src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh, src/tgba/tgbaproxy.cc, src/tgba/tgbaproxy.hh, src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh, src/tgbaalgos/bfssteps.cc, src/tgbaalgos/complete.cc, src/tgbaalgos/compsusp.cc, src/tgbaalgos/degen.cc, src/tgbaalgos/dotty.cc, src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbacomp.cc, src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/dupexp.cc, src/tgbaalgos/emptiness.cc, src/tgbaalgos/emptiness.hh, src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/sccstack.cc, src/tgbaalgos/gtec/sccstack.hh, src/tgbaalgos/gv04.cc, src/tgbaalgos/hoaf.cc, src/tgbaalgos/isweakscc.cc, src/tgbaalgos/lbtt.cc, src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/magic.cc, src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/neverclaim.cc, src/tgbaalgos/postproc.cc, src/tgbaalgos/powerset.cc, src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh, src/tgbaalgos/reducerun.cc, src/tgbaalgos/replayrun.cc, src/tgbaalgos/safety.cc, src/tgbaalgos/save.cc, src/tgbaalgos/scc.cc, src/tgbaalgos/scc.hh, src/tgbaalgos/sccfilter.cc, src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh, src/tgbaalgos/se05.cc, src/tgbaalgos/simulation.cc, src/tgbaalgos/simulation.hh, src/tgbaalgos/stats.cc, src/tgbaalgos/stripacc.cc, src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc, src/tgbaalgos/weight.cc, src/tgbaalgos/weight.hh, src/tgbaparse/tgbaparse.yy, src/tgbatest/Makefile.am, src/tgbatest/complementation.cc, src/tgbatest/complementation.test, src/tgbatest/degenlskip.test, src/tgbatest/det.test, src/tgbatest/dstar.test, src/tgbatest/emptchk.cc, src/tgbatest/explpro2.test, src/tgbatest/explpro3.test, src/tgbatest/explpro4.test, src/tgbatest/explprod.test, src/tgbatest/ltl2tgba.cc, src/tgbatest/ltl2tgba.test, src/tgbatest/maskacc.cc, src/tgbatest/maskacc.test, src/tgbatest/neverclaimread.test, src/tgbatest/randtgba.cc, src/tgbatest/readsave.test, src/tgbatest/sim.test, src/tgbatest/sim2.test, src/tgbatest/spotlbtt.test, src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test, iface/dve2/dve2.cc: Adjust or use to the new acceptance interface. --- NEWS | 38 +- iface/dve2/dve2.cc | 3 +- src/bin/ltlcross.cc | 2 +- src/dstarparse/dra2ba.cc | 5 +- src/dstarparse/nsa2tgba.cc | 2 +- src/graphtest/tgbagraph.cc | 24 +- src/graphtest/tgbagraph.test | 66 +-- src/kripke/fairkripke.cc | 6 +- src/kripke/fairkripke.hh | 16 +- src/kripke/kripke.cc | 20 +- src/kripke/kripke.hh | 12 +- src/kripke/kripkeexplicit.cc | 14 +- src/kripke/kripkeexplicit.hh | 2 - src/misc/hash.hh | 7 +- src/neverparse/neverclaimparse.yy | 9 +- src/priv/accmap.hh | 69 +-- src/ta/ta.cc | 2 +- src/ta/ta.hh | 39 +- src/ta/taexplicit.cc | 11 +- src/ta/taexplicit.hh | 33 +- src/ta/taproduct.cc | 11 +- src/ta/taproduct.hh | 7 +- src/ta/tgta.cc | 14 +- src/ta/tgta.hh | 4 +- src/ta/tgtaexplicit.cc | 18 +- src/ta/tgtaexplicit.hh | 10 +- src/ta/tgtaproduct.cc | 4 +- src/ta/tgtaproduct.hh | 4 +- src/taalgos/dotty.cc | 5 +- src/taalgos/emptinessta.cc | 33 +- src/taalgos/minimize.cc | 248 ++++++----- src/taalgos/tgba2ta.cc | 61 ++- src/tgba/Makefile.am | 7 +- src/tgba/acc.hh | 433 +++++++++++++++++++ src/tgba/fwd.hh | 4 - src/tgba/taatgba.cc | 48 +-- src/tgba/taatgba.hh | 58 +-- src/tgba/tgba.cc | 23 +- src/tgba/tgba.hh | 44 +- src/tgba/tgbagraph.cc | 39 +- src/tgba/tgbagraph.hh | 61 ++- src/tgba/tgbakvcomplement.cc | 685 ------------------------------ src/tgba/tgbakvcomplement.hh | 124 ------ src/tgba/tgbamask.cc | 26 +- src/tgba/tgbamask.hh | 8 +- src/tgba/tgbaproduct.cc | 116 ++--- src/tgba/tgbaproduct.hh | 12 +- src/tgba/tgbaproxy.cc | 21 +- src/tgba/tgbaproxy.hh | 6 - src/tgba/tgbasafracomplement.cc | 62 +-- src/tgba/tgbasafracomplement.hh | 9 +- src/tgba/tgbasgba.cc | 262 ------------ src/tgba/tgbasgba.hh | 76 ---- src/tgbaalgos/bfssteps.cc | 2 +- src/tgbaalgos/complete.cc | 8 +- src/tgbaalgos/compsusp.cc | 42 +- src/tgbaalgos/degen.cc | 123 +++--- src/tgbaalgos/dotty.cc | 16 +- src/tgbaalgos/dtbasat.cc | 8 +- src/tgbaalgos/dtgbacomp.cc | 53 +-- src/tgbaalgos/dtgbasat.cc | 225 ++++------ src/tgbaalgos/dupexp.cc | 6 +- src/tgbaalgos/emptiness.cc | 10 +- src/tgbaalgos/emptiness.hh | 2 +- src/tgbaalgos/gtec/ce.cc | 13 +- src/tgbaalgos/gtec/gtec.cc | 14 +- src/tgbaalgos/gtec/gtec.hh | 6 +- src/tgbaalgos/gtec/sccstack.cc | 2 +- src/tgbaalgos/gtec/sccstack.hh | 6 +- src/tgbaalgos/gv04.cc | 15 +- src/tgbaalgos/hoaf.cc | 41 +- src/tgbaalgos/isweakscc.cc | 13 +- src/tgbaalgos/lbtt.cc | 49 +-- src/tgbaalgos/ltl2tgba_fm.cc | 68 ++- src/tgbaalgos/magic.cc | 20 +- src/tgbaalgos/ndfs_result.hxx | 30 +- src/tgbaalgos/neverclaim.cc | 9 +- src/tgbaalgos/postproc.cc | 9 +- src/tgbaalgos/powerset.cc | 4 +- src/tgbaalgos/randomgraph.cc | 42 +- src/tgbaalgos/randomgraph.hh | 6 +- src/tgbaalgos/reducerun.cc | 13 +- src/tgbaalgos/replayrun.cc | 25 +- src/tgbaalgos/safety.cc | 6 +- src/tgbaalgos/save.cc | 32 +- src/tgbaalgos/scc.cc | 38 +- src/tgbaalgos/scc.hh | 25 +- src/tgbaalgos/sccfilter.cc | 257 ++--------- src/tgbaalgos/sccinfo.cc | 31 +- src/tgbaalgos/sccinfo.hh | 23 +- src/tgbaalgos/se05.cc | 25 +- src/tgbaalgos/simulation.cc | 96 +++-- src/tgbaalgos/simulation.hh | 4 + src/tgbaalgos/stats.cc | 2 +- src/tgbaalgos/stripacc.cc | 4 +- src/tgbaalgos/tau03.cc | 43 +- src/tgbaalgos/tau03opt.cc | 111 +++-- src/tgbaalgos/weight.cc | 93 +--- src/tgbaalgos/weight.hh | 23 +- src/tgbaparse/tgbaparse.yy | 15 +- src/tgbatest/Makefile.am | 10 +- src/tgbatest/acc.cc | 107 +++++ src/tgbatest/acc.test | 63 +++ src/tgbatest/complementation.cc | 86 ++-- src/tgbatest/complementation.test | 17 +- src/tgbatest/degenlskip.test | 30 +- src/tgbatest/det.test | 20 +- src/tgbatest/dstar.test | 84 ++-- src/tgbatest/emptchk.cc | 2 +- src/tgbatest/explpro2.test | 6 +- src/tgbatest/explpro3.test | 6 +- src/tgbatest/explpro4.test | 6 +- src/tgbatest/explprod.test | 8 +- src/tgbatest/ltl2tgba.cc | 26 +- src/tgbatest/ltl2tgba.test | 2 +- src/tgbatest/maskacc.cc | 10 +- src/tgbatest/maskacc.test | 12 +- src/tgbatest/neverclaimread.test | 28 +- src/tgbatest/randtgba.cc | 4 +- src/tgbatest/readsave.test | 12 +- src/tgbatest/sim.test | 6 +- src/tgbatest/sim2.test | 4 +- src/tgbatest/spotlbtt.test | 4 +- src/tgbatest/tgbaread.test | 6 +- src/tgbatest/tripprod.test | 14 +- 125 files changed, 1950 insertions(+), 3254 deletions(-) create mode 100644 src/tgba/acc.hh delete mode 100644 src/tgba/tgbakvcomplement.cc delete mode 100644 src/tgba/tgbakvcomplement.hh delete mode 100644 src/tgba/tgbasgba.cc delete mode 100644 src/tgba/tgbasgba.hh create mode 100644 src/tgbatest/acc.cc create mode 100755 src/tgbatest/acc.test diff --git a/NEWS b/NEWS index d55e19aa3..128f772f2 100644 --- a/NEWS +++ b/NEWS @@ -56,12 +56,35 @@ New in spot 1.99a (not yet released) Where the virtual calls to done() and delete have been avoided. - - tgba::support_variables() and tgba::compute_support_variables() + - tgba::succ_iter() now takes only one argument. The optional + global_state and global_automaton arguments have been removed. + + - The following methods have been removed from the TGBA interface and + all their subclasses: + - tgba::support_variables() + - tgba::compute_support_variables() + - tgba::all_acceptance_conditions() // use acc().accepting(...) + - tgba::neg_acceptance_conditions() + - tgba::number_of_acceptance_conditions() // use acc().num_sets() methods have been removed from the TGBA interface and all subclasses. - - tgba::succ_iter() now takes only one argument. The optional - global_state and global_automaton arguments have been removed. + - Membership to acceptance sets are now stored using bit sets, + currently limited to 32 bits. Each TGBA has a acc() method that + returns a reference to an acceptance object (of type + spot::acc_cond), able to operate on acceptance marks + (spot::acc_cond::mark_t). + + Instead of writing + i->current_acceptance_conditions() == aut->all_acceptance_conditions() + we now write + aut->acc().accepting(i->current_acceptance_conditions()) + + Similarly, + aut->number_of_acceptance_conditions() + is now + aut->acc().num_sets() + * Removed features @@ -87,6 +110,15 @@ New in spot 1.99a (not yet released) automata (when viewed explictely), using the above and non longuer supported tgba_bdd_concrete class. + - Our implementation of the Kupferman-Vardi complementation has + been removed: it was useless in practice beause of the size of + the automata built, and it did not survive the conversion of + acceptance sets from BDDs to bitsets. + + - Conversion from TGBA to state-based Generalized Büchi automata + has been removed too, because it was only used by the KV + complementation. + New in spot 1.2.5a (not yet released) * New features: diff --git a/iface/dve2/dve2.cc b/iface/dve2/dve2.cc index e3d499e7d..9122f1796 100644 --- a/iface/dve2/dve2.cc +++ b/iface/dve2/dve2.cc @@ -606,7 +606,8 @@ namespace spot dve2_kripke(const dve2_interface* d, const bdd_dict_ptr& dict, const prop_set* ps, const ltl::formula* dead, int compress) - : d_(d), + : kripke(dict), + d_(d), state_size_(d_->get_state_variable_count()), dict_(dict), ps_(ps), compress_(compress == 0 ? 0 diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index 873a78c4b..61f93738e 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -1047,7 +1047,7 @@ namespace st->states = s.states; st->edges = s.transitions; st->transitions = s.sub_transitions; - st->acc = res->number_of_acceptance_conditions(); + st->acc = res->acc().num_sets(); spot::scc_map m(res); m.build_map(); unsigned c = m.scc_count(); diff --git a/src/dstarparse/dra2ba.cc b/src/dstarparse/dra2ba.cc index fe41b347f..7bd241844 100644 --- a/src/dstarparse/dra2ba.cc +++ b/src/dstarparse/dra2ba.cc @@ -23,6 +23,7 @@ #include "tgbaalgos/reachiter.hh" #include "tgbaalgos/gtec/gtec.hh" #include "tgbaalgos/sccfilter.hh" +#include "tgbaalgos/dotty.hh" namespace spot { @@ -55,7 +56,7 @@ namespace spot { typedef std::list state_list; - // The function that takes aut and dra is first arguments are + // The functions that take aut and dra as first arguments are // either called on the main automaton, in which case dra->aut == // aut, or it is called on a sub-automaton in which case aut is a // masked version of dra->aut. So we should always explore the @@ -293,7 +294,7 @@ namespace spot tgba_digraph_ptr out_; const state_set& final_; size_t num_states_; - bdd acc_; + acc_cond::mark_t acc_; const scc_map& sm_; const std::vector& realizable_; }; diff --git a/src/dstarparse/nsa2tgba.cc b/src/dstarparse/nsa2tgba.cc index 0aeca8fe7..da98b98d3 100644 --- a/src/dstarparse/nsa2tgba.cc +++ b/src/dstarparse/nsa2tgba.cc @@ -129,7 +129,7 @@ namespace spot for (auto& t: a->out(s.s)) { bitvect* pend = 0; - bdd acc = bddfalse; + acc_cond::mark_t acc = 0U; if (s.pend) { pend = s.pend->clone(); diff --git a/src/graphtest/tgbagraph.cc b/src/graphtest/tgbagraph.cc index 0ec15ce2e..e5fe33f9a 100644 --- a/src/graphtest/tgbagraph.cc +++ b/src/graphtest/tgbagraph.cc @@ -35,21 +35,20 @@ void f1() auto* f2 = e.require("p2"); bdd p1 = bdd_ithvar(d->register_proposition(f1, tg)); bdd p2 = bdd_ithvar(d->register_proposition(f2, tg)); - bdd a1 = bdd_ithvar(d->register_acceptance_variable(f1, tg)); - bdd a2 = bdd_ithvar(d->register_acceptance_variable(f2, tg)); + tg->acc().add_sets(2); f1->destroy(); f2->destroy(); auto s1 = tg->new_state(); auto s2 = tg->new_state(); auto s3 = tg->new_state(); - tg->new_transition(s1, s1, bddfalse, bddfalse); - tg->new_transition(s1, s2, p1, bddfalse); - tg->new_transition(s1, s3, p2, (!a1) & a2); - tg->new_transition(s2, s3, p1 & p2, a1 & !a2); - tg->new_transition(s3, s1, p1 | p2, ((!a1) & a2) | (a1 & !a2)); - tg->new_transition(s3, s2, p1 >> p2, bddfalse); - tg->new_transition(s3, s3, bddtrue, ((!a1) & a2) | (a1 & !a2)); + tg->new_transition(s1, s1, bddfalse, 0U); + tg->new_transition(s1, s2, p1, 0U); + tg->new_transition(s1, s3, p2, tg->acc().mark(1)); + tg->new_transition(s2, s3, p1 & p2, tg->acc().mark(0)); + tg->new_transition(s3, s1, p1 | p2, tg->acc().marks({0, 1})); + tg->new_transition(s3, s2, p1 >> p2, 0U); + tg->new_transition(s3, s3, bddtrue, tg->acc().marks({0, 1})); spot::dotty_reachable(std::cout, tg); @@ -69,9 +68,10 @@ void f1() spot::dotty_reachable(std::cout, tg); } - tg->new_transition(s3, s1, p1 | p2, ((!a1) & a2) | (a1 & !a2)); - tg->new_transition(s3, s2, p1 >> p2, bddfalse); - tg->new_transition(s3, s1, bddtrue, ((!a1) & a2) | (a1 & !a2)); + auto all = tg->acc().marks({0, 1}); + tg->new_transition(s3, s1, p1 | p2, all); + tg->new_transition(s3, s2, p1 >> p2, 0U); + tg->new_transition(s3, s1, bddtrue, all); std::cerr << tg->num_transitions() << '\n'; assert(tg->num_transitions() == 7); diff --git a/src/graphtest/tgbagraph.test b/src/graphtest/tgbagraph.test index 5276045fb..753b97214 100755 --- a/src/graphtest/tgbagraph.test +++ b/src/graphtest/tgbagraph.test @@ -37,76 +37,76 @@ digraph G { 0 [label="", style=invis, height=0] 0 -> 1 1 [label="0"] - 1 -> 1 [label="0\n"] - 1 -> 2 [label="p1\n"] - 1 -> 3 [label="p2\n{Acc[p2]}"] + 1 -> 1 [label="0"] + 1 -> 2 [label="p1"] + 1 -> 3 [label="p2\n{1}"] 2 [label="1"] - 2 -> 3 [label="p1 & p2\n{Acc[p1]}"] + 2 -> 3 [label="p1 & p2\n{0}"] 3 [label="2"] - 3 -> 1 [label="p1 | p2\n{Acc[p2], Acc[p1]}"] - 3 -> 2 [label="!p1 | p2\n"] - 3 -> 3 [label="1\n{Acc[p2], Acc[p1]}"] + 3 -> 1 [label="p1 | p2\n{0,1}"] + 3 -> 2 [label="!p1 | p2"] + 3 -> 3 [label="1\n{0,1}"] } digraph G { 0 [label="", style=invis, height=0] 0 -> 1 1 [label="0"] - 1 -> 1 [label="0\n"] - 1 -> 2 [label="p1\n"] - 1 -> 3 [label="p2\n{Acc[p2]}"] + 1 -> 1 [label="0"] + 1 -> 2 [label="p1"] + 1 -> 3 [label="p2\n{1}"] 2 [label="1"] - 2 -> 3 [label="p1 & p2\n{Acc[p1]}"] + 2 -> 3 [label="p1 & p2\n{0}"] 3 [label="2"] - 3 -> 1 [label="p1 | p2\n{Acc[p2], Acc[p1]}"] + 3 -> 1 [label="p1 | p2\n{0,1}"] } digraph G { 0 [label="", style=invis, height=0] 0 -> 1 1 [label="0"] - 1 -> 1 [label="0\n"] - 1 -> 2 [label="p1\n"] - 1 -> 3 [label="p2\n{Acc[p2]}"] + 1 -> 1 [label="0"] + 1 -> 2 [label="p1"] + 1 -> 3 [label="p2\n{1}"] 2 [label="1"] - 2 -> 3 [label="p1 & p2\n{Acc[p1]}"] + 2 -> 3 [label="p1 & p2\n{0}"] 3 [label="2"] } digraph G { 0 [label="", style=invis, height=0] 0 -> 1 1 [label="0"] - 1 -> 1 [label="0\n"] - 1 -> 2 [label="p1\n"] - 1 -> 3 [label="p2\n{Acc[p2]}"] + 1 -> 1 [label="0"] + 1 -> 2 [label="p1"] + 1 -> 3 [label="p2\n{1}"] 2 [label="1"] - 2 -> 3 [label="p1 & p2\n{Acc[p1]}"] + 2 -> 3 [label="p1 & p2\n{0}"] 3 [label="2"] - 3 -> 1 [label="p1 | p2\n{Acc[p2], Acc[p1]}"] - 3 -> 2 [label="!p1 | p2\n"] - 3 -> 1 [label="1\n{Acc[p2], Acc[p1]}"] + 3 -> 1 [label="p1 | p2\n{0,1}"] + 3 -> 2 [label="!p1 | p2"] + 3 -> 1 [label="1\n{0,1}"] } digraph G { 0 [label="", style=invis, height=0] 0 -> 1 1 [label="0"] - 1 -> 2 [label="p1\n"] - 1 -> 3 [label="p2\n{Acc[p2]}"] + 1 -> 2 [label="p1"] + 1 -> 3 [label="p2\n{1}"] 2 [label="1"] - 2 -> 3 [label="p1 & p2\n{Acc[p1]}"] + 2 -> 3 [label="p1 & p2\n{0}"] 3 [label="2"] - 3 -> 1 [label="1\n{Acc[p2], Acc[p1]}"] - 3 -> 2 [label="!p1 | p2\n"] + 3 -> 1 [label="1\n{0,1}"] + 3 -> 2 [label="!p1 | p2"] } digraph G { 0 [label="", style=invis, height=0] 0 -> 1 1 [label="0"] - 1 -> 2 [label="p1\n"] - 1 -> 3 [label="p2\n{Acc[p2]}"] + 1 -> 2 [label="p1"] + 1 -> 3 [label="p2\n{1}"] 2 [label="1"] - 2 -> 3 [label="p1 & p2\n{Acc[p1]}"] + 2 -> 3 [label="p1 & p2\n{0}"] 3 [label="2"] - 3 -> 1 [label="1\n{Acc[p2], Acc[p1]}"] - 3 -> 2 [label="!p1 | p2\n"] + 3 -> 1 [label="1\n{0,1}"] + 3 -> 2 [label="!p1 | p2"] } EOF diff --git a/src/kripke/fairkripke.cc b/src/kripke/fairkripke.cc index 10671d494..87209eb01 100644 --- a/src/kripke/fairkripke.cc +++ b/src/kripke/fairkripke.cc @@ -22,8 +22,8 @@ namespace spot { - fair_kripke_succ_iterator::fair_kripke_succ_iterator(const bdd& cond, - const bdd& acc_cond) + fair_kripke_succ_iterator::fair_kripke_succ_iterator + (const bdd& cond, acc_cond::mark_t acc_cond) : cond_(cond), acc_cond_(acc_cond) { } @@ -40,7 +40,7 @@ namespace spot return cond_; } - bdd + acc_cond::mark_t fair_kripke_succ_iterator::current_acceptance_conditions() const { // Do not assert(!done()) here. It is OK to call diff --git a/src/kripke/fairkripke.hh b/src/kripke/fairkripke.hh index 2f9590e8b..1693c0e72 100644 --- a/src/kripke/fairkripke.hh +++ b/src/kripke/fairkripke.hh @@ -52,14 +52,14 @@ namespace spot /// The \a cond and \a acc_cond arguments will be those returned /// by fair_kripke_succ_iterator::current_condition(), /// and fair_kripke_succ_iterator::current_acceptance_conditions(). - fair_kripke_succ_iterator(const bdd& cond, const bdd& acc_cond); + fair_kripke_succ_iterator(const bdd& cond, acc_cond::mark_t acc_cond); virtual ~fair_kripke_succ_iterator(); virtual bdd current_condition() const; - virtual bdd current_acceptance_conditions() const; + virtual acc_cond::mark_t current_acceptance_conditions() const; protected: bdd cond_; - bdd acc_cond_; + acc_cond::mark_t acc_cond_; }; /// \ingroup kripke @@ -86,16 +86,22 @@ namespace spot /// class and need not be defined. /// /// See also spot::fair_kripke_succ_iterator. - class SPOT_API fair_kripke : public tgba + class SPOT_API fair_kripke: public tgba { public: + fair_kripke(const bdd_dict_ptr& d) + : tgba(d) + { + } + /// \brief The condition that label the state \a s. /// /// This should be a conjunction of atomic propositions. virtual bdd state_condition(const state* s) const = 0; /// \brief The set of acceptance conditions that label the state \a s. - virtual bdd state_acceptance_conditions(const state* s) const = 0; + virtual acc_cond::mark_t + state_acceptance_conditions(const state* s) const = 0; protected: virtual bdd compute_support_conditions(const state* s) const; diff --git a/src/kripke/kripke.cc b/src/kripke/kripke.cc index 1dd937cf3..810c76d8d 100644 --- a/src/kripke/kripke.cc +++ b/src/kripke/kripke.cc @@ -34,33 +34,21 @@ namespace spot return cond_; } - bdd + acc_cond::mark_t kripke_succ_iterator::current_acceptance_conditions() const { // Do not assert(!done()) here. It is OK to call // this function on a state without successor. - return bddfalse; + return 0U; } kripke::~kripke() { } - bdd + acc_cond::mark_t kripke::state_acceptance_conditions(const state*) const { - return bddtrue; + return 0U; } - - bdd kripke::all_acceptance_conditions() const - { - // There is no acceptance conditions. - return bddfalse; - } - - bdd kripke::neg_acceptance_conditions() const - { - return bddtrue; - } - } diff --git a/src/kripke/kripke.hh b/src/kripke/kripke.hh index abf87c541..9e26a1d07 100644 --- a/src/kripke/kripke.hh +++ b/src/kripke/kripke.hh @@ -61,7 +61,7 @@ namespace spot virtual ~kripke_succ_iterator(); virtual bdd current_condition() const; - virtual bdd current_acceptance_conditions() const; + virtual acc_cond::mark_t current_acceptance_conditions() const; protected: bdd cond_; }; @@ -92,11 +92,15 @@ namespace spot class SPOT_API kripke: public fair_kripke { public: + kripke(const bdd_dict_ptr& d) + : fair_kripke(d) + { + } + + virtual ~kripke(); - virtual bdd state_acceptance_conditions(const state*) const; - virtual bdd neg_acceptance_conditions() const; - virtual bdd all_acceptance_conditions() const; + virtual acc_cond::mark_t state_acceptance_conditions(const state*) const; }; diff --git a/src/kripke/kripkeexplicit.cc b/src/kripke/kripkeexplicit.cc index 4e5f5eaed..9d7a4f86c 100644 --- a/src/kripke/kripkeexplicit.cc +++ b/src/kripke/kripkeexplicit.cc @@ -128,8 +128,8 @@ namespace spot kripke_explicit::kripke_explicit(const bdd_dict_ptr& dict, state_kripke* init) - : dict_(dict), - init_ (init) + : kripke(dict), + init_(init) { } @@ -148,7 +148,7 @@ namespace spot kripke_explicit::~kripke_explicit() { - dict_->unregister_all_my_variables(this); + get_dict()->unregister_all_my_variables(this); std::map::iterator it; for (it = ns_nodes_.begin(); it != ns_nodes_.end(); ++it) { @@ -163,12 +163,6 @@ namespace spot return init_; } - bdd_dict_ptr - kripke_explicit::get_dict() const - { - return dict_; - } - // FIXME: Change the bddtrue. kripke_explicit_succ_iterator* kripke_explicit::succ_iter(const spot::state* st) const @@ -269,7 +263,7 @@ namespace spot void kripke_explicit::add_condition(const ltl::formula* f, std::string on_me) { - add_conditions(formula_to_bdd(f, dict_, this), on_me); + add_conditions(formula_to_bdd(f, get_dict(), this), on_me); f->destroy(); } diff --git a/src/kripke/kripkeexplicit.hh b/src/kripke/kripkeexplicit.hh index fb0f1f684..370769225 100644 --- a/src/kripke/kripkeexplicit.hh +++ b/src/kripke/kripkeexplicit.hh @@ -117,7 +117,6 @@ namespace spot kripke_explicit(const bdd_dict_ptr&, state_kripke* = nullptr); ~kripke_explicit(); - bdd_dict_ptr get_dict() const; state_kripke* get_init_state() const; /// \brief Allow to get an iterator on the state we passed in @@ -174,7 +173,6 @@ namespace spot void add_transition(state_kripke* source, const state_kripke* dest); - bdd_dict_ptr dict_; state_kripke* init_; std::map ns_nodes_; std::map sn_nodes_; diff --git a/src/misc/hash.hh b/src/misc/hash.hh index 9a8ae8cb8..e789c995c 100644 --- a/src/misc/hash.hh +++ b/src/misc/hash.hh @@ -82,8 +82,11 @@ namespace spot template std::size_t operator()(const std::pair &p) const { - return wang32_hash(static_cast(p.first) ^ - static_cast(p.second)); + std::hash th; + std::hash uh; + + return wang32_hash(static_cast(th(p.first)) ^ + static_cast(uh(p.second))); } }; diff --git a/src/neverparse/neverclaimparse.yy b/src/neverparse/neverclaimparse.yy index 3e777a91f..11725244e 100644 --- a/src/neverparse/neverclaimparse.yy +++ b/src/neverparse/neverclaimparse.yy @@ -169,17 +169,16 @@ state: namer->new_transition(*$1, *$1, bddtrue, !strncmp("accept", $1->c_str(), 6) ? - result->all_acceptance_conditions() : - static_cast(bddfalse)); + result->acc().all_sets() : + spot::acc_cond::mark_t(0U)); delete $1; } | ident_list { delete $1; } | ident_list "false" { delete $1; } | ident_list transition_block { - bdd acc = !strncmp("accept", $1->c_str(), 6) ? - result->all_acceptance_conditions() : - static_cast(bddfalse); + auto acc = !strncmp("accept", $1->c_str(), 6) ? + result->acc().all_sets() : spot::acc_cond::mark_t(0U); for (auto& p: *$2) namer->new_transition(*$1, *p.second, *p.first, acc); // Free the list diff --git a/src/priv/accmap.hh b/src/priv/accmap.hh index 29e1f2ece..0710422b0 100644 --- a/src/priv/accmap.hh +++ b/src/priv/accmap.hh @@ -34,10 +34,9 @@ namespace spot bdd_dict_ptr dict_; tgba_digraph_ptr aut_; ltl::environment& env_; - bdd neg_; acc_mapper_common(const tgba_digraph_ptr& aut, ltl::environment& env) - : dict_(aut->get_dict()), aut_(aut), env_(env), neg_(bddtrue) + : dict_(aut->get_dict()), aut_(aut), env_(env) { } @@ -46,17 +45,11 @@ namespace spot { return env_; } - - // Commit all acceptance set to the automaton. - void commit() - { - aut_->set_acceptance_conditions(neg_); - } }; class acc_mapper_string: public acc_mapper_common { - std::unordered_map map_; + std::unordered_map map_; public: acc_mapper_string(const tgba_digraph_ptr& aut, @@ -72,24 +65,17 @@ namespace spot auto i = map_.find(name); if (i != map_.end()) return true; - auto f = env_.require(name); - if (!f) - return false; - int v = dict_->register_acceptance_variable(f, aut_); - f->destroy(); + auto v = aut_->acc().add_set(); map_[name] = v; - neg_ &= bdd_nithvar(v); return true; } - std::pair lookup(std::string name) const + std::pair lookup(std::string name) const { auto p = map_.find(name); if (p == map_.end()) - return std::make_pair(false, bddfalse); - return std::make_pair(true, bdd_compose(neg_, - bdd_nithvar(p->second), - p->second)); + return std::make_pair(false, 0U); + return std::make_pair(true, aut_->acc().marks({p->second})); } }; @@ -97,42 +83,23 @@ namespace spot // The acceptance sets are named using count consecutive integers. class acc_mapper_consecutive_int: public acc_mapper_common { - protected: - std::vector vec_; - std::map map_; - public: acc_mapper_consecutive_int(const tgba_digraph_ptr& aut, unsigned count, ltl::environment& env = ltl::default_environment::instance()) - : acc_mapper_common(aut, env), vec_(count) + : acc_mapper_common(aut, env) { - std::vector vmap(count); - for (unsigned n = 0; n < count; ++n) - { - std::ostringstream s; - s << n; - auto f = env.require(s.str()); - int v = dict_->register_acceptance_variable(f, aut_); - f->destroy(); - vmap[n] = v; - neg_ &= bdd_nithvar(v); - } - for (unsigned n = 0; n < count; ++n) - { - int v = vmap[n]; - vec_[n] = bdd_compose(neg_, bdd_nithvar(v), v); - } - commit(); + std::vector vmap(count); + aut->acc().add_sets(count); } - std::pair lookup(unsigned n) + std::pair lookup(unsigned n) { - if (n < vec_.size()) - return std::make_pair(true, vec_[n]); + if (n < aut_->acc().num_sets()) + return std::make_pair(true, aut_->acc().marks({n})); else - return std::make_pair(false, bddfalse); + return std::make_pair(false, 0U); } }; @@ -141,7 +108,7 @@ namespace spot class acc_mapper_int: public acc_mapper_consecutive_int { unsigned used_; - std::map map_; + std::map map_; public: acc_mapper_int(const tgba_digraph_ptr& aut, @@ -152,18 +119,18 @@ namespace spot { } - std::pair lookup(unsigned n) + std::pair lookup(unsigned n) { auto p = map_.find(n); if (p != map_.end()) return std::make_pair(true, p->second); - if (used_ < vec_.size()) + if (used_ < aut_->acc().num_sets()) { - bdd res = vec_[used_++]; + auto res = aut_->acc().marks({used_++}); map_[n] = res; return std::make_pair(true, res); } - return std::make_pair(false, bddfalse); + return std::make_pair(false, 0U); } }; } diff --git a/src/ta/ta.cc b/src/ta/ta.cc index c76517a4b..17c62aff9 100644 --- a/src/ta/ta.cc +++ b/src/ta/ta.cc @@ -28,7 +28,7 @@ namespace spot { index = i; is_accepting = false; - condition = bddfalse; + condition = 0U; } scc_stack_ta::connected_component& diff --git a/src/ta/ta.hh b/src/ta/ta.hh index e86f783c6..75b49962b 100644 --- a/src/ta/ta.hh +++ b/src/ta/ta.hh @@ -76,8 +76,15 @@ namespace spot class SPOT_API ta { + protected: + acc_cond acc_; public: + ta(const bdd_dict_ptr& d) + : acc_(d) + { + } + virtual ~ta() { @@ -128,8 +135,11 @@ namespace spot /// This is useful when dealing with several automata (which /// may use the same BDD variable for different formula), /// or simply when printing. - virtual bdd_dict_ptr - get_dict() const = 0; + bdd_dict_ptr + get_dict() const + { + return acc_.get_dict(); + } /// \brief Format the state as a string for printing. /// @@ -160,17 +170,16 @@ namespace spot virtual void free_state(const spot::state* s) const = 0; - /// \brief Return the set of all acceptance conditions used - /// by this automaton - /// (for Generalized form: Transition-based Generalized Testing Automata). - /// - /// The goal of the emptiness check is to ensure that - /// a strongly connected component walks through each - /// of these acceptiong conditions. I.e., the union - /// of the acceptiong conditions of all transition in - /// the SCC should be equal to the result of this function. - virtual bdd - all_acceptance_conditions() const = 0; + + const acc_cond& acc() const + { + return acc_; + } + + acc_cond& acc() + { + return acc_; + } }; @@ -206,7 +215,7 @@ namespace spot virtual bdd current_condition() const = 0; - bdd + acc_cond::mark_t current_acceptance_conditions() const = 0; }; @@ -228,7 +237,7 @@ namespace spot /// The bdd condition is the union of all acceptance conditions of /// transitions which connect the states of the connected component. - bdd condition; + acc_cond::mark_t condition; std::list rem; }; diff --git a/src/ta/taexplicit.cc b/src/ta/taexplicit.cc index 06e7262f8..c4b08f3bc 100644 --- a/src/ta/taexplicit.cc +++ b/src/ta/taexplicit.cc @@ -97,7 +97,7 @@ namespace spot return (*i_)->condition; } - bdd + acc_cond::mark_t ta_explicit_succ_iterator::current_acceptance_conditions() const { assert(!done()); @@ -352,13 +352,14 @@ namespace spot ta_explicit::ta_explicit(const const_tgba_ptr& tgba, - bdd all_acceptance_conditions, + unsigned n_acc, state_ta_explicit* artificial_initial_state): + ta(tgba->get_dict()), tgba_(tgba), - all_acceptance_conditions_(all_acceptance_conditions), artificial_initial_state_(artificial_initial_state) { get_dict()->register_all_variables_of(&tgba_, this); + acc().add_sets(n_acc); if (artificial_initial_state != 0) { state_ta_explicit* is = add_state(artificial_initial_state); @@ -403,7 +404,7 @@ namespace spot { state_ta_explicit* i = down_cast(get_artificial_initial_state()); - create_transition(i, condition, bddfalse, s); + create_transition(i, condition, 0U, s); } } @@ -420,7 +421,7 @@ namespace spot void ta_explicit::create_transition(state_ta_explicit* source, bdd condition, - bdd acceptance_conditions, + acc_cond::mark_t acceptance_conditions, state_ta_explicit* dest, bool add_at_beginning) { state_ta_explicit::transition* t = new state_ta_explicit::transition; diff --git a/src/ta/taexplicit.hh b/src/ta/taexplicit.hh index 4810192f9..02c57e326 100644 --- a/src/ta/taexplicit.hh +++ b/src/ta/taexplicit.hh @@ -41,7 +41,8 @@ namespace spot class SPOT_API ta_explicit : public ta { public: - ta_explicit(const const_tgba_ptr& tgba, bdd all_acceptance_conditions, + ta_explicit(const const_tgba_ptr& tgba, + unsigned n_acc, state_ta_explicit* artificial_initial_state = 0); const_tgba_ptr @@ -55,8 +56,9 @@ namespace spot void create_transition(state_ta_explicit* source, bdd condition, - bdd acceptance_conditions, state_ta_explicit* dest, - bool add_at_beginning = false); + acc_cond::mark_t acceptance_conditions, + state_ta_explicit* dest, + bool add_at_beginning = false); void delete_stuttering_transitions(); @@ -115,27 +117,12 @@ namespace spot return states_set_; } - /// \brief Return the set of all acceptance conditions used - /// by this automaton. - /// - /// The goal of the emptiness check is to ensure that - /// a strongly connected component walks through each - /// of these acceptiong conditions. I.e., the union - /// of the acceptiong conditions of all transition in - /// the SCC should be equal to the result of this function. - bdd - all_acceptance_conditions() const - { - return all_acceptance_conditions_; - } - private: // Disallow copy. ta_explicit(const ta_explicit& other) SPOT_DELETED; ta_explicit& operator=(const ta_explicit& other) SPOT_DELETED; const_tgba_ptr tgba_; - bdd all_acceptance_conditions_; state_ta_explicit* artificial_initial_state_; ta::states_set_t states_set_; ta::states_set_t initial_states_set_; @@ -152,7 +139,7 @@ namespace spot struct transition { bdd condition; - bdd acceptance_conditions; + acc_cond::mark_t acceptance_conditions; state_ta_explicit* dest; }; @@ -255,7 +242,7 @@ namespace spot virtual bdd current_condition() const; - virtual bdd + virtual acc_cond::mark_t current_acceptance_conditions() const; private: @@ -267,13 +254,11 @@ namespace spot typedef std::shared_ptr const_ta_explicit_ptr; inline ta_explicit_ptr make_ta_explicit(const const_tgba_ptr& tgba, - bdd all_acceptance_conditions, + unsigned n_acc, state_ta_explicit* artificial_initial_state = 0) { - return std::make_shared(tgba, - all_acceptance_conditions, - artificial_initial_state); + return std::make_shared(tgba, n_acc, artificial_initial_state); } } diff --git a/src/ta/taproduct.cc b/src/ta/taproduct.cc index 97c7bb763..2bb7bded7 100644 --- a/src/ta/taproduct.cc +++ b/src/ta/taproduct.cc @@ -190,7 +190,7 @@ namespace spot //if stuttering transition, the TA automata stays in the same state current_state_ = new state_ta_product(source_->get_ta_state(), kripke_current_dest_state->clone()); - current_acceptance_conditions_ = bddfalse; + current_acceptance_conditions_ = 0U; return true; } @@ -232,7 +232,7 @@ namespace spot return current_condition_; } - bdd + acc_cond::mark_t ta_succ_iterator_product::current_acceptance_conditions() const { return current_acceptance_conditions_; @@ -244,6 +244,7 @@ namespace spot ta_product::ta_product(const const_ta_ptr& testing_automata, const const_kripke_ptr& kripke_structure): + ta(testing_automata->get_dict()), dict_(testing_automata->get_dict()), ta_(testing_automata), kripke_(kripke_structure) @@ -387,12 +388,6 @@ namespace spot return is_hole_state; } - bdd - ta_product::all_acceptance_conditions() const - { - return get_ta()->all_acceptance_conditions(); - } - bdd ta_product::get_state_condition(const spot::state* s) const { diff --git a/src/ta/taproduct.hh b/src/ta/taproduct.hh index 70dc39bc2..f45e383f1 100644 --- a/src/ta/taproduct.hh +++ b/src/ta/taproduct.hh @@ -93,7 +93,7 @@ namespace spot bdd current_condition() const; - bdd + acc_cond::mark_t current_acceptance_conditions() const; /// \brief Return true if the changeset of the current transition is empty @@ -120,7 +120,7 @@ namespace spot tgba_succ_iterator* kripke_succ_it_; state_ta_product* current_state_; bdd current_condition_; - bdd current_acceptance_conditions_; + acc_cond::mark_t current_acceptance_conditions_; bool is_stuttering_transition_; bdd kripke_source_condition; state * kripke_current_dest_state; @@ -174,9 +174,6 @@ namespace spot virtual bdd get_state_condition(const spot::state* s) const; - virtual bdd - all_acceptance_conditions() const; - virtual void free_state(const spot::state* s) const; diff --git a/src/ta/tgta.cc b/src/ta/tgta.cc index f12211e05..d0bf8dc7f 100644 --- a/src/ta/tgta.cc +++ b/src/ta/tgta.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement +// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -22,11 +22,9 @@ namespace spot { - - tgta::tgta() - {}; - tgta::~tgta() - {}; - - + tgta::tgta(const bdd_dict_ptr& d) + : tgba(d) + {}; + tgta::~tgta() + {}; } diff --git a/src/ta/tgta.hh b/src/ta/tgta.hh index a7bcb4b95..90c29ff87 100644 --- a/src/ta/tgta.hh +++ b/src/ta/tgta.hh @@ -62,9 +62,9 @@ namespace spot { protected: - tgta(); - public: + tgta(const bdd_dict_ptr& d); + public: virtual ~tgta(); diff --git a/src/ta/tgtaexplicit.cc b/src/ta/tgtaexplicit.cc index e02ccc788..42ee7c6b9 100644 --- a/src/ta/tgtaexplicit.cc +++ b/src/ta/tgtaexplicit.cc @@ -30,10 +30,10 @@ namespace spot { tgta_explicit::tgta_explicit(const const_tgba_ptr& tgba, - bdd all_acceptance_conditions, + unsigned n_acc, state_ta_explicit* artificial_initial_state) : - ta_(make_ta_explicit(tgba, all_acceptance_conditions, - artificial_initial_state)) + tgta(tgba->get_dict()), + ta_(make_ta_explicit(tgba, n_acc, artificial_initial_state)) { } @@ -63,18 +63,6 @@ namespace spot return ta_->get_dict(); } - bdd - tgta_explicit::all_acceptance_conditions() const - { - return ta_->all_acceptance_conditions(); - } - - bdd - tgta_explicit::neg_acceptance_conditions() const - { - return ta_->get_tgba()->neg_acceptance_conditions(); - } - std::string tgta_explicit::format_state(const spot::state* s) const { diff --git a/src/ta/tgtaexplicit.hh b/src/ta/tgtaexplicit.hh index fe37c9c76..30370c279 100644 --- a/src/ta/tgtaexplicit.hh +++ b/src/ta/tgtaexplicit.hh @@ -39,7 +39,7 @@ namespace spot { public: tgta_explicit(const const_tgba_ptr& tgba, - bdd all_acceptance_conditions, + unsigned n_acc, state_ta_explicit* artificial_initial_state); // tgba interface @@ -54,9 +54,6 @@ namespace spot const_ta_explicit_ptr get_ta() const { return ta_; } ta_explicit_ptr get_ta() { return ta_; } - virtual bdd all_acceptance_conditions() const; - virtual bdd neg_acceptance_conditions() const; - virtual std::string format_state(const spot::state* s) const; virtual tgba_succ_iterator* @@ -71,12 +68,11 @@ namespace spot typedef std::shared_ptr const_tgta_explicit_ptr; inline tgta_explicit_ptr make_tgta_explicit(const const_tgba_ptr& tgba, - bdd all_acceptance_conditions, + unsigned n_acc, state_ta_explicit* artificial_initial_state = 0) { - return std::make_shared(tgba, - all_acceptance_conditions, + return std::make_shared(tgba, n_acc, artificial_initial_state); } } diff --git a/src/ta/tgtaproduct.cc b/src/ta/tgtaproduct.cc index dab27a394..068baec51 100644 --- a/src/ta/tgtaproduct.cc +++ b/src/ta/tgtaproduct.cc @@ -207,7 +207,7 @@ namespace spot kripke_current_dest_state->clone(), tgta_succ_it_->current_state(), pool_); current_acceptance_conditions_ - = tgta_succ_it_->current_acceptance_conditions(); + = tgta_succ_it_->current_acceptance_conditions(); return true; } @@ -244,7 +244,7 @@ namespace spot return current_condition_; } - bdd + acc_cond::mark_t tgta_succ_iterator_product::current_acceptance_conditions() const { return current_acceptance_conditions_; diff --git a/src/ta/tgtaproduct.hh b/src/ta/tgtaproduct.hh index 89225027a..1f50903c9 100644 --- a/src/ta/tgtaproduct.hh +++ b/src/ta/tgtaproduct.hh @@ -72,7 +72,7 @@ namespace spot bdd current_condition() const; - bdd + acc_cond::mark_t current_acceptance_conditions() const; private: @@ -96,7 +96,7 @@ namespace spot tgba_succ_iterator* kripke_succ_it_; state_product* current_state_; bdd current_condition_; - bdd current_acceptance_conditions_; + acc_cond::mark_t current_acceptance_conditions_; bdd kripke_source_condition; state* kripke_current_dest_state; }; diff --git a/src/taalgos/dotty.cc b/src/taalgos/dotty.cc index 3044325e1..692eb9217 100644 --- a/src/taalgos/dotty.cc +++ b/src/taalgos/dotty.cc @@ -106,9 +106,8 @@ namespace spot if (label.empty()) label = "{}"; - label += ("\n" + - bdd_format_accset(d, si->current_acceptance_conditions())); - + label += "\n"; + label += t_automata_->acc().format(si->current_acceptance_conditions()); os_ << " " << in << " -> " << out << " [label=\""; escape_str(os_, label); diff --git a/src/taalgos/emptinessta.cc b/src/taalgos/emptinessta.cc index bb65d6f3d..1b562d14b 100644 --- a/src/taalgos/emptinessta.cc +++ b/src/taalgos/emptinessta.cc @@ -54,7 +54,7 @@ namespace spot // * scc: (attribute) a stack of strongly connected components (SCC) // * arc, a stack of acceptance conditions between each of these SCC, - std::stack arc; + std::stack arc; // * h: a hash of all visited nodes, with their order, // (it is called "Hash" in Couvreur's paper) @@ -113,7 +113,7 @@ namespace spot } scc.push(++num); - arc.push(bddfalse); + arc.push(0U); ta_succ_iterator_product* iter = a_->succ_iter(init); iter->first(); @@ -194,7 +194,7 @@ namespace spot // Fetch the values destination state we are interested in... state* dest = succ->current_state(); - bdd acc_cond = succ->current_acceptance_conditions(); + auto acc_cond = succ->current_acceptance_conditions(); bool curr_is_livelock_hole_state_in_ta_component = (a_->is_hole_state_in_ta_component(curr)) @@ -284,8 +284,8 @@ namespace spot scc.top().condition |= acc_cond; scc.rem().splice(scc.rem().end(), rem); - bool is_accepting_sscc = (scc.top().is_accepting) - || (scc.top().condition == a_->all_acceptance_conditions()); + bool is_accepting_sscc = scc.top().is_accepting + || a_->acc().accepting(scc.top().condition); if (is_accepting_sscc) { @@ -294,25 +294,14 @@ namespace spot << a_->is_livelock_accepting_state(curr) << '\n'; trace << "PASS 1: scc.top().condition : " - << bdd_format_accset(a_->get_dict(), scc.top().condition) - << '\n'; + << scc.top().condition << '\n'; trace - << "PASS 1: a_->all_acceptance_conditions() : " - << (a_->all_acceptance_conditions()) << '\n'; + << "PASS 1: a_->acc().all_sets() : " + << (a_->acc().all_sets()) << '\n'; trace - << ("PASS 1 CYCLE and (scc.top().condition == " - "a_->all_acceptance_conditions()) : ") - << (scc.top().condition - == a_->all_acceptance_conditions()) << std::endl; - - trace - << "PASS 1: bddtrue: " << (a_->all_acceptance_conditions() - == bddtrue) << '\n'; - - trace - << "PASS 1: bddfalse: " << (a_->all_acceptance_conditions() - == bddfalse) << '\n'; - + << ("PASS 1 CYCLE and accepting? ") + << a_->acc().accepting(scc.top().condition) + << std::endl; clear(h, todo, ta_init_it_); return true; } diff --git a/src/taalgos/minimize.cc b/src/taalgos/minimize.cc index 352be7513..fb1123264 100644 --- a/src/taalgos/minimize.cc +++ b/src/taalgos/minimize.cc @@ -64,127 +64,149 @@ namespace spot return out; } - static std::string - format_hash_set(const hash_set* hs, const const_ta_ptr& aut) - { - std::ostringstream s; - dump_hash_set(hs, aut, s); - return s.str(); - } + static std::string + format_hash_set(const hash_set* hs, const const_ta_ptr& aut) + { + std::ostringstream s; + dump_hash_set(hs, aut, s); + return s.str(); + } - // From the base automaton and the list of sets, build the minimal - // automaton - static void - build_result(const const_ta_ptr& a, std::list& sets, - tgba_digraph_ptr result_tgba, const ta_explicit_ptr& result) - { - // For each set, create a state in the tgbaulting automaton. - // For a state s, state_num[s] is the number of the state in the minimal - // automaton. - hash_map state_num; - std::list::iterator sit; - unsigned num = 0; - for (sit = sets.begin(); sit != sets.end(); ++sit) - { - hash_set::iterator hit; - hash_set* h = *sit; - for (hit = h->begin(); hit != h->end(); ++hit) - state_num[*hit] = num; - result_tgba->new_state(); - ++num; - } + // From the base automaton and the list of sets, build the minimal + // automaton + static void + build_result(const const_ta_ptr& a, std::list& sets, + tgba_digraph_ptr result_tgba, const ta_explicit_ptr& result) + { + // For each set, create a state in the tgbaulting automaton. + // For a state s, state_num[s] is the number of the state in the minimal + // automaton. + hash_map state_num; + std::list::iterator sit; + unsigned num = 0; + for (sit = sets.begin(); sit != sets.end(); ++sit) + { + hash_set::iterator hit; + hash_set* h = *sit; + for (hit = h->begin(); hit != h->end(); ++hit) + state_num[*hit] = num; + result_tgba->new_state(); + ++num; + } - // For each transition in the initial automaton, add the corresponding - // transition in ta. + // For each transition in the initial automaton, add the corresponding + // transition in ta. - for (sit = sets.begin(); sit != sets.end(); ++sit) - { - hash_set::iterator hit; - hash_set* h = *sit; - hit = h->begin(); - const state* src = *hit; - unsigned src_num = state_num[src]; + for (sit = sets.begin(); sit != sets.end(); ++sit) + { + hash_set::iterator hit; + hash_set* h = *sit; + hit = h->begin(); + const state* src = *hit; + unsigned src_num = state_num[src]; - bdd tgba_condition = bddtrue; - bool is_initial_state = a->is_initial_state(src); - if ((a->get_artificial_initial_state() == 0) && is_initial_state) - tgba_condition = a->get_state_condition(src); - bool is_accepting_state = a->is_accepting_state(src); - bool is_livelock_accepting_state = - a->is_livelock_accepting_state(src); + bdd tgba_condition = bddtrue; + bool is_initial_state = a->is_initial_state(src); + if ((a->get_artificial_initial_state() == 0) && is_initial_state) + tgba_condition = a->get_state_condition(src); + bool is_accepting_state = a->is_accepting_state(src); + bool is_livelock_accepting_state = + a->is_livelock_accepting_state(src); - state_ta_explicit* new_src = - new state_ta_explicit(result_tgba->state_from_number(src_num), - tgba_condition, is_initial_state, - is_accepting_state, - is_livelock_accepting_state); + state_ta_explicit* new_src = + new state_ta_explicit(result_tgba->state_from_number(src_num), + tgba_condition, is_initial_state, + is_accepting_state, + is_livelock_accepting_state); - state_ta_explicit* ta_src = result->add_state(new_src); + state_ta_explicit* ta_src = result->add_state(new_src); - if (ta_src != new_src) - { - delete new_src; - } - else if (a->get_artificial_initial_state() != 0) - { - if (a->get_artificial_initial_state() == src) - result->set_artificial_initial_state(new_src); - } - else if (is_initial_state) - { - result->add_to_initial_states_set(new_src); - } + if (ta_src != new_src) + { + delete new_src; + } + else if (a->get_artificial_initial_state() != 0) + { + if (a->get_artificial_initial_state() == src) + result->set_artificial_initial_state(new_src); + } + else if (is_initial_state) + { + result->add_to_initial_states_set(new_src); + } - ta_succ_iterator* succit = a->succ_iter(src); + ta_succ_iterator* succit = a->succ_iter(src); - for (succit->first(); !succit->done(); succit->next()) - { - const state* dst = succit->current_state(); - hash_map::const_iterator i = state_num.find(dst); + for (succit->first(); !succit->done(); succit->next()) + { + const state* dst = succit->current_state(); + hash_map::const_iterator i = state_num.find(dst); - if (i == state_num.end()) // Ignore useless destinations. - continue; + if (i == state_num.end()) // Ignore useless destinations. + continue; - bdd tgba_condition = bddtrue; - is_initial_state = a->is_initial_state(dst); - if ((a->get_artificial_initial_state() == 0) && is_initial_state) - tgba_condition = a->get_state_condition(dst); - bool is_accepting_state = a->is_accepting_state(dst); - bool is_livelock_accepting_state = - a->is_livelock_accepting_state(dst); + bdd tgba_condition = bddtrue; + is_initial_state = a->is_initial_state(dst); + if ((a->get_artificial_initial_state() == 0) && is_initial_state) + tgba_condition = a->get_state_condition(dst); + bool is_accepting_state = a->is_accepting_state(dst); + bool is_livelock_accepting_state = + a->is_livelock_accepting_state(dst); - state_ta_explicit* new_dst = - new state_ta_explicit(result_tgba->state_from_number(i->second), - tgba_condition, is_initial_state, - is_accepting_state, - is_livelock_accepting_state); + state_ta_explicit* new_dst = + new state_ta_explicit + (result_tgba->state_from_number(i->second), + tgba_condition, is_initial_state, + is_accepting_state, + is_livelock_accepting_state); - state_ta_explicit* ta_dst = result->add_state(new_dst); + state_ta_explicit* ta_dst = result->add_state(new_dst); - if (ta_dst != new_dst) - { - delete new_dst; - } - else if (a->get_artificial_initial_state() != 0) - { - if (a->get_artificial_initial_state() == dst) - result->set_artificial_initial_state(new_dst); - } + if (ta_dst != new_dst) + { + delete new_dst; + } + else if (a->get_artificial_initial_state() != 0) + { + if (a->get_artificial_initial_state() == dst) + result->set_artificial_initial_state(new_dst); + } - else if (is_initial_state) - result->add_to_initial_states_set(new_dst); + else if (is_initial_state) + result->add_to_initial_states_set(new_dst); - result->create_transition(ta_src, succit->current_condition(), - succit->current_acceptance_conditions(), - ta_dst); - } - delete succit; - } - } + result->create_transition + (ta_src, succit->current_condition(), + succit->current_acceptance_conditions(), + ta_dst); + } + delete succit; + } + } static partition_t build_partition(const const_ta_ptr& ta_) { + unsigned num_sets = ta_->acc().num_sets(); + std::map m2b; + int acc_vars = ta_->get_dict()->register_anonymous_variables(num_sets, + &m2b); + auto mark_to_bdd = [&](acc_cond::mark_t m) -> bdd + { + auto i = m2b.find(m); + if (i != m2b.end()) + return i->second; + + bdd res = bddtrue; + for (unsigned n = 0; n < num_sets; ++n) + if (m.has(n)) + res &= bdd_ithvar(acc_vars + n); + else + res &= bdd_nithvar(acc_vars + n); + m2b.emplace_hint(i, m, res); + return res; + }; + partition_t cur_run; partition_t next_run; @@ -237,7 +259,7 @@ namespace spot // Use bdd variables to number sets. set_num is the first variable // available. unsigned set_num = - ta_->get_dict()->register_anonymous_variables(size, ta_); + ta_->get_dict()->register_anonymous_variables(size, &m2b); std::set free_var; for (unsigned i = set_num; i < set_num + size; ++i) @@ -335,6 +357,7 @@ namespace spot delete S; } + // A bdd_states_map is a list of formulae (in a BDD form) // associated with a destination set of states. typedef std::map bdd_states_map; @@ -372,13 +395,10 @@ namespace spot hash_map::const_iterator i = state_set_map.find(dst); assert(i != state_set_map.end()); - bdd current_acceptance_conditions = - si->current_acceptance_conditions(); - if (current_acceptance_conditions == bddfalse) - current_acceptance_conditions - = bdd_false_acceptance_condition; - f |= (bdd_ithvar(i->second) & si->current_condition() - & current_acceptance_conditions); + auto curacc = + mark_to_bdd(si->current_acceptance_conditions()); + f |= (bdd_ithvar(i->second) + & si->current_condition() & curacc); trace << "+f: " << bdd_format_accset(ta_->get_dict(), f) << "\n -bdd_ithvar(i->second): " @@ -388,9 +408,8 @@ namespace spot << bdd_format_accset(ta_->get_dict(), si->current_condition()) << "\n -current_acceptance_conditions: " - << bdd_format_accset(ta_->get_dict(), - current_acceptance_conditions) - << std::endl; + << si->current_acceptance_conditions() + << std::endl; } delete si; @@ -480,6 +499,7 @@ namespace spot trace << std::endl; #endif + ta_->get_dict()->unregister_all_my_variables(&m2b); return done; } } @@ -489,7 +509,7 @@ namespace spot { auto tgba = make_tgba_digraph(ta_->get_dict()); - auto res = make_ta_explicit(tgba, ta_->all_acceptance_conditions(), 0); + auto res = make_ta_explicit(tgba, ta_->acc().num_sets(), 0); partition_t partition = build_partition(ta_); @@ -509,7 +529,7 @@ namespace spot { auto tgba = make_tgba_digraph(tgta_->get_dict()); - auto res = make_tgta_explicit(tgba, tgta_->all_acceptance_conditions(), 0); + auto res = make_tgta_explicit(tgba, tgta_->acc().num_sets(), 0); auto ta = tgta_->get_ta(); diff --git a/src/taalgos/tgba2ta.cc b/src/taalgos/tgba2ta.cc index 5d830c4f7..0df289977 100644 --- a/src/taalgos/tgba2ta.cc +++ b/src/taalgos/tgba2ta.cc @@ -148,7 +148,7 @@ namespace spot } static void - compute_livelock_acceptance_states(const ta_explicit_ptr& testing_automata, + compute_livelock_acceptance_states(const ta_explicit_ptr& testing_aut, bool single_pass_emptiness_check, state_ta_explicit* artificial_livelock_acc_state) @@ -158,7 +158,7 @@ namespace spot scc_stack_ta sscc; // * arc, a stack of acceptance conditions between each of these SCC, - std::stack arc; + std::stack arc; // * h: a hash of all visited nodes, with their order, // (it is called "Hash" in Couvreur's paper) @@ -180,7 +180,7 @@ namespace spot // * init: the set of the depth-first search initial states std::stack init_set; - for (state* s: testing_automata->get_initial_states_set()) + for (state* s: testing_aut->get_initial_states_set()) init_set.push(s); while (!init_set.empty()) @@ -199,10 +199,10 @@ namespace spot } sscc.push(++num); - arc.push(bddfalse); + arc.push(0U); sscc.top().is_accepting - = testing_automata->is_accepting_state(init); - tgba_succ_iterator* iter = testing_automata->succ_iter(init); + = testing_aut->is_accepting_state(init); + tgba_succ_iterator* iter = testing_aut->succ_iter(init); iter->first(); todo.emplace(init, iter); } @@ -243,10 +243,9 @@ namespace spot // removing states std::list::iterator i; bool is_livelock_accepting_sscc = (sscc.rem().size() > 1) - && ((sscc.top().is_accepting) - || (sscc.top().condition == - testing_automata->all_acceptance_conditions())); - + && ((sscc.top().is_accepting) || + (testing_aut->acc(). + accepting(sscc.top().condition))); trace << "*** sscc.size() = ***" << sscc.size() << '\n'; for (auto j: sscc.rem()) { @@ -257,7 +256,7 @@ namespace spot // if it is an accepting sscc add the state to // G (=the livelock-accepting states set) trace << "*** sscc.size() > 1: states: ***" - << testing_automata->format_state(j) + << testing_aut->format_state(j) << '\n'; state_ta_explicit* livelock_accepting_state = down_cast(j); @@ -283,7 +282,7 @@ namespace spot } // automata reduction - testing_automata->delete_stuttering_and_hole_successors(curr); + testing_aut->delete_stuttering_and_hole_successors(curr); delete succ; // Do not delete CURR: it is a key in H. @@ -293,7 +292,7 @@ namespace spot // Fetch the values destination state we are interested in... state* dest = succ->current_state(); - bdd acc_cond = succ->current_acceptance_conditions(); + auto acc_cond = succ->current_acceptance_conditions(); // ... and point the iterator to the next successor, for // the next iteration. succ->next(); @@ -301,8 +300,8 @@ namespace spot // Are we going to a new state through a stuttering transition? bool is_stuttering_transition = - testing_automata->get_state_condition(curr) - == testing_automata->get_state_condition(dest); + testing_aut->get_state_condition(curr) + == testing_aut->get_state_condition(dest); auto id = h.find(dest); // Is this a new state? @@ -321,9 +320,9 @@ namespace spot sscc.push(num); arc.push(acc_cond); sscc.top().is_accepting = - testing_automata->is_accepting_state(dest); + testing_aut->is_accepting_state(dest); - tgba_succ_iterator* iter = testing_automata->succ_iter(dest); + tgba_succ_iterator* iter = testing_aut->succ_iter(dest); iter->first(); todo.emplace(dest, iter); continue; @@ -342,9 +341,8 @@ namespace spot down_cast (curr); assert(self_loop_state); - if (testing_automata->is_accepting_state(self_loop_state) - || (acc_cond - == testing_automata->all_acceptance_conditions())) + if (testing_aut->is_accepting_state(self_loop_state) + || (testing_aut->acc().accepting(acc_cond))) { self_loop_state->set_livelock_accepting_state(true); if (single_pass_emptiness_check) @@ -404,7 +402,7 @@ namespace spot if ((artificial_livelock_acc_state != 0) || single_pass_emptiness_check) - transform_to_single_pass_automaton(testing_automata, + transform_to_single_pass_automaton(testing_aut, artificial_livelock_acc_state); } @@ -429,7 +427,7 @@ namespace spot tgba_succ_iterator* it = tgba_->succ_iter(tgba_init_state); it->first(); if (!it->done()) - is_acc = it->current_acceptance_conditions() != bddfalse; + is_acc = it->current_acceptance_conditions() != 0U; delete it; } @@ -462,7 +460,7 @@ namespace spot { const state* tgba_state = tgba_succ_it->current_state(); bdd tgba_condition = tgba_succ_it->current_condition(); - bdd tgba_acceptance_conditions = + acc_cond::mark_t tgba_acceptance_conditions = tgba_succ_it->current_acceptance_conditions(); bdd satone_tgba_condition; while ((satone_tgba_condition = @@ -481,7 +479,7 @@ namespace spot tgba_succ_iterator* it = tgba_->succ_iter(tgba_state); it->first(); if (!it->done()) - is_acc = it->current_acceptance_conditions() != bddfalse; + is_acc = it->current_acceptance_conditions() != 0U; delete it; } @@ -554,12 +552,12 @@ namespace spot state_ta_explicit* artificial_init_state = new state_ta_explicit(tgba_init_state->clone(), bddfalse, true); - ta = make_ta_explicit(tgba_, tgba_->all_acceptance_conditions(), + ta = make_ta_explicit(tgba_, tgba_->acc().num_sets(), artificial_init_state); } else { - ta = make_ta_explicit(tgba_, tgba_->all_acceptance_conditions()); + ta = make_ta_explicit(tgba_, tgba_->acc().num_sets()); } tgba_init_state->destroy(); @@ -586,10 +584,7 @@ namespace spot for (it_trans = trans->begin(); it_trans != trans->end(); ++it_trans) - { - (*it_trans)->acceptance_conditions - = ta->all_acceptance_conditions(); - } + (*it_trans)->acceptance_conditions = ta->acc().all_sets(); state->set_accepting_state(false); } @@ -606,7 +601,7 @@ namespace spot bddfalse, true); tgba_init_state->destroy(); - auto tgta = make_tgta_explicit(tgba_, tgba_->all_acceptance_conditions(), + auto tgta = make_tgta_explicit(tgba_, tgba_->acc().num_sets(), artificial_init_state); // build a Generalized TA automaton involving a single_pass_emptiness_check @@ -644,13 +639,13 @@ namespace spot if (trans_empty || state->is_accepting_state()) { ta->create_transition(state, bdd_stutering_transition, - ta->all_acceptance_conditions(), state); + ta->acc().all_sets(), state); } } if (state->compare(ta->get_artificial_initial_state())) ta->create_transition(state, bdd_stutering_transition, - bddfalse, state); + 0U, state); state->set_livelock_accepting_state(false); state->set_accepting_state(false); diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index e405ef867..a71091724 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -26,6 +26,7 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS) tgbadir = $(pkgincludedir)/tgba tgba_HEADERS = \ + acc.hh \ bdddict.hh \ bddprint.hh \ formula2bdd.hh \ @@ -33,11 +34,9 @@ tgba_HEADERS = \ taatgba.hh \ tgba.hh \ tgbagraph.hh \ - tgbakvcomplement.hh \ tgbamask.hh \ tgbaproxy.hh \ tgbaproduct.hh \ - tgbasgba.hh \ tgbasafracomplement.hh noinst_LTLIBRARIES = libtgba.la @@ -48,9 +47,7 @@ libtgba_la_SOURCES = \ taatgba.cc \ tgba.cc \ tgbagraph.cc \ - tgbakvcomplement.cc \ tgbaproduct.cc \ tgbamask.cc \ tgbaproxy.cc \ - tgbasafracomplement.cc \ - tgbasgba.cc + tgbasafracomplement.cc diff --git a/src/tgba/acc.hh b/src/tgba/acc.hh new file mode 100644 index 000000000..a1a923f53 --- /dev/null +++ b/src/tgba/acc.hh @@ -0,0 +1,433 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2014 Laboratoire de Recherche et Développement de +// l'Epita. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + +#ifndef SPOT_TGBA_ACC_HH +# define SPOT_TGBA_ACC_HH + +# include +# include +# include +# include "bdddict.hh" +# include "ltlenv/defaultenv.hh" + +namespace spot +{ + class acc_cond + { + public: + struct mark_t + { + typedef unsigned value_t; + value_t id; + + mark_t() = default; + + mark_t(value_t id) + : id(id) + { + } + + bool operator==(unsigned o) const + { + assert(o == 0U); + return id == o; + } + + bool operator!=(unsigned o) const + { + assert(o == 0U); + return id != o; + } + + bool operator==(mark_t o) const + { + return id == o.id; + } + + bool operator!=(mark_t o) const + { + return id != o.id; + } + + bool operator<(mark_t o) const + { + return id < o.id; + } + + bool operator<=(mark_t o) const + { + return id <= o.id; + } + + bool operator>(mark_t o) const + { + return id > o.id; + } + + bool operator>=(mark_t o) const + { + return id >= o.id; + } + + operator bool() const + { + return id != 0; + } + + + bool has(unsigned u) const + { + return id & (1U << u); + } + + mark_t& operator&=(mark_t r) + { + id &= r.id; + return *this; + } + + mark_t& operator|=(mark_t r) + { + id |= r.id; + return *this; + } + + mark_t& operator-=(mark_t r) + { + id &= ~r.id; + return *this; + } + + mark_t operator&(mark_t r) const + { + return id & r.id; + } + + mark_t operator|(mark_t r) const + { + return id | r.id; + } + + mark_t operator-(mark_t r) const + { + return id & ~r.id; + } + + // Number of bits sets. + unsigned count() const + { +#ifdef __GNUC__ + return __builtin_popcount(id); +#else + unsigned c = 0U; + auto v = id; + while (v) + { + ++c; + v &= v - 1; + } + return c; +#endif + } + + // Remove n bits that where set + mark_t& remove_some(unsigned n) + { + while (n--) + id &= id - 1; + return *this; + } + + friend std::ostream& operator<<(std::ostream& os, mark_t m) + { + auto a = m.id; + os << '{'; + unsigned level = 0; + const char* comma = ""; + while (a) + { + if (a & 1) + { + os << comma << level; + comma = ","; + } + a >>= 1; + ++level; + } + os << '}'; + return os; + } + }; + + acc_cond(const bdd_dict_ptr& dict, unsigned n_sets = 0) + : d_(dict), num_(0U), all_(0U) + { + add_sets(n_sets); + } + + acc_cond(const acc_cond& o) + : num_(o.num_), all_(o.all_) + { + } + + ~acc_cond() + { + } + + const bdd_dict_ptr& get_dict() const + { + return d_; + } + + unsigned add_sets(unsigned num) + { + if (num == 0) + return -1U; + unsigned j = num_; + num_ += num; + if (num_ > 8 * sizeof(mark_t::id)) + throw std::runtime_error("Too many acceptance sets used."); + all_ = all_sets_(); + return j; + } + + unsigned add_set() + { + return add_sets(1); + } + + mark_t mark(unsigned u) const + { + return out(mark_(u)); + } + + template + mark_t marks(const iterator& begin, const iterator& end) const + { + mark_t::value_t res = 0U; + for (iterator i = begin; i != end; ++i) + res |= mark_(*i); + return out(res); + } + + mark_t marks(std::initializer_list vals) const + { + return marks(vals.begin(), vals.end()); + } + + template + void fill_from(mark_t m, iterator here) const + { + auto a = in(m); + unsigned level = 0; + while (a) + { + if (a & 1) + *here++ = level; + ++level; + a >>= 1; + } + assert(level <= num_sets()); + } + + // FIXME: Return some iterable object without building a vector. + std::vector sets(mark_t m) const + { + std::vector res; + fill_from(m, std::back_inserter(res)); + return res; + } + + // whether m contains u + bool has(mark_t m, unsigned u) const + { + return m.has(u); + } + + mark_t cup(mark_t l, mark_t r) const + { + return l | r; + } + + mark_t cap(mark_t l, mark_t r) const + { + return l & r; + } + + mark_t set_minus(mark_t l, mark_t r) const + { + return l - r; + } + + mark_t join(const acc_cond& la, mark_t lm, + const acc_cond& ra, mark_t rm) const + { + assert(la.num_sets() + ra.num_sets() == num_sets()); + return la.in(lm) | (ra.in(rm) << la.num_sets()); + } + + mark_t comp(mark_t l) const + { + return out(all_ ^ in(l)); + } + + mark_t all_sets() const + { + return out(all_); + } + + bool accepting(mark_t inf) const + { + return in(inf) == all_; + } + + std::ostream& format_quoted(std::ostream& os, mark_t m) const + { + auto a = in(m); + if (a == 0U) + return os; + unsigned level = 0; + const char* space = ""; + while (a) + { + if (a & 1) + { + os << space << '"' << level << '"'; + space = " "; + } + a >>= 1; + ++level; + } + return os; + } + + std::ostream& format(std::ostream& os, mark_t m) const + { + auto a = in(m); + if (a == 0U) + return os; + return os << m; + } + + std::string format(mark_t m) const + { + std::ostringstream os; + format(os, m); + return os.str(); + } + + unsigned num_sets() const + { + return num_; + } + + template + mark_t useless(iterator begin, iterator end) const + { + mark_t::value_t u = 0U; // The set of useless marks. + for (unsigned x = 0; x < num_; ++x) + { + // Skip marks that are already known to be useless. + if (u & (1 << x)) + continue; + unsigned all = all_ ^ (u | (1 << x)); + for (iterator y = begin; y != end; ++y) + { + auto v = in(*y); + if (v & (1 << x)) + { + all &= v; + if (!all) + break; + } + } + u |= all; + } + return out(u); + } + + mark_t strip(mark_t x, mark_t y) const + { + // strip every bit of x that is marked in y + // strip(100101110100, + // 001011001000) + // == 10 1 11 100 + // == 10111100 + + auto xv = in(x); // 100101110100 + auto yv = in(y); // 001011001000 + + while (yv && xv) + { + // Mask for everything after the last 1 in y + auto rm = (~yv) & (yv - 1); // 000000000111 + // Mask for everything before the last 1 in y + auto lm = ~(yv ^ (yv - 1)); // 111111110000 + xv = ((xv & lm) >> 1) | (xv & rm); + yv = (yv & lm) >> 1; + } + + return out(xv); + } + + protected: + mark_t::value_t mark_(unsigned u) const + { + assert(u < num_sets()); + return 1U << u; + } + + mark_t::value_t all_sets_() const + { + if (num_ == 0) + return 0; + return -1U >> (8 * sizeof(mark_t::value_t) - num_); + } + + mark_t::value_t in(mark_t m) const + { + return m.id; + } + + mark_t out(mark_t::value_t r) const + { + return r; + } + + bdd_dict_ptr d_; + unsigned num_; + mark_t::value_t all_; + }; + +} + +namespace std +{ + template<> + struct hash + { + size_t operator()(spot::acc_cond::mark_t m) const + { + std::hash h; + return h(m.id); + } + }; +} + +#endif // SPOT_TGBA_ACC_HH diff --git a/src/tgba/fwd.hh b/src/tgba/fwd.hh index 24e089ae5..72bcbaac4 100644 --- a/src/tgba/fwd.hh +++ b/src/tgba/fwd.hh @@ -35,10 +35,6 @@ namespace spot class tgba_product; typedef std::shared_ptr const_tgba_product_ptr; typedef std::shared_ptr tgba_product_ptr; - - class tgba_sgba_proxy; - typedef std::shared_ptr const_tgba_sgba_proxy_ptr; - typedef std::shared_ptr tgba_sgba_proxy_ptr; } #endif // SPOT_TGBA_FWD_HH diff --git a/src/tgba/taatgba.cc b/src/tgba/taatgba.cc index 97bf72b5c..f0bbf0419 100644 --- a/src/tgba/taatgba.cc +++ b/src/tgba/taatgba.cc @@ -34,10 +34,7 @@ namespace spot `--------*/ taa_tgba::taa_tgba(const bdd_dict_ptr& dict) - : dict_(dict), - all_acceptance_conditions_(bddfalse), - all_acceptance_conditions_computed_(false), - neg_acceptance_conditions_(bddtrue), + : tgba(dict), init_(0), state_set_vec_() { } @@ -47,13 +44,13 @@ namespace spot ss_vec::iterator j; for (j = state_set_vec_.begin(); j != state_set_vec_.end(); ++j) delete *j; - dict_->unregister_all_my_variables(this); + get_dict()->unregister_all_my_variables(this); } void taa_tgba::add_condition(transition* t, const ltl::formula* f) { - t->condition &= formula_to_bdd(f, dict_, this); + t->condition &= formula_to_bdd(f, get_dict(), this); f->destroy(); } @@ -69,31 +66,7 @@ namespace spot { const spot::set_state* s = down_cast(state); assert(s); - return new taa_succ_iterator(s->get_state(), all_acceptance_conditions()); - } - - bdd_dict_ptr - taa_tgba::get_dict() const - { - return dict_; - } - - bdd - taa_tgba::all_acceptance_conditions() const - { - if (!all_acceptance_conditions_computed_) - { - all_acceptance_conditions_ = - compute_all_acceptance_conditions(neg_acceptance_conditions_); - all_acceptance_conditions_computed_ = true; - } - return all_acceptance_conditions_; - } - - bdd - taa_tgba::neg_acceptance_conditions() const - { - return neg_acceptance_conditions_; + return new taa_succ_iterator(s->get_state(), acc_); } bdd @@ -172,14 +145,14 @@ namespace spot `--------------*/ taa_succ_iterator::taa_succ_iterator(const taa_tgba::state_set* s, - bdd all_acc) - : all_acceptance_conditions_(all_acc), seen_() + const acc_cond& acc) + : seen_(), acc_(acc) { if (s->empty()) { taa_tgba::transition* t = new taa_tgba::transition; t->condition = bddtrue; - t->acceptance_conditions = bddfalse; + t->acceptance_conditions = 0U; t->dst = new taa_tgba::state_set; succ_.push_back(t); return; @@ -202,7 +175,7 @@ namespace spot { taa_tgba::transition* t = new taa_tgba::transition; t->condition = bddtrue; - t->acceptance_conditions = bddfalse; + t->acceptance_conditions = 0U; taa_tgba::state_set* ss = new taa_tgba::state_set; unsigned p; @@ -330,12 +303,11 @@ namespace spot return (*i_)->condition; } - bdd + acc_cond::mark_t taa_succ_iterator::current_acceptance_conditions() const { assert(!done()); - return all_acceptance_conditions_ - - ((*i_)->acceptance_conditions & all_acceptance_conditions_); + return acc_.comp((*i_)->acceptance_conditions); } /*----------------. diff --git a/src/tgba/taatgba.hh b/src/tgba/taatgba.hh index 3e06eacc8..e9b376ebb 100644 --- a/src/tgba/taatgba.hh +++ b/src/tgba/taatgba.hh @@ -27,6 +27,7 @@ #include "ltlast/formula.hh" #include "bdddict.hh" #include "tgba.hh" +#include "ltlvisit/tostring.hh" namespace spot { @@ -45,7 +46,7 @@ namespace spot struct transition { bdd condition; - bdd acceptance_conditions; + acc_cond::mark_t acceptance_conditions; const state_set* dst; }; @@ -55,23 +56,19 @@ namespace spot virtual ~taa_tgba(); virtual spot::state* get_init_state() const; virtual tgba_succ_iterator* succ_iter(const spot::state* state) const; - virtual bdd_dict_ptr get_dict() const; virtual std::string format_state(const spot::state* state) const = 0; - virtual bdd all_acceptance_conditions() const; - virtual bdd neg_acceptance_conditions() const; protected: virtual bdd compute_support_conditions(const spot::state* state) const; typedef std::vector ss_vec; - bdd_dict_ptr dict_; - mutable bdd all_acceptance_conditions_; - mutable bool all_acceptance_conditions_computed_; - bdd neg_acceptance_conditions_; taa_tgba::state_set* init_; ss_vec state_set_vec_; + std::map acc_map_; + private: // Disallow copy. taa_tgba(const taa_tgba& other) SPOT_DELETED; @@ -106,7 +103,7 @@ namespace spot class SPOT_API taa_succ_iterator : public tgba_succ_iterator { public: - taa_succ_iterator(const taa_tgba::state_set* s, bdd all_acc); + taa_succ_iterator(const taa_tgba::state_set* s, const acc_cond& acc); virtual ~taa_succ_iterator(); virtual bool first(); @@ -115,7 +112,7 @@ namespace spot virtual set_state* current_state() const; virtual bdd current_condition() const; - virtual bdd current_acceptance_conditions() const; + virtual acc_cond::mark_t current_acceptance_conditions() const; private: /// Those typedefs are used to generate all possible successors in @@ -141,8 +138,8 @@ namespace spot std::vector::const_iterator i_; std::vector succ_; - bdd all_acceptance_conditions_; seen_map seen_; + const acc_cond& acc_; }; /// A taa_tgba instance with states labeled by a given type. @@ -153,6 +150,13 @@ namespace spot public: taa_tgba_labelled(const bdd_dict_ptr& dict) : taa_tgba(dict) {}; + ~taa_tgba_labelled() + { + auto i = acc_map_.begin(); + while (i != acc_map_.end()) + (i++)->first->destroy(); + } + void set_init_state(const label& s) { std::vector