Line data Source code
1 : // Author(s): Jeroen Keiren, 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/bes/pg_parse.h
10 : /// \brief Parsing of parity games in the format used by PGSolver.
11 :
12 : #ifndef MCRL2_BES_PG_PARSE_H
13 : #define MCRL2_BES_PG_PARSE_H
14 :
15 : #include <fstream>
16 :
17 : #include "mcrl2/core/parser_utility.h"
18 : #include "mcrl2/pbes/pbes.h"
19 : #include "mcrl2/pbes/join.h"
20 :
21 : extern "C"
22 : {
23 : extern D_ParserTables parser_tables_pg;
24 : }
25 :
26 : namespace mcrl2
27 : {
28 :
29 : namespace pbes_system
30 : {
31 :
32 : typedef unsigned long long identifier_t;
33 : typedef unsigned short priority_t;
34 :
35 : typedef bool owner_t;
36 :
37 : struct node_t
38 : {
39 : identifier_t id;
40 : priority_t prio;
41 : owner_t owner;
42 : std::set<identifier_t> successors;
43 :
44 : bool operator<(node_t const& other)
45 : {
46 : return id < other.id;
47 : }
48 : };
49 :
50 : // Build a formula from the strings in v. if p = 0, than a disjunction is built,
51 : // otherwise the result is a conjunction.
52 : // Prefix is added to each of the identifiers in v.
53 : inline
54 128 : pbes_expression formula(std::set<identifier_t> const& v, const owner_t owner, const std::string& prefix = "X")
55 : {
56 128 : std::set<pbes_expression> v_prefixed;
57 352 : for (identifier_t i: v)
58 : {
59 224 : std::stringstream id;
60 224 : id << prefix << i;
61 224 : v_prefixed.insert(propositional_variable_instantiation(id.str()));
62 224 : }
63 :
64 128 : if (owner == 0)
65 : {
66 40 : return join_or(v_prefixed.begin(), v_prefixed.end());
67 : }
68 : else
69 : {
70 88 : return join_and(v_prefixed.begin(), v_prefixed.end());
71 : }
72 128 : }
73 :
74 : struct pg_actions: public core::default_parser_actions
75 : {
76 : // Parse node specifications (store in map)
77 : std::map<identifier_t, node_t> game;
78 : identifier_t initial_node;
79 :
80 4 : pg_actions(const core::parser& parser_)
81 4 : : core::default_parser_actions(parser_),
82 4 : initial_node((std::numeric_limits<identifier_t>::max)())
83 4 : {}
84 :
85 : template <typename T, typename Function>
86 : std::set<T> parse_set(const core::parse_node& node, const std::string& type, Function f)
87 : {
88 : std::set<T> result;
89 : traverse(node, make_set_collector(m_parser, type, result, f));
90 : return result;
91 : }
92 :
93 4 : void create_boolean_equation_system(pbes& b, bool maxpg)
94 : {
95 : // Build Boolean equation system. First we group equations by block
96 4 : std::map<priority_t, std::set<pbes_equation> > blocks;
97 : // Translation scheme:
98 : // prefix every id with X. Owner 0 means ||, owner 1 means &&
99 :
100 132 : for (std::map<identifier_t, node_t>::const_iterator i = game.begin(); i != game.end(); ++i)
101 : {
102 128 : std::stringstream id;
103 128 : id << "X" << i->second.id;
104 :
105 128 : fixpoint_symbol fp(fixpoint_symbol::mu());
106 128 : if (i->second.prio % 2 == 0)
107 : {
108 64 : fp = fixpoint_symbol::nu();
109 : }
110 :
111 256 : pbes_equation eqn(fp, propositional_variable(id.str()), formula(i->second.successors, i->second.owner));
112 :
113 128 : blocks[i->second.prio].insert(eqn);
114 128 : }
115 :
116 4 : std::vector<pbes_equation> eqns;
117 4 : if(maxpg)
118 : {
119 16 : for (std::map<priority_t, std::set<pbes_equation> >::reverse_iterator i = blocks.rbegin(); i != blocks.rend(); ++i)
120 : {
121 12 : eqns.insert(eqns.end(), i->second.begin(), i->second.end());
122 : }
123 : }
124 : else
125 : {
126 0 : for (std::map<priority_t, std::set<pbes_equation> >::const_iterator i = blocks.begin(); i != blocks.end(); ++i)
127 : {
128 0 : eqns.insert(eqns.end(), i->second.begin(), i->second.end());
129 : }
130 : }
131 :
132 4 : b.equations() = eqns;
133 4 : std::stringstream init_id;
134 4 : init_id << initial_node;
135 4 : b.initial_state() = propositional_variable_instantiation("X" + init_id.str());
136 4 : }
137 :
138 4 : void parse_ParityGame(const core::parse_node& node, pbes& result, bool maxpg)
139 : {
140 4 : if(node.child_count() == 5)
141 : {
142 :
143 0 : initial_node = parse_Id(node.child(3));
144 : }
145 4 : if(node.child_count() == 3 && node.child(0).string() == "start")
146 : {
147 0 : initial_node = parse_Id(node.child(1));
148 : }
149 :
150 4 : game.clear();
151 4 : parse_NodeSpecList(node.child(node.child_count()-1));
152 4 : create_boolean_equation_system(result, maxpg);
153 4 : }
154 :
155 128 : void parse_NodeSpec(const core::parse_node& node)
156 : {
157 128 : node_t result;
158 128 : result.id = parse_Id(node.child(0));
159 128 : result.prio = parse_Priority(node.child(1));
160 128 : result.owner = parse_Owner(node.child(2));
161 128 : result.successors = parse_Successors(node.child(3));
162 128 : if (game.empty() && initial_node == (std::numeric_limits<identifier_t>::max)())
163 : {
164 4 : initial_node = result.id;
165 : }
166 128 : game[result.id] = result;
167 128 : }
168 :
169 4 : void parse_NodeSpecList(const core::parse_node& node)
170 : {
171 132 : traverse(node, make_visitor(m_parser.symbol_table(), "NodeSpec", [&](const core::parse_node& node) { return parse_NodeSpec(node); }));
172 4 : }
173 :
174 352 : identifier_t parse_Id(const core::parse_node& node)
175 : {
176 352 : return parse_Number<identifier_t>(node.child(0));
177 : }
178 :
179 128 : priority_t parse_Priority(const core::parse_node& node)
180 : {
181 128 : return parse_Number<priority_t>(node.child(0));
182 : }
183 :
184 128 : bool parse_Owner(const core::parse_node& node)
185 : {
186 128 : return node.string() == "1";
187 : }
188 :
189 128 : std::set<identifier_t> parse_Successors(const core::parse_node& node)
190 : {
191 128 : std::set<identifier_t> result;
192 352 : traverse(node, make_set_collector(m_parser.symbol_table(), "Id", result, [&](const core::parse_node& node) { return parse_Id(node); }));
193 128 : return result;
194 0 : }
195 :
196 : template <typename T>
197 480 : T parse_Number(const core::parse_node& node)
198 : {
199 : T result;
200 480 : std::stringstream tmp;
201 480 : tmp << node.string();
202 480 : tmp >> result;
203 480 : return result;
204 480 : }
205 : };
206 :
207 : /// \brief Reads a parity game from an input stream, and stores it as a BES.
208 : /// \param text A string
209 : /// \param result A boolean equation system
210 : /// \param maxpg If true a max-parity game is generated in \a result, otherwise a min-parity
211 : /// game is obtained.
212 : inline
213 4 : void parse_pgsolver_string(const std::string& text, pbes& result, bool maxpg = true)
214 : {
215 4 : core::parser p(parser_tables_pg);
216 4 : unsigned int start_symbol_index = p.start_symbol_index("ParityGame");
217 4 : bool partial_parses = false;
218 4 : core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
219 4 : pg_actions(p).parse_ParityGame(node, result, maxpg);
220 4 : }
221 :
222 : /// \brief Reads a parity game from an input stream, and stores it as a BES.
223 : /// \param from An input stream
224 : /// \param result A boolean equation system
225 : /// \param maxpg If true a max-parity game is generated in \a result, otherwise a min-parity
226 : /// game is obtained.
227 : inline
228 4 : void parse_pgsolver(std::istream& from, pbes& result, bool maxpg = true)
229 : {
230 4 : std::string text = utilities::read_text(from);
231 4 : parse_pgsolver_string(text, result, maxpg);
232 4 : }
233 :
234 : /// \brief Parse parity game in PGSolver format from filename, and store the
235 : /// resulting BES in b.
236 : inline void parse_pgsolver(const std::string& filename, pbes& b, bool maxpg = true)
237 : {
238 : if(filename == "-" || filename.empty())
239 : {
240 : parse_pgsolver(std::cin, b, maxpg);
241 : }
242 : else
243 : {
244 : std::ifstream f;
245 : f.open(filename.c_str());
246 : if(!f)
247 : {
248 : throw mcrl2::runtime_error("cannot open file " + filename + " for reading");
249 : }
250 : parse_pgsolver(f, b, maxpg);
251 : }
252 : }
253 :
254 : } // namespace pbes_system
255 :
256 : } // namespace mcrl2
257 :
258 : #endif // MCRL2_BES_PG_PARSE_H
|
