LCOV - code coverage report
Current view: top level - lts/source - exploration.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 304 709 42.9 %
Date: 2021-05-13 00:46:59 Functions: 19 42 45.2 %
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             : #include <iomanip>
      10             : 
      11             : #include "mcrl2/lps/resolve_name_clashes.h"
      12             : #include "mcrl2/lps/detail/instantiate_global_variables.h"
      13             : #include "mcrl2/lps/one_point_rule_rewrite.h"
      14             : #include "mcrl2/lps/detail/move_constants_to_substitution.h"
      15             : #include "mcrl2/lts/detail/exploration.h"
      16             : #include "mcrl2/lts/detail/counter_example.h"
      17             : 
      18             : using namespace mcrl2;
      19             : using namespace mcrl2::log;
      20             : using namespace mcrl2::lps;
      21             : using namespace mcrl2::lts;
      22             : 
      23         116 : probabilistic_state<std::size_t, probabilistic_data_expression> lps2lts_algorithm::transform_initial_probabilistic_state_list
      24             :                  (const next_state_generator::transition_t::state_probability_list& initial_states)
      25             : {
      26         116 :   assert(!initial_states.empty());
      27         116 :   if (++initial_states.begin() == initial_states.end()) // Means initial_states.size()==1
      28             :   {
      29         108 :     std::size_t state_number=m_state_numbers.insert(initial_states.front().state()).first;
      30         108 :     return probabilistic_state<std::size_t, probabilistic_data_expression>(state_number);
      31             :   }
      32          16 :   std::vector <state_probability_pair<std::size_t, lps::probabilistic_data_expression> > result;
      33          24 :   for(lps::next_state_generator::transition_t::state_probability_list::const_iterator i=initial_states.begin();
      34          24 :                     i!=initial_states.end(); ++i)
      35             :   {
      36          16 :     std::size_t state_number=m_state_numbers.insert(i->state()).first;
      37          16 :     result.push_back(state_probability_pair<std::size_t, probabilistic_data_expression>(state_number, i->probability()));
      38             :   }
      39           8 :   return probabilistic_state<std::size_t, probabilistic_data_expression>(result.begin(),result.end());
      40             : }
      41             : 
      42        1640 : probabilistic_state<std::size_t, probabilistic_data_expression> lps2lts_algorithm::create_a_probabilistic_state_from_target_distribution(
      43             :                const std::size_t base_state_number,
      44             :                const next_state_generator::transition_t::state_probability_list& other_probabilities,
      45             :                const lps::state& source_state,
      46             :                const std::function<void(const lps::state&)> add_state_to_todo_queue_function)
      47             : {
      48        1640 :   if (other_probabilities.empty())
      49             :   {
      50        1536 :     return probabilistic_state<std::size_t, probabilistic_data_expression>(base_state_number);
      51             :   }
      52             : 
      53         208 :   std::vector <state_probability_pair<std::size_t, probabilistic_data_expression> > result;
      54             : 
      55         208 :   probabilistic_data_expression residual_probability=probabilistic_data_expression::one();
      56             : 
      57         104 :   for(lps::next_state_generator::transition_t::state_probability_list::const_iterator
      58         104 :                          i=other_probabilities.begin();
      59         208 :                          i!=other_probabilities.end(); ++i)
      60             :   {
      61         104 :     if (is_application(i->probability()) && atermpp::down_cast<data::application>(i->probability()).head().size()!=3)
      62             :     {
      63           0 :       throw mcrl2::runtime_error("The probability " + data::pp(i->probability()) + " is not a proper rational number.");
      64             :     }
      65         104 :     residual_probability=data::sort_real::minus(residual_probability,i->probability());
      66         104 :     const std::size_t probability_destination_state_number=add_target_state(source_state,i->state(),add_state_to_todo_queue_function);
      67         104 :     result.push_back(state_probability_pair<std::size_t, probabilistic_data_expression>(probability_destination_state_number, i->probability()));
      68             :   }
      69             : 
      70         104 :   residual_probability= (m_generator->get_rewriter())(residual_probability);
      71         104 :   result.push_back(state_probability_pair<std::size_t, probabilistic_data_expression>(base_state_number, residual_probability));
      72         104 :   return  probabilistic_state<std::size_t, probabilistic_data_expression>(result.begin(),result.end());
      73             : }
      74             : 
      75           0 : bool is_hidden_summand(const mcrl2::process::action_list& l,
      76             :                        const std::set<core::identifier_string>& internal_action_labels)
      77             : {
      78             :   // Note that if l is empty, true is returned, as desired.
      79           0 :   for(const mcrl2::process::action& a: l)
      80             :   {
      81           0 :     if (internal_action_labels.count(a.label().name())==0) // Not found, s has a visible action among its multi-actions.
      82             :     {
      83           0 :       return false;
      84             :     }
      85             :   }
      86           0 :   return true;
      87             : }
      88             : 
      89         187 : void lps2lts_algorithm::initialise_lts_generation(const lts_generation_options& options)
      90             : {
      91         187 :   m_options = options;
      92             : 
      93         187 :   assert(!(m_options.bithashing && m_options.outformat != lts_aut && m_options.outformat != lts_none));
      94             : 
      95         187 :   if (m_options.bithashing)
      96             :   {
      97           0 :     m_bit_hash_table = bit_hash_table(m_options.bithashsize);
      98             :   }
      99             :   else
     100             :   {
     101         187 :     m_state_numbers = utilities::indexed_set<lps::state>(m_options.initial_table_size);
     102             :   }
     103             : 
     104         187 :   m_num_states = 0;
     105         187 :   m_num_transitions = 0;
     106         187 :   m_level = 1;
     107         187 :   m_traces_saved = 0;
     108             : 
     109         187 :   m_maintain_traces = m_options.trace || m_options.save_error_trace;
     110         187 :   m_value_prioritize = (m_options.expl_strat == es_value_prioritized || m_options.expl_strat == es_value_random_prioritized);
     111             : 
     112         374 :   lps::stochastic_specification specification(m_options.specification);
     113         187 :   resolve_summand_variable_name_clashes(specification);
     114             : 
     115         187 :   if (m_options.outformat == lts_aut)
     116             :   {
     117          71 :     mCRL2log(verbose) << "writing state space in AUT format to '" << m_options.lts << "'." << std::endl;
     118          71 :     m_aut_file.open(m_options.lts.c_str());
     119          71 :     if (!m_aut_file.is_open())
     120             :     {
     121           0 :       mCRL2log(error) << "cannot open '" << m_options.lts << "' for writing" << std::endl;
     122           0 :       std::exit(EXIT_FAILURE);
     123             :     }
     124             :   }
     125         116 :   else if (m_options.outformat == lts_none)
     126             :   {
     127           0 :     mCRL2log(verbose) << "not saving state space." << std::endl;
     128             :   }
     129             :   else
     130             :   {
     131         116 :     mCRL2log(verbose) << "writing state space in " << mcrl2::lts::detail::string_for_type(m_options.outformat)
     132           0 :                       << " format to '" << m_options.lts << "'." << std::endl;
     133         116 :     m_output_lts.set_data(specification.data());
     134         116 :     m_output_lts.set_process_parameters(specification.process().process_parameters());
     135         116 :     m_output_lts.set_action_label_declarations(specification.action_labels());
     136             :   }
     137             : 
     138             : 
     139         187 :   if (m_options.usedummies)
     140             :   {
     141         187 :     lps::detail::instantiate_global_variables(specification);
     142             :   }
     143             : 
     144         374 :   data::rewriter rewriter;
     145             : 
     146         187 :   if (m_options.removeunused)
     147             :   {
     148         187 :     mCRL2log(verbose) << "removing unused parts of the data specification." << std::endl;
     149         374 :     std::set<data::function_symbol> extra_function_symbols = lps::find_function_symbols(specification);
     150         187 :     extra_function_symbols.insert(data::sort_real::minus(data::sort_real::real_(),data::sort_real::real_()));
     151             :     // The symbols below are needed to compare probabilities. Greater implies the inclusion of smaller. 
     152         187 :     extra_function_symbols.insert(data::greater(data::sort_real::real_()));
     153             : 
     154         187 :     if (m_options.expl_strat == es_value_prioritized || m_options.expl_strat == es_value_random_prioritized)
     155             :     {
     156           0 :       extra_function_symbols.insert(data::greater(data::sort_nat::nat()));
     157           0 :       extra_function_symbols.insert(data::equal_to(data::sort_nat::nat()));
     158             :     }
     159             : 
     160         374 :     rewriter = data::rewriter(specification.data(), 
     161         374 :                               data::used_data_equation_selector(specification.data(), extra_function_symbols, specification.global_variables()), 
     162             :                               m_options.strat);
     163             :   }
     164             :   else
     165             :   {
     166           0 :     rewriter = data::rewriter(specification.data(), m_options.strat);
     167             :   }
     168             : 
     169             :   // Apply the one point rewriter to the linear process specification.
     170             :   // This simplifies expressions of the shape exists x:X . (x == e) && phi to phi[x:=e], enabling
     171             :   // more lps's to generate lts's. The overhead of this rewriter is limited.
     172         187 :   one_point_rule_rewrite(specification);
     173             : 
     174             :   // Replace all constant expressions t in a specification by a variable x, and set base_substitution(x)=u where u is the normal form of t.
     175             :   // This avoids having to rewrite the constant expressions each time they are encountered. This typically saves more than 50% of the total
     176             :   // time to generate a state space.
     177         374 :   data::mutable_indexed_substitution<> base_substitution;  // This is the substitution used as base in the state space generation.
     178         187 :   move_constants_to_substitution(specification, rewriter, base_substitution);
     179             : 
     180         374 :   stochastic_action_summand_vector prioritised_summands;
     181         374 :   stochastic_action_summand_vector nonprioritised_summands;
     182         187 :   if (m_options.priority_action != "")
     183             :   {
     184          12 :     mCRL2log(verbose) << "applying confluence reduction with tau action '" << m_options.priority_action << "'..." << std::endl;
     185             : 
     186          84 :     for(const stochastic_action_summand& s: specification.process().action_summands())
     187             :     {
     188         216 :       if ((m_options.priority_action == "tau" && s.is_tau()) ||
     189         204 :           (s.multi_action().actions().size() == 1 && m_options.priority_action == static_cast<std::string>(s.multi_action().actions().front().label().name())))
     190             :       {
     191           6 :         prioritised_summands.push_back(s);
     192             :       }
     193             :       else
     194             :       {
     195          66 :         nonprioritised_summands.push_back(s);
     196             :       }
     197             :     }
     198             : 
     199          12 :     m_use_confluence_reduction = true;
     200             :   }
     201             :   else
     202             :   {
     203         175 :     m_use_confluence_reduction = false;
     204             :   }
     205             : 
     206         374 :   stochastic_action_summand_vector tau_summands;
     207         187 :   if (m_options.detect_divergence)
     208             :   {
     209           0 :     mCRL2log(verbose) << "Detect divergences where actions with the following labels are hidden: tau";
     210           0 :     for(const core::identifier_string& a: m_options.actions_internal_for_divergencies)
     211             :     {
     212           0 :       mCRL2log(verbose) << ", " << a;
     213             :     }
     214           0 :     mCRL2log(verbose) << ".\n";
     215             : 
     216           0 :     for (const stochastic_action_summand& s: specification.process().action_summands())
     217             :     {
     218           0 :       if (is_hidden_summand(s.multi_action().actions(),m_options.actions_internal_for_divergencies))
     219             :       {
     220           0 :         tau_summands.push_back(s);
     221             :       }
     222             :     }
     223             :   }
     224             : 
     225         187 :   if (m_options.detect_action)
     226             :   {
     227           0 :     m_detected_action_summands.reserve(specification.process().action_summands().size());
     228           0 :     for (std::size_t i = 0; i < specification.process().action_summands().size(); i++)
     229             :     {
     230           0 :       bool found = false;
     231           0 :       for (process::action_list::const_iterator j = specification.process().action_summands()[i].multi_action().actions().begin();
     232           0 :                          j != specification.process().action_summands()[i].multi_action().actions().end(); j++)
     233             :       {
     234           0 :         if (m_options.trace_actions.count(j->label().name()) > 0)
     235             :         {
     236           0 :           found = true;
     237           0 :           break;
     238             :         }
     239             :       }
     240           0 :       m_detected_action_summands.push_back(found);
     241             :     }
     242             :   }
     243             : 
     244         187 :   bool compute_actions = m_options.outformat != lts_none || m_options.detect_action || !m_options.trace_multiactions.empty() ||
     245         187 :                          m_maintain_traces || m_value_prioritize || !m_options.actions_internal_for_divergencies.empty();
     246         187 :   if (!compute_actions)
     247             :   {
     248           0 :     for (std::size_t i = 0; i < specification.process().action_summands().size(); i++)
     249             :     {
     250           0 :       specification.process().action_summands()[i].multi_action().actions() = process::action_list();
     251             :     }
     252             : 
     253           0 :     if (m_use_confluence_reduction)
     254             :     {
     255           0 :       for (std::size_t i = 0; i < nonprioritised_summands.size(); i++)
     256             :       {
     257           0 :         nonprioritised_summands[i].multi_action().actions() = process::action_list();
     258             :       }
     259           0 :       for (std::size_t i = 0; i < prioritised_summands.size(); i++)
     260             :       {
     261           0 :         prioritised_summands[i].multi_action().actions() = process::action_list();
     262             :       }
     263             :     }
     264             :   }
     265         187 :   m_generator = new next_state_generator(specification, rewriter, base_substitution, m_options.use_enumeration_caching, m_options.use_summand_pruning);
     266             : 
     267         187 :   if (m_use_confluence_reduction)
     268             :   {
     269          12 :     m_nonprioritized_subset = next_state_generator::summand_subset_t(m_generator, nonprioritised_summands, m_options.use_summand_pruning);
     270          12 :     m_prioritized_subset = next_state_generator::summand_subset_t(m_generator, prioritised_summands, m_options.use_summand_pruning);
     271          12 :     m_main_subset = &m_nonprioritized_subset;
     272             :   }
     273             :   else
     274             :   {
     275         175 :     m_main_subset = &m_generator->full_subset();
     276             :   }
     277             : 
     278         187 :   if (m_options.detect_divergence)
     279             :   {
     280           0 :     m_tau_summands = next_state_generator::summand_subset_t(m_generator, tau_summands, m_options.use_summand_pruning);
     281             :   }
     282             : 
     283         187 :   if (m_options.detect_deadlock)
     284             :   {
     285           0 :     mCRL2log(verbose) << "Detect deadlocks.\n" ;
     286             :   }
     287             : 
     288         187 :   if (m_options.detect_nondeterminism)
     289             :   {
     290           0 :     mCRL2log(verbose) << "Detect nondeterministic states.\n" ;
     291             :   }
     292         187 : }
     293             : 
     294           0 : void set_seed_random_generator()
     295             : {
     296             :   // In order to guarantee that time is different from a previous run to initialise
     297             :   // the seed of a previous run and not get the same results, we wait until time gets
     298             :   // a fresh value. It is better to replace this by c++11 random generators, as this
     299             :   // is an awkward solution.
     300           0 :   for(time_t t = time(nullptr); time(nullptr) == t; )
     301             :   {}  ; // Wait until time changes.
     302           0 :   srand((unsigned)time(nullptr));
     303           0 : }
     304             : 
     305         187 : bool lps2lts_algorithm::generate_lts(const lts_generation_options& options)
     306             : {
     307         187 :   initialise_lts_generation(options);
     308             :   // First generate a vector of initial states from the initial distribution.
     309         187 :   m_initial_states=m_generator->initial_states();
     310         187 :   assert(!m_initial_states.empty());
     311             : 
     312             :   // Count the number of states.
     313         187 :   m_num_states = 0;
     314         386 :   for(lps::next_state_generator::transition_t::state_probability_list::const_iterator i=m_initial_states.begin();
     315         386 :                     i!=m_initial_states.end(); ++i)
     316             :   {
     317         199 :     m_num_states++;
     318             :   }
     319             : 
     320         187 :   if (m_use_confluence_reduction)
     321             :   {
     322          12 :     set_prioritised_representatives(m_initial_states);
     323             :   }
     324             : 
     325         187 :   if (m_options.bithashing)
     326             :   {
     327           0 :     m_bit_hash_table.add_states(m_initial_states);
     328             :   }
     329             :   else
     330             :   {
     331             :     // Store the initial states in the indexed set.
     332         386 :     for(lps::next_state_generator::transition_t::state_probability_list::const_iterator i=m_initial_states.begin();
     333         386 :                     i!=m_initial_states.end(); ++i)
     334             :     {
     335         199 :       if (m_state_numbers.insert(i->state()).second && m_options.outformat != lts_aut) // The state is new.
     336             :       {
     337         124 :         m_output_lts.add_state(state_label_lts(i->state()));
     338             :       }
     339             :     }
     340             :   }
     341             : 
     342         187 :   if (m_options.outformat == lts_aut)
     343             :   {
     344          71 :     m_aut_file << "des(";
     345          71 :     print_target_distribution_in_aut_format(m_initial_states,lps::state(),[](const lps::state&){});
     346             :     // HACK: this line will be overwritten once generation is finished.
     347          71 :     m_aut_file << ",0,0)                                          " << std::endl;
     348             :   }
     349         116 :   else if (m_options.outformat != lts_none)
     350             :   {
     351         116 :     m_output_lts.set_initial_probabilistic_state(transform_initial_probabilistic_state_list(m_initial_states));
     352             :   }
     353             : 
     354         187 :   mCRL2log(verbose) << "generating state space with '" << m_options.expl_strat << "' strategy...\n";
     355             : 
     356         187 :   if (m_options.max_states == 0)
     357             :   {
     358           0 :     return true;
     359             :   }
     360         187 :   if (m_options.expl_strat == es_breadth || m_options.expl_strat == es_value_prioritized)
     361             :   {
     362         100 :     if (m_options.bithashing)
     363             :     {
     364           0 :       generate_lts_breadth_bithashing(m_initial_states);
     365             :     }
     366             :     else
     367             :     {
     368         100 :       if (m_options.todo_max==std::string::npos)
     369             :       {
     370         100 :         generate_lts_breadth_todo_max_is_npos(m_initial_states);
     371             :       }
     372             :       else
     373             :       {
     374           0 :         set_seed_random_generator();
     375           0 :         generate_lts_breadth_todo_max_is_not_npos(m_initial_states);
     376             :       }
     377             :     }
     378             : 
     379         100 :     mCRL2log(verbose) << "done with state space generation ("
     380           0 :                       << m_level-1 << " level" << ((m_level==2)?"":"s") << ", "
     381           0 :                       << m_num_states << " state" << ((m_num_states == 1)?"":"s")
     382           0 :                       << " and " << m_num_transitions << " transition" << ((m_num_transitions==1)?"":"s") << ")" << std::endl;
     383             :   }
     384          87 :   else if (m_options.expl_strat == es_depth)
     385             :   {
     386          87 :     generate_lts_depth(m_initial_states);
     387             : 
     388          87 :     mCRL2log(verbose) << "done with state space generation ("
     389           0 :                       << m_num_states << " state" << ((m_num_states == 1)?"":"s")
     390           0 :                       << " and " << m_num_transitions << " transition" << ((m_num_transitions==1)?"":"s") << ")" << std::endl;
     391             :   }
     392           0 :   else if (m_options.expl_strat == es_random || m_options.expl_strat == es_value_random_prioritized)
     393             :   {
     394           0 :     set_seed_random_generator();
     395             : 
     396           0 :     generate_lts_random(m_initial_states);
     397             : 
     398           0 :     mCRL2log(verbose) << "done with random walk of "
     399           0 :                       << m_num_transitions << " transition" << ((m_num_transitions==1)?"":"s")
     400           0 :                       << " (visited " << m_num_states
     401           0 :                       << " unique state" << ((m_num_states == 1)?"":"s") << ")" << std::endl;
     402             :   }
     403             :   else
     404             :   {
     405           0 :     mCRL2log(error) << "unknown exploration strategy" << std::endl;
     406           0 :     return false;
     407             :   }
     408             : 
     409         187 :   finalise_lts_generation();
     410         187 :   return true;
     411             : }
     412             : 
     413         187 : void lps2lts_algorithm::finalise_lts_generation()
     414             : {
     415         187 :   if (m_options.outformat == lts_aut)
     416             :   {
     417          71 :     m_aut_file.flush();
     418          71 :     m_aut_file.seekp(0);
     419          71 :     m_aut_file << "des (";
     420          71 :     print_target_distribution_in_aut_format(m_initial_states,lps::state(),[](const lps::state&){});
     421          71 :     m_aut_file << "," << m_num_transitions << "," << m_num_states << ")";
     422          71 :     m_aut_file.close();
     423             :   }
     424         116 :   else if (m_options.outformat != lts_none)
     425             :   {
     426         116 :     if (!m_options.outinfo)
     427             :     {
     428           0 :       m_output_lts.clear_state_labels();
     429             :     }
     430             : 
     431         116 :     switch (m_options.outformat)
     432             :     {
     433          58 :       case lts_lts:
     434             :       {
     435          58 :         m_output_lts.save(m_options.lts);
     436          58 :         break;
     437             :       }
     438          58 :       case lts_fsm:
     439             :       {
     440         116 :         probabilistic_lts_fsm_t fsm;
     441          58 :         detail::lts_convert(m_output_lts, fsm);
     442          58 :         fsm.save(m_options.lts);
     443          58 :         break;
     444             :       }
     445           0 :       case lts_dot:
     446             :       {
     447           0 :         probabilistic_lts_dot_t dot;
     448           0 :         detail::lts_convert(m_output_lts, dot);
     449           0 :         dot.save(m_options.lts);
     450           0 :         break;
     451             :       }
     452           0 :       default:
     453           0 :         assert(0);
     454             :     }
     455             :   }
     456         187 : }
     457             : 
     458          12 : void lps2lts_algorithm::set_prioritised_representatives(next_state_generator::transition_t::state_probability_list& states)
     459             : {
     460          24 :   for(next_state_generator::transition_t::state_probability_list::iterator i=states.begin(); i!=states.end(); ++i)
     461             :   {
     462          12 :     i->state()=get_prioritised_representative(i->state());
     463             :   }
     464          12 : }
     465             : 
     466             : // Confluence reduction based on S.C.C. Blom, Partial tau-confluence for
     467             : // Efficient State Space Generation, Technical Report SEN-R0123, CWI, Amsterdam, 2001
     468             : 
     469         576 : lps::state lps2lts_algorithm::get_prioritised_representative(const lps::state& state1)
     470             : {
     471         576 :   lps::state state=state1;
     472         576 :   assert(m_use_confluence_reduction);
     473             : 
     474        1152 :   std::map<lps::state, std::size_t> number;
     475        1152 :   std::map<lps::state, std::size_t> low;
     476        1152 :   std::map<lps::state, std::list<lps::state> > next;
     477        1152 :   std::map<lps::state, lps::state> back;
     478        1152 :   next_state_generator::enumerator_queue_t enumeration_queue;
     479             : 
     480         576 :   std::size_t count = 0;
     481         576 :   number[state] = 0;
     482             : 
     483             :   while (true)
     484             :   {
     485         582 :     assert(number.count(state) > 0);
     486         582 :     if (number[state] == 0)
     487             :     {
     488         582 :       count++;
     489         582 :       number[state] = count;
     490         582 :       low[state] = count;
     491         582 :       next[state] = std::list<lps::state>();
     492             : 
     493         582 :       enumeration_queue.clear();
     494         588 :       for (next_state_generator::iterator i = m_generator->begin(state, m_prioritized_subset, &enumeration_queue); i; i++)
     495             :       {
     496          12 :         const lps::state s=i->target_state();
     497           6 :         next[state].push_back(s);
     498           6 :         if (number.count(s) == 0)
     499             :         {
     500           6 :           number[s] = 0;
     501             :         }
     502             :       }
     503             :     }
     504         582 :     assert(next.count(state) > 0);
     505         582 :     if (next[state].empty())
     506             :     {
     507         576 :       assert(low.count(state) > 0);
     508         576 :       if (number[state] == low[state])
     509             :       {
     510        1152 :         return state;
     511             :       }
     512           0 :       assert(back.count(state) > 0);
     513           0 :       lps::state back_state = back[state];
     514           0 :       low[back_state] = low[back_state] < low[state] ? low[back_state] : low[state];
     515           0 :       state = back_state;
     516             :     }
     517             :     else
     518             :     {
     519          12 :       lps::state next_state = next[state].front();
     520           6 :       next[state].pop_front();
     521           6 :       if (number[next_state] == 0)
     522             :       {
     523           6 :         back[next_state] = state;
     524           6 :         state = next_state;
     525             :       }
     526           0 :       else if (number[next_state] < number[state])
     527             :       {
     528           0 :         low[state] = low[state] < number[next_state] ? low[state] : number[next_state];
     529             :       }
     530             :     }
     531           6 :   }
     532             : }
     533             : 
     534           0 : void lps2lts_algorithm::value_prioritize(std::vector<next_state_generator::transition_t>& transitions)
     535             : {
     536           0 :   data::data_expression lowest_value;
     537             : 
     538           0 :   for (std::vector<next_state_generator::transition_t>::iterator i = transitions.begin(); i != transitions.end(); i++)
     539             :   {
     540           0 :     if (i->action().actions().size() == 1 && i->action().actions().front().arguments().size() > 0)
     541             :     {
     542           0 :       const data::data_expression& argument = i->action().actions().front().arguments().front();
     543           0 :       if (mcrl2::data::sort_nat::is_nat(argument.sort()))
     544             :       {
     545           0 :         if (lowest_value==data::data_expression()) // lowest value is undefined.
     546             :         {
     547           0 :           lowest_value = argument;
     548             :         }
     549             :         else
     550             :         {
     551           0 :           const data::data_expression result = m_generator->get_rewriter()(data::greater(lowest_value, argument));
     552             : 
     553           0 :           if (data::sort_bool::is_true_function_symbol(result))
     554             :           {
     555           0 :             lowest_value = argument;
     556             :           }
     557           0 :           else if (!data::sort_bool::is_false_function_symbol(result))
     558             :           {
     559           0 :             if (m_options.outformat == lts_aut)
     560             :             {
     561           0 :               m_aut_file.flush();
     562             :             }
     563           0 :             throw mcrl2::runtime_error("Fail to rewrite term " + data::pp(result) + " to true or false.");
     564             :           }
     565             :         }
     566             :       }
     567             :     }
     568             :   }
     569             : 
     570           0 :   std::size_t new_position=0;
     571           0 :   for (std::vector<next_state_generator::transition_t>::const_iterator i = transitions.begin(); i != transitions.end(); ++i)
     572             :   {
     573           0 :     if (i->action().actions().size() != 1)
     574             :     {
     575           0 :       transitions[new_position++]= *i;
     576             :     }
     577           0 :     else if (i->action().actions().front().arguments().size() == 0)
     578             :     {
     579           0 :       transitions[new_position++]= *i;
     580             :     }
     581           0 :     else if (!mcrl2::data::sort_nat::is_nat(i->action().actions().front().arguments().front().sort()))
     582             :     {
     583           0 :       transitions[new_position++]= *i;
     584             :     }
     585             :     else
     586             :     {
     587           0 :       data::data_expression result = m_generator->get_rewriter()(data::equal_to(lowest_value, i->action().actions().front().arguments().front()));
     588             : 
     589           0 :       if (data::sort_bool::is_true_function_symbol(result))
     590             :       {
     591           0 :         transitions[new_position++]= *i;
     592             :       }
     593           0 :       else if (data::sort_bool::is_false_function_symbol(result))
     594             :       {
     595             :         // Skip the transition at position i.
     596             :       }
     597             :       else
     598             :       {
     599           0 :         if (m_options.outformat == lts_aut)
     600             :         {
     601           0 :           m_aut_file.flush();
     602             :         }
     603           0 :         throw mcrl2::runtime_error("Fail to rewrite term " + data::pp(result) + " to true or false.");
     604             :       }
     605             :     }
     606             :   }
     607           0 :   transitions.resize(new_position);
     608           0 : }
     609             : 
     610           0 : void lps2lts_algorithm::construct_trace(const lps::state& state1, mcrl2::trace::Trace& trace)
     611             : {
     612           0 :   lps::state state=state1;
     613           0 :   std::deque<lps::state> states;
     614           0 :   std::map<lps::state, lps::state>::iterator source;
     615           0 :   while ((source = m_backpointers.find(state)) != m_backpointers.end())
     616             :   {
     617           0 :     states.push_front(state);
     618           0 :     state = source->second;
     619             :   }
     620             : 
     621           0 :   trace.setState(state);
     622           0 :   next_state_generator::enumerator_queue_t enumeration_queue;
     623           0 :   for (std::deque<lps::state>::iterator i = states.begin(); i != states.end(); i++)
     624             :   {
     625           0 :     bool found=false;
     626           0 :     for (next_state_generator::iterator j = m_generator->begin(state, &enumeration_queue); j != m_generator->end(); j++)
     627             :     {
     628           0 :       lps::state destination = j->target_state();
     629           0 :       if (m_use_confluence_reduction)
     630             :       {
     631           0 :         destination = get_prioritised_representative(destination);
     632             :       }
     633           0 :       if (destination == *i)
     634             :       {
     635           0 :         trace.addAction(j->action());
     636           0 :         found=true;
     637           0 :         break;
     638             :       }
     639             :     }
     640           0 :     if (not found)
     641             :     {
     642           0 :       throw mcrl2::runtime_error(std::string("Fail to save a trace. Most likely due to the use of binders (forall, exists, lambda, Set, Map) in a state vector.\n") +
     643           0 :                                  "Problematic state (" + pp(*i) + ")");
     644             :     }
     645           0 :     enumeration_queue.clear();
     646           0 :     state = *i;
     647           0 :     trace.setState(state);
     648             :   }
     649             : 
     650           0 : }
     651             : 
     652             : // Contruct a trace to state1 and store in in filename.
     653           0 : bool lps2lts_algorithm::save_trace(const lps::state& state1, const std::string& filename)
     654             : {
     655           0 :   mcrl2::trace::Trace trace;
     656           0 :   lps2lts_algorithm::construct_trace(state1, trace);
     657           0 :   m_traces_saved++;
     658             : 
     659             :   try
     660             :   {
     661           0 :     trace.save(filename);
     662           0 :     return true;
     663             :   }
     664           0 :   catch(...)
     665             :   {
     666           0 :     return false;
     667             :   }
     668             : }
     669             : 
     670             : // Contruct a trace to state1, then add transition to it and store in in filename.
     671           0 : bool lps2lts_algorithm::save_trace(const lps::state& state1,
     672             :                                    const next_state_generator::transition_t& transition,
     673             :                                    const std::string& filename)
     674             : {
     675           0 :   mcrl2::trace::Trace trace;
     676           0 :   lps2lts_algorithm::construct_trace(state1, trace);
     677           0 :   trace.addAction(transition.action());
     678           0 :   trace.setState(transition.target_state());
     679           0 :   m_traces_saved++;
     680             : 
     681             :   try
     682             :   {
     683           0 :     trace.save(filename);
     684           0 :     return true;
     685             :   }
     686           0 :   catch(...)
     687             :   {
     688           0 :     return false;
     689             :   }
     690             : }
     691             : 
     692             : template <class COUNTER_EXAMPLE_GENERATOR>
     693           0 : bool lps2lts_algorithm::search_divergence(
     694             :               const mcrl2::lts::detail::state_index_pair<COUNTER_EXAMPLE_GENERATOR>& state_pair,
     695             :               std::set<lps::state>& current_path,
     696             :               std::set<lps::state>& visited,
     697             :               COUNTER_EXAMPLE_GENERATOR& divergence_loop)
     698             : {
     699           0 :   current_path.insert(state_pair.state());
     700           0 :   std::vector<mcrl2::lts::detail::state_index_pair<COUNTER_EXAMPLE_GENERATOR> > new_states;
     701           0 :   next_state_generator::enumerator_queue_t enumeration_queue;
     702           0 :   for (next_state_generator::iterator j = m_generator->begin(state_pair.state(), m_tau_summands, &enumeration_queue); j != m_generator->end(); j++)
     703             :   {
     704           0 :     assert(is_hidden_summand(j->action().actions(),m_options.actions_internal_for_divergencies));
     705             : 
     706           0 :     std::pair<std::size_t, bool> action_label_number = m_action_label_numbers.put(j->action());
     707           0 :     if (action_label_number.second)
     708             :     {
     709           0 :       assert(j->action().actions().size() != 0);
     710           0 :       std::size_t action_number = m_output_lts.add_action(action_label_lts(j->action()));
     711           0 :       assert(action_number == action_label_number.first);
     712             :       static_cast <void>(action_number); // Avoid a warning when compiling in non debug mode.
     713             :     }
     714             : 
     715           0 :     if (non_divergent_states.count(j->target_state())==0) // This state is not shown to be non convergent. So, an investigation is in order.
     716             :     {
     717           0 :       typename COUNTER_EXAMPLE_GENERATOR::index_type i=divergence_loop.add_transition(action_label_number.first,state_pair.index());
     718           0 :       if (visited.insert(j->target_state()).second)
     719             :       {
     720           0 :         new_states.push_back(mcrl2::lts::detail::state_index_pair<COUNTER_EXAMPLE_GENERATOR>(j->target_state(),i));
     721             :       }
     722           0 :       else if (current_path.count(j->target_state()) != 0)
     723             :       {
     724           0 :         mCRL2log(info) << "divergence-detect: divergence found." << std::endl;
     725           0 :         divergence_loop.save_counter_example(i,m_output_lts);
     726           0 :         return true;
     727             :       }
     728             :     }
     729             :   }
     730             : 
     731           0 :   for (const mcrl2::lts::detail::state_index_pair<COUNTER_EXAMPLE_GENERATOR>& p: new_states)
     732             :   {
     733           0 :     if (search_divergence(p, current_path, visited,divergence_loop))
     734             :     {
     735           0 :       return true;
     736             :     }
     737             :   }
     738             : 
     739           0 :   assert(current_path.count(state_pair.state())==1);
     740           0 :   current_path.erase(state_pair.state());
     741           0 :   return false;
     742             : }
     743             : 
     744             : template <class COUNTER_EXAMPLE_GENERATOR>
     745           0 : void lps2lts_algorithm::check_divergence(
     746             :               const mcrl2::lts::detail::state_index_pair<COUNTER_EXAMPLE_GENERATOR>& state_pair,
     747             :               COUNTER_EXAMPLE_GENERATOR divergence_loop)
     748             : {
     749           0 :   std::set<lps::state> visited;
     750           0 :   std::set<lps::state> current_path;
     751           0 :   visited.insert(state_pair.state());
     752             : 
     753           0 :   if (search_divergence(state_pair, current_path, visited,divergence_loop))
     754             :   {
     755           0 :     if (m_options.trace && m_traces_saved < m_options.max_traces)
     756             :     {
     757           0 :       std::string filename = m_options.trace_prefix + "_divergence_" + std::to_string(m_traces_saved) + ".trc";
     758           0 :       if (save_trace(state_pair.state(), filename))
     759             :       {
     760           0 :         mCRL2log(info) << "Trace to the divergencing state is saved to '" << filename << std::endl;
     761             :       }
     762             :       else
     763             :       {
     764           0 :         mCRL2log(info) << "Failed to save trace to diverging state to the file " << filename << "." << std::endl;
     765             :       }
     766             :     }
     767           0 :     std::size_t state_number = m_state_numbers.index(state_pair.state());
     768           0 :     mCRL2log(info) << "State index of diverging state is " << state_number << "." << std::endl;
     769             :   }
     770             :   else
     771             :   {
     772             :     // No divergence has been found. Register all states as being non divergent.
     773           0 :     for(const lps::state& s: visited)
     774             :     {
     775           0 :       assert(non_divergent_states.count(s)==0);
     776           0 :       non_divergent_states.insert(s);
     777             :     }
     778             :   }
     779           0 : }
     780             : 
     781           0 : void lps2lts_algorithm::save_actions(const lps::state& state, const next_state_generator::transition_t& transition)
     782             : {
     783           0 :   std::size_t state_number = m_state_numbers.index(state);
     784           0 :   mCRL2log(info) << "Detected action '" << pp(transition.action()) << "' (state index " << state_number << ")";
     785           0 :   if (m_options.trace && m_traces_saved < m_options.max_traces)
     786             :   {
     787           0 :     std::string filename = m_options.trace_prefix + "_act_" + std::to_string(m_traces_saved);
     788           0 :     if (m_options.trace_multiactions.find(transition.action()) != m_options.trace_multiactions.end())
     789             :     {
     790           0 :       filename = filename + "_" + pp(transition.action());
     791             :     }
     792           0 :     for (const process::action& a: transition.action().actions())
     793             :     {
     794           0 :       if (m_options.trace_actions.count(a.label().name()) > 0)
     795             :       {
     796           0 :         filename = filename + "_" + core::pp(a.label().name());
     797             :       }
     798             :     }
     799           0 :     filename = filename + ".trc";
     800           0 :     if (save_trace(state, transition, filename))
     801             :     {
     802           0 :       mCRL2log(info) << " and saved to '" << filename << "'";
     803             :     }
     804             :     else
     805             :     {
     806           0 :       mCRL2log(info) << " but it could not saved to '" << filename << "'";
     807             :     }
     808             :   }
     809           0 :   mCRL2log(info) << std::endl;
     810           0 : }
     811             : 
     812           0 : void lps2lts_algorithm::save_nondeterministic_state(const lps::state& state,
     813             :                                                     const next_state_generator::transition_t& nondeterminist_transition)
     814             : {
     815           0 :   std::size_t state_number = m_state_numbers.index(state);
     816           0 :   if (m_options.trace && m_traces_saved < m_options.max_traces)
     817             :   {
     818           0 :     std::string filename = m_options.trace_prefix + "_nondeterministic_" + std::to_string(m_traces_saved) + ".trc";
     819           0 :     if (save_trace(state, nondeterminist_transition, filename))
     820             :     {
     821           0 :       mCRL2log(info) << "Nondeterministic state found and saved to '" << filename
     822           0 :                      << "' (state index: " << state_number << ").\n";
     823             :     }
     824             :     else
     825             :     {
     826           0 :       mCRL2log(info) << "Nondeterministic state found, but its trace could not be saved to '" << filename
     827           0 :                      << "' (state index: " << state_number << ").\n";
     828           0 :     }
     829             :   }
     830             :   else
     831             :   {
     832           0 :     mCRL2log(info) << "Nondeterministic state found (state index: " << state_number <<  ").\n";
     833             :   }
     834           0 : }
     835             : 
     836           0 : void lps2lts_algorithm::save_deadlock(const lps::state& state)
     837             : {
     838           0 :   std::size_t state_number = m_state_numbers.index(state);
     839           0 :   if (m_options.trace && m_traces_saved < m_options.max_traces)
     840             :   {
     841           0 :     std::string filename = m_options.trace_prefix + "_dlk_" + std::to_string(m_traces_saved) + ".trc";
     842           0 :     if (save_trace(state, filename))
     843             :     {
     844           0 :       mCRL2log(info) << "deadlock-detect: deadlock found and saved to '" << filename
     845           0 :                      << "' (state index: " << state_number << ").\n";
     846             :     }
     847             :     else
     848             :     {
     849           0 :       mCRL2log(info) << "deadlock-detect: deadlock found, but its trace could not be saved to '" << filename
     850           0 :                      << "' (state index: " << state_number << ").\n";
     851           0 :     }
     852             :   }
     853             :   else
     854             :   {
     855           0 :     mCRL2log(info) << "deadlock-detect: deadlock found (state index: " << state_number <<  ").\n";
     856             :   }
     857           0 : }
     858             : 
     859           0 : void lps2lts_algorithm::save_error(const lps::state& state)
     860             : {
     861           0 :   if (m_options.save_error_trace)
     862             :   {
     863           0 :     std::string filename = m_options.trace_prefix + "_error.trc";
     864           0 :     if (save_trace(state, filename))
     865             :     {
     866           0 :       mCRL2log(verbose) << "saved trace to error in '" << filename << "'.\n";
     867             :     }
     868             :     else
     869             :     {
     870           0 :       mCRL2log(verbose) << "trace to error could not be saved in '" << filename << "'.\n";
     871             :     }
     872             :   }
     873           0 : }
     874             : 
     875        2819 : std::pair<std::size_t, bool> lps2lts_algorithm::get_state_number(const lps::state& target_state)
     876             : {
     877        2819 :   if (m_options.bithashing)
     878             :   {
     879           0 :     return m_bit_hash_table.add_state(target_state);
     880             :   }
     881             :   else
     882             :   {
     883        2819 :     return m_state_numbers.insert(target_state);
     884             :   }
     885             : }
     886             : 
     887             : // Add the target state to the transition system, and if necessary store it to be investigated later.
     888             : // Return the number of the target state.
     889        2819 : std::size_t lps2lts_algorithm::add_target_state(
     890             :                                      const lps::state& source_state, 
     891             :                                      const lps::state& target_state,
     892             :                                      const std::function<void(const lps::state&)> add_state_to_todo_queue_function)
     893             : {
     894        2819 :   std::pair<std::size_t, bool> destination_state_number=get_state_number(target_state);;
     895        2819 :   if (destination_state_number.second) // The state is new.
     896             :   {
     897        1139 :     add_state_to_todo_queue_function(target_state);
     898        1139 :     m_num_states++;
     899        1139 :     if (m_maintain_traces)
     900             :     {
     901           0 :       assert(m_backpointers.count(target_state) == 0);
     902           0 :       m_backpointers[target_state] = source_state;
     903             :     }
     904             : 
     905        1139 :     if (m_options.outformat != lts_none && m_options.outformat != lts_aut)
     906             :     {
     907         740 :       assert(!m_options.bithashing);
     908         740 :       m_output_lts.add_state(state_label_lts(target_state));
     909             :     }
     910             :   }
     911        2819 :   return destination_state_number.first;
     912             : }
     913             : 
     914        1015 : void lps2lts_algorithm::print_target_distribution_in_aut_format(
     915             :                const lps::next_state_generator::transition_t::state_probability_list& state_probability_list,
     916             :                const std::size_t last_state_number,
     917             :                const lps::state& source_state,
     918             :                const std::function<void(const lps::state&)> add_state_to_todo_queue_function)
     919             : {
     920          60 :   for(lps::next_state_generator::transition_t::state_probability_list::const_iterator
     921        1015 :                         i=state_probability_list.begin();
     922        1075 :                         i!=state_probability_list.end(); ++i)
     923             :   {
     924          60 :     if (m_options.outformat == lts_aut)
     925             :     {
     926         120 :       const lps::state probability_destination = i->state();
     927          60 :       const std::size_t probability_destination_state_number=add_target_state(source_state,probability_destination,add_state_to_todo_queue_function);
     928          60 :       if (is_application(i->probability()) && atermpp::down_cast<data::application>(i->probability()).head().size()!=3)
     929             :       {
     930           0 :         if (m_options.outformat == lts_aut)
     931             :         {
     932           0 :           m_aut_file.flush();
     933             :         }
     934           0 :         throw mcrl2::runtime_error("The probability " + data::pp(i->probability()) + " is not a proper rational number.");
     935             :       }
     936          60 :       const data::application& prob=atermpp::down_cast<data::application>(i->probability());
     937          60 :       if (prob.head()!=data::sort_real::creal())
     938             :       {
     939           0 :         throw mcrl2::runtime_error("Probability is not a closed expression with a proper enumerator and denominator: " + pp(i->probability()) + ".");
     940             :       }
     941          60 :       m_aut_file << probability_destination_state_number << " " << (prob[0]) << "/"
     942          60 :                                                                 << (prob[1]) << " ";
     943             :     }
     944             :   }
     945        1015 :   m_aut_file << last_state_number;
     946        1015 : }
     947             : 
     948         142 : void lps2lts_algorithm::print_target_distribution_in_aut_format(
     949             :                 const lps::next_state_generator::transition_t::state_probability_list& state_probability_list,
     950             :                 const lps::state& source_state,
     951             :                 const std::function<void(const lps::state&)> add_state_to_todo_queue_function)
     952             : {
     953         142 :   assert(!state_probability_list.empty());
     954             :   const std::size_t a_destination_state_number=
     955         142 :                 add_target_state(source_state,state_probability_list.front().state(), add_state_to_todo_queue_function);
     956             : 
     957         284 :   lps::next_state_generator::transition_t::state_probability_list temporary_list=state_probability_list;
     958         142 :   temporary_list.pop_front();
     959         142 :   print_target_distribution_in_aut_format(temporary_list, a_destination_state_number, source_state, add_state_to_todo_queue_function);
     960         142 : }
     961             : 
     962             : 
     963        2513 : void lps2lts_algorithm::add_transition(const lps::state& source_state, 
     964             :                                        const next_state_generator::transition_t& transition,
     965             :                                        const std::function<void(const lps::state&)> add_state_to_todo_queue_function
     966             :                                       )
     967             : {
     968             :   std::size_t source_state_number;
     969        2513 :   if (m_options.bithashing)
     970             :   {
     971           0 :     source_state_number = m_bit_hash_table.add_state(source_state).first;
     972             :   }
     973             :   else
     974             :   {
     975        2513 :     source_state_number = m_state_numbers.index(source_state);
     976             :   }
     977             : 
     978        2513 :   const lps::state& destination = transition.target_state();
     979        2513 :   const std::size_t destination_state_number=add_target_state(source_state,destination,add_state_to_todo_queue_function);
     980             : 
     981        2513 :   if (m_options.detect_action && m_detected_action_summands[transition.summand_index()])
     982             :   {
     983           0 :     save_actions(source_state, transition);
     984             :   }
     985             : 
     986        2513 :   if (m_options.outformat == lts_aut || m_options.outformat == lts_none)
     987             :   {
     988             : 
     989         873 :     if (m_options.outformat == lts_aut)
     990             :     {
     991         873 :       m_aut_file << "(" << source_state_number << ",\"" << lps::pp(transition.action()) << "\",";
     992             :     }
     993             : 
     994         873 :     print_target_distribution_in_aut_format(transition.other_target_states(),destination_state_number, source_state, add_state_to_todo_queue_function);
     995             : 
     996             :     // Close transition.
     997        1746 :     if (m_options.outformat == lts_aut)
     998             :     {
     999         873 :       m_aut_file << ")\n"; // Intentionally do not use std::endl to avoid flushing.
    1000             :     }
    1001             :   }
    1002             :   else
    1003             :   {
    1004        1640 :     std::pair<std::size_t, bool> action_label_number = m_action_label_numbers.put(transition.action());
    1005        1640 :     if (action_label_number.second)
    1006             :     {
    1007         900 :       assert(transition.action().actions().size() != 0);
    1008         900 :       std::size_t action_number = m_output_lts.add_action(action_label_lts(transition.action()));
    1009         900 :       assert(action_number == action_label_number.first);
    1010             :       static_cast <void>(action_number); // Avoid a warning when compiling in non debug mode.
    1011             :     }
    1012        1640 :     std::size_t number_of_a_new_probabilistic_state=m_output_lts.add_probabilistic_state(
    1013        3280 :                                     create_a_probabilistic_state_from_target_distribution(
    1014             :                                                destination_state_number,
    1015             :                                                transition.other_target_states(),
    1016             :                                                source_state,
    1017        1640 :                                                add_state_to_todo_queue_function)); // Add a new probabilistic state.
    1018        1640 :     m_output_lts.add_transition(mcrl2::lts::transition(source_state_number, action_label_number.first, number_of_a_new_probabilistic_state));
    1019             :   }
    1020             : 
    1021        2513 :   m_num_transitions++;
    1022             : 
    1023        2513 :   for (std::set<lps::multi_action>::const_iterator ma = m_options.trace_multiactions.begin(); ma != m_options.trace_multiactions.end(); ++ma)
    1024             :   {
    1025           0 :     if (*ma == transition.action())
    1026             :     {
    1027           0 :       save_actions(source_state, transition);
    1028             :     }
    1029             :   }
    1030        2513 : }
    1031             : 
    1032             : // The function below checks whether in the set of outgoing transitions,
    1033             : // there are two transitions with the same label, going to different states.
    1034             : // If this is the case, true is delivered and one nondeterministic transition
    1035             : // is returned in the variable nondeterministic_transition.
    1036           0 : bool lps2lts_algorithm::is_nondeterministic(std::vector<lps2lts_algorithm::next_state_generator::transition_t>& transitions,
    1037             :                                             lps2lts_algorithm::next_state_generator::transition_t& nondeterministic_transition)
    1038             : {
    1039             :   // Below a mapping from transition labels to target states is made.
    1040           0 :   static std::map<lps::multi_action, lps::state> sorted_transitions; // The set is static to avoid repeated construction.
    1041           0 :   assert(sorted_transitions.empty());
    1042           0 :   for(const lps2lts_algorithm::next_state_generator::transition_t& t: transitions)
    1043             :   {
    1044           0 :     const std::map<lps::multi_action, lps::state>::const_iterator i=sorted_transitions.find(t.action());
    1045           0 :     if (i!=sorted_transitions.end())
    1046             :     {
    1047           0 :       if (i->second!=t.target_state())
    1048             :       {
    1049             :         // Two transitions with the same label and different targets states have been found. This state is nondeterministic.
    1050           0 :         sorted_transitions.clear();
    1051           0 :         nondeterministic_transition=t;
    1052           0 :         return true;
    1053             :       }
    1054             :     }
    1055             :     else
    1056             :     {
    1057           0 :       sorted_transitions[t.action()]=t.target_state();
    1058             :     }
    1059             :   }
    1060           0 :   sorted_transitions.clear();
    1061           0 :   return false;
    1062             : }
    1063             : 
    1064        1337 : void lps2lts_algorithm::get_transitions(const lps::state& state,
    1065             :                                         std::vector<lps2lts_algorithm::next_state_generator::transition_t>& transitions,
    1066             :                                         next_state_generator::enumerator_queue_t& enumeration_queue
    1067             :                                        )
    1068             : {
    1069        1337 :   bool structured_output = false;
    1070        1337 :   assert(transitions.empty());
    1071        1337 :   if (m_options.detect_divergence)
    1072             :   {
    1073           0 :     if (non_divergent_states.count(state)==0)  // This state was not already investigated earlier.
    1074           0 :     { if (m_options.trace)
    1075             :       {
    1076             :         // Onderstaande string generatie kan duur uitpakken.
    1077           0 :         std::string filename_divergence_loop = m_options.trace_prefix + "_divergence_loop" + std::to_string(m_traces_saved);
    1078           0 :         check_divergence<detail::counter_example_constructor>(
    1079           0 :                 detail::state_index_pair<detail::counter_example_constructor>(state,detail::counter_example_constructor::root_index()),
    1080           0 :                 detail::counter_example_constructor(filename_divergence_loop, structured_output));
    1081             :       }
    1082             :       else
    1083             :       {
    1084           0 :         check_divergence(
    1085           0 :                 detail::state_index_pair<detail::dummy_counter_example_constructor>(state,detail::dummy_counter_example_constructor::root_index()),
    1086             :                 detail::dummy_counter_example_constructor());
    1087             :       }
    1088             :     }
    1089             :   }
    1090             : 
    1091             :   try
    1092             :   {
    1093        1337 :     enumeration_queue.clear();
    1094        2674 :     next_state_generator::iterator it(m_generator->begin(state, *m_main_subset, &enumeration_queue));
    1095        6363 :     while (it)
    1096             :     {
    1097        2513 :       transitions.push_back(*it++);
    1098             :     }
    1099             :   }
    1100           0 :   catch (mcrl2::runtime_error& e)
    1101             :   {
    1102           0 :     mCRL2log(error) << "Error while exploring state space: " << e.what() << "\n";
    1103           0 :     save_error(state);
    1104           0 :     if (m_options.outformat == lts_aut)
    1105             :     {
    1106           0 :       m_aut_file.flush();
    1107             :     }
    1108           0 :     exit(EXIT_FAILURE);
    1109             :   }
    1110             : 
    1111        1337 :   if (m_value_prioritize)
    1112             :   {
    1113           0 :     value_prioritize(transitions);
    1114             :   }
    1115        1337 :   if (m_options.detect_deadlock && transitions.empty())
    1116             :   {
    1117           0 :     save_deadlock(state);
    1118             :   }
    1119             : 
    1120        1337 :   if (m_options.detect_nondeterminism)
    1121           0 :   { lps2lts_algorithm::next_state_generator::transition_t nondeterministic_transition;
    1122           0 :     if (is_nondeterministic(transitions, nondeterministic_transition))
    1123             :     {
    1124             :       // save the trace to the nondeterministic state and one transition to indicate
    1125             :       // which transition is nondeterministic.
    1126           0 :       save_nondeterministic_state(state, nondeterministic_transition);
    1127             :     }
    1128             :   }
    1129             : 
    1130        1337 :   if (m_use_confluence_reduction)
    1131             :   {
    1132        1026 :     for (std::vector<next_state_generator::transition_t>::iterator i = transitions.begin(); i != transitions.end(); i++)
    1133             :     {
    1134         564 :       i->set_target_state(get_prioritised_representative(i->target_state()));
    1135             :     }
    1136             :   }
    1137        1337 : }
    1138             : 
    1139         100 : void lps2lts_algorithm::generate_lts_breadth_todo_max_is_npos(const next_state_generator::transition_t::state_probability_list& initial_states)
    1140             : {
    1141         100 :   assert(m_options.todo_max==std::string::npos);
    1142         100 :   std::size_t current_state = 0;
    1143         100 :   std::size_t start_level_seen = 1;
    1144         100 :   std::size_t start_level_transitions = 0;
    1145         200 :   std::vector<next_state_generator::transition_t> transitions;
    1146         100 :   time_t last_log_time = time(nullptr) - 1, new_log_time;
    1147         200 :   next_state_generator::enumerator_queue_t enumeration_queue;
    1148             :   (void)initial_states; // suppress unused variable warning. 
    1149             : 
    1150        2957 :   while (!m_must_abort && (current_state < m_state_numbers.size()) &&
    1151        2168 :          (current_state < m_options.max_states) && (!m_options.trace || m_traces_saved < m_options.max_traces))
    1152             :   {
    1153        1378 :     lps::state state=m_state_numbers[current_state];
    1154         689 :     get_transitions(state,transitions,enumeration_queue);
    1155        1972 :     for (const next_state_generator::transition_t& t: transitions)
    1156             :     {
    1157        1867 :       add_transition(state, t, [](const lps::state&){});
    1158             :     }
    1159         689 :     transitions.clear();
    1160             : 
    1161         689 :     current_state++;
    1162         689 :     if (current_state == start_level_seen)
    1163             :     {
    1164         287 :       mCRL2log(debug) << "Number of states at level " << m_level << " is " << m_num_states - start_level_seen << "\n";
    1165         287 :       m_level++;
    1166         287 :       start_level_seen = m_num_states;
    1167         287 :       start_level_transitions = m_num_transitions;
    1168             :     }
    1169             : 
    1170         689 :     if (!m_options.suppress_progress_messages && time(&new_log_time) > last_log_time)
    1171             :     {
    1172         114 :       last_log_time = new_log_time;
    1173         114 :       std::size_t lvl_states = m_num_states - start_level_seen;
    1174         114 :       std::size_t lvl_transitions = m_num_transitions - start_level_transitions;
    1175         114 :       mCRL2log(status) << std::fixed << std::setprecision(2)
    1176           0 :                        << m_num_states << "st, " << m_num_transitions << "tr"
    1177           0 :                        << ", explored " << 100.0 * ((float)current_state / m_num_states)
    1178           0 :                        << "%. Last level: " << m_level << ", " << lvl_states << "st, " << lvl_transitions
    1179           0 :                        << "tr.\n";
    1180             :     }
    1181             :   }
    1182             : 
    1183         100 :   if (current_state == m_options.max_states)
    1184             :   {
    1185           1 :     mCRL2log(verbose) << "explored the maximum number (" << m_options.max_states << ") of states, terminating." << std::endl;
    1186             :   }
    1187         100 : }
    1188             : 
    1189           0 : void lps2lts_algorithm::generate_lts_breadth_todo_max_is_not_npos(const next_state_generator::transition_t::state_probability_list& initial_states)
    1190             : {
    1191           0 :   assert(m_options.todo_max!=std::string::npos);
    1192           0 :   std::size_t current_state = 0;
    1193           0 :   std::size_t start_level_seen = 1;
    1194           0 :   std::size_t start_level_explored = 0;
    1195           0 :   std::size_t start_level_transitions = 0;
    1196           0 :   time_t last_log_time = time(nullptr) - 1, new_log_time;
    1197             : 
    1198           0 :   queue<lps::state> state_queue;
    1199           0 :   state_queue.set_max_size(m_options.max_states < m_options.todo_max ? m_options.max_states : m_options.todo_max);
    1200           0 :   for(next_state_generator::transition_t::state_probability_list::const_iterator i=initial_states.begin(); i!=initial_states.end(); ++i)
    1201             :   {
    1202           0 :     state_queue.add_to_queue(i->state());
    1203             :   }
    1204           0 :   state_queue.swap_queues();
    1205           0 :   std::vector<next_state_generator::transition_t> transitions;
    1206           0 :   next_state_generator::enumerator_queue_t enumeration_queue;
    1207             : 
    1208           0 :   while (!m_must_abort && (state_queue.remaining() > 0) &&
    1209           0 :          (current_state < m_options.max_states) && (!m_options.trace || m_traces_saved < m_options.max_traces))
    1210             :   {
    1211           0 :     const lps::state state=state_queue.get_from_queue();
    1212           0 :     get_transitions(state,transitions, enumeration_queue);
    1213             : 
    1214           0 :     for (std::vector<next_state_generator::transition_t>::iterator i = transitions.begin(); i != transitions.end(); i++)
    1215             :     {
    1216           0 :       add_transition(state, *i, [&state_queue](const lps::state& s){ state_queue.add_to_queue(s);});
    1217             :     }
    1218           0 :     transitions.clear();
    1219             : 
    1220           0 :     current_state++;
    1221           0 :     if (state_queue.remaining() == 0)
    1222             :     {
    1223           0 :       state_queue.swap_queues();
    1224             : 
    1225           0 :       if (!m_options.suppress_progress_messages)
    1226             :       {
    1227           0 :         mCRL2log(verbose) << "monitor: level " << m_level << " done."
    1228           0 :                           << " (" << (current_state - start_level_explored) << " state"
    1229           0 :                           << ((current_state - start_level_explored)==1?"":"s") << ", "
    1230           0 :                           << (m_num_transitions - start_level_transitions) << " transition"
    1231           0 :                           << ((m_num_transitions - start_level_transitions)==1?")\n":"s)\n");
    1232             :       }
    1233             : 
    1234           0 :       m_level++;
    1235           0 :       start_level_seen = m_num_states;
    1236           0 :       start_level_explored = current_state;
    1237           0 :       start_level_transitions = m_num_transitions;
    1238             :     }
    1239             : 
    1240           0 :     if (!m_options.suppress_progress_messages && time(&new_log_time) > last_log_time)
    1241             :     {
    1242           0 :       last_log_time = new_log_time;
    1243           0 :       std::size_t lvl_states = m_num_states - start_level_seen;
    1244           0 :       std::size_t lvl_transitions = m_num_transitions - start_level_transitions;
    1245           0 :       mCRL2log(status) << std::fixed << std::setprecision(2)
    1246           0 :                        << m_num_states << "st, " << m_num_transitions << "tr"
    1247           0 :                        << ", explored " << 100.0 * ((float)current_state / m_num_states)
    1248           0 :                        << "%. Last level: " << m_level << ", " << lvl_states << "st, " << lvl_transitions
    1249           0 :                        << "tr.\n";
    1250             :     }
    1251             :   }
    1252             : 
    1253           0 :   if (current_state == m_options.max_states)
    1254             :   {
    1255           0 :     mCRL2log(verbose) << "explored the maximum number (" << m_options.max_states << ") of states, terminating." << std::endl;
    1256             :   }
    1257           0 : }
    1258             : 
    1259           0 : void lps2lts_algorithm::generate_lts_breadth_bithashing(const next_state_generator::transition_t::state_probability_list& initial_states)
    1260             : {
    1261           0 :   std::size_t current_state = 0;
    1262             : 
    1263           0 :   std::size_t start_level_seen = 1;
    1264           0 :   std::size_t start_level_explored = 0;
    1265           0 :   std::size_t start_level_transitions = 0;
    1266             : 
    1267           0 :   queue<lps::state> state_queue;
    1268           0 :   state_queue.set_max_size(m_options.max_states < m_options.todo_max ? m_options.max_states : m_options.todo_max);
    1269           0 :   for(next_state_generator::transition_t::state_probability_list::const_iterator i=initial_states.begin(); i!=initial_states.end(); ++i)
    1270             :   {
    1271           0 :     state_queue.add_to_queue(i->state());
    1272             :   }
    1273           0 :   state_queue.swap_queues();
    1274           0 :   std::vector<next_state_generator::transition_t> transitions;
    1275           0 :   next_state_generator::enumerator_queue_t enumeration_queue;
    1276             : 
    1277           0 :   while (!m_must_abort && (state_queue.remaining() > 0) && (current_state < m_options.max_states) && (!m_options.trace || m_traces_saved < m_options.max_traces))
    1278             :   {
    1279           0 :     const lps::state state=state_queue.get_from_queue();
    1280           0 :     get_transitions(state,transitions, enumeration_queue);
    1281             : 
    1282           0 :     for (std::vector<next_state_generator::transition_t>::iterator i = transitions.begin(); i != transitions.end(); i++)
    1283             :     {
    1284             :       // It can be that a state is dropped in the queue, as the queue reached its todo-limit.
    1285             :       // This is ignored in combination with bithashing. So, there might be states with outgoing
    1286             :       // transitions of which the outgoing transitions are not investigated.
    1287           0 :       add_transition(state, *i, [&state_queue](const lps::state& s){ state_queue.add_to_queue(s); });
    1288             : 
    1289             :       // if (add_transition(state, *i))
    1290             :       // {
    1291             :       //   // It can be that a state is dropped in the queue, as the queue reached its todo-limit.
    1292             :       //   // This is ignored in combination with bithashing. So, there might be states with outgoing
    1293             :       //   // transitions of which the outgoing transitions are not investigated.
    1294             :       //   state_queue.add_to_queue(i->target_state());
    1295             :       // }
    1296             :     }
    1297           0 :     transitions.clear();
    1298             : 
    1299           0 :     if (state_queue.remaining() == 0)
    1300             :     {
    1301           0 :       state_queue.swap_queues();
    1302             :     }
    1303             : 
    1304           0 :     current_state++;
    1305           0 :     if (!m_options.suppress_progress_messages && ((current_state % 1000) == 0))
    1306             :     {
    1307           0 :       mCRL2log(status) << "monitor: currently at level " << m_level << " with "
    1308           0 :                         << current_state << " state" << ((current_state==1)?"":"s") << " and "
    1309           0 :                         << m_num_transitions << " transition" << ((m_num_transitions==1)?"":"s")
    1310           0 :                         << " explored and " << m_num_states << " state" << ((m_num_states==1)?"":"s") << " seen." << std::endl;
    1311             :     }
    1312             : 
    1313           0 :     if (current_state == start_level_seen)
    1314             :     {
    1315           0 :       if (!m_options.suppress_progress_messages)
    1316             :       {
    1317           0 :         mCRL2log(verbose) << "monitor: level " << m_level << " done."
    1318           0 :                           << " (" << (current_state - start_level_explored) << " state"
    1319           0 :                           << ((current_state - start_level_explored)==1?"":"s") << ", "
    1320           0 :                           << (m_num_transitions - start_level_transitions) << " transition"
    1321           0 :                           << ((m_num_transitions - start_level_transitions)==1?")\n":"s)\n");
    1322             :       }
    1323             : 
    1324           0 :       m_level++;
    1325           0 :       start_level_seen = m_num_states;
    1326           0 :       start_level_explored = current_state;
    1327           0 :       start_level_transitions = m_num_transitions;
    1328             :     }
    1329             :   }
    1330             : 
    1331           0 :   if (current_state == m_options.max_states)
    1332             :   {
    1333           0 :     mCRL2log(verbose) << "explored the maximum number (" << m_options.max_states << ") of states, terminating." << std::endl;
    1334             :   }
    1335           0 : }
    1336             : 
    1337          87 : void lps2lts_algorithm::generate_lts_depth(const next_state_generator::transition_t::state_probability_list& initial_states)
    1338             : {
    1339         174 :   std::list<lps::state> stack;
    1340         180 :   for(next_state_generator::transition_t::state_probability_list::const_iterator i=initial_states.begin(); i!=initial_states.end(); ++i)
    1341             :   {
    1342          93 :     stack.push_back(i->state());
    1343             :   }
    1344         174 :   std::vector<next_state_generator::transition_t> transitions;
    1345             : 
    1346          87 :   std::size_t current_state = 0;
    1347         174 :   next_state_generator::enumerator_queue_t enumeration_queue;
    1348             : 
    1349        1383 :   while (!m_must_abort && (!stack.empty()) && (!m_options.trace || m_traces_saved < m_options.max_traces))
    1350             :   {
    1351        1296 :     const lps::state state=stack.back();
    1352         648 :     stack.pop_back();
    1353         648 :     get_transitions(state,transitions, enumeration_queue);
    1354             : 
    1355        1878 :     for (std::vector<next_state_generator::transition_t>::iterator i = transitions.begin(); i != transitions.end(); i++)
    1356             :     {
    1357        1230 :       add_transition(state, *i, 
    1358         555 :           [&](const lps::state& s)
    1359         555 :              { if ((current_state + stack.size() < m_options.max_states) && (stack.size() < m_options.todo_max))
    1360             :                {  
    1361         555 :                  stack.push_back(s);
    1362             :                }
    1363         555 :              });
    1364             :       // if (add_transition(state, *i) && (current_state + stack.size() < m_options.max_states) && (stack.size() < m_options.todo_max))
    1365             :       // {
    1366             :       //  stack.push_back(i->target_state());
    1367             :       // }
    1368             :     }
    1369         648 :     transitions.clear();
    1370             : 
    1371         648 :     current_state++;
    1372         648 :     if (!m_options.suppress_progress_messages && ((current_state % 1000) == 0))
    1373             :     {
    1374           0 :       mCRL2log(verbose) << "monitor: currently explored "
    1375           0 :                         << current_state << " state" << ((current_state==1)?"":"s")
    1376           0 :                         << " and " << m_num_transitions << " transition" << ((m_num_transitions==1)?"":"s")
    1377           0 :                         << " (stacksize is " << stack.size() << ")" << std::endl;
    1378             :     }
    1379             :   }
    1380             : 
    1381          87 :   if (current_state == m_options.max_states)
    1382             :   {
    1383           0 :     mCRL2log(verbose) << "explored the maximum number (" << m_options.max_states << ") of states, terminating." << std::endl;
    1384             :   }
    1385          87 : }
    1386             : 
    1387           0 : void lps2lts_algorithm::generate_lts_random(const next_state_generator::transition_t::state_probability_list& initial_states)
    1388             : {
    1389           0 :   if (++initial_states.begin()!=initial_states.end())  // There is more than one element in the set of initial states.
    1390             :   {
    1391           0 :     mCRL2log(warning) << "The initial state is not selected at random, conform its distribution. One specific state is chosen.";
    1392             :   }
    1393           0 :   lps::state state = initial_states.front().state();
    1394             : 
    1395           0 :   std::vector<next_state_generator::transition_t> transitions;
    1396           0 :   std::size_t current_state = 0;
    1397           0 :   next_state_generator::enumerator_queue_t enumeration_queue;
    1398             : 
    1399           0 :   while (!m_must_abort && current_state < m_options.max_states && (!m_options.trace || m_traces_saved < m_options.max_traces))
    1400             :   {
    1401           0 :     get_transitions(state,transitions, enumeration_queue);
    1402             : 
    1403           0 :     if (transitions.empty())
    1404             :     {
    1405           0 :       break;
    1406             :     }
    1407             : 
    1408           0 :     std::size_t index = rand() % transitions.size();
    1409           0 :     lps::state new_state;
    1410             : 
    1411           0 :     for (std::vector<next_state_generator::transition_t>::iterator i = transitions.begin(); i != transitions.end(); i++)
    1412             :     {
    1413             :       // Only the first state of a probabilistic state is randomly chosen. Not all states are considered. 
    1414           0 :       add_transition(state, *i, [](const lps::state& ){});
    1415             : 
    1416           0 :       if (index-- == 0)
    1417             :       {
    1418           0 :         new_state = i->target_state();
    1419             :       }
    1420             :     }
    1421           0 :     transitions.clear();
    1422             : 
    1423           0 :     state = new_state;
    1424             : 
    1425           0 :     current_state++;
    1426           0 :     if (!m_options.suppress_progress_messages && ((current_state % 1000) == 0))
    1427             :     {
    1428           0 :       mCRL2log(verbose) << "monitor: currently explored "
    1429           0 :                         << m_num_transitions << " transition" << ((m_num_transitions==1)?"":"s")
    1430           0 :                         << " and encountered " << m_num_states << " unique state" << ((m_num_states==1)?"":"s") << std::endl;
    1431             :     }
    1432             :   }
    1433             : 
    1434           0 :   if (current_state == m_options.max_states)
    1435             :   {
    1436           0 :     mCRL2log(verbose) << "explored the maximum number (" << m_options.max_states << ") of states, terminating." << std::endl;
    1437             :   }
    1438          21 : }

Generated by: LCOV version 1.13