diff --git a/ChangeLog b/ChangeLog index 889647914..07a0800b0 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,9 @@ +2004-09-23 Alexandre Duret-Lutz + + * src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): New unobs argument. + * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Handle unobs. + * src/tgbatest/ltl2tgba.cc (syntax, main): New -U option. + 2004-09-21 Alexandre Duret-Lutz * src/tgbaalgos/colordfs.hh, src/tgbaalgos/minimalce.cc, diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 2bf456846..20b1becbc 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -30,8 +30,9 @@ #include "ltlvisit/destroy.hh" #include "ltlvisit/tostring.hh" #include "ltlvisit/postfix.hh" +#include "ltlvisit/apcollect.hh" #include - +#include #include "tgba/tgbabddconcretefactory.hh" #include "ltl2tgba_fm.hh" @@ -639,7 +640,7 @@ namespace spot tgba_explicit* ltl_to_tgba_fm(const formula* f, bdd_dict* dict, bool exprop, bool symb_merge, bool branching_postponement, - bool fair_loop_approx) + bool fair_loop_approx, const ltl::atomic_prop_set* unobs) { possible_fair_loop_checker pflc; @@ -659,13 +660,47 @@ namespace spot // Compute the set of all promises occurring inside the formula. bdd all_promises = bddtrue; - if (fair_loop_approx) + if (fair_loop_approx || unobs) { ltl_promise_visitor pv(d); f2->accept(pv); all_promises = pv.result(); } + // These are used when atomic propositions are interpreted as + // events. There are two kinds of events: observable events are + // those used in the formula, and unobservable events or other + // events that can occur at anytime. All events exclude each + // other. + bdd observable_events = bddfalse; + bdd unobservable_events = bddfalse; + if (unobs) + { + bdd neg_events = bddtrue; + std::auto_ptr aps(ltl::atomic_prop_collect(f)); + for (ltl::atomic_prop_set::const_iterator i = aps->begin(); + i != aps->end(); ++i) + { + int p = d.register_proposition(*i); + bdd pos = bdd_ithvar(p); + bdd neg = bdd_nithvar(p); + observable_events = (observable_events & neg) | (neg_events & pos); + neg_events &= neg; + } + for (ltl::atomic_prop_set::const_iterator i = unobs->begin(); + i != unobs->end(); ++i) + { + int p = d.register_proposition(*i); + bdd pos = bdd_ithvar(p); + bdd neg = bdd_nithvar(p); + unobservable_events = ((unobservable_events & neg) + | (neg_events & pos)); + observable_events &= neg; + neg_events &= neg; + } + } + bdd all_events = observable_events | unobservable_events; + formulae_seen.insert(f2); formulae_to_translate.insert(f2); @@ -682,6 +717,14 @@ namespace spot // Translate it into a BDD to simplify it. bdd res = fc.translate(f); + // Handle exclusive events. + if (unobs) + { + res &= observable_events; + int n = d.register_next_variable(f); + res |= unobservable_events & bdd_ithvar(n) & all_promises; + } + std::string now = to_string(f); // When branching_postponement is used, we must assume that @@ -818,6 +861,11 @@ namespace spot assert(j->first == bddtrue); cond_for_true = j->second; + // When translating LTL for an event-based logic with + // unobservable events, the 1 state should accept even + // unobservable events. + if (unobs && f == constant::true_instance()) + cond_for_true = all_events; tgba_explicit::transition* t = a->create_transition(now, constant::true_instance()->val_name()); a->add_condition(t, d.bdd_to_formula(cond_for_true)); diff --git a/src/tgbaalgos/ltl2tgba_fm.hh b/src/tgbaalgos/ltl2tgba_fm.hh index 044dd26b4..ef36d0522 100644 --- a/src/tgbaalgos/ltl2tgba_fm.hh +++ b/src/tgbaalgos/ltl2tgba_fm.hh @@ -24,6 +24,7 @@ #include "ltlast/formula.hh" #include "tgba/tgbaexplicit.hh" +#include "ltlvisit/apcollect.hh" namespace spot { @@ -89,11 +90,16 @@ namespace spot /// unstable state is used to suppress all acceptance conditions from /// incoming transitions. /// + /// \param unobs When non-zero, the atomic propositions in the LTL formula + /// are interpreted as events that exclude each other. The events in the + /// formula are observable events, and \c unobs can be filled with + /// additional unobservable events. /// \return A spot::tgba_explicit that recognizes the language of \a f. tgba_explicit* ltl_to_tgba_fm(const ltl::formula* f, bdd_dict* dict, bool exprop = false, bool symb_merge = true, bool branching_postponement = false, - bool fair_loop_approx = false); + bool fair_loop_approx = false, + const ltl::atomic_prop_set* unobs = 0); } #endif // SPOT_TGBA_LTL2TGBA_HH diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 575af9cf5..6479c8752 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -26,6 +26,7 @@ #include "ltlvisit/destroy.hh" #include "ltlvisit/reduce.hh" #include "ltlvisit/tostring.hh" +#include "ltlvisit/apcollect.hh" #include "ltlast/allnodes.hh" #include "ltlparse/public.hh" #include "tgbaalgos/ltl2tgba_lacim.hh" @@ -45,7 +46,6 @@ #include "tgbaparse/public.hh" #include "tgbaalgos/dupexp.hh" #include "tgbaalgos/neverclaim.hh" - #include "tgbaalgos/reductgba_sim.hh" void @@ -152,6 +152,8 @@ syntax(char* prog) << std::endl << " -TJ tarjan-on-fly (implies -D), expect no counter-example" << std::endl + << " -U[PROPS] consider atomic properties PROPS as exclusive " + << "events (implies -f)" << std::endl << " -v display the BDD variables used by the automaton" << std::endl << " -x try to produce a more deterministic automata " @@ -193,6 +195,8 @@ main(int argc, char** argv) bool display_parity_game = false; bool post_branching = false; bool fair_loop_approx = false; + spot::ltl::environment& env(spot::ltl::default_environment::instance()); + spot::ltl::atomic_prop_set* unobservables = 0; for (;;) { @@ -470,6 +474,19 @@ main(int argc, char** argv) expect_counter_example = false; output = -1; } + else if (!strncmp(argv[formula_index], "-U", 2)) + { + unobservables = new spot::ltl::atomic_prop_set; + fm_opt = true; + // Parse -U's argument. + const char* tok = strtok(argv[formula_index] + 2, ",; \t"); + while (tok) + { + unobservables->insert + (static_cast(env.require(tok))); + tok = strtok(0, ",; \t"); + } + } else if (!strcmp(argv[formula_index], "-v")) { output = 5; @@ -523,7 +540,6 @@ main(int argc, char** argv) input = argv[formula_index]; } - spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::bdd_dict* dict = new spot::bdd_dict(); spot::ltl::formula* f = 0; @@ -563,7 +579,7 @@ main(int argc, char** argv) to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt, fm_symb_merge_opt, post_branching, - fair_loop_approx); + fair_loop_approx, unobservables); else to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict); }