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/pbes/io.h"
11 : #include "mcrl2/pbes/parity_game_generator.h"
12 : #include "mcrl2/pg/ParityGame.h"
13 :
14 : /* N.B. The PGSolver I/O functions reverse the priorities when reading/writing
15 : the game description. This is done to preserve solutions, since PGSolver
16 : considers higher values to dominate lower values, while I assume the opposite
17 : (i.e. 0 is the `highest` priority) throughout the rest of the code. */
18 :
19 0 : void ParityGame::read_pgsolver( std::istream &is,
20 : StaticGraph::EdgeDirection edge_dir )
21 : {
22 0 : priority_t max_prio = 0;
23 0 : std::vector<ParityGameVertex> vertices;
24 0 : StaticGraph::edge_list edges;
25 :
26 : // Read "parity" header line (if present)
27 0 : char ch = 0;
28 0 : while (!isalnum(ch)) is.get(ch);
29 0 : is.putback(ch);
30 0 : if (!isdigit(ch))
31 : {
32 0 : std::string parity;
33 : verti max_vertex;
34 :
35 0 : if (!(is >> parity >> max_vertex)) return;
36 0 : if (parity != "parity") return;
37 0 : vertices.reserve(max_vertex + 1);
38 :
39 : // Skip to terminating semicolon
40 0 : while (is.get(ch) && ch != ';') ch = 0;
41 0 : }
42 :
43 : // Read and discard "start" line (if present)
44 0 : while (!isalnum(ch)) is.get(ch);
45 0 : is.putback(ch);
46 0 : if (!isdigit(ch))
47 : {
48 0 : std::string start;
49 : verti vertex;
50 :
51 0 : if (!(is >> start >> vertex)) return;
52 0 : if (start != "start") return;
53 :
54 : // Skip to terminating semicolon
55 0 : while (is.get(ch) && ch != ';') ch = 0;
56 0 : }
57 :
58 : // Invalid vertex (used to mark uninitialized vertices)
59 0 : ParityGameVertex invalid = { PLAYER_EVEN, (priority_t)-1 };
60 :
61 : // Read vertex specs
62 0 : while (is)
63 : {
64 : verti id;
65 : int prio_raw, player_raw;
66 :
67 0 : if (!(is >> id >> prio_raw >> player_raw)) break;
68 :
69 0 : assert(prio_raw >= 0);
70 0 : assert(prio_raw < 65536);
71 0 : priority_t prio = prio_raw;
72 :
73 0 : assert(player_raw == 0 || player_raw == 1);
74 0 : player_t player = static_cast<player_t>(player_raw);
75 :
76 0 : if (prio > max_prio) max_prio = prio;
77 0 : if (id >= vertices.size()) vertices.resize(id + 1, invalid);
78 :
79 : /* FIXME: the PGSolver file format description allows vertices to be
80 : defined more than once (in that case, the old vertex should
81 : be removed), but we currently don't support that. Instead,
82 : just assert that each vertex is initialized once. */
83 0 : assert(vertices[id] == invalid);
84 :
85 0 : vertices[id].player = player;
86 0 : vertices[id].priority = prio;
87 :
88 : // Read successors
89 : do {
90 : verti succ;
91 0 : if (!(is >> succ)) break;
92 0 : if (succ >= vertices.size()) vertices.resize(succ + 1, invalid);
93 :
94 0 : edges.push_back(std::make_pair(id, succ));
95 :
96 : // Skip to separator (comma) or end-of-list (semicolon), while
97 : // ignoring the contents of quoted strings.
98 0 : bool quoted = false, escaped = false;
99 0 : while (is.get(ch)) {
100 0 : if (ch == '"' && !escaped) quoted = !quoted;
101 0 : escaped = ch == '\\' && !escaped;
102 0 : if ((ch == ',' || ch == ';') && !quoted) break;
103 : }
104 :
105 0 : } while (is && ch == ',');
106 : }
107 :
108 : // Ensure max_prio is even, so max_prio - p preserves parity:
109 0 : if (max_prio%2 == 1) ++max_prio;
110 :
111 : // Look for unused vertex indices:
112 0 : std::vector<verti> vertex_map(vertices.size(), NO_VERTEX);
113 0 : verti used = 0;
114 0 : for (verti v = 0; v < (verti)vertices.size(); ++v)
115 : {
116 0 : if (vertices[v] != invalid) {
117 0 : vertices[used] = vertices[v];
118 0 : vertex_map[v] = used++;
119 : }
120 : }
121 0 : if (used < (verti)vertices.size())
122 : {
123 : // Remove unused vertices:
124 0 : vertices.erase(vertices.begin() + used, vertices.end());
125 :
126 : // Remap edges to new vertex indices:
127 0 : for ( StaticGraph::edge_list::iterator it = edges.begin();
128 0 : it != edges.end(); ++it )
129 : {
130 0 : it->first = vertex_map[it->first];
131 0 : it->second = vertex_map[it->second];
132 0 : assert(it->first != NO_VERTEX && it->second != NO_VERTEX);
133 : }
134 : }
135 :
136 : // Assign vertex info and recount cardinalities
137 0 : reset((verti)vertices.size(), max_prio + 1);
138 0 : for (std::size_t n = 0; n < vertices.size(); ++n)
139 : {
140 0 : assert(vertices[n] != invalid);
141 0 : vertex_[n].player = vertices[n].player;
142 0 : vertex_[n].priority = max_prio - vertices[n].priority;
143 : }
144 0 : recalculate_cardinalities(vertices.size());
145 0 : vertices.clear();
146 :
147 : // Assign graph
148 0 : graph_.assign(edges, edge_dir);
149 0 : }
150 :
151 0 : void ParityGame::write_pgsolver(std::ostream &os) const
152 : {
153 : // Get max priority and make it even so max_prio - p preserves parity:
154 0 : int max_prio = d();
155 0 : if (max_prio%2 == 1) --max_prio;
156 :
157 : // Write out graph
158 0 : os << "parity " << (long long)graph_.V() - 1 << ";\n";
159 0 : for (verti v = 0; v < graph_.V(); ++v)
160 : {
161 0 : os << v << ' ' << (max_prio - priority(v)) << ' ' << player(v);
162 0 : StaticGraph::const_iterator it = graph_.succ_begin(v),
163 0 : end = graph_.succ_end(v);
164 0 : assert(it < end);
165 0 : os << ' ' << *it++;
166 0 : while (it != end) os << ',' << *it++;
167 0 : os << ";\n";
168 : }
169 0 : }
170 :
171 0 : void ParityGame::read_pbes( const std::string &file_path, verti *goal_vertex,
172 : StaticGraph::EdgeDirection edge_dir,
173 : const std::string &rewrite_strategy )
174 : {
175 0 : mcrl2::pbes_system::pbes pbes;
176 0 : load_pbes(pbes, file_path);
177 0 : assign_pbes(pbes, goal_vertex, edge_dir, rewrite_strategy);
178 0 : }
179 :
180 0 : void ParityGame::assign_pbes(mcrl2::pbes_system::pbes &pbes, verti *goal_vertex,
181 : StaticGraph::EdgeDirection edge_dir,
182 : const std::string &rewrite_strategy)
183 : {
184 : /* NOTE: this code assumes the vertices generated by parity_game_generator
185 : are numbered from 2 to num_vertices-1 with no gaps, with 0 and 1
186 : representing true and false (respectively) and 2 representing the
187 : initial condition. */
188 :
189 0 : if (goal_vertex) *goal_vertex = 2;
190 :
191 : // Generate min-priority parity game
192 : mcrl2::pbes_system::parity_game_generator pgg( pbes, true, true,
193 0 : mcrl2::data::parse_rewrite_strategy(rewrite_strategy) );
194 :
195 : // Build the edge list
196 0 : StaticGraph::edge_list edges;
197 0 : verti begin = 0, end = 3;
198 0 : for (verti v = begin; v < end; ++v)
199 : {
200 0 : std::set<std::size_t> deps = pgg.get_dependencies(v);
201 0 : for ( std::set<std::size_t>::const_iterator it = deps.begin();
202 0 : it != deps.end(); ++it )
203 : {
204 0 : verti w = (verti)*it;
205 0 : assert(w >= begin);
206 0 : if (w >= end) end = w + 1;
207 0 : edges.push_back(std::make_pair(v - begin, w - begin));
208 : }
209 0 : }
210 :
211 : // Determine maximum prioirity
212 0 : int max_prio = 0;
213 0 : for (verti v = begin; v < end; ++v)
214 : {
215 0 : max_prio = std::max(max_prio, (int)pgg.get_priority(v));
216 : }
217 :
218 : // Assign vertex info and recount cardinalities
219 0 : reset(end - begin, max_prio + 1);
220 0 : for (verti v = begin; v < end; ++v)
221 : {
222 0 : bool and_op = pgg.get_operation(v) ==
223 0 : mcrl2::pbes_system::parity_game_generator::PGAME_AND;
224 0 : vertex_[v - begin].player = and_op ? PLAYER_ODD : PLAYER_EVEN;
225 0 : vertex_[v - begin].priority = pgg.get_priority(v);
226 : }
227 0 : recalculate_cardinalities(end - begin);
228 :
229 : // Assign graph
230 0 : graph_.assign(edges, edge_dir);
231 0 : }
232 :
233 0 : void ParityGame::read_raw(std::istream &is)
234 : {
235 0 : graph_.read_raw(is);
236 0 : assert(is.good());
237 : int d;
238 0 : is.read((char*)&d, sizeof(d));
239 0 : reset(graph_.V(), d);
240 0 : is.read((char*)vertex_, sizeof(ParityGameVertex)*graph_.V());
241 0 : is.read((char*)cardinality_, sizeof(verti)*d);
242 0 : }
243 :
244 0 : void ParityGame::write_raw(std::ostream &os) const
245 : {
246 0 : graph_.write_raw(os);
247 0 : assert(os.good());
248 0 : os.write((const char*)&d_, sizeof(d_));
249 0 : os.write((const char*)vertex_, sizeof(ParityGameVertex)*graph_.V());
250 0 : os.write((const char*)cardinality_, sizeof(verti)*d_);
251 0 : }
252 :
253 0 : void ParityGame::write_dot(std::ostream &os) const
254 : {
255 0 : os << "digraph {\n";
256 0 : for (verti v = 0; v < graph_.V(); ++v)
257 : {
258 0 : bool even = player(v) == PLAYER_EVEN;
259 0 : os << v << " ["
260 : << "shape=" << (even ? "diamond" : "box") << ", "
261 0 : << "label=\"" << priority(v) << " (" << v << ")\"]\n";
262 :
263 0 : if (graph_.edge_dir() & StaticGraph::EDGE_SUCCESSOR)
264 : {
265 0 : for ( StaticGraph::const_iterator it = graph_.succ_begin(v);
266 0 : it != graph_.succ_end(v); ++it )
267 : {
268 0 : os << v << " -> " << *it;
269 : // if (*it < v) os << " [color=red]";
270 0 : os << ";\n";
271 : }
272 : }
273 : else
274 : {
275 0 : for ( StaticGraph::const_iterator it = graph_.pred_begin(v);
276 0 : it != graph_.pred_end(v); ++it )
277 : {
278 0 : os << *it << " -> " << v << ";\n";
279 : }
280 : }
281 : }
282 0 : os << "}\n";
283 0 : }
284 :
285 0 : void ParityGame::write_debug(const Strategy &s, std::ostream &os) const
286 : {
287 0 : for (verti v = 0; v < graph_.V(); ++v)
288 : {
289 0 : os << v << ' ';
290 :
291 : // Print controlling player and vertex priority:
292 0 : char l = ' ', r = ' ';
293 0 : if (player(v) == PLAYER_EVEN) l = '<', r = '>';
294 0 : if (player(v) == PLAYER_ODD) l = '[', r = ']';
295 0 : os << l << priority(v) << r;
296 :
297 : // Print outgoing edges:
298 0 : char sep = ' ';
299 0 : for (StaticGraph::const_iterator it = graph_.succ_begin(v);
300 0 : it != graph_.succ_end(v); ++it)
301 : {
302 0 : os << sep << *it;
303 0 : sep = ',';
304 : }
305 :
306 : // Print strategy (if applicable)
307 0 : if (!s.empty() && s.at(v) != NO_VERTEX) os << " -> " << s.at(v);
308 :
309 0 : os << '\n';
310 : }
311 0 : os << std::flush;
312 0 : }
|