LCOV - code coverage report
Current view: top level - lps/source - next_state_generator.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 270 291 92.8 %
Date: 2020-09-16 00:45:56 Functions: 21 22 95.5 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Ruud Koolen
       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 next_state_generator.cpp
      10             : 
      11             : #include "mcrl2/lps/next_state_generator.h"
      12             : 
      13             : using namespace mcrl2;
      14             : using namespace mcrl2::data;
      15             : using namespace mcrl2::lps;
      16             : using namespace mcrl2::lps::detail;
      17             : 
      18             : // First we provide two classes, that represent lambdas.
      19             : class rewriter_class
      20             : {
      21             :   protected:
      22             :     const rewriter& m_r;
      23             :     mutable_indexed_substitution<>& m_sigma;
      24             : 
      25             :   public:
      26        3669 :     rewriter_class(const rewriter& r, mutable_indexed_substitution<>& sigma)
      27        3669 :       :  m_r(r),
      28        3669 :          m_sigma(sigma)
      29        3669 :     {}
      30             : 
      31       22835 :     const data_expression operator()(const data_expression& t) const
      32             :     {
      33       22835 :       return m_r(t,m_sigma);
      34             :     }
      35             : }; 
      36             : 
      37             : class state_applier
      38             : {
      39             :   protected:
      40             :     const state& m_state;
      41             :     const std::size_t m_size;
      42             : 
      43             :   public:
      44        2305 :     state_applier(const state& state, const std::size_t size)
      45        2305 :       :  m_state(state),
      46        2305 :          m_size(size)
      47        2305 :     {}
      48             : 
      49        4609 :     const data_expression& operator()(const std::size_t n) const
      50             :     {
      51        4609 :       return m_state.element_at(n,m_size);
      52             :     }
      53             : };
      54             : 
      55         223 : next_state_generator::next_state_generator(
      56             :   const stochastic_specification& spec,
      57             :   const data::rewriter& rewriter,
      58             :   const substitution_t& base_substitution,
      59             :   bool use_enumeration_caching,
      60         223 :   bool use_summand_pruning)
      61             :   : m_specification(spec),
      62             :     m_rewriter(rewriter),
      63             :     m_substitution(base_substitution),
      64             :     m_base_substitution(base_substitution),
      65         223 :     m_enumerator(m_rewriter, m_specification.data(), m_rewriter, m_id_generator, (std::numeric_limits<std::size_t>::max)(),true),  // Generate exceptions.
      66         446 :     m_use_enumeration_caching(use_enumeration_caching)
      67             : {
      68         223 :   m_process_parameters = data::variable_vector(m_specification.process().process_parameters().begin(), m_specification.process().process_parameters().end());
      69             : 
      70         223 :   if (m_specification.process().has_time())
      71             :   {
      72           6 :     mCRL2log(log::warning) << "Specification uses time, which is (currently) only partly supported." << std::endl;
      73             :   }
      74             : 
      75         811 :   for (stochastic_action_summand_vector::iterator i = m_specification.process().action_summands().begin();
      76         811 :                  i != m_specification.process().action_summands().end(); i++)
      77             :   {
      78        1176 :     summand_t summand;
      79         588 :     summand.summand = &(*i);
      80         588 :     summand.variables =  order_variables_to_optimise_enumeration(i->summation_variables(),spec.data());
      81         588 :     summand.condition = i->condition();
      82        1176 :     const data_expression_list& l=i->next_state(m_specification.process().process_parameters());
      83         588 :     summand.distribution = i->distribution();
      84         588 :     summand.result_state = data_expression_vector(l.begin(),l.end());
      85         588 :     if (i->multi_action().has_time())
      86             :     {
      87           6 :       summand.time_tag=i->multi_action().time();
      88             :     }
      89             : 
      90        1140 :     for (process::action_list::const_iterator j = i->multi_action().actions().begin(); j != i->multi_action().actions().end(); j++)
      91             :     {
      92        1104 :       action_internal_t action_label;
      93         552 :       action_label.label = j->label();
      94             : 
      95        1000 :       for (data_expression_list::iterator k = j->arguments().begin(); k != j->arguments().end(); k++)
      96             :       {
      97         448 :         action_label.arguments.push_back(*k);
      98             :       }
      99             : 
     100         552 :       summand.action_label.push_back(action_label);
     101             :     }
     102             : 
     103        4070 :     for (std::size_t j = 0; j < m_process_parameters.size(); j++)
     104             :     {
     105        3482 :       if (data::search_free_variable(i->condition(), m_process_parameters[j]))
     106             :       {
     107         902 :         summand.condition_parameters.push_back(j);
     108             :       }
     109             :     }
     110         588 :     summand.condition_arguments_function = atermpp::function_symbol("condition_arguments", summand.condition_parameters.size());
     111        1176 :     std::vector<atermpp::aterm_int> dummy(summand.condition_arguments_function.arity(), atermpp::aterm_int(static_cast<std::size_t>(0)));
     112         588 :     summand.condition_arguments_function_dummy = atermpp::aterm_appl(summand.condition_arguments_function, dummy.begin(), dummy.end());
     113             : 
     114         588 :     m_summands.push_back(summand);
     115             :   }
     116             : 
     117         446 :   data::data_expression_list initial_state_raw = m_specification.initial_process().expressions();
     118             : 
     119         446 :   mutable_indexed_substitution<> sigma;
     120         446 :   data::data_expression_vector initial_symbolic_state(initial_state_raw.begin(),initial_state_raw.end());
     121         446 :   m_initial_states = calculate_distribution(m_specification.initial_process().distribution(),
     122             :                                             initial_symbolic_state,
     123         223 :                                             sigma);
     124             : 
     125         223 :   m_all_summands = summand_subset_t(this, use_summand_pruning);
     126         223 : }
     127             : 
     128         223 : next_state_generator::~next_state_generator()
     129         223 : {}
     130             : 
     131         223 : next_state_generator::summand_subset_t::summand_subset_t(next_state_generator *generator, bool use_summand_pruning)
     132             :   : m_generator(generator),
     133         223 :     m_use_summand_pruning(use_summand_pruning)
     134             : {
     135         223 :   if (m_use_summand_pruning)
     136             :   {
     137          12 :     m_pruning_tree.summand_subset = atermpp::detail::shared_subset<summand_t>(generator->m_summands);
     138          12 :     build_pruning_parameters(generator->m_specification.process().action_summands());
     139             :   }
     140             :   else
     141             :   {
     142         751 :     for (std::size_t i = 0; i < generator->m_summands.size(); i++)
     143             :     {
     144         540 :       m_summands.push_back(i);
     145             :     }
     146             :   }
     147         223 : }
     148             : 
     149           0 : bool next_state_generator::summand_subset_t::summand_set_contains(
     150             :             const std::set<stochastic_action_summand>& summand_set,
     151             :             const next_state_generator::summand_t& summand)
     152             : {
     153           0 :   return summand_set.count(*summand.summand) > 0;
     154             : }
     155             : 
     156          24 : next_state_generator::summand_subset_t::summand_subset_t(
     157             :                 next_state_generator *generator,
     158             :                 const stochastic_action_summand_vector& summands,
     159          24 :                 bool use_summand_pruning)
     160             :   : m_generator(generator),
     161          24 :     m_use_summand_pruning(use_summand_pruning)
     162             : {
     163          48 :   std::set<stochastic_action_summand> summand_set;
     164          96 :   for (const stochastic_action_summand& i: summands)
     165             :   {
     166          72 :     summand_set.insert(i);
     167             :   }
     168             : 
     169          24 :   if (m_use_summand_pruning)
     170             :   {
     171           0 :     atermpp::detail::shared_subset<summand_t> full_set(generator->m_summands);
     172           0 :     m_pruning_tree.summand_subset =  atermpp::detail::shared_subset<summand_t>(full_set, std::bind(next_state_generator::summand_subset_t::summand_set_contains, summand_set, std::placeholders::_1));
     173           0 :     build_pruning_parameters(summands);
     174             :   }
     175             :   else
     176             :   {
     177         168 :     for (std::size_t i = 0; i < generator->m_summands.size(); i++)
     178             :     {
     179         144 :       if (summand_set.count(*generator->m_summands[i].summand) > 0)
     180             :       {
     181          72 :         m_summands.push_back(i);
     182             :       }
     183             :     }
     184             :   }
     185          24 : }
     186             : 
     187        1160 : static float condition_selectivity(const data_expression& e, const variable& v)
     188             : {
     189        1160 :   if (sort_bool::is_and_application(e))
     190             :   {
     191         356 :     return condition_selectivity(data::binary_left(atermpp::down_cast<data::application>(e)), v)
     192         356 :         +  condition_selectivity(data::binary_right(atermpp::down_cast<data::application>(e)), v);
     193             :   }
     194         804 :   else if (sort_bool::is_or_application(e))
     195             :   {
     196           0 :     float sum = 0;
     197           0 :     std::size_t count = 0;
     198           0 :     std::list<data_expression> terms;
     199           0 :     terms.push_back(e);
     200           0 :     while (!terms.empty())
     201             :     {
     202           0 :       data_expression expression = terms.front();
     203           0 :       terms.pop_front();
     204           0 :       if (sort_bool::is_or_application(expression))
     205             :       {
     206           0 :         terms.push_back(data::binary_left(atermpp::down_cast<data::application>(e)));
     207           0 :         terms.push_back(data::binary_right(atermpp::down_cast<data::application>(e)));
     208             :       }
     209             :       else
     210             :       {
     211           0 :         sum += condition_selectivity(expression, v);
     212           0 :         count++;
     213             :       }
     214             :     }
     215           0 :     return sum / count;
     216             :   }
     217         804 :   else if (is_equal_to_application(e))
     218             :   {
     219         756 :     const data_expression& left = data::binary_left(atermpp::down_cast<data::application>(e));
     220         756 :     const data_expression& right = data::binary_right(atermpp::down_cast<data::application>(e));
     221             : 
     222         756 :     if (is_variable(left) && variable(left) == v)
     223             :     {
     224          68 :       return 1;
     225             :     }
     226         688 :     else if(is_variable(right) && variable(right) == v)
     227             :     {
     228           8 :       return 1;
     229             :     }
     230             :     else
     231             :     {
     232         680 :       return 0;
     233             :     }
     234             :   }
     235             :   else
     236             :   {
     237          48 :     return 0;
     238             :   }
     239             : }
     240             : 
     241             : struct parameter_score
     242             : {
     243             :   std::size_t parameter_id;
     244             :   float score;
     245             : 
     246             :   parameter_score() {}
     247             : 
     248          52 :   parameter_score(std::size_t id, float score_)
     249          52 :     : parameter_id(id), score(score_)
     250          52 :   {}
     251             : };
     252             : 
     253         148 : static bool parameter_score_compare(const parameter_score& left, const parameter_score& right)
     254             : {
     255         148 :   return left.score > right.score;
     256             : }
     257             : 
     258          12 : void next_state_generator::summand_subset_t::build_pruning_parameters(const stochastic_action_summand_vector& summands)
     259             : {
     260          24 :   std::vector < parameter_score> parameters;
     261             : 
     262          64 :   for (std::size_t i = 0; i < m_generator->m_process_parameters.size(); i++)
     263             :   {
     264          52 :     parameters.push_back(parameter_score(i, 0));
     265         500 :     for (stochastic_action_summand_vector::const_iterator j = summands.begin(); j != summands.end(); j++)
     266             :     {
     267         448 :       parameters[i].score += condition_selectivity(j->condition(), m_generator->m_process_parameters[i]);
     268             :     }
     269             :   }
     270             : 
     271          12 :   std::sort(parameters.begin(), parameters.end(), parameter_score_compare);
     272             : 
     273          64 :   for (std::size_t i = 0; i < m_generator->m_process_parameters.size(); i++)
     274             :   {
     275          52 :     if (parameters[i].score > 0)
     276             :     {
     277          32 :       m_pruning_parameters.push_back(parameters[i].parameter_id);
     278          32 :       mCRL2log(log::verbose) << "using pruning parameter " << m_generator->m_process_parameters[parameters[i].parameter_id].name() << std::endl;
     279             :     }
     280             :   }
     281          12 : }
     282             : 
     283         720 : bool next_state_generator::summand_subset_t::is_not_false(const next_state_generator::summand_t& summand)
     284             : {
     285         720 :   return m_generator->m_rewriter(summand.condition, m_pruning_substitution) != data::sort_bool::false_();
     286             : }
     287             : 
     288         154 : atermpp::detail::shared_subset<next_state_generator::summand_t>::iterator next_state_generator::summand_subset_t::begin(const state& state)
     289             : {
     290         154 :   assert(m_use_summand_pruning);
     291             : 
     292        1048 :   for (std::size_t i = 0; i < m_pruning_parameters.size(); i++)
     293             :   {
     294         894 :     const variable& v=m_generator->m_process_parameters[m_pruning_parameters[i]];
     295         894 :     m_pruning_substitution[v] = v;
     296             :   }
     297             : 
     298         154 :   pruning_tree_node_t *node = &m_pruning_tree;
     299        1048 :   for (std::size_t i = 0; i < m_pruning_parameters.size(); i++)
     300             :   {
     301         894 :     std::size_t parameter = m_pruning_parameters[i];
     302         894 :     const data_expression& argument = state.element_at(parameter,m_generator->m_process_parameters.size());
     303         894 :     m_pruning_substitution[m_generator->m_process_parameters[parameter]] = argument;
     304         894 :     std::map<data_expression, pruning_tree_node_t>::iterator position = node->children.find(argument);
     305         894 :     if (position == node->children.end())
     306             :     {
     307         240 :       pruning_tree_node_t child;
     308         120 :       child.summand_subset = atermpp::detail::shared_subset<summand_t>(node->summand_subset, std::bind(&next_state_generator::summand_subset_t::is_not_false, this, std::placeholders::_1));
     309         120 :       node->children[argument] = child;
     310         120 :       node = &node->children[argument];
     311             :     }
     312             :     else
     313             :     {
     314         774 :       node = &position->second;
     315             :     }
     316             :   }
     317             : 
     318         154 :   return node->summand_subset.begin();
     319             : }
     320             : 
     321             : 
     322             : 
     323        2231 : next_state_generator::iterator::iterator(
     324             :            next_state_generator *generator, 
     325             :            const state& state, 
     326             :            next_state_generator::substitution_t *substitution, 
     327             :            next_state_generator::substitution_t *base_substitution, 
     328             :            summand_subset_t& summand_subset, 
     329        2231 :            enumerator_queue_t* enumeration_queue)
     330             :   : m_generator(generator),
     331             :     m_state(state),
     332             :     m_substitution(substitution),
     333             :     m_base_substitution(base_substitution),
     334             :     m_single_summand(false),
     335        2231 :     m_use_summand_pruning(summand_subset.m_use_summand_pruning),
     336             :     m_summand(nullptr),
     337             :     m_caching(false),
     338        4466 :     m_enumeration_queue(enumeration_queue)
     339             : {
     340        2231 :   if (m_use_summand_pruning)
     341             :   {
     342         154 :     m_summand_subset_iterator = summand_subset.begin(state);
     343             :   }
     344             :   else
     345             :   {
     346        2077 :     m_summand_iterator = summand_subset.m_summands.begin();
     347        2077 :     m_summand_iterator_end = summand_subset.m_summands.end();
     348             :   }
     349             : 
     350        2231 :   std::size_t j=0;
     351       22622 :   for (state::iterator i = state.begin(); i!=state.end(); ++i, ++j)
     352             :   {
     353       20391 :     (*m_substitution)[generator->m_process_parameters[j]] = *i;
     354             :   }
     355             : 
     356        2231 :   increment();
     357        2227 : }
     358             : 
     359        2996 : next_state_generator::iterator::iterator(
     360             :            next_state_generator *generator, 
     361             :            const state& state, 
     362             :            next_state_generator::substitution_t *substitution, 
     363             :            next_state_generator::substitution_t *base_substitution, 
     364             :            std::size_t summand_index, 
     365        2996 :            enumerator_queue_t* enumeration_queue)
     366             :   : m_generator(generator),
     367             :     m_state(state),
     368             :     m_substitution(substitution),
     369             :     m_base_substitution(base_substitution),
     370             :     m_single_summand(true),
     371             :     m_single_summand_index(summand_index),
     372             :     m_use_summand_pruning(false),
     373             :     m_summand(nullptr),
     374             :     m_caching(false),
     375        3000 :     m_enumeration_queue(enumeration_queue)
     376             : {
     377        2996 :   std::size_t j=0;
     378       35832 :   for (state::iterator i = state.begin(); i!=state.end(); ++i, ++j)
     379             :   {
     380       32836 :     (*m_substitution)[generator->m_process_parameters[j]] = *i;
     381             :   }
     382             : 
     383        2996 :   increment();
     384        2992 : }
     385             : 
     386             : struct is_not_zero
     387             : {
     388             :   // The argument intentionally does not have the type probabilistic_data_expression,
     389             :   // as this invokes == on probabilistic data expressions, which expects two fractions.
     390             :   // The enumerator can also generate open data expressions, which == on probabilistic_data_expressions
     391             :   // cannot handle.
     392         504 :   bool operator()(const data_expression& x) const
     393             :   {
     394         504 :     assert(x.sort()==sort_real::real_());
     395         504 :     return x!=probabilistic_data_expression::zero();
     396             :   }
     397             : };
     398             : 
     399         379 : const next_state_generator::transition_t::state_probability_list next_state_generator::calculate_distribution(
     400             :                          const stochastic_distribution& dist,
     401             :                          const data::data_expression_vector& state_args,
     402             :                          substitution_t& sigma)
     403             : {
     404         379 :   transition_t::state_probability_list resulting_state_probability_list;
     405         379 :   if (dist.variables().empty())
     406             :   {
     407         211 :     rewriter_class r(m_rewriter,sigma);
     408         422 :     const lps::state target_state(state_args.begin(),state_args.size(),r);
     409         211 :     resulting_state_probability_list.push_front(state_probability_pair(target_state,probabilistic_data_expression::one()));
     410             :   }
     411             :   else
     412             :   {
     413             :     // Save the expressions for variables that occur in the distribution, and reset these in sigma.
     414         336 :     std::vector<data_expression> old_values_for_variables;
     415         168 :     old_values_for_variables.reserve(dist.variables().size());
     416         336 :     for(const variable& v: dist.variables())
     417             :     {
     418         168 :       old_values_for_variables.push_back(sigma(v));
     419         168 :       sigma[v]=v;
     420             :     }
     421             : 
     422             :     typedef enumerator_algorithm_with_iterator<rewriter, enumerator_list_element_with_substitution<>, is_not_zero> enumerator_type;
     423         168 :     const bool throw_exceptions=true;
     424         168 :     enumerator_type enumerator(m_rewriter, m_specification.data(), m_rewriter, m_id_generator,
     425         504 :                                std::numeric_limits<std::size_t>::max(), throw_exceptions);
     426         336 :     data::enumerator_queue<enumerator_list_element_with_substitution<> > enumerator_solution_deque(enumerator_list_element_with_substitution<>(dist.variables(), dist.distribution()));
     427         504 :     for(enumerator_type::iterator probabilistic_solution = enumerator.begin(sigma, enumerator_solution_deque);
     428         504 :                                   probabilistic_solution != enumerator.end(); ++probabilistic_solution)
     429             :     {
     430         336 :       probabilistic_solution->add_assignments(dist.variables(),sigma,m_rewriter);
     431         336 :       rewriter_class r(m_rewriter,sigma);
     432         672 :       const lps::state target_state(state_args.begin(),state_args.size(),r);
     433         336 :       assert(probabilistic_solution->expression()==m_rewriter(dist.distribution(),sigma));
     434         672 :       const data_expression result=m_rewriter(data::less(probabilistic_data_expression::zero(),probabilistic_solution->expression()),sigma);
     435             :       // Reset substitution
     436         672 :       for(const variable& v: dist.variables())
     437             :       {
     438         336 :         sigma[v]=v;
     439             :       }
     440             : 
     441         336 :       if (result==sort_bool::true_())
     442             :       {
     443         336 :         resulting_state_probability_list.push_front(state_probability_pair(target_state,probabilistic_solution->expression()));
     444             :       }
     445           0 :       else if (result!=sort_bool::false_())
     446             :       {
     447           0 :         throw mcrl2::runtime_error("Comparison of fraction does not rewrite to true or false: " + pp(result) + ".");
     448             :       }
     449             :     }
     450             : 
     451             :     // Set the old values of sigma back again.
     452         168 :     std::vector<data_expression>::const_iterator i=old_values_for_variables.begin();
     453         336 :     for(const variable& v: dist.variables())
     454             :     {
     455         168 :       sigma[v]=*i;
     456         168 :       assert(i!=old_values_for_variables.end());
     457         168 :       i++;
     458             :     }
     459             :   }
     460         379 :   return resulting_state_probability_list;
     461             : }
     462             : 
     463             : 
     464             : 
     465       25129 : void next_state_generator::iterator::increment()
     466             : {
     467       61655 :   while (!m_summand ||
     468       67162 :          (m_cached && m_enumeration_cache_iterator == m_enumeration_cache_end) ||
     469       35412 :          (!m_cached && m_enumeration_iterator == m_generator->m_enumerator.end())
     470             :         )
     471             :   {
     472             :     // Here we have to get a new summand. Search through the summands until one is
     473             :     // found of which the condition is not equal to false. As a new summand is started
     474             :     // we can reset the identifier_generator as no local variables are in use. 
     475       21843 :     m_generator->m_id_generator.clear();
     476       21843 :     if (m_caching)
     477             :     {
     478         249 :       m_summand->enumeration_cache[m_enumeration_cache_key] = m_enumeration_log;
     479             :     }
     480             : 
     481       21843 :     if (m_single_summand)
     482             :     {
     483        5988 :       if (m_summand)
     484             :       {
     485        2992 :         m_generator = nullptr;
     486        8211 :         return;
     487             :       }
     488        2996 :       m_summand = &(m_generator->m_summands[m_single_summand_index]);
     489             :     }
     490       15855 :     else if (m_use_summand_pruning)
     491             :     {
     492         304 :       if (!m_summand_subset_iterator)
     493             :       {
     494         152 :         m_generator = nullptr;
     495         152 :         return;
     496             :       }
     497         152 :       m_summand = &(*m_summand_subset_iterator++);
     498             :     }
     499             :     else
     500             :     {
     501       15551 :       if (m_summand_iterator == m_summand_iterator_end)
     502             :       {
     503        2075 :         m_generator = nullptr;
     504        2075 :         return;
     505             :       }
     506       13476 :       m_summand = &(m_generator->m_summands[*m_summand_iterator++]);
     507             :     }
     508             : 
     509       16624 :     if (m_generator->m_use_enumeration_caching)
     510             :     {
     511        2305 :       state_applier apply_m_state(m_state,m_generator->m_process_parameters.size());
     512        6915 :       m_enumeration_cache_key = condition_arguments_t(m_summand->condition_arguments_function,
     513        2305 :                                                       m_summand->condition_parameters.begin(),
     514        2305 :                                                       m_summand->condition_parameters.end(),
     515        2305 :                                                       apply_m_state);
     516             : 
     517        2305 :       std::map<condition_arguments_t, summand_enumeration_t>::iterator position = m_summand->enumeration_cache.find(m_enumeration_cache_key);
     518        2305 :       if (position == m_summand->enumeration_cache.end())
     519             :       {
     520         253 :         m_cached = false;
     521         253 :         m_caching = true;
     522         253 :         m_enumeration_log.clear();
     523             :       }
     524             :       else
     525             :       {
     526        2052 :         m_cached = true;
     527        2052 :         m_caching = false;
     528        2052 :         m_enumeration_cache_iterator = position->second.begin();
     529        2052 :         m_enumeration_cache_end = position->second.end();
     530             :       }
     531             :     }
     532             :     else
     533             :     {
     534       14319 :       m_cached = false;
     535       14319 :       m_caching = false;
     536             :     }
     537       16624 :     if (!m_cached)
     538             :     {
     539       21705 :       for (data::variable_list::iterator i = m_summand->variables.begin(); i != m_summand->variables.end(); i++)
     540             :       {
     541        7133 :         (*m_substitution)[*i] = *i;  // Reset the variable.
     542             :       }
     543       14572 :       enumerate(m_summand->variables, m_summand->condition, *m_substitution);
     544             :     }
     545             :   }
     546             : 
     547        6572 :   data_expression_list valuation;
     548        3286 :   if (m_cached)
     549             :   {
     550         288 :     valuation = *m_enumeration_cache_iterator;
     551         288 :     m_enumeration_cache_iterator++;
     552         288 :     assert(valuation.size() == m_summand->variables.size());
     553         288 :     data_expression_list::iterator v = valuation.begin();
     554         480 :     for (variable_list::iterator i = m_summand->variables.begin(); i != m_summand->variables.end(); i++, v++)
     555             :     {
     556         192 :       (*m_substitution)[*i] = *v;
     557             :     }
     558             :   }
     559             :   else
     560             :   {
     561        2998 :     m_enumeration_iterator->add_assignments(m_summand->variables,*m_substitution,m_generator->m_rewriter);
     562             : 
     563             :     // If we failed to exactly rewrite the condition to true, nextstate generation fails.
     564        2998 :     if (m_enumeration_iterator->expression()!=sort_bool::true_())
     565             :     {
     566           8 :       assert(m_enumeration_iterator->expression()!=sort_bool::false_());
     567             : 
     568             :       // Reduce condition as much as possible, and give a hint of the original condition in the error message.
     569          16 :       data_expression reduced_condition(m_generator->m_rewriter(m_summand->condition, *m_substitution));
     570          16 :       std::string printed_condition(data::pp(data::replace_variables(m_summand->condition,*m_base_substitution)).substr(0, 300));  //XXXX
     571             : 
     572          16 :       throw mcrl2::runtime_error("Expression " + data::pp(reduced_condition) +
     573             :                                  " does not rewrite to true or false in the condition "
     574          16 :                                  + printed_condition
     575          24 :                                  + (printed_condition.size() >= 300?"...":""));
     576             :     }
     577             : 
     578        2990 :     m_enumeration_iterator++;
     579        2990 :     if (m_caching)
     580             :     {
     581          84 :       valuation=data_expression_list(m_summand->variables.begin(),m_summand->variables.end(),*m_substitution);
     582          84 :       assert(valuation.size() == m_summand->variables.size());
     583             :     }
     584             :   }
     585             : 
     586        3278 :   if (m_caching)
     587             :   {
     588          84 :     m_enumeration_log.push_back(valuation);
     589             :   }
     590             : 
     591             :   // Calculate the effect of the distribution.
     592             : 
     593        3278 :   const stochastic_distribution& dist=m_summand->distribution;
     594        3278 :   if (dist.variables().empty())
     595             :   {
     596             :     // There is no distribution, and therefore only one target state is generated
     597        3122 :     const data_expression_vector& state_args=m_summand->result_state;
     598        3122 :     rewriter_class r(m_generator->m_rewriter,*m_substitution);
     599        3122 :     m_transition.set_target_state(lps::state(state_args.begin(),state_args.size(),r));
     600        3122 :     m_transition.set_other_target_states(transition_t::state_probability_list());
     601             :   }
     602             :   else
     603             :   {
     604             :     // There is a non trivial distribution. We need to generate states and their probabilities.
     605             :     // The current implementation is inefficient, but efficiency is of a later concern.
     606             : 
     607             :     transition_t::state_probability_list resulting_state_probability_list=
     608         312 :                          m_generator->calculate_distribution(dist,m_summand->result_state,*m_substitution);
     609         156 :     if (resulting_state_probability_list.empty())
     610             :     {
     611             :       // There are no state probability pairs. But this is wrong. The total probabilities should add up to one.
     612             :       // This means there should at least be one probability.
     613           0 :       throw mcrl2::runtime_error("The distribution " + pp(m_generator->m_rewriter(dist.distribution(),*m_substitution)) + " has an empty set of instances.");
     614             :     }
     615             :     // Set one state as the resulting state, and leave the other states in the resulting_state_probability_list.
     616         156 :     m_transition.set_target_state(resulting_state_probability_list.front().state());
     617         156 :     resulting_state_probability_list.pop_front();
     618         156 :     m_transition.set_other_target_states(resulting_state_probability_list);
     619             :   }
     620             : 
     621        6556 :   std::vector <process::action> actions;
     622        3278 :   actions.resize(m_summand->action_label.size());
     623        6556 :   std::vector < data_expression> arguments;
     624        6502 :   for (std::size_t i = 0; i < m_summand->action_label.size(); i++)
     625             :   {
     626        3224 :     arguments.resize(m_summand->action_label[i].arguments.size());
     627        6000 :     for (std::size_t j = 0; j < m_summand->action_label[i].arguments.size(); j++)
     628             :     {
     629        2776 :       arguments[j] = m_generator->m_rewriter(m_summand->action_label[i].arguments[j], *m_substitution);
     630             :     }
     631        3224 :     actions[i] = process::action(m_summand->action_label[i].label, data_expression_list(arguments.begin(), arguments.end()));
     632             :   }
     633        3278 :   if (m_summand->time_tag==data_expression())  // Check whether the time_tag is valid.
     634             :   {
     635        3272 :     m_transition.set_action(multi_action(process::action_list(actions.begin(), actions.end())));
     636             :   }
     637             :   else
     638             :   {
     639          12 :     m_transition.set_action(
     640          12 :               multi_action(process::action_list(actions.begin(), actions.end()),
     641          12 :                            m_generator->m_rewriter(m_summand->time_tag, *m_substitution)));
     642             :   }
     643             : 
     644        3278 :   m_transition.set_summand_index(m_summand - &m_generator->m_summands[0]);
     645             : 
     646        5718 :   for (variable_list::iterator i = m_summand->variables.begin(); i != m_summand->variables.end(); i++)
     647             :   {
     648        2440 :     (*m_substitution)[*i] = *i;  // Reset the variable.
     649             :   }
     650         261 : }

Generated by: LCOV version 1.13