mCRL2
Loading...
Searching...
No Matches
pbes_explorer.cpp
Go to the documentation of this file.
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//
11#include <climits>
12#include <queue>
13
17#include "mcrl2/pbes/io.h"
19
20
21namespace mcrl2
22{
23
24namespace pbes_system
25{
26
27namespace detail
28{
29 template <typename MapContainer>
30 typename MapContainer::mapped_type map_at(const MapContainer& m, typename MapContainer::key_type key)
31 {
32 typename MapContainer::const_iterator i = m.find(key);
33 if (i == m.end())
34 {
35 throw mcrl2::runtime_error("map_at: key is not present in the map: " + key);
36 }
37 return i->second;
38 }
39} // namespace detail
40
42
43lts_type::lts_type(int state_length)
44{
45 this->state_length = state_length;
46}
47
48
50{}
51
52
54{
55 return this->state_length;
56}
57
58
60{
61 return this->state_type_list.size();
62}
63
64
65int lts_type::get_state_type_no(int part) const
66{
67 return this->state_type_no.at(part);
68}
69
70std::string lts_type::get_state_type_name(int type_no) const
71{
72 return this->state_type_list.at(type_no);
73}
74
75const std::vector<std::string>& lts_type::get_state_names() const
76{
77 return state_names;
78}
79
80
81const std::vector<std::string>& lts_type::get_state_types() const
82{
83 return state_types;
84}
85
86
88{
89 return this->state_label_names.size();
90}
91
92
93const std::vector<std::string>& lts_type::get_state_labels() const
94{
95 return state_label_names;
96}
97
98
99const std::vector<std::string>& lts_type::get_state_label_types() const
100{
101 return state_label_types;
102}
103
104
106{
107 return this->edge_label_names.size();
108}
109
110
111const std::vector<std::string>& lts_type::get_edge_labels() const
112{
113 return edge_label_names;
114}
115
116
117const std::vector<std::string>& lts_type::get_edge_label_types() const
118{
119 return edge_label_types;
120}
121
122
123void 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 this->state_names.push_back(name);
129 this->state_types.push_back(type);
130 std::size_t type_index;
131 std::map<std::string,int>::iterator type_index_it = this->state_type_index.find(type);
132 if (type_index_it != this->state_type_index.end()) {
133 type_index = type_index_it->second;
134 } else {
135 this->state_type_list.push_back(type);
136 type_index = this->state_type_list.size() - 1;
137 this->state_type_index[type] = type_index;
138 }
139 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}
142
143
144void lts_type::add_state_label(const std::string& name,
145 const std::string& type)
146{
147 this->state_label_names.push_back(name);
148 this->state_label_types.push_back(type);
149}
150
151
152void lts_type::add_edge_label(const std::string& name,
153 const std::string& type)
154{
155 this->edge_label_names.push_back(name);
156 this->edge_label_types.push_back(type);
157}
158
159
160
161
163
164lts_info::lts_info(pbes& p, detail::pbes_greybox_interface* pgg, bool reset = false, bool always_split = false):
165 p(p),
166 pgg(pgg),
167 reset_option(reset),
168 always_split_option(always_split),
169 type(0)
170{
171 if (!detail::is_ppg(p))
172 {
173 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;
179}
180
181
183{
184 //std::clog << "pbes_type:" << std::endl;
185 mCRL2log(log::verbose) << "Compute LTS type." << std::endl;
186 std::vector<std::string> params;
187 std::map<std::string,std::string> paramtypes;
188 data::representative_generator default_expression_generator(p.data());
189
190 for (const auto& eqn : p.equations())
191 {
192 //std::clog << core::pp((*eqn).symbol()) << " " << (*eqn).variable().name()
193 // << std::endl;
194
195 propositional_variable var = eqn.variable();
196 for (const variable& varparam: var.parameters())
197 {
198 std::string signature = get_param_signature(varparam);
199 bool new_param = true;
200 for (auto & param : params) {
201 if (signature == param) new_param = false;
202 }
203 if (new_param) {
204 params.push_back(signature);
205 paramtypes[signature] = core::pp(varparam.sort());
206 //std::clog << "paramtypes[" << signature << "] = " << paramtypes[signature] << std::endl;
207 data_expression e(default_expression_generator(varparam.sort()));
209 this->param_default_values.push_back(atermpp::down_cast<const data::data_expression>(e1));
210 }
211 }
212 //params.sort();
213 }
214 this->type = lts_type(1 + params.size());
215 this->type.add_state("var", "string"); // Propositional variable name
216
217 int i = 0;
218 for (const std::string& signature: params) {
219 this->type.add_state(signature, paramtypes[signature]);
220 this->param_index[signature] = i;
221 i++;
222 }
223
224 this->type.add_state_label("priority", "int");
225 this->type.add_state_label("type", "int");
226
227 //this->type->add_edge_label("", "");
228 //std::clog << "-- end of pbes_type." << std::endl;
229 mCRL2log(log::verbose) << "end of compute_lts_type." << std::endl;
230}
231
232
234{
235 std::string varname = std::string(propvar.name());
236 data::variable_list params = this->variable_parameters[varname];
237 const data::data_expression_list& values = propvar.parameters();
238 if (params.size() != values.size())
239 {
240 return false;
241 }
242 else
243 {
244 data::variable_list::const_iterator param_it = params.begin();
245 for(const auto & value : values)
246 {
247 if (!data::is_variable(value))
248 {
249 return false;
250 }
251 else
252 {
253 data::variable param(*param_it);
254 data::variable param_expr(value);
255 if (param != param_expr)
256 {
257 return false;
258 }
259 }
260 if (param_it != params.end())
261 {
262 ++param_it;
263 }
264 }
265 }
266 if(params != values)
267 {
268 throw mcrl2::runtime_error("is_pass_through_state check failed on " + data::pp(params) + " " + data::pp(values));
269 }
270 return true;
271}
272
273
275{
277 {
278 return 1;
279 }
280 else if (is_and(e) || is_or(e) || is_imp(e))
281 {
283 }
284 else if (is_forall(e) || is_exists(e))
285 {
287 {
288 return INT_MAX;
289 }
290 else
291 {
292 return 0;
293 }
294 }
295 else if (is_not(e))
296 {
298 }
299 else if (is_data(e))
300 {
301 return 0;
302 }
303 else
304 {
305 throw(std::runtime_error("Unexpected expression: " + pbes_system::pp(e)));
306 }
307}
308
309std::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 std::vector<pbes_expression> result;
312 std::vector<pbes_expression> parts;
314 {
315 result.push_back(e);
316 }
318 {
319 result.push_back(e);
320 }
321 else if (is_and(e)) {
322 parts = split_conjuncts(e, true);
323 } else if (is_or(e)) {
324 parts = split_disjuncts(e, true);
325 } else {
326 parts.push_back(e);
327 }
328
329 bool pass_through = true;
330
331 for(std::vector<pbes_expression>::iterator p_it = parts.begin(); pass_through && p_it != parts.end(); ++p_it)
332 {
333 pbes_expression part = *p_it;
335 {
336 // Try to substitute the variable instantiation with the associated expression
337
339 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 std::string varname = std::string(propvar.name());
345 int priority = this->variable_priority[varname];
346 operation_type type = this->variable_type[varname];
347 pbes_expression expr = this->variable_expression[varname];
348
349 if ((priority == current_priority) &&
350 (current_type == type || is_simple_expression(expr) || count_variables(expr) <= 1) &&
351 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 std::set<std::string> new_vars_stack(vars_stack.begin(), vars_stack.end());
362 new_vars_stack.insert(varname);
363 std::vector<pbes_expression> part_result = split_expression_and_substitute_variables(expr, current_priority, current_type, new_vars_stack);
364 result.insert(result.end(), part_result.begin(), part_result.end());
365 }
366 else
367 {
368 result.push_back(part);
369 }
370 }
371 else
372 {
373 pass_through = false;
374 }
375 }
376 else
377 {
378 pass_through = false;
379 }
380 }
381 if (!pass_through)
382 {
383 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 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 result.clear();
394 result.push_back(e);
395 }
396 }
397 return result;
398}
399
400
402{
403 mCRL2log(log::verbose) << "Compute transition groups." << std::endl;
404
405 int group = 0;
406 int priority = 0;
409 detail::ppg_visitor checker;
410
411 std::string name = "true";
413 this->variables[name] = t;
414 this->variable_type[name] = type;
415 this->variable_symbol[name] = symbol;
416 this->variable_priority[name] = priority;
417 this->variable_parameters[name] = t.parameters();
418 this->variable_parameter_signatures[name] = get_param_sequence(t.parameters());
419 this->variable_parameter_indices[name] = this->get_param_indices(t.parameters());
420 this->variable_parameter_index_positions[name] = this->get_param_index_positions(t.parameters());
421 this->transition_expression_plain.push_back(true_());
423 this->transition_variable_name.push_back(name);
424 this->transition_type.push_back(type);
425 group++;
426 priority++;
427
428 name = "false";
430 symbol = fixpoint_symbol::mu();
432 this->variables[name] = f;
433 this->variable_type[name] = type;
434 this->variable_symbol[name] = symbol;
435 this->variable_priority[name] = priority;
436 this->variable_parameters[name] = f.parameters();
437 this->variable_parameter_signatures[name] = get_param_sequence(f.parameters());
438 this->variable_parameter_indices[name] = this->get_param_indices(f.parameters());
439 this->variable_parameter_index_positions[name] = this->get_param_index_positions(f.parameters());
440 this->transition_expression_plain.push_back(false_());
442 this->transition_variable_name.push_back(name);
443 this->transition_type.push_back(type);
444 group++;
445 priority++;
446
447 symbol = fixpoint_symbol::nu();
448
449 for (auto & eqn : p.equations()) {
450 pbes_expression expr = pgg->get_pbes_equation(eqn.variable().name()).formula();
451 std::string variable_name = eqn.variable().name();
452 this->variables[variable_name] = eqn.variable();
454 this->variable_type[variable_name] = type;
455 this->variable_symbol[variable_name] = eqn.symbol();
456 if (eqn.symbol() != symbol) {
457 priority++;
458 symbol = eqn.symbol();
459 }
460 mCRL2log(log::debug) << "Adding var " << variable_name << ", priority=" << priority << ", symbol=" << symbol << std::endl;
461 this->variable_priority[variable_name] = priority;
462 this->variable_parameters[variable_name] = eqn.variable().parameters();
463 this->variable_parameter_signatures[variable_name] = get_param_sequence(eqn.variable().parameters());
464 this->variable_parameter_indices[variable_name] = this->get_param_indices(eqn.variable().parameters());
465 this->variable_parameter_index_positions[variable_name] = this->get_param_index_positions(eqn.variable().parameters());
466 this->variable_expression[variable_name] = expr;
467 }
468
469 // Skip 'unused' equations....
470 std::set<std::string> variable_set;
471 {
473 std::queue<std::string> variable_queue;
474 variable_queue.push(init.name());
475 variable_set.insert(init.name());
476 while (!variable_queue.empty())
477 {
478 std::string var = variable_queue.front();
479 variable_queue.pop();
480 type = this->variable_type[var];
481 priority = this->variable_priority[var];
482 pbes_expression expr = this->variable_expression[var];
483 std::set<std::string> vars_stack;
484 std::vector<pbes_expression> expression_parts = split_expression_and_substitute_variables(expr, priority, type, vars_stack);
485 for (std::vector<pbes_expression>::const_iterator e =
486 expression_parts.begin(); e != expression_parts.end(); ++e) {
487 std::set<std::string> occ_vars = lts_info::occ(*e);
488 for (const auto & var_str : variable_set)
489 {
490 occ_vars.erase(var_str);
491 }
492 for(const auto & occ_var : occ_vars)
493 {
494 variable_queue.push(occ_var);
495 }
496 variable_set.insert(occ_vars.begin(), occ_vars.end());
497 }
498 }
499 mCRL2log(log::debug) << "Set of 'used' variables: " << std::endl;
500 for (const auto & var_str : variable_set)
501 {
502 mCRL2log(log::debug) << " " << var_str << std::endl;
503 }
504 mCRL2log(log::debug) << std::endl;
505 }
506
507 for (auto & eqn : p.equations()) {
508 std::string variable_name = eqn.variable().name();
509 if (variable_set.find(variable_name) != variable_set.end())
510 {
511 type = this->variable_type[variable_name];
512 priority = this->variable_priority[variable_name];
513 pbes_expression expr = this->variable_expression[variable_name];
514 std::set<std::string> vars_stack;
515 mCRL2log(log::debug) << std::endl << "Generating groups for equation " << variable_name << std::endl;
516 std::vector<pbes_expression> expression_parts = split_expression_and_substitute_variables(expr, priority, type, vars_stack);
517 for (std::vector<pbes_expression>::const_iterator e =
518 expression_parts.begin(); e != expression_parts.end(); ++e) {
519 this->transition_expression_plain.push_back(*e);
521 this->transition_variable_name.push_back(variable_name);
522 this->transition_type.push_back(type);
523 mCRL2log(log::debug) << "Add transition group " << group << ": "
524 << (type==parity_game_generator::PGAME_AND ? "AND" : "OR") << " " << variable_name << " "
525 << pbes_system::pp(*e) << std::endl;
526 group++;
527 }
528 }
529 }
530 number_of_groups = group;
531 //std::clog << "Added " << group << " transition groups." << std::endl;
532 mCRL2log(log::debug) << "end of compute_transition_groups." << std::endl;
533}
534
535
537{
538 mCRL2log(log::verbose) << "Compute dependency matrix." << std::endl;
539 for(int group=0; group < number_of_groups; group++)
540 {
541 std::vector<bool> dep_row;
542 std::vector<bool> read_row;
543 std::vector<bool> write_row;
544 bool r = is_read_dependent_propvar(group);
545 bool w = is_write_dependent_propvar(group);
546 bool d = r || w;
547 dep_row.push_back(d);
548 read_row.push_back(r);
549 write_row.push_back(w);
550 for (int part = 1; part < type.get_state_length(); part++)
551 {
552 r = is_read_dependent_parameter(group, part);
553 w = is_write_dependent_parameter(group, part);
554 d = r || w;
555 dep_row.push_back(d);
556 read_row.push_back(r);
557 write_row.push_back(w);
558 }
559 matrix[group] = dep_row;
560 read_matrix[group] = read_row;
561 write_matrix[group] = write_row;
562 }
563 mCRL2log(log::verbose) << "end of compute_dependency_matrix." << std::endl;
564}
565
566
568{
569 return reset_option;
570}
571
572
574{
575 return number_of_groups;
576}
577
578
579const std::vector<pbes_expression>& lts_info::get_transition_expressions() const
580{
582}
583
584
585const std::vector<std::string>& lts_info::get_transition_variable_names() const
586{
588}
589
590
591const std::vector<lts_info::operation_type>& lts_info::get_transition_types() const
592{
593 return transition_type;
594}
595
596
597const std::map<std::string, propositional_variable>& lts_info::get_variables() const
598{
599 return variables;
600}
601
602
603const std::map<std::string, lts_info::operation_type>& lts_info::get_variable_types() const
604{
605 return variable_type;
606}
607
608const std::map<std::string, fixpoint_symbol>& lts_info::get_variable_symbols() const
609{
610 return variable_symbol;
611}
612
613
614const std::map<std::string, int>& lts_info::get_variable_priorities() const
615{
616 return variable_priority;
617}
618
619
620const std::map<std::string, data::variable_list>& lts_info::get_variable_parameters() const
621{
622 return variable_parameters;
623}
624
625
626const std::map<std::string, std::vector<std::string> >& lts_info::get_variable_parameter_signatures() const
627{
629}
630
631
632const std::map<std::string, std::vector<int> >& lts_info::get_variable_parameter_indices() const
633{
635}
636
637
638const std::map<std::string, std::map<int,int> >& lts_info::get_variable_parameter_index_positions() const
639{
641}
642
643
645{
646 return type;
647}
648
649
650const std::map<int,std::vector<bool> >& lts_info::get_dependency_matrix() const
651{
652 return matrix;
653}
654
655
656const std::map<int,std::vector<bool> >& lts_info::get_read_matrix() const
657{
658 return read_matrix;
659}
660
661
662const std::map<int,std::vector<bool> >& lts_info::get_write_matrix() const
663{
664 return write_matrix;
665}
666
667
668int lts_info::get_index(const std::string& signature)
669{
670 return param_index[signature];
671}
672
673
675{
676 return param_default_values.at(index);
677}
678
679
681{
682 return true;
683}
684
685
687{
688 if (group==0 || group==1) return false;
689 std::string p = type.get_state_names()[part];
690 mCRL2log(log::debug) << "is_read_dependent_parameter (group=" << group << ", part=" << part << " [" << p << "]" << std::endl;
692 std::string X = transition_variable_name[group];
693 std::set<std::string> params = lts_info::get_param_set(variable_parameters[X]);
694 if (params.find(p) == params.end())
695 {
696 return false; // Parameter is not in params(X).
697 }
698 else
699 {
700 std::set<std::string> usedSet = used(phi);
701 std::set<std::string> changedSet = changed(phi);
702 std::set<std::string> copySet = copied(phi);
703 std::set<std::string> changedAndCopied;
704 std::set_intersection(changedSet.begin(), changedSet.end(), copySet.begin(), copySet.end(),
705 std::inserter(changedAndCopied, changedAndCopied.end()));
706
707 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 return false; // Parameter is not in used(phi).
711 }
712 else
713 {
714 return true; // Parameter is both in used(phi) and in params(X).
715 }
716 }
717
718}
719
720
722{
723 if (group==0 || group==1) return false;
725 std::string X = transition_variable_name[group];
726 if (lts_info::tf(phi))
727 {
728 return true;
729 }
730 std::set<std::string> occ = lts_info::occ(phi);
731 if (occ.empty())
732 {
733 return false; // Not dependent if occ(phi) == {}.
734 }
735 else if (occ.size() == 1)
736 {
737 bool containsX = occ.find(X) != occ.end();
738 return !containsX; // Not dependent if occ(phi) == {X}.
739 }
740 else
741 {
742 return true; // Dependent, because occ(phi) contains multiple elements.
743 }
744}
745
746
748{
749 if (group==0 || group==1) return false;
750 std::string p = type.get_state_names().at(part);
752 std::string X = transition_variable_name[group];
753 if (this->reset_option) {
754 if (lts_info::tf(phi))
755 {
756 // phi may have boolean result (not only propositional variable instantiations)
757 return true;
758 }
759 std::set<std::string> params = lts_info::get_param_set(variable_parameters[X]);
760 std::set<std::string> resetSet = reset(phi, params);
761 if (resetSet.find(p) != resetSet.end())
762 {
763 return true; // Dependent, because p in reset(phi, params(X)).
764 }
765 }
766 std::set<std::string> changedSet = changed(phi);
767 bool changedSetContainsP = (changedSet.find(p) != changedSet.end());
768 return changedSetContainsP; // Dependent, because p in changed(phi, {}).
769}
770
771
772std::set<std::string> lts_info::changed(const pbes_expression& phi)
773{
774 std::set<std::string> empty;
775 return changed(phi, empty);
776}
777
778
779std::set<std::string> lts_info::changed(const pbes_expression& phi, const std::set<std::string>& L)
780{
781 std::set<std::string> result;
782 if (is_not(phi))
783 {
784 result = changed(pbes_system::accessors::arg(phi), L);
785 }
786 else if (is_and(phi) || is_or(phi) || is_imp(phi))
787 {
788 std::set<std::string> l = changed(pbes_system::accessors::left(phi), L);
789 result.insert(l.begin(), l.end());
790 std::set<std::string> r = changed(pbes_system::accessors::right(phi), L);
791 result.insert(r.begin(), r.end());
792 }
793 else if (is_forall(phi) || is_exists(phi))
794 {
795 std::set<std::string> LL;
796 LL.insert(L.begin(), L.end());
798 for (auto variable : vars)
799 {
800 LL.insert(get_param_signature(variable));
801 }
802 result = changed(pbes_system::accessors::arg(phi), LL);
803 }
805 {
806 std::vector<std::string> var_param_signatures =
807 variable_parameter_signatures[atermpp::down_cast<propositional_variable_instantiation>(phi).name()];
808 data::data_expression_list values = atermpp::down_cast<propositional_variable_instantiation>(phi).parameters();
809 assert(var_param_signatures.size() == values.size());
811 for (std::vector<std::string>::const_iterator param =
812 var_param_signatures.begin(); param != var_param_signatures.end(); ++param) {
813 std::string param_signature = *param;
814 if (data::is_variable(*val))
815 {
816 const variable& value = atermpp::down_cast<variable>(*val);
817 std::string value_signature = get_param_signature(value);
818 if (param_signature != value_signature || L.find(value_signature) != L.end())
819 {
820 result.insert(param_signature);
821 }
822 }
823 else
824 {
825 result.insert(param_signature);
826 }
827 if (val != values.end()) {
828 ++val;
829 }
830 }
831 }
832 return result;
833}
834
835
836std::set<std::string> lts_info::reset(const pbes_expression& phi, const std::set<std::string>& d)
837{
838 std::set<std::string> result;
839 if (is_not(phi))
840 {
841 result = reset(pbes_system::accessors::arg(phi), d);
842 }
843 else if (is_and(phi) || is_or(phi) || is_imp(phi))
844 {
845 std::set<std::string> l = reset(pbes_system::accessors::left(phi), d);
846 result.insert(l.begin(), l.end());
847 std::set<std::string> r = reset(pbes_system::accessors::right(phi), d);
848 result.insert(r.begin(), r.end());
849 }
850 else if (is_forall(phi) || is_exists(phi))
851 {
852 result = reset(pbes_system::accessors::arg(phi), d);
853 }
855 {
856 std::set<std::string> params;
857 std::vector<std::string> var_params =
858 variable_parameter_signatures[atermpp::down_cast<propositional_variable_instantiation>(phi).name()];
859 for (std::vector<std::string>::const_iterator param =
860 var_params.begin(); param != var_params.end(); ++param) {
861 std::string signature = *param;
862 params.insert(signature);
863 }
864 for (auto signature : d) {
865 if (params.find(signature) == params.end())
866 {
867 result.insert(signature);
868 }
869 }
870 }
871 return result;
872}
873
874
876{
877 if (is_not(phi))
878 {
879 return tf(pbes_system::accessors::arg(phi));
880 }
881 else if (is_and(phi) || is_or(phi) || is_imp(phi))
882 {
884 }
885 else if (is_forall(phi) || is_exists(phi))
886 {
887 return tf(pbes_system::accessors::arg(phi));
888 }
890 {
891 return false;
892 }
893 return true;
894}
895
896
897std::set<std::string> lts_info::occ(const pbes_expression& expr)
898{
899 std::set<std::string> result;
901 {
902 result.insert(atermpp::down_cast<propositional_variable_instantiation>(expr).name());
903 }
904 else if (is_and(expr) || is_or(expr) ||is_imp(expr))
905 {
906 std::set<std::string> l = occ(pbes_system::accessors::left(expr));
907 result.insert(l.begin(), l.end());
908 std::set<std::string> r = occ(pbes_system::accessors::right(expr));
909 result.insert(r.begin(), r.end());
910 }
911 else if (is_forall(expr) || is_exists(expr) || is_not(expr))
912 {
913 result = occ(pbes_system::accessors::arg(expr));
914 }
915 return result;
916}
917
918
919std::set<std::string> lts_info::free(const pbes_expression& expr)
920{
921 std::set<std::string> result;
923 {
924 result.insert(get_param_signature(var));
925 }
926 return result;
927}
928
929
930std::set<std::string> lts_info::used(const pbes_expression& expr)
931{
932 std::set<std::string> emptySet;
933 return used(expr, emptySet);
934}
935
936
937std::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 std::set<std::string> result;
941 if (is_data(expr))
942 {
943 std::set<std::string> fv = free(expr);
944 result.insert(fv.begin(), fv.end());
945 }
947 {
948 data::variable_list var_params =
949 variable_parameters[atermpp::down_cast<propositional_variable_instantiation>(expr).name()];
950 data::data_expression_list values = atermpp::down_cast<propositional_variable_instantiation>(expr).parameters();
951 assert(var_params.size() == values.size());
953 for (auto parameter : var_params) {
954 std::string param_signature = get_param_signature(parameter);
955 if (data::is_variable(*val))
956 {
957 const variable& value = atermpp::down_cast<variable>(*val);
958 std::string value_signature = get_param_signature(value);
959 if (param_signature != value_signature || L.find(value_signature) != L.end())
960 {
961 result.insert(value_signature);
962 }
963 }
964 else
965 {
966 // add free variables in data expression
967 std::set<std::string> l = used(*val, L);
968 result.insert(l.begin(), l.end());
969 }
970 if (val != values.end()) {
971 ++val;
972 }
973 }
974 }
975 else if (is_and(expr) || is_or(expr) || is_imp(expr))
976 {
977 std::set<std::string> l = used(pbes_system::accessors::left(expr), L);
978 result.insert(l.begin(), l.end());
979 std::set<std::string> r = used(pbes_system::accessors::right(expr), L);
980 result.insert(r.begin(), r.end());
981 }
982 else if (is_not(expr))
983 {
984 result = used(pbes_system::accessors::arg(expr), L);
985 }
986 else if (is_forall(expr) || is_exists(expr))
987 {
988 std::set<std::string> LL;
989 LL.insert(L.begin(), L.end());
991 for (auto variable : vars)
992 {
993 LL.insert(get_param_signature(variable));
994 }
995 result = used(pbes_system::accessors::arg(expr), LL);
996 }
997 return result;
998}
999
1000
1001std::set<std::string> lts_info::copied(const pbes_expression& expr)
1002{
1003 std::set<std::string> emptySet;
1004 return copied(expr, emptySet);
1005}
1006
1007
1008std::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 std::set<std::string> result;
1012 if (is_data(expr))
1013 {
1014 // skip
1015 }
1017 {
1018 data::variable_list var_params =
1019 variable_parameters[atermpp::down_cast<propositional_variable_instantiation>(expr).name()];
1020 data::data_expression_list values = atermpp::down_cast<propositional_variable_instantiation>(expr).parameters();
1021 assert(var_params.size() == values.size());
1023 for (auto parameter : var_params) {
1024 std::string param_signature = get_param_signature(parameter);
1025 if (data::is_variable(*val))
1026 {
1027 const variable& value = atermpp::down_cast<variable>(*val);
1028 std::string value_signature = get_param_signature(value);
1029 if (param_signature == value_signature && L.find(value_signature) == L.end())
1030 {
1031 result.insert(value_signature);
1032 }
1033 }
1034 if (val != values.end()) {
1035 ++val;
1036 }
1037 }
1038 }
1039 else if (is_and(expr) || is_or(expr) || is_imp(expr))
1040 {
1041 std::set<std::string> l = copied(pbes_system::accessors::left(expr), L);
1042 result.insert(l.begin(), l.end());
1043 std::set<std::string> r = copied(pbes_system::accessors::right(expr), L);
1044 result.insert(r.begin(), r.end());
1045 }
1046 else if (is_not(expr))
1047 {
1048 result = copied(pbes_system::accessors::arg(expr), L);
1049 }
1050 else if (is_forall(expr) || is_exists(expr))
1051 {
1052 std::set<std::string> LL;
1053 LL.insert(L.begin(), L.end());
1055 for (auto variable : vars)
1056 {
1057 LL.insert(get_param_signature(variable));
1058 }
1059 result = copied(pbes_system::accessors::arg(expr), LL);
1060 }
1061 return result;
1062}
1063
1064
1066{
1067 //std::clog << "info::to_string" << std::endl;
1068 std::string result;
1069 std::stringstream ss;
1070 operation_type type = detail::map_at(get_variable_types(), state.get_variable());
1071 ss << (type==parity_game_generator::PGAME_AND ? "AND" : "OR");
1072 ss << ":" << state.get_variable();
1073 ss << "(";
1074 const std::vector<data_expression>& param_values = state.get_parameter_values();
1075 std::vector<std::string> param_signatures =
1077 std::vector<std::string>::const_iterator param_signature =
1078 param_signatures.begin();
1079 for (std::vector<data_expression>::const_iterator param_value =
1080 param_values.begin(); param_value != param_values.end(); ++param_value) {
1081 if (param_value != param_values.begin())
1082 ss << ", ";
1083 ss << *param_signature << " = ";
1084 ss << *param_value;
1085 if (param_signature != param_signatures.end())
1086 {
1087 ++param_signature;
1088 }
1089 }
1090 ss << ")";
1091 result = ss.str();
1092 return result;
1093}
1094
1095
1096std::set<std::string> lts_info::get_param_set(const data::variable_list& params)
1097{
1098 std::set<std::string> result;
1099 for (auto parameter : params) {
1100 result.insert(get_param_signature(parameter));
1101 }
1102 return result;
1103}
1104
1105
1106std::vector<std::string> lts_info::get_param_sequence(const data::variable_list& params)
1107{
1108 std::vector<std::string> result;
1109 for (auto parameter : params) {
1110 result.push_back(get_param_signature(parameter));
1111 }
1112 return result;
1113}
1114
1115
1117{
1118 std::vector<int> result;
1119 for (auto parameter : params) {
1120 int index = this->get_index(get_param_signature(parameter));
1121 result.push_back(index);
1122 }
1123 return result;
1124}
1125
1126
1128{
1129 std::map<int,int> result;
1130 int i = 0;
1131 for (auto parameter : params) {
1132 int index = this->get_index(get_param_signature(parameter));
1133 result.insert(std::make_pair(index,i));
1134 i++;
1135 }
1136 return result;
1137}
1138
1139
1140std::map<variable,std::string> lts_info::variable_signatures;
1141
1142
1144{
1145 std::map<variable,std::string>::const_iterator i = variable_signatures.find(param);
1146 if (i == variable_signatures.end())
1147 {
1148 std::string paramname = param.name();
1149 std::string paramtype = core::pp(param.sort());
1150 std::string signature = get_param_signature(paramname, paramtype);
1151 variable_signatures[param] = signature;
1152 return signature;
1153 }
1154 return i->second;
1155}
1156
1157
1158std::string lts_info::get_param_signature(const std::string& paramname,
1159 const std::string& paramtype)
1160{
1161 return paramname + ":" + paramtype;
1162}
1163
1164
1165
1166
1167// ltsmin_state
1168
1169ltsmin_state::ltsmin_state(const std::string& varname)
1170{
1171 this->var = varname;
1172}
1173
1174
1175ltsmin_state::ltsmin_state(const std::string& varname,
1176 const pbes_expression& e)
1177{
1178 data_expression novalue;
1179 //std::clog << "ltsmin_state v = " << pp(v) << std::endl;
1180 this->var = varname;
1182 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 const data::data_expression_list& values = atermpp::down_cast<propositional_variable_instantiation>(e).parameters();
1185 for (const auto & value : values)
1186 {
1187 if (value == novalue)
1188 {
1189 throw(std::runtime_error("Error in ltsmin_state: state expression contains NoValue: "
1190 + pp(e)));
1191 }
1192 this->add_parameter_value(value);
1193 //std::clog << "ltsmin_state: " << *val << std::endl;
1194 }
1195 //std::clog << std::endl;
1196 } else {
1197 throw(std::runtime_error("Not a valid state expression! " + pp(e)));
1198 }
1199}
1200
1201bool ltsmin_state::operator<( const ltsmin_state& other ) const
1202{
1203 if (this->var < other.var) return true;
1204 else if (this->var == other.var)
1205 {
1206 if (param_values.size() < other.param_values.size()) return true;
1207 else if (param_values.size() == other.param_values.size())
1208 {
1209 if (param_values < other.param_values) return true;
1210 }
1211 }
1212 return false;
1213}
1214
1215
1216bool ltsmin_state::operator==( const ltsmin_state& other ) const
1217{
1218 return this->var==other.var
1219 && param_values.size()==other.param_values.size()
1220 && param_values == other.param_values;
1221}
1222
1223
1225{
1226 return var;
1227}
1228
1229
1230const std::vector<data_expression>& ltsmin_state::get_parameter_values() const
1231{
1232 return param_values;
1233}
1234
1235
1237{
1238 param_values.push_back(value);
1239}
1240
1241
1243{
1244 data::data_expression_vector parameter_values;
1245 for (const auto & param_value : param_values) {
1246 parameter_values.push_back(param_value);
1247 }
1248 data::data_expression_list parameter_values_list(parameter_values.begin(), parameter_values.end());
1249 // Create propositional variable instantiation.
1252 return workaround::return_std_move(expr);
1253}
1254
1255
1257{
1258 std::string result;
1259 std::stringstream ss;
1260 ss << (type==parity_game_generator::PGAME_AND ? "AND" : "OR");
1261 ss << ":" << var;
1262 ss << "[" << std::endl;
1263 for (std::vector<data_expression>::const_iterator entry =
1264 param_values.begin(); entry != param_values.end(); ++entry) {
1265 if (entry != param_values.begin())
1266 ss << std::endl << " value = ";
1267 ss << *entry;
1268 }
1269 ss << "]";
1270 result = ss.str();
1271 return result;
1272}
1273
1274
1275
1276
1278
1279explorer::explorer(const std::string& filename, const std::string& rewrite_strategy = "jittyc", bool reset_flag = false, bool always_split_flag = false)
1280{
1281 load_pbes(p, filename);
1282 for (auto & eqn : p.equations()) {
1283 std::string variable_name = eqn.variable().name();
1284 //std::clog << "varname = " << variable_name << std::endl;
1285 }
1287 if (!detail::is_ppg(p))
1288 {
1289 mCRL2log(log::info) << "Rewriting to PPG..." << std::endl;
1290 p = detail::to_ppg(p);
1291 mCRL2log(log::info) << "Rewriting done." << std::endl;
1292 }
1293 this->pgg = new detail::pbes_greybox_interface(p, true, true, data::parse_rewrite_strategy(rewrite_strategy));
1294 this->info = new lts_info(p, pgg, reset_flag, always_split_flag);
1295 //std::clog << "explorer" << std::endl;
1296 for (std::size_t i = 0; i < info->get_lts_type().get_number_of_state_types(); ++i) {
1297 std::map<data_expression,int> data2int_map;
1298 this->localmaps_data2int.push_back(data2int_map);
1299 std::vector<data_expression> int2data_map;
1300 this->localmaps_int2data.push_back(int2data_map);
1301 }
1302 //std::clog << "-- end of explorer." << std::endl;
1303}
1304
1305
1306explorer::explorer(const pbes& p_, const std::string& rewrite_strategy = "jittyc", bool reset_flag = false, bool always_split_flag = false)
1307{
1308 p = p_;
1309 this->pgg = new detail::pbes_greybox_interface(p, true, true, data::parse_rewrite_strategy(rewrite_strategy));
1310 this->info = new lts_info(p, pgg, reset_flag, always_split_flag);
1311 //std::clog << "explorer" << std::endl;
1312 for (std::size_t i = 0; i < info->get_lts_type().get_number_of_state_types(); i++) {
1313 std::map<data_expression,int> data2int_map;
1314 this->localmaps_data2int.push_back(data2int_map);
1315 std::vector<data_expression> int2data_map;
1316 this->localmaps_int2data.push_back(int2data_map);
1317 }
1318 //std::clog << "-- end of explorer." << std::endl;
1319}
1320
1321
1323{
1324 delete info;
1325 delete pgg;
1326}
1327
1328
1330{
1331 return info;
1332}
1333
1334
1336{
1338 return this->get_state(initial_state);
1339}
1340
1341
1343{
1345 ltsmin_state dummy("dummy");
1346 this->to_state_vector(initial_state, state, dummy, nullptr);
1347}
1348
1349
1351{
1352 //std::clog << "-- get_state --" << std::endl;
1353 //std::clog << " expr = " << expr << std::endl;
1355 assert(is_propositional_variable_instantiation(expr) && expr != novalue);
1356 std::string varname = expr.name();
1357 //std::clog << " varname = " << varname << std::endl;
1358 ltsmin_state s(varname, expr);
1359 return s;
1360}
1361
1362
1364{
1365 return ltsmin_state("true");
1366}
1367
1368
1370{
1371 return ltsmin_state("false");
1372}
1373
1374
1376{
1378 return atermpp::down_cast<data::data_expression>(data::detail::add_index(static_cast<const atermpp::aterm&>(t)));
1379}
1380
1381
1382int explorer::get_index(int type_no, const std::string& s)
1383{
1384 if (type_no==0)
1385 {
1386 return get_string_index(s);
1387 }
1388 else
1389 {
1390 data_expression value = this->string_to_data(s);
1391 return get_value_index(type_no, value);
1392 }
1393}
1394
1395
1396int explorer::get_string_index(const std::string& s)
1397{
1398 std::map<std::string,int>::iterator it = this->localmap_string2int.find(s);
1399 std::size_t index;
1400 if (it != this->localmap_string2int.end()) {
1401 index = it->second;
1402 } else {
1403 this->localmap_int2string.push_back(s);
1404 index = this->localmap_int2string.size() - 1;
1405 //std::clog << "[" << getpid() << "] get_string_index DEBUG push_back " << index << ": " << s << std::endl;
1406 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 return index;
1410}
1411
1412
1413int 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 std::map<data_expression,int>& data2int_map = this->localmaps_data2int.at(type_no);
1419 std::map<data_expression,int>::iterator it = data2int_map.find(value);
1420 std::size_t index;
1421 if (it != data2int_map.end()) {
1422 index = it->second;
1423 } else {
1424 this->localmaps_int2data.at(type_no).push_back(value);
1425 index = this->localmaps_int2data.at(type_no).size() - 1;
1426 data2int_map.insert(std::make_pair(value,index));
1427 }
1428 return index;
1429}
1430
1431
1432void 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 data_expression novalue;
1437 //std::clog << "-- to_state_vector -- " << std::endl;
1438 int state_length = info->get_lts_type().get_state_length();
1439
1440 std::string varname = dst_state.get_variable();
1441 std::string src_varname;
1442 bool same_var = false;
1443 if (!(src==nullptr)) {
1444 src_varname = src_state.get_variable();
1445 same_var = (varname==src_varname);
1446 }
1447 int varindex;
1448 if (same_var) {
1449 varindex = src[0];
1450 } else {
1451 varindex = this->get_string_index(varname);
1452 }
1453 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 std::vector < data_expression > values(state_length);
1459
1460 if (info->get_reset_option() || src == nullptr) {
1461 int type_no;
1462 for (int i = 1; i < state_length; i++) {
1463 data_expression default_value = info->get_default_value(i-1);
1464 values[i] = default_value;
1465 type_no = info->get_lts_type().get_state_type_no(i);
1466 dst[i] = this->get_value_index(type_no, values[i]);
1467 }
1468 } else {
1469 for (int i = 1; i < state_length; i++) {
1470 dst[i] = src[i];
1471 }
1472 }
1473 bool error = false;
1474 const std::vector<data_expression>& parameter_values = dst_state.get_parameter_values();
1475 std::vector<int> parameter_indices =
1477 std::vector<std::string> parameter_signatures =
1479 std::vector<std::string>::iterator param_signature = parameter_signatures.begin();
1480 int value_index = 0;
1481 for(int & parameter_indice : parameter_indices)
1482 {
1483 int i = parameter_indice + 1;
1484 int type_no = info->get_lts_type().get_state_type_no(i);
1485 values[i] = parameter_values[value_index];
1486 if (values[i]==novalue)
1487 {
1488 error = true;
1489 } else {
1490 if (src==nullptr) {
1491 // no source state available; compute index for value.
1492 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 std::map<int,int> src_param_index_positions = detail::map_at(info->get_variable_parameter_index_positions(), src_state.get_variable());
1499 std::map<int,int>::iterator src_param_index_position_it = src_param_index_positions.find(parameter_indice);
1500 if ( src_param_index_position_it != src_param_index_positions.end()
1501 && 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 dst[i] = this->get_value_index(type_no, values[i]);
1509 }
1510 }
1511 }
1512 if (param_signature != parameter_signatures.end())
1513 {
1514 ++param_signature;
1515 }
1516 value_index++;
1517 }
1518 if (error)
1519 {
1520 throw(std::runtime_error("Error in to_state_vector: NoValue in parameters of dst_state: "
1521 + info->state_to_string(dst_state) + "."));
1522 }
1523 //std::clog << "-- to_state_vector: done --" << std::endl;
1524}
1525
1526
1527std::string explorer::get_value(int type_no, int index)
1528{
1529 //std::clog << "get_value type_no = " << type_no << " index = " << index << std::endl;
1530 if (type_no==0)
1531 {
1532 return this->get_string_value(index);
1533 }
1534 else
1535 {
1536 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();
1542 return pp(t);
1543 }
1544}
1545
1546
1547const std::string& explorer::get_string_value(int index)
1548{
1549 if (index >= (int)(localmap_int2string.size()))
1550 {
1551 throw(std::runtime_error("Error in get_string_value: Value not found for index " + std::to_string(index) + "."));
1552 }
1553 return localmap_int2string.at(index);
1554}
1555
1556
1557const data_expression& explorer::get_data_value(int type_no, int index)
1558{
1559 std::vector<data_expression>& int2data_map = this->localmaps_int2data.at(type_no);
1560 if (index >= (int)(int2data_map.size()))
1561 {
1562 throw(std::runtime_error("Error in get_data_value: Value not found for type_no "
1563 + std::to_string(type_no) + " at index " + std::to_string(index) + "."));
1564 }
1565 return int2data_map.at(index);
1566}
1567
1568
1570{
1571 //std::clog << "-- from_state_vector(model, src) --" << std::endl;
1572 data_expression novalue;
1573 int state_length = info->get_lts_type().get_state_length();
1574
1575 std::string varname = this->get_string_value(src[0]);
1576 //std::clog << "from_state_vector: varname = " << varname << std::endl;
1577
1578 bool error = false;
1579
1580 // data_expression values[state_length]; N.B. This is not portable C++
1581 std::vector <data_expression> values(state_length);
1582
1583 int type_no;
1584 for (int i = 1; i < state_length; i++) {
1585 //std::clog << "from_state_vector: values: " << i << " (" << src[i] << "): " << std::endl;
1586 type_no = info->get_lts_type().get_state_type_no(i);
1587 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;
1592 std::vector<int> parameter_indices =
1594 for (int & parameter_indice : parameter_indices) {
1595 if (values[parameter_indice+1]==novalue)
1596 {
1597 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 parameters.push_back(values[parameter_indice+1]);
1601 }
1602 if (error)
1603 {
1604 throw(std::runtime_error("Error in from_state_vector: NoValue in parameters."));
1605 }
1606 data::data_expression_list paramlist(parameters.begin(), parameters.end());
1607 propositional_variable_instantiation state_expression(varname, paramlist);
1608 //std::clog << "from_state_vector: state_expression = " << state_expression.to_string() << std::endl;
1609 ltsmin_state state = this->get_state(state_expression);
1610 //std::clog << "from_state_vector: state = " << state->to_string() << std::endl;
1611 return state;
1612}
1613
1614
1615std::vector<ltsmin_state> explorer::get_successors(const ltsmin_state& state)
1616{
1617 //std::cout << "get_successors: " << state->to_string() << std::endl;
1618 std::vector<ltsmin_state> result;
1619
1620 pbes_expression e = state.to_pbes_expression();
1622 if (state.get_variable()=="true")
1623 {
1624 // Adding true=true
1625 result.push_back(state);
1626 }
1627 else if (state.get_variable()=="false")
1628 {
1629 // Adding false=false
1630 result.push_back(state);
1631 }
1632 else
1633 {
1634 std::set<pbes_expression> successors
1635 = pgg->get_successors(e);
1636 operation_type type = detail::map_at(info->get_variable_types(), state.get_variable());
1637 for (const auto & successor : successors) {
1639 result.push_back(get_state(atermpp::down_cast<propositional_variable_instantiation>(successor)));
1640 } else if (is_true(successor)) {
1642 {
1643 result.push_back(true_state());
1644 }
1645 } else if (is_false(successor)) {
1647 {
1648 result.push_back(false_state());
1649 }
1650 } else {
1651 throw(std::runtime_error("!! Successor is NOT a propvar: " + pbes_system::pp(successor)));
1652 }
1653 }
1654 }
1655 return result;
1656}
1657
1658
1659std::vector<ltsmin_state> explorer::get_successors(const ltsmin_state& state,
1660 int group)
1661{
1662 //std::clog << "get_successors: group=" << group << std::endl;
1663 std::vector<ltsmin_state> result;
1664
1665 if (group == 0 && state.get_variable()=="true")
1666 {
1667 // Adding true=true
1668 result.push_back(state);
1669 }
1670 else if (group == 1 && state.get_variable()=="false")
1671 {
1672 // Adding false=false
1673 result.push_back(state);
1674 }
1675 else
1676 {
1677 std::string varname = state.get_variable();
1678 std::string group_varname = info->get_transition_variable_names()[group];
1679 if (varname==group_varname)
1680 {
1681 pbes_expression e = state.to_pbes_expression();
1682 std::set<pbes_expression> successors
1683 = pgg->get_successors(e, group_varname,
1685 operation_type type = detail::map_at(info->get_variable_types(), state.get_variable());
1686 for (const auto & successor : successors) {
1687 //std::clog << " * successor: " << pp(*expr) << std::endl;
1689 result.push_back(get_state(atermpp::down_cast<propositional_variable_instantiation>(successor)));
1690 } else if (is_true(successor)) {
1692 {
1693 result.push_back(true_state());
1694 }
1695 } else if (is_false(successor)) {
1697 {
1698 result.push_back(false_state());
1699 }
1700 } else {
1701 throw(std::runtime_error("!! Successor is NOT a propvar: " + pbes_system::pp(successor)));
1702 }
1703 }
1704 }
1705 }
1706 return result;
1707}
1708
1709
1710} // namespace pbes_system
1711
1712} // namespace mcrl2
Term containing a string.
Iterator for term_list.
size_type size() const
Returns the size of the term_list.
Definition aterm_list.h:256
const_iterator end() const
Returns a const_iterator pointing to the end of the term_list.
Definition aterm_list.h:282
const Term & front() const
Returns the first element of the list.
Definition aterm_list.h:239
const_iterator begin() const
Returns a const_iterator pointing to the beginning of the term_list.
Definition aterm_list.h:275
Components for generating an arbitrary element of a sort.
\brief A data variable
Definition variable.h:28
std::set< pbes_expression > get_successors(const pbes_expression &phi)
Returns the successors of a state, which is a instantiated propositional variable....
pbes_equation get_pbes_equation(const core::identifier_string &s)
Returns the equation for variable s.
propositional_variable_instantiation get_initial_state()
Returns the initial state, rewritten and simplified.
pbes_expression rewrite_and_simplify_expression(const pbes_expression &e, const bool=true)
Rewrites and simplifies an expression.
static ltsmin_state false_state()
Returns the state representing false.
ltsmin_state get_state(const propositional_variable_instantiation &expr) const
Returns a PBES_State object for expr.
std::vector< std::vector< data_expression > > localmaps_int2data
int get_index(int type_no, const std::string &s)
Returns the index of value in the local store for the data type with number type_no....
std::vector< std::string > localmap_int2string
ltsmin_state get_initial_state() const
Returns the initial state.
static ltsmin_state true_state()
Returns the state representing true.
void to_state_vector(const ltsmin_state &dst_state, int *dst, const ltsmin_state &src_state, int *const &src)
Transforms a PBES state to a state vector, represented by an array of integers.
std::string get_value(int type_no, int index)
Returns the value at position index in the local store for the data type with number type_no....
int get_value_index(int type_no, const data_expression &value)
Returns the index of value in the local store for the data type with number type_no....
explorer(const std::string &filename, const std::string &rewrite_strategy, bool reset_flag, bool always_split_flag)
Constructor.
std::map< std::string, int > localmap_string2int
std::vector< std::map< data_expression, int > > localmaps_data2int
ltsmin_state from_state_vector(int *const &src)
Transforms a state vector src into a PBES_State object object containing the variable and parameter v...
int get_string_index(const std::string &s)
Returns the index of s in the local store for string values. This store is reserved for the string re...
const std::string & get_string_value(int index)
Returns the string at position index in the local store for string values. An exception is thrown if ...
std::vector< ltsmin_state > get_successors(const ltsmin_state &state)
Computes successor states for a state. Serves as a wrapper around the get_successors function of the ...
data::data_expression string_to_data(const std::string &s)
Returns a data expression for the string representation s.
lts_info * get_info() const
Returns the PBES_Info object.
const data_expression & get_data_value(int type_no, int index)
Returns the value at position index in the local store for the data type with number type_no....
detail::pbes_greybox_interface * pgg
the PBES greybox interface
static fixpoint_symbol nu()
Returns the nu symbol.
static fixpoint_symbol mu()
Returns the mu symbol.
bool is_write_dependent_propvar(int group)
Determines if group is write dependent on the propositional variable. Returns true if propositional v...
const std::map< std::string, std::map< int, int > > & get_variable_parameter_index_positions() const
Returns the map from variable names to the map from indices of parameter signatures for the variable ...
std::map< std::string, int > variable_priority
const std::map< int, std::vector< bool > > & get_read_matrix() const
Returns the read dependency matrix.
const std::map< int, std::vector< bool > > & get_write_matrix() const
Returns the write dependency matrix.
static std::vector< std::string > get_param_sequence(const data::variable_list &params)
Converts a variable_sequence_type into a sequence of parameter signatures.
bool is_read_dependent_parameter(int group, int part)
Determines if group is read dependent on part part of the state vector. Returns true if the parameter...
std::vector< int > get_param_indices(const data::variable_list &params)
Converts a variable_sequence_type into a sequence of indices of parameter signatures in the list of p...
std::vector< std::string > transition_variable_name
bool is_pass_through_state(const propositional_variable_instantiation &propvar)
Determines if the propositional variable instantiation is one that only copies parameters from the cu...
const std::map< std::string, fixpoint_symbol > & get_variable_symbols() const
Returns the map from variable names to the fixpoint operator of the equation for the variable.
static std::map< variable, std::string > variable_signatures
std::map< std::string, fixpoint_symbol > variable_symbol
const std::map< std::string, data::variable_list > & get_variable_parameters() const
Returns the map from variable names to the sequence of parameters for the variable.
const std::map< std::string, std::vector< std::string > > & get_variable_parameter_signatures() const
Returns the map from variable names to the list of parameters signatures for the variable.
const std::map< std::string, propositional_variable > & get_variables() const
Returns the map from variable names to the variable object for the variable.
int get_index(const std::string &signature)
Returns the index for a parameter signature in the list of parameter signatures for the system.
const lts_type & get_lts_type() const
Returns the LTS Type.
std::map< std::string, int > param_index
bool get_reset_option() const
Returns if the reset option is set.
std::map< std::string, std::vector< std::string > > variable_parameter_signatures
const std::vector< pbes_expression > & get_transition_expressions() const
Returns the map from transition group number to the expression of the transition group.
std::set< std::string > copied(const pbes_expression &expr)
Computes the free variables which are copied/passed through (to a recursive variable) in an expressio...
std::map< int, std::vector< bool > > read_matrix
std::vector< data_expression > param_default_values
detail::pbes_greybox_interface * pgg
bool is_read_dependent_propvar(int group)
Determines if group is read dependent on the propositional variable. Returns true,...
std::vector< pbes_expression > transition_expression
const std::map< int, std::vector< bool > > & get_dependency_matrix() const
Returns the dependency matrix.
const std::vector< operation_type > & get_transition_types() const
Returns the map from transition group number to the type of the right hand side of the equation to wh...
std::set< std::string > used(const pbes_expression &expr)
Computes the free variables actually used, not only passed through, in an expression.
std::map< std::string, std::map< int, int > > variable_parameter_index_positions
static std::string get_param_signature(const variable &param)
Returns a signature for parameter param.
const std::map< std::string, operation_type > & get_variable_types() const
Returns the map from variable names to the type of the right hand side of the equation for the variab...
void compute_dependency_matrix()
Computes dependency matrix from PBES.
lts_info(pbes &p, detail::pbes_greybox_interface *pgg, bool reset, bool always_split)
Constructor.
static bool tf(const pbes_expression &phi)
Determines if the term phi contains a branch that directly results in true or false (not a variable).
std::vector< pbes_expression > split_expression_and_substitute_variables(const pbes_expression &e, int current_priority, operation_type current_type, std::set< std::string > vars_stack)
Splits the expression into parts (disjuncts or conjuncts) and recursively tries to substitute the pro...
std::map< std::string, propositional_variable > variables
int get_number_of_groups() const
Returns the number of transition groups.
static std::set< std::string > get_param_set(const data::variable_list &params)
Converts a variable_sequence_type into a set of parameter signatures.
std::map< int, int > get_param_index_positions(const data::variable_list &params)
Converts a variable_sequence_type into a map from indices of parameter signatures (in the list of par...
static std::set< std::string > occ(const pbes_expression &expr)
Computes the propositional variables used in an expression.
std::map< std::string, operation_type > variable_type
int count_variables(const pbes_expression &e)
Counts the number of propositional variables in an expression.
void compute_lts_type()
Computes LTS Type from PBES.
std::vector< operation_type > transition_type
std::string state_to_string(const ltsmin_state &state)
Returns a string representation for state state.
const std::map< std::string, int > & get_variable_priorities() const
Returns the map from variable names to the priority of the equation for the variable.
std::map< std::string, data::variable_list > variable_parameters
const data_expression & get_default_value(int index)
Returns a default value for the sort of a parameter signature.
const std::vector< std::string > & get_transition_variable_names() const
Returns the map from transition group number to the variable name of the equation to which the transi...
std::map< int, std::vector< bool > > matrix
std::set< std::string > reset(const pbes_expression &phi, const std::set< std::string > &d)
Computes the set of parameters reset in the expression.
static std::set< std::string > free(const pbes_expression &expr)
Computes the free variables read in an expression.
std::vector< pbes_expression > transition_expression_plain
std::map< int, std::vector< bool > > write_matrix
bool is_write_dependent_parameter(int group, int part)
Determines if group is read dependent on part part of the state vector. Returns true if the parameter...
std::map< std::string, pbes_expression > variable_expression
std::set< std::string > changed(const pbes_expression &phi)
Computes the set of parameters changed in the expression.
std::map< std::string, std::vector< int > > variable_parameter_indices
void compute_transition_groups()
Computes transition groups from PBES.
const std::map< std::string, std::vector< int > > & get_variable_parameter_indices() const
Returns the map from variable names to the list of indices of the parameters signatures for the varia...
const std::vector< std::string > & get_edge_label_types() const
Returns the sequence of edge label types.
std::size_t get_number_of_state_types() const
Returns the number of state types.
const std::vector< std::string > & get_edge_labels() const
Returns the sequence of edge labels.
int get_state_type_no(int part) const
Returns the state type index for the state part part.
std::vector< std::string > state_type_list
std::vector< std::string > state_label_types
std::vector< std::string > state_names
std::vector< int > state_type_no
void add_state(const std::string &name, const std::string &type)
Adds a state part of type type with name name.
void add_state_label(const std::string &name, const std::string &type)
Adds a state label of type type with name name.
lts_type(int state_length)
Contructor.
std::string get_state_type_name(int type_no) const
Returns the name of the state type with number type_no.
int get_state_length() const
Returns the state length.
std::map< std::string, int > state_type_index
std::vector< std::string > edge_label_names
const std::vector< std::string > & get_state_label_types() const
Returns the sequence of state label types.
std::vector< std::string > edge_label_types
std::vector< std::string > state_types
std::size_t get_number_of_edge_labels() const
Returns the number of edge labels.
std::vector< std::string > state_label_names
const std::vector< std::string > & get_state_types() const
Returns the sequence of state part types.
void add_edge_label(const std::string &name, const std::string &type)
Adds an edge label of type type with name name.
const std::vector< std::string > & get_state_labels() const
Returns the sequence of state labels.
const std::vector< std::string > & get_state_names() const
Returns the sequence of state part names.
std::size_t get_number_of_state_labels() const
Returns the number of state labels.
void add_parameter_value(const data_expression &)
Adds a parameter value to the list of parameter values.
pbes_expression to_pbes_expression() const
Returns a PBES expression representing the state.
std::vector< data_expression > param_values
std::string state_to_string() const
Returns the player or type of the state (And/Or, Abelard/Eloise, Odd/Even).
bool operator<(const ltsmin_state &other) const
Compares two PBES_State objects. Uses lexicographical ordering on priority, type, variable and parame...
bool operator==(const ltsmin_state &other) const
Checks if two PBES_State objects are equal.
ltsmin_state(const std::string &varname, const pbes_expression &e)
Constructor.
std::string get_variable() const
Returns the priority for the state, which depends on the fixpoint operator of the equation of the pro...
const std::vector< data_expression > & get_parameter_values() const
Returns the list of parameter values.
virtual operation_type get_expression_operation(const pbes_expression &phi)
Returns the vertex type.
operation_type
The operation type of the vertices.
parameterized boolean equation system
Definition pbes.h:58
const data::data_specification & data() const
Returns the data specification.
Definition pbes.h:150
const propositional_variable_instantiation & initial_state() const
Returns the initial state.
Definition pbes.h:192
const std::vector< pbes_equation > & equations() const
Returns the equations.
Definition pbes.h:164
\brief A propositional variable instantiation
\brief A propositional variable declaration
const data::variable_list & parameters() const
const core::identifier_string & name() const
Standard exception class for reporting runtime errors.
Definition exception.h:27
add your file description here.
MCRL2_EXPORT bool init(rewriter_interface *i, RewriterCompilingJitty *this_rewriter)
@ error
Definition linearise.cpp:68
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:391
aterm read_term_from_string(const std::string &s)
Reads an aterm from a string. The string can be in either binary or text format.
bool check_term_PropVarInst(const Term &t)
std::string pp(const identifier_string &x)
Definition core.cpp:26
atermpp::aterm_string identifier_string
String type of the LPS library. Identifier strings are represented internally as ATerms.
atermpp::aterm add_index(const atermpp::aterm &x)
Definition io.h:55
atermpp::aterm remove_index(const atermpp::aterm &x)
Definition io.h:61
std::vector< data_expression > data_expression_vector
\brief vector of data_expressions
std::string pp(const abstraction &x)
Definition data.cpp:39
atermpp::term_list< variable > variable_list
\brief list of variables
rewrite_strategy parse_rewrite_strategy(const std::string &s)
standard conversion from string to rewrite strategy
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
@ verbose
Definition logger.h:37
const pbes_expression & arg(const pbes_expression &t)
Returns the pbes expression argument of expressions of type not, exists and forall.
const pbes_expression & left(const pbes_expression &t)
Returns the left hand side of an expression of type and, or or imp.
const pbes_expression & right(const pbes_expression &t)
Returns the right hand side of an expression of type and, or or imp.
void normalize(pbes &x)
The function normalize brings (embedded) pbes expressions into positive normal form,...
pbes to_ppg(pbes x)
Rewrites a PBES to a PPG.
bool is_ppg(const T &x)
Determines if an expression is a PPG expression.
MapContainer::mapped_type map_at(const MapContainer &m, typename MapContainer::key_type key)
bool is_data(const pbes_expression &t)
Returns true if the term t is a data expression.
const pbes_expression & true_()
bool is_not(const atermpp::aterm &x)
void load_pbes(pbes &pbes, std::istream &stream, utilities::file_format format, const std::string &source="")
Load a PBES from file.
Definition io.cpp:82
bool is_exists(const atermpp::aterm &x)
void find_free_variables(const T &x, OutputIterator o)
Definition find.h:87
bool is_or(const atermpp::aterm &x)
const data::variable_list & quantifier_variables(const pbes_expression &x)
bool is_forall(const atermpp::aterm &x)
bool is_false(const pbes_expression &t)
Test for the value false.
std::vector< pbes_expression > split_disjuncts(const pbes_expression &expr, bool split_simple_expr=false)
Splits a disjunction into a sequence of operands. Given a pbes expression of the form p1 || p2 || ....
pbes_expression formula(std::set< identifier_t > const &v, const owner_t owner, const std::string &prefix="X")
Definition pg_parse.h:54
std::vector< pbes_expression > split_conjuncts(const pbes_expression &expr, bool split_simple_expr=false)
Splits a conjunction into a sequence of operands Given a pbes expression of the form p1 && p2 && ....
bool is_propositional_variable_instantiation(const atermpp::aterm &x)
std::string pp(const fixpoint_symbol &x)
Definition pbes.cpp:37
bool is_and(const atermpp::aterm &x)
bool is_imp(const atermpp::aterm &x)
bool is_simple_expression(const T &x)
Determines if an expression is a simple expression. An expression is simple if it is free of proposit...
bool is_true(const pbes_expression &t)
Test for the value true.
const pbes_expression & false_()
T && return_std_move(T &t)
This is a workaround for the return by value diagnostic (clang -Wreturn-std-move)....
Definition workarounds.h:24
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
IO routines for boolean equation systems.
Visitor class for Parameterised Parity Games (PPG), PBES expressions of the form: PPG :== /_{i: I} f_...
Component for generating representatives of sorts.