diff --git a/ChangeLog b/ChangeLog index b6b0a9510..029220d0f 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,12 @@ 2003-07-08 Alexandre Duret-Lutz + * src/tgbatest/ltl2tgba.cc: Add option -t to output the LBTT automata. + * src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh: New files. + * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS): Add lbtt.hh. + (libtgbaalgos_la_SOURCES): Add lbtt.cc. + * src/tgba/bddprint.cc (print_sat_handler): Put a space after "!". + * src/tgbatest/readsave.test: Adjust spaces after "!". + * src/ltlvisit/dump.cc: Strip useless spot::ltl:: prefixes. 2003-07-07 Alexandre Duret-Lutz diff --git a/src/tgba/bddprint.cc b/src/tgba/bddprint.cc index 89d039836..e8fe12288 100644 --- a/src/tgba/bddprint.cc +++ b/src/tgba/bddprint.cc @@ -73,7 +73,8 @@ namespace spot else not_first = true; if (varset[v] == 0) - *where << "!"; + // The space is important for LBTT. + *where << "! "; print_handler(*where, v); } } diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 1fc7ff6e5..ec9563bf6 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -5,11 +5,13 @@ tgbaalgosdir = $(pkgincludedir)/tgbaalgos tgbaalgos_HEADERS = \ dotty.hh \ + lbtt.hh \ ltl2tgba.hh \ save.hh noinst_LTLIBRARIES = libtgbaalgos.la libtgbaalgos_la_SOURCES = \ dotty.cc \ + lbtt.cc \ ltl2tgba.cc \ save.cc diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc new file mode 100644 index 000000000..5ff4b9024 --- /dev/null +++ b/src/tgbaalgos/lbtt.cc @@ -0,0 +1,220 @@ +#include +#include +#include +#include +#include "tgba/tgba.hh" +#include "save.hh" +#include "tgba/bddprint.hh" +#include "ltlvisit/tostring.hh" +#include "tgba/bddprint.hh" + +namespace spot +{ + struct bdd_less_than + { + bool + operator()(const bdd& left, const bdd& right) const + { + return left.id() < right.id(); + } + }; + + // At some point we'll need to print an accepting set into LBTT's + // forma. LBTT expect numbered accepting sets, so first we'll + // number each accepting condition, and latter when we have to print + // them we'll just have to look up each of them. + class accepting_cond_splitter + { + public: + accepting_cond_splitter(bdd all_acc) + { + unsigned count = 0; + while (all_acc != bddfalse) + { + bdd acc = bdd_satone(all_acc); + all_acc &= !acc; + sm[acc] = count++; + } + } + + std::ostream& + split(std::ostream& os, bdd b) + { + while (b != bddfalse) + { + bdd acc = bdd_satone(b); + b &= !acc; + os << sm[acc] << " "; + } + return os; + } + + unsigned + count() const + { + return sm.size(); + } + + private: + typedef std::map split_map; + split_map sm; + }; + + // Convert a BDD formula to the syntax used by LBTT's transition guards. + // Conjunctions are printed by bdd_format_sat, so we just have + // to handle the other cases. + static std::string + bdd_to_lbtt(bdd b, const tgba_bdd_dict& d) + { + if (b == bddfalse) + return "f"; + else if (b == bddtrue) + return "t"; + else + { + bdd cube = bdd_satone(b); + b &= !cube; + if (b != bddfalse) + { + return "| " + bdd_to_lbtt(b, d) + " " + bdd_to_lbtt(cube, d); + } + else + { + std::string res = ""; + for (int count = bdd_nodecount(cube); count > 1; --count) + res += "& "; + return res + bdd_format_sat(d, cube); + } + } + + } + + // Each state in the produced automata corresponds to + // a (state, accepting set) pair for the source automata. + + typedef std::pair state_acc_pair; + + struct state_acc_pair_less_than + { + bool + operator()(const state_acc_pair& left, const state_acc_pair& right) const + { + int cmp = left.first->compare(right.first); + if (cmp < 0) + return true; + if (cmp > 0) + return false; + return left.second.id() < right.second.id(); + } + }; + + // Each state of the produced automata is numbered. Map of state seen. + typedef std::map acp_seen_map; + + // Set of states yet to produce. + typedef std::set todo_set; + + // Each *source* car correspond to several state in the produced + // automate. A minmax_pair specify the range of such associated states. + typedef std::pair minmax_pair; + typedef std::map seen_map; + + // Take a STATE from the source automata, and fill TODO with + // the list of associated states to output. Return the correponding + // range in MMP. Update SEEN, ACP_SEEN, and STATE_NUMBER. + void + fill_todo(todo_set& todo, seen_map& seen, acp_seen_map& acp_seen, + state* state, const tgba& g, + minmax_pair& mmp, unsigned& state_number) + { + typedef std::set bdd_set; + + seen_map::iterator i = seen.find(state); + if (i != seen.end()) + { + mmp = i->second; + delete state; + return; + } + + // Browse the successors of STATE to gather accepting + // conditions of outgoing transitions. + bdd_set acc_seen; + tgba_succ_iterator* si = g.succ_iter(state); + for (si->first(); !si->done(); si->next()) + { + acc_seen.insert(si->current_accepting_conditions()); + } + mmp.first = state_number; + for (bdd_set::iterator i = acc_seen.begin(); i != acc_seen.end(); ++i) + { + state_acc_pair p(state, *i); + todo.insert(p); + acp_seen[p] = state_number++; + } + mmp.second = state_number; + seen[state] = mmp; + } + + std::ostream& + lbtt_reachable(std::ostream& os, const tgba& g) + { + const tgba_bdd_dict& d = g.get_dict(); + std::ostringstream body; + + seen_map seen; + acp_seen_map acp_seen; + todo_set todo; + unsigned state_number = 0; + + minmax_pair mmp; + + fill_todo(todo, seen, acp_seen, + g.get_init_state(), g, mmp, state_number); + accepting_cond_splitter acs(g.all_accepting_conditions()); + + while(! todo.empty()) + { + state_acc_pair sap = *todo.begin(); + todo.erase(todo.begin()); + unsigned number = acp_seen[sap]; + + body << number << " " + // Mark the initial state. + << ((number >= mmp.first && number < mmp.second) ? 1 : 0) << " "; + + acs.split(body, sap.second); + body << "-1" << std::endl; + + tgba_succ_iterator* si = g.succ_iter(sap.first); + for (si->first(); !si->done(); si->next()) + { + // We have put the accepting conditions on the state, + // so draw only outgoing transition with these accepting + // conditions. + if (si->current_accepting_conditions() != sap.second) + continue; + + minmax_pair destrange; + fill_todo(todo, seen, acp_seen, + si->current_state(), g, destrange, state_number); + + // Link to all instances of the successor. + std::string s = bdd_to_lbtt(si->current_condition(), d); + for (unsigned i = destrange.first; i < destrange.second; ++i) + { + body << i << " " << s << " " << "-1" << std::endl; + } + } + body << "-1" << std::endl; + delete si; + } + + os << state_number << " " << acs.count() << std::endl; + os << body.str(); + // Finally delete all states used as keys in m: + for (seen_map::iterator i = seen.begin(); i != seen.end(); ++i) + delete i->first; + return os; + } +} diff --git a/src/tgbaalgos/lbtt.hh b/src/tgbaalgos/lbtt.hh new file mode 100644 index 000000000..4c5e5ef9f --- /dev/null +++ b/src/tgbaalgos/lbtt.hh @@ -0,0 +1,31 @@ +#ifndef SPOT_TGBAALGOS_LBTT_HH +# define SPOT_TGBAALGOS_LBTT_HH + +#include "tgba/tgba.hh" +#include + +namespace spot +{ + /// \brief Print reachable states in LBTT format. + /// + /// Note that LBTT expects an automaton with transition + /// labeled by propositional formulae, and generalized + /// Büchi accepting conditions on \emph states. This + /// is unlike our spot::tgba automata which put + /// botg generalized accepting conditions and propositional + /// formulae) on \emph transitions. + /// + /// This algorithm will therefore produce an automata + /// where accepting conditions have been moved from + /// each transition to previous state. In the worst + /// case, doing so will multiply the number of states + /// and transitions of the automata by 2^|Acc|. + /// where |Acc| is the number of accepting + /// conditions used by the automata. You have been warned. + /// + /// \param g The automata to print. + /// \param os Where to print. + std::ostream& lbtt_reachable(std::ostream& os, const tgba& g); +} + +#endif // SPOT_TGBAALGOS_LBTT_HH diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 1489581db..c28cb90f6 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -7,6 +7,7 @@ #include "tgba/bddprint.hh" #include "tgba/tgbabddtranslatefactory.hh" #include "tgbaalgos/dotty.hh" +#include "tgbaalgos/lbtt.hh" void syntax(char* prog) @@ -19,10 +20,10 @@ syntax(char* prog) << " -A same as -a, but as a set" << std::endl << " -d turn on traces during parsing" << std::endl << " -o re-order BDD variables in the automata" << std::endl - << std::endl << " -r display the relation BDD, not the reachability graph" << std::endl << " -R same as -r, but as a set" << std::endl + << " -t display reachable states in LBTT's format" << std::endl << " -v display the BDD variables used by the automaton" << std::endl; exit(2); @@ -69,6 +70,10 @@ main(int argc, char** argv) { output = 3; } + else if (!strcmp(argv[formula_index], "-t")) + { + output = 6; + } else if (!strcmp(argv[formula_index], "-v")) { output = 5; @@ -118,6 +123,9 @@ main(int argc, char** argv) case 5: a.get_dict().dump(std::cout); break; + case 6: + spot::lbtt_reachable(std::cout, a); + break; default: assert(!"unknown output option"); } diff --git a/src/tgbatest/readsave.test b/src/tgbatest/readsave.test index 5e7b9412e..f5a6f4193 100755 --- a/src/tgbatest/readsave.test +++ b/src/tgbatest/readsave.test @@ -15,7 +15,7 @@ EOF cat >expected <