LCOV - code coverage report
Current view: top level - pg/include/mcrl2/pg - SmallProgressMeasures_impl.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 0 74 0.0 %
Date: 2024-03-08 02:52:28 Functions: 0 7 0.0 %
Legend: Lines: hit not hit

          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             : // Don't include this file directly! Include SmallProgressMeasures.h instead.
      11             : 
      12             : #ifndef MCRL2_PG_SMALLPROGRESSMEASURES_IMPL_H
      13             : #define MCRL2_PG_SMALLPROGRESSMEASURES_IMPL_H
      14             : 
      15             : #include <deque>
      16             : 
      17             : #include "mcrl2/pg/SmallProgressMeasures.h"
      18             : 
      19           0 : inline int SmallProgressMeasures::vector_cmp(verti v, verti w, int N) const
      20             : {
      21           0 :     return vector_cmp(vec(v), vec(w), N);
      22             : }
      23             : 
      24           0 : inline int SmallProgressMeasures::vector_cmp( const verti vec1[],
      25             :                                               const verti vec2[], int N ) const
      26             : {
      27           0 :     if (is_top(vec1)) return is_top(vec2) ? 0 : +1;  // v is top
      28           0 :     if (is_top(vec2)) return -1;                     // w is top, but v isn't
      29             : 
      30           0 :     for (int n = 0; n < N; ++n)
      31             :     {
      32           0 :         if (vec1[n] < vec2[n]) return -1;
      33           0 :         if (vec1[n] > vec2[n]) return +1;
      34             :     }
      35             : 
      36           0 :     return 0;
      37             : }
      38             : 
      39           0 : inline verti SmallProgressMeasures::get_ext_succ(verti v, bool take_max) const
      40             : {
      41           0 :     const verti *it  = game_.graph().succ_begin(v),
      42           0 :                 *end = game_.graph().succ_end(v);
      43             : 
      44           0 :     assert(it < end);  /* assume we have at least one successor */
      45             : 
      46           0 :     int N = len(v);
      47           0 :     verti res = *it++;
      48           0 :     for ( ; it != end; ++it)
      49             :     {
      50           0 :         int d = vector_cmp(*it, res, N);
      51           0 :         if (take_max ? d > 0 : d < 0) res = *it;
      52             :     }
      53           0 :     return res;
      54             : }
      55             : 
      56             : template<class OutputIterator>
      57           0 : void SmallProgressMeasures::get_winning_set( ParityGame::Player player,
      58             :                                              OutputIterator result )
      59             : {
      60           0 :     const StaticGraph& graph = game_.graph();
      61           0 :     const verti V = graph.V();
      62             : 
      63           0 :     if (player == p_)
      64             :     {
      65             :         // Conservatively estimate vertices won by player.
      66           0 :         std::vector<char> marked(V, 0);
      67           0 :         std::vector<char> queued(V, 0);
      68           0 :         std::deque<int> dirty;
      69           0 :         for (verti v = 0; v < V; ++v)
      70             :         {
      71           0 :             if (is_top(v))
      72             :             {
      73           0 :                 marked[v] = true;
      74             :             }
      75             :             else
      76             :             {
      77           0 :                 queued[v] = true;
      78           0 :                 dirty.push_back(v);
      79             :             }
      80             :         }
      81           0 :         while (!dirty.empty())
      82             :         {
      83           0 :             const verti v = dirty.front();
      84           0 :             dirty.pop_front();
      85           0 :             assert(queued[v] && !marked[v]);
      86           0 :             queued[v] = false;
      87           0 :             if (game_.player(v) == p_)
      88             :             {
      89             :                 // Look for an unmarked successor with a progress value
      90             :                 // less than (or equal to, if priority is even) that of v:
      91           0 :                 bool mark = true;
      92           0 :                 for ( StaticGraph::const_iterator it = graph.succ_begin(v);
      93           0 :                       it != graph.succ_end(v); ++it )
      94             :                 {
      95           0 :                     if ( !marked[*it] && vector_cmp(v, *it, len(v))
      96           0 :                             >= (int) (game_.priority(v)%2 ^ p_) )
      97             :                     {
      98           0 :                         mark = false;
      99           0 :                         break;
     100             :                     }
     101             :                 }
     102           0 :                 marked[v] = mark;
     103             :             }
     104             :             else  // v is controlled by opponent
     105             :             {
     106             :                 // Look for a marked successor, or an unmarked one with a
     107             :                 // progress value less than (or equal to, if priority is
     108             :                 // even) that of v:
     109           0 :                 for ( StaticGraph::const_iterator it = graph.succ_begin(v);
     110           0 :                       it != graph.succ_end(v); ++it )
     111             :                 {
     112           0 :                     const verti w = *it;
     113           0 :                     if ( marked[*it] || vector_cmp(v, w, len(v))
     114           0 :                             < (int) (game_.priority(v)%2 ^ p_) )
     115             :                     {
     116           0 :                         marked[v] = true;
     117           0 :                         break;
     118             :                     }
     119             :                 }
     120             :             }
     121           0 :             if (marked[v])
     122             :             {
     123             :                 // Mark possibly losing vertex and queue its predecessors:
     124           0 :                 for ( StaticGraph::const_iterator it = graph.pred_begin(v);
     125           0 :                       it != graph.pred_end(v); ++it )
     126             :                 {
     127           0 :                     if (!marked[*it] && !queued[*it])
     128             :                     {
     129           0 :                         queued[*it] = true;
     130           0 :                         dirty.push_back(*it);
     131             :                     }
     132             :                 }
     133             :             }
     134             :         }
     135             :         // Now collect guaranteed winning vertices:
     136           0 :         for (verti v = 0; v < V; ++v)
     137             :         {
     138           0 :             if (!marked[v]) *result++ = v;
     139             :         }
     140           0 :     }
     141             :     else
     142             :     {
     143             :         // All vertices with Top progress measures are won by opponent:
     144           0 :         for (verti v = 0; v < V; ++v)
     145             :         {
     146           0 :             if (is_top(v)) *result++ = v;
     147             :         }
     148             :     }
     149           0 : }
     150             : 
     151           0 : bool SmallProgressMeasures::lift_to_top(verti v)
     152             : {
     153           0 :     if (is_top(v)) return false;
     154           0 :     set_top(v);
     155           0 :     return true;
     156             : }
     157             : 
     158           0 : void SmallProgressMeasures::set_top(verti v)
     159             : {
     160           0 :     assert(!is_top(v));
     161           0 :     set_vec_to_top(v);
     162           0 :     std::size_t prio = game_.priority(v);
     163           0 :     if (prio%2 != p_) decr_M(prio/2);
     164           0 : }
     165             : 
     166             : #endif // MCRL2_PG_SMALLPROGRESSMEASURES_IMPL_H

Generated by: LCOV version 1.14