diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc index 29b024f4f..be4c9831e 100644 --- a/src/tgbaalgos/simulation.cc +++ b/src/tgbaalgos/simulation.cc @@ -78,6 +78,13 @@ // bdd_support(sig(X)) - allacc - allclassvar +// We have had the Cosimulation by changing the acc_compl_automaton by +// adding a template parameter. If this parameter is set to true, we +// record the transition in the opposite direction (we just swap +// sources and destination). In the build result we are making the +// same thing to rebuild the automaton. +// In the signature, + namespace spot { namespace @@ -93,7 +100,6 @@ namespace spot state_ptr_hash, state_ptr_equal> map_state_unsigned; - // Get the list of state for each class. typedef std::map, bdd_less_than> map_bdd_lstate; @@ -101,6 +107,7 @@ namespace spot // This class takes an automaton and creates a copy with all // acceptance conditions complemented. + template class acc_compl_automaton: public tgba_reachable_iterator_depth_first { @@ -139,6 +146,15 @@ namespace spot int src = get_state(in_s); int dst = get_state(out_s); + + // In the case of the cosimulation, we want to have all the + // ingoing transition, and to keep the rest of the code + // similar, we just create equivalent transition in the other + // direction. Since we do not have to run through the + // automaton to get the signature, this is correct. + if (Cosimulation) + std::swap(src, dst); + bdd acc = ac_.complement(si->current_acceptance_conditions()); tgba_explicit_number::transition* t @@ -170,7 +186,7 @@ namespace spot state* init_; }; - + template class direct_simulation { // Shortcut used in update_po and go_to_next_it. @@ -181,7 +197,7 @@ namespace spot po_size_(0), all_class_var_(bddtrue) { - acc_compl_automaton + acc_compl_automaton acc_compl(t); // We'll start our work by replacing all the acceptance @@ -190,6 +206,8 @@ namespace spot a_ = acc_compl.out_; + initial_state = a_->get_init_state(); + // We use the previous run to know the size of the // automaton, and to class all the reachable states in the // map previous_class_. @@ -199,11 +217,10 @@ namespace spot // class. We register one bdd by state, because in the worst // case, |Class| == |State|. unsigned set_num = a_->get_dict() - ->register_anonymous_variables(size_a_, a_); - bdd init = bdd_ithvar(set_num); + ->register_anonymous_variables(size_a_ + 1, a_); - // Because we have already take the first element which is init. - ++set_num; + bdd_initial = bdd_ithvar(set_num++); + bdd init = bdd_ithvar(set_num++); used_var_.push_back(init); all_class_var_ = init; @@ -258,12 +275,12 @@ namespace spot it_s != it->second.end(); ++it_s) { - // If the signature of a state is bddfalse (which is - // roughly equivalent to no transition) the class of - // this state is bddfalse instead of an anonymous - // variable. It allows simplifications in the signature - // by removing a transition which has as a destination a - // state with no outgoing transition. + // If the signature of a state is bddfalse (no + // transitions) the class of this state is bddfalse + // instead of an anonymous variable. It allows + // simplifications in the signature by removing a + // transition which has as a destination a state with + // no outgoing transition. if (it->first == bddfalse) previous_class_[*it_s] = bddfalse; else @@ -297,10 +314,10 @@ namespace spot // Take a state and compute its signature. bdd compute_sig(const state* src) { - tgba_succ_iterator* sit = a_->succ_iter(src); - bdd res = bddfalse; + tgba_succ_iterator* sit = a_->succ_iter(src); + bdd res = bddfalse; - for (sit->first(); !sit->done(); sit->next()) + for (sit->first(); !sit->done(); sit->next()) { const state* dst = sit->current_state(); bdd acc = sit->current_acceptance_conditions(); @@ -315,10 +332,16 @@ namespace spot dst->destroy(); } - delete sit; - return res; + // When we Cosimulate, we add a special flag to differentiate + // initial state. + if (Cosimulation && initial_state == src) + res |= bdd_initial; + + delete sit; + return res; } + void update_sig() { // At this time, current_class_ must be empty. It implies @@ -402,21 +425,20 @@ namespace spot ++it1) { bdd accu = it1->second; - for (map_bdd_bdd::const_iterator it2 = now_to_next.begin(); it2 != now_to_next.end(); ++it2) - { - // Skip the case managed by the initialization of accu. - if (it1 == it2) - continue; + { + // Skip the case managed by the initialization of accu. + if (it1 == it2) + continue; - if (bdd_implies(it1->first, it2->first)) - { - accu &= it2->second; - ++po_size_; - } - } + if (bdd_implies(it1->first, it2->first)) + { + accu &= it2->second; + ++po_size_; + } + } relation_[it1->second] = accu; } } @@ -476,6 +498,9 @@ namespace spot // Get the signature. bdd sig = compute_sig(*(it->second.begin())); + if (Cosimulation) + sig = bdd_compose(sig, bddfalse, bdd_var(bdd_initial)); + // Get all the variable in the signature. bdd sup_sig = bdd_support(sig); @@ -495,7 +520,6 @@ namespace spot bddtrue); all_atomic_prop -= one; - // For each possible valuation, iterator over all possible // destination classes. We use minato_isop here, because // if the same valuation of atomic properties can go @@ -533,6 +557,9 @@ namespace spot int src = bdd2state[previous_class_[*it->second.begin()]]; int dst = bdd2state[dest]; + if (Cosimulation) + std::swap(src, dst); + // src or dst == 0 means "dest" or "prev..." isn't // in the map. so it is a bug. assert(src != 0); @@ -550,7 +577,9 @@ namespace spot res->set_init_state(bdd2state[previous_class_ [a_->get_init_state()]]); + res->merge_transitions(); + return res; } @@ -629,13 +658,29 @@ namespace spot // All the class variable: bdd all_class_var_; + + // The flag to say if the outgoing state is initial or not + bdd bdd_initial; + + // Initial state of the automaton we are working on + state* initial_state; + }; + } // End namespace anonymous. tgba* simulation(const tgba* t) { - direct_simulation simul(t); + direct_simulation simul(t); + + return simul.run(); + } + + tgba* + cosimulation(const tgba* t) + { + direct_simulation simul(t); return simul.run(); } diff --git a/src/tgbaalgos/simulation.hh b/src/tgbaalgos/simulation.hh index 6373039b6..b6e6b21d1 100644 --- a/src/tgbaalgos/simulation.hh +++ b/src/tgbaalgos/simulation.hh @@ -30,12 +30,11 @@ namespace spot /// \addtogroup tgba_reduction /// @{ - /// \brief Attempt to reduce the automaton by direct simulation - /// - /// When the language recognized by one state is included in the - /// language recognized by an another one, the first one is merged - /// with the second. The algorithm is based on the following - /// paper, but generalized to handle TGBA directly. + /// \brief Attempt to reduce the automaton by direct simulation When + /// the suffixes (letter and acceptance conditions) seen by one + /// state is included in the suffixes seen by another one, the first + /// one is merged with the second. The algorithm is based on the + /// following paper, but generalized to handle TGBA directly. /// /// \verbatim /// @InProceedings{ etessami.00.concur, @@ -58,6 +57,34 @@ namespace spot /// one tgba* simulation(const tgba* automaton); + + /// \brief Attempt to reduce the automaton by direct cosimulation. + /// When the prefixes (letter and acceptance conditions) seen by one + /// state is included in the prefixes seen by another one, the first + /// one is merged with the second. The algorithm is based on the + /// following paper, but generalized to handle TGBA directly. + /// \verbatim + /// @InProceedings{Somenzi:2000:EBA:647769.734097, + /// author = {Somenzi, Fabio and Bloem, Roderick}, + /// title = {Efficient {B\"u}chi Automata from LTL Formulae}, + /// booktitle = {Proceedings of the 12th International + /// Conference on Computer Aided Verification}, + /// series = {CAV '00}, + /// year = {2000}, + /// isbn = {3-540-67770-4}, + /// pages = {248--263}, + /// numpages = {16}, + /// url = {http://dl.acm.org/citation.cfm?id=647769.734097}, + /// acmid = {734097}, + /// publisher = {Springer-Verlag}, + /// address = {London, UK, UK}, + /// } + /// \endverbatim + /// \param automaton the automaton to simulate. + /// \return a new automaton which is at worst a copy of the received + /// one + tgba* cosimulation(const tgba* automaton); + /// @} } // End namespace spot. diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index e752a2c7b..c06fac474 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -204,6 +204,8 @@ syntax(char* prog) << std::endl << " -RDS minimize the automaton with direct simulation" << std::endl + << " -RRS minimize the automaton with reverse simulation" + << std::endl << " -Rm attempt to WDBA-minimize the automata" << std::endl << std::endl @@ -352,13 +354,14 @@ main(int argc, char** argv) bool use_timer = false; bool assume_sba = false; bool reduction_dir_sim = false; + bool reduction_rev_sim = false; spot::tgba* temp_dir_sim = 0; bool ta_opt = false; bool tgta_opt = false; bool opt_with_artificial_initial_state = true; bool opt_single_pass_emptiness_check = false; bool opt_with_artificial_livelock = false; - + spot::tgba* temp_rev_sim = 0; for (;;) { @@ -631,6 +634,10 @@ main(int argc, char** argv) // equal to -RDS. reduction_dir_sim = true; } + else if (!strcmp(argv[formula_index], "-RRS")) + { + reduction_rev_sim = true; + } else if (!strcmp(argv[formula_index], "-R3")) { scc_filter = true; @@ -1031,11 +1038,21 @@ main(int argc, char** argv) a = minimized; // When the minimization succeed, simulation is useless. reduction_dir_sim = false; + reduction_rev_sim = false; assume_sba = true; } } + if (reduction_rev_sim) + { + tm.start("Reduction w/ reverse simulation"); + temp_rev_sim = spot::cosimulation(a); + a = temp_rev_sim; + tm.stop("Reduction w/ reverse simulation"); + assume_sba = false; + } + if (reduction_dir_sim) { tm.start("Reduction w/ direct simulation"); @@ -1505,6 +1522,7 @@ main(int argc, char** argv) delete to_free; delete echeck_inst; delete temp_dir_sim; + delete temp_rev_sim; } else { diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test index a5816e14a..241f7b178 100755 --- a/src/tgbatest/spotlbtt.test +++ b/src/tgbatest/spotlbtt.test @@ -199,6 +199,15 @@ Algorithm Enabled = yes } +Algorithm +{ + Name = "Spot (Couvreur -- FM), cosimulated" + Path = "${LBTT_TRANSLATE}" + Parameters = "--spot '../ltl2tgba -F -f -t -RRS -r4 -R3'" + Enabled = yes +} + + Algorithm { Name = "Spot (Couvreur -- LaCim), simulated"