diff --git a/ChangeLog b/ChangeLog index f6e594a15..873364840 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,25 @@ 2003-11-14 Alexandre Duret-Lutz + * src/ltltest/Makefile.am (AM_CXXFLAGS): New variable. + * tgba/bdddict.hh (bdd_dict::register_propositions, + bdd_dict::register_accepting_variables): New methods. + * src/bdddict.cc: Likewise. + * tgba/tgbaexplicit.cc (tgba_explicit::add_conditions, + tgba_explicit::add_accepting_conditions): New methods. + (tgba_explicit::get_init_state): Add an "empty" initial + state to empty automata. + * tgba/tgbaexplicit.hh: (tgba_explicit::add_conditions, + tgba_explicit::add_accepting_conditions): New methods. + * tgbaalgos/Makefiles.am (tgbaalgos_HEADERS, libtgbaalgos_la_SOURCES): + Add dupexp.hh and dupexp.cc. + * tgbaalgos/dupexp.hh, tgbaalgos/dupexp.cc: New files. + * tgbatest/Makefile.am (AM_CXXFLAGS): New variable. + (check_SCRIPTS): Add dupexp.test. + (CLEANFILES): Add output1 and output2. + * tgbatest/dupexp.test: New file. + * tgbatest/ltl2tgba.cc: Handle -s and -S. + * tgbatest/tgbaread.cc: Remove unused variable exit_code. + * src/ltlparse/ltlscan.ll: Include ltlparse/parsedecl.hh, not parsedecl.hh. * src/tgbaparse/tgbascan.ll: Likewise, include tgbaparse/parsedecl.hh. diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am index c4641b07e..6e06e84cb 100644 --- a/src/ltltest/Makefile.am +++ b/src/ltltest/Makefile.am @@ -1,4 +1,5 @@ AM_CPPFLAGS = -I$(srcdir)/.. +AM_CXXFLAGS = $(WARNING_CXXFLAGS) LDADD = ../ltlparse/libltlparse.la \ ../ltlvisit/libltlvisit.la \ ../ltlenv/libltlenv.la \ diff --git a/src/tgba/bdddict.cc b/src/tgba/bdddict.cc index 5a344690e..9e507ddcd 100644 --- a/src/tgba/bdddict.cc +++ b/src/tgba/bdddict.cc @@ -41,6 +41,20 @@ namespace spot return num; } + void + bdd_dict::register_propositions(bdd f, const void* for_me) + { + if (f == bddtrue || f == bddfalse) + return; + + vf_map::iterator i = var_formula_map.find(bdd_var(f)); + assert(i != var_formula_map.end()); + var_refs[i->first].insert(for_me); + + register_propositions(bdd_high(f), for_me); + register_propositions(bdd_low(f), for_me); + } + int bdd_dict::register_state(const ltl::formula* f, const void* for_me) { @@ -88,6 +102,21 @@ namespace spot return num; } + void + bdd_dict::register_accepting_variables(bdd f, const void* for_me) + { + if (f == bddtrue || f == bddfalse) + return; + + vf_map::iterator i = acc_formula_map.find(bdd_var(f)); + assert(i != acc_formula_map.end()); + var_refs[i->first].insert(for_me); + + register_accepting_variables(bdd_high(f), for_me); + register_accepting_variables(bdd_low(f), for_me); + } + + void bdd_dict::register_all_variables_of(const void* from_other, const void* for_me) diff --git a/src/tgba/bdddict.hh b/src/tgba/bdddict.hh index 30fae1270..ab49d0c3e 100644 --- a/src/tgba/bdddict.hh +++ b/src/tgba/bdddict.hh @@ -54,6 +54,15 @@ namespace spot /// to convert this to a BDD. int register_proposition(const ltl::formula* f, const void* for_me); + /// \brief Register BDD variables as atomic propositions. + /// + /// Register all variables occurring in \a f as atomic propositions + /// used by \a for_me. This assumes that these atomic propositions + /// are already known from the dictionary (i.e., they have already + /// been registered by register_proposition() for another + /// automaton). + void register_propositions(bdd f, const void* for_me); + /// \brief Register a couple of Now/Next variables /// /// Return (and maybe allocate) two BDD variables for a state @@ -79,6 +88,15 @@ namespace spot /// to convert this to a BDD. int register_accepting_variable(const ltl::formula* f, const void* for_me); + /// \brief Register BDD variables as accepting variables. + /// + /// Register all variables occurring in \a f as accepting variables + /// used by \a for_me. This assumes that these accepting variables + /// are already known from the dictionary (i.e., they have already + /// been registered by register_accepting_variable() for another + /// automaton). + void register_accepting_variables(bdd f, const void* for_me); + /// \brief Duplicate the variable usage of another object. /// /// This tells this dictionary that the \a for_me object diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc index 02edc2b4d..eed9820f0 100644 --- a/src/tgba/tgbaexplicit.cc +++ b/src/tgba/tgbaexplicit.cc @@ -119,7 +119,7 @@ namespace spot // The first state we add is the inititial state. // It can also be overridden with set_init_state(). - if (! init_) + if (!init_) init_ = s; return s; @@ -170,6 +170,13 @@ namespace spot t->condition -= get_condition(f); } + void + tgba_explicit::add_conditions(transition* t, bdd f) + { + dict_->register_propositions(f, this); + t->condition &= f; + } + void tgba_explicit::declare_accepting_condition(ltl::formula* f) { @@ -245,9 +252,25 @@ namespace spot t->accepting_conditions |= c; } + void + tgba_explicit::add_accepting_conditions(transition* t, bdd f) + { + bdd sup = bdd_support(f); + dict_->register_accepting_variables(sup, this); + while (sup != bddtrue) + { + neg_accepting_conditions_ &= bdd_nithvar(bdd_var(sup)); + sup = bdd_high(sup); + } + t->accepting_conditions |= f; + } + state* tgba_explicit::get_init_state() const { + // Fix empty automata by adding a lone initial state. + if (!init_) + const_cast(this)->add_state("empty"); return new state_explicit(init_); } diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index 68295feca..df726d92a 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -36,9 +36,13 @@ namespace spot void add_condition(transition* t, ltl::formula* f); void add_neg_condition(transition* t, ltl::formula* f); + /// This assumes that all variables in \a f are known from dict. + void add_conditions(transition* t, bdd f); void declare_accepting_condition(ltl::formula* f); bool has_accepting_condition(ltl::formula* f) const; void add_accepting_condition(transition* t, ltl::formula* f); + /// This assumes that all accepting conditions in \a f are known from dict. + void add_accepting_conditions(transition* t, bdd f); void complement_all_accepting_conditions(); // tgba interface diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 2eb5877b5..f024dbe99 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -4,22 +4,24 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS) tgbaalgosdir = $(pkgincludedir)/tgbaalgos tgbaalgos_HEADERS = \ - reachiter.hh \ dotty.hh \ + dupexp.hh \ + emptinesscheck.hh \ lbtt.hh \ ltl2tgba_fm.hh \ ltl2tgba_lacim.hh \ magic.hh \ - emptinesscheck.hh \ + reachiter.hh \ save.hh noinst_LTLIBRARIES = libtgbaalgos.la libtgbaalgos_la_SOURCES = \ - reachiter.cc \ dotty.cc \ + dupexp.cc \ + emptinesscheck.cc \ lbtt.cc \ ltl2tgba_fm.cc \ ltl2tgba_lacim.cc \ magic.cc \ - emptinesscheck.cc \ + reachiter.cc \ save.cc diff --git a/src/tgbaalgos/dupexp.cc b/src/tgbaalgos/dupexp.cc new file mode 100644 index 000000000..ce9f724d6 --- /dev/null +++ b/src/tgbaalgos/dupexp.cc @@ -0,0 +1,91 @@ +#include "dupexp.hh" +#include +#include +#include +#include "reachiter.hh" + +namespace spot { + + template + class dupexp_iter: public T + { + public: + dupexp_iter(const tgba* a) + : T(a), out_(new tgba_explicit(a->get_dict())) + { + } + + tgba_explicit* + result() + { + return out_; + } + + void + process_state(const state* s, int n, tgba_succ_iterator*) + { + std::ostringstream os; + os << "(#" << n << ") " << automata_->format_state(s); + name_[n] = os.str(); + } + + std::string + declare_state(const state* s, int n) + { + std::string str; + name_map_::const_iterator i = name_.find(n); + if (i == name_.end()) + { + std::ostringstream os; + os << "(#" << n << ") " << automata_->format_state(s); + name_[n] = str = os.str(); + } + else + { + str = i->second; + } + delete s; + return str; + } + + void + process_link(int in, int out, const tgba_succ_iterator* si) + { + // We might need to format out before process_state is called. + name_map_::const_iterator i = name_.find(out); + if (i == name_.end()) + { + const state* s = si->current_state(); + process_state(s, out, 0); + delete s; + } + + tgba_explicit::transition* t = + out_->create_transition(name_[in], name_[out]); + out_->add_conditions(t, si->current_condition()); + out_->add_accepting_conditions(t, si->current_accepting_conditions()); + } + + private: + tgba_explicit* out_; + typedef std::map name_map_; + std::map name_; + }; + + tgba_explicit* + tgba_dupexp_bfs(const tgba* aut) + { + dupexp_iter di(aut); + di.run(); + return di.result(); + } + + tgba_explicit* + tgba_dupexp_dfs(const tgba* aut) + { + dupexp_iter di(aut); + di.run(); + return di.result(); + } + +} diff --git a/src/tgbaalgos/dupexp.hh b/src/tgbaalgos/dupexp.hh new file mode 100644 index 000000000..d54740985 --- /dev/null +++ b/src/tgbaalgos/dupexp.hh @@ -0,0 +1,16 @@ +#ifndef SPOT_TGBAALGOS_DUPEXPL_HH +# define SPOT_TGBAALGOS_DUPEXPL_HH + +# include "tgba/tgbaexplicit.hh" + +namespace spot +{ + /// Build an explicit automata from all states of \a aut, numbering + /// states in bread first order as they are processed. + tgba_explicit* tgba_dupexp_bfs(const tgba* aut); + /// Build an explicit automata from all states of \a aut, numbering + /// states in depth first order as they are processed. + tgba_explicit* tgba_dupexp_dfs(const tgba* aut); +} + +#endif // SPOT_TGBAALGOS_DUPEXPL_HH diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 22631fac2..201214d7e 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -1,4 +1,5 @@ AM_CPPFLAGS = -I$(srcdir)/.. $(BUDDY_CPPFLAGS) +AM_CXXFLAGS = $(WARNING_CXXFLAGS) LDADD = ../libspot.la check_SCRIPTS = defs @@ -40,10 +41,11 @@ TESTS = \ explpro3.test \ tripprod.test \ mixprod.test \ + dupexp.test \ emptchk.test \ emptchke.test \ spotlbtt.test EXTRA_DIST = $(TESTS) -CLEANFILES = input input1 input2 input3 stdout expected config +CLEANFILES = input input1 input2 input3 stdout expected config output1 output2 diff --git a/src/tgbatest/dupexp.test b/src/tgbatest/dupexp.test new file mode 100755 index 000000000..6b71f531a --- /dev/null +++ b/src/tgbatest/dupexp.test @@ -0,0 +1,30 @@ +#!/bin/sh + +. ./defs + +set -e + +run() +{ + ./ltl2tgba -f -s "$1" >output1 + ./ltl2tgba -f -S "$1" >output2 + test `wc -l output1 + ./ltl2tgba -S "$1" >output2 + test `wc -l (F x))' +run '!((FF a) <=> (F a))' +run 'Xa && (!a U b) && !b && X!b' +run '(a U !b) && Gb' diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 8e852f9f2..f117ec7a4 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -14,6 +14,7 @@ #include "tgbaalgos/magic.hh" #include "tgbaalgos/emptinesscheck.hh" #include "tgbaparse/public.hh" +#include "tgbaalgos/dupexp.hh" void syntax(char* prog) @@ -45,6 +46,10 @@ syntax(char* prog) << " -r display the relation BDD, not the reachability graph" << std::endl << " -R same as -r, but as a set" << std::endl + << " -s convert to explicit automata, and number states " + << "in DFS order" << std::endl + << " -S convert to explicit automata, and number states " + << "in BFS order" << std::endl << " -t display reachable states in LBTT's format" << std::endl << " -v display the BDD variables used by the automaton" << std::endl @@ -65,6 +70,7 @@ main(int argc, char** argv) int output = 0; int formula_index = 0; enum { None, Couvreur, MagicSearch } echeck = None; + enum { NoneDup, BFS, DFS } dupexp = NoneDup; bool magic_many = false; bool expect_counter_example = false; bool from_file = false; @@ -142,6 +148,14 @@ main(int argc, char** argv) { output = 3; } + else if (!strcmp(argv[formula_index], "-s")) + { + dupexp = DFS; + } + else if (!strcmp(argv[formula_index], "-S")) + { + dupexp = BFS; + } else if (!strcmp(argv[formula_index], "-t")) { output = 6; @@ -218,6 +232,19 @@ main(int argc, char** argv) if (degeneralize_opt) a = degeneralized = new spot::tgba_tba_proxy(a); + spot::tgba_explicit* expl = 0; + switch (dupexp) + { + case NoneDup: + break; + case BFS: + a = expl = tgba_dupexp_bfs(a); + break; + case DFS: + a = expl = tgba_dupexp_dfs(a); + break; + } + switch (output) { case -1: @@ -305,6 +332,8 @@ main(int argc, char** argv) break; } + if (expl) + delete expl; if (degeneralize_opt) delete degeneralized; diff --git a/src/tgbatest/tgbaread.cc b/src/tgbatest/tgbaread.cc index d22a32fa4..9b9b2c1d2 100644 --- a/src/tgbatest/tgbaread.cc +++ b/src/tgbatest/tgbaread.cc @@ -15,8 +15,6 @@ syntax(char* prog) int main(int argc, char** argv) { - int exit_code = 0; - if (argc < 2) syntax(argv[0]);