Line data Source code
1 : // Author(s): Gijs Kant
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/pbes_explorer.cpp
10 : /// \brief
11 : #include <climits>
12 : #include <queue>
13 :
14 : #include "mcrl2/data/detail/io.h"
15 : #include "mcrl2/data/representative_generator.h"
16 : #include "mcrl2/pbes/detail/ppg_visitor.h"
17 : #include "mcrl2/pbes/io.h"
18 : #include "mcrl2/pbes/pbes_explorer.h"
19 :
20 :
21 : namespace mcrl2
22 : {
23 :
24 : namespace pbes_system
25 : {
26 :
27 : namespace detail
28 : {
29 : template <typename MapContainer>
30 19364 : typename MapContainer::mapped_type map_at(const MapContainer& m, typename MapContainer::key_type key)
31 : {
32 19364 : typename MapContainer::const_iterator i = m.find(key);
33 19364 : if (i == m.end())
34 : {
35 0 : throw mcrl2::runtime_error("map_at: key is not present in the map: " + key);
36 : }
37 36996 : return i->second;
38 : }
39 : } // namespace detail
40 :
41 : /// lts_type
42 :
43 12 : lts_type::lts_type(int state_length)
44 : {
45 12 : this->state_length = state_length;
46 12 : }
47 :
48 :
49 12 : lts_type::~lts_type()
50 12 : {}
51 :
52 :
53 13730 : int lts_type::get_state_length() const
54 : {
55 13730 : return this->state_length;
56 : }
57 :
58 :
59 18 : std::size_t lts_type::get_number_of_state_types() const
60 : {
61 18 : return this->state_type_list.size();
62 : }
63 :
64 :
65 27696 : int lts_type::get_state_type_no(int part) const
66 : {
67 27696 : return this->state_type_no.at(part);
68 : }
69 :
70 0 : std::string lts_type::get_state_type_name(int type_no) const
71 : {
72 0 : return this->state_type_list.at(type_no);
73 : }
74 :
75 76 : const std::vector<std::string>& lts_type::get_state_names() const
76 : {
77 76 : return state_names;
78 : }
79 :
80 :
81 0 : const std::vector<std::string>& lts_type::get_state_types() const
82 : {
83 0 : return state_types;
84 : }
85 :
86 :
87 0 : std::size_t lts_type::get_number_of_state_labels() const
88 : {
89 0 : return this->state_label_names.size();
90 : }
91 :
92 :
93 0 : const std::vector<std::string>& lts_type::get_state_labels() const
94 : {
95 0 : return state_label_names;
96 : }
97 :
98 :
99 0 : const std::vector<std::string>& lts_type::get_state_label_types() const
100 : {
101 0 : return state_label_types;
102 : }
103 :
104 :
105 0 : std::size_t lts_type::get_number_of_edge_labels() const
106 : {
107 0 : return this->edge_label_names.size();
108 : }
109 :
110 :
111 0 : const std::vector<std::string>& lts_type::get_edge_labels() const
112 : {
113 0 : return edge_label_names;
114 : }
115 :
116 :
117 0 : const std::vector<std::string>& lts_type::get_edge_label_types() const
118 : {
119 0 : return edge_label_types;
120 : }
121 :
122 :
123 20 : void lts_type::add_state(const std::string& name, const std::string& type)
124 : {
125 : //std::clog << "Adding state part " << this->state_names->size() << ": "
126 : // << info::get_param_signature(name, type)
127 : // << std::endl;
128 20 : this->state_names.push_back(name);
129 20 : this->state_types.push_back(type);
130 : std::size_t type_index;
131 20 : std::map<std::string,int>::iterator type_index_it = this->state_type_index.find(type);
132 20 : if (type_index_it != this->state_type_index.end()) {
133 8 : type_index = type_index_it->second;
134 : } else {
135 12 : this->state_type_list.push_back(type);
136 12 : type_index = this->state_type_list.size() - 1;
137 12 : this->state_type_index[type] = type_index;
138 : }
139 20 : this->state_type_no.push_back(type_index);
140 : //std::clog << " type_no = " << type_index << ": " << this->state_type_list->at(type_index) << std::endl;
141 20 : }
142 :
143 :
144 12 : void lts_type::add_state_label(const std::string& name,
145 : const std::string& type)
146 : {
147 12 : this->state_label_names.push_back(name);
148 12 : this->state_label_types.push_back(type);
149 12 : }
150 :
151 :
152 0 : void lts_type::add_edge_label(const std::string& name,
153 : const std::string& type)
154 : {
155 0 : this->edge_label_names.push_back(name);
156 0 : this->edge_label_types.push_back(type);
157 0 : }
158 :
159 :
160 :
161 :
162 : /// lts_info
163 :
164 6 : lts_info::lts_info(pbes& p, detail::pbes_greybox_interface* pgg, bool reset = false, bool always_split = false):
165 6 : p(p),
166 6 : pgg(pgg),
167 6 : reset_option(reset),
168 6 : always_split_option(always_split),
169 6 : type(0)
170 : {
171 6 : if (!detail::is_ppg(p))
172 : {
173 0 : throw std::runtime_error("PBES is not a PPG! Please rewrite with pbesrewr -pppg.");
174 : }
175 : //std::clog << "info: resetOption = " << (this->resetOption ? "true":"false") << ", reset = " << reset << std::endl;
176 6 : compute_lts_type();
177 6 : compute_transition_groups();
178 6 : compute_dependency_matrix();
179 6 : }
180 :
181 :
182 6 : void lts_info::compute_lts_type()
183 : {
184 : //std::clog << "pbes_type:" << std::endl;
185 6 : mCRL2log(log::verbose) << "Compute LTS type." << std::endl;
186 6 : std::vector<std::string> params;
187 6 : std::map<std::string,std::string> paramtypes;
188 6 : data::representative_generator default_expression_generator(p.data());
189 :
190 20 : for (const auto& eqn : p.equations())
191 : {
192 : //std::clog << core::pp((*eqn).symbol()) << " " << (*eqn).variable().name()
193 : // << std::endl;
194 :
195 14 : propositional_variable var = eqn.variable();
196 48 : for (const variable& varparam: var.parameters())
197 : {
198 34 : std::string signature = get_param_signature(varparam);
199 34 : bool new_param = true;
200 98 : for (auto & param : params) {
201 64 : if (signature == param) new_param = false;
202 : }
203 34 : if (new_param) {
204 14 : params.push_back(signature);
205 14 : paramtypes[signature] = core::pp(varparam.sort());
206 : //std::clog << "paramtypes[" << signature << "] = " << paramtypes[signature] << std::endl;
207 14 : data_expression e(default_expression_generator(varparam.sort()));
208 14 : pbes_expression e1 = pgg->rewrite_and_simplify_expression(e,false);
209 14 : this->param_default_values.push_back(atermpp::down_cast<const data::data_expression>(e1));
210 14 : }
211 34 : }
212 : //params.sort();
213 14 : }
214 6 : this->type = lts_type(1 + params.size());
215 6 : this->type.add_state("var", "string"); // Propositional variable name
216 :
217 6 : int i = 0;
218 20 : for (const std::string& signature: params) {
219 14 : this->type.add_state(signature, paramtypes[signature]);
220 14 : this->param_index[signature] = i;
221 14 : i++;
222 : }
223 :
224 6 : this->type.add_state_label("priority", "int");
225 6 : this->type.add_state_label("type", "int");
226 :
227 : //this->type->add_edge_label("", "");
228 : //std::clog << "-- end of pbes_type." << std::endl;
229 6 : mCRL2log(log::verbose) << "end of compute_lts_type." << std::endl;
230 6 : }
231 :
232 :
233 8 : inline bool lts_info::is_pass_through_state(const propositional_variable_instantiation& propvar)
234 : {
235 8 : std::string varname = std::string(propvar.name());
236 8 : data::variable_list params = this->variable_parameters[varname];
237 8 : const data::data_expression_list& values = propvar.parameters();
238 8 : if (params.size() != values.size())
239 : {
240 0 : return false;
241 : }
242 : else
243 : {
244 8 : data::variable_list::const_iterator param_it = params.begin();
245 32 : for(const auto & value : values)
246 : {
247 24 : if (!data::is_variable(value))
248 : {
249 0 : return false;
250 : }
251 : else
252 : {
253 24 : data::variable param(*param_it);
254 24 : data::variable param_expr(value);
255 24 : if (param != param_expr)
256 : {
257 0 : return false;
258 : }
259 24 : }
260 24 : if (param_it != params.end())
261 : {
262 24 : ++param_it;
263 : }
264 : }
265 : }
266 8 : if(params != values)
267 : {
268 0 : throw mcrl2::runtime_error("is_pass_through_state check failed on " + data::pp(params) + " " + data::pp(values));
269 : }
270 8 : return true;
271 8 : }
272 :
273 :
274 368 : inline int lts_info::count_variables(const pbes_expression& e)
275 : {
276 368 : if (is_propositional_variable_instantiation(e))
277 : {
278 72 : return 1;
279 : }
280 296 : else if (is_and(e) || is_or(e) || is_imp(e))
281 : {
282 156 : return count_variables(pbes_system::accessors::left(e)) + count_variables(pbes_system::accessors::right(e));
283 : }
284 140 : else if (is_forall(e) || is_exists(e))
285 : {
286 36 : if (count_variables(pbes_system::accessors::arg(e)) > 0)
287 : {
288 36 : return INT_MAX;
289 : }
290 : else
291 : {
292 0 : return 0;
293 : }
294 : }
295 104 : else if (is_not(e))
296 : {
297 0 : return count_variables(pbes_system::accessors::arg(e));
298 : }
299 104 : else if (is_data(e))
300 : {
301 104 : return 0;
302 : }
303 : else
304 : {
305 0 : throw(std::runtime_error("Unexpected expression: " + pbes_system::pp(e)));
306 : }
307 : }
308 :
309 28 : std::vector<pbes_expression> lts_info::split_expression_and_substitute_variables(const pbes_expression& e, int current_priority, operation_type current_type, std::set<std::string> vars_stack)
310 : {
311 28 : std::vector<pbes_expression> result;
312 28 : std::vector<pbes_expression> parts;
313 28 : if (is_simple_expression(e))
314 : {
315 0 : result.push_back(e);
316 : }
317 28 : else if (!is_propositional_variable_instantiation(e) && count_variables(e) <= 1 && !always_split_option)
318 : {
319 20 : result.push_back(e);
320 : }
321 8 : else if (is_and(e)) {
322 0 : parts = split_conjuncts(e, true);
323 8 : } else if (is_or(e)) {
324 0 : parts = split_disjuncts(e, true);
325 : } else {
326 8 : parts.push_back(e);
327 : }
328 :
329 28 : bool pass_through = true;
330 :
331 36 : for(std::vector<pbes_expression>::iterator p_it = parts.begin(); pass_through && p_it != parts.end(); ++p_it)
332 : {
333 8 : pbes_expression part = *p_it;
334 8 : if (is_propositional_variable_instantiation(part))
335 : {
336 : // Try to substitute the variable instantiation with the associated expression
337 :
338 8 : propositional_variable_instantiation propvar = (propositional_variable_instantiation)part;
339 8 : if (is_pass_through_state(propvar))
340 : {
341 : // The variable instantiation only copies the current parameters and local data variables,
342 : // so substitution is safe with respect to that.
343 :
344 8 : std::string varname = std::string(propvar.name());
345 8 : int priority = this->variable_priority[varname];
346 8 : operation_type type = this->variable_type[varname];
347 8 : pbes_expression expr = this->variable_expression[varname];
348 :
349 0 : if ((priority == current_priority) &&
350 8 : (current_type == type || is_simple_expression(expr) || count_variables(expr) <= 1) &&
351 8 : vars_stack.find(varname) == vars_stack.end())
352 : {
353 : // The associated equation has the same priority and operation type as the current equation,
354 : // so substitution is safe.
355 :
356 : //std::clog << " Substituting variable instantiation: " << pbes_system::pp(part) << std::endl
357 : // << " with: " << pbes_system::pp(expr) << std::endl;
358 :
359 : // Recursively try to further substitute variables:
360 : // (vars_stack is used to prevent infinite recursion)
361 0 : std::set<std::string> new_vars_stack(vars_stack.begin(), vars_stack.end());
362 0 : new_vars_stack.insert(varname);
363 0 : std::vector<pbes_expression> part_result = split_expression_and_substitute_variables(expr, current_priority, current_type, new_vars_stack);
364 0 : result.insert(result.end(), part_result.begin(), part_result.end());
365 0 : }
366 : else
367 : {
368 8 : result.push_back(part);
369 : }
370 8 : }
371 : else
372 : {
373 0 : pass_through = false;
374 : }
375 8 : }
376 : else
377 : {
378 0 : pass_through = false;
379 : }
380 8 : }
381 28 : if (!pass_through)
382 : {
383 0 : if (always_split_option && !parts.empty())
384 : {
385 : // the old behaviour of the explorer: always split conjunctions and disjunctions
386 : // into subexpressions that form groups
387 0 : result = parts;
388 : }
389 : else
390 : {
391 : // the new behaviour: only split expressions if every part is a pass-through variable instantiation,
392 : // i.e., all values are copied and not changed.
393 0 : result.clear();
394 0 : result.push_back(e);
395 : }
396 : }
397 56 : return result;
398 28 : }
399 :
400 :
401 6 : void lts_info::compute_transition_groups()
402 : {
403 6 : mCRL2log(log::verbose) << "Compute transition groups." << std::endl;
404 :
405 6 : int group = 0;
406 6 : int priority = 0;
407 6 : operation_type type = parity_game_generator::PGAME_AND;
408 6 : fixpoint_symbol symbol = fixpoint_symbol::nu();
409 6 : detail::ppg_visitor checker;
410 :
411 6 : std::string name = "true";
412 12 : propositional_variable t{core::identifier_string(name), data::variable_list()};
413 6 : this->variables[name] = t;
414 6 : this->variable_type[name] = type;
415 6 : this->variable_symbol[name] = symbol;
416 6 : this->variable_priority[name] = priority;
417 6 : this->variable_parameters[name] = t.parameters();
418 6 : this->variable_parameter_signatures[name] = get_param_sequence(t.parameters());
419 6 : this->variable_parameter_indices[name] = this->get_param_indices(t.parameters());
420 6 : this->variable_parameter_index_positions[name] = this->get_param_index_positions(t.parameters());
421 6 : this->transition_expression_plain.push_back(true_());
422 6 : this->transition_expression.push_back(pgg->rewrite_and_simplify_expression(true_()));
423 6 : this->transition_variable_name.push_back(name);
424 6 : this->transition_type.push_back(type);
425 6 : group++;
426 6 : priority++;
427 :
428 6 : name = "false";
429 6 : type = parity_game_generator::PGAME_OR;
430 6 : symbol = fixpoint_symbol::mu();
431 12 : propositional_variable f{core::identifier_string(name), data::variable_list()};
432 6 : this->variables[name] = f;
433 6 : this->variable_type[name] = type;
434 6 : this->variable_symbol[name] = symbol;
435 6 : this->variable_priority[name] = priority;
436 6 : this->variable_parameters[name] = f.parameters();
437 6 : this->variable_parameter_signatures[name] = get_param_sequence(f.parameters());
438 6 : this->variable_parameter_indices[name] = this->get_param_indices(f.parameters());
439 6 : this->variable_parameter_index_positions[name] = this->get_param_index_positions(f.parameters());
440 6 : this->transition_expression_plain.push_back(false_());
441 6 : this->transition_expression.push_back(pgg->rewrite_and_simplify_expression(false_()));
442 6 : this->transition_variable_name.push_back(name);
443 6 : this->transition_type.push_back(type);
444 6 : group++;
445 6 : priority++;
446 :
447 6 : symbol = fixpoint_symbol::nu();
448 :
449 20 : for (auto & eqn : p.equations()) {
450 14 : pbes_expression expr = pgg->get_pbes_equation(eqn.variable().name()).formula();
451 14 : std::string variable_name = eqn.variable().name();
452 14 : this->variables[variable_name] = eqn.variable();
453 14 : type = pgg->get_expression_operation(expr);
454 14 : this->variable_type[variable_name] = type;
455 14 : this->variable_symbol[variable_name] = eqn.symbol();
456 14 : if (eqn.symbol() != symbol) {
457 4 : priority++;
458 4 : symbol = eqn.symbol();
459 : }
460 14 : mCRL2log(log::debug) << "Adding var " << variable_name << ", priority=" << priority << ", symbol=" << symbol << std::endl;
461 14 : this->variable_priority[variable_name] = priority;
462 14 : this->variable_parameters[variable_name] = eqn.variable().parameters();
463 14 : this->variable_parameter_signatures[variable_name] = get_param_sequence(eqn.variable().parameters());
464 14 : this->variable_parameter_indices[variable_name] = this->get_param_indices(eqn.variable().parameters());
465 14 : this->variable_parameter_index_positions[variable_name] = this->get_param_index_positions(eqn.variable().parameters());
466 14 : this->variable_expression[variable_name] = expr;
467 14 : }
468 :
469 : // Skip 'unused' equations....
470 6 : std::set<std::string> variable_set;
471 : {
472 6 : propositional_variable_instantiation init = p.initial_state();
473 6 : std::queue<std::string> variable_queue;
474 6 : variable_queue.push(init.name());
475 6 : variable_set.insert(init.name());
476 20 : while (!variable_queue.empty())
477 : {
478 14 : std::string var = variable_queue.front();
479 14 : variable_queue.pop();
480 14 : type = this->variable_type[var];
481 14 : priority = this->variable_priority[var];
482 14 : pbes_expression expr = this->variable_expression[var];
483 14 : std::set<std::string> vars_stack;
484 14 : std::vector<pbes_expression> expression_parts = split_expression_and_substitute_variables(expr, priority, type, vars_stack);
485 14 : for (std::vector<pbes_expression>::const_iterator e =
486 28 : expression_parts.begin(); e != expression_parts.end(); ++e) {
487 14 : std::set<std::string> occ_vars = lts_info::occ(*e);
488 40 : for (const auto & var_str : variable_set)
489 : {
490 26 : occ_vars.erase(var_str);
491 : }
492 22 : for(const auto & occ_var : occ_vars)
493 : {
494 8 : variable_queue.push(occ_var);
495 : }
496 14 : variable_set.insert(occ_vars.begin(), occ_vars.end());
497 14 : }
498 14 : }
499 6 : mCRL2log(log::debug) << "Set of 'used' variables: " << std::endl;
500 20 : for (const auto & var_str : variable_set)
501 : {
502 14 : mCRL2log(log::debug) << " " << var_str << std::endl;
503 : }
504 6 : mCRL2log(log::debug) << std::endl;
505 6 : }
506 :
507 20 : for (auto & eqn : p.equations()) {
508 14 : std::string variable_name = eqn.variable().name();
509 14 : if (variable_set.find(variable_name) != variable_set.end())
510 : {
511 14 : type = this->variable_type[variable_name];
512 14 : priority = this->variable_priority[variable_name];
513 14 : pbes_expression expr = this->variable_expression[variable_name];
514 14 : std::set<std::string> vars_stack;
515 14 : mCRL2log(log::debug) << std::endl << "Generating groups for equation " << variable_name << std::endl;
516 14 : std::vector<pbes_expression> expression_parts = split_expression_and_substitute_variables(expr, priority, type, vars_stack);
517 14 : for (std::vector<pbes_expression>::const_iterator e =
518 28 : expression_parts.begin(); e != expression_parts.end(); ++e) {
519 14 : this->transition_expression_plain.push_back(*e);
520 14 : this->transition_expression.push_back(pgg->rewrite_and_simplify_expression(*e));
521 14 : this->transition_variable_name.push_back(variable_name);
522 14 : this->transition_type.push_back(type);
523 28 : mCRL2log(log::debug) << "Add transition group " << group << ": "
524 14 : << (type==parity_game_generator::PGAME_AND ? "AND" : "OR") << " " << variable_name << " "
525 14 : << pbes_system::pp(*e) << std::endl;
526 14 : group++;
527 : }
528 14 : }
529 14 : }
530 6 : number_of_groups = group;
531 : //std::clog << "Added " << group << " transition groups." << std::endl;
532 6 : mCRL2log(log::debug) << "end of compute_transition_groups." << std::endl;
533 6 : }
534 :
535 :
536 6 : void lts_info::compute_dependency_matrix()
537 : {
538 6 : mCRL2log(log::verbose) << "Compute dependency matrix." << std::endl;
539 32 : for(int group=0; group < number_of_groups; group++)
540 : {
541 26 : std::vector<bool> dep_row;
542 26 : std::vector<bool> read_row;
543 26 : std::vector<bool> write_row;
544 26 : bool r = is_read_dependent_propvar(group);
545 26 : bool w = is_write_dependent_propvar(group);
546 26 : bool d = r || w;
547 26 : dep_row.push_back(d);
548 26 : read_row.push_back(r);
549 26 : write_row.push_back(w);
550 92 : for (int part = 1; part < type.get_state_length(); part++)
551 : {
552 66 : r = is_read_dependent_parameter(group, part);
553 66 : w = is_write_dependent_parameter(group, part);
554 66 : d = r || w;
555 66 : dep_row.push_back(d);
556 66 : read_row.push_back(r);
557 66 : write_row.push_back(w);
558 : }
559 26 : matrix[group] = dep_row;
560 26 : read_matrix[group] = read_row;
561 26 : write_matrix[group] = write_row;
562 26 : }
563 6 : mCRL2log(log::verbose) << "end of compute_dependency_matrix." << std::endl;
564 6 : }
565 :
566 :
567 3366 : bool lts_info::get_reset_option() const
568 : {
569 3366 : return reset_option;
570 : }
571 :
572 :
573 6 : int lts_info::get_number_of_groups() const
574 : {
575 6 : return number_of_groups;
576 : }
577 :
578 :
579 866 : const std::vector<pbes_expression>& lts_info::get_transition_expressions() const
580 : {
581 866 : return transition_expression;
582 : }
583 :
584 :
585 5168 : const std::vector<std::string>& lts_info::get_transition_variable_names() const
586 : {
587 5168 : return transition_variable_name;
588 : }
589 :
590 :
591 0 : const std::vector<lts_info::operation_type>& lts_info::get_transition_types() const
592 : {
593 0 : return transition_type;
594 : }
595 :
596 :
597 0 : const std::map<std::string, propositional_variable>& lts_info::get_variables() const
598 : {
599 0 : return variables;
600 : }
601 :
602 :
603 1732 : const std::map<std::string, lts_info::operation_type>& lts_info::get_variable_types() const
604 : {
605 1732 : return variable_type;
606 : }
607 :
608 0 : const std::map<std::string, fixpoint_symbol>& lts_info::get_variable_symbols() const
609 : {
610 0 : return variable_symbol;
611 : }
612 :
613 :
614 0 : const std::map<std::string, int>& lts_info::get_variable_priorities() const
615 : {
616 0 : return variable_priority;
617 : }
618 :
619 :
620 0 : const std::map<std::string, data::variable_list>& lts_info::get_variable_parameters() const
621 : {
622 0 : return variable_parameters;
623 : }
624 :
625 :
626 3366 : const std::map<std::string, std::vector<std::string> >& lts_info::get_variable_parameter_signatures() const
627 : {
628 3366 : return variable_parameter_signatures;
629 : }
630 :
631 :
632 5098 : const std::map<std::string, std::vector<int> >& lts_info::get_variable_parameter_indices() const
633 : {
634 5098 : return variable_parameter_indices;
635 : }
636 :
637 :
638 9168 : const std::map<std::string, std::map<int,int> >& lts_info::get_variable_parameter_index_positions() const
639 : {
640 9168 : return variable_parameter_index_positions;
641 : }
642 :
643 :
644 41352 : const lts_type& lts_info::get_lts_type() const
645 : {
646 41352 : return type;
647 : }
648 :
649 :
650 6 : const std::map<int,std::vector<bool> >& lts_info::get_dependency_matrix() const
651 : {
652 6 : return matrix;
653 : }
654 :
655 :
656 6 : const std::map<int,std::vector<bool> >& lts_info::get_read_matrix() const
657 : {
658 6 : return read_matrix;
659 : }
660 :
661 :
662 6 : const std::map<int,std::vector<bool> >& lts_info::get_write_matrix() const
663 : {
664 6 : return write_matrix;
665 : }
666 :
667 :
668 68 : int lts_info::get_index(const std::string& signature)
669 : {
670 68 : return param_index[signature];
671 : }
672 :
673 :
674 14 : const data_expression& lts_info::get_default_value(int index)
675 : {
676 14 : return param_default_values.at(index);
677 : }
678 :
679 :
680 26 : bool lts_info::is_read_dependent_propvar(int /* group */)
681 : {
682 26 : return true;
683 : }
684 :
685 :
686 66 : bool lts_info::is_read_dependent_parameter(int group, int part)
687 : {
688 66 : if (group==0 || group==1) return false;
689 38 : std::string p = type.get_state_names()[part];
690 38 : mCRL2log(log::debug) << "is_read_dependent_parameter (group=" << group << ", part=" << part << " [" << p << "]" << std::endl;
691 38 : pbes_expression phi = transition_expression_plain[group];
692 38 : std::string X = transition_variable_name[group];
693 38 : std::set<std::string> params = lts_info::get_param_set(variable_parameters[X]);
694 38 : if (params.find(p) == params.end())
695 : {
696 4 : return false; // Parameter is not in params(X).
697 : }
698 : else
699 : {
700 34 : std::set<std::string> usedSet = used(phi);
701 34 : std::set<std::string> changedSet = changed(phi);
702 34 : std::set<std::string> copySet = copied(phi);
703 34 : std::set<std::string> changedAndCopied;
704 34 : std::set_intersection(changedSet.begin(), changedSet.end(), copySet.begin(), copySet.end(),
705 : std::inserter(changedAndCopied, changedAndCopied.end()));
706 :
707 34 : if (usedSet.find(p) == usedSet.end() && changedAndCopied.find(p) == changedAndCopied.end())
708 : {
709 : // Parameter is not in used(phi) and not in (changed(phi) /\ copied(phi)).
710 12 : return false; // Parameter is not in used(phi).
711 : }
712 : else
713 : {
714 22 : return true; // Parameter is both in used(phi) and in params(X).
715 : }
716 34 : }
717 :
718 38 : }
719 :
720 :
721 26 : bool lts_info::is_write_dependent_propvar(int group)
722 : {
723 26 : if (group==0 || group==1) return false;
724 14 : pbes_expression phi = transition_expression_plain[group];
725 14 : std::string X = transition_variable_name[group];
726 14 : if (lts_info::tf(phi))
727 : {
728 10 : return true;
729 : }
730 4 : std::set<std::string> occ = lts_info::occ(phi);
731 4 : if (occ.empty())
732 : {
733 0 : return false; // Not dependent if occ(phi) == {}.
734 : }
735 4 : else if (occ.size() == 1)
736 : {
737 4 : bool containsX = occ.find(X) != occ.end();
738 4 : return !containsX; // Not dependent if occ(phi) == {X}.
739 : }
740 : else
741 : {
742 0 : return true; // Dependent, because occ(phi) contains multiple elements.
743 : }
744 14 : }
745 :
746 :
747 66 : bool lts_info::is_write_dependent_parameter(int group , int part)
748 : {
749 66 : if (group==0 || group==1) return false;
750 38 : std::string p = type.get_state_names().at(part);
751 38 : pbes_expression phi = transition_expression_plain[group];
752 38 : std::string X = transition_variable_name[group];
753 38 : if (this->reset_option) {
754 0 : if (lts_info::tf(phi))
755 : {
756 : // phi may have boolean result (not only propositional variable instantiations)
757 0 : return true;
758 : }
759 0 : std::set<std::string> params = lts_info::get_param_set(variable_parameters[X]);
760 0 : std::set<std::string> resetSet = reset(phi, params);
761 0 : if (resetSet.find(p) != resetSet.end())
762 : {
763 0 : return true; // Dependent, because p in reset(phi, params(X)).
764 : }
765 0 : }
766 38 : std::set<std::string> changedSet = changed(phi);
767 38 : bool changedSetContainsP = (changedSet.find(p) != changedSet.end());
768 38 : return changedSetContainsP; // Dependent, because p in changed(phi, {}).
769 38 : }
770 :
771 :
772 72 : std::set<std::string> lts_info::changed(const pbes_expression& phi)
773 : {
774 72 : std::set<std::string> empty;
775 144 : return changed(phi, empty);
776 72 : }
777 :
778 :
779 952 : std::set<std::string> lts_info::changed(const pbes_expression& phi, const std::set<std::string>& L)
780 : {
781 952 : std::set<std::string> result;
782 952 : if (is_not(phi))
783 : {
784 0 : result = changed(pbes_system::accessors::arg(phi), L);
785 : }
786 952 : else if (is_and(phi) || is_or(phi) || is_imp(phi))
787 : {
788 396 : std::set<std::string> l = changed(pbes_system::accessors::left(phi), L);
789 396 : result.insert(l.begin(), l.end());
790 396 : std::set<std::string> r = changed(pbes_system::accessors::right(phi), L);
791 396 : result.insert(r.begin(), r.end());
792 396 : }
793 556 : else if (is_forall(phi) || is_exists(phi))
794 : {
795 88 : std::set<std::string> LL;
796 88 : LL.insert(L.begin(), L.end());
797 88 : data::variable_list vars = quantifier_variables(phi);
798 176 : for (auto variable : vars)
799 : {
800 88 : LL.insert(get_param_signature(variable));
801 88 : }
802 88 : result = changed(pbes_system::accessors::arg(phi), LL);
803 88 : }
804 468 : else if (is_propositional_variable_instantiation(phi))
805 : {
806 : std::vector<std::string> var_param_signatures =
807 208 : variable_parameter_signatures[atermpp::down_cast<propositional_variable_instantiation>(phi).name()];
808 208 : data::data_expression_list values = atermpp::down_cast<propositional_variable_instantiation>(phi).parameters();
809 208 : assert(var_param_signatures.size() == values.size());
810 208 : data::data_expression_list::const_iterator val = values.begin();
811 208 : for (std::vector<std::string>::const_iterator param =
812 756 : var_param_signatures.begin(); param != var_param_signatures.end(); ++param) {
813 548 : std::string param_signature = *param;
814 548 : if (data::is_variable(*val))
815 : {
816 320 : const variable& value = atermpp::down_cast<variable>(*val);
817 320 : std::string value_signature = get_param_signature(value);
818 320 : if (param_signature != value_signature || L.find(value_signature) != L.end())
819 : {
820 20 : result.insert(param_signature);
821 : }
822 320 : }
823 : else
824 : {
825 228 : result.insert(param_signature);
826 : }
827 548 : if (val != values.end()) {
828 548 : ++val;
829 : }
830 548 : }
831 208 : }
832 952 : return result;
833 0 : }
834 :
835 :
836 0 : std::set<std::string> lts_info::reset(const pbes_expression& phi, const std::set<std::string>& d)
837 : {
838 0 : std::set<std::string> result;
839 0 : if (is_not(phi))
840 : {
841 0 : result = reset(pbes_system::accessors::arg(phi), d);
842 : }
843 0 : else if (is_and(phi) || is_or(phi) || is_imp(phi))
844 : {
845 0 : std::set<std::string> l = reset(pbes_system::accessors::left(phi), d);
846 0 : result.insert(l.begin(), l.end());
847 0 : std::set<std::string> r = reset(pbes_system::accessors::right(phi), d);
848 0 : result.insert(r.begin(), r.end());
849 0 : }
850 0 : else if (is_forall(phi) || is_exists(phi))
851 : {
852 0 : result = reset(pbes_system::accessors::arg(phi), d);
853 : }
854 0 : else if (is_propositional_variable_instantiation(phi))
855 : {
856 0 : std::set<std::string> params;
857 : std::vector<std::string> var_params =
858 0 : variable_parameter_signatures[atermpp::down_cast<propositional_variable_instantiation>(phi).name()];
859 0 : for (std::vector<std::string>::const_iterator param =
860 0 : var_params.begin(); param != var_params.end(); ++param) {
861 0 : std::string signature = *param;
862 0 : params.insert(signature);
863 0 : }
864 0 : for (auto signature : d) {
865 0 : if (params.find(signature) == params.end())
866 : {
867 0 : result.insert(signature);
868 : }
869 0 : }
870 0 : }
871 0 : return result;
872 0 : }
873 :
874 :
875 42 : bool lts_info::tf(const pbes_expression& phi)
876 : {
877 42 : if (is_not(phi))
878 : {
879 0 : return tf(pbes_system::accessors::arg(phi));
880 : }
881 42 : else if (is_and(phi) || is_or(phi) || is_imp(phi))
882 : {
883 20 : return tf(pbes_system::accessors::left(phi)) || tf(pbes_system::accessors::right(phi));
884 : }
885 22 : else if (is_forall(phi) || is_exists(phi))
886 : {
887 8 : return tf(pbes_system::accessors::arg(phi));
888 : }
889 14 : else if (is_propositional_variable_instantiation(phi))
890 : {
891 4 : return false;
892 : }
893 10 : return true;
894 : }
895 :
896 :
897 192 : std::set<std::string> lts_info::occ(const pbes_expression& expr)
898 : {
899 192 : std::set<std::string> result;
900 192 : if (is_propositional_variable_instantiation(expr))
901 : {
902 44 : result.insert(atermpp::down_cast<propositional_variable_instantiation>(expr).name());
903 : }
904 148 : else if (is_and(expr) || is_or(expr) ||is_imp(expr))
905 : {
906 78 : std::set<std::string> l = occ(pbes_system::accessors::left(expr));
907 78 : result.insert(l.begin(), l.end());
908 78 : std::set<std::string> r = occ(pbes_system::accessors::right(expr));
909 78 : result.insert(r.begin(), r.end());
910 78 : }
911 70 : else if (is_forall(expr) || is_exists(expr) || is_not(expr))
912 : {
913 18 : result = occ(pbes_system::accessors::arg(expr));
914 : }
915 192 : return result;
916 0 : }
917 :
918 :
919 224 : std::set<std::string> lts_info::free(const pbes_expression& expr)
920 : {
921 224 : std::set<std::string> result;
922 550 : for (const data::variable& var: pbes_system::find_free_variables(expr))
923 : {
924 326 : result.insert(get_param_signature(var));
925 224 : }
926 224 : return result;
927 0 : }
928 :
929 :
930 34 : std::set<std::string> lts_info::used(const pbes_expression& expr)
931 : {
932 34 : std::set<std::string> emptySet;
933 68 : return used(expr, emptySet);
934 34 : }
935 :
936 :
937 540 : std::set<std::string> lts_info::used(const pbes_expression& expr, const std::set<std::string>& L)
938 : {
939 : //std::clog << "lts_info::used(" << bqnf_visitor<equation_type, term_type>::print_brief(expr) << ", L)" << std::endl;
940 540 : std::set<std::string> result;
941 540 : if (is_data(expr))
942 : {
943 224 : std::set<std::string> fv = free(expr);
944 224 : result.insert(fv.begin(), fv.end());
945 224 : }
946 540 : if (is_propositional_variable_instantiation(expr))
947 : {
948 : data::variable_list var_params =
949 96 : variable_parameters[atermpp::down_cast<propositional_variable_instantiation>(expr).name()];
950 96 : data::data_expression_list values = atermpp::down_cast<propositional_variable_instantiation>(expr).parameters();
951 96 : assert(var_params.size() == values.size());
952 96 : data::data_expression_list::const_iterator val = values.begin();
953 352 : for (auto parameter : var_params) {
954 256 : std::string param_signature = get_param_signature(parameter);
955 256 : if (data::is_variable(*val))
956 : {
957 152 : const variable& value = atermpp::down_cast<variable>(*val);
958 152 : std::string value_signature = get_param_signature(value);
959 152 : if (param_signature != value_signature || L.find(value_signature) != L.end())
960 : {
961 8 : result.insert(value_signature);
962 : }
963 152 : }
964 : else
965 : {
966 : // add free variables in data expression
967 104 : std::set<std::string> l = used(*val, L);
968 104 : result.insert(l.begin(), l.end());
969 104 : }
970 256 : if (val != values.end()) {
971 256 : ++val;
972 : }
973 256 : }
974 96 : }
975 444 : else if (is_and(expr) || is_or(expr) || is_imp(expr))
976 : {
977 182 : std::set<std::string> l = used(pbes_system::accessors::left(expr), L);
978 182 : result.insert(l.begin(), l.end());
979 182 : std::set<std::string> r = used(pbes_system::accessors::right(expr), L);
980 182 : result.insert(r.begin(), r.end());
981 182 : }
982 262 : else if (is_not(expr))
983 : {
984 0 : result = used(pbes_system::accessors::arg(expr), L);
985 : }
986 262 : else if (is_forall(expr) || is_exists(expr))
987 : {
988 38 : std::set<std::string> LL;
989 38 : LL.insert(L.begin(), L.end());
990 38 : data::variable_list vars = quantifier_variables(expr);
991 76 : for (auto variable : vars)
992 : {
993 38 : LL.insert(get_param_signature(variable));
994 38 : }
995 38 : result = used(pbes_system::accessors::arg(expr), LL);
996 38 : }
997 540 : return result;
998 0 : }
999 :
1000 :
1001 34 : std::set<std::string> lts_info::copied(const pbes_expression& expr)
1002 : {
1003 34 : std::set<std::string> emptySet;
1004 68 : return copied(expr, emptySet);
1005 34 : }
1006 :
1007 :
1008 436 : std::set<std::string> lts_info::copied(const pbes_expression& expr, const std::set<std::string>& L)
1009 : {
1010 : //std::clog << "lts_info::copied(" << bqnf_visitor<equation_type, term_type>::print_brief(expr) << ", L)" << std::endl;
1011 436 : std::set<std::string> result;
1012 436 : if (is_data(expr))
1013 : {
1014 : // skip
1015 : }
1016 436 : if (is_propositional_variable_instantiation(expr))
1017 : {
1018 : data::variable_list var_params =
1019 96 : variable_parameters[atermpp::down_cast<propositional_variable_instantiation>(expr).name()];
1020 96 : data::data_expression_list values = atermpp::down_cast<propositional_variable_instantiation>(expr).parameters();
1021 96 : assert(var_params.size() == values.size());
1022 96 : data::data_expression_list::const_iterator val = values.begin();
1023 352 : for (auto parameter : var_params) {
1024 256 : std::string param_signature = get_param_signature(parameter);
1025 256 : if (data::is_variable(*val))
1026 : {
1027 152 : const variable& value = atermpp::down_cast<variable>(*val);
1028 152 : std::string value_signature = get_param_signature(value);
1029 152 : if (param_signature == value_signature && L.find(value_signature) == L.end())
1030 : {
1031 144 : result.insert(value_signature);
1032 : }
1033 152 : }
1034 256 : if (val != values.end()) {
1035 256 : ++val;
1036 : }
1037 256 : }
1038 96 : }
1039 340 : else if (is_and(expr) || is_or(expr) || is_imp(expr))
1040 : {
1041 182 : std::set<std::string> l = copied(pbes_system::accessors::left(expr), L);
1042 182 : result.insert(l.begin(), l.end());
1043 182 : std::set<std::string> r = copied(pbes_system::accessors::right(expr), L);
1044 182 : result.insert(r.begin(), r.end());
1045 182 : }
1046 158 : else if (is_not(expr))
1047 : {
1048 0 : result = copied(pbes_system::accessors::arg(expr), L);
1049 : }
1050 158 : else if (is_forall(expr) || is_exists(expr))
1051 : {
1052 38 : std::set<std::string> LL;
1053 38 : LL.insert(L.begin(), L.end());
1054 38 : data::variable_list vars = quantifier_variables(expr);
1055 76 : for (auto variable : vars)
1056 : {
1057 38 : LL.insert(get_param_signature(variable));
1058 38 : }
1059 38 : result = copied(pbes_system::accessors::arg(expr), LL);
1060 38 : }
1061 436 : return result;
1062 0 : }
1063 :
1064 :
1065 0 : std::string lts_info::state_to_string(const ltsmin_state& state)
1066 : {
1067 : //std::clog << "info::to_string" << std::endl;
1068 0 : std::string result;
1069 0 : std::stringstream ss;
1070 0 : operation_type type = detail::map_at(get_variable_types(), state.get_variable());
1071 0 : ss << (type==parity_game_generator::PGAME_AND ? "AND" : "OR");
1072 0 : ss << ":" << state.get_variable();
1073 0 : ss << "(";
1074 0 : const std::vector<data_expression>& param_values = state.get_parameter_values();
1075 : std::vector<std::string> param_signatures =
1076 0 : this->variable_parameter_signatures[state.get_variable()];
1077 : std::vector<std::string>::const_iterator param_signature =
1078 0 : param_signatures.begin();
1079 0 : for (std::vector<data_expression>::const_iterator param_value =
1080 0 : param_values.begin(); param_value != param_values.end(); ++param_value) {
1081 0 : if (param_value != param_values.begin())
1082 0 : ss << ", ";
1083 0 : ss << *param_signature << " = ";
1084 0 : ss << *param_value;
1085 0 : if (param_signature != param_signatures.end())
1086 : {
1087 0 : ++param_signature;
1088 : }
1089 : }
1090 0 : ss << ")";
1091 0 : result = ss.str();
1092 0 : return result;
1093 0 : }
1094 :
1095 :
1096 38 : std::set<std::string> lts_info::get_param_set(const data::variable_list& params)
1097 : {
1098 38 : std::set<std::string> result;
1099 136 : for (auto parameter : params) {
1100 98 : result.insert(get_param_signature(parameter));
1101 98 : }
1102 38 : return result;
1103 0 : }
1104 :
1105 :
1106 26 : std::vector<std::string> lts_info::get_param_sequence(const data::variable_list& params)
1107 : {
1108 26 : std::vector<std::string> result;
1109 60 : for (auto parameter : params) {
1110 34 : result.push_back(get_param_signature(parameter));
1111 34 : }
1112 26 : return result;
1113 0 : }
1114 :
1115 :
1116 26 : std::vector<int> lts_info::get_param_indices(const data::variable_list& params)
1117 : {
1118 26 : std::vector<int> result;
1119 60 : for (auto parameter : params) {
1120 34 : int index = this->get_index(get_param_signature(parameter));
1121 34 : result.push_back(index);
1122 34 : }
1123 26 : return result;
1124 0 : }
1125 :
1126 :
1127 26 : std::map<int,int> lts_info::get_param_index_positions(const data::variable_list& params)
1128 : {
1129 26 : std::map<int,int> result;
1130 26 : int i = 0;
1131 60 : for (auto parameter : params) {
1132 34 : int index = this->get_index(get_param_signature(parameter));
1133 34 : result.insert(std::make_pair(index,i));
1134 34 : i++;
1135 34 : }
1136 52 : return result;
1137 0 : }
1138 :
1139 :
1140 : std::map<variable,std::string> lts_info::variable_signatures;
1141 :
1142 :
1143 1860 : std::string lts_info::get_param_signature(const variable& param)
1144 : {
1145 1860 : std::map<variable,std::string>::const_iterator i = variable_signatures.find(param);
1146 1860 : if (i == variable_signatures.end())
1147 : {
1148 7 : std::string paramname = param.name();
1149 7 : std::string paramtype = core::pp(param.sort());
1150 7 : std::string signature = get_param_signature(paramname, paramtype);
1151 7 : variable_signatures[param] = signature;
1152 7 : return signature;
1153 7 : }
1154 1853 : return i->second;
1155 : }
1156 :
1157 :
1158 7 : std::string lts_info::get_param_signature(const std::string& paramname,
1159 : const std::string& paramtype)
1160 : {
1161 14 : return paramname + ":" + paramtype;
1162 : }
1163 :
1164 :
1165 :
1166 :
1167 : // ltsmin_state
1168 :
1169 6 : ltsmin_state::ltsmin_state(const std::string& varname)
1170 : {
1171 6 : this->var = varname;
1172 6 : }
1173 :
1174 :
1175 5098 : ltsmin_state::ltsmin_state(const std::string& varname,
1176 5098 : const pbes_expression& e)
1177 : {
1178 5098 : data_expression novalue;
1179 : //std::clog << "ltsmin_state v = " << pp(v) << std::endl;
1180 5098 : this->var = varname;
1181 5098 : if (is_propositional_variable_instantiation(e)) {
1182 5098 : assert(std::string(atermpp::down_cast<propositional_variable_instantiation>(e).name()) == varname);
1183 : //std::clog << "ltsmin_state: var = " << atermpp::down_cast<propositional_variable_instantiation>(e).name() << std::endl;
1184 5098 : const data::data_expression_list& values = atermpp::down_cast<propositional_variable_instantiation>(e).parameters();
1185 19024 : for (const auto & value : values)
1186 : {
1187 13926 : if (value == novalue)
1188 : {
1189 0 : throw(std::runtime_error("Error in ltsmin_state: state expression contains NoValue: "
1190 0 : + pp(e)));
1191 : }
1192 13926 : this->add_parameter_value(value);
1193 : //std::clog << "ltsmin_state: " << *val << std::endl;
1194 : }
1195 : //std::clog << std::endl;
1196 : } else {
1197 0 : throw(std::runtime_error("Not a valid state expression! " + pp(e)));
1198 : }
1199 5098 : }
1200 :
1201 0 : bool ltsmin_state::operator<( const ltsmin_state& other ) const
1202 : {
1203 0 : if (this->var < other.var) return true;
1204 0 : else if (this->var == other.var)
1205 : {
1206 0 : if (param_values.size() < other.param_values.size()) return true;
1207 0 : else if (param_values.size() == other.param_values.size())
1208 : {
1209 0 : if (param_values < other.param_values) return true;
1210 : }
1211 : }
1212 0 : return false;
1213 : }
1214 :
1215 :
1216 0 : bool ltsmin_state::operator==( const ltsmin_state& other ) const
1217 : {
1218 0 : return this->var==other.var
1219 0 : && param_values.size()==other.param_values.size()
1220 0 : && param_values == other.param_values;
1221 : }
1222 :
1223 :
1224 20224 : std::string ltsmin_state::get_variable() const
1225 : {
1226 20224 : return var;
1227 : }
1228 :
1229 :
1230 12198 : const std::vector<data_expression>& ltsmin_state::get_parameter_values() const
1231 : {
1232 12198 : return param_values;
1233 : }
1234 :
1235 :
1236 13926 : void ltsmin_state::add_parameter_value(const data_expression& value)
1237 : {
1238 13926 : param_values.push_back(value);
1239 13926 : }
1240 :
1241 :
1242 1732 : pbes_expression ltsmin_state::to_pbes_expression() const
1243 : {
1244 1732 : data::data_expression_vector parameter_values;
1245 6480 : for (const auto & param_value : param_values) {
1246 4748 : parameter_values.push_back(param_value);
1247 : }
1248 1732 : data::data_expression_list parameter_values_list(parameter_values.begin(), parameter_values.end());
1249 : // Create propositional variable instantiation.
1250 : propositional_variable_instantiation expr =
1251 1732 : propositional_variable_instantiation(core::identifier_string(var), parameter_values_list);
1252 3464 : return workaround::return_std_move(expr);
1253 1732 : }
1254 :
1255 :
1256 0 : std::string ltsmin_state::state_to_string() const
1257 : {
1258 0 : std::string result;
1259 0 : std::stringstream ss;
1260 0 : ss << (type==parity_game_generator::PGAME_AND ? "AND" : "OR");
1261 0 : ss << ":" << var;
1262 0 : ss << "[" << std::endl;
1263 0 : for (std::vector<data_expression>::const_iterator entry =
1264 0 : param_values.begin(); entry != param_values.end(); ++entry) {
1265 0 : if (entry != param_values.begin())
1266 0 : ss << std::endl << " value = ";
1267 0 : ss << *entry;
1268 : }
1269 0 : ss << "]";
1270 0 : result = ss.str();
1271 0 : return result;
1272 0 : }
1273 :
1274 :
1275 :
1276 :
1277 : /// explorer
1278 :
1279 2 : explorer::explorer(const std::string& filename, const std::string& rewrite_strategy = "jittyc", bool reset_flag = false, bool always_split_flag = false)
1280 : {
1281 2 : load_pbes(p, filename);
1282 8 : for (auto & eqn : p.equations()) {
1283 6 : std::string variable_name = eqn.variable().name();
1284 : //std::clog << "varname = " << variable_name << std::endl;
1285 6 : }
1286 2 : pbes_system::algorithms::normalize(p);
1287 2 : if (!detail::is_ppg(p))
1288 : {
1289 0 : mCRL2log(log::info) << "Rewriting to PPG..." << std::endl;
1290 0 : p = detail::to_ppg(p);
1291 0 : mCRL2log(log::info) << "Rewriting done." << std::endl;
1292 : }
1293 2 : this->pgg = new detail::pbes_greybox_interface(p, true, true, data::parse_rewrite_strategy(rewrite_strategy));
1294 2 : this->info = new lts_info(p, pgg, reset_flag, always_split_flag);
1295 : //std::clog << "explorer" << std::endl;
1296 6 : for (std::size_t i = 0; i < info->get_lts_type().get_number_of_state_types(); ++i) {
1297 4 : std::map<data_expression,int> data2int_map;
1298 4 : this->localmaps_data2int.push_back(data2int_map);
1299 4 : std::vector<data_expression> int2data_map;
1300 4 : this->localmaps_int2data.push_back(int2data_map);
1301 4 : }
1302 : //std::clog << "-- end of explorer." << std::endl;
1303 2 : }
1304 :
1305 :
1306 4 : explorer::explorer(const pbes& p_, const std::string& rewrite_strategy = "jittyc", bool reset_flag = false, bool always_split_flag = false)
1307 : {
1308 4 : p = p_;
1309 4 : this->pgg = new detail::pbes_greybox_interface(p, true, true, data::parse_rewrite_strategy(rewrite_strategy));
1310 4 : this->info = new lts_info(p, pgg, reset_flag, always_split_flag);
1311 : //std::clog << "explorer" << std::endl;
1312 12 : for (std::size_t i = 0; i < info->get_lts_type().get_number_of_state_types(); i++) {
1313 8 : std::map<data_expression,int> data2int_map;
1314 8 : this->localmaps_data2int.push_back(data2int_map);
1315 8 : std::vector<data_expression> int2data_map;
1316 8 : this->localmaps_int2data.push_back(int2data_map);
1317 8 : }
1318 : //std::clog << "-- end of explorer." << std::endl;
1319 4 : }
1320 :
1321 :
1322 6 : explorer::~explorer()
1323 : {
1324 6 : delete info;
1325 6 : delete pgg;
1326 6 : }
1327 :
1328 :
1329 16742 : lts_info* explorer::get_info() const
1330 : {
1331 16742 : return info;
1332 : }
1333 :
1334 :
1335 6 : ltsmin_state explorer::get_initial_state() const
1336 : {
1337 6 : propositional_variable_instantiation initial_state = pgg->get_initial_state();
1338 12 : return this->get_state(initial_state);
1339 6 : }
1340 :
1341 :
1342 6 : void explorer::initial_state(int* state)
1343 : {
1344 6 : ltsmin_state initial_state = this->get_initial_state();
1345 12 : ltsmin_state dummy("dummy");
1346 6 : this->to_state_vector(initial_state, state, dummy, nullptr);
1347 6 : }
1348 :
1349 :
1350 5098 : ltsmin_state explorer::get_state(const propositional_variable_instantiation& expr) const
1351 : {
1352 : //std::clog << "-- get_state --" << std::endl;
1353 : //std::clog << " expr = " << expr << std::endl;
1354 5098 : propositional_variable_instantiation novalue;
1355 5098 : assert(is_propositional_variable_instantiation(expr) && expr != novalue);
1356 5098 : std::string varname = expr.name();
1357 : //std::clog << " varname = " << varname << std::endl;
1358 5098 : ltsmin_state s(varname, expr);
1359 10196 : return s;
1360 5098 : }
1361 :
1362 :
1363 0 : ltsmin_state explorer::true_state()
1364 : {
1365 0 : return ltsmin_state("true");
1366 : }
1367 :
1368 :
1369 0 : ltsmin_state explorer::false_state()
1370 : {
1371 0 : return ltsmin_state("false");
1372 : }
1373 :
1374 :
1375 9998 : data::data_expression explorer::string_to_data(const std::string& s)
1376 : {
1377 9998 : atermpp::aterm t = atermpp::read_term_from_string(s);
1378 19996 : return atermpp::down_cast<data::data_expression>(data::detail::add_index(static_cast<const atermpp::aterm_appl&>(t)));
1379 9998 : }
1380 :
1381 :
1382 13364 : int explorer::get_index(int type_no, const std::string& s)
1383 : {
1384 13364 : if (type_no==0)
1385 : {
1386 3366 : return get_string_index(s);
1387 : }
1388 : else
1389 : {
1390 9998 : data_expression value = this->string_to_data(s);
1391 9998 : return get_value_index(type_no, value);
1392 9998 : }
1393 : }
1394 :
1395 :
1396 4572 : int explorer::get_string_index(const std::string& s)
1397 : {
1398 4572 : std::map<std::string,int>::iterator it = this->localmap_string2int.find(s);
1399 : std::size_t index;
1400 4572 : if (it != this->localmap_string2int.end()) {
1401 4558 : index = it->second;
1402 : } else {
1403 14 : this->localmap_int2string.push_back(s);
1404 14 : index = this->localmap_int2string.size() - 1;
1405 : //std::clog << "[" << getpid() << "] get_string_index DEBUG push_back " << index << ": " << s << std::endl;
1406 14 : this->localmap_string2int.insert(std::make_pair(s,index));
1407 : }
1408 : //std::clog << "get_string_index result =" << index << " (" << this->localmap_int2string->size() << ")" << std::endl;
1409 4572 : return index;
1410 : }
1411 :
1412 :
1413 13622 : int explorer::get_value_index(int type_no, const data_expression& value)
1414 : {
1415 : //std::clog << " get_value_index type_no=" << type_no << " (" << info->get_lts_type().get_number_of_state_types() << ")" << std::endl;
1416 : //std::clog << " type=" << info->get_lts_type().get_state_type_name(type_no) << std::endl;
1417 : //std::clog << " value=" << value << std::endl;
1418 13622 : std::map<data_expression,int>& data2int_map = this->localmaps_data2int.at(type_no);
1419 13622 : std::map<data_expression,int>::iterator it = data2int_map.find(value);
1420 : std::size_t index;
1421 13622 : if (it != data2int_map.end()) {
1422 13572 : index = it->second;
1423 : } else {
1424 50 : this->localmaps_int2data.at(type_no).push_back(value);
1425 50 : index = this->localmaps_int2data.at(type_no).size() - 1;
1426 50 : data2int_map.insert(std::make_pair(value,index));
1427 : }
1428 13622 : return index;
1429 : }
1430 :
1431 :
1432 3366 : void explorer::to_state_vector(const ltsmin_state& dst_state, int* dst, const ltsmin_state& src_state, int* const& src)
1433 : {
1434 : //std::clog << "to_state_vector: " << dst_state.to_string() << std::endl;
1435 :
1436 3366 : data_expression novalue;
1437 : //std::clog << "-- to_state_vector -- " << std::endl;
1438 3366 : int state_length = info->get_lts_type().get_state_length();
1439 :
1440 3366 : std::string varname = dst_state.get_variable();
1441 3366 : std::string src_varname;
1442 3366 : bool same_var = false;
1443 3366 : if (!(src==nullptr)) {
1444 3360 : src_varname = src_state.get_variable();
1445 3360 : same_var = (varname==src_varname);
1446 : }
1447 : int varindex;
1448 3366 : if (same_var) {
1449 2160 : varindex = src[0];
1450 : } else {
1451 1206 : varindex = this->get_string_index(varname);
1452 : }
1453 3366 : dst[0] = varindex;
1454 : //std::clog << " to_state_vector: DEBUG: varname = " << varname << " index = " << varindex << (same_var ? " SAME VAR": "") << std::endl;
1455 :
1456 :
1457 : // data_expression values[state_length]; N.B. This is not portable C++
1458 3366 : std::vector < data_expression > values(state_length);
1459 :
1460 3366 : if (info->get_reset_option() || src == nullptr) {
1461 : int type_no;
1462 20 : for (int i = 1; i < state_length; i++) {
1463 14 : data_expression default_value = info->get_default_value(i-1);
1464 14 : values[i] = default_value;
1465 14 : type_no = info->get_lts_type().get_state_type_no(i);
1466 14 : dst[i] = this->get_value_index(type_no, values[i]);
1467 14 : }
1468 : } else {
1469 13344 : for (int i = 1; i < state_length; i++) {
1470 9984 : dst[i] = src[i];
1471 : }
1472 : }
1473 3366 : bool error = false;
1474 3366 : const std::vector<data_expression>& parameter_values = dst_state.get_parameter_values();
1475 : std::vector<int> parameter_indices =
1476 3366 : detail::map_at(info->get_variable_parameter_indices(), varname);
1477 : std::vector<std::string> parameter_signatures =
1478 3366 : detail::map_at(info->get_variable_parameter_signatures(), varname);
1479 3366 : std::vector<std::string>::iterator param_signature = parameter_signatures.begin();
1480 3366 : int value_index = 0;
1481 12544 : for(int & parameter_indice : parameter_indices)
1482 : {
1483 9178 : int i = parameter_indice + 1;
1484 9178 : int type_no = info->get_lts_type().get_state_type_no(i);
1485 9178 : values[i] = parameter_values[value_index];
1486 9178 : if (values[i]==novalue)
1487 : {
1488 0 : error = true;
1489 : } else {
1490 9178 : if (src==nullptr) {
1491 : // no source state available; compute index for value.
1492 10 : dst[i] = this->get_value_index(type_no, values[i]);
1493 : }
1494 : else
1495 : {
1496 : // lookup src parameter value
1497 : // FIXME: this could be computed statically: a map from src_var, dst_var and part to boolean
1498 9168 : std::map<int,int> src_param_index_positions = detail::map_at(info->get_variable_parameter_index_positions(), src_state.get_variable());
1499 9168 : std::map<int,int>::iterator src_param_index_position_it = src_param_index_positions.find(parameter_indice);
1500 9168 : if ( src_param_index_position_it != src_param_index_positions.end()
1501 9168 : && src_state.get_parameter_values()[src_param_index_position_it->second] == values[i])
1502 : {
1503 : // src value exists and is equal to the dst value.
1504 : // save to copy index from src_state
1505 : // which has been done earlier
1506 : } else {
1507 : // parameter value has changed or does not exists in src; compute index for value.
1508 3600 : dst[i] = this->get_value_index(type_no, values[i]);
1509 : }
1510 9168 : }
1511 : }
1512 9178 : if (param_signature != parameter_signatures.end())
1513 : {
1514 9178 : ++param_signature;
1515 : }
1516 9178 : value_index++;
1517 : }
1518 3366 : if (error)
1519 : {
1520 0 : throw(std::runtime_error("Error in to_state_vector: NoValue in parameters of dst_state: "
1521 0 : + info->state_to_string(dst_state) + "."));
1522 : }
1523 : //std::clog << "-- to_state_vector: done --" << std::endl;
1524 3366 : }
1525 :
1526 :
1527 13364 : std::string explorer::get_value(int type_no, int index)
1528 : {
1529 : //std::clog << "get_value type_no = " << type_no << " index = " << index << std::endl;
1530 13364 : if (type_no==0)
1531 : {
1532 3366 : return this->get_string_value(index);
1533 : }
1534 : else
1535 : {
1536 9998 : data_expression value = get_data_value(type_no, index);
1537 : //std::stringstream os;
1538 : //write_term_to_text_stream(value, os);
1539 : //std::string s = atermpp::pp(value);
1540 : //return os.str();
1541 9998 : atermpp::aterm t = data::detail::remove_index(value);
1542 9998 : return pp(t);
1543 9998 : }
1544 : }
1545 :
1546 :
1547 9400 : const std::string& explorer::get_string_value(int index)
1548 : {
1549 9400 : if (index >= (int)(localmap_int2string.size()))
1550 : {
1551 0 : throw(std::runtime_error("Error in get_string_value: Value not found for index " + std::to_string(index) + "."));
1552 : }
1553 9400 : return localmap_int2string.at(index);
1554 : }
1555 :
1556 :
1557 15138 : const data_expression& explorer::get_data_value(int type_no, int index)
1558 : {
1559 15138 : std::vector<data_expression>& int2data_map = this->localmaps_int2data.at(type_no);
1560 15138 : if (index >= (int)(int2data_map.size()))
1561 : {
1562 0 : throw(std::runtime_error("Error in get_data_value: Value not found for type_no "
1563 0 : + std::to_string(type_no) + " at index " + std::to_string(index) + "."));
1564 : }
1565 15138 : return int2data_map.at(index);
1566 : }
1567 :
1568 :
1569 1732 : ltsmin_state explorer::from_state_vector(int* const& src)
1570 : {
1571 : //std::clog << "-- from_state_vector(model, src) --" << std::endl;
1572 1732 : data_expression novalue;
1573 1732 : int state_length = info->get_lts_type().get_state_length();
1574 :
1575 1732 : std::string varname = this->get_string_value(src[0]);
1576 : //std::clog << "from_state_vector: varname = " << varname << std::endl;
1577 :
1578 1732 : bool error = false;
1579 :
1580 : // data_expression values[state_length]; N.B. This is not portable C++
1581 1732 : std::vector <data_expression> values(state_length);
1582 :
1583 : int type_no;
1584 6872 : for (int i = 1; i < state_length; i++) {
1585 : //std::clog << "from_state_vector: values: " << i << " (" << src[i] << "): " << std::endl;
1586 5140 : type_no = info->get_lts_type().get_state_type_no(i);
1587 5140 : values[i] = this->get_data_value(type_no, src[i]);
1588 : //std::clog << "from_state_vector: " << values[i].to_string() << std::endl;
1589 : }
1590 : //std::clog << "from_state_vector: values done." << std::endl;
1591 1732 : data::data_expression_vector parameters;
1592 : std::vector<int> parameter_indices =
1593 1732 : detail::map_at(info->get_variable_parameter_indices(), varname);
1594 6480 : for (int & parameter_indice : parameter_indices) {
1595 4748 : if (values[parameter_indice+1]==novalue)
1596 : {
1597 0 : error = true;
1598 : //std::clog << "from_state_vector: varname = " << varname << ", values[" << *param_index+1 << "] = " << values[*param_index+1].to_string() << "(" << src[*param_index+1] << ")" << std::endl;
1599 : }
1600 4748 : parameters.push_back(values[parameter_indice+1]);
1601 : }
1602 1732 : if (error)
1603 : {
1604 0 : throw(std::runtime_error("Error in from_state_vector: NoValue in parameters."));
1605 : }
1606 1732 : data::data_expression_list paramlist(parameters.begin(), parameters.end());
1607 1732 : propositional_variable_instantiation state_expression(varname, paramlist);
1608 : //std::clog << "from_state_vector: state_expression = " << state_expression.to_string() << std::endl;
1609 1732 : ltsmin_state state = this->get_state(state_expression);
1610 : //std::clog << "from_state_vector: state = " << state->to_string() << std::endl;
1611 3464 : return state;
1612 1732 : }
1613 :
1614 :
1615 866 : std::vector<ltsmin_state> explorer::get_successors(const ltsmin_state& state)
1616 : {
1617 : //std::cout << "get_successors: " << state->to_string() << std::endl;
1618 866 : std::vector<ltsmin_state> result;
1619 :
1620 866 : pbes_expression e = state.to_pbes_expression();
1621 866 : assert(core::detail::check_term_PropVarInst(e));
1622 866 : if (state.get_variable()=="true")
1623 : {
1624 : // Adding true=true
1625 0 : result.push_back(state);
1626 : }
1627 866 : else if (state.get_variable()=="false")
1628 : {
1629 : // Adding false=false
1630 0 : result.push_back(state);
1631 : }
1632 : else
1633 : {
1634 : std::set<pbes_expression> successors
1635 866 : = pgg->get_successors(e);
1636 866 : operation_type type = detail::map_at(info->get_variable_types(), state.get_variable());
1637 2546 : for (const auto & successor : successors) {
1638 1680 : if (is_propositional_variable_instantiation(successor)) {
1639 1680 : result.push_back(get_state(atermpp::down_cast<propositional_variable_instantiation>(successor)));
1640 0 : } else if (is_true(successor)) {
1641 0 : if (type != parity_game_generator::PGAME_AND)
1642 : {
1643 0 : result.push_back(true_state());
1644 : }
1645 0 : } else if (is_false(successor)) {
1646 0 : if (type != parity_game_generator::PGAME_OR)
1647 : {
1648 0 : result.push_back(false_state());
1649 : }
1650 : } else {
1651 0 : throw(std::runtime_error("!! Successor is NOT a propvar: " + pbes_system::pp(successor)));
1652 : }
1653 : }
1654 866 : }
1655 1732 : return result;
1656 866 : }
1657 :
1658 :
1659 866 : std::vector<ltsmin_state> explorer::get_successors(const ltsmin_state& state,
1660 : int group)
1661 : {
1662 : //std::clog << "get_successors: group=" << group << std::endl;
1663 866 : std::vector<ltsmin_state> result;
1664 :
1665 866 : if (group == 0 && state.get_variable()=="true")
1666 : {
1667 : // Adding true=true
1668 0 : result.push_back(state);
1669 : }
1670 866 : else if (group == 1 && state.get_variable()=="false")
1671 : {
1672 : // Adding false=false
1673 0 : result.push_back(state);
1674 : }
1675 : else
1676 : {
1677 866 : std::string varname = state.get_variable();
1678 866 : std::string group_varname = info->get_transition_variable_names()[group];
1679 866 : if (varname==group_varname)
1680 : {
1681 866 : pbes_expression e = state.to_pbes_expression();
1682 : std::set<pbes_expression> successors
1683 866 : = pgg->get_successors(e, group_varname,
1684 866 : info->get_transition_expressions()[group]);
1685 866 : operation_type type = detail::map_at(info->get_variable_types(), state.get_variable());
1686 2546 : for (const auto & successor : successors) {
1687 : //std::clog << " * successor: " << pp(*expr) << std::endl;
1688 1680 : if (is_propositional_variable_instantiation(successor)) {
1689 1680 : result.push_back(get_state(atermpp::down_cast<propositional_variable_instantiation>(successor)));
1690 0 : } else if (is_true(successor)) {
1691 0 : if (type != parity_game_generator::PGAME_AND)
1692 : {
1693 0 : result.push_back(true_state());
1694 : }
1695 0 : } else if (is_false(successor)) {
1696 0 : if (type != parity_game_generator::PGAME_OR)
1697 : {
1698 0 : result.push_back(false_state());
1699 : }
1700 : } else {
1701 0 : throw(std::runtime_error("!! Successor is NOT a propvar: " + pbes_system::pp(successor)));
1702 : }
1703 : }
1704 866 : }
1705 866 : }
1706 866 : return result;
1707 0 : }
1708 :
1709 :
1710 : } // namespace pbes_system
1711 :
1712 : } // namespace mcrl2
|
