Line data Source code
1 : // Author(s): Wieger Wesselink
2 : // Copyright: see the accompanying file COPYING or copy at
3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4 : //
5 : // Distributed under the Boost Software License, Version 1.0.
6 : // (See accompanying file LICENSE_1_0.txt or copy at
7 : // http://www.boost.org/LICENSE_1_0.txt)
8 : //
9 : /// \file mcrl2/pbes/detail/parity_game_output.h
10 : /// \brief add your file description here.
11 :
12 : #include "mcrl2/pbes/parity_game_generator.h"
13 : #include <boost/algorithm/string/join.hpp>
14 :
15 : #ifndef MCRL2_PBES_DETAIL_PARITY_GAME_OUTPUT_H
16 : #define MCRL2_PBES_DETAIL_PARITY_GAME_OUTPUT_H
17 :
18 : namespace mcrl2
19 : {
20 :
21 : namespace pbes_system
22 : {
23 :
24 : namespace detail
25 : {
26 :
27 : /// A class that generates python code for a parity game, such
28 : /// that it can be solved with a parity game solver written in
29 : /// python.
30 : class parity_game_output: public parity_game_generator
31 : {
32 : protected:
33 : /// The vertices of the parity game graph.
34 : std::set<std::size_t> V;
35 :
36 : /// The edges of the parity game graph.
37 : std::set<std::pair<std::size_t, std::size_t> > E;
38 :
39 : /// The vertex priorities of the parity game graph.
40 : std::map<std::size_t, std::size_t> priorities;
41 :
42 : /// The even vertices of the parity game graph.
43 : std::set<std::size_t> even_vertices;
44 :
45 : /// The odd vertices of the parity game graph.
46 : std::set<std::size_t> odd_vertices;
47 :
48 : /// \brief Returns the quoted name of the vertex, for example "X1"
49 : /// \param i A positive integer
50 : /// \return The quoted name of the vertex, for example "X1"
51 : std::string vertex(std::size_t i) const
52 : {
53 : return "\"X" + utilities::number2string(i+1) + "\"";
54 : }
55 :
56 : /// \brief Returns a tuple representing an edge, for example ("X1", "X2")
57 : /// \param e An edge
58 : /// \return A tuple representing an edge, for example ("X1", "X2")
59 : std::string edge(std::pair<std::size_t, std::size_t> e) const
60 : {
61 : return "(" + vertex(e.first) + ", " + vertex(e.second) + ")";
62 : }
63 :
64 : /// \brief Returns a string representing a priority, for example "X1":0
65 : /// \param p A pair of integers
66 : /// \return A string representing a priority, for example "X1":0
67 : std::string priority(std::pair<std::size_t, std::size_t> p) const
68 : {
69 : return vertex(p.first) + ":" + utilities::number2string(p.second);
70 : }
71 :
72 : /// \brief Applies a function to the elements of a container
73 : /// \param c A container
74 : /// \param f A function
75 : /// \return The transformed container
76 : template <typename Container, typename Function>
77 : std::vector<std::string> apply(const Container& c, const Function& f) const
78 : {
79 : std::vector<std::string> result;
80 : for (auto i = c.begin(); i != c.end(); ++i)
81 : {
82 : result.push_back(f(*i));
83 : }
84 : return result;
85 : }
86 :
87 : /// \brief Prints the elements of a container with a separator between them
88 : /// \param c A container
89 : /// \param sep A string
90 : /// \return The joined elements
91 : template <typename Container>
92 : std::string join(const Container& c, const std::string& sep) const
93 : {
94 : std::ostringstream out;
95 : for (auto i = c.begin(); i != c.end(); ++i)
96 : {
97 : out << (i == c.begin() ? "" : sep) << *i;
98 : }
99 : return out.str();
100 : }
101 :
102 : /// \brief Wraps a sequence of strings in a Python set.
103 : /// \param elements A vector of strings
104 : /// \return The Python set representation
105 : std::string python_set(const std::vector<std::string>& elements) const
106 : {
107 : return "set([" + join(elements, ", ") + "])";
108 : }
109 :
110 : /// \brief Prints the todo list
111 : /// \param name A string
112 : /// \param todo A todo list
113 : void print_set(const std::string& name, const std::set<std::size_t>& todo) const
114 : {
115 : mCRL2log(log::verbose) << name << " = {";
116 : for (auto i = todo.begin(); i != todo.end(); ++i)
117 : {
118 : mCRL2log(log::verbose) << (i == todo.begin() ? "" : ", ") << *i;
119 : }
120 : mCRL2log(log::verbose) << "}" << std::endl;
121 : }
122 :
123 : public:
124 12 : explicit parity_game_output(pbes& p, bool min_parity_game = true)
125 12 : : parity_game_generator(p, true, min_parity_game)
126 12 : {}
127 :
128 : // Example:
129 : // set(["X1", "X2", "X3", "X4", "X5"])
130 : // set([("X1", "X2"), ("X2", "X1"), ("X2", "X3"), ("X3", "X4"), ("X3", "X5"), ("X4", "X1"), ("X5", "X3"), ("X5", "X1")])
131 : // {"X1":0, "X2":1, "X3":2, "X4":1, "X5":3}
132 : // set(["X3", "X4"])
133 : // set(["X1", "X2", "X5"])
134 : //
135 : // Line 1: set of vertices
136 : // Line 2: set of edges
137 : // Line 3: dictionary of priorities
138 : // Line 4: set of vertices for player even
139 : // Line 5: set of vertices for player oneven
140 : /// \brief Returns a representation of the parity game in python format.
141 : /// This code is used as input for a python parity game solver.
142 : /// \return A representation of the parity game in python format.
143 : std::string python_graph()
144 : {
145 : std::string result;
146 : result = result + python_set(apply(V, [&](std::size_t i) { return vertex(i); })) + "\n";
147 : result = result + python_set(apply(E, [&](std::pair<std::size_t, std::size_t> e) { return edge(e); })) + "\n";
148 : result = result + "{" + join(apply(priorities, [&](std::pair<std::size_t, std::size_t> p) { return priority(p); }), ", ") + "}\n";
149 : result = result + python_set(apply(even_vertices, [&](std::size_t i) { return vertex(i); })) + "\n";
150 : result = result + python_set(apply(odd_vertices, [&](std::size_t i) { return vertex(i); }));
151 : return result;
152 : }
153 :
154 : /// \brief Returns a representation of the parity game in Alpaga format.
155 : /// \return A representation of the parity game in Alpaga format.
156 : std::string pgsolver_graph()
157 : {
158 : std::vector<std::string> lines(V.size());
159 : for (std::size_t k: V)
160 : {
161 : lines[k] = std::to_string(k) + " " + utilities::number2string(priorities[k]) + " " + (odd_vertices.find(k) == odd_vertices.end() ? "0 " : "1 ");
162 : }
163 : for (const auto& i: E)
164 : {
165 : std::size_t k = i.first;
166 : std::size_t m = i.second;
167 : std::string& line = lines[k];
168 : line += ((line[line.size()-1] == ' ' ? "" : ", ") + utilities::number2string(m));
169 : }
170 : return join(lines, ";\n") + ";";
171 : }
172 :
173 : /// \brief Generates the parity game graph
174 12 : void run()
175 : {
176 12 : std::set<std::size_t> todo = get_initial_values();
177 12 : std::set<std::size_t> done;
178 135 : while (!todo.empty())
179 : {
180 : // handle vertex i
181 123 : std::size_t i = *todo.begin();
182 123 : todo.erase(i);
183 123 : done.insert(i);
184 123 : V.insert(i);
185 123 : std::size_t p = get_priority(i);
186 123 : priorities[i] = p;
187 123 : std::set<std::size_t> dep_i = get_dependencies(i);
188 123 : switch (get_operation(i))
189 : {
190 36 : case PGAME_AND:
191 36 : odd_vertices.insert(i);
192 36 : break;
193 87 : case PGAME_OR:
194 87 : even_vertices.insert(i);
195 87 : break;
196 0 : default:
197 0 : assert(false);
198 : }
199 :
200 272 : for (std::size_t j: dep_i)
201 : {
202 : // handle edge (i, *j)
203 149 : E.insert(std::make_pair(i, j));
204 149 : if (done.find(j) == done.end())
205 : {
206 92 : todo.insert(j);
207 : }
208 : }
209 123 : }
210 12 : }
211 : };
212 :
213 : } // namespace detail
214 :
215 : } // namespace pbes_system
216 :
217 : } // namespace mcrl2
218 :
219 : #endif // MCRL2_PBES_DETAIL_PARITY_GAME_OUTPUT_H
|
