game.cc 7.73 KB
Newer Older
Thibaud Michaud's avatar
Thibaud Michaud committed
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2017, 2018, 2020 Laboratoire de Recherche et Développement
Thibaud Michaud's avatar
Thibaud Michaud committed
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

20
#include "config.h"
Thibaud Michaud's avatar
Thibaud Michaud committed
21
22

#include <cmath>
23
#include <spot/misc/game.hh>
Thibaud Michaud's avatar
Thibaud Michaud committed
24
25
26

namespace spot
{
27
28
  namespace
  {
Thibaud Michaud's avatar
Thibaud Michaud committed
29

30
31
    static const std::vector<bool>*
    ensure_parity_game(const const_twa_graph_ptr& arena, const char* fnname)
Thibaud Michaud's avatar
Thibaud Michaud committed
32
    {
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
      bool max, odd;
      arena->acc().is_parity(max, odd, true);
      if (!(max && odd))
        throw std::runtime_error
          (std::string(fnname) +
           ": arena must have max-odd acceptance condition");

      for (const auto& e : arena->edges())
        if (!e.acc)
          throw std::runtime_error
            (std::string(fnname) + ": arena must be colorized");

      auto owner = arena->get_named_prop<std::vector<bool>>("state-player");
      if (!owner)
        throw std::runtime_error
          (std::string(fnname) + ": automaton should define \"state-player\"");

      return owner;
Thibaud Michaud's avatar
Thibaud Michaud committed
51
52
    }

53

54
55
56
57
58
59
60
61
62
63
    strategy_t attractor(const const_twa_graph_ptr& arena,
                         const std::vector<bool>* owner,
                         const region_t& subgame, region_t& set,
                         unsigned max_parity, int p,
                         bool attr_max)
    {
      strategy_t strategy;
      std::set<unsigned> complement(subgame.begin(), subgame.end());
      for (unsigned s: set)
        complement.erase(s);
64

65
66
67
      acc_cond::mark_t max_acc({});
      for (unsigned i = 0; i <= max_parity; ++i)
        max_acc.set(i);
68

69
70
      bool once_more;
      do
71
        {
72
73
74
75
76
          once_more = false;
          for (auto it = complement.begin(); it != complement.end();)
            {
              unsigned s = *it;
              unsigned i = 0;
77

78
79
              bool is_owned = (*owner)[s] == p;
              bool wins = !is_owned;
80

81
              for (const auto& e: arena->out(s))
82
                {
83
                  if ((e.acc & max_acc) && subgame.count(e.dst))
84
                    {
85
86
                      if (set.count(e.dst)
                          || (attr_max && e.acc.max_set() - 1 == max_parity))
87
                        {
88
89
90
91
92
93
                          if (is_owned)
                            {
                              strategy[s] = i;
                              wins = true;
                              break; // no need to check all edges
                            }
94
                        }
95
                      else
96
                        {
97
98
99
100
101
                          if (!is_owned)
                            {
                              wins = false;
                              break; // no need to check all edges
                            }
102
103
                        }
                    }
104
                  ++i;
105
                }
106

107
108
109
110
111
112
113
114
115
              if (wins)
                {
                  // FIXME C++17 extract/insert could be useful here
                  set.emplace(s);
                  it = complement.erase(it);
                  once_more = true;
                }
              else
                ++it;
116
            }
117
118
        } while (once_more);
      return strategy;
119
    }
120

121
122
123
124
    void solve_rec(const const_twa_graph_ptr& arena,
                   const std::vector<bool>* owner,
                   region_t& subgame, unsigned max_parity,
                   region_t (&w)[2], strategy_t (&s)[2])
125
    {
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
      assert(w[0].empty());
      assert(w[1].empty());
      assert(s[0].empty());
      assert(s[1].empty());
      // The algorithm works recursively on subgames. To avoid useless copies of
      // the game at each call, subgame and max_parity are used to filter states
      // and transitions.
      if (subgame.empty())
        return;
      int p = max_parity % 2;

      // Recursion on max_parity.
      region_t u;
      auto strat_u = attractor(arena, owner, subgame, u, max_parity, p, true);

      if (max_parity == 0)
        {
          s[p] = std::move(strat_u);
          w[p] = std::move(u);
          // FIXME what about w[!p]?
          return;
        }

      for (unsigned s: u)
        subgame.erase(s);
      region_t w0[2]; // Player's winning region in the first recursive call.
      strategy_t s0[2]; // Player's winning strategy in the first
                        // recursive call.
      solve_rec(arena, owner, subgame, max_parity - 1, w0, s0);
      if (w0[0].size() + w0[1].size() != subgame.size())
        throw std::runtime_error("size mismatch");
      //if (w0[p].size() != subgame.size())
      //  for (unsigned s: subgame)
      //    if (w0[p].find(s) == w0[p].end())
      //      w0[!p].insert(s);
      subgame.insert(u.begin(), u.end());

      if (w0[p].size() + u.size() == subgame.size())
        {
          s[p] = std::move(strat_u);
          s[p].insert(s0[p].begin(), s0[p].end());
          w[p].insert(subgame.begin(), subgame.end());
          return;
        }
170

171
172
173
      // Recursion on game size.
      auto strat_wnp = attractor(arena, owner,
                                 subgame, w0[!p], max_parity, !p, false);
174

175
176
      for (unsigned s: w0[!p])
        subgame.erase(s);
177

178
179
180
181
182
      region_t w1[2]; // Odd's winning region in the second recursive call.
      strategy_t s1[2]; // Odd's winning strategy in the second recursive call.
      solve_rec(arena, owner, subgame, max_parity, w1, s1);
      if (w1[0].size() + w1[1].size() != subgame.size())
        throw std::runtime_error("size mismatch");
183

184
185
      w[p] = std::move(w1[p]);
      s[p] = std::move(s1[p]);
186

187
188
189
190
191
      w[!p] = std::move(w1[!p]);
      w[!p].insert(w0[!p].begin(), w0[!p].end());
      s[!p] = std::move(strat_wnp);
      s[!p].insert(s0[!p].begin(), s0[!p].end());
      s[!p].insert(s1[!p].begin(), s1[!p].end());
192

193
194
      subgame.insert(w0[!p].begin(), w0[!p].end());
    }
195

196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
  } // anonymous

  void pg_print(std::ostream& os, const const_twa_graph_ptr& arena)
  {
    auto owner = ensure_parity_game(arena, "pg_print");

    unsigned ns = arena->num_states();
    unsigned init = arena->get_init_state_number();
    os << "parity " << ns - 1 << ";\n";
    std::vector<bool> seen(ns, false);
    std::vector<unsigned> todo({init});
    while (!todo.empty())
      {
        unsigned src = todo.back();
        todo.pop_back();
        if (seen[src])
          continue;
        seen[src] = true;
        os << src << ' ';
        os << arena->out(src).begin()->acc.max_set() - 1 << ' ';
        os << (*owner)[src] << ' ';
        bool first = true;
        for (auto& e: arena->out(src))
          {
            if (!first)
              os << ',';
            first = false;
            os << e.dst;
            if (!seen[e.dst])
              todo.push_back(e.dst);
          }
        if (src == init)
          os << " \"INIT\"";
        os << ";\n";
      }
  }

  void parity_game_solve(const const_twa_graph_ptr& arena,
                         region_t (&w)[2], strategy_t (&s)[2])
  {
    const std::vector<bool>* owner =
      ensure_parity_game(arena, "parity_game_solve");

    region_t states_;
    unsigned ns = arena->num_states();
    for (unsigned i = 0; i < ns; ++i)
      states_.insert(i);

    acc_cond::mark_t m{};
    for (const auto& e: arena->edges())
      m |= e.acc;

    solve_rec(arena, owner, states_, m.max_set(), w, s);
  }
Thibaud Michaud's avatar
Thibaud Michaud committed
250
}