diff --git a/ChangeLog b/ChangeLog index c1d9cc9aa..bbf1c5bcb 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,12 @@ 2003-06-26 Alexandre Duret-Lutz + * src/tgba/succiter.hh: Adjust comments about promises to + refer to accepting conditions. + * src/tgba/tgbabddconcretefactory.hh: Likewise. + * src/tgba/tgbabddcoredata.hh: Likewise. + * src/tgba/dictunion.cc: Likewise. + * src/tgba/tgba.hh: Likewise. + * doc/Makefile.am (doc): Typo. * src/ltlvisit/tostring.hh (to_string): Add doxygen comments. * src/ltlast/multop.hh (multop::paircmp): Add doxygen comments. diff --git a/src/tgba/dictunion.cc b/src/tgba/dictunion.cc index 7ac857e13..5c745db92 100644 --- a/src/tgba/dictunion.cc +++ b/src/tgba/dictunion.cc @@ -12,7 +12,7 @@ namespace spot { std::set now; std::set var; - std::set prom; + std::set acc; tgba_bdd_dict::fv_map::const_iterator i; @@ -28,21 +28,21 @@ namespace spot for (i = r.var_map.begin(); i != r.var_map.end(); ++i) var.insert(i->first); - // Merge promises. + // Merge accepting conditions. for (i = l.acc_map.begin(); i != l.acc_map.end(); ++i) - prom.insert(i->first); + acc.insert(i->first); for (i = r.acc_map.begin(); i != r.acc_map.end(); ++i) - prom.insert(i->first); + acc.insert(i->first); // Ensure we have enough BDD variables. int have = bdd_extvarnum(0); - int want = now.size() * 2 + var.size() + prom.size(); + int want = now.size() * 2 + var.size() + acc.size(); if (have < want) bdd_setvarnum(want); // Fill in the "defragmented" union dictionary. - // FIXME: Make some experiments with ordering of prom/var/now variables. + // FIXME: Make some experiments with ordering of acc/var/now variables. // Maybe there is one order that usually produces smaller BDDs? // Next BDD variable to use. @@ -51,7 +51,7 @@ namespace spot tgba_bdd_dict res; std::set::const_iterator f; - for (f = prom.begin(); f != prom.end(); ++f) + for (f = acc.begin(); f != acc.end(); ++f) { clone(*f); res.acc_map[*f] = v; diff --git a/src/tgba/succiter.hh b/src/tgba/succiter.hh index 2c4740259..7a382db15 100644 --- a/src/tgba/succiter.hh +++ b/src/tgba/succiter.hh @@ -11,8 +11,8 @@ namespace spot /// This class provides the basic functionalities required to /// iterate over the successors of a state, as well as querying /// transition labels. Because transitions are never explicitely - /// encoded, labels (conditions and promises) can only be queried - /// while iterating over the successors. + /// encoded, labels (conditions and accepting conditions) can only + /// be queried while iterating over the successors. class tgba_succ_iterator { public: @@ -63,8 +63,7 @@ namespace spot /// Note that the same state may occur at different points /// in the iteration. These actually correspond to the same /// destination. It just means there were several transitions, - /// with different conditions or promises, leading to the - /// same state. + /// with different conditions, leading to the same state. virtual state* current_state() = 0; /// \brief Get the condition on the transition leading to this successor. virtual bdd current_condition() = 0; diff --git a/src/tgba/tgbabddconcretefactory.hh b/src/tgba/tgbabddconcretefactory.hh index dadac1d60..c827d496a 100644 --- a/src/tgba/tgbabddconcretefactory.hh +++ b/src/tgba/tgbabddconcretefactory.hh @@ -56,8 +56,8 @@ namespace spot /// \brief Perfom final computations before the relation can be used. /// /// This function should be called after all propositions, state, - /// promise, and constraints have been declared, and before calling - /// get_code_data() or get_dict(). + /// accepting conditions, and constraints have been declared, and + /// before calling get_code_data() or get_dict(). void finish(); private: diff --git a/src/tgba/tgbabddcoredata.hh b/src/tgba/tgbabddcoredata.hh index 98e1ec085..fca5e44d7 100644 --- a/src/tgba/tgbabddcoredata.hh +++ b/src/tgba/tgbabddcoredata.hh @@ -19,36 +19,37 @@ namespace spot /// \brief encodes the accepting conditions /// - /// \c a \c U \c b, or \c F \c b, both imply that \c b - /// should be verified eventually. We encode this with generalized - /// Büchi acceptating conditions. An accepting set, called Acc[b], - /// hold all the state that do not promise to verify \c b eventually. - /// (I.e., all the states that contain \c b, or do not conatain - /// \c a \c U \c b, or \c F \c b.) + /// a U b, or F b, both imply that \c b should + /// be verified eventually. We encode this with generalized Büchi + /// acceptating conditions. An accepting set, called + /// Acc[b], hold all the state that do not promise to + /// verify \c b eventually. (I.e., all the states that contain \c + /// b, or do not contain a U b, or F b.) /// /// The spot::succ_iter::current_accepting_conditions() method - /// will return the Acc[x] variables of the accepting sets - /// in which a transition is. Actually we never return Acc[x] - /// alone, but Acc[x] and all other accepting variables negated. + /// will return the \c Acc[x] variables of the accepting sets + /// in which a transition is. Actually we never return \c Acc[x] + /// alone, but \c Acc[x] and all other accepting variables negated. /// - /// So if there is three accepting set \c a, \c b, and \c c, and - /// a transition is in set \c a, we'll return \c Acc[a]&!Acc[b]&!Acc[c]. - /// If the transition is in both \c a and \c b, we'll return - /// \c (Acc[a]\&!Acc[b]\&!Acc[c]) \c | \c (!Acc[a]\&Acc[b]\&!Acc[c]). + /// So if there is three accepting set \c a, \c b, and \c c, and a + /// transition is in set \c a, we'll return + /// Acc[a]&!Acc[b]&!Acc[c]. If the transition is in both \c + /// a and \c b, we'll return (Acc[a]\&!Acc[b]\&!Acc[c]) \c | \c + /// (!Acc[a]\&Acc[b]\&!Acc[c]). /// /// Accepting conditions are attributed to transitions and are /// only concerned by atomic propositions (which label the /// transitions) and Next variables (the destination). Typically, - /// a transition should bear the variable Acc[b] if it doesn't - /// check for `b' and have a destination of the form \c a \c U \c - /// b, or \c F \c b. + /// a transition should bear the variable \c Acc[b] if it doesn't + /// check for `b' and have a destination of the form a U b, + /// or F b. /// /// To summarize, \c accepting_conditions contains three kinds of /// variables: /// \li "Next" variables, that encode the destination state, /// \li atomic propositions, which are things to verify before going on /// to the next state, - /// \li promise variables. + /// \li "Acc" variables. bdd accepting_conditions; /// The set of all accepting conditions used by the Automaton.