25 #include <unordered_map> 29 #include <spot/twa/twagraph.hh> 30 #include <spot/twaalgos/parity.hh> 38 const const_twa_graph_ptr arena_;
39 const std::vector<bool> owner_;
50 parity_game(
const twa_graph_ptr& arena,
const std::vector<bool>& owner);
52 unsigned num_states()
const 54 return arena_->num_states();
57 unsigned get_init_state_number()
const 59 return arena_->get_init_state_number();
63 out(
unsigned src)
const 65 return arena_->out(src);
71 return arena_->out(src);
74 bool owner(
unsigned src)
const 79 unsigned max_parity()
const 81 unsigned max_parity = 0;
82 for (
const auto& e: arena_->edges())
83 max_parity = std::max(max_parity, e.acc.max_set());
84 SPOT_ASSERT(max_parity);
85 return max_parity - 1;
89 void print(std::ostream& os);
91 typedef std::unordered_set<unsigned> region_t;
93 typedef std::unordered_map<unsigned, unsigned> strategy_t;
109 void solve(region_t (&w)[2], strategy_t (&s)[2])
const;
134 bool solve_qp()
const;
143 strategy_t attractor(
const region_t& subgame, region_t&
set,
144 unsigned max_parity,
int odd,
145 bool attr_max =
false)
const;
148 void solve_rec(region_t& subgame,
unsigned max_parity,
149 region_t (&w)[2], strategy_t (&s)[2])
const;
157 std::vector<unsigned> b_;
163 : num_(state), b_(b), anke_(anke)
167 int compare(
const state* other)
const override;
171 return compare(&o) == 0;
176 return compare(&o) != 0;
184 for (
unsigned i = 0; i < b_.size(); ++i)
194 std::vector<unsigned> b()
const 210 typedef std::shared_ptr<const reachability_state>
211 const_reachability_state_ptr;
237 it_ = pg_.out(state_.num()).begin();
238 return it_ != pg_.out(state_.num()).end();
244 return it_ != pg_.out(state_.num()).end();
249 return it_ == pg_.out(state_.num()).end();
273 typedef std::unordered_map<spot::reachability_state,
274 std::vector<spot::reachability_state>,
282 const_reachability_state_ptr init_state_;
287 :
twa(std::make_shared<bdd_dict>()), pg_(pg)
289 init_state_ = std::shared_ptr<const reachability_state>(get_init_state());
296 std::string format_state(
const state* s)
const override;
301 bool mark(
const spot::reachability_state& s);
Definition: automata.hh:26
size_t wang32_hash(size_t key)
Thomas Wang's 32 bit hash function.
Definition: hashfunc.hh:41
acc_cond::mark_t acc() const override
Get the acceptance mark of the edge leading to this successor.
Definition: game.hh:259
bool done() const override
Check whether the iteration is finished.
Definition: game.hh:247
A Transition-based ω-Automaton.
Definition: twa.hh:622
Abstract class for states.
Definition: twa.hh:50
bdd cond() const override
Get the condition on the edge leading to this successor.
Definition: game.hh:254
reachability_state * clone() const override
Duplicate a state.
Definition: game.hh:189
Iterate over the successors of a state.
Definition: twa.hh:397
bool next() override
Jump to the next successor (if any).
Definition: game.hh:241
bool first() override
Position the iterator on the first successor (if any).
Definition: game.hh:235
size_t hash() const override
Hash a state.
Definition: game.hh:181