f0de38680a
(state_ptr_equal, state_ptr_hash): New functors. * src/tgba/statebdd.hh, src/tgba/statebdd.cc (state_bdd::hash): New method. * src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc (state_explicit::hash): New method. (ns_map, sn_map): Use Sgi::hash_map instead of std::map. * src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc (state_product::hash): New method. * src/tgba/tgbatba.cc (state_tba_proxy::hash): New method. * src/tgbaalgos/lbtt.cc (acp_seen, todo_set, seen_map): Redefine using Sgi::hash_map or Sgi::hash_set. (lbtt_reachable): Don't erase a key that is pointed to by an iterator. * src/tgbaalgos/reachiter.cc (tgba_reachable_iterator::~tgba_reachable_iterator): Likewise. * src/tgbaalgos/magic.cc (magic_search::~magic_search()): Likewise. * src/tgbaalgos/magic.hh (hash_type): Redefine using Sgi::hash_map. * src/tgbaalgos/reachiter.hh (seen_map): Redefine using Sgi::hash_map. * iface/gspn/gspn.cc (state_gspn::hash): New method. * src/misc/hash.hh (string_hash): New functor.
103 lines
3.1 KiB
C++
103 lines
3.1 KiB
C++
#ifndef SPOT_TGBAALGOS_MAGIC_HH
|
|
# define SPOT_TGBAALGOS_MAGIC_HH
|
|
|
|
#include "misc/hash.hh"
|
|
#include <list>
|
|
#include <utility>
|
|
#include <ostream>
|
|
#include "tgba/tgbatba.hh"
|
|
|
|
namespace spot
|
|
{
|
|
/// \brief Emptiness check on spot::tgba_tba_proxy automata using
|
|
/// the Magic Search algorithm.
|
|
///
|
|
/// This algorithm comes from
|
|
/// \verbatim
|
|
/// @InProceedings{ godefroid.93.pstv,
|
|
/// author = {Patrice Godefroid and Gerard .J. Holzmann},
|
|
/// title = {On the verification of temporal properties},
|
|
/// booktitle = {Proceedings of the 13th IFIP TC6/WG6.1 International
|
|
/// Symposium on Protocol Specification, Testing, and
|
|
/// Verification (PSTV'93)},
|
|
/// month = {May},
|
|
/// editor = {Andr{\'e} A. S. Danthine and Guy Leduc
|
|
/// and Pierre Wolper},
|
|
/// address = {Liege, Belgium},
|
|
/// pages = {109--124},
|
|
/// publisher = {North-Holland},
|
|
/// year = {1993},
|
|
/// series = {IFIP Transactions},
|
|
/// volume = {C-16},
|
|
/// isbn = {0-444-81648-8}
|
|
/// }
|
|
/// \endverbatim
|
|
struct magic_search
|
|
{
|
|
/// Initialize the Magic Search algorithm on the automaton \a a.
|
|
magic_search(const tgba_tba_proxy *a);
|
|
~magic_search();
|
|
|
|
/// \brief Perform a Magic Search.
|
|
///
|
|
/// \return true iff the algorithm has found a new accepting
|
|
/// path.
|
|
///
|
|
/// check() can be called several times until it return false,
|
|
/// to enumerate all accepting paths.
|
|
bool check();
|
|
|
|
/// \brief Print the last accepting path found.
|
|
///
|
|
/// Restrict printed states to \a the state space of restrict if
|
|
/// supplied.
|
|
std::ostream& print_result(std::ostream& os,
|
|
const tgba* restrict = 0) const;
|
|
|
|
private:
|
|
|
|
// The names "stack", "h", and "x", are those used in the paper.
|
|
|
|
/// \brief Records whether a state has be seen with the magic bit
|
|
/// on or off.
|
|
struct magic
|
|
{
|
|
bool seen_without : 1;
|
|
bool seen_with : 1;
|
|
};
|
|
|
|
/// \brief A state for the spot::magic_search algorithm.
|
|
struct magic_state
|
|
{
|
|
const state* s;
|
|
bool m; ///< The state of the magic demon.
|
|
};
|
|
|
|
typedef std::pair<magic_state, tgba_succ_iterator*> state_iter_pair;
|
|
typedef std::list<state_iter_pair> stack_type;
|
|
stack_type stack; ///< Stack of visited states on the path.
|
|
|
|
typedef std::list<bdd> tstack_type;
|
|
/// \brief Stack of transitions.
|
|
///
|
|
/// This is an addition to the data from the paper.
|
|
tstack_type tstack;
|
|
|
|
typedef Sgi::hash_map<const state*, magic,
|
|
state_ptr_hash, state_ptr_equal> hash_type;
|
|
hash_type h; ///< Map of visited states.
|
|
|
|
/// Append a new state to the current path.
|
|
void push(const state* s, bool m);
|
|
/// Check whether we already visited \a s with the Magic bit set to \a m.
|
|
bool has(const state* s, bool m) const;
|
|
|
|
const tgba_tba_proxy* a; ///< The automata to check.
|
|
/// The state for which we are currently seeking an SCC.
|
|
const state* x;
|
|
};
|
|
|
|
|
|
}
|
|
|
|
#endif // SPOT_TGBAALGOS_MAGIC_HH
|