LCOV - code coverage report
Current view: top level - pbes/source - pbes_explorer.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 688 853 80.7 %
Date: 2020-02-28 00:44:21 Functions: 78 99 78.8 %
Legend: Lines: hit not hit

          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       19364 :     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             :     p(p),
     166             :     pgg(pgg),
     167             :     reset_option(reset),
     168             :     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          12 :     std::vector<std::string> params;
     187          12 :     std::map<std::string,std::string> paramtypes;
     188          12 :     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          28 :         propositional_variable var = eqn.variable();
     196          48 :         for (const variable& varparam: var.parameters())
     197             :         {
     198          68 :             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          28 :                 data_expression e(default_expression_generator(varparam.sort()));
     208          28 :                 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             :             }
     211             :         }
     212             :         //params.sort();
     213             :     }
     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          16 :     std::string varname = std::string(propvar.name());
     236          16 :     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          48 :                 data::variable param(*param_it);
     254          48 :                 data::variable param_expr(value);
     255          24 :                 if (param != param_expr)
     256             :                 {
     257           0 :                     return false;
     258             :                 }
     259             :             }
     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             : }
     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          56 :     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          16 :         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          16 :             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          16 :                 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          16 :                 pbes_expression expr = this->variable_expression[varname];
     348             : 
     349           8 :                 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             :                 }
     366             :                 else
     367             :                 {
     368           8 :                     result.push_back(part);
     369             :                 }
     370             :             }
     371             :             else
     372             :             {
     373           0 :                 pass_through = false;
     374             :             }
     375             :         }
     376             :         else
     377             :         {
     378           0 :             pass_through = false;
     379             :         }
     380             :     }
     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             : }
     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          12 :     fixpoint_symbol symbol = fixpoint_symbol::nu();
     409          12 :     detail::ppg_visitor checker;
     410             : 
     411          12 :     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          28 :         pbes_expression expr = pgg->get_pbes_equation(eqn.variable().name()).formula();
     451          28 :         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             :     }
     468             : 
     469             :     // Skip 'unused' equations....
     470          12 :     std::set<std::string> variable_set;
     471             :     {
     472          12 :         propositional_variable_instantiation init = p.initial_state();
     473          12 :         std::queue<std::string> variable_queue;
     474           6 :         variable_queue.push(init.name());
     475           6 :         variable_set.insert(init.name());
     476          34 :         while (!variable_queue.empty())
     477             :         {
     478          28 :             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          28 :             pbes_expression expr = this->variable_expression[var];
     483          28 :             std::set<std::string> vars_stack;
     484          28 :             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          14 :                     expression_parts.begin(); e != expression_parts.end(); ++e) {
     487          28 :                  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             :             }
     498             :         }
     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             :     }
     506             : 
     507          20 :     for (auto & eqn : p.equations()) {
     508          28 :         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          28 :             pbes_expression expr = this->variable_expression[variable_name];
     514          28 :             std::set<std::string> vars_stack;
     515          14 :             mCRL2log(log::debug) << std::endl << "Generating groups for equation " << variable_name << std::endl;
     516          28 :             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          14 :                     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          28 :                         << pbes_system::pp(*e) << std::endl;
     526          14 :                 group++;
     527             :             }
     528             :         }
     529             :     }
     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          52 :         std::vector<bool> dep_row;
     542          52 :         std::vector<bool> read_row;
     543          52 :         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             :     }
     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          76 :     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          76 :     pbes_expression phi = transition_expression_plain[group];
     692          76 :     std::string X = transition_variable_name[group];
     693          76 :     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          68 :         std::set<std::string> usedSet = used(phi);
     701          68 :         std::set<std::string> changedSet = changed(phi);
     702          68 :         std::set<std::string> copySet = copied(phi);
     703          68 :         std::set<std::string> changedAndCopied;
     704          34 :         std::set_intersection(changedSet.begin(), changedSet.end(), copySet.begin(), copySet.end(),
     705          34 :             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             :     }
     717             : 
     718             : }
     719             : 
     720             : 
     721          26 : bool lts_info::is_write_dependent_propvar(int group)
     722             : {
     723          26 :     if (group==0 || group==1) return false;
     724          28 :     pbes_expression phi = transition_expression_plain[group];
     725          28 :     std::string X = transition_variable_name[group];
     726          14 :     if (lts_info::tf(phi))
     727             :     {
     728          10 :         return true;
     729             :     }
     730           8 :     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             : }
     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          76 :     std::string p = type.get_state_names().at(part);
     751          76 :     pbes_expression phi = transition_expression_plain[group];
     752          76 :     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             :     }
     766          76 :     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             : }
     770             : 
     771             : 
     772          72 : std::set<std::string> lts_info::changed(const pbes_expression& phi)
     773             : {
     774         144 :     std::set<std::string> empty;
     775         144 :     return changed(phi, empty);
     776             : }
     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         792 :         std::set<std::string> l = changed(pbes_system::accessors::left(phi), L);
     789         396 :         result.insert(l.begin(), l.end());
     790         792 :         std::set<std::string> r = changed(pbes_system::accessors::right(phi), L);
     791         396 :         result.insert(r.begin(), r.end());
     792             :     }
     793         556 :     else if (is_forall(phi) || is_exists(phi))
     794             :     {
     795         176 :         std::set<std::string> LL;
     796          88 :         LL.insert(L.begin(), L.end());
     797         176 :         data::variable_list vars = quantifier_variables(phi);
     798         176 :         for (auto variable : vars)
     799             :         {
     800          88 :             LL.insert(get_param_signature(variable));
     801             :         }
     802          88 :         result = changed(pbes_system::accessors::arg(phi), LL);
     803             :     }
     804         468 :     else if (is_propositional_variable_instantiation(phi))
     805             :     {
     806             :         std::vector<std::string> var_param_signatures =
     807         416 :                     variable_parameter_signatures[atermpp::down_cast<propositional_variable_instantiation>(phi).name()];
     808         416 :         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         548 :         for (std::vector<std::string>::const_iterator param =
     812         208 :                 var_param_signatures.begin(); param != var_param_signatures.end(); ++param) {
     813        1096 :             std::string param_signature = *param;
     814         548 :             if (data::is_variable(*val))
     815             :             {
     816         320 :                 const variable& value = atermpp::down_cast<variable>(*val);
     817         640 :                 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             :             }
     823             :             else
     824             :             {
     825         228 :                 result.insert(param_signature);
     826             :             }
     827         548 :             if (val != values.end()) {
     828         548 :                 ++val;
     829             :             }
     830             :         }
     831             :     }
     832         952 :     return result;
     833             : }
     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             :     }
     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             :         }
     864           0 :         for (auto signature : d) {
     865           0 :             if (params.find(signature) == params.end())
     866             :             {
     867           0 :                 result.insert(signature);
     868             :             }
     869             :         }
     870             :     }
     871           0 :     return result;
     872             : }
     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         156 :         std::set<std::string> l = occ(pbes_system::accessors::left(expr));
     907          78 :         result.insert(l.begin(), l.end());
     908         156 :         std::set<std::string> r = occ(pbes_system::accessors::right(expr));
     909          78 :         result.insert(r.begin(), r.end());
     910             :     }
     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             : }
     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             :     }
     926         224 :     return result;
     927             : }
     928             : 
     929             : 
     930          34 : std::set<std::string> lts_info::used(const pbes_expression& expr)
     931             : {
     932          68 :     std::set<std::string> emptySet;
     933          68 :     return used(expr, emptySet);
     934             : }
     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         448 :         std::set<std::string> fv = free(expr);
     944         224 :         result.insert(fv.begin(), fv.end());
     945             :     }
     946         540 :     if (is_propositional_variable_instantiation(expr))
     947             :     {
     948             :         data::variable_list var_params =
     949         192 :                     variable_parameters[atermpp::down_cast<propositional_variable_instantiation>(expr).name()];
     950         192 :         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         512 :             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         304 :                 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             :             }
     964             :             else
     965             :             {
     966             :                 // add free variables in data expression
     967         208 :                 std::set<std::string> l = used(*val, L);
     968         104 :                 result.insert(l.begin(), l.end());
     969             :             }
     970         256 :             if (val != values.end()) {
     971         256 :                 ++val;
     972             :             }
     973             :         }
     974             :     }
     975         444 :     else if (is_and(expr) || is_or(expr) || is_imp(expr))
     976             :     {
     977         364 :         std::set<std::string> l = used(pbes_system::accessors::left(expr), L);
     978         182 :         result.insert(l.begin(), l.end());
     979         364 :         std::set<std::string> r = used(pbes_system::accessors::right(expr), L);
     980         182 :         result.insert(r.begin(), r.end());
     981             :     }
     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          76 :         std::set<std::string> LL;
     989          38 :         LL.insert(L.begin(), L.end());
     990          76 :         data::variable_list vars = quantifier_variables(expr);
     991          76 :         for (auto variable : vars)
     992             :         {
     993          38 :             LL.insert(get_param_signature(variable));
     994             :         }
     995          38 :         result = used(pbes_system::accessors::arg(expr), LL);
     996             :     }
     997         540 :     return result;
     998             : }
     999             : 
    1000             : 
    1001          34 : std::set<std::string> lts_info::copied(const pbes_expression& expr)
    1002             : {
    1003          68 :     std::set<std::string> emptySet;
    1004          68 :     return copied(expr, emptySet);
    1005             : }
    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         192 :                     variable_parameters[atermpp::down_cast<propositional_variable_instantiation>(expr).name()];
    1020         192 :         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         512 :             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         304 :                 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             :             }
    1034         256 :             if (val != values.end()) {
    1035         256 :                 ++val;
    1036             :             }
    1037             :         }
    1038             :     }
    1039         340 :     else if (is_and(expr) || is_or(expr) || is_imp(expr))
    1040             :     {
    1041         364 :         std::set<std::string> l = copied(pbes_system::accessors::left(expr), L);
    1042         182 :         result.insert(l.begin(), l.end());
    1043         364 :         std::set<std::string> r = copied(pbes_system::accessors::right(expr), L);
    1044         182 :         result.insert(r.begin(), r.end());
    1045             :     }
    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          76 :         std::set<std::string> LL;
    1053          38 :         LL.insert(L.begin(), L.end());
    1054          76 :         data::variable_list vars = quantifier_variables(expr);
    1055          76 :         for (auto variable : vars)
    1056             :         {
    1057          38 :             LL.insert(get_param_signature(variable));
    1058             :         }
    1059          38 :         result = copied(pbes_system::accessors::arg(expr), LL);
    1060             :     }
    1061         436 :     return result;
    1062             : }
    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             : }
    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             :     }
    1102          38 :     return result;
    1103             : }
    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             :     }
    1112          26 :     return result;
    1113             : }
    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             :     }
    1123          26 :     return result;
    1124             : }
    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          68 :         result.insert(std::make_pair(index,i));
    1134          34 :         i++;
    1135             :     }
    1136          26 :     return result;
    1137             : }
    1138             : 
    1139             : 
    1140          42 : 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          14 :         std::string paramname = param.name();
    1149          14 :         std::string paramtype = core::pp(param.sort());
    1150          14 :         std::string signature = get_param_signature(paramname, paramtype);
    1151           7 :         variable_signatures[param] = signature;
    1152           7 :         return signature;
    1153             :     }
    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           7 :     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       10196 :     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             :                 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        3464 :     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        3464 :     data::data_expression_list parameter_values_list(parameter_values.begin(), parameter_values.end());
    1249             :     // Create propositional variable instantiation.
    1250             :     propositional_variable_instantiation expr =
    1251        3464 :             propositional_variable_instantiation(core::identifier_string(var), parameter_values_list);
    1252        3464 :     return workaround::return_std_move(expr);
    1253             : }
    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             : }
    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             :     }
    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           8 :         std::map<data_expression,int> data2int_map;
    1298           4 :         this->localmaps_data2int.push_back(data2int_map);
    1299           8 :         std::vector<data_expression> int2data_map;
    1300           4 :         this->localmaps_int2data.push_back(int2data_map);
    1301             :     }
    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          16 :         std::map<data_expression,int> data2int_map;
    1314           8 :         this->localmaps_data2int.push_back(data2int_map);
    1315          16 :         std::vector<data_expression> int2data_map;
    1316           8 :         this->localmaps_int2data.push_back(int2data_map);
    1317             :     }
    1318             :     //std::clog << "-- end of explorer." << std::endl;
    1319           4 : }
    1320             : 
    1321             : 
    1322          12 : 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          12 :     propositional_variable_instantiation initial_state = pgg->get_initial_state();
    1338          12 :     return this->get_state(initial_state);
    1339             : }
    1340             : 
    1341             : 
    1342           6 : void explorer::initial_state(int* state)
    1343             : {
    1344          12 :     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       10196 :     propositional_variable_instantiation novalue;
    1355        5098 :     assert(is_propositional_variable_instantiation(expr) && expr != novalue);
    1356       10196 :     std::string varname = expr.name();
    1357             :     //std::clog << "  varname = " << varname << std::endl;
    1358        5098 :     ltsmin_state s(varname, expr);
    1359       10196 :     return s;
    1360             : }
    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       19996 :   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             : }
    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       19996 :         data_expression value = this->string_to_data(s);
    1391        9998 :         return get_value_index(type_no, value);
    1392             :     }
    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        6732 :     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        6732 :     std::string varname = dst_state.get_variable();
    1441        6732 :     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        6732 :     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          28 :             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             :         }
    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        6732 :                         detail::map_at(info->get_variable_parameter_indices(), varname);
    1477             :     std::vector<std::string> parameter_signatures =
    1478        6732 :                     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       18336 :                 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       18336 :                 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             :             }
    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             :         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       19996 :         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       19996 :         atermpp::aterm t = data::detail::remove_index(value);
    1542        9998 :         return pp(t);
    1543             :     }
    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             :         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        3464 :     data_expression novalue;
    1573        1732 :     int state_length = info->get_lts_type().get_state_length();
    1574             : 
    1575        3464 :     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        3464 :     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        3464 :     data::data_expression_vector parameters;
    1592             :     std::vector<int> parameter_indices =
    1593        3464 :             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        3464 :     data::data_expression_list paramlist(parameters.begin(), parameters.end());
    1607        3464 :     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             : }
    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        1732 :     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        1732 :                 = 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             :     }
    1655        1732 :     return result;
    1656             : }
    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        1732 :         std::string varname = state.get_variable();
    1678        1732 :         std::string group_varname = info->get_transition_variable_names()[group];
    1679         866 :         if (varname==group_varname)
    1680             :         {
    1681        1732 :             pbes_expression e = state.to_pbes_expression();
    1682             :             std::set<pbes_expression> successors
    1683         866 :                     = pgg->get_successors(e, group_varname,
    1684        1732 :                                              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             :         }
    1705             :     }
    1706         866 :     return result;
    1707             : }
    1708             : 
    1709             : 
    1710             : } // namespace pbes_system
    1711             : 
    1712         126 : } // namespace mcrl2

Generated by: LCOV version 1.13