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

Generated by: LCOV version 1.12