25 #include <unordered_map> 29 #include <spot/twa/twagraph.hh> 30 #include <spot/twaalgos/parity.hh> 38 const const_twa_graph_ptr dpa_;
39 const std::vector<bool> owner_;
50 : dpa_(dpa), owner_(owner)
54 dpa_->acc().is_parity(max, odd,
true);
55 SPOT_ASSERT(max && odd);
56 SPOT_ASSERT(owner_.size() == dpa_->num_states());
59 unsigned num_states()
const 61 return dpa_->num_states();
64 unsigned get_init_state_number()
const 66 return dpa_->get_init_state_number();
70 out(
unsigned src)
const 72 return dpa_->out(src);
78 return dpa_->out(src);
81 bool owner(
unsigned src)
const 86 unsigned max_parity()
const 88 unsigned max_parity = 0;
89 for (
auto& e: dpa_->edges())
90 max_parity = std::max(max_parity, e.acc.max_set());
91 SPOT_ASSERT(max_parity);
92 return max_parity - 1;
96 void print(std::ostream& os);
98 typedef std::unordered_set<unsigned> region_t;
100 typedef std::unordered_map<unsigned, unsigned> strategy_t;
116 std::pair<region_t, strategy_t> solve()
const;
141 bool solve_qp()
const;
150 strategy_t attractor(
const region_t& subgame, region_t&
set,
151 unsigned max_parity,
bool odd,
152 bool attr_max =
false)
const;
155 std::pair<region_t, strategy_t>
156 solve_rec(region_t& subgame,
unsigned max_parity)
const;
164 std::vector<unsigned> b_;
170 : num_(state), b_(b), anke_(anke)
174 int compare(
const state* other)
const override;
178 return compare(&o) == 0;
183 return compare(&o) != 0;
191 for (
unsigned i = 0; i < b_.size(); ++i)
201 std::vector<unsigned> b()
const 217 typedef std::shared_ptr<const reachability_state>
218 const_reachability_state_ptr;
244 it_ = pg_.out(state_.num()).begin();
245 return it_ != pg_.out(state_.num()).end();
251 return it_ != pg_.out(state_.num()).end();
256 return it_ == pg_.out(state_.num()).end();
280 typedef std::unordered_map<spot::reachability_state,
281 std::vector<spot::reachability_state>,
289 const_reachability_state_ptr init_state_;
294 :
twa(std::make_shared<bdd_dict>()), pg_(pg)
296 init_state_ = std::shared_ptr<const reachability_state>(get_init_state());
303 std::string format_state(
const state* s)
const override;
308 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:40
acc_cond::mark_t acc() const override
Get the acceptance mark of the edge leading to this successor.
Definition: game.hh:266
bool done() const override
Check whether the iteration is finished.
Definition: game.hh:254
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:261
reachability_state * clone() const override
Duplicate a state.
Definition: game.hh:196
Iterate over the successors of a state.
Definition: twa.hh:397
parity_game(const twa_graph_ptr dpa, std::vector< bool > owner)
Definition: game.hh:49
bool next() override
Jump to the next successor (if any).
Definition: game.hh:248
bool first() override
Position the iterator on the first successor (if any).
Definition: game.hh:242
size_t hash() const override
Hash a state.
Definition: game.hh:188