spot  2.7.4
game.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2017-2018 Laboratoire de Recherche et Développement
3 // de l'Epita (LRDE).
4 //
5 // This file is part of Spot, a model checking library.
6 //
7 // Spot is free software; you can redistribute it and/or modify it
8 // under the terms of the GNU General Public License as published by
9 // the Free Software Foundation; either version 3 of the License, or
10 // (at your option) any later version.
11 //
12 // Spot is distributed in the hope that it will be useful, but WITHOUT
13 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
15 // License for more details.
16 //
17 // You should have received a copy of the GNU General Public License
18 // along with this program. If not, see <http://www.gnu.org/licenses/>.
19 
20 #pragma once
21 
22 #include <algorithm>
23 #include <memory>
24 #include <ostream>
25 #include <unordered_map>
26 #include <vector>
27 
28 #include <bddx.h>
29 #include <spot/twa/twagraph.hh>
30 #include <spot/twaalgos/parity.hh>
31 
32 namespace spot
33 {
34 
35 class SPOT_API parity_game
36 {
37 private:
38  const const_twa_graph_ptr arena_;
39  const std::vector<bool> owner_;
40 
41 public:
50  parity_game(const twa_graph_ptr& arena, const std::vector<bool>& owner);
51 
52  unsigned num_states() const
53  {
54  return arena_->num_states();
55  }
56 
57  unsigned get_init_state_number() const
58  {
59  return arena_->get_init_state_number();
60  }
61 
63  out(unsigned src) const
64  {
65  return arena_->out(src);
66  }
67 
69  out(unsigned src)
70  {
71  return arena_->out(src);
72  }
73 
74  bool owner(unsigned src) const
75  {
76  return owner_[src];
77  }
78 
79  unsigned max_parity() const
80  {
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;
86  }
87 
89  void print(std::ostream& os);
90 
91  typedef std::unordered_set<unsigned> region_t;
92  // Map state number to index of the transition to take.
93  typedef std::unordered_map<unsigned, unsigned> strategy_t;
94 
97 
109  void solve(region_t (&w)[2], strategy_t (&s)[2]) const;
110 
111 private:
113 
114  // Compute (in place) a set of states from which player can force a visit
115  // through set, and a strategy to do it.
116  // if attr_max is true, states that can force a visit through an edge with
117  // max parity are also counted in.
118  strategy_t attractor(const region_t& subgame, region_t& set,
119  unsigned max_parity, int odd,
120  bool attr_max = false) const;
121 
122  // Compute the winning strategy and winning region for both players.
123  void solve_rec(region_t& subgame, unsigned max_parity,
124  region_t (&w)[2], strategy_t (&s)[2]) const;
125 };
126 
127 }
Definition: automata.hh:26
Definition: game.hh:35
Definition: graph.hh:183
Definition: graph.hh:384

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.8.13