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;
178 : num_(other.num_), b_(other.b_), anke_(other.anke_)
184 return compare(&o) == 0;
189 return compare(&o) != 0;
197 for (
unsigned i = 0; i < b_.size(); ++i)
207 std::vector<unsigned> b()
const 223 typedef std::shared_ptr<const reachability_state>
224 const_reachability_state_ptr;
250 it_ = pg_.out(state_.num()).begin();
251 return it_ != pg_.out(state_.num()).end();
257 return it_ != pg_.out(state_.num()).end();
262 return it_ == pg_.out(state_.num()).end();
286 typedef std::unordered_map<spot::reachability_state,
287 std::vector<spot::reachability_state>,
295 const_reachability_state_ptr init_state_;
300 :
twa(std::make_shared<bdd_dict>()), pg_(pg)
302 init_state_ = std::shared_ptr<const reachability_state>(get_init_state());
309 std::string format_state(
const state* s)
const override;
314 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:272
bool done() const override
Check whether the iteration is finished.
Definition: game.hh:260
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:267
reachability_state * clone() const override
Duplicate a state.
Definition: game.hh:202
Iterate over the successors of a state.
Definition: twa.hh:397
bool next() override
Jump to the next successor (if any).
Definition: game.hh:254
bool first() override
Position the iterator on the first successor (if any).
Definition: game.hh:248
size_t hash() const override
Hash a state.
Definition: game.hh:194