diff --git a/lbtt/src/BuchiProduct.cc b/lbtt/src/BuchiProduct.cc new file mode 100644 index 000000000..c5f5c51d5 --- /dev/null +++ b/lbtt/src/BuchiProduct.cc @@ -0,0 +1,98 @@ +/* + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 + * Heikki Tauriainen + * + * This program 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. + * + * This program 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 this program; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. + */ + +#include "BuchiProduct.h" + +namespace Graph +{ + +/****************************************************************************** + * + * Static member definitions for class BuchiProduct. + * + *****************************************************************************/ + +map< ::Ltl::LtlFormula*, BuchiProduct::SatisfiabilityMapping, + less< ::Ltl::LtlFormula*>, ALLOC(BuchiProduct::SatisfiabilityMapping) > + BuchiProduct::sat_cache; + + + +/****************************************************************************** + * + * Function definitions for class BuchiProduct. + * + *****************************************************************************/ + +/* ========================================================================= */ +bool BuchiProduct::synchronizable + (const Graph::Edge& transition_1, + const Graph::Edge& transition_2) +/* ---------------------------------------------------------------------------- + * + * Description: Tests whether two transitions of two Büchi automata are + * synchronizable by checking whether the conjunction of their + * guard formulas is satisfiable. + * + * Arguments: transition_1, -- Constant references to the transitions. + * transition_2 + * + * Returns: true iff the transitions are synchronizable. The result is + * also stored into `this->sat_cache' for later reference. + * + * ------------------------------------------------------------------------- */ +{ + using ::Ltl::LtlFormula; + using ::Ltl::And; + + LtlFormula* guard_1 = &static_cast + (transition_1).guard(); + LtlFormula* guard_2 = &static_cast + (transition_2).guard(); + + if (guard_2 > guard_1) + { + LtlFormula* swap_guard = guard_2; + guard_2 = guard_1; + guard_1 = swap_guard; + } + + map, + ALLOC(SatisfiabilityMapping) >::iterator + sat_cache_element = sat_cache.find(guard_1); + + if (sat_cache_element == sat_cache.end()) + sat_cache_element = sat_cache.insert + (make_pair(guard_1, SatisfiabilityMapping())).first; + else + { + SatisfiabilityMapping::const_iterator sat_result + = sat_cache_element->second.find(guard_2); + if (sat_result != sat_cache_element->second.end()) + return sat_result->second; + } + + LtlFormula* f = &And::construct(*guard_1, *guard_2); + const bool result = f->satisfiable(); + LtlFormula::destruct(f); + sat_cache_element->second.insert(make_pair(guard_2, result)); + return result; +} + +} diff --git a/lbtt/src/BuchiProduct.h b/lbtt/src/BuchiProduct.h new file mode 100644 index 000000000..43200f521 --- /dev/null +++ b/lbtt/src/BuchiProduct.h @@ -0,0 +1,512 @@ +/* + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 + * Heikki Tauriainen + * + * This program 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. + * + * This program 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 this program; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. + */ + +#ifndef BUCHIPRODUCT_H +#define BUCHIPRODUCT_H + +#include +#include +#include +#include +#include +#include +#include "BitArray.h" +#include "BuchiAutomaton.h" +#include "EdgeContainer.h" +#include "Graph.h" +#include "LtlFormula.h" + +using namespace std; + +namespace Graph +{ + +/****************************************************************************** + * + * A class with operations for checking the intersection of two Büchi automata + * (represented as two BuchiAutomaton objects) for emptiness. + * + *****************************************************************************/ + +class BuchiProduct +{ +public: + BuchiProduct /* Constructor. */ + (const Graph& a1, + const Graph& a2); + + /* default copy constructor */ + + ~BuchiProduct(); /* Destructor. */ + + /* default assignment operator */ + + bool empty() const; /* Tells whether the + * intersection of the + * Büchi automata + * associated with the + * product object is + * (trivially) empty. + */ + + unsigned long int numberOfAcceptanceSets() const; /* Tells the number of + * acceptance sets in the + * intersection of the + * automata associated with + * the object. + */ + + const BuchiAutomaton::BuchiState& firstComponent /* Mappings between an */ + (const Graph::size_type /* intersection state */ + state_id) const; /* identifier and states */ + const BuchiAutomaton::BuchiState& secondComponent /* of the underlying */ + (const Graph::size_type /* automata. */ + state_id) const; + + void mergeAcceptanceInformation /* Merges the acceptance */ + (const Graph::Node& state1, /* sets associated with */ + const Graph::Node& state2, /* a pair of states into */ + BitArray& acceptance_sets) const; /* a collection of sets. */ + + void mergeAcceptanceInformation /* Merges the acceptance */ + (const Graph::Edge& /* sets associated with */ + transition1, /* a pair of */ + const Graph::Edge& /* transitions into a */ + transition2, /* collection of sets. */ + BitArray& acceptance_sets) const; + + void validateEdgeIterators /* Ensures that a pair */ + (const Graph::Node& /* of transition */ + state_1, /* iterators points to a */ + const Graph::Node& /* transition beginning */ + state_2, /* from a given state in */ + GraphEdgeContainer::const_iterator& /* the intersection of */ + transition_1, /* two Büchi automata. */ + GraphEdgeContainer::const_iterator& + transition_2); + + void incrementEdgeIterators /* Updates a pair of */ + (const Graph::Node& /* transition iterators */ + state_1, /* to make them point to */ + const Graph::Node& /* the "next" transition */ + state_2, /* starting from a given */ + GraphEdgeContainer::const_iterator& /* state in the */ + transition_1, /* intersection of two */ + GraphEdgeContainer::const_iterator& /* Büchi automata. */ + transition_2); + + static void clearSatisfiabilityCache(); /* Clears information about + * the satisfiability of + * the guards of product + * transitions. + */ +private: + void mergeAcceptanceInformation /* Bitwise or between */ + (const BitArray& sets1, const BitArray& sets2, /* two "component" */ + BitArray& result) const; /* acceptance set + * vectors and a result + * vector. + */ + + + + bool synchronizable /* Tests whether a pair */ + (const Graph::Edge& /* of transitions of two */ + transition_1, /* Büchi automata is */ + const Graph::Edge& /* synchronizable. */ + transition_2); + + const BuchiAutomaton& automaton_1; /* Automata associated */ + const BuchiAutomaton& automaton_2; /* with the BuchiProduct */ + /* object. */ + + const unsigned long int /* Number of acceptance */ + number_of_acceptance_sets; /* sets in the + * intersection of the + * automata. + */ + + typedef map< ::Ltl::LtlFormula*, bool, /* Type definition for */ + less< ::Ltl::LtlFormula*>, /* storing information */ + ALLOC(bool) > /* about the */ + SatisfiabilityMapping; /* satisfiability of the + * guards of product + * transitions. + */ + + static map< ::Ltl::LtlFormula*, /* Result cache for */ + SatisfiabilityMapping, /* satisfiability tests. */ + less< ::Ltl::LtlFormula*>, + ALLOC(SatisfiabilityMapping) > + sat_cache; +}; + + + +/****************************************************************************** + * + * Inline function definitions for class BuchiProduct. + * + *****************************************************************************/ + +/* ========================================================================= */ +inline BuchiProduct::BuchiProduct + (const Graph& a1, const Graph& a2) : + automaton_1(static_cast(a1)), + automaton_2(static_cast(a2)), + number_of_acceptance_sets(static_cast(a1) + .numberOfAcceptanceSets() + + static_cast(a2) + .numberOfAcceptanceSets()) +/* ---------------------------------------------------------------------------- + * + * Description: Constructor for class BuchiProduct. Initializes a new object + * with operations for checking the emptiness of two Büchi + * automata. + * + * Arguments: a1, a2 -- Constant references to two + * Graph objects, assumed to be + * BüchiAutomaton objects to which to apply the + * operations. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +inline BuchiProduct::~BuchiProduct() +/* ---------------------------------------------------------------------------- + * + * Description: Destructor for class BuchiProduct. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +inline bool BuchiProduct::empty() const +/* ---------------------------------------------------------------------------- + * + * Description: Tells whether the intersection of the Büchi automata + * associated with a BuchiProduct object is (trivially) empty. + * + * Arguments: None. + * + * Returns: true iff either of the automata associated with the + * BuchiProduct object is (trivially) empty (i.e., whether + * either of the automata has no states). + * + * ------------------------------------------------------------------------- */ +{ + return (automaton_1.empty() || automaton_2.empty()); +} + + +/* ========================================================================= */ +inline unsigned long int BuchiProduct::numberOfAcceptanceSets() const +/* ---------------------------------------------------------------------------- + * + * Description: Tells the number of acceptance sets in the intersection of + * the two Büchi automata associated with a BuchiProduct object. + * + * Arguments: None. + * + * Returns: The number of acceptance sets in the intersection. + * + * ------------------------------------------------------------------------- */ +{ + return number_of_acceptance_sets; +} + +/* ========================================================================= */ +inline const BuchiAutomaton::BuchiState& BuchiProduct::firstComponent + (const Graph::size_type state_id) const +/* ---------------------------------------------------------------------------- + * + * Description: Function for accessing states of the "first" component + * automaton in the intersection of two Büchi automata. + * + * Argument: state_id -- Identifier of a state in the component + * automaton. + * + * Returns: A constant reference to a state in the component automaton. + * + * ------------------------------------------------------------------------- */ +{ + return automaton_1[state_id]; +} + +/* ========================================================================= */ +inline const BuchiAutomaton::BuchiState& BuchiProduct::secondComponent + (const Graph::size_type state_id) const +/* ---------------------------------------------------------------------------- + * + * Description: Function for accessing states of the "second" component + * automaton in the intersection of two Büchi automata. + * + * Argument: state_id -- Identifier of a state in the component + * automaton. + * + * Returns: A constant reference to a state in the component automaton. + * + * ------------------------------------------------------------------------- */ +{ + return automaton_2[state_id]; +} + +/* ========================================================================= */ +inline void BuchiProduct::mergeAcceptanceInformation + (const Graph::Node& state1, + const Graph::Node& state2, + BitArray& acceptance_sets) const +/* ---------------------------------------------------------------------------- + * + * Description: Merges the acceptance sets associated with a pair of states + * of two Büchi automata into a collection of sets. + * + * Arguments: state1, state2 -- Constant references to the states of the + * automata. + * acceptance_sets -- A reference to a BitArray for storing + * the result. The BitArray is assumed to + * have capacity for + * `this->number_of_acceptance_sets' bits. + * + * Returns: Nothing. Let n=`this->automaton_1.numberOfAcceptanceSets()'; + * after the operation, `acceptance_sets[i] = true' holds if + * either + * 0 <= i < n and + * `state1.acceptanceSets().test(i) == true' + * or 0 <= i - n < `this->automaton_2.numberOfAcceptanceSets()' + * and `state2.acceptanceSets().test(i - n) == true'. + * + * ------------------------------------------------------------------------- */ +{ + mergeAcceptanceInformation + (static_cast(state1).acceptanceSets(), + static_cast(state2).acceptanceSets(), + acceptance_sets); +} + +/* ========================================================================= */ +inline void BuchiProduct::mergeAcceptanceInformation + (const Graph::Edge& transition1, + const Graph::Edge& transition2, + BitArray& acceptance_sets) const +/* ---------------------------------------------------------------------------- + * + * Description: Merges the acceptance sets associated with a pair of + * transitions of two Büchi automata into a collection of + * acceptance sets. + * + * Arguments: transition1, -- Constant references to the transitions + * transition2 of the automata. + * acceptance_sets -- A reference to a BitArray for storing + * the result. The BitArray is assumed to + * have capacity for + * `this->number_of_acceptance_sets' bits. + * + * Returns: Nothing. Let n=`this->automaton_1.numberOfAcceptanceSets()'; + * after the operation, `acceptance_sets[i] = true' holds if + * either + * 0 <= i < n and + * `transition1.acceptanceSets().test(i) == true' + * or 0 <= i - n < `this->automaton_2.numberOfAcceptanceSets()' + * and `transition2.acceptanceSets().test(i - n) == true'. + * + * ------------------------------------------------------------------------- */ +{ + mergeAcceptanceInformation + (static_cast(transition1) + .acceptanceSets(), + static_cast(transition2) + .acceptanceSets(), + acceptance_sets); +} + +/* ========================================================================= */ +inline void BuchiProduct::mergeAcceptanceInformation + (const BitArray& sets1, const BitArray& sets2, BitArray& result) const +/* ---------------------------------------------------------------------------- + * + * Description: Bitwise or between two acceptance set vectors and a result + * vector. + * + * Arguments: sets1, -- Constant references to two BitArrays having (at + * sets2 least) capacities + * `automaton_1.numberOfAcceptanceSets()' and + * `automaton_2.numberOfAcceptanceSets()', + * respectively. + * result -- A BitArray for storing the result, assumed to + * have room for at least + * `this->number_of_acceptance_sets' bits. + * + * Returns: Nothing. Let n=`this->automaton_1.numberOfAcceptanceSets()'; + * after the operation, `result[i] = true' holds if + * either + * 0 <= i < n and `sets1[i] == true' + * or 0 <= i - n < `this->automaton_2.numberOfAcceptanceSets()' + * and `sets2[i - n] == true'. + * + * ------------------------------------------------------------------------- */ +{ + const unsigned long int shift + = automaton_1.numberOfAcceptanceSets(); + unsigned long int acceptance_set; + for (acceptance_set = 0; acceptance_set < shift; ++acceptance_set) + { + if (sets1[acceptance_set]) + result.setBit(acceptance_set); + } + for ( ; acceptance_set < number_of_acceptance_sets; ++acceptance_set) + { + if (sets2[acceptance_set - shift]) + result.setBit(acceptance_set); + } +} + +/* ========================================================================= */ +inline void BuchiProduct::validateEdgeIterators + (const Graph::Node& state_1, + const Graph::Node& state_2, + GraphEdgeContainer::const_iterator& transition_1, + GraphEdgeContainer::const_iterator& transition_2) +/* ---------------------------------------------------------------------------- + * + * Description: Checks whether a pair of transition iterators corresponds to + * a transition beginning from a state in the intersection of + * two Büchi automata; if this is not the case, increments the + * iterators to make them point to a valid transition beginning + * from the state in the intersection (or to the "end" of the + * collection of transitions beginning from the state if no + * valid transition can be found by incrementing the iterators). + * + * Arguments: state_1, -- These variables determine the state in + * state_2 the intersection automaton; `state_1' and + * `state_2' should both be references to + * BuchiAutomaton::BuchiState objects. + * transition_1, -- References to the transition iterators. + * transition_2 Initially, `transition_1' and + * `transition_2' should point to two + * transitions starting from `state_1' and + * `state_2', respectively. + * + * Returns: Nothing. Upon return, `transition_1' and `transition_2' will + * either equal `state_1.edges().end()' and + * `state_2.edges().end()', respectively, or they will point to + * a pair of transitions beginning from `state_1' and `state_2' + * such that this pair of transitions corresponds to a + * transition starting from the intersection state determined by + * `state_1' and `state_2'. + * + * ------------------------------------------------------------------------- */ +{ + const GraphEdgeContainer& transitions_1 = state_1.edges(); + const GraphEdgeContainer& transitions_2 = state_2.edges(); + + if (transition_1 == transitions_1.end()) + { + transition_2 = transitions_2.end(); + return; + } + if (transition_2 == transitions_2.end()) + { + transition_1 = transitions_1.end(); + return; + } + + if (!synchronizable(**transition_1, **transition_2)) + incrementEdgeIterators(state_1, state_2, transition_1, transition_2); +} + +/* ========================================================================= */ +inline void BuchiProduct::incrementEdgeIterators + (const Graph::Node& state_1, + const Graph::Node& state_2, + GraphEdgeContainer::const_iterator& transition_1, + GraphEdgeContainer::const_iterator& transition_2) +/* ---------------------------------------------------------------------------- + * + * Description: Increments a pair of transition iterators to point to the + * "next" transition beginning from a state in the intersection + * of two Büchi automata. If no "next" transition exists, makes + * the iterators point to the "end" of the collection of + * transitions beginning from the state. + * + * Arguments: state_1, -- These variables determine the state in + * state_2 the intersection automaton; `state_1' and + * `state_2' should both be references to + * BuchiAutomaton::BuchiState objects. + * transition_1, -- References to the transition iterators. + * transition_2 Initially, `transition_1' and + * `transition_2' should point to two + * transitions starting from `state_1' and + * `state_2', respectively. + * + * Returns: Nothing. Upon return, `transition_1' and `transition_2' will + * either equal `state_1.edges().end()' and + * `state_2.edges().end()', respectively, or they will point to + * a pair of transitions beginning from `state_1' and `state_2' + * such that this pair of transitions corresponds to a + * transition starting from the intersection state determined by + * `state_1' and `state_2'. + * + * ------------------------------------------------------------------------- */ +{ + const GraphEdgeContainer& transitions_1 = state_1.edges(); + const GraphEdgeContainer& transitions_2 = state_2.edges(); + + do + { + ++transition_2; + if (transition_2 == transitions_2.end()) + { + ++transition_1; + if (transition_1 == transitions_1.end()) + return; + transition_2 = transitions_2.begin(); + } + } + while (!synchronizable(**transition_1, **transition_2)); +} + +/* ========================================================================= */ +inline void BuchiProduct::clearSatisfiabilityCache() +/* ---------------------------------------------------------------------------- + * + * Description: Clears information about the satisfiability of the guard + * formulas of product transitions. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ + sat_cache.clear(); +} + +} + +#endif /* !BUCHIPRODUCT_H */ diff --git a/lbtt/src/IntervalList.cc b/lbtt/src/IntervalList.cc new file mode 100644 index 000000000..52a5ebb35 --- /dev/null +++ b/lbtt/src/IntervalList.cc @@ -0,0 +1,187 @@ +/* + * Copyright (C) 2004 + * Heikki Tauriainen + * + * This program 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. + * + * This program 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 this program; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. + */ + +#include "IntervalList.h" +#include "StringUtil.h" + +/****************************************************************************** + * + * Function definitions for class IntervalList. + * + *****************************************************************************/ + +/* ========================================================================= */ +void IntervalList::merge(unsigned long int min, unsigned long int max) +/* ---------------------------------------------------------------------------- + * + * Description: Merges a new interval with a list of intervals. + * + * Arguments: min, max -- Upper and lower bound of the new interval. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ + if (min > max) + return; + + list::iterator interval; + for (interval = intervals.begin(); + interval != intervals.end() && interval->second + 1 < min; + ++interval) + ; + + if (interval == intervals.end()) + { + intervals.insert(interval, make_pair(min, max)); + return; + } + + if (interval->first <= min && max <= interval->second) + return; + + if (max + 1 < interval->first) + { + intervals.insert(interval, make_pair(min, max)); + return; + } + + if (min < interval->first) + interval->first = min; + + if (interval->second < max) + { + interval->second = max; + list::iterator interval2 = interval; + ++interval2; + while (interval2 != intervals.end() + && interval2->first <= interval->second + 1) + { + if (interval->second < interval2->second) + interval->second = interval2->second; + list::iterator interval_to_erase = interval2; + ++interval2; + intervals.erase(interval_to_erase); + } + } +} + +/* ========================================================================= */ +void IntervalList::remove(unsigned long int min, unsigned long int max) +/* ---------------------------------------------------------------------------- + * + * Description: Removes a closed interval from an interval list. + * + * Arguments: min, max -- Bounds for the interval to remove. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ + if (min > max) + return; + + list::iterator interval; + for (interval = intervals.begin(); + interval != intervals.end() && interval->second < min; + ++interval) + ; + + while (interval != intervals.end()) + { + if (max < interval->first) /* min <= max < imin <= imax */ + return; + + if (interval->first < min) + { + if (max < interval->second) /* imin < min <= max < imax */ + { + intervals.insert(interval, make_pair(interval->first, min - 1)); + interval->first = max + 1; + return; + } + interval->second = min - 1; /* imin < min <= imax <= max */ + ++interval; + } + else if (max < interval->second) /* min <= imin <= max < imax */ + { + interval->first = max + 1; + return; + } + else /* min <= imin <= imax <= max */ + { + list::iterator interval_to_erase = interval; + ++interval; + intervals.erase(interval_to_erase); + } + } +} + +/* ========================================================================= */ +bool IntervalList::covers(unsigned long int min, unsigned long int max) const +/* ---------------------------------------------------------------------------- + * + * Description: Test whether an interval list covers a given interval. + * + * Arguments: min, max -- Upper and lower bound for the interval to test. + * + * Returns: True if the IntervalList covers the given interval. + * + * ------------------------------------------------------------------------- */ +{ + if (min > max) + return true; /* empty interval is always covered */ + + list::const_iterator interval; + for (interval = intervals.begin(); + interval != intervals.end() && min > interval->second; + ++interval) + ; + + if (interval == intervals.end()) + return false; + + return (min >= interval->first && max <= interval->second); +} + +/* ========================================================================= */ +string IntervalList::toString() const +/* ---------------------------------------------------------------------------- + * + * Description: Converts the interval list to a string. + * + * Arguments: None. + * + * Returns: A string listing the intervals in the interval list. + * + * ------------------------------------------------------------------------- */ +{ + string s; + for (list::const_iterator + interval = intervals.begin(); + interval != intervals.end(); + ++interval) + { + if (interval != intervals.begin()) + s += ','; + s += StringUtil::toString(interval->first) + "..." + + StringUtil::toString(interval->second); + } + return s; +} diff --git a/lbtt/src/IntervalList.h b/lbtt/src/IntervalList.h new file mode 100644 index 000000000..2a55b9641 --- /dev/null +++ b/lbtt/src/IntervalList.h @@ -0,0 +1,499 @@ +/* + * Copyright (C) 2004 + * Heikki Tauriainen + * + * This program 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. + * + * This program 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 this program; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. + */ + +#ifndef INTERVALLIST_H +#define INTERVALLIST_H + +#include +#include +#include +#include +#include "LbttAlloc.h" + +using namespace std; + +/****************************************************************************** + * + * The IntervalList class represents a list of disjoint closed intervals + * formed from pairs of unsigned long integers. The class supports merging + * a new interval with a list of intervals, removing an interval from a list + * of intervals and checking whether the interval list covers a given element + * (or a given interval). The elements of the intervals can also be accessed + * in increasing order via IntervalList::const_iterator. + * + *****************************************************************************/ + +class IntervalList +{ +private: + typedef pair + Interval; + +public: + /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ + + class const_iterator /* A class for iterating */ + { /* over the elements of */ + /* an IntervalList. */ + public: + const_iterator(); /* Constructor. */ + + /* default copy constructor */ + + ~const_iterator(); /* Destructor. */ + + /* default assignment operator */ + + bool operator==(const const_iterator& it) /* Comparison operators. */ + const; + + bool operator!=(const const_iterator& it) + const; + + unsigned long int operator*() const; /* Dereference operator. */ + + unsigned long int operator++(); /* Prefix increment. */ + + unsigned long int operator++(int); /* Postfix increment. */ + + private: + const list* /* The interval list */ + interval_list; /* associated with the */ + /* iterator. */ + + list /* An iterator pointing */ + ::const_iterator interval; /* at the current */ + /* interval list. */ + + unsigned long int element; /* Element currently + * pointed to by the + * iterator. + */ + + friend class IntervalList; + }; + + /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ + + IntervalList(); /* Constructor. */ + + ~IntervalList(); /* Destructor. */ + + /* default copy constructor */ + + /* default assignment operator */ + + void merge(unsigned long int element); /* Merges a point interval + * with the list of + * intervals. + */ + + void merge /* Merges a new interval */ + (unsigned long int min, unsigned long int max); /* with the list of + * intervals. + */ + + void remove(unsigned long int element); /* Removes an element from + * the list of intervals. + */ + + void remove /* Removes an interval */ + (unsigned long int min, unsigned long int max); /* from the list of + * intervals. + */ + + bool covers(unsigned long int element) const; /* Tests whether the + * interval list covers an + * element. + */ + + bool covers /* Tests whether the */ + (unsigned long int min, unsigned long int max) /* interval list covers */ + const; /* an interval. */ + + const_iterator begin() const; /* Returns an iterator to + * the beginning of the + * interval list. + */ + + const_iterator end() const; /* Returns an iterator to + * the end of the interval + * list. + */ + + typedef const_iterator iterator; /* The interval list + * cannot be modified with + * iterators. + */ + + typedef list /* Size type. */ + ::size_type size_type; + + size_type size() const; /* Tell the number of + * disjoint intervals in + * the interval list. + */ + + size_type max_size() const; /* Tell the maximum + * allowable number of + * disjoint intervals in + * the interval list. + */ + + bool empty() const; /* Tell whether the + * interval list is empty. + */ + + void clear(); /* Makes the interval list + * empty. + */ + + string toString() const; /* Converts the interval + * list to a string. + */ + +private: + list intervals; /* List of intervals. */ + + friend class const_iterator; +}; + + + +/****************************************************************************** + * + * Inline function definitions for class IntervalList. + * + *****************************************************************************/ + +/* ========================================================================= */ +inline IntervalList::IntervalList() +/* ---------------------------------------------------------------------------- + * + * Description: Constructor for class IntervalList. Creates an empty list of + * intervals. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +inline IntervalList::~IntervalList() +/* ---------------------------------------------------------------------------- + * + * Description: Destructor for class IntervalList. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +inline void IntervalList::merge(unsigned long int element) +/* ---------------------------------------------------------------------------- + * + * Description: Merges an element (a point interval) with an IntervalList. + * + * Arguments: element -- Element to merge. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ + merge(element, element); +} + +/* ========================================================================= */ +inline bool IntervalList::covers(unsigned long int element) const +/* ---------------------------------------------------------------------------- + * + * Description: Tests whether an interval list covers an element. + * + * Arguments: element -- Element to test. + * + * Returns: True if the IntervalList covers the element. + * + * ------------------------------------------------------------------------- */ +{ + return covers(element, element); +} + +/* ========================================================================= */ +inline IntervalList::size_type IntervalList::size() const +/* ---------------------------------------------------------------------------- + * + * Description: Tells the number of disjoint intervals in an IntervalList. + * + * Arguments: None. + * + * Returns: Number of disjoint intervals in the IntervalList. + * + * ------------------------------------------------------------------------- */ +{ + return intervals.size(); +} + +/* ========================================================================= */ +inline IntervalList::size_type IntervalList::max_size() const +/* ---------------------------------------------------------------------------- + * + * Description: Tells the maximum allowable number of disjoint intervals in + * an IntervalList. + * + * Arguments: None. + * + * Returns: Maximum allowable number of disjoint intervals in the + * IntervalList. + * + * ------------------------------------------------------------------------- */ +{ + return intervals.max_size(); +} + +/* ========================================================================= */ +inline bool IntervalList::empty() const +/* ---------------------------------------------------------------------------- + * + * Description: Tells whether an IntervalList is empty. + * + * Arguments: None. + * + * Returns: True if the IntervalList is empty. + * + * ------------------------------------------------------------------------- */ +{ + return intervals.empty(); +} + +/* ========================================================================= */ +inline void IntervalList::clear() +/* ---------------------------------------------------------------------------- + * + * Description: Makes an IntervalList empty. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ + intervals.clear(); +} + +/* ========================================================================= */ +inline IntervalList::const_iterator IntervalList::begin() const +/* ---------------------------------------------------------------------------- + * + * Description: Returns an IntervalList::const_iterator pointing to the + * beginning of an IntervalList. + * + * Arguments: None. + * + * Returns: An IntervalList::const_iterator pointing to the beginning of + * the IntervalList. + * + * ------------------------------------------------------------------------- */ +{ + const_iterator it; + it.interval_list = &this->intervals; + it.interval = intervals.begin(); + if (it.interval != intervals.end()) + it.element = it.interval->first; + else + it.element = 0; + return it; +} + +/* ========================================================================= */ +inline IntervalList::const_iterator IntervalList::end() const +/* ---------------------------------------------------------------------------- + * + * Description: Returns an IntervalList::const_iterator pointing to the end + * of an IntervalList. + * + * Arguments: None. + * + * Returns: An IntervalList::const_iterator pointing to the end of the + * IntervalList. + * + * ------------------------------------------------------------------------- */ +{ + const_iterator it; + it.interval_list = &this->intervals; + it.interval = intervals.end(); + it.element = 0; + return it; +} + + + +/****************************************************************************** + * + * Inline function definitions for class IntervalList::const_iterator. + * + *****************************************************************************/ + +/* ========================================================================= */ +inline IntervalList::const_iterator::const_iterator() +/* ---------------------------------------------------------------------------- + * + * Description: Constructor for class IntervalList::const_iterator. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +inline IntervalList::const_iterator::~const_iterator() +/* ---------------------------------------------------------------------------- + * + * Description: Destructor for class IntervalList::const_iterator. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +inline bool IntervalList::const_iterator::operator== + (const const_iterator& it) const +/* ---------------------------------------------------------------------------- + * + * Description: Equality test for two IntervalList::const_iterators. Two + * IntervalList::const_iterators are equal if and only if they + * point to the same interval of an interval list and the same + * element in the interval. + * + * Argument: it -- A constant reference to another + * IntervalList::const_iterator. + * + * Returns: Result of the equality test (a truth value). + * + * ------------------------------------------------------------------------- */ +{ + return (interval_list == it.interval_list && interval == it.interval + && element == it.element); +} + +/* ========================================================================= */ +inline bool IntervalList::const_iterator::operator!= + (const const_iterator& it) const +/* ---------------------------------------------------------------------------- + * + * Description: Inequality test for two IntervalList::const_iterators. Two + * IntervalList::const_iterators are not equal if and only if + * they point to different intervals of an interval list or to + * different elements of the same interval in the list. + * + * Argument: it -- A constant reference to another + * IntervalList::const_iterator. + * + * Returns: Result of the inequality test (a truth value). + * + * ------------------------------------------------------------------------- */ +{ + return (interval_list != it.interval_list || interval != it.interval + || element != it.element); +} + +/* ========================================================================= */ +inline unsigned long int IntervalList::const_iterator::operator*() const +/* ---------------------------------------------------------------------------- + * + * Description: Dereferencing operator for IntervalList::const_iterator. + * + * Arguments: None. + * + * Returns: The element currently pointed to by the iterator. + * + * ------------------------------------------------------------------------- */ +{ + return element; +} + +/* ========================================================================= */ +inline unsigned long int IntervalList::const_iterator::operator++() +/* ---------------------------------------------------------------------------- + * + * Description: Prefix increment operator for IntervalList::const_iterator. + * + * Arguments: None. + * + * Returns: The element following the "current" element in the interval + * list. + * + * ------------------------------------------------------------------------- */ +{ + if (element == interval->second) + { + ++interval; + if (interval != interval_list->end()) + element = interval->first; + else + element = 0; + } + else + ++element; + + return element; +} + +/* ========================================================================= */ +inline unsigned long int IntervalList::const_iterator::operator++(int) +/* ---------------------------------------------------------------------------- + * + * Description: Postfix increment operator for IntervalList::const_iterator. + * + * Arguments: None. + * + * Returns: The "current" element in the interval list. + * + * ------------------------------------------------------------------------- */ +{ + unsigned long int current_element = element; + if (element == interval->second) + { + ++interval; + if (interval != interval_list->end()) + element = interval->first; + else + element = 0; + } + else + ++element; + + return current_element; +} + +#endif /* INTERVALLIST_H */ diff --git a/lbtt/src/Ltl-parse.yy b/lbtt/src/Ltl-parse.yy new file mode 100644 index 000000000..d558db0b7 --- /dev/null +++ b/lbtt/src/Ltl-parse.yy @@ -0,0 +1,610 @@ +/* + * Copyright (C) 2004 + * Heikki Tauriainen + * + * This program 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. + * + * This program 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 this program; 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 "Exception.h" +#include "LbttAlloc.h" +#include "LtlFormula.h" + +using namespace Ltl; + +/****************************************************************************** + * + * Variables and functions used for parsing an LTL formula. + * + *****************************************************************************/ + +static Exceptional_istream* estream; /* Pointer to input stream. + */ + +static LtlFormula* result; /* This variable stores the + * result after a call to + * ltl_parse. + */ + +static std::set, /* Intermediate results. */ + ALLOC(LtlFormula*) > /* (This set is used */ + intermediate_results; /* for keeping track of + * the subformulas of a + * partially constructed + * formula in case the + * memory allocated for + * the subformulas needs + * to be freed because + * of a parse error.) + */ + +static int ltl_lex(); /* The lexical scanner. */ + + + +/****************************************************************************** + * + * Function for reporting parse errors. + * + *****************************************************************************/ + +static void ltl_error(const char*) +{ + throw LtlFormula::ParseErrorException("error parsing LTL formula"); +} + + + +/****************************************************************************** + * + * Function for updating the set of intermediate results. + * + *****************************************************************************/ + +inline LtlFormula* newFormula(LtlFormula& f) +{ + intermediate_results.insert(&f); + return &f; +} + +%} + + + +%name-prefix="ltl_" + + + +/****************************************************************************** + * + * Declarations for terminal and nonterminal symbols used in the grammar rules + * below. + * + *****************************************************************************/ + +%union { + class LtlFormula* formula; +} + +/* Uninterpreted symbols. */ + +%token LTLPARSE_LPAR LTLPARSE_RPAR LTLPARSE_FALSE LTLPARSE_TRUE + LTLPARSE_UNKNOWN + +/* Atomic propositions. */ + +%token LTLPARSE_ATOM + +/* Operators. */ + +%nonassoc LTLPARSE_UNTIL LTLPARSE_RELEASE LTLPARSE_WEAK_UNTIL + LTLPARSE_STRONG_RELEASE LTLPARSE_BEFORE +%left LTLPARSE_IMPLY LTLPARSE_EQUIV LTLPARSE_XOR +%left LTLPARSE_OR +%left LTLPARSE_AND +%nonassoc LTLPARSE_NOT LTLPARSE_NEXT LTLPARSE_FINALLY LTLPARSE_GLOBALLY +%nonassoc LTLPARSE_EQUALS + +/* Compound formulas. */ + +%type formula atomic_formula unary_formula prefix_op_formula + binary_formula prefix_b_formula infix_b_formula + + + +/****************************************************************************** + * + * Grammar rule definitions. + * + *****************************************************************************/ + +%% + +ltl_formula: formula + { result = $1; } + ; + +formula: atomic_formula + { $$ = $1; } + + | unary_formula + { $$ = $1; } + + | binary_formula + { $$ = $1; } + + | LTLPARSE_LPAR formula LTLPARSE_RPAR + { $$ = $2; } + ; + +atomic_formula: LTLPARSE_ATOM + { $$ = $1; } + + | LTLPARSE_ATOM LTLPARSE_EQUALS LTLPARSE_FALSE + { + intermediate_results.erase($1); + $$ = newFormula(Not::construct($1)); + } + + | LTLPARSE_ATOM LTLPARSE_EQUALS LTLPARSE_TRUE + { $$ = $1; } + + | LTLPARSE_FALSE + { $$ = newFormula(False::construct()); } + + | LTLPARSE_TRUE + { $$ = newFormula(True::construct()); } + ; + +unary_formula: LTLPARSE_NOT formula + { + intermediate_results.erase($2); + $$ = newFormula(Not::construct($2)); + } + + | LTLPARSE_NEXT formula + { + intermediate_results.erase($2); + $$ = newFormula(Next::construct($2)); + } + + | LTLPARSE_FINALLY formula + { + intermediate_results.erase($2); + $$ = newFormula(Finally::construct($2)); + } + + | LTLPARSE_GLOBALLY formula + { + intermediate_results.erase($2); + $$ = newFormula(Globally::construct($2)); + } + ; + +prefix_op_formula: atomic_formula + { $$ = $1; } + + | unary_formula + { $$ = $1; } + + | prefix_b_formula + { $$ = $1; } + + | LTLPARSE_LPAR formula LTLPARSE_RPAR + { $$ = $2; } + ; + +binary_formula: prefix_b_formula + { $$ = $1; } + | infix_b_formula + { $$ = $1; } + ; + +prefix_b_formula: LTLPARSE_AND prefix_op_formula prefix_op_formula + { + intermediate_results.erase($2); + intermediate_results.erase($3); + $$ = newFormula(And::construct($2, $3)); + } + + | LTLPARSE_OR prefix_op_formula prefix_op_formula + { + intermediate_results.erase($2); + intermediate_results.erase($3); + $$ = newFormula(Or::construct($2, $3)); + } + + | LTLPARSE_IMPLY prefix_op_formula prefix_op_formula + { + intermediate_results.erase($2); + intermediate_results.erase($3); + $$ = newFormula(Imply::construct($2, $3)); + } + + | LTLPARSE_EQUIV prefix_op_formula prefix_op_formula + { + intermediate_results.erase($2); + intermediate_results.erase($3); + $$ = newFormula(Equiv::construct($2, $3)); + } + + | LTLPARSE_XOR prefix_op_formula prefix_op_formula + { + intermediate_results.erase($2); + intermediate_results.erase($3); + $$ = newFormula(Xor::construct($2, $3)); + } + + | LTLPARSE_UNTIL prefix_op_formula prefix_op_formula + { + intermediate_results.erase($2); + intermediate_results.erase($3); + $$ = newFormula(Until::construct($2, $3)); + } + + | LTLPARSE_RELEASE prefix_op_formula prefix_op_formula + { + intermediate_results.erase($2); + intermediate_results.erase($3); + $$ = newFormula(V::construct($2, $3)); + } + + | LTLPARSE_WEAK_UNTIL prefix_op_formula prefix_op_formula + { + intermediate_results.erase($2); + intermediate_results.erase($3); + $$ = newFormula(WeakUntil::construct($2, $3)); + } + + | LTLPARSE_STRONG_RELEASE prefix_op_formula + prefix_op_formula + { + intermediate_results.erase($2); + intermediate_results.erase($3); + $$ = newFormula(StrongRelease::construct($2, $3)); + } + + | LTLPARSE_BEFORE prefix_op_formula prefix_op_formula + { + intermediate_results.erase($2); + intermediate_results.erase($3); + $$ = newFormula(Before::construct($2, $3)); + } + ; + +infix_b_formula: formula LTLPARSE_AND formula + { + intermediate_results.erase($1); + intermediate_results.erase($3); + $$ = newFormula(And::construct($1, $3)); + } + + | formula LTLPARSE_OR formula + { + intermediate_results.erase($1); + intermediate_results.erase($3); + $$ = newFormula(Or::construct($1, $3)); + } + + | formula LTLPARSE_IMPLY formula + { + intermediate_results.erase($1); + intermediate_results.erase($3); + $$ = newFormula(Imply::construct($1, $3)); + } + + | formula LTLPARSE_EQUIV formula + { + intermediate_results.erase($1); + intermediate_results.erase($3); + $$ = newFormula(Equiv::construct($1, $3)); + } + + | formula LTLPARSE_XOR formula + { + intermediate_results.erase($1); + intermediate_results.erase($3); + $$ = newFormula(Xor::construct($1, $3)); + } + + | formula LTLPARSE_UNTIL formula + { + intermediate_results.erase($1); + intermediate_results.erase($3); + $$ = newFormula(Until::construct($1, $3)); + } + + | formula LTLPARSE_RELEASE formula + { + intermediate_results.erase($1); + intermediate_results.erase($3); + $$ = newFormula(V::construct($1, $3)); + } + + | formula LTLPARSE_WEAK_UNTIL formula + { + intermediate_results.erase($1); + intermediate_results.erase($3); + $$ = newFormula(WeakUntil::construct($1, $3)); + } + + | formula LTLPARSE_STRONG_RELEASE formula + { + intermediate_results.erase($1); + intermediate_results.erase($3); + $$ = newFormula(StrongRelease::construct($1, $3)); + } + + | formula LTLPARSE_BEFORE formula + { + intermediate_results.erase($1); + intermediate_results.erase($3); + $$ = newFormula(Before::construct($1, $3)); + } + ; + +%% + + + +/****************************************************************************** + * + * Helper function for reading lexical tokens from a stream. + * + *****************************************************************************/ + +static inline size_t matchCharactersFromStream + (istream& stream, char* chars) +{ + size_t num_matched; + for (num_matched = 0; *chars != '\0' && stream.peek() == *chars; ++chars) + { + stream.ignore(1); + ++num_matched; + } + return num_matched; +} + + +/****************************************************************************** + * + * Main interface to the parser. + * + *****************************************************************************/ + +namespace Ltl +{ + +/* ========================================================================= */ +LtlFormula* parseFormula(istream& stream) +/* ---------------------------------------------------------------------------- + * + * Description: Parses an LTL formula from a stream. The formula should be + * in one of the formats used by the tools lbtt 1.0.x (both + * prefix and infix form), Spin/Temporal Massage Parlor/LTL2BA, + * LTL2AUT or Wring 1.1.0 (actually, the grammar is basically + * a combination of the grammars of the above tools with the + * exception that propositions should always be written in the + * form `pN' for some integer N; in principle, it is possible to + * use a mixed syntax for the formula). The input should be + * terminated with a newline. + * + * Argument: stream -- A reference to the input stream. + * + * Returns: A pointer to the formula. The function throws an + * LtlFormula::ParseErrorException if the syntax is incorrect, + * or an IOException in case of an end-of-file or another I/O + * error. + * + * ------------------------------------------------------------------------- */ +{ + Exceptional_istream es(&stream, ios::badbit | ios::failbit | ios::eofbit); + estream = &es; + intermediate_results.clear(); + + try + { + ltl_parse(); + } + catch (...) + { + for (std::set, ALLOC(LtlFormula*) > + ::const_iterator f = intermediate_results.begin(); + f != intermediate_results.end(); + ++f) + LtlFormula::destruct(*f); + throw; + } + return result; +} + +} + + + +/****************************************************************************** + * + * The lexical scanner. + * + *****************************************************************************/ + +static int ltl_lex() +{ + char c; + std::istream& stream = static_cast(*estream); + + do + { + estream->get(c); + } + while (isspace(c) && c != '\n'); + + switch (c) + { + case '\n' : return 0; + + case '(' : + return (matchCharactersFromStream(stream, ")") == 1 + ? LTLPARSE_NEXT + : LTLPARSE_LPAR); + + case ')' : return LTLPARSE_RPAR; + + case 'f' : + switch (matchCharactersFromStream(stream, "alse")) + { + case 0 : case 4 : + return LTLPARSE_FALSE; + default: + break; + } + return LTLPARSE_UNKNOWN; + + case '0' : return LTLPARSE_FALSE; + + case 't' : + switch (matchCharactersFromStream(stream, "rue")) + { + case 0 : case 3 : + return LTLPARSE_TRUE; + default : + return LTLPARSE_UNKNOWN; + } + + case 'T' : + return (matchCharactersFromStream(stream, "RUE") == 3 + ? LTLPARSE_TRUE + : LTLPARSE_UNKNOWN); + + case '1' : return LTLPARSE_TRUE; + + case '!' : case '~' : return LTLPARSE_NOT; + + case '&' : + matchCharactersFromStream(stream, "&"); + return LTLPARSE_AND; + + case '/' : + return (matchCharactersFromStream(stream, "\\") == 1 + ? LTLPARSE_AND + : LTLPARSE_UNKNOWN); + + case '*' : return LTLPARSE_AND; + + case '|' : + matchCharactersFromStream(stream, "|"); + return LTLPARSE_OR; + + case '\\' : + return (matchCharactersFromStream(stream, "/") == 1 + ? LTLPARSE_OR + : LTLPARSE_UNKNOWN); + + case '+' : return LTLPARSE_OR; + + case '=' : + return (matchCharactersFromStream(stream, ">") == 1 + ? LTLPARSE_IMPLY + : LTLPARSE_EQUALS); + + case '-' : + return (matchCharactersFromStream(stream, ">") == 1 + ? LTLPARSE_IMPLY + : LTLPARSE_UNKNOWN); + + case 'i' : return LTLPARSE_IMPLY; + + case '<' : + if (matchCharactersFromStream(stream, ">") == 1) + return LTLPARSE_FINALLY; + return (matchCharactersFromStream(stream, "->") == 2 + || matchCharactersFromStream(stream, "=>") == 2 + ? LTLPARSE_EQUIV + : LTLPARSE_UNKNOWN); + + case 'e' : return LTLPARSE_EQUIV; + + case 'x' : + return (matchCharactersFromStream(stream, "or") == 2 + ? LTLPARSE_XOR + : LTLPARSE_UNKNOWN); + + case '^' : return LTLPARSE_XOR; + + case 'X' : return LTLPARSE_NEXT; + + case 'U' : return LTLPARSE_UNTIL; + + case 'V' : case 'R' : return LTLPARSE_RELEASE; + + case 'W' : return LTLPARSE_WEAK_UNTIL; + + case 'M' : return LTLPARSE_STRONG_RELEASE; + + case 'B' : return LTLPARSE_BEFORE; + + case 'F' : + switch (matchCharactersFromStream(stream, "ALSE")) + { + case 0 : + return LTLPARSE_FINALLY; + case 4 : + return LTLPARSE_FALSE; + default : + return LTLPARSE_UNKNOWN; + } + + case '[' : + return (matchCharactersFromStream(stream, "]") == 1 + ? LTLPARSE_GLOBALLY + : LTLPARSE_UNKNOWN); + + case 'G' : return LTLPARSE_GLOBALLY; + + case 'p' : + { + long int id = 0; + bool id_ok = false; + int ch = stream.peek(); + while (ch >= '0' && ch <= '9') + { + id_ok = true; + estream->get(c); + if (LONG_MAX / 10 < id) + throw LtlFormula::ParseErrorException + ("error parsing LTL formula (proposition identifier out of " + "range)"); + id *= 10; + id += (c - '0'); + ch = stream.peek(); + } + + if (id_ok) + { + ltl_lval.formula = newFormula(Atom::construct(id)); + return LTLPARSE_ATOM; + } + return LTLPARSE_UNKNOWN; + } + + default : return LTLPARSE_UNKNOWN; + } +} diff --git a/lbtt/src/Product.h b/lbtt/src/Product.h new file mode 100644 index 000000000..f7b49a677 --- /dev/null +++ b/lbtt/src/Product.h @@ -0,0 +1,2936 @@ +/* + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 + * Heikki Tauriainen + * + * This program 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. + * + * This program 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 this program; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. + */ + +#ifndef PRODUCT_H +#define PRODUCT_H + +#include +#include +#include +#include +#include +#include "LbttAlloc.h" +#include "BitArray.h" +#include "EdgeContainer.h" +#include "Exception.h" +#include "Graph.h" +#include "SccCollection.h" + +using namespace std; + +extern bool user_break; + +namespace Graph +{ + +/****************************************************************************** + * + * A template class for representing the product of two + * Graph objects (which, in lbtt, are always either two + * BuchiAutomaton objects, or a BuchiAutomaton and a StateSpace). + * + * The class provides functions for checking the products of these objects for + * emptiness (i.e., for two Büchi automata, whether the intersection of their + * languages is (non)empty; for a Büchi automaton and a state space, whether + * some infinite path in the state space is accepted by the automaton). The + * functions are as follows: + * + * * bool localEmptinessCheck + * (Graph::size_type, + * Graph::size_type) + * Checks whether the subproduct rooted at a product state + * determined by a pair of component state identifiers is not + * empty and returns true if this is the case. + * + * * pair::size_type, unsigned long int> + * globalEmptinessCheck + * (Graph::size_type state, Bitset&, + * unsigned long int emptiness_check_size) + * Checks a set of subproducts for emptiness and stores the + * results in a bit set that should have room for (at least) + * `emptiness_check_size' bits (this number is assumed to be less + * than the number of states in the second component of the + * product). The first parameter `state' identifies a state in + * the first component of the product. After the call, the i'th + * bit (for all 0 <= i < emptiness_check_size) in the bit set will + * then be 1 iff the subproduct rooted at the product state + * determined by the pair of state identifiers (state, i) is + * nonempty. The function returns a pair of numbers corresponding + * to the number of product states and transitions generated + * during the emptiness check. + * + * * void findWitness + * (Graph::size_type, + * Graph::size_type, + * Product::Witness&) + * Checks whether the subproduct rooted at a product state + * determined by a pair of component state identifiers is not + * empty. If this is the case, the function constructs a + * certificate (a "witness") for the nonemptiness. For the + * product of two Büchi automata, the witness is an accepting + * execution from both automata on the same input; for the product + * of a Büchi automaton and a state space, the witness is a path + * in the state space that is accepted by the automaton. + * + * All of these functions construct the product "on the fly" with the help of + * operations provided by the class Operations used for instantiating the + * template. The public interface of this class must support the following + * operations: + * + * * Operations(const Graph&, + * const Graph&) + * Constructor that accepts references to the first and second + * component of the product (in this order) as parameters. + * + * * bool empty() + * A predicate which returns "true" iff either of the product + * components is (trivially) empty, i.e., iff either component has + * no states. + * + * * unsigned long int numberOfAcceptanceSets() + * Returns the number of acceptance sets associated with a state + * or a transition in the product. + * + * * const Graph::Node& firstComponent + * (Graph::size_type), + * const Graph::Node& secondComponent + * (Graph::size_type) + * Functions for accessing the states in the individual product + * components such that firstComponent(i) (secondComponent(i)) + * returns a reference to the i'th state of the first (second) + * component in the product. + * + * * void mergeAcceptanceInformation + * (const Graph::Node&, + * const Graph::Node&, + * BitArray&) + * Updates the acceptance information of a product state + * (determined by a state of the first and the second component, + * respectively) into a BitArray that is guaranteed to have room + * for at least numberOfAcceptanceSets() bits. The function + * should not clear bits in the array. + * + * * void mergeAcceptanceInformation + * (const Graph::Edge&, + * const Graph::Edge&, + * BitArray& + * Updates the acceptance information of a product transition + * (corresponding to a pair of transitions of the first and second + * product component) into a BitArray (guaranteed to have room for + * at least numberOfAcceptanceSets() bits). The function should + * not clear bits in the array. + * + * * void validateEdgeIterators + * (const Graph::Node& node_1, + * const Graph::Node& node_2, + * GraphEdgeContainer::const_iterator iterator_1&, + * GraphEdgeContainer::const_iterator iterator_2&) + * Checks whether a pair of edges determined from a pair of + * iterators corresponds to an edge starting from a given state + * (node_1, node_2) in the product. If yes, the function should + * leave the iterators intact; otherwise the iterators should be + * updated such that they point to a pair of edges corresponding + * to an edge in the product (or to `node_1.edges().end()' and + * `node_2.edges().end()' if this is not possible). + * Calling the function with the iterators initialized to + * `node_1.edges().begin()' and `node_2.edges().begin()' should + * update the iterators such that repeated calls to + * `incrementEdgeIterators' (see below) result in an enumeration + * of all product edges beginning from the product state + * (node_1, node_2). + * + * * void incrementEdgeIterators + * (const Graph::Node& node_1, + * const Graph::Node& node_2, + * GraphEdgeContainer::const_iterator iterator_1&, + * GraphEdgeContainer::const_iterator iterator_2&) + * Updates a pair of edge iterators to point to the "next" edge + * starting from a given state (node_1, node_2) in the product + * (or to (node_1.edges().end(), node_2.edges().end()) if this is + * not possible). + * + * See the files BuchiProduct.h and StateSpaceProduct.h for examples of classes + * used for instantiating the template. + * + * Given a class suitable for instantiating the Product template, a product is + * built with the constructor + * Product::Product + * (const Graph& graph_1, + * const Graph& graph_2). + * The product can be then analyzed by calling one of the emptiness checking + * functions described above. + * + * Note: All emptiness checking functions fail by throwing an exception of type + * Product::SizeException if + * `graph_1.size() * graph_2.size()' exceeds the maximum integer + * representables using Graph::size_type. The + * implementation does not support such products. + * + * Note: Operations in the Product class are not re-entrant. + * + *****************************************************************************/ + +template +class Product +{ +public: + Product /* Constructor. */ + (const Graph& g1, + const Graph& g2); + + ~Product(); /* Destructor. */ + + typedef typename Graph /* Type of product state */ + ::size_type size_type; /* identifiers. */ + + class ProductState; /* A class for accessing + * states in the product. + */ + + const ProductState operator[] /* Indexing operator. */ + (const size_type index) const; + + size_type stateId /* Constructs a product */ + (const size_type state_1, /* state identifier from */ + const size_type state_2) const; /* the identifiers of + * the state components. + */ + + const Graph::Node& /* Functions for */ + firstComponent(const size_type state) const; /* accessing the */ + const Graph::Node& /* components of a */ + secondComponent(const size_type state) const; /* product state. */ + + bool empty() const; /* Tells whether the + * product is (trivially) + * empty. + */ + + struct Witness /* Structure for */ + { /* representing witness */ + pair::Path, /* paths for */ + Graph::Path> /* the nonemptiness of */ + prefix; /* the product. */ + pair::Path, + Graph::Path> + cycle; + }; + + bool localEmptinessCheck /* Checks whether the */ + (const typename Graph /* subproduct rooted at */ + ::size_type s1_id, /* a product state */ + const typename Graph /* determined by a pair */ + ::size_type s2_id); /* of component state + * identifiers is empty. + */ + + const pair /* Checks a set of */ + globalEmptinessCheck /* subproducts for */ + (const typename Graph /* emptiness (see */ + ::size_type state_id, /* above). */ + Bitset& result, + const unsigned long int emptiness_check_size); + + void findWitness + (const size_type s1_id, const size_type s2_id, /* Checks whether the */ + Witness& witness); /* subproduct rooted at + * a product state + * determined by a pair + * of component state + * identifiers is empty. + * If this is the case, + * constructs also a + * witness for the + * nonemptiness. + */ + + /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ + + class ProductEdge; /* Classes for */ + class ProductEdgePointer; /* representing + * transitions in the + * product and + * "pointer-like" + * objects to them. + */ + + /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ + + class ProductEdgeCollection /* A class that mimics + * a container for + * transitions starting + * from a product state. + * (The container does + * not actually store the + * transitions; instead, + * it provides functions + * for constructing + * iterators that can be + * used to generate the + * transitions.) + */ + { + public: + explicit ProductEdgeCollection /* Constructor. */ + (const size_type state); + + /* default copy constructor */ + + ~ProductEdgeCollection(); /* Destructor. */ + + /* default assignment operator */ + + class const_iterator /* Iterator for generating + * the transitions starting + * from a product state. + */ + { + public: + const_iterator(); /* Default constructor. */ + + const_iterator + (const size_type state, /* Constructor. */ + const GraphEdgeContainer::const_iterator& + e1, + const GraphEdgeContainer::const_iterator& + e2); + + /* default copy constructor */ + + ~const_iterator(); /* Destructor. */ + + /* default assignment operator */ + + bool operator==(const const_iterator& it) /* Equality test between */ + const; /* iterators. */ + + bool operator!=(const const_iterator& it) /* Inequality test */ + const; /* between iterators. */ + + const ProductEdgePointer operator*() const; /* Dereferencing */ + const ProductEdge operator->() const; /* operators. */ + + const ProductEdgePointer operator++(); /* Prefix and postfix */ + const ProductEdgePointer operator++(int); /* increment operators. */ + + private: + size_type product_state; /* Product state */ + /* associated with the + * iterator. + */ + + GraphEdgeContainer::const_iterator edge_1; /* Pair of iterators */ + GraphEdgeContainer::const_iterator edge_2; /* from which product + * edges are determined. + */ + }; + + const const_iterator begin() const; /* Returns an iterator to + * the "beginning" of the + * list of transitions + * starting from the + * product state + * `this->product_state'. + */ + + const const_iterator end() const; /* Returns an iterator to + * the "end" of the list of + * transitions starting + * from the product state + * `this->product_state'. + */ + + private: + size_type product_state; /* Product state associated + * with the transition + * container. + */ + }; + + /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ + + class SizeException : public Exception /* An exception class to */ + /* be used in cases */ + /* where `size_type' */ + /* cannot hold values */ + /* large enough to */ + /* accommodate the */ + /* largest identifier */ + /* for a product state. */ + { + public: + SizeException(); /* Constructor. */ + + /* default copy constructor */ + + ~SizeException() throw(); /* Destructor. */ + + SizeException& operator= /* Assignment operator. */ + (const SizeException& e); + + /* `what' inherited from class Exception */ + }; + + /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ + + typedef ProductEdge Edge; /* Type definitions */ + typedef ProductEdgeCollection EdgeContainerType; /* required for making */ + /* Product */ + struct PathElement; /* suitable for */ + typedef deque /* instantiating the */ + Path; /* SccCollection + * template (see + * SccCollection.h). + */ + + /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ + +private: + Product(const Product&); /* Prevent copying and */ + Product& operator=(const Product&); /* assignment of Product + * objects. + */ + + class AcceptanceTracker; /* Callback operations */ + class SimpleEmptinessChecker; /* used when searching */ + class AcceptanceReachabilityTracker; /* the product for */ + class AcceptingComponentFinder; /* strongly connected + * components. + */ + + void addCycleSegment /* Helper function for */ + (pair::Path, /* constructing a */ + Graph::Path >& cycle, /* segment of the cycle */ + size_type source_state_id, Edge transition, /* in a witness for the */ + const size_type root_id, /* nonemptiness of the */ + const map, + ALLOC(PathElement) >& + predecessor) const; + + Operations operations; /* Operations for + * building the product + * on the fly. + */ + + bool too_large; /* Will be set to true + * if `size_type' cannot + * hold the maximum value + * that may be required for + * product state + * identifiers. Calling + * one of the emptiness + * checking operations on + * such a product results + * in a run-time exception. + */ + + const size_type state_id_multiplier; /* Size of the "second" + * component of the + * product. + */ + + static Product* product; /* Pointer to the "current" + * product (i.e., the + * product for which one + * of the emptiness + * checking operations was + * last called) to allow + * accessing it from + * member classes. + */ +}; + + + +/****************************************************************************** + * + * A template class for providing a Graph<>::Node-like interface to the states + * in a product (needed for accessing the transitions leaving from a state). + * + *****************************************************************************/ + +template +class Product::ProductState +{ +public: + ProductState(const size_type state); /* Constructor. */ + + /* default copy constructor */ + + ~ProductState(); /* Destructor. */ + + /* default assignment operator */ + + const EdgeContainerType& edges() const; /* Returns an object for + * generating the + * transitions starting + * from the state. + */ + +private: + EdgeContainerType outgoing_edges; /* Object for generating + * the transitions starting + * from the state. + */ +}; + + + +/****************************************************************************** + * + * A template class for providing a Graph<>::Edge-like interface to the + * transitions in a product. + * + *****************************************************************************/ + +template +class Product::ProductEdge +{ +public: + ProductEdge /* Constructor. */ + (const GraphEdgeContainer::const_iterator& e1, + const GraphEdgeContainer::const_iterator& e2); + + /* default copy constructor */ + + ~ProductEdge(); /* Destructor. */ + + /* default assignment operator */ + + const Graph::Edge& /* Functions for */ + firstComponent() const; /* accessing the */ + const Graph::Edge& /* components of a */ + secondComponent() const; /* product transition. */ + + size_type targetNode() const; /* Returns the target state + * of the transition. + */ + +private: + const Graph::Edge* edge_1; /* Components of the */ + const Graph::Edge* edge_2; /* transition. */ +}; + + + +/****************************************************************************** + * + * A template class for providing a constant pointer -like interface to + * ProductEdge objects. + * + *****************************************************************************/ + +template +class Product::ProductEdgePointer +{ +public: + ProductEdgePointer /* Constructor. */ + (const GraphEdgeContainer::const_iterator& e1, + const GraphEdgeContainer::const_iterator& e2); + + /* default copy constructor */ + + ~ProductEdgePointer(); /* Destructor. */ + + /* default assignment operator */ + + const ProductEdge& operator*() const; /* Dereferencing */ + const ProductEdge* operator->() const; /* operators. */ + +private: + ProductEdge edge; /* The product transition. + */ +}; + + + +/****************************************************************************** + * + * A template class for representing (product state, product transition) pairs + * in a path in the product. + * + *****************************************************************************/ + +template +struct Product::PathElement +{ + PathElement(const size_type s, const Edge& t); /* Constructor. */ + + /* default copy constructor */ + + ~PathElement(); /* Destructor. */ + + /* default assignment operator */ + + size_type state; /* Product state and */ + Edge transition; /* transition. */ +}; + + + +/****************************************************************************** + * + * A template class for tracking acceptance information in strongly connected + * product components by (essentially) recording the information into roots of + * the components. This is done using the method described by Couvreur in + * [J.-M. Couvreur. On-the-fly verification of linear temporal logic. + * In Proceedings of the FM'99 World Congress on Formal Methods in the + * Development of Computing Systems, Volume I, LNCS 1708, pp. 253--271. + * Springer-Verlag, 1999]. + * + *****************************************************************************/ + +template +class Product::AcceptanceTracker : + public VisitorInterface > +{ +public: + explicit AcceptanceTracker /* Constructor. */ + (const unsigned long int num_accept_sets); + + virtual ~AcceptanceTracker(); /* Destructor. */ + + /* `enter' inherited */ + + /* `backtrack' inherited */ + + /* `touch' inherited */ + + /* `leave' inherited */ + + virtual void addEdgeToComponent /* Adds the acceptance */ + (const Edge& t, const size_type scc_id); /* sets associated with + * a product transition + * to a nontrivial + * strongly connected + * component of the + * product. + */ + + virtual void addNodeToComponent /* Adds the acceptance */ + (const size_type state_id, /* sets associated with */ + const size_type scc_id); /* a product state to a */ + /* nontrivial strongly + * connected component + * of the product. + */ + + /* `beginComponent' inherited */ + + /* `insert' inherited */ + + virtual void endComponent /* Removes the */ + (const size_type scc_id); /* association between a + * nontrivial strongly + * connected product + * component and a set + * of acceptance sets + * when the component is + * not needed any + * longer. + */ + +protected: + typedef pair /* Association between */ + AcceptanceStackElement; /* a strongly connected + * component identifier + * and a collection of + * acceptance sets. + */ + + typedef deque /* the above */ + AcceptanceStack; /* associations. */ + + AcceptanceStack acceptance_stack; /* Stack for storing the + * dfs numbers of roots + * of strongly connected + * components and + * acceptance sets + * associated with them. + */ + + BitArray* acceptance_sets; /* Used for manipulating + * the stack. + */ + + const unsigned long int /* Number of acceptance */ + number_of_acceptance_sets; /* sets in the product. */ + +private: + AcceptanceTracker(const AcceptanceTracker&); /* Prevent copying and */ + AcceptanceTracker& operator= /* assignment of */ + (const AcceptanceTracker&); /* AcceptanceTracker + * objects. + */ +}; + + + +/****************************************************************************** + * + * A template class for checking a product for emptiness. + * + *****************************************************************************/ + +template +class Product::SimpleEmptinessChecker : public AcceptanceTracker +{ +public: + explicit SimpleEmptinessChecker /* Constructor. */ + (const unsigned long int num_accept_sets); + + ~SimpleEmptinessChecker(); /* Destructor. */ + + typedef int SccType; /* Dummy type definition + * required for supporting + * the expected class + * interface. + */ + + const SccType& operator()() const; /* Dummy function required + * for supporting the + * expected class + * interface. + */ + + /* `enter' inherited */ + + /* `backtrack' inherited */ + + /* `touch' inherited */ + + /* `leave' inherited */ + + void addEdgeToComponent /* Adds the acceptance */ + (const Edge& t, const size_type scc_id); /* sets associated with + * a product transition + * to a nontrivial + * strongly connected + * component of the + * product and aborts + * the emptiness check + * if an accepting + * strongly connected + * component is + * detected. + */ + + void addNodeToComponent /* Adds the acceptance */ + (const size_type state, /* sets associated with */ + const size_type scc_id); /* a product state to a + * nontrivial strongly + * connected component + * of the product and + * aborts the emptiness + * check if an accepting + * strongly connected + * component is + * detected. + */ + + /* `beginComponent' inherited */ + + /* `insert' inherited */ + + /* `endComponent' inherited */ + +private: + SimpleEmptinessChecker /* Prevent copying and */ + (const SimpleEmptinessChecker&); /* assignment of */ + SimpleEmptinessChecker& /* SimpleEmptiness- */ + operator=(const SimpleEmptinessChecker&); /* Checker objects. */ + + void abortIfNonempty() const; /* Aborts the search when + * an accepting strongly + * connected component is + * found. + */ + + SccType dummy; /* Dummy variable needed + * for implementing the + * operator() function. + */ +}; + + + +/****************************************************************************** + * + * A template class for tracking the reachability of accepting strongly + * connected components in a product. + * + *****************************************************************************/ + +template +class Product::AcceptanceReachabilityTracker + : public Product::AcceptanceTracker +{ +public: + explicit AcceptanceReachabilityTracker /* Constructor. */ + (const unsigned long int num_accept_sets); + + ~AcceptanceReachabilityTracker(); /* Destructor. */ + + typedef int SccType; /* Dummy type definition + * required for supporting + * the expected class + * interface. + */ + + const SccType& operator()() const; /* Dummy function required + * for supporting the + * expected class + * interface. + */ + + void enter(const size_type); /* Function called when + * entering a new product + * state. + */ + + void backtrack /* Function called when */ + (const size_type source, const Edge&, /* backtracking from a */ + const size_type target); /* product state. */ + + void touch /* Function called when */ + (const size_type source, const Edge& edge, /* processing an edge */ + const size_type target); /* with a target state + * that has already been + * visited during the + * search. + */ + + /* `leave' inherited */ + + /* `addEdgeToComponent' inherited */ + + /* `addNodeToComponent' inherited */ + + void beginComponent /* Tests whether the */ + (const size_type, const size_type state_id); /* strongly connected + * component about to + * be extracted from the + * product is an + * accepting component, + * or if it contains a + * state from which such + * a component is known + * to be reachable. + */ + + void insert(const size_type state); /* Function used for + * updating accepting + * component reachability + * information while + * extracting states from + * a product component. + */ + + /* `endComponent' inherited */ + + bool isMarked(const size_type state) const; /* Tests whether an + * accepting component is + * known to be reachable + * from a product state. + */ + + size_type numberOfStates() const; /* Tells the number of + * product states explored + * during the search. + */ + + unsigned long int numberOfTransitions() const; /* Tells the number of + * product transitions + * explored during the + * search. + */ + +private: + AcceptanceReachabilityTracker /* Prevent copying and */ + (const AcceptanceReachabilityTracker&); /* assignment of */ + AcceptanceReachabilityTracker& /* AcceptanceSet- */ + operator= /* ReachabilityTracker */ + (const AcceptanceReachabilityTracker&); /* objects. */ + + void markState(const size_type state); /* Adds a product state to + * the set of states from + * which an accepting + * component is known to be + * reachable. + */ + + set, /* Set of states from */ + ALLOC(size_type) > /* which an accepting */ + reachability_info; /* component is known to + * be reachable in the + * product. + */ + + size_type number_of_states; /* Number of states + * explored during the + * search. + */ + + unsigned long int number_of_transitions; /* Number of transitions + * explored during the + * search. + */ + + bool mark_scc; /* Used for determining + * whether to insert states + * into `this-> + * reachability_info' while + * extracting a strongly + * connected component from + * the product. + */ + + SccType dummy; /* Dummy variable needed + * for implementing the + * operator() function. + */ +}; + + + +/****************************************************************************** + * + * A template class for finding accepting maximal strongly connected components + * in a product. + * + *****************************************************************************/ + +template +class Product::AcceptingComponentFinder : + public Product::AcceptanceTracker +{ +public: + explicit AcceptingComponentFinder /* Constructor. */ + (const unsigned long int num_accept_sets); + + ~AcceptingComponentFinder(); /* Destructor. */ + + typedef set, /* Type definition for */ + ALLOC(size_type) > /* the set of product */ + SccType; /* state identifiers in + * an accepting + * strongly connected + * component. + */ + + const SccType& operator()() const; /* Returns the last + * accepting maximal + * strongly connected + * component found in the + * product. + */ + + /* `enter' inherited */ + + /* `backtrack' inherited */ + + /* `touch' inherited */ + + /* `leave' inherited */ + + /* `addEdgeToComponent' inherited */ + + /* `addNodeToComponent' inherited */ + + void beginComponent /* Tests whether the */ + (const size_type, const size_type); /* maximal strongly + * connected component + * that is about to be + * extracted from the + * product is an + * accepting component. + */ + + void insert(const size_type state); /* Inserts a state to an + * accepting component. + */ + + /* `endComponent' inherited */ + +private: + AcceptingComponentFinder /* Prevent copying and */ + (const AcceptingComponentFinder&); /* assignment of */ + AcceptingComponentFinder& /* AcceptingComponent- */ + operator=(const AcceptingComponentFinder&); /* Finder objects. */ + + SccType scc; /* Set of product state + * identifiers forming the + * last accepting strongly + * connected component + * found in the product. + */ + + bool construct_component; /* Used for determining + * whether the states + * extracted from a + * strongly connected + * component in the product + * should be inserted into + * `this->scc'. + */ +}; + + + +/****************************************************************************** + * + * Inline function definitions for template class Product. + * + *****************************************************************************/ + +/* ========================================================================= */ +template +inline Product::Product + (const Graph& g1, const Graph& g2) + : operations(g1, g2), state_id_multiplier(g2.size()) +/* ---------------------------------------------------------------------------- + * + * Description: Constructor for class Product. + * + * Arguments: g1, g2 -- Constant references to the components of the + * product. + * + * Returns: Nothing. If `Product::size_type' cannot hold + * values large enough to accommodate the largest identifier for + * a product state, `this->too_large' is set to true to cause + * all emptiness checking operations on the product to fail by + * throwing a Product::SizeException. + * + * ------------------------------------------------------------------------- */ +{ + too_large = (!g2.empty() && + g1.size() > (static_cast(-1) / g2.size())); +} + +/* ========================================================================= */ +template +inline Product::~Product() +/* ---------------------------------------------------------------------------- + * + * Description: Destructor for class Product. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +template +inline const typename Product::ProductState +Product::operator[] + (const typename Product::size_type index) const +/* ---------------------------------------------------------------------------- + * + * Description: Indexing operator for class Product. + * + * Argument: index -- Index of a state of the product. + * + * Returns: A ProductState object corresponding to the state with the + * given index. + * + * ------------------------------------------------------------------------- */ +{ + return ProductState(index); +} + +/* ========================================================================= */ +template +inline typename Product::size_type Product + ::stateId + (const size_type state_1, const size_type state_2) const +/* ---------------------------------------------------------------------------- + * + * Description: Returns the product state identifier corresponding to + * identifiers of the state components. + * + * Arguments: state_1, state_2 -- Identifiers for the product state + * components. + * + * Returns: Identifier of the product state corresponding to the + * components. + * + * ------------------------------------------------------------------------- */ +{ + return (state_1 * state_id_multiplier) + state_2; +} + +/* ========================================================================= */ +template +inline const Graph::Node& +Product::firstComponent(const size_type state) const +/* ---------------------------------------------------------------------------- + * + * Description: Function for accessing the "first" component state of a + * product state. + * + * Arguments: state -- Identifier of a product state. + * + * Returns: A constant reference to the state corresponding to the + * "first" component of the product state. + * + * ------------------------------------------------------------------------- */ +{ + return operations.firstComponent(state / state_id_multiplier); +} + +/* ========================================================================= */ +template +inline const Graph::Node& +Product::secondComponent(const size_type state) const +/* ---------------------------------------------------------------------------- + * + * Description: Function for accessing the "second" component state of a + * product state. + * + * Arguments: state -- Identifier of a product state. + * + * Returns: A constant reference to the state corresponding to the + * "second" component of the product state. + * + * ------------------------------------------------------------------------- */ +{ + return operations.secondComponent(state % state_id_multiplier); +} + +/* ========================================================================= */ +template +inline bool Product::empty() const +/* ---------------------------------------------------------------------------- + * + * Description: Tells whether the product is (trivially) empty, i.e., if + * either of its components has no states. + * + * Arguments: None. + * + * Returns: true iff the product is trivially empty. + * + * ------------------------------------------------------------------------- */ +{ + return operations.empty(); +} + + + +/****************************************************************************** + * + * Function definitions for template class Product. + * + *****************************************************************************/ + +/* ========================================================================= */ +template +bool Product::localEmptinessCheck + (const Graph::size_type s1_id, + const Graph::size_type s2_id) +/* ---------------------------------------------------------------------------- + * + * Description: Checks whether the subproduct rooted at a product state + * determined by a pair of component state identifiers is not + * empty. + * + * Arguments: s1_id, s2_id -- Identifiers for the product state + * components. + * + * Returns: true iff the subproduct rooted at the product state + * determined by `s1_id' and `s2_id' is not empty. Throws a + * Product::SizeException if the product is too + * large to handle. + * + * ------------------------------------------------------------------------- */ +{ + if (too_large) + throw SizeException(); + + if (empty()) + return false; + + product = this; + + SimpleEmptinessChecker ec(operations.numberOfAcceptanceSets()); + typedef SccCollection, SimpleEmptinessChecker> + ProductSccCollection; + + ProductSccCollection sccs(*this, ec); + + try + { + for (typename ProductSccCollection::iterator scc + = sccs.begin(stateId(s1_id, s2_id)); + scc != sccs.end(); + ++scc) + { + if (::user_break) + throw UserBreakException(); + } + } + catch (const int) + { + return true; + } + + return false; +} + +/* ========================================================================= */ +template +const pair::size_type, unsigned long int> +Product::globalEmptinessCheck + (const Graph::size_type state_id, + Bitset& result, const unsigned long int emptiness_check_size) +/* ---------------------------------------------------------------------------- + * + * Description: Checks a set of subproducts of the product for emptiness. + * + * Arguments: state_id -- Identifier of a state in the first + * component of the product. + * result -- A reference to a Bitset for storing + * the result of the emptiness check. + * The set should have room for at + * least `emptiness_check_size' bits. + * emptiness_check_size -- Determines the scope of the + * emptiness check (see below). + * + * Returns: A pair giving the numbers of product states and transitions + * generated during the emptiness check. The result of the + * emptiness check itself is stored into `result' such that + * the i'th bit (for all 0 <= i < emptiness_check_size) in the + * bit set will be 1 iff the subproduct rooted at the product + * state determined by the pair of state identifiers + * (state_id, i) is nonempty. + * + * The function throws a Product::SizeException if + * the product may be too large to handle. + * + * ------------------------------------------------------------------------- */ +{ + if (too_large) + throw SizeException(); + + result.clear(); + + if (empty()) + return make_pair(0, 0); + + product = this; + + AcceptanceReachabilityTracker rt(operations.numberOfAcceptanceSets()); + + typedef SccCollection, AcceptanceReachabilityTracker> + ProductSccCollection; + + ProductSccCollection sccs(*this, rt); + + for (Graph::size_type state = 0; + state < emptiness_check_size; + ++state) + { + for (typename ProductSccCollection::iterator scc + = sccs.begin(stateId(state_id, state)); + scc != sccs.end(); + ++scc) + { + if (::user_break) + throw UserBreakException(); + } + } + + for (Graph::size_type state = 0; + state < emptiness_check_size; + ++state) + { + if (rt.isMarked(stateId(state_id, state))) + result.setBit(state); + } + + return make_pair(rt.numberOfStates(), rt.numberOfTransitions()); +} + +/* ========================================================================= */ +template +void Product::findWitness + (const typename Graph::size_type s1_id, + const typename Graph::size_type s2_id, + typename Product::Witness& witness) +/* ---------------------------------------------------------------------------- + * + * Description: Checks whether the subproduct rooted at a product state + * determined by a pair of component state identifiers is not + * empty. If this is the case, constructs a witness for the + * nonemptiness. + * + * Arguments: s1_id, s2_id -- Identifiers for the product state + * components. + * witness -- A reference to an object for storing a + * witness if such a witness exists. + * + * Returns: Nothing. A witness was found iff + * `!witness.cycle.first.empty() + * && !witness.cycle.second.empty()' holds after the call. + * + * The function throws a Product::SizeException if + * the product may be too large to handle. + * + * ------------------------------------------------------------------------- */ +{ + if (too_large) + throw SizeException(); + + witness.prefix.first.clear(); + witness.prefix.second.clear(); + witness.cycle.first.clear(); + witness.cycle.second.clear(); + + if (empty()) + return; + + product = this; + const unsigned long int number_of_acceptance_sets + = operations.numberOfAcceptanceSets(); + const size_type start_state = stateId(s1_id, s2_id); + + AcceptingComponentFinder acf(number_of_acceptance_sets); + typedef SccCollection, AcceptingComponentFinder> + ProductSccCollection; + + ProductSccCollection sccs(*this, acf); + + for (typename ProductSccCollection::iterator scc = sccs.begin(start_state); + scc != sccs.end(); + ++scc) + { + if (::user_break) + throw UserBreakException(); + + if (!scc->empty()) + { + /* + * The prefix of the witness consists of a path from the given product + * state to a state in an accepting strongly connected product + * component. + */ + + Path path; + scc.getPath(path); + + for (typename Path::const_iterator path_element = path.begin(); + path_element != path.end(); + ++path_element) + { + witness.prefix.first.push_back + (Graph::PathElement + (path_element->state / state_id_multiplier, + path_element->transition.firstComponent())); + witness.prefix.second.push_back + (Graph::PathElement + (path_element->state % state_id_multiplier, + path_element->transition.secondComponent())); + } + + /* + * Construct an accepting cycle by performing a breadth-first search + * in the MSCC. + */ + + const size_type search_start_state + = path.empty() ? start_state : path.back().transition.targetNode(); + + BitArray collected_acceptance_sets(number_of_acceptance_sets); + collected_acceptance_sets.clear(number_of_acceptance_sets); + operations.mergeAcceptanceInformation + (firstComponent(search_start_state), + secondComponent(search_start_state), collected_acceptance_sets); + + unsigned long int number_of_collected_acceptance_sets + = collected_acceptance_sets.count(number_of_acceptance_sets); + + deque search_queue; + set, ALLOC(size_type) > visited; + map, ALLOC(PathElement) > + shortest_path_predecessor; + + size_type bfs_root = search_start_state; + +continue_bfs: + search_queue.clear(); + search_queue.push_back(bfs_root); + visited.clear(); + visited.insert(bfs_root); + shortest_path_predecessor.clear(); + + while (!search_queue.empty()) + { + const EdgeContainerType transitions + = ProductState(search_queue.front()).edges(); + + for (typename EdgeContainerType::const_iterator transition + = transitions.begin(); + transition != transitions.end(); + ++transition) + { + const size_type target = (*transition)->targetNode(); + if (scc->find(target) == scc->end()) + continue; + + if (visited.find(target) == visited.end()) + { + visited.insert(target); + shortest_path_predecessor.insert + (make_pair(target, PathElement(search_queue.front(), + **transition))); + search_queue.push_back(target); + + if (number_of_collected_acceptance_sets + < number_of_acceptance_sets) + operations.mergeAcceptanceInformation + (firstComponent(target), secondComponent(target), + collected_acceptance_sets); + } + + if (number_of_collected_acceptance_sets < number_of_acceptance_sets) + { + /* + * Test whether the current product transition or the target + * state of the transition covers new acceptance sets. If + * this is the case, construct the next segment of the cycle + * and begin a new breadth-first search in the target state of + * the transition. + */ + + operations.mergeAcceptanceInformation + ((*transition)->firstComponent(), + (*transition)->secondComponent(), collected_acceptance_sets); + + const unsigned long int num + = collected_acceptance_sets.count(number_of_acceptance_sets); + if (num > number_of_collected_acceptance_sets) + { + number_of_collected_acceptance_sets = num; + + addCycleSegment(witness.cycle, search_queue.front(), + **transition, bfs_root, + shortest_path_predecessor); + + if (number_of_collected_acceptance_sets + == number_of_acceptance_sets + && target == search_start_state) + return; + + bfs_root = target; + goto continue_bfs; + } + } + else if (target == search_start_state) + { + /* + * If all acceptance sets have been collected and the current + * product transition points to the first state of the cycle, + * the cycle is complete. + */ + + addCycleSegment(witness.cycle, search_queue.front(), **transition, + bfs_root, shortest_path_predecessor); + return; + } + } + + search_queue.pop_front(); + } + + throw Exception + ("Product::findWitness(...): internal error [cycle construction " + "failed]"); + } + } +} + +/* ========================================================================= */ +template +void Product::addCycleSegment + (pair::Path, Graph::Path>& + cycle, + size_type source_state_id, Edge transition, const size_type root_id, + const map, ALLOC(PathElement) >& + predecessor) const +/* ---------------------------------------------------------------------------- + * + * Description: Helper function for constructing a segment of an accepting + * cycle in the product. + * + * Arguments: cycle -- A reference to a pair of paths for + * storing the result. + * source_state_id -- Identifier of the last product state in + * the cycle segment. + * transition -- Last product transition in the cycle + * segment. + * root_id -- Identifier of the first product state in + * the cycle segment. + * predecessor -- Mapping between states and their + * predecessors in the cycle segment. + * + * Returns: Nothing. The segment of the cycle is appended to `cycle'. + * + * ------------------------------------------------------------------------- */ +{ + Graph::Path first_segment; + Graph::Path second_segment; + + while (1) + { + first_segment.push_front + (Graph::PathElement + (source_state_id / state_id_multiplier, transition.firstComponent())); + second_segment.push_front + (Graph::PathElement + (source_state_id % state_id_multiplier, + transition.secondComponent())); + + if (source_state_id == root_id) + { + cycle.first.insert(cycle.first.end(), first_segment.begin(), + first_segment.end()); + cycle.second.insert(cycle.second.end(), second_segment.begin(), + second_segment.end()); + return; + } + + const PathElement& p = predecessor.find(source_state_id)->second; + source_state_id = p.state; + transition = p.transition; + } +} + + + +/****************************************************************************** + * + * Inline function definitions for template class + * Product::ProductState. + * + *****************************************************************************/ + +/* ========================================================================= */ +template +inline Product::ProductState::ProductState + (const size_type state) : outgoing_edges(state) +/* ---------------------------------------------------------------------------- + * + * Description: Constructor for class Product::ProductState. + * + * Argument: state -- Identifier of a product state. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +template +inline Product::ProductState::~ProductState() +/* ---------------------------------------------------------------------------- + * + * Description: Destructor for class Product::ProductState. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +template +inline const typename Product::EdgeContainerType& +Product::ProductState::edges() const +/* ---------------------------------------------------------------------------- + * + * Description: Returns an object for generating the transitions starting + * from a product state. + * + * Arguments: None. + * + * Returns: A constant reference to an object that can be used for + * generating the transitions starting from the state. + * + * ------------------------------------------------------------------------- */ +{ + return outgoing_edges; +} + + + +/****************************************************************************** + * + * Inline function definitions for template class + * Product::ProductEdge. + * + *****************************************************************************/ + +/* ========================================================================= */ +template +inline Product::ProductEdge::ProductEdge + (const GraphEdgeContainer::const_iterator& e1, + const GraphEdgeContainer::const_iterator& e2) + : edge_1(*e1), edge_2(*e2) +/* ---------------------------------------------------------------------------- + * + * Description: Constructor for class Product::ProductEdge. + * + * Arguments: e1, e2 -- Iterators pointing to the components of the + * product transition. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +template +inline Product::ProductEdge::~ProductEdge() +/* ---------------------------------------------------------------------------- + * + * Description: Destructor for class Product::ProductEdge. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +template +inline const Graph::Edge& +Product::ProductEdge::firstComponent() const +/* ---------------------------------------------------------------------------- + * + * Description: Function for accessing the "first" component of a product + * transition. + * + * Arguments: None. + * + * Returns: A constant reference to the "first" component of the + * transition. + * + * ------------------------------------------------------------------------- */ +{ + return *edge_1; +} + +/* ========================================================================= */ +template +inline const Graph::Edge& +Product::ProductEdge::secondComponent() const +/* ---------------------------------------------------------------------------- + * + * Description: Function for accessing the "second" component of a product + * transition. + * + * Arguments: None. + * + * Returns: A constant reference to the "second" component of the + * transition. + * + * ------------------------------------------------------------------------- */ +{ + return *edge_2; +} + +/* ========================================================================= */ +template +inline typename Product::size_type +Product::ProductEdge::targetNode() const +/* ---------------------------------------------------------------------------- + * + * Description: Returns the target state of a product transition. + * + * Arguments: None. + * + * Returns: Identifier of the target state of the product transition. + * + * ------------------------------------------------------------------------- */ +{ + return product->stateId(edge_1->targetNode(), edge_2->targetNode()); +} + + + +/****************************************************************************** + * + * Inline function definitions for template class + * Product::ProductEdgePointer. + * + *****************************************************************************/ + +/* ========================================================================= */ +template +inline Product::ProductEdgePointer::ProductEdgePointer + (const GraphEdgeContainer::const_iterator& e1, + const GraphEdgeContainer::const_iterator& e2) + : edge(e1, e2) +/* ---------------------------------------------------------------------------- + * + * Description: Constructor for class + * Product::ProductEdgePointer. + * + * Arguments: e1, e2 -- Iterators pointing to the components of the + * product transition. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +template +inline Product::ProductEdgePointer::~ProductEdgePointer() +/* ---------------------------------------------------------------------------- + * + * Description: Destructor for class + * Product::ProductEdgePointer. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +template +inline const typename Product::ProductEdge& +Product::ProductEdgePointer::operator*() const +/* ---------------------------------------------------------------------------- + * + * Description: Dereferencing operator for class + * Product::ProductEdgePointer. + * + * Arguments: None. + * + * Returns: A reference to the product transition associated with the + * object. + * + * ------------------------------------------------------------------------- */ +{ + return edge; +} + +/* ========================================================================= */ +template +inline const typename Product::ProductEdge* +Product::ProductEdgePointer::operator->() const +/* ---------------------------------------------------------------------------- + * + * Description: Dereferencing operator for class + * Product::ProductEdgePointer. + * + * Arguments: None. + * + * Returns: A pointer to the product transition associated with the + * object. + * + * ------------------------------------------------------------------------- */ +{ + return &edge; +} + + + +/****************************************************************************** + * + * Inline function definitions for template class + * Product::ProductEdgeCollection. + * + *****************************************************************************/ + +/* ========================================================================= */ +template +inline Product::ProductEdgeCollection::ProductEdgeCollection + (const size_type state) : product_state(state) +/* ---------------------------------------------------------------------------- + * + * Description: Constructor for class + * Product::ProductEdgeCollection. + * + * Argument: state -- Identifier of a product state. The + * ProductEdgeCollection object will mimic a + * container for the product transitions starting + * from this state. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +template +inline Product::ProductEdgeCollection::~ProductEdgeCollection() +/* ---------------------------------------------------------------------------- + * + * Description: Destructor for class + * Product::ProductEdgeCollection. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +template +inline const typename Product::ProductEdgeCollection + ::const_iterator +Product::ProductEdgeCollection::begin() const +/* ---------------------------------------------------------------------------- + * + * Description: Returns an iterator for generating the transitions starting + * from the product state identified by `this->product_state'. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ + return const_iterator + (product_state, + product->firstComponent(product_state).edges().begin(), + product->secondComponent(product_state).edges().begin()); +} + +/* ========================================================================= */ +template +inline const typename Product::ProductEdgeCollection + ::const_iterator +Product::ProductEdgeCollection::end() const +/* ---------------------------------------------------------------------------- + * + * Description: Returns an iterator pointing to the "end" of the collection + * of transitions starting from the product state identified by + * `this->product_state'. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ + return const_iterator + (product_state, + product->firstComponent(product_state).edges().end(), + product->secondComponent(product_state).edges().end()); +} + + + +/****************************************************************************** + * + * Inline function definitions for template class + * Product::ProductEdgeCollection::const_iterator. + * + *****************************************************************************/ + +/* ========================================================================= */ +template +inline Product::ProductEdgeCollection::const_iterator + ::const_iterator() : product_state(0) +/* ---------------------------------------------------------------------------- + * + * Description: Default constructor for class + * Product::ProductEdgeCollection::const_iterator. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +template +inline Product::ProductEdgeCollection::const_iterator + ::const_iterator + (const size_type state, + const GraphEdgeContainer::const_iterator& e1, + const GraphEdgeContainer::const_iterator& e2) : + product_state(state), edge_1(e1), edge_2(e2) +/* ---------------------------------------------------------------------------- + * + * Description: Constructor for class + * Product::ProductEdgeCollection::const_iterator. + * + * Arguments: state -- Identifier of a product state to associate with + * the iterator. + * e1, e1 -- Constant references to a pair of iterators + * pointing to a pair of transitions starting from + * the component states of the product state. These + * iterators are used to determine where to start + * iterating over the product transitions. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ + product->operations.validateEdgeIterators + (product->firstComponent(product_state), + product->secondComponent(product_state), + edge_1, edge_2); +} + +/* ========================================================================= */ +template +inline Product::ProductEdgeCollection::const_iterator + ::~const_iterator() +/* ---------------------------------------------------------------------------- + * + * Description: Destructor for class + * Product::ProductEdgeCollection::const_iterator. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +template +inline bool Product::ProductEdgeCollection::const_iterator + ::operator== + (const const_iterator& it) const +/* ---------------------------------------------------------------------------- + * + * Description: Equality test between two + * Product::ProductEdgeCollection::const_iterators. + * + * Argument: it -- A constant reference to an iterator to compare for + * equality. It is assumed that the iterators are + * associated with the same product state; the result of + * a comparison between iterators associated with + * different product states is undefined. + * + * Returns: true iff `it' and `*this' point to the same transition in the + * product. + * + * ------------------------------------------------------------------------- */ +{ + return (it.edge_1 == edge_1 && it.edge_2 == edge_2); +} + +/* ========================================================================= */ +template +inline bool Product::ProductEdgeCollection::const_iterator + ::operator!= + (const const_iterator& it) const +/* ---------------------------------------------------------------------------- + * + * Description: Inequality test between two + * Product::ProductEdgeCollection::const_iterators. + * + * Argument: it -- A constant reference to an iterator to compare for + * equality. It is assumed that the iterators are + * associated with the same product state; the result of + * a comparison between iterators associated with + * different product states is undefined. + * + * Returns: true iff `it' and `*this' point to different transitions in + * the product. + * + * ------------------------------------------------------------------------- */ +{ + return (it.edge_1 != edge_1 || it.edge_2 != edge_2); +} + +/* ========================================================================= */ +template +inline const typename Product::ProductEdgePointer +Product::ProductEdgeCollection::const_iterator::operator*() const +/* ---------------------------------------------------------------------------- + * + * Description: Dereferencing operator for class + * Product::ProductEdgeCollection::const_iterator. + * + * Arguments: None. + * + * Returns: An object of type Product::ProductEdgePointer + * that allows access to the product transition pointed to by + * the iterator. + * + * ------------------------------------------------------------------------- */ +{ + return ProductEdgePointer(edge_1, edge_2); +} + +/* ========================================================================= */ +template +inline const typename Product::ProductEdge +Product::ProductEdgeCollection::const_iterator::operator->() const +/* ---------------------------------------------------------------------------- + * + * Description: Dereferencing operator for class + * Product::ProductEdgeCollection::const_iterator. + * + * Arguments: None. + * + * Returns: A Product::ProductEdge corresponding to the + * product transition pointed to by the iterator. + * + * ------------------------------------------------------------------------- */ +{ + return ProductEdge(edge_1, edge_2); +} + +/* ========================================================================= */ +template +inline const typename Product::ProductEdgePointer +Product::ProductEdgeCollection::const_iterator::operator++() +/* ---------------------------------------------------------------------------- + * + * Description: Prefix increment operator for class + * Product::ProductEdgeCollection::const_iterator. + * + * Arguments: None. + * + * Returns: An object of type Product::ProductEdgePointer + * that behaves like a pointer to the product transition + * obtained by advancing the iterator in the sequence of product + * transitions. + * + * ------------------------------------------------------------------------- */ +{ + product->operations.incrementEdgeIterators + (product->firstComponent(product_state), + product->secondComponent(product_state), + edge_1, edge_2); + return ProductEdgePointer(edge_1, edge_2); +} + +/* ========================================================================= */ +template +inline const typename Product::ProductEdgePointer +Product::ProductEdgeCollection::const_iterator::operator++(int) +/* ---------------------------------------------------------------------------- + * + * Description: Postfix increment operator for class + * Product::ProductEdgeCollection::const_iterator. + * + * Arguments: None. + * + * Returns: An object of type Product::ProductEdgePointer + * that behaves like a pointer to the product transition pointed + * to by the iterator before advancing it in the sequence of + * product transitions. + * + * ------------------------------------------------------------------------- */ +{ + const typename Product::ProductEdgePointer edge(edge_1, edge_2); + product->operations.incrementEdgeIterators + (product->firstComponent(product_state), + product->secondComponent(product_state), + edge_1, edge_2); + return edge; +} + + + +/****************************************************************************** + * + * Inline function definitions for template class + * Product::PathElement. + * + *****************************************************************************/ + +/* ========================================================================= */ +template +inline Product::PathElement::PathElement + (const size_type s, const Edge& t) : state(s), transition(t) +/* ---------------------------------------------------------------------------- + * + * Description: Constructor for class Product::PathElement. + * + * Arguments: s, t -- Product state and transition associated with the + * element. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +template +inline Product::PathElement::~PathElement() +/* ---------------------------------------------------------------------------- + * + * Description: Destructor for class Product::PathElement. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + + + +/****************************************************************************** + * + * Inline function definitions for template class + * Product::SizeException. + * + *****************************************************************************/ + +/* ========================================================================= */ +template +inline Product::SizeException::SizeException() : + Exception("product may be too large") +/* ---------------------------------------------------------------------------- + * + * Description: Constructor for class Product::SizeException. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +template +inline Product::SizeException::~SizeException() throw() +/* ---------------------------------------------------------------------------- + * + * Description: Destructor for class Product::SizeException. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +template +inline typename Product::SizeException& +Product::SizeException::operator= + (const typename Product::SizeException& e) +/* ---------------------------------------------------------------------------- + * + * Description: Assignment operator for class + * Product::SizeException. Assigns the value of + * another Product::SizeException to `this' one. + * + * Arguments: e -- A reference to a constant object of type + * ProductSizeException. + * + * Returns: A reference to the object whose value was changed. + * + * ------------------------------------------------------------------------- */ +{ + Exception::operator=(e); + return *this; +} + + + +/****************************************************************************** + * + * Inline function definitions for template class + * Product::AcceptanceTracker. + * + *****************************************************************************/ + +/* ========================================================================= */ +template +inline Product::AcceptanceTracker::AcceptanceTracker + (const unsigned long int num_accept_sets) + : number_of_acceptance_sets(num_accept_sets) +/* ---------------------------------------------------------------------------- + * + * Description: Constructor for class Product::AcceptanceTracker. + * + * Arguments: num_accept_sets -- Number of acceptance sets in the + * product. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ + /* Initialize `acceptance_stack' with a sentinel element. */ + acceptance_stack.push_front(make_pair(0, new BitArray(0))); +} + +/* ========================================================================= */ +template +inline Product::AcceptanceTracker::~AcceptanceTracker() +/* ---------------------------------------------------------------------------- + * + * Description: Destructor for class Product::AcceptanceTracker. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ + for (AcceptanceStack::iterator a = acceptance_stack.begin(); + a != acceptance_stack.end(); + ++a) + delete a->second; +} + +/* ========================================================================= */ +template +inline void Product::AcceptanceTracker::addEdgeToComponent + (const typename Product::Edge& t, + const typename Product::size_type scc_id) +/* ---------------------------------------------------------------------------- + * + * Description: Adds the acceptance sets of the product transition `t' + * (inside a strongly connected product component) to the + * collection of acceptance sets associated with the strongly + * connected component identifier (a dfs number of a product + * state in Tarjan's algorithm). (The component is therefore + * nontrivial, because it contains a transition.) This is done + * as described by Couvreur + * [J.-M. Couvreur. On-the-fly verification of linear + * temporal logic. In Proceedings of the FM'99 World + * Congress on Formal Methods in the Development of + * Computing Systems, Volume I, LNCS 1708, pp. 253--271. + * Springer-Verlag, 1999] + * by first collapsing all elements in the top part of + * `this->acceptance_stack' (*) with strongly connected + * component identifiers greater than or equal to `scc_id' into + * a single element by taking the union of their acceptance sets + * and then merging the acceptance sets of the transition `t' + * with this element. + * After the call, the top element of `this->acceptance_stack' + * will have the scc id `scc_id', and `this->acceptance_sets' + * points to the acceptance sets associated with this stack + * element. + * + * (*) It is assumed that the contents of + * `this->acceptance_stack' form (from top to bottom) a sequence + * of elements (id1,a1), (id2,a2), (id3,a3), ..., where + * id1 > id2 > id3 > ... . The function maintains this + * invariant. + * + * Arguments: t -- A constant reference to the product transition. + * scc_id -- Identifier of the strongly connected component + * (assumed to be >= 1). + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ + acceptance_sets = 0; + while (acceptance_stack.front().first >= scc_id) + { + if (acceptance_sets != 0) + { + acceptance_stack.front().second->bitwiseOr + (*acceptance_sets, number_of_acceptance_sets); + delete acceptance_sets; + } + acceptance_sets = acceptance_stack.front().second; + if (acceptance_stack.front().first == scc_id) + goto merge_sets; + + acceptance_stack.pop_front(); + } + + if (acceptance_sets == 0) + { + acceptance_sets = new BitArray(number_of_acceptance_sets); + acceptance_sets->clear(number_of_acceptance_sets); + } + acceptance_stack.push_front(make_pair(scc_id, acceptance_sets)); +merge_sets: + product->operations.mergeAcceptanceInformation + (t.firstComponent(), t.secondComponent(), *acceptance_sets); +} + +/* ========================================================================= */ +template +inline void Product::AcceptanceTracker::addNodeToComponent + (const typename Product::size_type state_id, + const typename Product::size_type scc_id) +/* ---------------------------------------------------------------------------- + * + * Description: Adds the acceptance sets of the product state `state_id' to + * the collection of acceptance sets associated with a + * nontrivial strongly connected component identifier (a dfs + * number of a product state in Tarjan's algorithm). + * + * Arguments: state_id -- Identifier of the product state. + * scc_id -- Identifier of the strongly connected component + * (assumed to be >= 1). + * + * Returns: Nothing. Upon return, `this->acceptance_sets' either points + * to the acceptance sets associated with the topmost element of + * `this->acceptance_sets', or, if the component is a + * trivial strongly connected component, + * `this->acceptance_sets == 0'. + * + * ------------------------------------------------------------------------- */ +{ + /* + * When this function gets called, then depth-first search guarantees that + * the strongly connected component identifier of the topmost element (if + * such an element exists) of `this->acceptance_stack' is <= 'scc_id'. + * Furthermore, the strongly connected is nontrivial only if equality holds + * in the above test. + */ + + if (acceptance_stack.front().first < scc_id) + { + acceptance_sets = 0; + return; + } + + acceptance_sets = acceptance_stack.front().second; + product->operations.mergeAcceptanceInformation + (product->firstComponent(state_id), product->secondComponent(state_id), + *acceptance_sets); +} + +/* ========================================================================= */ +template +inline void Product::AcceptanceTracker::endComponent + (const typename Product::size_type scc_id) +/* ---------------------------------------------------------------------------- + * + * Description: Removes the association between a nontrivial strongly + * connected component identifier and a collection of acceptance + * sets when the component is not needed any longer. (This + * function gets called after extracting a maximal strongly + * connected component from the product. It is safe to remove + * the association at this point, because the search will not + * enter the component afterwards, nor can any state visited + * in the future belong to the strongly connected component + * identified by `scc_id'.) + * + * Argument: scc_id -- Identifier of the strongly connected component. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ + /* + * Because the depth-first search made a call to `addNodeToComponent' before + * extracting the component from the product, the topmost element (if any) + * of `this->acceptance_stack' is guaranteed to have scc id <= `scc_id' at + * this point. + */ + + if (acceptance_stack.front().first == scc_id) + { + delete acceptance_stack.front().second; + acceptance_stack.pop_front(); + } +} + + + +/****************************************************************************** + * + * Inline function definitions for template class + * Product::SimpleEmptinessChecker. + * + *****************************************************************************/ + +/* ========================================================================= */ +template +inline Product::SimpleEmptinessChecker::SimpleEmptinessChecker + (const unsigned long int num_accept_sets) + : AcceptanceTracker(num_accept_sets), dummy(0) +/* ---------------------------------------------------------------------------- + * + * Description: Constructor for class + * Product::SimpleEmptinessChecker. + * + * Arguments: num_accept_sets -- Number of acceptance sets in the + * product. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +template +inline Product::SimpleEmptinessChecker::~SimpleEmptinessChecker() +/* ---------------------------------------------------------------------------- + * + * Description: Destructor for class + * Product::SimpleEmptinessChecker. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +template +inline const typename Product::SimpleEmptinessChecker::SccType& +Product::SimpleEmptinessChecker::operator()() const +/* ---------------------------------------------------------------------------- + * + * Description: Dummy function required for supporting the expected class + * interface. + * + * Arguments: None. + * + * Returns: A constant reference to `this->dummy'. + * + * ------------------------------------------------------------------------- */ +{ + return dummy; +} + +/* ========================================================================= */ +template +inline void Product::SimpleEmptinessChecker::addEdgeToComponent + (const typename Product::Edge& t, + const typename Product::size_type scc_id) +/* ---------------------------------------------------------------------------- + * + * Description: Adds a transition to a nontrivial strongly connected product + * component and aborts the search if the addition of the + * transition in the component makes the component accepting. + * + * Arguments: t -- A constant reference to the product transition to + * be added to the component. + * scc_id -- Identifier of the strongly connected component. + * + * Returns: Nothing; aborts the search by throwing the constant 0 if the + * addition of the transition in the component makes the + * component accepting. + * + * ------------------------------------------------------------------------- */ +{ + AcceptanceTracker::addEdgeToComponent(t, scc_id); + /* `this->acceptance_sets' points to the acceptance sets associated with + * the nontrivial SCC `scc_id' at this point. */ + abortIfNonempty(); +} + +/* ========================================================================= */ +template +inline void Product::SimpleEmptinessChecker::addNodeToComponent + (const typename Product::size_type state, + const typename Product::size_type scc_id) +/* ---------------------------------------------------------------------------- + * + * Description: Adds a state to a nontrivial strongly connected product + * component and aborts the search if the addition of the state + * in the component makes the component accepting. + * + * Arguments: state -- Identifier of a product state to be added to the + * component. + * scc_id -- Identifier of the strongly connected component. + * + * Returns: Nothing; aborts the search by throwing the constant 0 if the + * addition of the state in the component makes the component + * accepting. + * + * ------------------------------------------------------------------------- */ +{ + AcceptanceTracker::addNodeToComponent(state, scc_id); + /* If `this->acceptance_sets != 0', then `this->acceptance_sets' points to + * the acceptance sets associated with the nontrivial SCC `scc_id'; + * otherwise the component `scc_id' is a trivial SCC. */ + if (this->acceptance_sets != 0) + abortIfNonempty(); +} + +/* ========================================================================= */ +template +inline void Product::SimpleEmptinessChecker::abortIfNonempty() + const +/* ---------------------------------------------------------------------------- + * + * Description: Tests whether the strongly connected component with + * acceptance sets pointed to by `this->acceptance_sets' is an + * accepting component. This holds if all bits in the + * acceptance set bit vector pointed to by + * `this->acceptance_sets' are set to 1. + * + * Arguments: None. + * + * Returns: Nothing; throws the constant 0 if the component with + * acceptance sets pointed to by `this->acceptance_sets' is an + * accepting strongly connected component. + * + * ------------------------------------------------------------------------- */ +{ + if (this->acceptance_sets->count(this->number_of_acceptance_sets) + == this->number_of_acceptance_sets) + throw 0; +} + + + +/****************************************************************************** + * + * Inline function definitions for template class + * Product::AcceptanceReachabilityTracker. + * + *****************************************************************************/ + +/* ========================================================================= */ +template +inline Product::AcceptanceReachabilityTracker + ::AcceptanceReachabilityTracker + (const unsigned long int num_accept_sets) : + AcceptanceTracker(num_accept_sets), number_of_states(0), + number_of_transitions(0), mark_scc(false), dummy(0) +/* ---------------------------------------------------------------------------- + * + * Description: Constructor for class + * Product::AcceptanceReachabilityTracker. + * + * Arguments: num_accept_sets -- Number of acceptance sets in the + * product. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +template +inline Product::AcceptanceReachabilityTracker + ::~AcceptanceReachabilityTracker() +/* ---------------------------------------------------------------------------- + * + * Description: Destructor for class + * Product::AcceptanceReachabilityTracker. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +template +inline +const typename Product::AcceptanceReachabilityTracker::SccType& +Product::AcceptanceReachabilityTracker::operator()() const +/* ---------------------------------------------------------------------------- + * + * Description: Dummy function required for supporting the expected class + * interface. + * + * Arguments: None. + * + * Returns: A constant reference to `this->dummy'. + * + * ------------------------------------------------------------------------- */ +{ + return dummy; +} + +/* ========================================================================= */ +template +inline void Product::AcceptanceReachabilityTracker::enter + (const typename Product::size_type) +/* ---------------------------------------------------------------------------- + * + * Description: Function called when entering a new state in the product. + * Increments the number of product states that have been + * explored. + * + * Arguments: The single argument is required to support the expected class + * interface. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ + ++number_of_states; +} + +/* ========================================================================= */ +template +inline void Product::AcceptanceReachabilityTracker::backtrack + (const typename Product::size_type source, + const typename Product::Edge&, + const typename Product::size_type target) +/* ---------------------------------------------------------------------------- + * + * Description: Function called when backtracking from a state in the + * product. Increments the number of product edges that have + * been explored. Additionally, if the state from which the + * search backtracks belongs to the set of states from which an + * accepting strongly connected component is known to be + * reachable in the product, adds also the state to which the + * search backtracks into this set of states. + * + * Arguments: (source, target) describe the endpoints of the product + * transition along which the backtrack occurs (i.e., `source' + * is the state _to_ which the search backtracks). The second + * argument is only needed to support the expected function call + * interface. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ + ++number_of_transitions; + if (isMarked(target)) + markState(source); +} + +/* ========================================================================= */ +template +inline void Product::AcceptanceReachabilityTracker::touch + (const typename Product::size_type source, + const typename Product::Edge& edge, + const typename Product::size_type target) +/* ---------------------------------------------------------------------------- + * + * Description: Function called when the search encounters an edge with a + * target node that has already been explored. Increments the + * number of explored product transitions and updates accepting + * strongly connected reachability information by calling + * `this->backtrack()'. (This function is needed for supporting + * the expected class interface.) + * + * Arguments: (source, edge, target) describe the product transition that + * "touches" the state `target'. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ + backtrack(source, edge, target); +} + +/* ========================================================================= */ +template +inline void Product::AcceptanceReachabilityTracker::beginComponent + (const typename Product::size_type, + const typename Product::size_type state_id) +/* ---------------------------------------------------------------------------- + * + * Description: Tests whether the maximal strongly connected component that + * is about to be extracted from the product is an accepting + * component, or if the component contains a state from which + * such a component is known to be reachable. If either of + * these properties holds, `this->mark_scc' is set to true to + * cause all states referred to in subsequent calls to + * `this->insert' that occur before the next call to + * `this->endComponent' to be added into the set of states from + * which an accepting strongly connected component in the + * product is known to be reachable. + * + * A component is accepting iff `this->acceptance_sets' points + * to a bit vector in which all bits are set to 1. + * + * Arguments: state_id -- Identifier of a product state (in the + * component) that was encountered first during + * the search. + * The first argument is needed to support the expected function + * interface. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ + if (isMarked(state_id)) /* If the component itself is not accepting, but */ + mark_scc = true; /* it contains a state from which such a component */ + /* is reachable, then the fact that `state_id' is */ + /* the first state of the component encountered */ + /* during the search and the operation of the */ + /* backtrack and touch functions guarantee that */ + /* `isMarked(state_id) == true' holds at this */ + /* point (the search is about to backtrack from */ + /* this state when this function gets called). */ + else /* test whether the component is an accepting component */ + { + /* + * The dfs search guarantees (by having made a call to + * AcceptanceTracker::addNodeToComponent before calling this function) that + * `this->acceptance_sets' is either equal to 0 (in which case the + * component to be extracted is trivial), or it points to the acceptance + * sets associated with the component to be extracted. + */ + mark_scc = (this->acceptance_sets != 0 + && this->acceptance_sets->count + (this->number_of_acceptance_sets) + == this->number_of_acceptance_sets); + } +} + +/* ========================================================================= */ +template +inline void Product::AcceptanceReachabilityTracker::insert + (const typename Product::size_type state) +/* ---------------------------------------------------------------------------- + * + * Description: If `this->mark_scc == true', inserts a product state + * identifier to the set of states from which an accepting + * strongly connected component is known to be reachable in the + * product. Discards the state otherwise. + * + * Argument: state -- Identifier of a product state. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ + if (mark_scc) + markState(state); +} + +/* ========================================================================= */ +template +inline bool Product::AcceptanceReachabilityTracker::isMarked + (const typename Product::size_type state) const +/* ---------------------------------------------------------------------------- + * + * Description: Tells whether an accepting strongly connected component is + * known to be reachable from a state in the product. + * + * Argument: state -- Identifier of the product state to test. + * + * Returns: true iff an accepting strongly connected component is known + * to be reachable from the product state. + * + * ------------------------------------------------------------------------- */ +{ + return (reachability_info.find(state) != reachability_info.end()); +} + +/* ========================================================================= */ +template +inline typename Product::size_type +Product::AcceptanceReachabilityTracker::numberOfStates() const +/* ---------------------------------------------------------------------------- + * + * Description: Tells the number of product states explored during the + * search. + * + * Arguments: None. + * + * Returns: Number of product states explored. + * + * ------------------------------------------------------------------------- */ +{ + return number_of_states; +} + +/* ========================================================================= */ +template +inline unsigned long int +Product::AcceptanceReachabilityTracker::numberOfTransitions() const +/* ---------------------------------------------------------------------------- + * + * Description: Tells the number of product transitions explored during the + * search. + * + * Arguments: None. + * + * Returns: Number of transitions explored. + * + * ------------------------------------------------------------------------- */ +{ + return number_of_transitions; +} + +/* ========================================================================= */ +template +inline void Product::AcceptanceReachabilityTracker::markState + (const typename Product::size_type state) +/* ---------------------------------------------------------------------------- + * + * Description: Adds a product state to the set of states from which an + * accepting strongly connected component is known to be + * reachable in the product. + * + * Argument: state -- Identifier of a product state. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ + reachability_info.insert(state); +} + + + +/****************************************************************************** + * + * Inline function definitions for template class + * Product::AcceptingComponentFinder. + * + *****************************************************************************/ + +/* ========================================================================= */ +template +inline Product::AcceptingComponentFinder::AcceptingComponentFinder + (const unsigned long int num_accept_sets) + : AcceptanceTracker(num_accept_sets), construct_component(false) +/* ---------------------------------------------------------------------------- + * + * Description: Constructor for class + * Product::AcceptingComponentFinder. + * + * Arguments: num_accept_sets -- Number of acceptance sets in the + * product. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +template +inline Product::AcceptingComponentFinder + ::~AcceptingComponentFinder() +/* ---------------------------------------------------------------------------- + * + * Description: Destructor for class + * Product::AcceptingComponentFinder. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +template +inline const typename Product::AcceptingComponentFinder::SccType& +Product::AcceptingComponentFinder::operator()() const +/* ---------------------------------------------------------------------------- + * + * Description: Returns the latest accepting maximal strongly connected + * component found in the product. + * + * Arguments: None. + * + * Returns: A constant reference to a set of states containing the + * identifiers of product states forming an accepting maximal + * strongly connected component in the product. This set is + * empty if no such component has yet been found during the + * emptiness check. + * + * ------------------------------------------------------------------------- */ +{ + return scc; +} + +/* ========================================================================= */ +template +inline void Product::AcceptingComponentFinder::beginComponent + (const typename Product::size_type, + const typename Product::size_type) +/* ---------------------------------------------------------------------------- + * + * Description: Tests whether the maximal strongly connected component that + * is about to be extracted from the product is an accepting + * component. If this is the case, `this->construct_component' + * is set to true to cause all states referred to in subsequent + * calls to `this->insert' that occur before the next call to + * `this->endComponent' to be inserted into `this->scc'. + * + * A component is accepting iff `this->acceptance_sets' points + * to a bit vector in which all bits are set to 1. + * + * Arguments: The arguments are required to support the expected class + * interface. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ + scc.clear(); + /* + * The dfs search guarantees (by having made a call to + * AcceptanceTracker::addNodeToComponent before calling this function) that + * `this->acceptance_sets' is either equal to 0 (in which case the component + * to be extracted is trivial), or it points to the acceptance sets + * associated with the component to be extracted. + */ + construct_component = (this->acceptance_sets != 0 + && this->acceptance_sets->count + (this->number_of_acceptance_sets) + == this->number_of_acceptance_sets); +} + +/* ========================================================================= */ +template +inline void Product::AcceptingComponentFinder::insert + (const typename Product::size_type state) +/* ---------------------------------------------------------------------------- + * + * Description: If `this->construct_component == true', inserts a product + * state identifier to the set of identifiers representing an + * accepting maximal strongly connected component. Discards the + * state otherwise. + * + * Argument: state -- Identifier of a product state. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ + if (construct_component) + scc.insert(state); +} + +} + +#endif /* !PRODUCT_H */ diff --git a/lbtt/src/SccCollection.h b/lbtt/src/SccCollection.h new file mode 100644 index 000000000..ea31ac97f --- /dev/null +++ b/lbtt/src/SccCollection.h @@ -0,0 +1,1174 @@ +/* + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 + * Heikki Tauriainen + * + * This program 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. + * + * This program 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 this program; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. + */ + +#ifndef SCCCOLLECTION_H +#define SCCCOLLECTION_H + +#include +#include +#include +#include +#include +#include +#include "EdgeContainer.h" +#include "LbttAlloc.h" +#include "Graph.h" + +using namespace std; + +namespace Graph +{ + +/****************************************************************************** + * + * Interface for a "node visitor" object that provides implementations of + * callback functions to be used during a depth-first search for strongly + * connected components. The VisitorInterface class provides empty + * implementations for the operations; visitor objects can be defined by making + * them inherit the VisitorInterface and then overriding some (or all) of the + * interface functions. + * + * A "node visitor" object must always implement the following type definition + * and operation: + * + * SccType + * A type definition for storing data associated with a maximal strongly + * connected component. This data type should support copying and + * assignment; no other assumptions are made about the internals of this + * data type. It is intended that a node visitor object has a member of + * type SccType (which need not be public); this member can then be + * manipulated freely during the search for strongly connected + * components by giving implementations for the other interface + * functions listed below. + * + * const SccType& operator()() + * Function for accessing the data associated with a maximal strongly + * connected component. This function is called when dereferencing a + * strongly connected component iterator (see below). + * + * In addition, a node visitor can overload the default (empty) implementations + * for the following operations: + * + * void enter(typename GraphType::size_type node_id) + * This function is called whenever the search enters a new node of the + * graph, using the identifier of the node as a parameter. + * + * void backtrack + * (typename GraphType::size_type source_id, + * const typename GraphType::Edge& edge, + * typename GraphType::size_type target_id) + * This function is called when the search backtracks from a node with + * the identifier `target_id' to the node `source_id'. `edge' is a + * reference to the edge between graph nodes identified by `source_id' + * and `target_id'. + * + * void touch + * (typename GraphType::size_type source_id, + * const typename GraphType::Edge& edge, + * typename GraphType::size_type target_id) + * This function is called when the search (in node `source_id') + * encounters an edge (`edge') with a target node (with identifier + * `target_id') that has already been visited during the search. + * + * void leave(typename GraphType::size_type node_id) + * This function is called when the search leaves a node with the + * identifier `node_id'. + * + * void addEdgeToComponent + * (const typename GraphType::Edge& edge, + * typename GraphType::size_type component_id) + * This function is called when the search finds an edge belonging to a + * strongly connected component of the graph (i.e., an edge between two + * states in the component). The function is called with a constant + * reference to the edge and a strongly connected component identifier + * as parameters. + * + * void addNodeToComponent + * (typename GraphType::size_type node_id, + * typename GraphType::size_type component_id) + * This function is called when the search finds a state belonging to a + * strongly connected component of the graph. + * + * void beginComponent + * (typename GraphType::size_type component_id, + * typename GraphType::size_type component_root_id) + * This function is called when the SCC algorithm is about to extract a + * new maximal strongly connected component from the graph. Here, + * `component_id' corresponds to the identifier of the component, and + * `component_root_id' is the identifier of the node in the component + * which was first encountered during the search (the depth-first search + * is about to backtrack from this node). + * + * void insert(typename GraphType::size_type node_id) + * After a call to `beginComponent', the SCC search algorithm will call + * `insert' for each identifier of a node in the maximal strongly + * connected component. + * + * void endComponent(typename GraphType::size_type component_id) + * This function is called after the SCC algorithm has finished + * `insert''ing nodes into a maximal strongly connected component. The + * component identifier is given as a parameter. + * + *****************************************************************************/ + +template +class VisitorInterface +{ +public: + VisitorInterface(); /* Constructor. */ + + /* default copy constructor */ + + virtual ~VisitorInterface(); /* Destructor. */ + + /* default assignment operator */ + + virtual void enter /* Interface operations. */ + (const typename GraphType::size_type); + + virtual void backtrack + (const typename GraphType::size_type, + const typename GraphType::Edge&, + const typename GraphType::size_type); + + virtual void touch + (const typename GraphType::size_type, + const typename GraphType::Edge&, + const typename GraphType::size_type); + + virtual void leave + (const typename GraphType::size_type); + + virtual void addEdgeToComponent + (const typename GraphType::Edge&, + const typename GraphType::size_type); + + virtual void addNodeToComponent + (const typename GraphType::size_type, + const typename GraphType::size_type); + + virtual void beginComponent + (const typename GraphType::size_type, + const typename GraphType::size_type); + + virtual void insert + (const typename GraphType::size_type); + + virtual void endComponent + (const typename GraphType::size_type); +}; + + + +/****************************************************************************** + * + * A template class defining a node visitor for collecting the identifiers of + * nodes in a maximal strongly connected component into a set. + * + *****************************************************************************/ + +template +class SccCollector : public VisitorInterface +{ +public: + SccCollector(); /* Constructor. */ + + /* default copy constructor */ + + ~SccCollector(); /* Destructor. */ + + /* default assignment operator */ + + typedef set, /* a set of node id's. */ + ALLOC(typename GraphType::size_type) > + SccType; + + const SccType& operator()() const; /* Returns the set of node + * identifiers in a + * maximal strongly + * connected component. + */ + + /* `enter' inherited */ + + /* `backtrack' inherited */ + + /* `touch' inherited */ + + /* `leave' inherited */ + + /* `addEdgeToComponent' inherited */ + + /* `addNodeToComponent' inherited */ + + void beginComponent /* Function called */ + (const typename GraphType::size_type, /* before inserting */ + const typename GraphType::size_type); /* nodes in a component. */ + + void insert /* Function for */ + (const typename GraphType::size_type node_id); /* inserting nodes into + * a component. + */ + + /* `endComponent' inherited */ + +private: + SccType scc; /* A set of node + * identifiers representing + * a maximal strongly + * connected component. + */ +}; + + + +/****************************************************************************** + * + * A template class for defining a "container" of maximal strongly connected + * components of a graph. The template should be instantiated with two classes + * GraphType and NodeVisitor, where the NodeVisitor type should support the + * interface required of a node visitor (see the above documentation of + * VisitorInterface), and GraphType (which defaults to + * Graph) should support the following type definitions and + * operations: + * + * size_type + * A type that can be used for identifying nodes (uniquely) in the + * graph. This type should have a constructor taking no parameters, + * and it should support copying, assignment, and comparison using the + * `less than' operator. + * + * EdgeContainerType + * A type that represents a container of objects behaving similarly to + * pointers to edges in the graph. This type is expected to have an + * STL-like container interface with `begin()' and `end()' operations + * and a const_iterator with a constructor having no parameters and + * copying and assignment operations. + * + * The objects in the container should behave similarly to pointers + * that can be dereferenced using the * and -> operators to get access + * to objects (the edges in the graph, e.g., + * Graph::Edge) that support the operation + * size_type targetNode() + * that returns the identifier of an edge's target node in the graph. + * + * PathElement + * An object for representing (node_id, edge) pairs of the graph. + * The object should provide a constructor that can be called with two + * parameters: a parameter of type `size_type' and another parameter + * corresponding to the type obtained by dereferencing a pointer-like + * object stored in an object of type EdgeContainerType. + * + * Path + * A type that supports the `clear' operation (with no arguments) and + * the `push_front' operation with an argument of type PathElement. + * + * operator[](size_type node_id) + * This function should return an object that provides access to the + * edges starting from the graph node identified by `node_id' through + * the member function + * const EdgeContainerType& edges(), + * which returns the collection of (pointer-like objects to) edges + * beginning from the graph node with the identifier `node_id'. + * + * bool empty() + * This function should return true iff the graph contains no nodes. + * + * The NodeVisitor type defaults to SccCollector. + * + * The SccCollection class provides the following operations: + * + * SccCollection(const GraphType& g, NodeVisitor& node_visitor) + * Constructor that binds the SccCollection object to the graph `g' + * using the operations defined by `node_visitor' when visiting nodes + * of the graph during the search for strongly connected components. + * + * iterator begin(const typename GraphType::size_type initial_node_id) + * Returns an iterator to the strongly connected components of the + * graph. The function returns an iterator that points to the "first" + * maximal strongly connected component of the graph when starting the + * search for maximal strongly connected components from the node with + * the identifier `initial_node_id'. + * + * Note: If `initial_node_id' belongs to a strongly connected component + * of the graph which has alredy been visited by an iterator obtained + * by a previous call to `begin', the returned iterator is equal to + * `end()'. If this is not desired (i.e., if you wish to repeat the + * search for strongly connected components in a part of the graph, + * initialize a new SccCollection to the graph). + * + * iterator end() + * Returns an iterator pointing "past the end" of the collection of + * strongly connected components. + * + * The class `SccCollection::iterator' provides standard dereferencing and + * prefix and postfix increment operators. It also supports comparison for + * equality and inequality. See below for more detailed information. + * + *****************************************************************************/ + +template , + class NodeVisitor = SccCollector > +class SccCollection +{ +public: + SccCollection /* Constructor. */ + (const GraphType& g, + NodeVisitor& node_visitor); + + ~SccCollection(); /* Destructor. */ + + /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ + + typedef map, /* identifiers and the */ + ALLOC(typename GraphType::size_type) >/* order in which they */ + DfsOrdering; /* were encountered in + * the search for + * strongly connected + * components. + */ + + /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ + + class iterator /* Iterator for */ + { /* accessing the maximal + * strongly connected + * components. + */ + public: + iterator(); /* Default constructor. */ + + /* default copy constructor */ + + ~iterator(); /* Destructor. */ + + /* default assignment operator */ + + bool operator==(const iterator& it) const; /* Comparison functions. */ + bool operator!=(const iterator& it) const; + + const typename NodeVisitor::SccType& /* Dereferencing */ + operator*() const; /* operators. */ + const typename NodeVisitor::SccType* + operator->() const; + + const typename NodeVisitor::SccType& /* Prefix and postfix */ + operator++(); /* increment operators. */ + const typename NodeVisitor::SccType + operator++(int); + + void getPath(typename GraphType::Path& path); /* Function for accessing + * the path from the + * initial node of the + * search to a node in + * the most recently found + * strongly connected + * component. + */ + + private: + iterator /* Constructor. */ + (const GraphType& g, + NodeVisitor& node_visitor, + DfsOrdering& ordering); + + void initialize /* Instructs the */ + (const typename GraphType::size_type /* iterator to continue */ + node_id); /* the search for + * strongly connected + * components from a + * given node. + */ + + const GraphType& graph; /* Reference to the graph + * with which the iterator + * is associated. + */ + + NodeVisitor& visitor; /* Reference to an object + * that provides + * implementations for the + * functions listed in the + * VisitorInterface class. + */ + + DfsOrdering& dfs_ordering; /* Mapping between node + * identifiers and their + * dfs numbers. + */ + + typename GraphType::size_type initial_node; /* Node from which the + * search was started. + */ + + typename GraphType::size_type dfs_number; /* Number of graph nodes + * processed by the + * iterator. + */ + + struct NodeStackElement /* Structure for */ + { /* storing information */ + typename GraphType::size_type id; /* needed for */ + typename GraphType::EdgeContainerType /* backtracking during */ + ::const_iterator edge; /* the search. */ + typename GraphType::size_type lowlink; + }; + + deque /* backtracking stack. */ + node_stack; + + NodeStackElement* current_node; /* Pointer to the top + * element of the + * backtracking stack. + */ + + deque /* collecting the nodes */ + scc_stack; /* in a strongly + * connected component, + * excluding the root + * nodes of the + * components. + */ + + void computeNextScc(); /* Updates the iterator to + * point to the next + * strongly connected + * component. + */ + + friend class SccCollection; + }; + + /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ + + iterator begin /* Returns an iterator */ + (const typename GraphType::size_type /* pointing to the */ + node_id); /* "first" maximal + * strongly connected + * component reachable + * from a given node. + */ + + const iterator& end() const; /* Returns an iterator + * pointing past the "end" + * of the maximal strongly + * connected components. + */ + +private: + SccCollection(const SccCollection&); /* Prevent copying and */ + SccCollection& operator=(const SccCollection&); /* assignment of + * SccCollection + * objects. + */ + + const GraphType& graph; /* Reference to the graph + * associated with the + * container. + */ + + NodeVisitor& visitor; /* Reference to an object + * that provides + * implementations for + * callback operations + * needed during the + * search for strongly + * connected components. + */ + + const iterator end_iterator; /* Iterator pointing past + * the "end" of the + * collection of strongly + * connected components in + * the graph. This + * iterator is special by + * having both + * `initial_node' and + * `dfs_number' set to 0. + */ + + DfsOrdering dfs_ordering; /* Mapping between node + * identifiers and their + * visiting order during + * the search for strongly + * connected components. + */ +}; + + + +/****************************************************************************** + * + * Inline function definitions for template class VisitorInterface. This class + * provides default empty implementations for node visitor operations. + * + *****************************************************************************/ + +template +inline VisitorInterface::VisitorInterface() +{ +} + +template +inline VisitorInterface::~VisitorInterface() +{ +} + +template +inline void VisitorInterface::enter + (const typename GraphType::size_type) +{ +} + +template +inline void VisitorInterface::backtrack + (const typename GraphType::size_type, const typename GraphType::Edge&, + const typename GraphType::size_type) +{ +} + +template +inline void VisitorInterface::touch + (const typename GraphType::size_type, const typename GraphType::Edge&, + const typename GraphType::size_type) +{ +} + +template +inline void VisitorInterface::leave + (const typename GraphType::size_type) +{ +} + +template +inline void VisitorInterface::addEdgeToComponent + (const typename GraphType::Edge&, const typename GraphType::size_type) +{ +} + +template +inline void VisitorInterface::addNodeToComponent + (const typename GraphType::size_type, const typename GraphType::size_type) +{ +} + +template +inline void VisitorInterface::beginComponent + (const typename GraphType::size_type, const typename GraphType::size_type) +{ +} + +template +inline void VisitorInterface::insert + (const typename GraphType::size_type) +{ +} + +template +inline void VisitorInterface::endComponent + (const typename GraphType::size_type) +{ +} + + + +/****************************************************************************** + * + * Inline function definitions for template class SccCollector. + * + *****************************************************************************/ + +/* ========================================================================= */ +template +inline SccCollector::SccCollector() +/* ---------------------------------------------------------------------------- + * + * Description: Constructor for class SccCollector. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +template +inline SccCollector::~SccCollector() +/* ---------------------------------------------------------------------------- + * + * Description: Destructor for class SccCollector. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +template +inline const typename SccCollector::SccType& +SccCollector::operator()() const +/* ---------------------------------------------------------------------------- + * + * Description: Returns the set of identifiers of nodes in the maximal + * strongly connected component. + * + * Arguments: None. + * + * Returns: A constant reference to the set of identifiers of nodes in + * the component. + * + * ------------------------------------------------------------------------- */ +{ + return scc; +} + +/* ========================================================================= */ +template +inline void SccCollector::beginComponent + (const typename GraphType::size_type, const typename GraphType::size_type) +/* ---------------------------------------------------------------------------- + * + * Description: Clears the set of node identifiers to make it empty before + * filling it with (identifiers of) nodes of a new maximal + * strongly connected component. + * + * Arguments: The arguments are needed to support the expected function + * calling interface. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ + scc.clear(); +} + +/* ========================================================================= */ +template +inline void SccCollector::insert + (const typename GraphType::size_type node_id) +/* ---------------------------------------------------------------------------- + * + * Description: Inserts an identifier into the set of node identifiers in a + * maximal strongly connected component. + * + * Arguments: node_id -- Node identifier. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ + scc.insert(node_id); +} + + + +/****************************************************************************** + * + * Inline function definitions for template class SccCollection. + * + *****************************************************************************/ + +/* ========================================================================= */ +template +inline SccCollection::SccCollection + (const GraphType& g, NodeVisitor& node_visitor) : + graph(g), visitor(node_visitor), end_iterator(g, node_visitor, dfs_ordering) +/* ---------------------------------------------------------------------------- + * + * Description: Constructor for class SccCollection. + * + * Arguments: g -- A constant reference to an object of type + * GraphType. See above for the description + * of the interface that this object should + * support. + * node_visitor -- A reference to an object that provides + * node visiting operations. See the + * documentation of VisitorInterface for more + * information. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +template +inline SccCollection::~SccCollection() +/* ---------------------------------------------------------------------------- + * + * Description: Destructor for class SccCollection. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +template +inline typename SccCollection::iterator +SccCollection::begin + (const typename GraphType::size_type node_id) +/* ---------------------------------------------------------------------------- + * + * Description: Returns an iterator pointing to the "first" strongly + * connected component reachable from a given node of + * `this->graph'. + * + * Argument: node_id -- Identifier of the node. + * + * Returns: An iterator pointing to the "first" strongly connected + * component reachable from the node, or an iterator equal to + * `this->end()' if the node with the identifier `node_id' has + * already been included in a strongly connected component + * returned by another iterator to the same collection of + * strongly connected components. + * + * ------------------------------------------------------------------------- */ +{ + iterator it(graph, visitor, dfs_ordering); + it.initialize(node_id); + return it; +} + +/* ========================================================================= */ +template +inline const typename SccCollection::iterator& +SccCollection::end() const +/* ---------------------------------------------------------------------------- + * + * Description: Returns an iterator pointing past the "end" of the collection + * of strongly connected components in `this->graph'. + * + * Arguments: None. + * + * Returns: A constant reference to `this->end_iterator'. + * + * ------------------------------------------------------------------------- */ +{ + return end_iterator; +} + + + +/****************************************************************************** + * + * Inline function definitions for template class SccCollection::iterator. + * + *****************************************************************************/ + +/* ========================================================================= */ +template +inline SccCollection::iterator::iterator + (const GraphType& g, NodeVisitor& node_visitor, + SccCollection::DfsOrdering& ordering) : + graph(g), visitor(node_visitor), dfs_ordering(ordering), initial_node(0), + dfs_number(0) +/* ---------------------------------------------------------------------------- + * + * Description: Constructor for class + * SccCollection::iterator. Initializes + * a new iterator for scanning the maximal strongly connected + * components of a graph. + * + * Arguments: g -- The graph with which the iterator is to be + * associated. + * node_visitor -- A reference to a object that implements + * callback functions to be invoked during the + * search for strongly connected components. + * ordering -- A reference to a mapping between node + * identifiers and their dfs numbers. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +template +inline SccCollection::iterator::~iterator() +/* ---------------------------------------------------------------------------- + * + * Description: Destructor for class + * SccCollection::iterator. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +template +inline bool SccCollection::iterator::operator== + (const SccCollection::iterator& it) const +/* ---------------------------------------------------------------------------- + * + * Description: Equality comparison between two SccCollection::iterators. Two + * iterators are equal iff they have the same initial state and + * they have visited the same amount of graph nodes. + * + * Argument: it -- A constant reference to an iterator. + * + * Returns: true iff the iterators are equal. + * + * ------------------------------------------------------------------------- */ +{ + return (it.initial_node == initial_node && it.dfs_number == dfs_number); +} + +/* ========================================================================= */ +template +inline bool SccCollection::iterator::operator!= + (const SccCollection::iterator& it) const +/* ---------------------------------------------------------------------------- + * + * Description: Inequality comparison between two SccCollection::iterators. + * Two iterators are not equal iff they have different initial + * states or if they have visited different numbers of graph + * nodes. + * + * Argument: it -- A constant reference to an iterator. + * + * Returns: true iff the iterators are not equal. + * + * ------------------------------------------------------------------------- */ +{ + return (it.initial_node != initial_node || it.dfs_number != dfs_number); +} + +/* ========================================================================= */ +template +inline const typename NodeVisitor::SccType& +SccCollection::iterator::operator*() const +/* ---------------------------------------------------------------------------- + * + * Description: Dereferencing operator for class + * SccCollection::iterator. Returns the + * data associated with the maximal strongly connected component + * currently pointed to by the iterator. + * + * Arguments: None. + * + * Returns: A constant reference to the data associated with the strongly + * connected component. + * + * ------------------------------------------------------------------------- */ +{ + return visitor(); +} + +/* ========================================================================= */ +template +inline const typename NodeVisitor::SccType* +SccCollection::iterator::operator->() const +/* ---------------------------------------------------------------------------- + * + * Description: Dereferencing operator for class + * SccCollection::iterator. Returns a + * pointer to the data associated with the maximal strongly + * connected component currently pointed to by the iterator. + * + * Arguments: None. + * + * Returns: A constant pointer to the data associated with the strongly + * connected component. + * + * ------------------------------------------------------------------------- */ +{ + return &visitor(); +} + +/* ========================================================================= */ +template +inline const typename NodeVisitor::SccType& +SccCollection::iterator::operator++() +/* ---------------------------------------------------------------------------- + * + * Description: Prefix increment operator for class + * SccCollection::iterator. Computes + * the next maximal strongly connected component of + * `this->graph' and then returns the data associated with it. + * + * Arguments: None. + * + * Returns: A reference to the data associated with the maximal strongly + * connected component found by incrementing the iterator. + * + * ------------------------------------------------------------------------- */ +{ + computeNextScc(); + return visitor(); +} + +/* ========================================================================= */ +template +inline const typename NodeVisitor::SccType +SccCollection::iterator::operator++(int) +/* ---------------------------------------------------------------------------- + * + * Description: Postfix increment operator for class + * SccCollection::iterator. Computes + * the next strongly connected component of + * `this->graph', but returns the data associated with the + * strongly connected component that the iterator pointed to + * _before_ this operation. + * + * Arguments: None (the `int' is only required to distinguish this operator + * from the prefix increment operator). + * + * Returns: The data associated with the maximal strongly connected + * component pointed to by the iterator before incrementing it. + * + * ------------------------------------------------------------------------- */ +{ + const typename NodeVisitor::SccType old_scc = visitor(); + computeNextScc(); + return old_scc; +} + + + +/****************************************************************************** + * + * Function definitions for template class + * SccCollection. + * + *****************************************************************************/ + +/* ========================================================================= */ +template +void SccCollection::iterator::getPath + (typename GraphType::Path& path) +/* ---------------------------------------------------------------------------- + * + * Description: Constructs a path from the initial state of the search for + * the strongly connected components to a node in the most + * recently found maximal strongly connected graph component. + * + * Argument: path -- A reference to a GraphType::Path object for storing + * the (node_id, edge) pairs in the path. + * + * Returns: Nothing. Assuming that `path' is a standard STL container + * type object with the `push_front' operation, `*path.begin()' + * will correspond to the first element on the path after the + * call. + * + * ------------------------------------------------------------------------- */ +{ + path.clear(); + + /* + * When this function is called after extracting a maximal strongly connected + * component from the graph, `node_stack.front()' corresponds to the root + * node of the component. This node will not be included in the path + * (that is, the edge component of `path.back()' will point to this node + * when exiting from this function). + */ + + typename deque::const_iterator + n = node_stack.begin(); + if (n != node_stack.end()) + { + for (++n; n != node_stack.end(); ++n) + { + const typename GraphType::PathElement element(n->id, **n->edge); + path.push_front(element); + } + } +} + +/* ========================================================================= */ +template +void SccCollection::iterator::initialize + (const typename GraphType::size_type node_id) +/* ---------------------------------------------------------------------------- + * + * Description: Initializes a + * SccCollection::iterator for scanning + * the maximal strongly connected components of `this->graph'. + * + * Argument: node_id -- Identifier of a graph node from which to start + * the search for maximal strongly connected + * components. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ + node_stack.clear(); + scc_stack.clear(); + + /* + * If `node_id' is an identifier of a node that has not yet been visited, + * make the iterator point to the next strongly connected component of + * `this->graph'. + */ + + if (!graph.empty() && dfs_ordering.find(node_id) == dfs_ordering.end()) + { + initial_node = node_id; + visitor.enter(node_id); + dfs_ordering[node_id] = dfs_number = 1; + const NodeStackElement element + = { node_id, graph[node_id].edges().begin(), 1 }; + node_stack.push_front(element); + current_node = &node_stack.front(); + computeNextScc(); + } +} + +/* ========================================================================= */ +template +void SccCollection::iterator::computeNextScc() +/* ---------------------------------------------------------------------------- + * + * Description: Makes an SccCollection::iterator + * point to the "next" maximal strongly connected component of + * `this->graph', using an algorithm based on the depth-first + * search algorithm of Tarjan + * [R. J. Tarjan. Depth-first search and linear graph + * algorithms. SIAM Journal on Computing 1(2):146--160, + * 1972] + * for computing the maximal strongly connected components of + * the graph. + * + * The implementation includes the optimization in the first + * improved algorithm found in + * [E. Nuutila and E. Soisalon-Soininen. On finding the + * strongly connected components in a directed graph. + * Information Processing Letters 49(1):9--14, 1994]. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ + if (current_node->lowlink == 0) + { + /* Backtrack from the root of an SCC that was extracted from the graph */ + const typename GraphType::size_type child_node = current_node->id; + node_stack.pop_front(); + if (node_stack.empty()) + { + initial_node = dfs_number = 0; + return; + } + current_node = &node_stack.front(); + visitor.backtrack(current_node->id, **current_node->edge, child_node); + ++current_node->edge; /* prepare to process the next edge */ + } + +next_edge: + while (current_node->edge != graph[current_node->id].edges().end()) + { + const typename GraphType::size_type child_node + = (*current_node->edge)->targetNode(); + const typename DfsOrdering::const_iterator child_dfs_number_finder + = dfs_ordering.find(child_node); + + if (child_dfs_number_finder == dfs_ordering.end()) /* child not visited */ + { + ++dfs_number; + dfs_ordering[child_node] = dfs_number; + visitor.enter(child_node); + const NodeStackElement element + = { child_node, graph[child_node].edges().begin(), dfs_number }; + node_stack.push_front(element); + current_node = &node_stack.front(); + goto next_edge; + } + + visitor.touch(current_node->id, **current_node->edge, child_node); + if (child_dfs_number_finder->second != 0) /* child in the same SCC */ + { + if (child_dfs_number_finder->second < current_node->lowlink) + current_node->lowlink = child_dfs_number_finder->second; + visitor.addEdgeToComponent(**current_node->edge, current_node->lowlink); + } + + ++current_node->edge; + } + + visitor.addNodeToComponent(current_node->id, current_node->lowlink); + visitor.leave(current_node->id); + + if (dfs_ordering.find(current_node->id)->second != current_node->lowlink) + { + scc_stack.push_front(current_node->id); + + /* Backtrack from a node into a node in the same SCC */ + const typename GraphType::size_type child_node = current_node->id; + const typename GraphType::size_type child_lowlink = current_node->lowlink; + node_stack.pop_front(); + current_node = &node_stack.front(); + if (current_node->lowlink > child_lowlink) + current_node->lowlink = child_lowlink; + visitor.backtrack(current_node->id, **current_node->edge, child_node); + visitor.addEdgeToComponent(**current_node->edge, current_node->lowlink); + ++current_node->edge; /* prepare to process the next edge */ + goto next_edge; + } + + /* + * `current_node' is a root of a maximal strongly connected graph component. + * Extract the component from the graph. + */ + + visitor.beginComponent(current_node->lowlink, current_node->id); + visitor.insert(current_node->id); + dfs_ordering.find(current_node->id)->second = 0; + while (!scc_stack.empty()) + { + const typename GraphType::size_type node = scc_stack.front(); + typename GraphType::size_type& node_dfs_number + = dfs_ordering.find(node)->second; + if (node_dfs_number > current_node->lowlink) + { + scc_stack.pop_front(); + visitor.insert(node); + node_dfs_number = 0; + } + else + break; + } + visitor.endComponent(current_node->lowlink); + current_node->lowlink = 0; +} + +} + +#endif /* !SCCCOLLECTION_H */ diff --git a/lbtt/src/StateSpaceProduct.h b/lbtt/src/StateSpaceProduct.h new file mode 100644 index 000000000..87fab2fbd --- /dev/null +++ b/lbtt/src/StateSpaceProduct.h @@ -0,0 +1,430 @@ +/* + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 + * Heikki Tauriainen + * + * This program 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. + * + * This program 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 this program; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. + */ + +#ifndef STATESPACEPRODUCT_H +#define STATESPACEPRODUCT_H + +#include +#include "BitArray.h" +#include "BuchiAutomaton.h" +#include "EdgeContainer.h" +#include "Graph.h" +#include "StateSpace.h" + +using namespace std; + +namespace Graph +{ + +/****************************************************************************** + * + * A class with operations for checking the product of a Büchi automaton and + * a state space for emptiness. + * + *****************************************************************************/ + +class StateSpaceProduct +{ +public: + StateSpaceProduct /* Constructor. */ + (const Graph& a, + const Graph& s); + + /* default copy constructor */ + + ~StateSpaceProduct(); /* Destructor. */ + + /* default assignment operator */ + + bool empty() const; /* Tells whether the + * product of a Büchi + * automaton and a state + * space is (trivially) + * empty. + */ + + unsigned long int numberOfAcceptanceSets() const; /* Tells the number of + * acceptance sets in a + * Büchi automaton in its + * product with a state + * space. + */ + + const BuchiAutomaton::BuchiState& firstComponent /* Mappings between a */ + (const Graph::size_type /* product state */ + state_id) const; /* identifier and */ + const StateSpace::State& secondComponent /* states of the Büchi */ + (const Graph::size_type /* automaton and the */ + state_id) const; /* state space forming + * the product. + */ + + void mergeAcceptanceInformation /* Merges the acceptance */ + (const Graph::Node& state, /* sets associated with */ + const Graph::Node&, /* a state in the Büchi */ + BitArray& acceptance_sets) const; /* automaton into a + * collection of sets. + */ + + void mergeAcceptanceInformation /* Merges the acceptance */ + (const Graph::Edge& /* sets associated with */ + buchi_transition, /* a transition in the */ + const Graph::Edge&, /* Büchi automaton into */ + BitArray& acceptance_sets) const; /* a collection of sets. */ + + void validateEdgeIterators /* Ensures that a pair */ + (const Graph::Node& /* of transition */ + buchi_state, /* iterators points to a */ + const Graph::Node& /* transition beginning */ + system_state, /* from a given state in */ + GraphEdgeContainer::const_iterator& /* the product of a */ + buchi_transition, /* Büchi automaton and */ + GraphEdgeContainer::const_iterator& /* a state space. */ + system_transition) const; + + void incrementEdgeIterators /* Updates a pair of */ + (const Graph::Node& /* transition iterators */ + buchi_state, /* to make them point to */ + const Graph::Node& /* the "next" transition */ + system_state, /* starting from a given */ + GraphEdgeContainer::const_iterator& /* state in the product */ + buchi_transition, /* of a Büchi automaton */ + GraphEdgeContainer::const_iterator& /* and a state space. */ + system_transition) const; + +private: + const BuchiAutomaton& buchi_automaton; /* Büchi automaton + * associated with the + * product. + */ + + const StateSpace& statespace; /* State space associated + * with the product. + */ +}; + + + +/****************************************************************************** + * + * Inline function definitions for class StateSpaceProduct. + * + *****************************************************************************/ + +/* ========================================================================= */ +inline StateSpaceProduct::StateSpaceProduct + (const Graph& a, const Graph& s) : + buchi_automaton(static_cast(a)), + statespace(static_cast(s)) +/* ---------------------------------------------------------------------------- + * + * Description: Constructor for class StateSpaceProduct. Initializes a new + * object with operations for checking the emptiness of the + * product of a Büchi automaton and a state space. + * + * Arguments: a -- A constant reference to a Graph + * object, assumed to be a BuchiAutomaton. + * s -- A constant reference to a Graph + * object, assumed to be a StateSpace. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +inline StateSpaceProduct::~StateSpaceProduct() +/* ---------------------------------------------------------------------------- + * + * Description: Destructor for class StateSpaceProduct. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +inline bool StateSpaceProduct::empty() const +/* ---------------------------------------------------------------------------- + * + * Description: Tells whether the product of `this->buchi_automaton' and + * `this->statespace' is (trivially) empty. + * + * Arguments: None. + * + * Returns: true iff either the Büchi automaton or the state space has + * no states. + * + * ------------------------------------------------------------------------- */ +{ + return (buchi_automaton.empty() || statespace.empty()); +} + +/* ========================================================================= */ +inline unsigned long int StateSpaceProduct::numberOfAcceptanceSets() const +/* ---------------------------------------------------------------------------- + * + * Description: Tells the number of acceptance sets in the Büchi automaton + * associated with a StateSpaceProduct object. + * + * Arguments: None. + * + * Returns: The number of acceptance sets in the automaton. + * + * ------------------------------------------------------------------------- */ +{ + return buchi_automaton.numberOfAcceptanceSets(); +} + +/* ========================================================================= */ +inline const BuchiAutomaton::BuchiState& StateSpaceProduct::firstComponent + (const Graph::size_type state_id) const +/* ---------------------------------------------------------------------------- + * + * Description: Function for accessing states in the Büchi automaton + * associated with a StateSpaceProduct object. + * + * Argument: state_id -- Identifier of a state in the automaton. + * + * Returns: A constant reference to a state in the automaton. + * + * ------------------------------------------------------------------------- */ +{ + return buchi_automaton[state_id]; +} + +/* ========================================================================= */ +inline const StateSpace::State& StateSpaceProduct::secondComponent + (const Graph::size_type state_id) const +/* ---------------------------------------------------------------------------- + * + * Description: Function for accessing states in the state space associated + * with a StateSpaceProduct object. + * + * Argument: state_id -- Identifier of a state in the state space. + * + * Returns: A constant reference to a state in the state space. + * + * ------------------------------------------------------------------------- */ +{ + return statespace[state_id]; +} + +/* ========================================================================= */ +inline void StateSpaceProduct::mergeAcceptanceInformation + (const Graph::Node& state, + const Graph::Node&, BitArray& acceptance_sets) const +/* ---------------------------------------------------------------------------- + * + * Description: Merges the acceptance sets associated with a state of a Büchi + * automaton into a collection of sets. + * + * Arguments: state -- A constant reference to a state in the + * automaton. + * acceptance_sets -- A reference to a BitArray for storing + * the result. The BitArray should have + * capacity for (at least) + * `this->buchi_automaton + * .numberOfAcceptanceSets()' bits. + * (The second argument is needed to allow the class + * StateSpaceProduct to be used for instantiating the Product + * template; see file Product.h.) + * + * Returns: Nothing. After the operation, `acceptance_sets[i] == true' + * holds if `state.acceptanceSets().test(i) == true' for all + * 0 <= i < `this->buchi_automaton.numberOfAcceptanceSets()'. + * + * ------------------------------------------------------------------------- */ +{ + acceptance_sets.bitwiseOr + (static_cast(state).acceptanceSets(), + numberOfAcceptanceSets()); +} + +/* ========================================================================= */ +inline void StateSpaceProduct::mergeAcceptanceInformation + (const Graph::Edge& buchi_transition, + const Graph::Edge&, BitArray& acceptance_sets) const +/* ---------------------------------------------------------------------------- + * + * Description: Merges the acceptance sets associated with a transition of a + * Büchi automaton into a collection of sets. + * + * Arguments: transition -- A constant reference to a transition in + * the automaton. + * acceptance_sets -- A reference to a BitArray for storing + * the result. The BitArray should have + * capacity for (at least) + * `this->buchi_automaton + * .numberOfAcceptanceSets()' bits. + * (The second argument is needed to allow the class + * StateSpaceProduct to be used for instantiating the Product + * template; see file Product.h.) + * + * Returns: Nothing. After the operation, `acceptance_sets[i] == true' + * holds if `transition.acceptanceSets().test(i) == true' for + * all + * 0 <= i < `this->buchi_automaton.numberOfAcceptanceSets()'. + * + * ------------------------------------------------------------------------- */ +{ + acceptance_sets.bitwiseOr + (static_cast(buchi_transition) + .acceptanceSets(), + numberOfAcceptanceSets()); +} + +/* ========================================================================= */ +inline void StateSpaceProduct::validateEdgeIterators + (const Graph::Node& buchi_state, + const Graph::Node& system_state, + GraphEdgeContainer::const_iterator& buchi_transition, + GraphEdgeContainer::const_iterator& system_transition) const +/* ---------------------------------------------------------------------------- + * + * Description: Checks whether a pair of transition iterators corresponds to + * a transition beginning from a state in the product of a Büchi + * automaton and a state space; if this is not the case, makes + * the iterators point to a valid transition beginning from the + * product state (or to the "end" of the collection of + * transitions beginning from the product state if no valid + * transition can be found by incrementing the iterators). + * + * Arguments: buchi_state, -- These variables determine the state + * system_state, in the product; `buchi_state' and + * `system_state' should be references to + * states in `this->buchi_automaton' and + * `this->statespace', respectively. + * buchi_transition, -- References to the transition + * system_transition iterators. It is assumed that + * `buchi_transition' and + * `system_transition' initially point to + * two transitions starting from + * `buchi_state' and `system_state', + * respectively. + * + * Returns: Nothing. Upon return, `buchi_transition' and + * `system_transition' will either equal + * `buchi_state.edges().end()' and `system_state.edges().end()', + * respectively, or they will point to a pair of transitions + * beginning from `buchi_state' and `system_state' such that + * this pair of transitions corresponds to a transition starting + * from the product state determined by `buchi_state' and + * `system_state'. + * + * ------------------------------------------------------------------------- */ +{ + const GraphEdgeContainer& buchi_transitions = buchi_state.edges(); + const GraphEdgeContainer& system_transitions = system_state.edges(); + + if (buchi_transition == buchi_transitions.end()) + { + system_transition = system_transitions.end(); + return; + } + if (system_transition == system_transitions.end()) + { + buchi_transition = buchi_transitions.end(); + return; + } + + while (!static_cast + (*buchi_transition)->enabled + (static_cast(system_state) + .positiveAtoms(), + statespace.numberOfPropositions())) + { + ++buchi_transition; + if (buchi_transition == buchi_transitions.end()) + { + system_transition = system_transitions.end(); + return; + } + } + + system_transition = system_transitions.begin(); +} + +/* ========================================================================= */ +inline void StateSpaceProduct::incrementEdgeIterators + (const Graph::Node& buchi_state, + const Graph::Node& system_state, + GraphEdgeContainer::const_iterator& buchi_transition, + GraphEdgeContainer::const_iterator& system_transition) const +/* ---------------------------------------------------------------------------- + * + * Description: Increments a pair of transition iterators to point to the + * "next" transition beginning from a state in the product of a + * Büchi automaton and a state space. If no "next" transition + * exists, makes the iterators point to the "end" of the + * collection of transitions beginning from the product state. + * + * Arguments: buchi_state, -- These variables determine the state + * system_state, in the product; `buchi_state' and + * `system_state' should be references to + * states in `this->buchi_automaton' and + * `this->statespace', respectively. + * buchi_transition, -- References to the transition + * system_transition iterators. It is assumed that + * `buchi_transition' and + * `system_transition' initially point to + * two transitions starting from + * `buchi_state' and `system_state', + * respectively. + * + * Returns: Nothing. Upon return, `buchi_transition' and + * `system_transition' will either equal + * `buchi_state.edges().end()' and `system_state.edges().end()', + * respectively, or they will point to a pair of transitions + * beginning from `buchi_state' and `system_state' such that + * this pair of transitions corresponds to a transition starting + * from the product state determined by `buchi_state' and + * `system_state'. + * + * ------------------------------------------------------------------------- */ +{ + const GraphEdgeContainer& buchi_transitions = buchi_state.edges(); + const GraphEdgeContainer& system_transitions = system_state.edges(); + + ++system_transition; + if (system_transition == system_transitions.end()) + { + do + { + ++buchi_transition; + if (buchi_transition == buchi_transitions.end()) + return; + } + while (!static_cast + (*buchi_transition)->enabled + (static_cast(system_state) + .positiveAtoms(), + statespace.numberOfPropositions())); + + system_transition = system_transitions.begin(); + } +} + +} + +#endif /* !STATESPACEPRODUCT_H */ diff --git a/lbtt/src/TempFsysName.cc b/lbtt/src/TempFsysName.cc new file mode 100644 index 000000000..51dc9c335 --- /dev/null +++ b/lbtt/src/TempFsysName.cc @@ -0,0 +1,125 @@ +/* + * Copyright (C) 2004 + * Heikki Tauriainen + * + * This program 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. + * + * This program 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 this program; 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 +#ifdef HAVE_FCNTL_H +#include +#endif /* HAVE_FCNTL_H */ +#include +#include "Exception.h" +#include "StringUtil.h" +#include "TempFsysName.h" + +/****************************************************************************** + * + * Number of generated temporary names. + * + *****************************************************************************/ + +unsigned long int TempFsysName::number_of_allocated_names = 0; + + + +/****************************************************************************** + * + * Function definitions for class TempFsysName. + * + *****************************************************************************/ + +/* ========================================================================= */ +const char* TempFsysName::allocate + (const char* prefix, const NameType t, const bool literal) +/* ---------------------------------------------------------------------------- + * + * Description: Associates a TempFsysName object with a temporary name. (As + * a side effect, the function actually creates an empty + * temporary file or a directory to reserve the name in the file + * system. The file or directory should never be removed + * explicitly; it is removed automatically when the TempFsysName + * object is destroyed or another call is made to + * `this->allocate'.) + * + * Arguments: prefix -- Pointer to a C-style string containing a prefix + * for the temporary name (empty by default). If + * `literal == true', `prefix' (if nonempty) is + * assumed to contain the full path for the + * temporary file or directory; otherwise the + * function will reserve a temporary name in the + * `P_tmpdir' directory. This name will consist + * of the value of `prefix' (if nonempty), followed + * by the current value of + * `TempFsysName::number_of_allocated_names' and + * the current process id, separated by dots. + * t -- Determines the type of the name (file or a + * directory). + * literal -- See above. + * + * Returns: A pointer to a constant C-style string containing the + * temporary name. The function throws an IOException if the + * name allocation or the file or directory creation fails. + * + * ------------------------------------------------------------------------- */ +{ + releaseName(); + + using ::StringUtil::toString; + string tempname; + + try + { + if (!literal || strlen(prefix) == 0) + { + tempname = toString(P_tmpdir) + "/"; + if (strlen(prefix)) + tempname += string(prefix) + "."; + tempname += toString(number_of_allocated_names) + "." + + toString(getpid()); + ++number_of_allocated_names; + } + else + tempname = prefix; + + name = new char[tempname.length() + 1]; + strcpy(name, tempname.c_str()); + } + catch (const bad_alloc&) + { + name = 0; + throw IOException + ("unable to allocate a temporary name in the file system"); + } + + type = t; + if (t == FILE) + { + int fd = open(name, O_RDWR | O_CREAT | O_EXCL, S_IREAD | S_IWRITE); + if (fd == -1) + throw IOException("unable to create a temporary file"); + close(fd); + } + else if (mkdir(name, S_IRWXU) == -1) + throw IOException("unable to create a temporary directory"); + + return name; +} diff --git a/lbtt/src/TempFsysName.h b/lbtt/src/TempFsysName.h new file mode 100644 index 000000000..f2845ebb6 --- /dev/null +++ b/lbtt/src/TempFsysName.h @@ -0,0 +1,157 @@ +/* + * Copyright (C) 2004 + * Heikki Tauriainen + * + * This program 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. + * + * This program 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 this program; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. + */ + +#ifndef TEMPFSYSNAME_H +#define TEMPFSYSNAME_H + +#include +#include +#ifdef HAVE_UNISTD_H +#include +#endif /* HAVE_UNISTD_H */ + +/****************************************************************************** + * + * A class for temporary file system names. + * + *****************************************************************************/ + +class TempFsysName +{ +public: + TempFsysName(); /* Constructor. */ + + ~TempFsysName(); /* Destructor. */ + + enum NameType { FILE, DIRECTORY }; /* Types of temporary + * file system names. + */ + + const char* allocate /* Allocates a name */ + (const char* prefix = "", /* in the file system. */ + const NameType t = FILE, + const bool literal = false); + + const char* get() const; /* Tells the name. */ + +private: + TempFsysName(const TempFsysName&); /* Prevent copying and */ + TempFsysName& operator=(const TempFsysName&); /* assignment of + * TempFsysName objects. + */ + + void releaseName(); /* Frees a name in the file + * system. + */ + + char* name; /* Temporary name. */ + + NameType type; /* Tells whether the name + * refers to a file or a + * directory. + */ + + static unsigned long int /* Counter for the */ + number_of_allocated_names; /* number of generated + * temporary names. + */ +}; + + + +/****************************************************************************** + * + * Inline function definitions for class TempFsysName. + * + *****************************************************************************/ + +/* ========================================================================= */ +inline TempFsysName::TempFsysName() : name(static_cast(0)) +/* ---------------------------------------------------------------------------- + * + * Description: Constructor for class TempFsysName. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +inline TempFsysName::~TempFsysName() +/* ---------------------------------------------------------------------------- + * + * Description: Destructor for class TempFsysName. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ + releaseName(); +} + +/* ========================================================================= */ +inline const char* TempFsysName::get() const +/* ---------------------------------------------------------------------------- + * + * Description: Tells the name associated with the TempFsysName object. + * + * Arguments: None. + * + * Returns: A pointer to a constant C-style string containing the name + * associated with the TempFsysName object. If the TempFsysName + * object has not yet been (successfully) associated with a file + * using TempFsysName::allocate, this pointer has the value 0. + * + * ------------------------------------------------------------------------- */ +{ + return name; +} + +/* ========================================================================= */ +inline void TempFsysName::releaseName() +/* ---------------------------------------------------------------------------- + * + * Description: Deallocates the memory reserved for `this->name' and frees + * the name also in the file system by removing the file or + * directory associated with the object. If the name + * is associated with a directory, the directory is assumed to + * be empty. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ + if (name == static_cast(0)) + return; + if (type == FILE) + remove(name); + else + rmdir(name); + delete[] name; + name = 0; +} + +#endif /* !TEMPFSYSNAME_H */