LCOV - code coverage report
Current view: top level - lts/include/mcrl2/lts - lts_algorithm.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 248 300 82.7 %
Date: 2019-09-14 00:54:39 Functions: 9 9 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Muck van Weerdenburg, Jan Friso Groote
       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             : 
      10             : /** \file
      11             :  *
      12             :  * \brief Algorithms for LTS, such as equivalence reductions, determinisation, etc.
      13             :  * \details This contains the main algorithms useful to manipulate with
      14             :  * labelled transition systems. Typically, it contains algorithms for bisimulation
      15             :  * reduction, removal of tau loops, making an lts deterministic etc.
      16             :  * \author Jan Friso Groote, Bas Ploeger, Muck van Weerdenburg
      17             :  */
      18             : 
      19             : #ifndef MCRL2_LTS_LTS_ALGORITHM_H
      20             : #define MCRL2_LTS_LTS_ALGORITHM_H
      21             : 
      22             : #include <string>
      23             : #include <vector>
      24             : #include <stack>
      25             : #include <algorithm>
      26             : #include <iostream>
      27             : #include <cstdio>
      28             : #include <cstdlib>
      29             : #include <functional>
      30             : #include "mcrl2/utilities/logger.h"
      31             : #include "mcrl2/lts/lts.h"
      32             : #include "mcrl2/lts/detail/liblts_merge.h"
      33             : #include "mcrl2/lts/lts_utilities.h"
      34             : #include "mcrl2/lts/detail/liblts_bisim.h"
      35             : #include "mcrl2/lts/detail/liblts_bisim_gjkw.h"
      36             : #include "mcrl2/lts/detail/liblts_bisim_dnj.h"
      37             : #include "mcrl2/lts/detail/liblts_weak_bisim.h"
      38             : #include "mcrl2/lts/detail/liblts_add_an_action_loop.h"
      39             : #include "mcrl2/lts/detail/liblts_scc.h"
      40             : #include "mcrl2/lts/detail/liblts_sim.h"
      41             : #include "mcrl2/lts/detail/liblts_ready_sim.h"
      42             : #include "mcrl2/lts/detail/liblts_failures_refinement.h"
      43             : #include "mcrl2/lts/detail/liblts_tau_star_reduce.h"
      44             : #include "mcrl2/utilities/exception.h"
      45             : #include "mcrl2/lts/detail/tree_set.h"
      46             : #include "mcrl2/lts/lts_equivalence.h"
      47             : #include "mcrl2/lts/lts_preorder.h"
      48             : #include "mcrl2/lts/sigref.h"
      49             : 
      50             : namespace mcrl2
      51             : {
      52             : namespace lts
      53             : {
      54             : 
      55             : /** \brief Applies a reduction algorithm to this LTS.
      56             :  * \param[in] l A labelled transition system that must be reduced.
      57             :  * \param[in] eq The equivalence with respect to which the LTS will be
      58             :  * reduced.
      59             :  **/
      60             : template <class LTS_TYPE>
      61             : void reduce(LTS_TYPE& l, lts_equivalence eq);
      62             : 
      63             : /** \brief Checks whether this LTS is equivalent to another LTS.
      64             :  * \param[in] l1 The first LTS that will be compared.
      65             :  * \param[in] l2 The second LTS that will be compared.
      66             :  * \param[in] eq The equivalence with respect to which the LTSs will be
      67             :  * compared.
      68             :  * \param[in] generate_counter_examples
      69             :  * \retval true if the LTSs are found to be equivalent.
      70             :  * \retval false otherwise.
      71             :  * \warning This function alters the internal data structure of
      72             :  * both LTSs for efficiency reasons. After comparison, this LTS is
      73             :  * equivalent to the original LTS by equivalence \a eq, and
      74             :  * similarly for the LTS \a l.
      75             :  */
      76             : template <class LTS_TYPE>
      77          50 : bool destructive_compare(LTS_TYPE& l1,
      78             :                          LTS_TYPE& l2,
      79             :                          const lts_equivalence eq,
      80             :                          const bool generate_counter_examples = false)
      81             : {
      82             :   // Merge this LTS and l and store the result in this LTS.
      83             :   // In the resulting LTS, the initial state i of l will have the
      84             :   // state number i + N where N is the number of states in this
      85             :   // LTS (before the merge).
      86             : 
      87          50 :   switch (eq)
      88             :   {
      89             :     case lts_eq_none:
      90           0 :       return false;
      91             :     case lts_eq_bisim:
      92             :     {
      93          15 :       if (generate_counter_examples)
      94             :       {
      95           1 :         mCRL2log(mcrl2::log::warning) << "The default bisimulation comparison algorithm cannot generate counter examples. Therefore the slower gv algorithm is used instead.\n";
      96           1 :         return detail::destructive_bisimulation_compare(l1,l2, false,false,generate_counter_examples);
      97             :       }
      98          14 :       return detail::destructive_bisimulation_compare_dnj(l1,l2, false,false,generate_counter_examples);
      99             :     }
     100             :     case lts_eq_bisim_gv:
     101             :     {
     102           2 :       return detail::destructive_bisimulation_compare(l1,l2, false,false,generate_counter_examples);
     103             :     }
     104             :     case lts_eq_bisim_gjkw:
     105             :     {
     106           2 :       return detail::destructive_bisimulation_compare_gjkw(l1,l2, false,false,generate_counter_examples);
     107             :     }
     108             :     case lts_eq_branching_bisim:
     109             :     {
     110           0 :       if (generate_counter_examples)
     111             :       {
     112           0 :         mCRL2log(mcrl2::log::warning) << "The default branching bisimulation comparison algorithm cannot generate counter examples. Therefore the slower gv algorithm is used instead.\n";
     113           0 :         return detail::destructive_bisimulation_compare(l1,l2, true,false,generate_counter_examples);
     114             :       }
     115           0 :       return detail::destructive_bisimulation_compare_dnj(l1,l2, true,false,generate_counter_examples);
     116             :     }
     117             :     case lts_eq_branching_bisim_gv:
     118             :     {
     119           0 :       return detail::destructive_bisimulation_compare(l1,l2, true,false,generate_counter_examples);
     120             :     }
     121             :     case lts_eq_branching_bisim_gjkw:
     122             :     {
     123           0 :       return detail::destructive_bisimulation_compare_gjkw(l1,l2, true,false,generate_counter_examples);
     124             :     }
     125             :     case lts_eq_divergence_preserving_branching_bisim:
     126             :     {
     127           0 :       if (generate_counter_examples)
     128             :       {
     129           0 :         mCRL2log(mcrl2::log::warning) << "The default divergence-preserving branching bisimulation comparison algorithm cannot generate counter examples. Therefore the slower gv algorithm is used instead.\n";
     130           0 :         return detail::destructive_bisimulation_compare(l1,l2, true,true,generate_counter_examples);
     131             :       }
     132           0 :       return detail::destructive_bisimulation_compare_dnj(l1,l2, true,true,generate_counter_examples);
     133             :     }
     134             :     case lts_eq_divergence_preserving_branching_bisim_gv:
     135             :     {
     136           0 :       return detail::destructive_bisimulation_compare(l1,l2, true,true,generate_counter_examples);
     137             :     }
     138             :     case lts_eq_divergence_preserving_branching_bisim_gjkw:
     139             :     {
     140           0 :       return detail::destructive_bisimulation_compare_gjkw(l1,l2, true,true,generate_counter_examples);
     141             :     }
     142             :     case lts_eq_weak_bisim:
     143             :     {
     144           0 :       if (generate_counter_examples)
     145             :       {
     146           0 :         mCRL2log(log::warning) << "Cannot generate counter example traces for weak bisimulation\n";
     147             :       }
     148           0 :       return detail::destructive_weak_bisimulation_compare(l1,l2,false);
     149             :     }
     150             :     case lts_eq_divergence_preserving_weak_bisim:
     151             :     {
     152           0 :       if (generate_counter_examples)
     153             :       {
     154           0 :         mCRL2log(log::warning) << "Cannot generate counter example traces for for divergence-preserving weak bisimulation\n";
     155             :       }
     156           0 :       return detail::destructive_weak_bisimulation_compare(l1,l2, true);
     157             :     }
     158             :     case lts_eq_sim:
     159             :     {
     160           9 :       if (generate_counter_examples)
     161             :       {
     162           0 :         mCRL2log(log::warning) << "Cannot generate counter example traces for simulation equivalence\n";
     163             :       }
     164             :       // Run the partitioning algorithm on this merged LTS
     165           9 :       std::size_t init_l2 = l2.initial_state() + l1.num_states();
     166           9 :       detail::merge(l1,l2);
     167           9 :       l2.clear(); // l2 is not needed anymore.
     168          18 :       detail::sim_partitioner<LTS_TYPE> sp(l1);
     169           9 :       sp.partitioning_algorithm();
     170             : 
     171           9 :       return sp.in_same_class(l1.initial_state(),init_l2);
     172             :     }
     173             :     case lts_eq_ready_sim:
     174             :     {
     175           7 :       if (generate_counter_examples)
     176             :       {
     177           0 :         mCRL2log(log::warning) << "Cannot generate counter example traces for ready-simulation equivalence\n";
     178             :       }
     179             :       // Run the partitioning algorithm on this merged LTS
     180           7 :       std::size_t init_l2 = l2.initial_state() + l1.num_states();
     181           7 :       detail::merge(l1,l2);
     182           7 :       l2.clear(); // l2 is not needed anymore.
     183          14 :       detail::ready_sim_partitioner<LTS_TYPE> rsp(l1);
     184           7 :       rsp.partitioning_algorithm();
     185             : 
     186           7 :       return rsp.in_same_class(l1.initial_state(),init_l2);
     187             :     }
     188             :     case lts_eq_trace:
     189             :     {
     190             :       // Determinise first LTS
     191           9 :       detail::bisimulation_reduce(l1,false);
     192           9 :       determinise(l1);
     193             : 
     194             :       // Determinise second LTS
     195           9 :       detail::bisimulation_reduce(l2,false);
     196           9 :       determinise(l2);
     197             : 
     198             :       // Trace equivalence now corresponds to bisimilarity
     199           9 :       return detail::destructive_bisimulation_compare(l1,l2,false,false,generate_counter_examples);
     200             :     }
     201             :     case lts_eq_weak_trace:
     202             :     {
     203             :       // Eliminate silent steps and determinise first LTS
     204           6 :       detail::bisimulation_reduce(l1,true,false);
     205           6 :       detail::tau_star_reduce(l1);
     206           6 :       detail::bisimulation_reduce(l1,false);
     207           6 :       determinise(l1);
     208             : 
     209             :       // Eliminate silent steps and determinise second LTS
     210           6 :       detail::bisimulation_reduce(l2,true,false);
     211           6 :       detail::tau_star_reduce(l2);
     212           6 :       detail::bisimulation_reduce(l2,false);
     213           6 :       determinise(l2);
     214             : 
     215             :       // Weak trace equivalence now corresponds to bisimilarity
     216           6 :       return detail::destructive_bisimulation_compare(l1,l2,false,false,generate_counter_examples);
     217             :     }
     218             :     default:
     219           0 :     throw mcrl2::runtime_error("Comparison for this equivalence is not available");
     220             :     return false;
     221             :   }
     222             : }
     223             : 
     224             : /** \brief Checks whether this LTS is equivalent to another LTS.
     225             :  * \details The input labelled transition systems are duplicated in memory to carry
     226             :  *          out the comparison. When space efficiency is a concern, one can consider
     227             :  *          to use destructive_compare.
     228             :  * \param[in] l1 The first LTS to compare.
     229             :  * \param[in] l2 The second LTS to compare.
     230             :  * \param[in] eq The equivalence with respect to which the LTSs will be
     231             :  * compared.
     232             :  * \param[in] generate_counter_examples If true counter examples are written to file.
     233             :  * \retval true if the LTSs are found to be equivalent.
     234             :  * \retval false otherwise.
     235             :  */
     236             : template <class LTS_TYPE>
     237             : bool compare(const LTS_TYPE& l1,
     238             :              const LTS_TYPE& l2,
     239             :              const lts_equivalence eq,
     240             :              const bool generate_counter_examples = false);
     241             : 
     242             : /** \brief Checks whether this LTS is smaller than another LTS according
     243             :  * to a preorder.
     244             :  * \param[in] l1 The first LTS to be compared.
     245             :  * \param[in] l2 The second LTS to be compared.
     246             :  * \param[in] pre The preorder with respect to which the LTSs will be
     247             :  * compared.
     248             :  * \param[in] generate_counter_example Indicates whether a file containing a counter example is
     249             :  *            generated when the comparison fails.
     250             :  * \param[in] strategy Choose breadth-first or depth-first for exploration strategy
     251             :  *            of the antichain algorithms.
     252             :  * \param[in] preprocess Whether to allow preprocessing of the given LTSs.
     253             :  * \retval true if LTS \a l1 is smaller than LTS \a l2 according to
     254             :  * preorder \a pre.
     255             :  * \retval false otherwise.
     256             :  * \warning This function alters the internal data structure of
     257             :  * both LTSs for efficiency reasons. After comparison, this LTS is
     258             :  * equivalent to the original LTS by equivalence \a eq, and
     259             :  * similarly for the LTS \a l, where \a eq is the equivalence
     260             :  * induced by the preorder \a pre (i.e. \f$eq = pre \cap
     261             :  * pre^{-1}\f$).
     262             :  */
     263             : template <class LTS_TYPE >
     264             : bool destructive_compare(LTS_TYPE& l1,
     265             :                          LTS_TYPE& l2,
     266             :                          const lts_preorder pre,
     267             :                          const bool generate_counter_example,
     268             :                          const lps::exploration_strategy strategy = lps::es_breadth,
     269             :                          const bool preprocess = true);
     270             : 
     271             : /** \brief Checks whether this LTS is smaller than another LTS according
     272             :  * to a preorder.
     273             :  * \param[in] l1 The first LTS to be compared.
     274             :  * \param[in] l2 The second LTS to be compared.
     275             :  * \param[in] pre The preorder with respect to which the LTSs will be compared.
     276             :  * \param[in] generate_counter_example Indicates whether a file containing a counter example is
     277             :  *            generated when the comparison fails.
     278             :  * \param[in] strategy Choose breadth-first or depth-first for exploration strategy
     279             :  *            of the antichain algorithms.
     280             :  * \param[in] preprocess Whether to allow preprocessing of the given LTSs.
     281             :  * \retval true if this LTS is smaller than LTS \a l according to
     282             :  * preorder \a pre.
     283             :  * \retval false otherwise.
     284             :  */
     285             : template <class  LTS_TYPE >
     286             : bool compare(const LTS_TYPE&  l1,
     287             :              const  LTS_TYPE& l2,
     288             :              const lts_preorder pre,
     289             :              const bool generate_counter_example,
     290             :              const lps::exploration_strategy strategy = lps::es_breadth,
     291             :              const bool preprocess = true);
     292             : 
     293             : /** \brief Determinises this LTS. */
     294             : template <class LTS_TYPE>
     295             : void determinise(LTS_TYPE& l);
     296             : 
     297             : 
     298             : /** \brief Checks whether all states in this LTS are reachable
     299             :  * from the initial state and remove unreachable states if required.
     300             :  * \details Runs in O(num_states * num_transitions) time.
     301             :  * \param[in] l The LTS on which reachability is checked.
     302             :  * \param[in] remove_unreachable Indicates whether all unreachable states
     303             :  *            should be removed from the LTS. This option does not
     304             :  *            influence the return value; the return value is with
     305             :  *            respect to the original LTS.
     306             :  * \retval true if all states are reachable from the initial state;
     307             :  * \retval false otherwise. */
     308             : template <class SL, class AL, class BASE>
     309          39 : bool reachability_check(lts < SL, AL, BASE>& l, bool remove_unreachable = false)
     310             : {
     311             :   // First calculate which states can be reached, and store this in the array visited.
     312          78 :   const outgoing_transitions_per_state_t out_trans(l.get_transitions(),l.num_states(),true);
     313             : 
     314          78 :   std::vector < bool > visited(l.num_states(),false);
     315          78 :   std::stack<std::size_t> todo;
     316             : 
     317          39 :   visited[l.initial_state()]=true;
     318          39 :   todo.push(l.initial_state());
     319             : 
     320         389 :   while (!todo.empty())
     321             :   {
     322         175 :     std::size_t state_to_consider=todo.top();
     323         175 :     todo.pop();
     324             :     // for (const outgoing_pair_t& p: out_trans[state_to_consider])
     325         398 :     for (detail::state_type i=out_trans.lowerbound(state_to_consider); i<out_trans.upperbound(state_to_consider); ++i)
     326             :     {
     327         223 :       const outgoing_pair_t& p=out_trans.get_transitions()[i];
     328         223 :       assert(visited[state_to_consider] && state_to_consider<l.num_states() && to(p)<l.num_states());
     329         223 :       if (!visited[to(p)])
     330             :       {
     331         136 :         visited[to(p)]=true;
     332         136 :         todo.push(to(p));
     333             :       }
     334             :     }
     335             :   }
     336             : 
     337             :   // Property: in_visited(s) == true: state s is reachable from the initial state
     338             : 
     339             :   // check to see if all states are reachable from the initial state, i.e.
     340             :   // whether all bits are set.
     341          39 :   bool all_reachable = find(visited.begin(),visited.end(),false)==visited.end();
     342             : 
     343          39 :   if (!all_reachable && remove_unreachable)
     344             :   {
     345             :     // Remove all unreachable states, transitions from such states and labels
     346             :     // that are only used in these transitions.
     347             : 
     348          14 :     std::vector < detail::state_type > state_map(l.num_states());
     349          14 :     std::vector < detail::state_type > label_map(l.num_action_labels());
     350             : 
     351          14 :     lts < SL, AL, BASE> new_lts=l; // In this way set data specification and action declarations in the new lts.
     352           7 :     new_lts.clear();
     353             : 
     354           7 :     std::size_t new_nstates = 0;
     355          56 :     for (std::size_t i=0; i<l.num_states(); i++)
     356             :     {
     357          49 :       if (visited[i])
     358             :       {
     359          34 :         state_map[i] = new_nstates;
     360          34 :         if (l.has_state_info())
     361             :         {
     362           0 :           new_lts.add_state(l.state_label(i));
     363             :         }
     364             :         else
     365             :         {
     366          34 :           new_lts.add_state();
     367             :         }
     368          34 :         new_nstates++;
     369             :       }
     370             :     }
     371             : 
     372          83 :     for (const transition& t: l.get_transitions())
     373             :     {
     374          76 :       if (visited[t.from()])
     375             :       {
     376          58 :         label_map[t.label()] = 1;
     377             :       }
     378             :     }
     379             : 
     380           7 :     label_map[0]=1; // Declare the tau action explicitly present.
     381           7 :     std::size_t new_nlabels = 0;
     382          41 :     for (std::size_t i=0; i<l.num_action_labels(); i++)
     383             :     {
     384          34 :       if (label_map[i]>0)   // Label i is used.
     385             :       {
     386          33 :         label_map[i] = new_nlabels;
     387          33 :         new_lts.add_action(l.action_label(i));
     388          33 :         new_nlabels++;
     389             :       }
     390             :     }
     391             : 
     392          83 :     for (const transition& t: l.get_transitions())
     393             :     {
     394          76 :       if (visited[t.from()])
     395             :       {
     396          58 :         new_lts.add_transition(transition(state_map[t.from()],label_map[t.label()],state_map[t.to()]));
     397             :       }
     398             :     }
     399             : 
     400           7 :     new_lts.set_initial_state(state_map.at(l.initial_state()));
     401           7 :     l.swap(new_lts);
     402             :   }
     403             : 
     404          78 :   return all_reachable;
     405             : }
     406             : 
     407             : /** \brief Checks whether all states in a probabilistic LTS are reachable
     408             :  * from the initial state and remove unreachable states if required.
     409             :  * \details Runs in O(num_states * num_transitions) time.
     410             :  * \param[in] l The LTS on which reachability is checked.
     411             :  * \param[in] remove_unreachable Indicates whether all unreachable states
     412             :  *            should be removed from the LTS. This option does not
     413             :  *            influence the return value; the return value is with
     414             :  *            respect to the original LTS.
     415             :  * \retval true if all states are reachable from the initial state;
     416             :  * \retval false otherwise. */
     417             : template <class SL, class AL, class PROBABILISTIC_STATE, class BASE>
     418             : bool reachability_check(probabilistic_lts < SL, AL, PROBABILISTIC_STATE, BASE>&  l, bool remove_unreachable = false)
     419             : {
     420             :   // First calculate which states can be reached, and store this in the array visited.
     421             :   const outgoing_transitions_per_state_t out_trans(l.get_transitions(),l.num_states(),true);
     422             : 
     423             :   std::vector < bool > visited(l.num_states(),false);
     424             :   std::stack<std::size_t> todo;
     425             : 
     426             :   for(const typename PROBABILISTIC_STATE::state_probability_pair& s: l.initial_probabilistic_state())
     427             :   {
     428             :     visited[s.state()]=true;
     429             :     todo.push(s.state());
     430             :   }
     431             : 
     432             :   while (!todo.empty())
     433             :   {
     434             :     std::size_t state_to_consider=todo.top();
     435             :     todo.pop();
     436             :     // for (const outgoing_pair_t& p: out_trans[state_to_consider])
     437             :     for (detail::state_type i=out_trans.lowerbound(state_to_consider); i<out_trans.upperbound(state_to_consider); ++i)
     438             :     {
     439             :       const outgoing_pair_t& p=out_trans.get_transitions()[i];
     440             :       assert(visited[state_to_consider] && state_to_consider<l.num_states() && to(p)<l.num_probabilistic_states());
     441             :       // Walk through the the states in this probabilistic state.
     442             :       for(const typename PROBABILISTIC_STATE::state_probability_pair& pr: l.probabilistic_state(to(p)))
     443             :       {
     444             :         if (!visited[pr.state()])
     445             :         {
     446             :           visited[pr.state()]=true;
     447             :           todo.push(pr.state());
     448             :         }
     449             :       }
     450             :     }
     451             :   }
     452             : 
     453             :   // Property: in_visited(s) == true: state s is reachable from the initial state
     454             : 
     455             :   // check to see if all states are reachable from the initial state, i.e.
     456             :   // whether all bits are set.
     457             :   bool all_reachable = find(visited.begin(),visited.end(),false)==visited.end();
     458             : 
     459             :   if (!all_reachable && remove_unreachable)
     460             :   {
     461             :     // Remove all unreachable states, transitions from such states and labels
     462             :     // that are only used in these transitions.
     463             : 
     464             :     std::vector < detail::state_type > state_map(l.num_states());
     465             :     std::vector < detail::state_type > label_map(l.num_action_labels());
     466             : 
     467             :     probabilistic_lts < SL, AL, PROBABILISTIC_STATE, BASE> new_lts=l; // In this way set data specification and action declarations in the new lts.
     468             :     new_lts.clear();
     469             : 
     470             :     std::size_t new_nstates = 0;
     471             :     for (std::size_t i=0; i<l.num_states(); i++)
     472             :     {
     473             :       if (visited[i])
     474             :       {
     475             :         state_map[i] = new_nstates;
     476             :         if (l.has_state_info())
     477             :         {
     478             :           new_lts.add_state(l.state_label(i));
     479             :         }
     480             :         else
     481             :         {
     482             :           new_lts.add_state();
     483             :         }
     484             :         new_nstates++;
     485             :       }
     486             :     }
     487             : 
     488             :     for (const transition& t: l.get_transitions())
     489             :     {
     490             :       if (visited[t.from()])
     491             :       {
     492             :         label_map[t.label()] = 1;
     493             :       }
     494             :     }
     495             : 
     496             :     label_map[0]=1; // Declare the tau action explicitly present.
     497             :     std::size_t new_nlabels = 0;
     498             :     for (std::size_t i=0; i<l.num_action_labels(); i++)
     499             :     {
     500             :       if (label_map[i]>0)   // Label i is used.
     501             :       {
     502             :         label_map[i] = new_nlabels;
     503             :         new_lts.add_action(l.action_label(i));
     504             :         new_nlabels++;
     505             :       }
     506             :     }
     507             : 
     508             :     for (const transition& t: l.get_transitions())
     509             :     {
     510             :       if (visited[t.from()])
     511             :       {
     512             :         new_lts.add_transition(transition(state_map[t.from()],label_map[t.label()],t.to()));
     513             :       }
     514             :     }
     515             : 
     516             :     PROBABILISTIC_STATE new_initial_state;
     517             :     for(const typename PROBABILISTIC_STATE::state_probability_pair& s: l.initial_probabilistic_state())
     518             :     {
     519             :       new_initial_state.add(state_map[s.state()], s.probability());
     520             :     }
     521             :     new_lts.set_initial_probabilistic_state(new_initial_state);
     522             :     l.swap(new_lts);
     523             :   }
     524             : 
     525             :   return all_reachable;
     526             : }
     527             : 
     528             : /** \brief Checks whether this LTS is deterministic.
     529             :  * \retval true if this LTS is deterministic;
     530             :  * \retval false otherwise. */
     531             : template <class LTS_TYPE>
     532             : bool is_deterministic(const LTS_TYPE& l);
     533             : 
     534             : /** \brief Merge the second lts into the first lts.
     535             :     \param[in,out] l1 The transition system in which l2 is merged.
     536             :     \param[in] l2 The second transition system, which remains unchanged
     537             :  */
     538             : template <class LTS_TYPE>
     539             : void merge(LTS_TYPE& l1, const LTS_TYPE& l2)
     540             : {
     541             :   detail::merge(l1,l2);
     542             : }
     543             : 
     544             : 
     545             : /* Here the implementations of the declared functions above are given.
     546             :    Originally these were in a .cpp file, before lts's were templated  */
     547             : 
     548             : 
     549             : 
     550             : template <class LTS_TYPE>
     551         272 : void reduce(LTS_TYPE& l,lts_equivalence eq)
     552             : {
     553             : 
     554         272 :   switch (eq)
     555             :   {
     556             :     case lts_eq_none:
     557           5 :       return;
     558             :     case lts_eq_bisim:
     559             :     {
     560          19 :       detail::bisimulation_reduce_dnj(l,false,false);
     561          19 :       return;
     562             :     }
     563             :     case lts_eq_bisim_gv:
     564             :     {
     565          19 :       detail::bisimulation_reduce(l,false,false);
     566          19 :       return;
     567             :     }
     568             :     case lts_eq_bisim_gjkw:
     569             :     {
     570          19 :       detail::bisimulation_reduce_gjkw(l,false,false);
     571          19 :       return;
     572             :     }
     573             :     case lts_eq_bisim_sigref:
     574             :     {
     575          38 :       sigref<LTS_TYPE, signature_bisim<LTS_TYPE> > s(l);
     576          19 :       s.run();
     577          19 :       return;
     578             :     }
     579             :     case lts_eq_branching_bisim:
     580             :     {
     581          20 :       detail::bisimulation_reduce_dnj(l,true,false);
     582          20 :       return;
     583             :     }
     584             :     case lts_eq_branching_bisim_gv:
     585             :     {
     586          20 :       detail::bisimulation_reduce(l,true,false);
     587          20 :       return;
     588             :     }
     589             :     case lts_eq_branching_bisim_gjkw:
     590             :     {
     591          19 :       detail::bisimulation_reduce_gjkw(l,true,false);
     592          19 :       return;
     593             :     }
     594             :     case lts_eq_branching_bisim_sigref:
     595             :     {
     596          38 :       sigref<LTS_TYPE, signature_branching_bisim<LTS_TYPE> > s(l);
     597          19 :       s.run();
     598          19 :       return;
     599             :     }
     600             :     case lts_eq_divergence_preserving_branching_bisim:
     601             :     {
     602          15 :       detail::bisimulation_reduce_dnj(l,true,true);
     603          15 :       return;
     604             :     }
     605             :     case lts_eq_divergence_preserving_branching_bisim_gv:
     606             :     {
     607          15 :       detail::bisimulation_reduce(l,true,true);
     608          15 :       return;
     609             :     }
     610             :     case lts_eq_divergence_preserving_branching_bisim_gjkw:
     611             :     {
     612          15 :       detail::bisimulation_reduce_gjkw(l,true,true);
     613          15 :       return;
     614             :     }
     615             :     case lts_eq_divergence_preserving_branching_bisim_sigref:
     616             :     {
     617          30 :       sigref<LTS_TYPE, signature_divergence_preserving_branching_bisim<LTS_TYPE> > s(l);
     618          15 :       s.run();
     619          15 :       return;
     620             :     }
     621             :     case lts_eq_weak_bisim:
     622             :     {
     623          17 :       detail::weak_bisimulation_reduce(l,false);
     624          17 :       return;
     625             :     }
     626             :     /*
     627             :     case lts_eq_weak_bisim_sigref:
     628             :     {
     629             :      {
     630             :       sigref<LTS_TYPE, signature_branching_bisim<LTS_TYPE> > s1(l);
     631             :       s1.run();
     632             :      }
     633             :       detail::reflexive_transitive_tau_closure(l);
     634             :      {
     635             :       sigref<LTS_TYPE, signature_bisim<LTS_TYPE> > s2(l);
     636             :       s2.run();
     637             :      }
     638             :       scc_reduce(l); // Remove tau loops
     639             :       return;
     640             :     }
     641             :     */
     642             :     case lts_eq_divergence_preserving_weak_bisim:
     643             :     {
     644          14 :       detail::weak_bisimulation_reduce(l,true);
     645          14 :       return;
     646             :     }
     647             :     /*
     648             :     case lts_eq_divergence_preserving_weak_bisim_sigref:
     649             :     {
     650             :      {
     651             :       sigref<LTS_TYPE, signature_divergence_preserving_branching_bisim<LTS_TYPE> > s1(l);
     652             :       s1.run();
     653             :      }
     654             :       std::size_t divergence_label=detail::mark_explicit_divergence_transitions(l);
     655             :       detail::reflexive_transitive_tau_closure(l);
     656             :      {
     657             :       sigref<LTS_TYPE, signature_bisim<LTS_TYPE> > s2(l);
     658             :       s2.run();
     659             :      }
     660             :       scc_reduce(l); // Remove tau loops
     661             :       detail::unmark_explicit_divergence_transitions(l,divergence_label);
     662             :       return;
     663             :     }
     664             :     */
     665             :     case lts_eq_sim:
     666             :     {
     667             :       // Run the partitioning algorithm on this LTS
     668          10 :       detail::sim_partitioner<LTS_TYPE> sp(l);
     669           5 :       sp.partitioning_algorithm();
     670             : 
     671             :       // Clear this LTS, but keep the labels
     672             :       // l.clear_type();
     673           5 :       l.clear_state_labels();
     674           5 :       l.clear_transitions();
     675             : 
     676             :       // Assign the reduced LTS
     677           5 :       l.set_num_states(sp.num_eq_classes());
     678           5 :       l.set_initial_state(sp.get_eq_class(l.initial_state()));
     679             : 
     680          10 :       const std::vector <transition> trans=sp.get_transitions();
     681           5 :       l.clear_transitions();
     682          88 :       for (std::vector <transition>::const_iterator i=trans.begin(); i!=trans.end(); ++i)
     683             :       {
     684          83 :         l.add_transition(*i);
     685             :       }
     686             :       // Remove unreachable parts
     687             : 
     688           5 :       reachability_check(l,true);
     689             : 
     690           5 :       return;
     691             :     }
     692             :     case lts_eq_ready_sim:
     693             :     {
     694             :       // Run the partitioning algorithm on this LTS
     695           0 :       detail::ready_sim_partitioner<LTS_TYPE> rsp(l);
     696           0 :       rsp.partitioning_algorithm();
     697             : 
     698             :       // Clear this LTS, but keep the labels
     699             :       // l.clear_type();
     700           0 :       l.clear_state_labels();
     701           0 :       l.clear_transitions();
     702             : 
     703             :       // Assign the reduced LTS
     704           0 :       l.set_num_states(rsp.num_eq_classes());
     705           0 :       l.set_initial_state(rsp.get_eq_class(l.initial_state()));
     706             : 
     707           0 :       const std::vector <transition> trans=rsp.get_transitions();
     708           0 :       l.clear_transitions();
     709           0 :       for (std::vector <transition>::const_iterator i=trans.begin(); i!=trans.end(); ++i)
     710             :       {
     711           0 :         l.add_transition(*i);
     712             :       }
     713             :       // Remove unreachable parts
     714             : 
     715           0 :       reachability_check(l,true);
     716             : 
     717           0 :       return;
     718             :     }
     719             :     case lts_eq_trace:
     720           5 :       detail::bisimulation_reduce(l,false);
     721           5 :       determinise(l);
     722           5 :       detail::bisimulation_reduce(l,false);
     723           5 :       return;
     724             :     case lts_eq_weak_trace:
     725             :     {
     726           5 :       detail::bisimulation_reduce(l,true,false);
     727           5 :       detail::tau_star_reduce(l);
     728           5 :       detail::bisimulation_reduce(l,false);
     729           5 :       determinise(l);
     730           5 :       detail::bisimulation_reduce(l,false);
     731           5 :       return;
     732             :     }
     733             :     case lts_red_tau_star:
     734             :     {
     735           2 :       detail::bisimulation_reduce(l,true,false);
     736           2 :       detail::tau_star_reduce(l);
     737           2 :       detail::bisimulation_reduce(l,false);
     738           2 :       return;
     739             :     }
     740             :     case lts_red_determinisation:
     741             :     {
     742           5 :       determinise(l);
     743           5 :       return;
     744             :     }
     745             :     default:
     746           0 :       throw mcrl2::runtime_error("Unknown reduction method.");
     747             :   }
     748             : }
     749             : 
     750             : template <class LTS_TYPE>
     751          50 : bool compare(const LTS_TYPE& l1, const LTS_TYPE& l2, const lts_equivalence eq, const bool generate_counter_examples)
     752             : {
     753          50 :   switch (eq)
     754             :   {
     755             :     case lts_eq_none:
     756           0 :       return false;
     757             :     default:
     758         100 :       LTS_TYPE l1_copy(l1);
     759         100 :       LTS_TYPE l2_copy(l2);
     760          50 :       return destructive_compare(l1_copy,l2_copy,eq,generate_counter_examples);
     761             :   }
     762             :   return false;
     763             : }
     764             : 
     765             : template <class LTS_TYPE>
     766          89 : bool compare(const LTS_TYPE& l1, const LTS_TYPE& l2, const lts_preorder pre, const bool generate_counter_example, const lps::exploration_strategy strategy, const bool preprocess)
     767             : {
     768         178 :   LTS_TYPE l1_copy(l1);
     769         178 :   LTS_TYPE l2_copy(l2);
     770         178 :   return destructive_compare(l1_copy, l2_copy, pre, generate_counter_example, strategy, preprocess);
     771             : }
     772             : 
     773             : template <class LTS_TYPE>
     774         110 : bool destructive_compare(LTS_TYPE& l1, LTS_TYPE& l2, const lts_preorder pre, const bool generate_counter_example, const lps::exploration_strategy strategy, const bool preprocess)
     775             : {
     776         110 :   switch (pre)
     777             :   {
     778             :     case lts_pre_sim:
     779             :     {
     780             :       // Merge this LTS and l and store the result in this LTS.
     781             :       // In the resulting LTS, the initial state i of l will have the
     782             :       // state number i + N where N is the number of states in this
     783             :       // LTS (before the merge).
     784          24 :       const std::size_t init_l2 = l2.initial_state() + l1.num_states();
     785          24 :       detail::merge(l1,l2);
     786             : 
     787             :       // We no longer need l, so clear it to save memory
     788          24 :       l2.clear();
     789             : 
     790             :       // Run the partitioning algorithm on this merged LTS
     791          48 :       detail::sim_partitioner<LTS_TYPE> sp(l1);
     792          24 :       sp.partitioning_algorithm();
     793             : 
     794          24 :       return sp.in_preorder(l1.initial_state(),init_l2);
     795             :     }
     796             :     case lts_pre_ready_sim:
     797             :     {
     798             :       // Merge this LTS and l and store the result in this LTS.
     799             :       // In the resulting LTS, the initial state i of l will have the
     800             :       // state number i + N where N is the number of states in this
     801             :       // LTS (before the merge).
     802           9 :       const std::size_t init_l2 = l2.initial_state() + l1.num_states();
     803           9 :       detail::merge(l1,l2);
     804             : 
     805             :       // We no longer need l, so clear it to save memory
     806           9 :       l2.clear();
     807             : 
     808             :       // Run the partitioning algorithm on this prepropcessed LTS
     809          18 :       detail::ready_sim_partitioner<LTS_TYPE> rsp(l1);
     810           9 :       rsp.partitioning_algorithm();
     811             : 
     812           9 :       return rsp.in_preorder(l1.initial_state(),init_l2);
     813             :     }
     814             :     case lts_pre_trace:
     815             :     {
     816             :       // Preprocessing: reduce modulo strong bisimulation equivalence.
     817             :       // This is not strictly necessary, but may reduce time/memory
     818             :       // needed for determinisation.
     819          15 :       detail::bisimulation_reduce(l1,false);
     820          15 :       detail::bisimulation_reduce(l2,false);
     821             : 
     822             :       // Determinise both LTSes. As postprocessing, reduce modulo
     823             :       // strong bisimulation equivalence. This is not strictly
     824             :       // necessary, but may reduce time/memory needed for simulation
     825             :       // preorder checking.
     826          15 :       determinise(l1);
     827          15 :       detail::bisimulation_reduce(l1,false);
     828             : 
     829          15 :       determinise(l2);
     830          15 :       detail::bisimulation_reduce(l2,false);
     831             : 
     832             :       // Trace preorder now corresponds to simulation preorder
     833          15 :       return destructive_compare(l1, l2, lts_pre_sim, generate_counter_example, strategy);
     834             :     }
     835             :     case lts_pre_weak_trace:
     836             :     {
     837             :       // Eliminate silent steps of first LTS
     838           6 :       detail::bisimulation_reduce(l1,true,false);
     839           6 :       detail::tau_star_reduce(l1);
     840             : 
     841             :       // Eliminate silent steps of second LTS
     842           6 :       detail::bisimulation_reduce(l2,true,false);
     843           6 :       detail::tau_star_reduce(l2);
     844             : 
     845             :       // Weak trace preorder now corresponds to strong trace preorder
     846           6 :       return destructive_compare(l1, l2, lts_pre_trace, generate_counter_example, strategy);
     847             :     }
     848             :     case lts_pre_trace_anti_chain:
     849             :     {
     850          10 :       if (generate_counter_example)
     851             :       {
     852           0 :         detail::counter_example_constructor cec("counter_example_trace_preorder.trc");
     853           0 :         return destructive_refinement_checker(l1, l2, trace, false, strategy, preprocess, cec);
     854             :       }
     855          10 :       return destructive_refinement_checker(l1, l2, trace, false, strategy, preprocess);
     856             :     }
     857             :     case lts_pre_weak_trace_anti_chain:
     858             :     {
     859           8 :       if (generate_counter_example)
     860             :       {
     861           0 :         detail::counter_example_constructor cec("counter_example_weak_trace_preorder.trc");
     862           0 :         return destructive_refinement_checker(l1, l2, trace, true, strategy, preprocess, cec);
     863             :       }
     864           8 :       return destructive_refinement_checker(l1, l2, trace, true, strategy, preprocess);
     865             :     }
     866             :     case lts_pre_failures_refinement:
     867             :     {
     868          17 :       if (generate_counter_example)
     869             :       {
     870           0 :         detail::counter_example_constructor cec("counter_example_failures_refinement.trc");
     871           0 :         return destructive_refinement_checker(l1, l2, failures, false, strategy, preprocess, cec);
     872             :       }
     873          17 :       return destructive_refinement_checker(l1, l2, failures, false, strategy, preprocess);
     874             :     }
     875             :     case lts_pre_weak_failures_refinement:
     876             :     {
     877           8 :       if (generate_counter_example)
     878             :       {
     879           0 :         detail::counter_example_constructor cec("counter_example_weak_failures_refinement.trc");
     880           0 :         return destructive_refinement_checker(l1, l2, failures, true, strategy, preprocess, cec);
     881             :       }
     882           8 :       return destructive_refinement_checker(l1, l2, failures, true, strategy, preprocess);
     883             :     }
     884             :     case lts_pre_failures_divergence_refinement:
     885             :     {
     886          13 :       if (generate_counter_example)
     887             :       {
     888           0 :         detail::counter_example_constructor cec("counter_example_failures_divergence_refinement.trc");
     889           0 :         return destructive_refinement_checker(l1, l2, failures_divergence, true, strategy, preprocess, cec);
     890             :       }
     891          13 :       return destructive_refinement_checker(l1, l2, failures_divergence, true, strategy, preprocess);
     892             :     }
     893             :     default:
     894           0 :       mCRL2log(log::error) << "Comparison for this preorder is not available\n";
     895           0 :       return false;
     896             :   }
     897             : }
     898             : 
     899             : 
     900             : template <class LTS_TYPE>
     901          87 : bool is_deterministic(const LTS_TYPE& l)
     902             : {
     903             :   outgoing_transitions_per_state_action_t trans_lut=
     904         174 :                   transitions_per_outgoing_state_action_pair(l.get_transitions(),l.hidden_label_map());
     905             : 
     906         714 :   for(outgoing_transitions_per_state_action_t::const_iterator i=trans_lut.begin(); i!=trans_lut.end(); ++i)
     907             :   {
     908         630 :     outgoing_transitions_per_state_action_t::const_iterator i_next=i;
     909         630 :     i_next++;
     910        1377 :     if (i_next!=trans_lut.end() &&
     911         546 :                   from(i)==from(i_next) &&
     912         197 :                   label(i)==label(i_next) &&
     913           4 :                   to(i)!=to(i_next))
     914             :     {
     915             :       // found a pair <s,l,t> and <s,l,t'> with t!=t', so l is not deterministic.
     916           3 :       return false;
     917             :     }
     918             :   }
     919          84 :   return true;
     920             : }
     921             : 
     922             : 
     923             : namespace detail
     924             : {
     925             : 
     926             : template <class LTS_TYPE>
     927         558 : void get_trans(const outgoing_transitions_per_state_t& begin,
     928             :                tree_set_store& tss,
     929             :                std::size_t d,
     930             :                std::vector<transition>& d_trans,
     931             :                LTS_TYPE& aut)
     932             : {
     933         558 :   if (!tss.is_set_empty(d))
     934             :   {
     935         558 :     if (tss.is_set_empty(tss.get_set_child_right(d)))
     936             :     {
     937             :       // for (outgoing_transitions_per_state_t:: const_iterator
     938             :       //     j=begin.lower_bound(tss.get_set_child_left(d)); j!=begin.upper_bound(tss.get_set_child_left(d)); ++j)
     939         465 :       const state_type from=tss.get_set_child_left(d);
     940             :       // for(const outgoing_pair_t& p: begin[from])
     941        1084 :       for (detail::state_type i=begin.lowerbound(from); i<begin.upperbound(from); ++i)
     942             :       {
     943         619 :         const outgoing_pair_t& p=begin.get_transitions()[i];
     944         619 :         d_trans.push_back(transition(from, aut.apply_hidden_label_map(label(p)), to(p)));
     945             :       }
     946             :     }
     947             :     else
     948             :     {
     949          93 :       get_trans(begin,tss,tss.get_set_child_left(d),d_trans,aut);
     950          93 :       get_trans(begin,tss,tss.get_set_child_right(d),d_trans,aut);
     951             :     }
     952             :   }
     953         558 : }
     954             : } // namespace detail
     955             : 
     956             : 
     957             : template <class LTS_TYPE>
     958          75 : void determinise(LTS_TYPE& l)
     959             : {
     960         150 :   tree_set_store tss;
     961             : 
     962         150 :   std::vector<transition> d_transs;
     963         150 :   std::vector<std::ptrdiff_t> d_states;
     964             : 
     965             :   // create the initial state of the DLTS
     966          75 :   d_states.push_back(l.initial_state());
     967          75 :   std::ptrdiff_t d_id = tss.set_set_tag(tss.create_set(d_states));
     968          75 :   d_states.clear();
     969             : 
     970             :   // std::multimap < transition::size_type, std::pair < transition::size_type, transition::size_type > >
     971             :   // const outgoing_transitions_per_state_t begin(l.get_transitions(),l.hidden_label_map(),l.num_states(),true);
     972         150 :   const outgoing_transitions_per_state_t begin(l.get_transitions(),l.num_states(),true);
     973             : 
     974          75 :   l.clear_transitions();
     975          75 :   l.clear_state_labels();
     976          75 :   std::size_t d_ntransitions = 0;
     977         150 :   std::vector < transition > d_transitions;
     978             : 
     979             :   std::size_t s;
     980             :   std::size_t i,to,lbl,n_t;
     981             : 
     982         819 :   while (d_id < tss.get_next_tag())
     983             :   {
     984             :     // collect the outgoing transitions of every state of DLTS state d_id in
     985             :     // the vector d_transs
     986         372 :     detail::get_trans(begin,tss,tss.get_set(d_id),d_transs,l);
     987             : 
     988             :     // sort d_transs by label and (if labels are equal) by destination
     989         372 :     const detail::compare_transitions_lts compare(l.hidden_label_map());
     990         372 :     sort(d_transs.begin(),d_transs.end(),compare);
     991             : 
     992         372 :     n_t = d_transs.size();
     993         372 :     i = 0;
     994        2263 :     for (lbl = 0; lbl < l.num_action_labels(); ++lbl)
     995             :     {
     996             :       // compute the destination of the transition with label lbl
     997        1891 :       while (i < n_t && l.apply_hidden_label_map(d_transs[i].label()) < lbl)
     998             :       {
     999           0 :         ++i;
    1000             :       }
    1001        3035 :       while (i < n_t && l.apply_hidden_label_map(d_transs[i].label()) == lbl)
    1002             :       {
    1003         572 :         to = d_transs[i].to();
    1004         572 :         d_states.push_back(to);
    1005        2531 :         while (i < n_t && l.apply_hidden_label_map(d_transs[i].label()) == lbl &&
    1006         721 :                d_transs[i].to() == to)
    1007             :         {
    1008         619 :           ++i;
    1009             :         }
    1010             :       }
    1011        1891 :       s = tss.create_set(d_states);
    1012             : 
    1013             :       // generate the transitions to each of the next states
    1014        1891 :       if (!tss.is_set_empty(s))
    1015             :       {
    1016         470 :         d_transitions.push_back(transition(d_id,lbl,tss.set_set_tag(s)));
    1017             : 
    1018         470 :         if (d_ntransitions%10000 == 0)
    1019             :         {
    1020         470 :           mCRL2log(log::debug) <<
    1021           0 :             "generated " << tss.get_next_tag() << " states and " << d_ntransitions
    1022           0 :                          << " transitions; explored " << d_id << " states" << std::endl;
    1023             :         }
    1024             :       }
    1025        1891 :       d_states.clear();
    1026             :     }
    1027         372 :     d_transs.clear();
    1028         372 :     ++d_id;
    1029             :   }
    1030             : 
    1031             : 
    1032          75 :   l.set_num_states(d_id,false); // remove the state values, and reset the number of states.
    1033          75 :   l.set_initial_state(0);
    1034             : 
    1035         545 :   for (const transition& t: d_transitions)
    1036             :   {
    1037         470 :     l.add_transition(t);
    1038             :   }
    1039          75 :   assert(is_deterministic(l));
    1040          75 : }
    1041             : 
    1042             : } // namespace lts
    1043             : } // namespace mcrl2
    1044             : 
    1045             : #endif // MCRL2_LTS_LTS_ALGORITHM_H
    1046             : 
    1047             : 
    1048             : 

Generated by: LCOV version 1.12