25 #include <spot/twa/twa.hh>
26 #include <spot/misc/fixpool.hh>
48 : left_(left), right_(right), count_(1), pool_(pool)
52 virtual void destroy()
const override;
66 virtual int compare(
const state* other)
const override;
67 virtual size_t hash()
const override;
68 virtual state_product* clone()
const override;
73 mutable unsigned count_;
74 fixed_size_pool* pool_;
76 virtual ~state_product();
77 state_product(
const state_product& o) =
delete;
89 twa_product(
const const_twa_ptr& left,
const const_twa_ptr& right);
93 virtual const state* get_init_state()
const override;
98 virtual std::string format_state(
const state* state)
const override;
100 virtual state* project_state(
const state* s,
const const_twa_ptr& t)
108 const_twa_ptr right_;
123 const state* left_init,
const state* right_init);
124 virtual const state* get_init_state()
const override;
126 const state* left_init_;
127 const state* right_init_;
131 inline twa_product_ptr otf_product(
const const_twa_ptr& left,
132 const const_twa_ptr& right)
134 return std::make_shared<twa_product>(left, right);
138 inline twa_product_ptr otf_product_at(
const const_twa_ptr& left,
139 const const_twa_ptr& right,
140 const state* left_init,
141 const state* right_init)
143 return std::make_shared<twa_product_init>(left, right,
144 left_init, right_init);
A lazy product. (States are computed on the fly.)
Definition: twaproduct.hh:82
A Transition-based ω-Automaton.
Definition: twa.hh:622
Abstract class for states.
Definition: twa.hh:50
A lazy product with different initial states.
Definition: twaproduct.hh:119
Iterate over the successors of a state.
Definition: twa.hh:397
A state for spot::twa_product.
Definition: twaproduct.hh:36
state_product(const state *left, const state *right, fixed_size_pool *pool)
Constructor.
Definition: twaproduct.hh:45
A fixed-size memory pool implementation.
Definition: fixpool.hh:31