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