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

Generated by: LCOV version 1.12