game.cc 10.7 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
  } // 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";
      }
  }

233
  solved_game parity_game_solve(const const_twa_graph_ptr& arena)
234
  {
235
236
237
    solved_game result;
    result.arena = arena;

238
239
240
241
242
243
244
245
246
247
248
249
    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;

250
251
252
253
    solve_rec(arena, owner, states_, m.max_set(),
              result.winning_region, result.winning_strategy);

    return result;
254
  }
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311

  void propagate_players(spot::twa_graph_ptr& arena,
                         bool first_player, bool complete0)
  {
    auto um = arena->acc().unsat_mark();
    if (!um.first)
      throw std::runtime_error("game winning condition is a tautology");

    unsigned sink_env = 0;
    unsigned sink_con = 0;

    std::vector<bool> seen(arena->num_states(), false);
    unsigned init = arena->get_init_state_number();
    std::vector<unsigned> todo({init});
    auto owner = new std::vector<bool>(arena->num_states(), false);
    (*owner)[init] = first_player;
    while (!todo.empty())
      {
        unsigned src = todo.back();
        todo.pop_back();
        seen[src] = true;
        bdd missing = bddtrue;
        for (const auto& e: arena->out(src))
          {
            bool osrc = (*owner)[src];
            if (complete0 && !osrc)
              missing -= e.cond;

            if (!seen[e.dst])
              {
                (*owner)[e.dst] = !osrc;
                todo.push_back(e.dst);
              }
            else if ((*owner)[e.dst] == osrc)
              {
                delete owner;
                throw
                  std::runtime_error("propagate_players(): odd cycle detected");
              }
          }
        if (complete0 && !(*owner)[src] && missing != bddfalse)
          {
            if (sink_env == 0)
              {
                sink_env = arena->new_state();
                sink_con = arena->new_state();
                owner->push_back(true);
                owner->push_back(false);
                arena->new_edge(sink_con, sink_env, bddtrue, um.second);
                arena->new_edge(sink_env, sink_con, bddtrue, um.second);
              }
            arena->new_edge(src, sink_con, missing, um.second);
          }
      }

    arena->set_named_prop("state-player", owner);
  }
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351

  twa_graph_ptr
  highlight_strategy(twa_graph_ptr& aut, const strategy_t& s,
                     unsigned color)
  {
    unsigned ns = aut->num_states();
    auto* highlight = aut->get_or_set_named_prop<std::map<unsigned, unsigned>>
      ("highlight-edges");

    for (auto [src, n]: s)
      {
        if (src >= ns)
          throw std::runtime_error
            ("highlight_strategy(): strategy refers to unexisting states");
        unsigned int i = 0;
        for (auto& t: aut->out(src))
          if (i++ == n)
            {
              (*highlight)[aut->edge_number(t)] = color;
              break;
            }
      }

    return aut;
  }

  twa_graph_ptr
  solved_game::highlight_strategy(unsigned player, unsigned color)
  {
    auto aut = std::const_pointer_cast<twa_graph>(arena);

    auto* highlight = aut->get_or_set_named_prop<std::map<unsigned, unsigned>>
      ("highlight-states");
    unsigned ns = aut->num_states();
    for (unsigned i = 0; i < ns; ++i)
      if (player_winning_at(player, i))
        (*highlight)[i] = color;

    return spot::highlight_strategy(aut, winning_strategy[!!player], color);
  }
Thibaud Michaud's avatar
Thibaud Michaud committed
352
}