spot  2.8.3
Public Member Functions | List of all members
spot::state_ta_product Class Reference

A state for spot::ta_product. More...

#include <spot/ta/taproduct.hh>

Inheritance diagram for spot::state_ta_product:
Collaboration diagram for spot::state_ta_product:

Public Member Functions

 state_ta_product (const state *ta_state, const state *kripke_state)
 Constructor. More...
 state_ta_product (const state_ta_product &o)=delete
const stateget_ta_state () const
const stateget_kripke_state () const
virtual int compare (const state *other) const override
 Compares two states (that come from the same automaton). More...
virtual size_t hash () const override
 Hash a state. More...
virtual state_ta_productclone () const override
 Duplicate a state. More...
virtual void destroy () const
 Release a state. More...

Detailed Description

A state for spot::ta_product.

This state is in fact a pair of state: the state from the TA automaton and that of Kripke structure.

Constructor & Destructor Documentation

◆ state_ta_product()

spot::state_ta_product::state_ta_product ( const state ta_state,
const state kripke_state 


ta_stateThe state from the ta automaton.
kripke_stateThe state from Kripke structure.

Member Function Documentation

◆ clone()

virtual state_ta_product* spot::state_ta_product::clone ( ) const

Duplicate a state.

Implements spot::state.

◆ compare()

virtual int spot::state_ta_product::compare ( const state other) const

Compares two states (that come from the same automaton).

This method returns an integer less than, equal to, or greater than zero if this is found, respectively, to be less than, equal to, or greater than other according to some implicit total order.

This method should not be called to compare states from different automata.

See also

Implements spot::state.

◆ destroy()

virtual void spot::state::destroy ( ) const

Release a state.

Methods from the tgba or twa_succ_iterator always return a new state that you should deallocate with this function. Before Spot 0.7, you had to "delete" your state directly. Starting with Spot 0.7, you should update your code to use this function instead. destroy() usually calls delete, except in subclasses that destroy() to allow better memory management (e.g., no memory allocation for explicit automata).

Reimplemented in spot::state_ta_explicit, spot::twa_graph_state, spot::kripke_graph_state, and spot::state_product.

Referenced by spot::state_unicity_table::is_new(), and spot::state_unicity_table::operator()().

◆ hash()

virtual size_t spot::state_ta_product::hash ( ) const

Hash a state.

This method returns an integer that can be used as a hash value for this state.

Note that the hash value is guaranteed to be unique for all equal states (in compare()'s sense) for only as long as one of these states exists. So it's OK to use a spot::state as a key in a hash_map because the mere use of the state as a key in the hash will ensure the state continues to exist.

However if you create the state, get its hash key, delete the state, recreate the same state, and get its hash key, you may obtain two different hash keys if the same state were not already used elsewhere. In practice this weird situation can occur only when the state is BDD-encoded, because BDD numbers (used to build the hash value) can be reused for other formulas. That probably doesn't matter, since the hash value is meant to be used in a hash_map, but it had to be noted.

Implements spot::state.

The documentation for this class was generated from the following file:

Please direct any question, comment, or bug report to the Spot mailing list at
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.8.13