From c5f8eafb017f8ac4b9d4e6d05b100b15733a59fa Mon Sep 17 00:00:00 2001 From: Guillaume Sadegh Date: Tue, 24 Feb 2009 15:01:29 +0100 Subject: [PATCH] =?UTF-8?q?Add=20an=20algorithm=20to=20complement=20B?= =?UTF-8?q?=C3=BCchi=20automata.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * src/tgba/tgbacomplement.hh, src/tgba/tgbacomplement.cc: New files. The complementation algorithm. * src/tgba/Makefile.am: Adjust. * src/tgbatest/complementation.test, src/tgbatest/complementation.cc: New files. Test suite for the complementation algorithm. * src/tgbatest/Makefile.am: Adjust. * src/tgbaalgos/Makefile.am: Reformat the header using 80 columns. --- ChangeLog | 14 + src/tgba/Makefile.am | 4 +- src/tgba/tgbacomplement.cc | 1247 +++++++++++++++++++++++++++++ src/tgba/tgbacomplement.hh | 68 ++ src/tgbaalgos/Makefile.am | 3 +- src/tgbatest/Makefile.am | 5 +- src/tgbatest/complementation.cc | 217 +++++ src/tgbatest/complementation.test | 31 + 8 files changed, 1586 insertions(+), 3 deletions(-) create mode 100644 src/tgba/tgbacomplement.cc create mode 100644 src/tgba/tgbacomplement.hh create mode 100644 src/tgbatest/complementation.cc create mode 100755 src/tgbatest/complementation.test diff --git a/ChangeLog b/ChangeLog index d50e50db5..d71deb53a 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,17 @@ +2009-06-05 Guillaume Sadegh + + Add an algorithm to complement Büchi automata. + + * src/tgba/tgbacomplement.hh, src/tgba/tgbacomplement.cc: New + files. The complementation algorithm. + * src/tgba/Makefile.am: Adjust. + * src/tgbatest/complementation.test, + src/tgbatest/complementation.cc: New files. Test suite for the + complementation algorithm. + * src/tgbatest/Makefile.am: Adjust. + * src/tgbaalgos/Makefile.am: Reformat the header using 80 + columns. + 2009-06-05 Damien Lefortier Modify the ELTL parser to be able to support PSL operators. Add a diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index 322a8e562..624f2f031 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2003, 2004, 2009 Laboratoire d'Informatique de Paris 6 (LIP6), +## Copyright (C) 2003, 2004, 2009 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre ## et Marie Curie. ## @@ -41,6 +41,7 @@ tgba_HEADERS = \ tgbabddcoredata.hh \ tgbabddfactory.hh \ tgbascc.hh \ + tgbacomplement.hh \ tgbaexplicit.hh \ tgbaproduct.hh \ tgbatba.hh \ @@ -60,6 +61,7 @@ libtgba_la_SOURCES = \ tgbabddconcreteproduct.cc \ tgbabddcoredata.cc \ tgbascc.cc \ + tgbacomplement.cc \ tgbaexplicit.cc \ tgbaproduct.cc \ tgbatba.cc \ diff --git a/src/tgba/tgbacomplement.cc b/src/tgba/tgbacomplement.cc new file mode 100644 index 000000000..3b5cbb333 --- /dev/null +++ b/src/tgba/tgbacomplement.cc @@ -0,0 +1,1247 @@ +// Copyright (C) 2009 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include +#include +#include +#include +#include +#include +#include "bdd.h" +#include "misc/bddlt.hh" +#include "tgba/tgbatba.hh" +#include "tgba/bdddict.hh" +#include "tgba/state.hh" +#include "misc/hashfunc.hh" +#include "ltlast/formula.hh" +#include "ltlast/constant.hh" +#include "tgbaalgos/dotty.hh" +#include "tgba/tgbacomplement.hh" + +namespace spot +{ + typedef boost::dynamic_bitset<> bitset_t; + + namespace + { + // forward decl. + struct safra_tree; + struct safra_tree_ptr_less_than: + public std::binary_function + { + bool + operator()(const safra_tree* left, + const safra_tree* right) const; + }; + } // anonymous. + + /// \brief Automaton with Safra's tree as states. + struct safra_tree_automaton + { + safra_tree_automaton(const tgba* sba); + ~safra_tree_automaton(); + typedef std::map transition_list; + typedef + std::map + automaton_t; + automaton_t automaton; + + /// \brief The number of acceptance pairs of this Rabin (Streett) + /// automaton. + int get_nb_acceptance_pairs() const; + safra_tree* get_initial_state() const; + void set_initial_state(safra_tree* s); + private: + mutable int max_nb_pairs_; + safra_tree* initial_state; + const tgba* a_; + }; + + namespace + { + /// \brief A Safra tree, used as state during the determinization + /// of a Büchi automaton + /// + /// It is the key structure of the construction. + /// Each node of the tree has: + /// - A \a name, + /// - A subset of states of the original Büchi automaton (\a nodes), + /// - A flag that is \a marked to denote vertical merge of nodes, + /// - A list of \a children. + /// + /// This class implements operations: + /// - To compute the successor of this tree, + /// - To retrive acceptance condition on this tree. + /// \see safra_determinisation. + struct safra_tree + { + typedef std::set subset_t; + typedef std::list child_list; + typedef std::multimap tr_cache_t; + typedef std::map cache_t; + + safra_tree(); + safra_tree(const safra_tree& other); + safra_tree(const subset_t& nodes, safra_tree* p, int n); + ~safra_tree(); + + const safra_tree& operator=(const safra_tree& other); + int compare(const safra_tree* other) const; + + void add_node(const state* s); + int max_name() const; + + // Operations to get successors of a tree. + safra_tree* branch_accepting(const tgba_sba_proxy& a); + safra_tree* succ_create(const bdd& condition, + cache_t& cache_transition); + safra_tree* normalize_siblings(); + safra_tree* remove_empty(); + safra_tree* mark(); + + // To get Rabin/Streett acceptance conditions. + void getL(bitset_t& bitset) const; + void getU(bitset_t& bitset) const; + + /// \brief Does this node the root of the tree? + bool is_parent() const + { + return parent == 0; + } + + bool marked; + int name; + subset_t nodes; + child_list children; + private: + void remove_node_from_children(const state* state); + int get_new_name() const; + mutable std::deque free_names_; // Some free names. + safra_tree* parent; + }; + + safra_tree::safra_tree() + : marked(false), name(0) + { + parent = 0; + } + + /// \brief Copy the tree \a other, and set \c marked to false. + safra_tree::safra_tree(const safra_tree& other) + : marked(false) + { + name = other.name; + parent = 0; + nodes = other.nodes; + for (child_list::const_iterator i = other.children.begin(); + i != other.children.end(); ++i) + { + safra_tree* c = new safra_tree(**i); + c->parent = this; + children.push_back(c); + } + } + + safra_tree::safra_tree(const subset_t& nodes, safra_tree* p, int n) + : marked(false), name(n), nodes(nodes) + { + parent = p; + } + + safra_tree::~safra_tree() + { + for (child_list::iterator i = children.begin(); i != children.end(); ++i) + delete *i; + + for (subset_t::iterator i = nodes.begin(); i != nodes.end(); ++i) + delete *i; + } + + const safra_tree& + safra_tree::operator=(const safra_tree& other) + { + if (this != &other) + { + this->~safra_tree(); + new (this) safra_tree(other); + } + return *this; + } + + /// \brief Compare two safra trees. + /// + /// \param other + /// + /// \return 0 if the trees are the same. Otherwise + /// a signed value. + int safra_tree::compare(const safra_tree* other) const + { + int subset_compare = 0; + subset_t::const_iterator in1 = nodes.begin(); + subset_t::const_iterator in2 = other->nodes.begin(); + + if (nodes.size() != other->nodes.size()) + return (nodes.size() - other->nodes.size()); + + if (name != other->name) + return name - other->name; + + for (; in1 != nodes.end() && in2 != other->nodes.end(); ++in1, ++in2) + if ((subset_compare = (*in1)->compare(*in2)) != 0) + break; + + if (subset_compare != 0) + return subset_compare; + + child_list::const_iterator ic1 = children.begin(); + child_list::const_iterator ic2 = other->children.begin(); + + if (children.size() != other->children.size()) + return (children.size() - other->children.size()); + + for (; ic1 != children.end() && ic2 != other->children.end(); + ++ic1, ++ic2) + { + int compare_value = (*ic1)->compare(*ic2); + if (compare_value != 0) + return compare_value; + } + + if (marked != other->marked) + return (marked) ? -1 : 1; + + return 0; + } + + void + safra_tree::add_node(const state* s) + { + nodes.insert(s); + } + + /*---------------------------------. + | Operations to compute successors | + `---------------------------------*/ + + int + safra_tree::max_name() const + { + int max_name = name; + for (child_list::const_iterator i = children.begin(); + i != children.end(); ++i) + max_name = std::max(max_name, (*i)->max_name()); + return max_name; + } + + /// \brief Get an unused name in the tree for a new node. + /// + /// The root of the tree maintains a list of unused names. + /// When this list is empty, new names are computed. + int + safra_tree::get_new_name() const + { + if (parent == 0) + { + if (free_names_.empty()) + { + std::set used_names; + std::deque queue; + queue.push_back(this); + while (!queue.empty()) + { + const safra_tree* current = queue.front(); + queue.pop_front(); + used_names.insert(current->name); + for (child_list::const_iterator i = current->children.begin(); + i != current->children.end(); ++i) + queue.push_back(*i); + } + + int l = 0; + int nb_found = 0; + std::set::const_iterator i = used_names.begin(); + while (i != used_names.end() && nb_found != 3) + { + if (l != *i) + { + free_names_.push_back(l); + ++nb_found; + } + else + ++i; + ++l; + } + + while (nb_found++ < 3) + free_names_.push_back(l++); + } + + int result = free_names_.front(); + free_names_.pop_front(); + return result; + } + else + return parent->get_new_name(); + } + + /// If the node has an accepting state in its label, a new child + /// is inserted with the set of all accepting states of \c nodes + /// as label and an unused name. + safra_tree* + safra_tree::branch_accepting(const tgba_sba_proxy& a) + { + for (child_list::iterator i = children.begin(); i != children.end(); ++i) + (*i)->branch_accepting(a); + + subset_t subset; + for(subset_t::const_iterator i = nodes.begin(); i != nodes.end(); ++i) + if (a.state_is_accepting(*i)) + subset.insert(*i); + + if (!subset.empty()) + children.push_back(new safra_tree(subset, this, get_new_name())); + + return this; + } + + /// \brief A powerset construction. + /// + /// The successors of each state in \c nodes with \a condition + /// as atomic property remplace the current \c nodes set. + /// + /// @param cache_transition is a map of the form: state -> bdd -> state. + /// Only states present in \c nodes are keys of the map. + /// @param condition is an atomic property. We are looking for successors + /// of this atomic property. + safra_tree* + safra_tree::succ_create(const bdd& condition, + cache_t& cache_transition) + { + subset_t new_subset; + + for (subset_t::iterator i = nodes.begin(); i != nodes.end(); ++i) + { + if (cache_transition.find(*i) == cache_transition.end()) + continue; + + tr_cache_t transitions = cache_transition[*i]; + for (tr_cache_t::const_iterator t_it = transitions.begin(); + t_it != transitions.end(); + ++t_it) + { + if (((*t_it).first & condition) != bddfalse) + { + if (new_subset.find((*t_it).second) == new_subset.end()) + { + const state* s = (*t_it).second->clone(); + new_subset.insert(s); + } + } + } + } + nodes = new_subset; + + for (child_list::iterator i = children.begin(); i != children.end(); ++i) + (*i)->succ_create(condition, cache_transition); + + return this; + } + + /// \brief Horizontal Merge + /// + /// If many children share the same state in their labels, we must keep + /// only one occurrence (in the older node). + safra_tree* + safra_tree::normalize_siblings() + { + std::set node_set; + for (child_list::iterator child_it = children.begin(); + child_it != children.end(); + ++child_it) + { + subset_t::iterator node_it = (*child_it)->nodes.begin(); + while (node_it != (*child_it)->nodes.end()) + { + if (node_set.find(*node_it) != node_set.end()) + { + const state* s = *node_it; + (*child_it)->remove_node_from_children(*node_it); + (*child_it)->nodes.erase(node_it++); + delete s; + } + else + { + node_set.insert(*node_it); + ++node_it; + } + } + + (*child_it)->normalize_siblings(); + } + + return this; + } + + /// \brief Remove recursively all the occurrences of \c state in the label. + void + safra_tree::remove_node_from_children(const state* state) + { + for (child_list::iterator child_it = children.begin(); + child_it != children.end(); + ++child_it) + { + subset_t::iterator it = (*child_it)->nodes.find(state); + if (it != (*child_it)->nodes.end()) + { + const spot::state* s = *it; + (*child_it)->nodes.erase(it); + delete s; + } + (*child_it)->remove_node_from_children(state); + } + } + + /// \brief Remove empty nodes + /// + /// If a child of the node has an empty label, we remove this child. + safra_tree* + safra_tree::remove_empty() + { + child_list::iterator child_it = children.begin(); + while (child_it != children.end()) + { + if ((*child_it)->nodes.empty()) + { + safra_tree* to_delete = *child_it; + child_it = children.erase(child_it); + delete to_delete; + } + else + { + (*child_it)->remove_empty(); + ++child_it; + } + } + + return this; + } + + /// \brief Vertical merge + /// + /// If a parent has the same states as its childen in its label, + /// All the children a deleted and the node is marked. This mean + /// an accepting infinite run is found. + safra_tree* + safra_tree::mark() + { + std::set node_set; + for (child_list::const_iterator child_it = children.begin(); + child_it != children.end(); + ++child_it) + { + node_set.insert((*child_it)->nodes.begin(), (*child_it)->nodes.end()); + (*child_it)->mark(); + } + + char same = node_set.size() == nodes.size(); + + if (same) + { + subset_t::const_iterator i = node_set.begin(); + subset_t::const_iterator j = nodes.begin(); + + while (i != node_set.end() && j != nodes.end()) + { + if ((*i)->compare(*j) != 0) + { + same = 0; + break; + } + ++i; + ++j; + } + } + + if (same) + { + marked = true; + for (child_list::iterator i = children.begin(); + i != children.end(); + ++i) + delete *i; + children = child_list(); + } + + return this; + } + + /*-----------------------. + | Acceptances conditions | + `-----------------------*/ + + /// Returns in which sets L (the semantic differs according to Rabin or + /// Streett) the state-tree is included. + /// + /// \param bitset a bitset of size \c this->get_nb_acceptance_pairs() + /// filled with FALSE bits. + /// \return bitset[i] will be true if this state-tree is included in L_i + void + safra_tree::getL(bitset_t& bitset) const + { + assert(bitset.size() > static_cast(name)); + if (marked && !nodes.empty()) + bitset[name] = true; + for (child_list::const_iterator i = children.begin(); + i != children.end(); + ++i) + (*i)->getL(bitset); + } + + /// Returns in which sets U (the semantic differs according to Rabin or + /// Streett) the state-tree is included. + /// + /// \param bitset a bitset of size \c this->get_nb_acceptance_pairs() + /// filled with TRUE bits. + /// \return bitset[i] will be true if this state-tree is included in U_i + void + safra_tree::getU(bitset_t& bitset) const + { + assert(bitset.size() > static_cast(name)); + if (!nodes.empty()) + bitset[name] = false; + for (child_list::const_iterator i = children.begin(); + i != children.end(); + ++i) + (*i)->getU(bitset); + } + + bool + safra_tree_ptr_less_than::operator()(const safra_tree* left, + const safra_tree* right) const + { + assert(left); + return left->compare(right) < 0; + } + + struct safra_tree_ptr_equal: + public std::unary_function + { + safra_tree_ptr_equal(const safra_tree* left) + : left_(left) {} + + bool + operator()(const safra_tree* right) const + { + return left_->compare(right) == 0; + } + private: + const safra_tree* left_; + }; + + /// \brief Algorithm to determinize Büchi automaton. + /// + /// Determinization of a Büchi automaton into a Rabin automaton + /// using the Safra's construction. + /// + /// This construction is presented in: + /// @PhDThesis{ safra.89.phd, + /// author = {Shmuel Safra}, + /// title = {Complexity of Automata on Infinite Objects}, + /// school = {The Weizmann Institute of Science}, + /// year = {1989}, + /// address = {Rehovot, Israel}, + /// month = mar + /// } + /// + class safra_determinisation + { + public: + static safra_tree_automaton* create_safra_automaton(const tgba* a); + private: + typedef std::set atomic_list_t; + typedef std::set conjunction_list_t; + static void retrieve_atomics(const safra_tree* node, tgba_sba_proxy* sba, + safra_tree::cache_t& cache, + atomic_list_t& atomic_list); + static void set_atomic_list(atomic_list_t& list, bdd condition); + static conjunction_list_t + get_conj_list(const atomic_list_t& atomics); + }; + + /// \brief The body of Safra's construction. + safra_tree_automaton* + safra_determinisation::create_safra_automaton(const tgba* a) + { + // initialization. + tgba_sba_proxy* sba = new tgba_sba_proxy(a); + + safra_tree_automaton* st = new safra_tree_automaton(sba); + + std::deque queue; + safra_tree* q0 = new safra_tree(); + q0->add_node(sba->get_init_state()); + queue.push_back(q0); + st->set_initial_state(q0); + + // main loop + while (!queue.empty()) + { + safra_tree* current = queue.front(); + // safra_tree* node = new safra_tree(*current); + + // Get conjunction list and save successors. + safra_tree::cache_t cache; + atomic_list_t atomic_list; + retrieve_atomics(current, sba, cache, atomic_list); + conjunction_list_t conjunction = get_conj_list(atomic_list); + + // Create successors of the Safra's tree. + safra_tree_automaton::transition_list transitions; + for (conjunction_list_t::const_iterator i = conjunction.begin(); + i != conjunction.end(); ++i) + { + safra_tree* successor = new safra_tree(*current); + successor->branch_accepting(sba); // Step 2 + successor->succ_create(*i, cache); // Step 3 + successor->normalize_siblings(); // Step 4 + successor->remove_empty(); // Step 5 + successor->mark(); // Step 6 + + bool delete_this_successor = true; + safra_tree_ptr_equal comparator(successor); + if (st->automaton.find(successor) != st->automaton.end()) + { + transitions[*i] = st->automaton.find(successor)->first; + } + else + { + std::deque::iterator item_in_queue = + std::find_if(queue.begin(), queue.end(), comparator); + if (item_in_queue != queue.end()) + { + transitions[*i] = *item_in_queue; + } + else + { + delete_this_successor = false; + transitions[*i] = successor; + queue.push_back(successor); + } + } + if (delete_this_successor) + delete successor; + } + + if (st->automaton.find(current) == st->automaton.end()) + st->automaton[current] = transitions; + + queue.pop_front(); + + for (safra_tree::cache_t::iterator i = cache.begin(); + i != cache.end(); + ++i) + for (safra_tree::tr_cache_t::iterator j = i->second.begin(); + j != i->second.end(); + ++j) + delete j->second; + // delete node; + } + + // delete sba; + return st; + } + + /// Retrieve all atomics properties that are in successors formulae + /// of the states in the label of the node. + void + safra_determinisation::retrieve_atomics(const safra_tree* node, + tgba_sba_proxy* sba, + safra_tree::cache_t& cache, + atomic_list_t& atomic_list) + { + for (safra_tree::subset_t::iterator it = node->nodes.begin(); + it != node->nodes.end(); + ++it) + { + safra_tree::tr_cache_t transitions; + tgba_succ_iterator* iterator = sba->succ_iter(*it); + for (iterator->first(); !iterator->done(); iterator->next()) + { + bdd condition = iterator->current_condition(); + typedef std::pair bdd_state; + transitions.insert(bdd_state(condition, iterator->current_state())); + set_atomic_list(atomic_list, condition); + } + delete iterator; + cache[*it] = transitions; + } + } + + /// Insert in \a list atomic properties of the formula \a c. + void + safra_determinisation::set_atomic_list(atomic_list_t& list, bdd c) + { + bdd current = bdd_satone(c); + while (current != bddtrue && current != bddfalse) + { + list.insert(bdd_var(current)); + bdd high = bdd_high(current); + if (high == bddfalse) + current = bdd_low(current); + else + current = high; + } + } + + /// From the list of atomic properties \a atomics, create the list + /// of all the conjunctions of properties. + safra_determinisation::conjunction_list_t + safra_determinisation::get_conj_list(const atomic_list_t& atomics) + { + conjunction_list_t list; + unsigned atomics_size = atomics.size(); + + assert(atomics_size < 32); + for (unsigned i = 1; i <= static_cast(1 << atomics_size); ++i) + { + bdd result = bddtrue; + unsigned position = 1; + for (atomic_list_t::const_iterator a_it = atomics.begin(); + a_it != atomics.end(); + ++a_it, position <<= 1) + { + bdd this_atomic; + if (position & i) + this_atomic = bdd_ithvar(*a_it); + else + this_atomic = bdd_nithvar(*a_it); + result = bdd_apply(result, this_atomic, bddop_and); + } + list.insert(result); + } + + return list; + } + + // Safra's test part. Dot output. + ////////////////////////////// + namespace test + { + void print_safra_tree(const safra_tree* this_node, + std::map& node_names, + int& current_node, + int nb_accepting_conditions) + { + std::string conditions; + if (this_node->is_parent()) + { + bitset_t l(nb_accepting_conditions); + bitset_t u(nb_accepting_conditions); + u.flip(); + this_node->getL(l); + this_node->getU(u); + std::stringstream s; + s << "\\nL:" << l << ", U:" << u; + conditions = s.str(); + } + + std::cout << "node" << this_node << "[label=\""; + std::cout << this_node->name << "|"; + for (safra_tree::subset_t::const_iterator j = this_node->nodes.begin(); + j != this_node->nodes.end(); + ++j) + { + if (node_names.find((*j)->hash()) == node_names.end()) + node_names[(*j)->hash()] = current_node++; + std::cout << node_names[(*j)->hash()] << ", "; + } + std::cout << conditions; + if (this_node->marked) + std::cout << "\",style=filled,fillcolor=\"gray"; + + std::cout << "\"];" << std::endl; + + safra_tree::child_list::const_iterator i = this_node->children.begin(); + for (; i != this_node->children.end(); ++i) + { + print_safra_tree(*i, node_names, current_node, + nb_accepting_conditions); + std::cout << "node" << this_node << " -> node" << *i + << "[color=\"red\",arrowhead=\"none\"];" + << std::endl; + } + } + + void print_safra_automaton(safra_tree_automaton* a) + { + safra_tree_automaton::automaton_t node_list = a->automaton; + typedef safra_tree_automaton::automaton_t::const_reverse_iterator + automaton_cit; + typedef safra_tree_automaton::transition_list::const_iterator + trans_cit; + std::map node_names; + int current_node = 0; + int nb_accepting_conditions = a->get_nb_acceptance_pairs(); + + std::cout << "digraph A {" << std::endl; + + for (automaton_cit i = a->automaton.rbegin(); + i != a->automaton.rend(); + ++i) + { + std::cout << "subgraph sg" << i->first << "{" << std::endl; + print_safra_tree(i->first, node_names, current_node, + nb_accepting_conditions); + std::cout << "}" << std::endl; + + // Successors. + for (trans_cit j = i->second.begin(); j != i->second.end(); ++j) + std::cout << "node" << i->first << "->" + << "node" << j->second << + " [label=\"" << bddset << j->first << "\"];" << std::endl; + } + + std::cout << "}" << std::endl; + } + } // test + + //////////////////////////////////////// + // state_complement + + /// States used by spot::tgba_complement. + /// \ingroup tgba_representation + class state_complement : public state + { + public: + state_complement(bitset_t U, bitset_t L, const safra_tree* tree, + bool use_bitset = true); + state_complement(const state_complement& other); + + /// \return the safra tree associated to this state. + const safra_tree* get_safra() const + { + return tree; + } + + /// \return in which sets U this state is included. + bitset_t get_U() const + { + return U; + } + + /// \return in which sets L this state is included. + bitset_t get_L() const + { + return L; + } + + /// \return whether this state track an infinite run. + bool get_use_bitset() const + { + return use_bitset; + } + + virtual int compare(const state* other) const; + virtual size_t hash() const; + virtual state_complement* clone() const; + + virtual ~state_complement() + { + } + + std::string to_string() const; + const state* get_state() const; + private: + bitset_t U; + bitset_t L; + const safra_tree* tree; + bool use_bitset; + }; + + state_complement::state_complement(bitset_t L, bitset_t U, + const safra_tree* tree, + bool use_bitset) + : U(U), L(L), tree(tree), use_bitset(use_bitset) + { + } + + state_complement::state_complement(const state_complement& other) + { + U = other.U; + L = other.L; + tree = other.tree; + use_bitset = other.use_bitset; + } + + int + state_complement::compare(const state* other) const + { + if (other == this) + return 0; + const state_complement* s = dynamic_cast(other); + if (s == 0) + return 1; + if (U != s->U) + return (U < s->U) ? -1 : 1; + if (L != s->L) + return (L < s->L) ? -1 : 1; + if (use_bitset != s->use_bitset) + return use_bitset - s->use_bitset; + return tree->compare(s->tree); + } + + size_t + state_complement::hash() const + { + return 0; // \todo + } + + state_complement* + state_complement::clone() const + { + return new state_complement(*this); + } + + const state* + state_complement::get_state() const + { + return this; + } + + std::string + state_complement::to_string() const + { + std::stringstream ss; + ss << tree; + if (use_bitset) + ss << " - I:" << U << " J:" << L; + return ss.str(); + } + + /// Successor iterators used by spot::tgba_complement. + /// \ingroup tgba_representation + class tgba_complement_succ_iterator: public tgba_succ_iterator + { + public: + typedef std::multimap succ_list_t; + + tgba_complement_succ_iterator(const succ_list_t& list, + bdd the_acceptance_cond) + : list_(list), the_acceptance_cond_(the_acceptance_cond) + { + } + + virtual + ~tgba_complement_succ_iterator() + { + for (succ_list_t::iterator i = list_.begin(); i != list_.end(); ++i) + delete i->second; + } + + virtual void first(); + virtual void next(); + virtual bool done() const; + virtual state_complement* current_state() const; + virtual bdd current_condition() const; + virtual bdd current_acceptance_conditions() const; + private: + succ_list_t list_; + bdd the_acceptance_cond_; + succ_list_t::const_iterator it_; + }; + + void + tgba_complement_succ_iterator::first() + { + it_ = list_.begin(); + } + + void + tgba_complement_succ_iterator::next() + { + ++it_; + } + + bool + tgba_complement_succ_iterator::done() const + { + return it_ == list_.end(); + } + + state_complement* + tgba_complement_succ_iterator::current_state() const + { + assert(!done()); + return new state_complement(*(it_->second)); + } + + bdd + tgba_complement_succ_iterator::current_condition() const + { + assert(!done()); + return it_->first; + } + + bdd + tgba_complement_succ_iterator::current_acceptance_conditions() const + { + assert(!done()); + return the_acceptance_cond_; + } + + } // anonymous + + // safra_tree_automaton + //////////////////////// + + safra_tree_automaton::safra_tree_automaton(const tgba* a) + : max_nb_pairs_(-1), initial_state(0), a_(a) + { + a->get_dict()->register_all_variables_of(a, this); + } + + safra_tree_automaton::~safra_tree_automaton() + { + for (automaton_t::iterator i = automaton.begin(); + i != automaton.end(); + ++i) + { + delete i->first; + } + delete a_; + } + + int + safra_tree_automaton::get_nb_acceptance_pairs() const + { + if (max_nb_pairs_ != -1) + return max_nb_pairs_; + + int max = -1; + for (automaton_t::const_iterator i = automaton.begin(); + i != automaton.end(); + ++i) + max = std::max(max, (*i).first->max_name()); + return max_nb_pairs_ = max + 1; + } + + safra_tree* + safra_tree_automaton::get_initial_state() const + { + return initial_state; + } + + void + safra_tree_automaton::set_initial_state(safra_tree* s) + { + initial_state = s; + } + + // End of the safra construction + ////////////////////////////////////////// + + // tgba_complement + ////////////////////////// + + tgba_complement::tgba_complement(const tgba* a) + : automaton_(a), safra_(safra_determinisation::create_safra_automaton(a)) + { + assert(safra_ || "safra construction fails"); + + // We will use one acceptance condition for this automata. + // Let's call it Acc[True]. + int v = get_dict() + ->register_acceptance_variable(ltl::constant::true_instance(), safra_); + the_acceptance_cond_ = bdd_ithvar(v); + } + + tgba_complement::~tgba_complement() + { + get_dict()->unregister_all_my_variables(safra_); + delete safra_; + } + + state* + tgba_complement::get_init_state() const + { + bitset_t empty(safra_->get_nb_acceptance_pairs()); + return new state_complement(empty, empty, safra_->get_initial_state(), + false); + } + + + /// @brief Compute successors of the state @a local_state, and returns an + /// iterator on the successors collection. + /// + /// This algorithm is a Deterministic Streett to nondeterministic Büchi + /// transformation, presented by Christof Löding in his Diploma thesis. + /// + /// @MastersThesis{ loding.98, + /// author = {Christof L\"oding}, + /// title = {Methods for the Transformation of omega-Automata: + /// Complexity and Connection to Second Order Logic}, + /// school = {University of Kiel}, + /// year = {1998} + /// } + /// + /// @param local_state + /// + tgba_succ_iterator* + tgba_complement::succ_iter(const state* local_state, + const state* /* = 0 */, + const tgba* /* = 0 */) const + { + const state_complement* s = + dynamic_cast(local_state); + assert(s); + safra_tree_automaton::automaton_t::const_iterator tr = + safra_->automaton.find(const_cast(s->get_safra())); + + typedef safra_tree_automaton::transition_list::const_iterator trans_iter; + + if (tr != safra_->automaton.end()) + { + bdd condition = bddfalse; + tgba_complement_succ_iterator::succ_list_t succ_list; + int nb_acceptance_pairs = safra_->get_nb_acceptance_pairs(); + bitset_t e(nb_acceptance_pairs); + + if (!s->get_use_bitset()) // if \delta'(q, a) + { + for (trans_iter i = tr->second.begin(); i != tr->second.end(); ++i) + { + state_complement* s1 = new state_complement(e, e, i->second, false); + state_complement* s2 = new state_complement(e, e, i->second, true); + succ_list.insert(std::make_pair(i->first, s1)); + succ_list.insert(std::make_pair(i->first, s2)); + } + } + else + { + bitset_t l(nb_acceptance_pairs); + bitset_t u(nb_acceptance_pairs); + u.flip(); + s->get_safra()->getL(l); // {i : q \in L_i} + s->get_safra()->getU(u); // {j : q \in U_i} + bitset_t newI = s->get_L() | l; // {I' = I \cup {i : q \in L_i}} + bitset_t newJ = s->get_U() | u; // {J' = J \cup {j : q \in U_i}} + state_complement* st; + + if (newI.is_subset_of(newJ)) // \delta'((q, I, J), a) if I'\subseteq J' + { + for (trans_iter i = tr->second.begin(); i != tr->second.end(); ++i) + { + st = new state_complement(e, e, i->second, true); + succ_list.insert(std::make_pair(i->first, st)); + } + condition = the_acceptance_cond_; + } + else // \delta'((q, I, J), a) + { + for (trans_iter i = tr->second.begin(); i != tr->second.end(); ++i) + { + st = new state_complement(newI, newJ, i->second, true); + succ_list.insert(std::make_pair(i->first, st)); + } + } + } + + return new tgba_complement_succ_iterator(succ_list, condition); + } + assert("Safra automaton do not find this node"); + return 0; + } + + bdd_dict* + tgba_complement::get_dict() const + { + return automaton_->get_dict(); + } + + std::string + tgba_complement::format_state(const state* state) const + { + const state_complement* s = + dynamic_cast(state); + assert(s); + return s->to_string(); + } + + bdd + tgba_complement::all_acceptance_conditions() const + { + return the_acceptance_cond_; + } + + bdd + tgba_complement::neg_acceptance_conditions() const + { + return !the_acceptance_cond_; + } + + bdd + tgba_complement::compute_support_conditions(const state* state) const + { + const state_complement* s = dynamic_cast(state); + assert(s); + typedef safra_tree_automaton::automaton_t::const_iterator auto_it; + typedef safra_tree_automaton::transition_list::const_iterator trans_it; + auto_it node(safra_-> + automaton.find(const_cast(s->get_safra()))); + + if (node == safra_->automaton.end()) + return bddtrue; + + bdd res = bddtrue; + trans_it i; + for (i = node->second.begin(); i != node->second.end(); ++i) + res |= (*i).first; + return res; + } + + bdd + tgba_complement::compute_support_variables(const state* state) const + { + const state_complement* s = dynamic_cast(state); + assert(s); + typedef safra_tree_automaton::automaton_t::const_iterator auto_it; + typedef safra_tree_automaton::transition_list::const_iterator trans_it; + auto_it node(safra_-> + automaton.find(const_cast(s->get_safra()))); + + if (node == safra_->automaton.end()) + return bddtrue; + + bdd res = bddtrue; + trans_it i; + for (i = node->second.begin(); i != node->second.end(); ++i) + res &= bdd_support((*i).first); + return res; + } + + // display_safra: debug routine. + ////////////////////////////// + void display_safra(const tgba_complement* a) + { + test::print_safra_automaton(a->get_safra()); + } +} diff --git a/src/tgba/tgbacomplement.hh b/src/tgba/tgbacomplement.hh new file mode 100644 index 000000000..ae80d69bc --- /dev/null +++ b/src/tgba/tgbacomplement.hh @@ -0,0 +1,68 @@ +#ifndef SPOT_TGBA_TGBACOMPLEMENT_HH +# define SPOT_TGBA_TGBACOMPLEMENT_HH + +# include "tgba/tgba.hh" + +namespace spot +{ + struct safra_tree_automaton; + + /// \brief Build a complemented automaton. + /// \ingroup tgba + /// + /// It creates an automaton that recognizes the + /// negated language of \a aut. + /// + /// 1. First Safra construction algorithm produces a + /// deterministic Rabin automaton. + /// 2. Interpreting this deterministic Rabin automaton as a + /// deterministic Streett will produce a complemented automaton. + /// 3. Then we use a transformation from deterministic Streett + /// automaton to nondeterministic Büchi automaton. + /// + /// Safra construction is done in \a tgba_complement, the transformation + /// is done on-the-fly when successors are called. + /// + /// \sa safra_determinisation, tgba_complement::succ_iter. + class tgba_complement : public tgba + { + public: + tgba_complement(const tgba* a); + virtual ~tgba_complement(); + + safra_tree_automaton* get_safra() const + { + return safra_; + } + + // tgba interface. + virtual state* get_init_state() const; + virtual tgba_succ_iterator* + succ_iter(const state* local_state, + const state* global_state = 0, + const tgba* global_automaton = 0) const; + + virtual bdd_dict* get_dict() const; + virtual std::string format_state(const state* state) const; + virtual bdd all_acceptance_conditions() const; + virtual bdd neg_acceptance_conditions() const; + + protected: + virtual bdd compute_support_conditions(const state* state) const; + virtual bdd compute_support_variables(const state* state) const; + private: + const tgba* automaton_; + safra_tree_automaton* safra_; + bdd the_acceptance_cond_; + }; + + /// \brief Produce a dot output of the Safra automaton associated + /// to \a a. + /// + /// @param a The \c tgba_complement with an intermediate Safra + /// automaton to display + /// + void display_safra(const tgba_complement* a); +} + +#endif // SPOT_TGBA_TGBACOMPLEMENT_HH diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 2acfba1e0..0e8d6dd06 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -1,4 +1,5 @@ -## Copyright (C) 2003, 2004, 2005, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +## Copyright (C) 2003, 2004, 2005, 2008, 2009 Laboratoire +## d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre ## et Marie Curie. ## diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index a2646a9f0..692bed88a 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -31,6 +31,7 @@ check_SCRIPTS = defs # Keep this sorted alphabetically. check_PROGRAMS = \ bddprod \ + complement \ explicit \ expldot \ explprod \ @@ -46,6 +47,7 @@ check_PROGRAMS = \ # Keep this sorted alphabetically. bddprod_SOURCES = ltlprod.cc bddprod_CXXFLAGS = -DBDD_CONCRETE_PRODUCT +complement_SOURCES = complementation.cc eltl2tgba_SOURCES = eltl2tgba.cc explicit_SOURCES = explicit.cc expldot_SOURCES = powerset.cc @@ -88,7 +90,8 @@ TESTS = \ emptchke.test \ dfs.test \ emptchkr.test \ - spotlbtt.test + spotlbtt.test \ + complementation.test EXTRA_DIST = $(TESTS) diff --git a/src/tgbatest/complementation.cc b/src/tgbatest/complementation.cc new file mode 100644 index 000000000..f5895010f --- /dev/null +++ b/src/tgbatest/complementation.cc @@ -0,0 +1,217 @@ +#include +#include +#include "tgbaalgos/dotty.hh" +#include "tgbaparse/public.hh" +#include "tgba/tgbaproduct.hh" +#include "tgbaalgos/gtec/gtec.hh" +#include "tgbaalgos/ltl2tgba_fm.hh" +#include "ltlparse/public.hh" +#include "tgbaalgos/stats.hh" +#include "tgbaalgos/emptiness.hh" +#include "ltlast/unop.hh" +#include "tgbaalgos/stats.hh" +#include "tgbaalgos/emptiness_stats.hh" +#include "ltlvisit/destroy.hh" +#include "ltlvisit/clone.hh" +#include "tgba/tgbatba.hh" + +#include "tgba/tgbacomplement.hh" + +void usage(const char* prog) +{ + std::cout << "usage: " << prog << " [options]" << std::endl; + std::cout << "with options" << std::endl + << "-s buchi_automaton display the safra automaton" + << std::endl + << "-a buchi_automaton display the complemented automaton" + << std::endl + << "-astat buchi_automaton statistics for !a" << std::endl + << "-fstat formula statistics for !A_f" << std::endl + << "-f formula test !A_f and !A_!f" << std::endl; +} + +int main(int argc, char* argv[]) +{ + char *file = 0; + bool print_safra = false; + bool print_automaton = false; + bool check = false; + int return_value = 0; + bool stats = false; + bool formula = false; + bool automaton = false; + + if (argc < 3) + { + usage(argv[0]); + return 1; + } + + for (int i = 1; i < argc; ++i) + { + if (argv[i][0] == '-') + { + if (strcmp(argv[i] + 1, "astat") == 0) + { + stats = true; + automaton = true; + continue; + } + + if (strcmp(argv[i] + 1, "fstat") == 0) + { + stats = true; + formula = true; + continue; + } + + switch (argv[i][1]) + { + case 's': print_safra = true; break; + case 'a': print_automaton = true; break; + case 'f': check = true; break; + default: + std::cerr << "unrecognized option `-" << argv[i][1] + << "'" << std::endl; + return 2; + } + } + else + file = argv[i]; + } + + if (file == 0) + { + usage(argv[0]); + return 1; + } + + spot::bdd_dict* dict = new spot::bdd_dict(); + if (print_automaton || print_safra) + { + spot::ltl::environment& env(spot::ltl::default_environment::instance()); + spot::tgba_parse_error_list pel; + spot::tgba_explicit* a = spot::tgba_parse(file, pel, dict, env); + if (spot::format_tgba_parse_errors(std::cerr, file, pel)) + return 2; + + spot::tgba_complement* complement = new spot::tgba_complement(a); + + if (print_automaton) + spot::dotty_reachable(std::cout, complement); + + if (print_safra) + spot::display_safra(complement); + delete complement; + delete a; + } + else if (stats) + { + spot::tgba* a; + spot::ltl::formula* f1 = 0; + + if (formula) + { + spot::ltl::parse_error_list p1; + f1 = spot::ltl::parse(file, p1); + + if (spot::ltl::format_parse_errors(std::cerr, file, p1)) + return 2; + + a = spot::ltl_to_tgba_fm(f1, dict); + } + else + { + spot::tgba_parse_error_list pel; + spot::ltl::environment& env(spot::ltl::default_environment::instance()); + a = spot::tgba_parse(file, pel, dict, env); + if (spot::format_tgba_parse_errors(std::cerr, file, pel)) + return 2; + } + + spot::tgba_complement* complement = new spot::tgba_complement(a); + + spot::tgba_statistics a_size = spot::stats_reachable(a); + std::cout << "Original: " + << a_size.states << ", " + << a_size.transitions << std::endl; + + spot::tgba *buchi = new spot::tgba_sba_proxy(a); + a_size = spot::stats_reachable(buchi); + std::cout << "Buchi: " + << a_size.states << ", " + << a_size.transitions << std::endl; + delete buchi; + + spot::tgba_statistics b_size = spot::stats_reachable(complement); + std::cout << "Complement: " + << b_size.states << ", " + << b_size.transitions << std::endl; + + delete complement; + delete a; + if (formula) + { + spot::ltl::formula* nf1 = + spot::ltl::unop::instance(spot::ltl::unop::Not, + spot::ltl::clone(f1)); + spot::tgba* a2 = spot::ltl_to_tgba_fm(nf1, dict); + spot::tgba_statistics a_size = spot::stats_reachable(a2); + std::cout << "Not Formula: " + << a_size.states << ", " + << a_size.transitions << std::endl; + + delete a2; + spot::ltl::destroy(f1); + spot::ltl::destroy(nf1); + } + } + else + { + spot::ltl::parse_error_list p1; + spot::ltl::formula* f1 = spot::ltl::parse(file, p1); + + if (spot::ltl::format_parse_errors(std::cerr, file, p1)) + return 2; + + spot::tgba* Af = spot::ltl_to_tgba_fm(f1, dict); + spot::ltl::formula* nf1 = spot::ltl::unop::instance(spot::ltl::unop::Not, + spot::ltl::clone(f1)); + spot::tgba* Anf = spot::ltl_to_tgba_fm(nf1, dict); + spot::tgba_complement* nAf = new spot::tgba_complement(Af); + spot::tgba_complement* nAnf = new spot::tgba_complement(Anf); + spot::tgba* prod = new spot::tgba_product(nAf, nAnf); + spot::emptiness_check* ec = spot::couvreur99(prod); + spot::emptiness_check_result* res = ec->check(); + spot::tgba_statistics a_size = spot::stats_reachable(ec->automaton()); + std::cout << std::right << std::setw(10) + << a_size.states << ", " + << std::right << std::setw(10) + << a_size.transitions << ", " + << ec->automaton()->number_of_acceptance_conditions(); + if (res) + { + std::cout << ", FAIL"; + return_value = 1; + } + else + std::cout << ", OK"; + std::cout << std::endl; + + delete res; + delete ec; + delete prod; + delete nAf; + delete Af; + delete nAnf; + delete Anf; + + spot::ltl::destroy(nf1); + spot::ltl::destroy(f1); + + } + + delete dict; + + return return_value; +} diff --git a/src/tgbatest/complementation.test b/src/tgbatest/complementation.test new file mode 100755 index 000000000..bd42f2e79 --- /dev/null +++ b/src/tgbatest/complementation.test @@ -0,0 +1,31 @@ +#!/bin/sh +# Copyright (C) 2009 Laboratoire d'Informatique de Paris 6 (LIP6), +# département Systèmes Répartis Coopératifs (SRC), Université Pierre +# et Marie Curie. +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 2 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with Spot; see the file COPYING. If not, write to the Free +# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +# 02111-1307, USA. + +. ./defs + +set -e + +FORMULAE='GFa FGa <>p1->(p0Up1) [](p0-><>p3) GFa&&FGa' + +for f in $FORMULAE; do + run 0 ./complement -f "$f" +done