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

Generated by: LCOV version 1.12