Line data    Source code

       1             : // Copyright (c) 2009-2013 University of Twente
       2             : // Copyright (c) 2009-2013 Michael Weber <michaelw@cs.utwente.nl>
       3             : // Copyright (c) 2009-2013 Maks Verver <maksverver@geocities.com>
       4             : // Copyright (c) 2009-2013 Eindhoven University of Technology
       5             : //
       6             : // Distributed under the Boost Software License, Version 1.0.
       7             : // (See accompanying file LICENSE_1_0.txt or copy at
       8             : // http://www.boost.org/LICENSE_1_0.txt)
       9             : 
      10             : #include "mcrl2/pg/ParityGame.h"
      11             : #include "mcrl2/pg/SCC.h"
      12             : 
      13             : /*! \file ParityGame_verify.cc
      14             : 
      15             :     Implementation of parity game solution verification algorithm.
      16             : */
      17             : 
      18             : 
      19             : /*! A functor that is used to verify the solution for a strongly-connected
      20             :     component of the game graph.
      21             : 
      22             :     This is a separate class because the SCC decomposition algorithm expects
      23             :     a functor which is called for every component found.
      24             : 
      25             :     \see ParityGame::verify
      26             : */
      27             : struct VerifySCC  // used by ParityGame::verify()
      28             : {
      29             :     const ParityGame    &game;
      30             :     const StaticGraph   &graph;
      31             :     const priority_t    prio;
      32             :     verti * const       error;
      33             : 
      34           0 :     int operator() (const verti *scc, std::size_t scc_size)
      35             :     {
      36             :         // Search vertices in this SCC for a vertex with priority `prio`:
      37           0 :         for (std::size_t i = 0; i < scc_size; ++i)
      38             :         {
      39           0 :             verti v = scc[i];
      40           0 :             if (game.priority(v) == prio)
      41             :             {
      42             :                 // Cycle detected if |SCC| > 1 or v has a self-edge:
      43           0 :                 if (scc_size > 1 || graph.has_succ(v, v))
      44             :                 {
      45           0 :                     if (error) *error = v;
      46           0 :                     return 1;
      47             :                 }
      48             :             }
      49             :         }
      50           0 :         return 0;
      51             :     }
      52             : };
      53             : 
      54           0 : bool ParityGame::verify(const Strategy &s, verti *error) const
      55             : {
      56           0 :     assert(s.size() == graph_.V());
      57             : 
      58             :     /* Make sure winning sets are consistently defined; i.e. only existent
      59             :        edges are used, and there are no transitions that cross winning sets. */
      60           0 :     for (verti v = 0; v < graph_.V(); ++v)
      61             :     {
      62           0 :         Player pl = winner(s, v);
      63             : 
      64           0 :         if (pl == player(v))  /* vertex won by owner */
      65             :         {
      66             :             /* Verify that:
      67             :                 1. the vertex owner has a strategy (necessarily passes)
      68             :                 2. the strategy uses an existing edge
      69             :                 3. the strategy doesn't move outside the owner's winning set */
      70           0 :             if ( s[v] == NO_VERTEX || !graph_.has_succ(v, s[v]) ||
      71           0 :                  winner(s, s[v]) != pl )
      72             :             {
      73           0 :                 if (error) *error = v;
      74           0 :                 return false;
      75             :             }
      76             :         }
      77             :         else  /* vertex lost by owner */
      78             :         {
      79             :             // Verify owner has no strategy: (necessarily passes)
      80           0 :             if (s[v] != NO_VERTEX)
      81             :             {
      82           0 :                 if (error) *error = v;
      83           0 :                 return false;
      84             :             }
      85             : 
      86             :             // Verify owner cannot move outside this winning set:
      87           0 :             for (StaticGraph::const_iterator it = graph_.succ_begin(v);
      88           0 :                  it != graph_.succ_end(v); ++it)
      89             :             {
      90           0 :                 if (winner(s, *it) != pl)
      91             :                 {
      92           0 :                     if (error) *error = v;
      93           0 :                     return false;
      94             :                 }
      95             :             }
      96             :         }
      97             :     }
      98             : 
      99             :     // Verify absence of cycles owned by opponent in winning sets
     100           0 :     for (priority_t prio = 0; prio < d(); ++prio)
     101             :     {
     102             :         /* Create set of edges incident with vertices in the winning set of
     103             :            player (1 - prio%2) consistent with strategy s and incident with
     104             :            vertices of priorities >= prio only. */
     105           0 :         StaticGraph::edge_list edges;
     106           0 :         for (verti v = 0; v < graph_.V(); ++v)
     107             :         {
     108           0 :             if (priority(v) >= prio && (int)winner(s, v) == (1 - prio%2))
     109             :             {
     110           0 :                 if (s[v] != NO_VERTEX)
     111             :                 {
     112           0 :                     if (priority(s[v]) >= prio)
     113             :                     {
     114           0 :                         edges.push_back(std::make_pair(v, s[v]));
     115             :                     }
     116             :                 }
     117             :                 else
     118             :                 {
     119           0 :                     for (StaticGraph::const_iterator it = graph_.succ_begin(v);
     120           0 :                          it != graph_.succ_end(v); ++it)
     121             :                     {
     122           0 :                         if (priority(*it) >= prio)
     123             :                         {
     124           0 :                             edges.push_back(std::make_pair(v, *it));
     125             :                         }
     126             :                     }
     127             :                 }
     128             :             }
     129             :         }
     130             : 
     131             :         /* NOTE: we should NOT compact vertices here, because then we cannot
     132             :            use their indices to determine the priority of vertices in
     133             :            VerifySCC::operator().
     134             : 
     135             :            Alternatively, we could compress the priority vector as well.
     136             :            We could share some code with make_subgame() to do this (except that
     137             :            we don't need the player vector, and we don't need bidirectional
     138             :            edges, which require sorting).
     139             :         */
     140             : 
     141             :         // Create a subgraph storing successors only:
     142           0 :         StaticGraph subgraph;
     143           0 :         subgraph.assign(edges, StaticGraph::EDGE_SUCCESSOR);
     144             : 
     145             :         // Find a vertex with priority prio on a cycle:
     146           0 :         VerifySCC verifier = { *this, subgraph, prio, error };
     147           0 :         if (decompose_graph(subgraph, verifier) != 0)
     148             :         {
     149             :             // VerifySCC has already set *error here.
     150           0 :             return false;
     151             :         }
     152           0 :     }
     153           0 :     if (error) *error = NO_VERTEX;
     154           0 :     return true;
     155             : }