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;
97 void solve(region_t (&w)[2], strategy_t (&s)[2])
const;
106 strategy_t attractor(
const region_t& subgame, region_t&
set,
107 unsigned max_parity,
int odd,
108 bool attr_max =
false)
const;
111 void solve_rec(region_t& subgame,
unsigned max_parity,
112 region_t (&w)[2], strategy_t (&s)[2])
const;
Definition: automata.hh:26