LCOV - code coverage report
Current view: top level - lts/include/mcrl2/lts/detail - liblts_sim.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 326 387 84.2 %
Date: 2020-07-11 00:44:39 Functions: 22 30 73.3 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Bas Ploeger
       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             : /// \file liblts_sim.h
      10             : /// \brief Header file for the simulation preorder algorithm
      11             : 
      12             : #ifndef LIBLTS_SIM_H
      13             : #define LIBLTS_SIM_H
      14             : #include "mcrl2/lts/lts_utilities.h"
      15             : #include "mcrl2/lts/detail/sim_hashtable.h"
      16             : #include "mcrl2/lts/lts_aut.h"
      17             : #include "mcrl2/lts/lts_fsm.h"
      18             : #include "mcrl2/lts/lts_dot.h"
      19             : 
      20             : namespace mcrl2
      21             : {
      22             : namespace lts
      23             : {
      24             : namespace detail
      25             : {
      26             : 
      27             : template <class LTS_TYPE>
      28             : class sim_partitioner
      29             : {
      30             :   public:
      31             :     /** Creates a partitioner for an LTS.
      32             :      * \param[in] l Pointer to the LTS. */
      33             :     sim_partitioner(LTS_TYPE& l);
      34             : 
      35             :     /** Destroys this partitioner. */
      36             :     ~sim_partitioner();
      37             : 
      38             :     /** Computes the simulation equivalence classes and preorder
      39             :      * relations of the LTS. */
      40             :     virtual void partitioning_algorithm();
      41             : 
      42             :     /** Gives the transition relation on the computed equivalence
      43             :      * classes of the LTS. The label numbers of the transitions
      44             :      * correspond to the label numbers of the LTS that was passed as an
      45             :      * argument to the constructor of this partitioner.
      46             :      * The state numbers of the transitions are the equivalence class
      47             :      * numbers which range from 0 upto (and excluding) \ref num_eq_classes().
      48             :      *
      49             :      * \pre The simulation equivalence classes have been computed.
      50             :      * \return A vector containing the transitions between the
      51             :      * simulation equivalence classes. */
      52             :     std::vector < mcrl2::lts::transition> get_transitions() const;
      53             : 
      54             :     /** Gives the number of simulation equivalence classes of the LTS.
      55             :      * \pre The simulation equivalence classes have been computed.
      56             :      * \return The number of simulation equivalence classes of the LTS.
      57             :      */
      58             :     std::size_t num_eq_classes() const;
      59             : 
      60             :     /** Gives the equivalence class number of a state.
      61             :      * The equivalence class numbers range from 0 upto (and excluding)
      62             :      * \ref num_eq_classes().
      63             :      * \pre The simulation equivalence classes have been computed.
      64             :      * \param[in] s A state number.
      65             :      * \return The number of the equivalence class to which \e s
      66             :      * belongs. */
      67             :     std::size_t get_eq_class(std::size_t s) const;
      68             : 
      69             :     /** Returns whether one state is simulated by another state.
      70             :      * \pre The simulation preorder has been computed.
      71             :      * \param[in] s A state number.
      72             :      * \param[in] t A state number.
      73             :      * \retval true if \e s is simulated by \e t;
      74             :      * \retval false otherwise. */
      75             :     bool in_preorder(std::size_t s,std::size_t t) const;
      76             : 
      77             :     /** Returns whether two states are in the same simulation
      78             :      * equivalence class.
      79             :      * \pre The simulation equivalence classes have been computed.
      80             :      * \param[in] s A state number.
      81             :      * \param[in] t A state number.
      82             :      * \retval true if \e s and \e t are in the same simulation
      83             :      * equivalence class;
      84             :      * \retval false otherwise. */
      85             :     bool in_same_class(std::size_t s,std::size_t t) const;
      86             : 
      87             :   protected:
      88             : 
      89             :     /** Computes the simulation equivalence classes and preorder
      90             :      * relations of the LTS.
      91             :      * \pre : initialise_datastructures called */
      92             :     void partitioning_algorithmG();
      93             :     
      94             :     struct state_bucket
      95             :     {
      96             :       ptrdiff_t next;
      97             :       ptrdiff_t prev;
      98             :     };
      99             : 
     100             :     LTS_TYPE& aut;
     101             :     mcrl2::lts::outgoing_transitions_per_state_action_t trans_index;
     102             :     std::size_t s_Sigma;
     103             :     std::size_t s_Pi;
     104             :     std::vector<bool> state_touched;
     105             :     std::vector<bool> block_touched;
     106             :     std::vector<state_bucket> state_buckets;
     107             :     std::vector<std::size_t> block_Pi;
     108             :     std::vector<std::size_t> parent;
     109             :     std::vector< std::vector<std::size_t> > children;
     110             :     std::vector<ptrdiff_t> contents_t;
     111             :     std::vector<ptrdiff_t> contents_u;
     112             :     std::vector< std::vector<bool> > stable;
     113             :     hash_table3* exists;
     114             :     hash_table3* forall;
     115             :     std::vector< std::vector<std::size_t> > pre_exists;
     116             :     std::vector< std::vector<std::size_t> > pre_forall;
     117             :     hash_table3* match;
     118             :     std::vector< std::vector<bool> > P;
     119             :     std::vector< std::vector<bool> > Q;
     120             : 
     121             :     /* auxiliary variables */
     122             :     std::vector<std::size_t> touched_blocks;
     123             :     std::vector<std::size_t> contents;
     124             : 
     125             :     void initialise_datastructures();
     126             :     //void read_partition_from_file(char *parfile);
     127             : 
     128             :     void refine(bool& change);
     129             :     void update();
     130             :     //void update_lts();
     131             : 
     132             :     void touch(std::size_t a,std::size_t alpha);
     133             :     void untouch(std::size_t alpha);
     134             : 
     135             :     void reverse_topological_sort(std::vector<std::size_t>& Sort);
     136             :     void dfs_visit(std::size_t u,std::vector<bool>& visited,
     137             :                    std::vector<std::size_t>& Sort);
     138             : 
     139             :     void initialise_Sigma(std::size_t gamma,std::size_t l);
     140             :     void initialise_Pi(std::size_t gamma,std::size_t l);
     141             :     void filter(std::size_t S,std::vector< std::vector<bool> >& R,bool B);
     142             :     void cleanup(std::size_t alpha,std::size_t beta);
     143             :     void initialise_pre_EA();
     144             :     void induce_P_on_Pi();
     145             : 
     146             :     std::string print_Sigma_P();
     147             :     std::string print_Pi_Q();
     148             :     std::string print_Sigma();
     149             :     std::string print_Pi();
     150             :     std::string print_relation(std::size_t s,std::vector< std::vector<bool> >& R);
     151             :     std::string print_block(std::size_t b);
     152             :     std::string print_structure(hash_table3* struc);
     153             :     std::string print_reverse_topological_sort(const std::vector<std::size_t>& Sort);
     154             : };
     155             : 
     156             : 
     157             : #define LIST_END (-1)
     158             : #define UNIVERSAL_PART (0)
     159             : 
     160             : template <class LTS_TYPE>
     161          54 : sim_partitioner<LTS_TYPE>::sim_partitioner(LTS_TYPE& l)
     162          54 :   : aut(l)
     163             : {
     164          54 :   match  = new hash_table3(1000);
     165          54 :   exists = new hash_table3(1000);
     166          54 :   forall = new hash_table3(1000);
     167          54 : }
     168             : 
     169             : template <class LTS_TYPE>
     170          54 : sim_partitioner<LTS_TYPE>::~sim_partitioner()
     171             : {
     172          54 :   delete match;
     173          54 :   delete exists;
     174          54 :   delete forall;
     175         108 : }
     176             : 
     177             : /* ----------------- PARTITIONING ALGORITHM ------------------------- */
     178             : 
     179             : template <class LTS_TYPE>
     180          38 : void sim_partitioner<LTS_TYPE>::partitioning_algorithm()
     181             : {
     182          38 :   initialise_datastructures();
     183          38 :   partitioning_algorithmG();
     184          38 : }
     185             : 
     186             : /* Pre : initialise_datastructures called */
     187             : template <class LTS_TYPE>
     188          54 : void sim_partitioner<LTS_TYPE>::partitioning_algorithmG()
     189             : {
     190             :   using namespace mcrl2::core;
     191             : 
     192             :   bool change;
     193             :   std::size_t i;
     194             : 
     195          54 :   refine(change);
     196          54 :   update();
     197             : 
     198          54 :   change = true;
     199          54 :   i = 0;
     200         236 :   while (change)
     201             :   {
     202          91 :     change = false;
     203             : 
     204             :     /* Set Sigma to Pi and P to Q*/
     205          91 :     s_Sigma = s_Pi;
     206             :     /* The following statement simultaneously assigns P to Q and Q to P.
     207             :      * The assignment of Q to P is safe because Q is not used in
     208             :      * refine() and will be freshly computed at the start of update().
     209             :      * The advantage of using swap() is that it is executed in constant
     210             :      * time. */
     211          91 :     P.swap(Q);
     212             : 
     213          91 :     mCRL2log(log::debug) << "--------------------- ITERATION " << i << " ----------------------------------" << std::endl;
     214             : 
     215          91 :     mCRL2log(log::debug) << "  iteration " << i << "; number of blocks: " << s_Sigma << std::endl;
     216             : 
     217          91 :     refine(change);
     218          91 :     if (change)
     219             :     {
     220          37 :       update();
     221             :     }
     222             :     else
     223             :     {
     224             :       /* No blocks were split by refine(), so update() need not be
     225             :        * called. However, we do need to swap P and Q again: Q currently
     226             :        * contains the P-relation of the previous iteration (due to the
     227             :        * call to swap() prior to the call to refine()) but we want it to
     228             :        * contain that of the current iteration! */
     229          54 :       P.swap(Q);
     230             :     }
     231          91 :     ++i;
     232             :   }
     233             : 
     234          54 :   if (mCRL2logEnabled(log::debug))
     235             :   {
     236           0 :     mCRL2log(log::debug) << print_Pi_Q();
     237             :   }
     238          54 : }
     239             : 
     240             : template <class LTS_TYPE>
     241          54 : void sim_partitioner<LTS_TYPE>::initialise_datastructures()
     242             : {
     243             :   // aut.sort_transitions(mcrl2::lts::lbl_tgt_src);
     244             :   // trans_index = aut.get_transition_pre_table();
     245          54 :   trans_index=transitions_per_outgoing_state_action_pair_reversed(aut.get_transitions(),aut.hidden_label_map());
     246             : 
     247          54 :   std::size_t N = aut.num_states();
     248             : 
     249          54 :   state_bucket sb = { LIST_END, LIST_END };
     250          54 :   state_buckets.assign(N,sb);
     251          54 :   state_touched.assign(N,false);
     252          54 :   block_Pi.assign(N,UNIVERSAL_PART);
     253             : 
     254             :   /* put all states in one block */
     255          54 :   s_Pi = 1;
     256          54 :   contents_u.push_back(UNIVERSAL_PART);
     257          54 :   contents_t.push_back(LIST_END);
     258         620 :   for (std::size_t i = 0; i < N; ++i)
     259             :   {
     260         566 :     if (i > 0)
     261             :     {
     262         512 :       state_buckets[i].prev = i-1;
     263             :     }
     264             :     else
     265             :     {
     266          54 :       state_buckets[i].prev = LIST_END;
     267             :     }
     268         566 :     if (i < N-1)
     269             :     {
     270         512 :       state_buckets[i].next = i+1;
     271             :     }
     272             :     else
     273             :     {
     274          54 :       state_buckets[i].next = LIST_END;
     275             :     }
     276             :   }
     277             : 
     278          54 :   block_touched.assign(s_Pi,false);
     279          54 :   s_Sigma = s_Pi;
     280             : 
     281             :   /* initialise P and children */
     282         108 :   std::vector<std::size_t> vi;
     283          54 :   children.assign(s_Sigma,vi);
     284         108 :   std::vector<bool> vb(s_Sigma,false);
     285          54 :   P.assign(s_Sigma,vb);
     286         108 :   for (std::size_t i = 0; i < s_Sigma; ++i)
     287             :   {
     288          54 :     children[i].push_back(i);
     289          54 :     P[i][i] = true;
     290             :   }
     291             : 
     292          54 :   mCRL2log(log::debug) << "--------------------- INITIALISATION ---------------------------" << std::endl;
     293          54 :   mCRL2log(log::debug) << "  initialisation; number of blocks: " << s_Sigma << std::endl;
     294          54 : }
     295             : 
     296             : /* ----------------- INITIALISE ------------------------------------- */
     297             : 
     298             : template <class LTS_TYPE>
     299        9302 : void sim_partitioner<LTS_TYPE>::initialise_Pi(std::size_t gamma,std::size_t l)
     300             : {
     301             :   std::size_t alpha, a, c;
     302        9302 :   std::vector<std::size_t>::iterator ci, last;
     303             : 
     304        9302 :   contents.clear();
     305       32849 :   for (ptrdiff_t i = contents_u[gamma]; i != LIST_END;
     306       23547 :        i = state_buckets[i].next)
     307             :   {
     308       23547 :     contents.push_back(std::size_t(i));
     309             :   }
     310        9531 :   for (ptrdiff_t i = contents_t[gamma]; i != LIST_END;
     311         229 :        i = state_buckets[i].next)
     312             :   {
     313         229 :     contents.push_back(std::size_t(i));
     314             :   }
     315        9302 :   last = contents.end();
     316       33078 :   for (ci = contents.begin(); ci != last; ++ci)
     317             :   {
     318       23776 :     c = *ci;
     319             :     /* iterate over the incoming l-transitions of c */
     320             :     using namespace mcrl2::lts;
     321        5556 :     for (outgoing_transitions_per_state_action_t::iterator
     322       23776 :          t=trans_index.lower_bound(std::pair < transition::size_type, transition::size_type >(c,l));
     323       29332 :          t!=trans_index.upper_bound(std::pair < transition::size_type, transition::size_type >(c,l)); ++t)
     324             :     {
     325        5556 :       a = to(t); // As trans_index is reversed, this is actually the state from which the transition t goes.
     326        5556 :       if (!state_touched[a])
     327             :       {
     328        5154 :         alpha = block_Pi[a];
     329        5154 :         touch(a,alpha);
     330        5154 :         if (!block_touched[alpha])
     331             :         {
     332        2730 :           touched_blocks.push_back(alpha);
     333        2730 :           block_touched[alpha] = true;
     334             :         }
     335             :       }
     336             :     }
     337             :   }
     338        9302 : }
     339             : 
     340             : template <class LTS_TYPE>
     341        4977 : void sim_partitioner<LTS_TYPE>::initialise_Sigma(std::size_t gamma,std::size_t l)
     342             : {
     343        4977 :   std::vector<std::size_t>::iterator deltai, last;
     344        4977 :   last = children[gamma].end();
     345       11628 :   for (deltai = children[gamma].begin(); deltai != last; ++deltai)
     346             :   {
     347        6651 :     initialise_Pi(*deltai,l);
     348             :   }
     349        4977 : }
     350             : 
     351             : /* ----------------- REFINE ----------------------------------------- */
     352             : 
     353             : /* PRE: s_Sigma = s_Pi */
     354             : template <class LTS_TYPE>
     355         145 : void sim_partitioner<LTS_TYPE>::refine(bool& change)
     356             : {
     357             :   using namespace mcrl2::core;
     358             :   /* Initialise the parent and children functions */
     359         290 :   std::vector<std::size_t> v;
     360         145 :   children.assign(s_Pi,v);
     361         145 :   parent.assign(s_Pi,0);
     362             :   std::size_t alpha;
     363         818 :   for (alpha = 0; alpha < s_Pi; ++alpha)
     364             :   {
     365         673 :     children[alpha].push_back(alpha);
     366         673 :     parent[alpha] = alpha;
     367             :   }
     368             : 
     369         145 :   if (mCRL2logEnabled(log::debug))
     370             :   {
     371           0 :     mCRL2log(log::debug) << "--------------------- Refine ---------------------------------------" << std::endl;
     372           0 :     mCRL2log(log::debug) << print_Sigma_P();
     373             :   }
     374             : 
     375             :   /* Compute a reverse topological sorting of Sigma w.r.t. P */
     376         290 :   std::vector<std::size_t> Sort;
     377         145 :   Sort.reserve(s_Sigma);
     378         145 :   reverse_topological_sort(Sort);
     379             : 
     380         145 :   if (mCRL2logEnabled(log::debug))
     381             :   {
     382           0 :     mCRL2log(log::debug) << print_reverse_topological_sort(Sort);
     383             :   }
     384             : 
     385             :   /* Some local variables */
     386         290 :   std::vector<bool> v_false(s_Sigma,false);
     387         145 :   std::vector<std::size_t>::iterator alphai, last, gammai;
     388         145 :   std::vector< std::vector<bool> >::iterator stable_alpha, P_gamma;
     389             :   bool stable_alpha_gamma;
     390             :   std::size_t gamma, delta, l;
     391             : 
     392             :   /* The main loop */
     393         764 :   for (l = 0; l < aut.num_action_labels(); ++l)
     394             :   {
     395         619 :     mCRL2log(log::debug) << "---------------------------------------------------" << std::endl;
     396         619 :     mCRL2log(log::debug) << "Label = \"" << mcrl2::lts::pp(aut.action_label(l)) << "\"" << std::endl;
     397             : 
     398             :     /* reset the stable function */
     399         619 :     stable.assign(s_Pi,v_false);
     400             : 
     401             :     /* iterate over the reverse topological sorting */
     402        3727 :     for (gammai = Sort.begin(); gammai != Sort.end(); ++gammai)
     403             :     {
     404        3108 :       gamma = *gammai;
     405             : 
     406        3108 :       touched_blocks.clear();
     407        3108 :       initialise_Sigma(gamma,l);
     408             : 
     409             :       /* iterate over all alpha such that alpha -l->E gamma */
     410        3108 :       last = touched_blocks.end();
     411        4186 :       for (alphai = touched_blocks.begin(); alphai != last; ++alphai)
     412             :       {
     413        1078 :         alpha = *alphai;
     414             :         /* compute stable(alpha,gamma); use a local boolean variable for
     415             :          * efficiency */
     416        1078 :         stable_alpha_gamma = false;
     417        1078 :         stable_alpha = stable.begin() + alpha;
     418        1078 :         P_gamma = P.begin() + gamma;
     419       10358 :         for (delta = 0; delta < s_Sigma && !stable_alpha_gamma; ++delta)
     420             :         {
     421        9280 :           if ((*stable_alpha)[delta] && (*P_gamma)[delta])
     422             :           {
     423          32 :             stable_alpha_gamma = true;
     424             :           }
     425             :         }
     426        1078 :         (*stable_alpha)[gamma] = stable_alpha_gamma;
     427        1078 :         if (!stable_alpha_gamma)
     428             :         {
     429             :           /* if alpha -l->A gamma then alpha cannot be split */
     430        1046 :           if (contents_u[alpha] != LIST_END)
     431             :           {
     432             :             /* split alpha; new block will be s_Pi */
     433         191 :             change = true;
     434             : 
     435         191 :             children[parent[alpha]].push_back(s_Pi);
     436         191 :             parent.push_back(parent[alpha]);
     437         191 :             stable.push_back(*stable_alpha);
     438         191 :             block_touched.push_back(false);
     439         191 :             contents_t.push_back(LIST_END);
     440             : 
     441             :             /* assign the untouched contents of alpha to s_Pi */
     442         191 :             contents_u.push_back(contents_u[alpha]);
     443         191 :             contents_u[alpha] = LIST_END;
     444             : 
     445             :             /* update the block information for the moved states */
     446        1337 :             for (ptrdiff_t i = contents_u[s_Pi]; i != LIST_END;
     447        1146 :                  i = state_buckets[i].next)
     448             :             {
     449        1146 :               block_Pi[i] = s_Pi;
     450             :             }
     451         191 :             ++s_Pi;
     452             :           }
     453        1046 :           stable[alpha][gamma] = true;
     454             :         }
     455        1078 :         untouch(alpha);
     456             :       }
     457             :     }
     458             :   }
     459         145 : }
     460             : 
     461             : template <class LTS_TYPE>
     462         145 : void sim_partitioner<LTS_TYPE>::reverse_topological_sort(std::vector<std::size_t>& Sort)
     463             : {
     464         290 :   std::vector<bool> visited(s_Sigma,false);
     465         818 :   for (std::size_t u = 0; u < s_Sigma; ++u)
     466             :   {
     467         673 :     if (!visited[u])
     468             :     {
     469         583 :       dfs_visit(u,visited,Sort);
     470             :     }
     471             :   }
     472         145 : }
     473             : 
     474             : template <class LTS_TYPE>
     475         673 : void sim_partitioner<LTS_TYPE>::dfs_visit(std::size_t u,std::vector<bool>& visited,
     476             :     std::vector<std::size_t> &Sort)
     477             : {
     478         673 :   visited[u] = true;
     479        6824 :   for (std::size_t v = 0; v < s_Sigma; ++v)
     480             :   {
     481        6151 :     if (!visited[v] && P[u][v])
     482             :     {
     483          90 :       dfs_visit(v,visited,Sort);
     484             :     }
     485             :   }
     486         673 :   Sort.push_back(u);
     487         673 : }
     488             : 
     489             : template <class LTS_TYPE>
     490        5154 : void sim_partitioner<LTS_TYPE>::touch(std::size_t a,std::size_t alpha)
     491             : {
     492        5154 :   state_touched[a] = true;
     493        5154 :   ptrdiff_t p = state_buckets[a].prev;
     494        5154 :   ptrdiff_t n = state_buckets[a].next;
     495        5154 :   if (p == LIST_END)
     496             :   {
     497        2881 :     contents_u[alpha] = n;
     498             :   }
     499             :   else
     500             :   {
     501        2273 :     state_buckets[p].next = n;
     502             :   }
     503        5154 :   if (n != LIST_END)
     504             :   {
     505        1456 :     state_buckets[n].prev = p;
     506             :   }
     507        5154 :   state_buckets[a].prev = LIST_END;
     508        5154 :   state_buckets[a].next = contents_t[alpha];
     509        5154 :   if (contents_t[alpha] != LIST_END)
     510             :   {
     511        2424 :     state_buckets[contents_t[alpha]].prev = a;
     512             :   }
     513        5154 :   contents_t[alpha] = a;
     514        5154 : }
     515             : 
     516             : /* PRE: contents_t[alpha] != LIST_END */
     517             : template <class LTS_TYPE>
     518        2730 : void sim_partitioner<LTS_TYPE>::untouch(std::size_t alpha)
     519             : {
     520             :   // search linearly for the last element of contents_t[alpha];
     521             :   // untouch every state we encounter along the way
     522        2730 :   ptrdiff_t i = contents_t[alpha];
     523        7578 :   while (state_buckets[i].next != LIST_END)
     524             :   {
     525        2424 :     state_touched[i] = false;
     526        2424 :     i = state_buckets[i].next;
     527             :   }
     528             :   // last element has not been untouched yet
     529        2730 :   state_touched[i] = false;
     530             : 
     531             :   // insert the list contents_t[alpha] at the beginning of
     532             :   // contents_u[alpha]
     533        2730 :   state_buckets[i].next = contents_u[alpha];
     534        2730 :   if (contents_u[alpha] != LIST_END)
     535             :   {
     536         125 :     state_buckets[contents_u[alpha]].prev = i;
     537             :   }
     538        2730 :   contents_u[alpha] = contents_t[alpha];
     539        2730 :   contents_t[alpha] = LIST_END;
     540        2730 :   block_touched[alpha] = false;
     541        2730 : }
     542             : 
     543             : /* ----------------- UPDATE ----------------------------------------- */
     544             : 
     545             : template <class LTS_TYPE>
     546          91 : void sim_partitioner<LTS_TYPE>::update()
     547             : {
     548             :   using namespace mcrl2::core;
     549          91 :   mCRL2log(log::debug) << "--------------------- Update ---------------------------------------" << std::endl;
     550             : 
     551             :   std::size_t l,alpha,gamma;
     552          91 :   std::vector<std::size_t>::iterator alphai, last;
     553             : 
     554          91 :   induce_P_on_Pi();
     555             : 
     556          91 :   initialise_pre_EA();
     557             : 
     558             :   /* Compute the pre_exists and pre_forall functions */
     559         485 :   for (l = 0; l < aut.num_action_labels(); ++l)
     560             :   {
     561         394 :     pre_exists[l].reserve(s_Sigma + 1);
     562         394 :     pre_forall[l].reserve(s_Sigma + 1);
     563         394 :     pre_exists[l].push_back(exists->get_num_elements());
     564         394 :     pre_forall[l].push_back(forall->get_num_elements());
     565        2135 :     for (gamma = 0; gamma < s_Sigma; ++gamma)
     566             :     {
     567        1741 :       touched_blocks.clear();
     568        1741 :       initialise_Sigma(gamma,l);
     569        1741 :       last = touched_blocks.end();
     570        2461 :       for (alphai = touched_blocks.begin(); alphai != last; ++alphai)
     571             :       {
     572         720 :         alpha = *alphai;
     573         720 :         exists->add(alpha,l,gamma);
     574         720 :         if (contents_u[alpha] == LIST_END)
     575             :         {
     576         714 :           forall->add(alpha,l,gamma);
     577             :         }
     578         720 :         untouch(alpha);
     579             :       }
     580        1741 :       pre_exists[l].push_back(exists->get_num_elements());
     581        1741 :       pre_forall[l].push_back(forall->get_num_elements());
     582             :     }
     583             :   }
     584             : 
     585          91 :   mCRL2log(log::debug) << "------ Filter(false) ------\nExists: ";
     586          91 :   mCRL2log(log::debug) << print_structure(exists);
     587          91 :   mCRL2log(log::debug) << "\nForall: ";
     588          91 :   mCRL2log(log::debug) << print_structure(forall);
     589          91 :   mCRL2log(log::debug) << "\nSimulation relation: ";
     590          91 :   mCRL2log(log::debug) << print_relation(s_Pi,Q);
     591             : 
     592             :   /* Apply the first filtering to Q */
     593          91 :   filter(s_Sigma,P,false);
     594             : 
     595             : 
     596          91 :   initialise_pre_EA();
     597             : 
     598             :   /* Compute the pre_exists and pre_forall functions */
     599         485 :   for (l = 0; l < aut.num_action_labels(); ++l)
     600             :   {
     601         394 :     pre_exists[l].reserve(s_Pi + 1);
     602         394 :     pre_forall[l].reserve(s_Pi + 1);
     603         394 :     pre_exists[l].push_back(exists->get_num_elements());
     604         394 :     pre_forall[l].push_back(forall->get_num_elements());
     605        3045 :     for (gamma = 0; gamma < s_Pi; ++gamma)
     606             :     {
     607        2651 :       touched_blocks.clear();
     608        2651 :       initialise_Pi(gamma,l);
     609        2651 :       last = touched_blocks.end();
     610        3448 :       for (alphai = touched_blocks.begin(); alphai != last; ++alphai)
     611             :       {
     612         797 :         alpha = *alphai;
     613         797 :         exists->add(alpha,l,gamma);
     614         797 :         if (contents_u[alpha] == LIST_END)
     615             :         {
     616         684 :           forall->add(alpha,l,gamma);
     617             :         }
     618         797 :         untouch(alpha);
     619             :       }
     620        2651 :       pre_exists[l].push_back(exists->get_num_elements());
     621        2651 :       pre_forall[l].push_back(forall->get_num_elements());
     622             :     }
     623             :   }
     624             : 
     625          91 :   mCRL2log(log::debug) << "------ Filter(true) ------\nExists: ";
     626          91 :   mCRL2log(log::debug) << print_structure(exists);
     627          91 :   mCRL2log(log::debug) << "\nForall: ";
     628          91 :   mCRL2log(log::debug) << print_structure(forall);
     629          91 :   mCRL2log(log::debug) << "\nSimulation relation: ";
     630          91 :   mCRL2log(log::debug) << print_relation(s_Pi,Q);
     631             : 
     632             :   /* Apply the second filtering to Q */
     633          91 :   filter(s_Pi,Q,true);
     634          91 : }
     635             : 
     636             : template <class LTS_TYPE>
     637         182 : void sim_partitioner<LTS_TYPE>::initialise_pre_EA()
     638             : {
     639             :   /* Initialise the pre_exists and pre_forall data structures */
     640         182 :   exists->clear();
     641         182 :   forall->clear();
     642         364 :   std::vector<std::size_t> v;
     643         182 :   pre_exists.assign(aut.num_action_labels(),v);
     644         182 :   pre_forall.assign(aut.num_action_labels(),v);
     645         182 : }
     646             : 
     647             : template <class LTS_TYPE>
     648         107 : void sim_partitioner<LTS_TYPE>::induce_P_on_Pi()
     649             : {
     650             :   /* Compute the relation induced on Pi by P, store it in Q */
     651         214 :   std::vector<bool> v(s_Pi,false);
     652         107 :   Q.assign(s_Pi,v);
     653             : 
     654             :   std::size_t alpha,beta;
     655         107 :   std::vector< std::vector<bool> >::iterator P_parent_alpha;
     656         742 :   for (alpha = 0; alpha < s_Pi; ++alpha)
     657             :   {
     658         635 :     P_parent_alpha = P.begin() + parent[alpha];
     659        6748 :     for (beta = 0; beta < s_Pi; ++beta)
     660             :     {
     661        6113 :       Q[alpha][beta] = (*P_parent_alpha)[parent[beta]];
     662             :     }
     663             :   }
     664         107 : }
     665             : 
     666             : 
     667             : /* ----------------- FILTER ----------------------------------------- */
     668             : 
     669             : template <class LTS_TYPE>
     670         182 : void sim_partitioner<LTS_TYPE>::filter(std::size_t S,std::vector< std::vector<bool> > &R,
     671             :                                        bool B)
     672             : {
     673             :   /* Initialise the match function */
     674         182 :   match->clear();
     675             : 
     676             :   std::size_t alpha,beta,gamma,delta,l;
     677         182 :   hash_table3_iterator etrans(exists);
     678         970 :   for (l = 0; l < aut.num_action_labels(); ++l)
     679             :   {
     680        5180 :     for (delta = 0; delta < S; ++delta)
     681             :     {
     682        4392 :       etrans.set_end(pre_exists[l][delta+1]);
     683        5909 :       for (etrans.set(pre_exists[l][delta]); !etrans.is_end(); ++etrans)
     684             :       {
     685        1517 :         beta = etrans.get_x();
     686       15826 :         for (gamma = 0; gamma < S; ++gamma)
     687             :         {
     688       14309 :           if (R[gamma][delta])
     689             :           {
     690        2338 :             match->add(l,beta,gamma);
     691             :           }
     692             :         }
     693             :       }
     694             :     }
     695             :   }
     696             : 
     697         182 :   hash_table3_iterator atrans(forall);
     698             :   /* The main for loop */
     699         970 :   for (l = 0; l < aut.num_action_labels(); ++l)
     700             :   {
     701        5180 :     for (gamma = 0; gamma < S; ++gamma)
     702             :     {
     703        4392 :       atrans.set_end(pre_forall[l][gamma+1]);
     704        5790 :       for (atrans.set(pre_forall[l][gamma]); !atrans.is_end(); ++atrans)
     705             :       {
     706        1398 :         alpha = atrans.get_x();
     707       16732 :         for (beta = 0; beta < s_Pi; ++beta)
     708             :         {
     709       15334 :           if (Q[alpha][beta] && !match->find(l,beta,gamma))
     710             :           {
     711        1033 :             Q[alpha][beta] = false;
     712        1033 :             if (B)
     713             :             {
     714          20 :               cleanup(alpha,beta);
     715             :             }
     716             :           }
     717             :         }
     718             :       }
     719             :     }
     720             :   }
     721         182 : }
     722             : 
     723             : /* ----------------- CLEANUP ---------------------------------------- */
     724             : 
     725             : template <class LTS_TYPE>
     726          28 : void sim_partitioner<LTS_TYPE>::cleanup(std::size_t alpha,std::size_t beta)
     727             : {
     728             :   std::size_t l,alpha1,beta1,delta;
     729             :   bool match_l_beta1_alpha;
     730          28 :   hash_table3_iterator alpha1i(forall);
     731          28 :   hash_table3_iterator beta1i(exists);
     732         203 :   for (l = 0; l < aut.num_action_labels(); ++l)
     733             :   {
     734         175 :     alpha1i.set_end(pre_forall[l][alpha+1]);
     735         175 :     beta1i.set_end(pre_exists[l][beta+1]);
     736         204 :     for (beta1i.set(pre_exists[l][beta]); !beta1i.is_end(); ++beta1i)
     737             :     {
     738          29 :       beta1 = beta1i.get_x();
     739          29 :       match_l_beta1_alpha = false;
     740         843 :       for (delta = 0; delta < s_Pi && !match_l_beta1_alpha; ++delta)
     741             :       {
     742         814 :         if (exists->find(beta1,l,delta) && Q[alpha][delta])
     743             :         {
     744           1 :           match_l_beta1_alpha = true;
     745             :         }
     746             :       }
     747          29 :       if (!match_l_beta1_alpha)
     748             :       {
     749          28 :         match->remove(l,beta1,alpha);
     750          43 :         for (alpha1i.set(pre_forall[l][alpha]); !alpha1i.is_end();
     751          15 :              ++alpha1i)
     752             :         {
     753          15 :           alpha1 = alpha1i.get_x();
     754          15 :           if (Q[alpha1][beta1])
     755             :           {
     756           8 :             Q[alpha1][beta1] = false;
     757           8 :             cleanup(alpha1,beta1);
     758             :           }
     759             :         }
     760             :       }
     761             :     }
     762             :   }
     763          28 : }
     764             : 
     765             : /* ----------------- FOR POST-PROCESSING ---------------------------- */
     766             : 
     767             : template <class LTS_TYPE>
     768           5 : std::vector < mcrl2::lts::transition> sim_partitioner<LTS_TYPE>::get_transitions() const
     769             : {
     770             :   using namespace mcrl2::lts;
     771             : 
     772           5 :   std::vector < mcrl2::lts::transition> ts;
     773           5 :   ts.reserve(forall->get_num_elements());
     774             : 
     775          10 :   std::vector<bool> pre_sim;
     776             :   transition::size_type l,beta,gamma;
     777           5 :   hash_table3_iterator alphai(exists);
     778           5 :   hash_table3_iterator gammai(forall);
     779          65 :   for (beta = 0; beta < s_Pi; ++beta)
     780             :   {
     781         409 :     for (l = 0; l < aut.num_action_labels(); ++l)
     782             :     {
     783             :       // there is an l-transition from alpha to beta iff:
     784             :       // - alpha -l->A [beta]
     785             :       // - not Exists gamma : beta Q gamma  /\  alpha -l->E gamma
     786             :       // first compute for which alpha the latter statement does not
     787             :       // hold
     788         349 :       pre_sim.assign(s_Pi,false);
     789        9978 :       for (gamma = 0; gamma < s_Pi; ++gamma)
     790             :       {
     791             :         // only consider gammas that are unequal to beta
     792        9629 :         if (gamma != beta && Q[beta][gamma])
     793             :         {
     794          49 :           alphai.set_end(pre_exists[l][gamma+1]);
     795          62 :           for (alphai.set(pre_exists[l][gamma]); !alphai.is_end();
     796          13 :                ++alphai)
     797             :           {
     798          13 :             pre_sim[alphai.get_x()] = true;
     799             :           }
     800             :         }
     801             :       }
     802         349 :       gammai.set_end(pre_forall[l][beta+1]);
     803         434 :       for (gammai.set(pre_forall[l][beta]); !gammai.is_end(); ++gammai)
     804             :       {
     805          85 :         gamma = gammai.get_x();
     806          85 :         if (!pre_sim[gamma])
     807             :         {
     808             :           // add the transition gamma -l-> beta
     809          83 :           ts.push_back(transition(gamma,l,beta));
     810             :         }
     811             :       }
     812             :     }
     813             :   }
     814          10 :   return ts;
     815             : }
     816             : 
     817             : template <class LTS_TYPE>
     818           5 : std::size_t sim_partitioner<LTS_TYPE>::num_eq_classes() const
     819             : {
     820           5 :   return s_Pi;
     821             : }
     822             : 
     823             : template <class LTS_TYPE>
     824           5 : std::size_t sim_partitioner<LTS_TYPE>::get_eq_class(std::size_t s) const
     825             : {
     826           5 :   return block_Pi[s];
     827             : }
     828             : 
     829             : template <class LTS_TYPE>
     830          33 : bool sim_partitioner<LTS_TYPE>::in_preorder(std::size_t s,std::size_t t) const
     831             : {
     832          33 :   return Q[block_Pi[s]][block_Pi[t]];
     833             : }
     834             : 
     835             : template <class LTS_TYPE>
     836          16 : bool sim_partitioner<LTS_TYPE>::in_same_class(std::size_t s,std::size_t t) const
     837             : {
     838          16 :   return (block_Pi[s] == block_Pi[t]);
     839             : }
     840             : 
     841             : /*
     842             : // PRE: FORALL and EXISTS structures on Pi are computed
     843             : void sim_partitione<LTS_TYPE>r::update_nfa()
     844             : {
     845             :   std::vector< std::vector<std::size_t> > v(s_Pi);
     846             :   std::vector< std::vector< std::vector<std::size_t> > > post_trans(L,v);
     847             : 
     848             :   std::vector<bool> pre_sim;
     849             :   std::size_t l,beta,alpha,gamma;
     850             :   hash_table3_iterator alphai(exists);
     851             :   hash_table3_iterator gammai(forall);
     852             :   for (beta = 0; beta < s_Pi; ++beta)
     853             :   {
     854             :     for (l = 0; l < aut.num_action_labels(); ++l)
     855             :     {
     856             :       // there is an l-transition from alpha to beta iff:
     857             :       // - alpha -l->A [beta]
     858             :       // - not Exists gamma : beta Q gamma  /\  alpha -l->E gamma
     859             :       // first compute for which alpha the latter statement does not
     860             :       // hold
     861             :       pre_sim.assign(s_Pi,false);
     862             :       for (gamma = 0; gamma < s_Pi; ++gamma)
     863             :       {
     864             :         // only consider gammas that are unequal to beta
     865             :         if (gamma != beta && Q[beta][gamma])
     866             :         {
     867             :           alphai.set_end(pre_exists[l][gamma+1]);
     868             :           for (alphai.set(pre_exists[l][gamma]); !alphai.is_end();
     869             :               ++alphai)
     870             :           {
     871             :             pre_sim[alphai.get_x()] = true;
     872             :           }
     873             :         }
     874             :       }
     875             :       gammai.set_end(pre_forall[l][beta+1]);
     876             :       for (gammai.set(pre_forall[l][beta]); !gammai.is_end(); ++gammai)
     877             :       {
     878             :         gamma = gammai.get_x();
     879             :         if (!pre_sim[gamma])
     880             :         {
     881             :           post_trans[l][gamma].push_back(beta);
     882             :         }
     883             :       }
     884             :     }
     885             :   }
     886             : 
     887             :   std::vector<transition> *trans = new std::vector<transition> ();
     888             :   std::vector<bool> *final = new std::vector<bool> ();
     889             : 
     890             :   // Do a breadth first search over the computed graph to assign ids to
     891             :   // the reachable blocks and construct the final transition relation
     892             :   std::vector<std::size_t>::iterator post_it,post_last;
     893             :   std::queue<std::size_t> todo;
     894             :   std::vector<std::size_t> block_id(s_Pi,s_Pi);
     895             :   todo.push(block_Pi[aut.initial_state()]);
     896             :   block_id[block_Pi[aut.initial_state()]] = 0;
     897             :   std::size_t n_s = 1;
     898             :   std::size_t n_f = 0;
     899             :   if (aut.is_final(aut.initial_state()))
     900             :   {
     901             :     final->push_back(true);
     902             :     ++n_f;
     903             :   }
     904             :   else
     905             :   {
     906             :     final->push_back(false);
     907             :   }
     908             :   while (!todo.empty())
     909             :   {
     910             :     // visit todo.front()
     911             :     beta = todo.front();
     912             :     for (l = 0; l < L; ++l)
     913             :     {
     914             :       post_last = post_trans[l][beta].end();
     915             :       for (post_it = post_trans[l][beta].begin(); post_it != post_last;
     916             :           ++post_it)
     917             :       {
     918             :         alpha = *post_it;
     919             :         if (block_id[alpha] == s_Pi)
     920             :         {
     921             :           todo.push(alpha);
     922             :           block_id[alpha] = n_s;
     923             :           ++n_s;
     924             :           if (aut.is_final(contents_u[alpha]))
     925             :           {
     926             :             final->push_back(true);
     927             :             ++n_f;
     928             :           }
     929             :           else
     930             :           {
     931             :             final->push_back(false);
     932             :           }
     933             :         }
     934             :         transition t = {block_id[beta], l, block_id[alpha]};
     935             :         trans->push_back(t);
     936             :       }
     937             :     }
     938             :     todo.pop();
     939             :   }
     940             : 
     941             :   // assign the new transition relation to aut
     942             :   aut.clear_transition_relation();
     943             :   aut.clear_final();
     944             :   aut.set_num_states(n_s);
     945             :   aut.set_num_transitions(trans->size());
     946             :   aut.set_num_final(n_f);
     947             :   aut.set_init(0);
     948             :   aut.set_trans(trans);
     949             :   aut.set_final(final);
     950             : 
     951             :   // assign the simulation relation to aut
     952             :   aut.init_simulation_relation();
     953             :   for (beta = 0; beta < s_Pi; ++beta)
     954             :   {
     955             :     // only consider reachable blocks
     956             :     if (block_id[beta] < s_Pi)
     957             :     {
     958             :       for (gamma = 0; gamma < s_Pi; ++gamma)
     959             :       {
     960             :         if (block_id[gamma] < s_Pi && Q[beta][gamma])
     961             :         {
     962             :           aut.add_simulation(block_id[beta],block_id[gamma]);
     963             :         }
     964             :       }
     965             :     }
     966             :   }
     967             : }
     968             : */
     969             : 
     970             : /* ----------------- FOR DEBUGGING ---------------------------------- */
     971             : 
     972             : template <class LTS_TYPE>
     973           0 : std::string sim_partitioner<LTS_TYPE>::print_Sigma_P()
     974             : {
     975             :   using namespace mcrl2::core;
     976           0 :   std::stringstream result;
     977           0 :   result << print_Sigma() << "Simulation relation: " << print_relation(s_Sigma,P);
     978           0 :   return result.str();
     979             : }
     980             : 
     981             : template <class LTS_TYPE>
     982           0 : std::string sim_partitioner<LTS_TYPE>::print_Pi_Q()
     983             : {
     984             :   using namespace mcrl2::core;
     985           0 :   std::stringstream result;
     986           0 :   result << print_Pi() << "Simulation relation: " << print_relation(s_Pi,Q);
     987           0 :   return result.str();
     988             : }
     989             : 
     990             : template <class LTS_TYPE>
     991           0 : std::string sim_partitioner<LTS_TYPE>::print_Sigma()
     992             : {
     993             :   using namespace mcrl2::core;
     994           0 :   std::stringstream result;
     995           0 :   std::vector<std::size_t>::iterator ci, last;
     996           0 :   for (std::size_t b = 0; b < s_Sigma; ++b)
     997             :   {
     998           0 :     result << "block " << b << ": {";
     999           0 :     last = children[b].end();
    1000           0 :     for (ci = children[b].begin(); ci != last; ++ci)
    1001             :     {
    1002           0 :       result << print_block(*ci);
    1003             :     }
    1004           0 :     result << "}" << std::endl;
    1005             :   }
    1006           0 :   return result.str();
    1007             : }
    1008             : 
    1009             : template <class LTS_TYPE>
    1010           0 : std::string sim_partitioner<LTS_TYPE>::print_Pi()
    1011             : {
    1012           0 :   std::stringstream result;
    1013             :   using namespace mcrl2::core;
    1014           0 :   for (std::size_t b = 0; b < s_Pi; ++b)
    1015             :   {
    1016           0 :     result << "block " << b << ": {" << print_block(b) << "}" << std::endl;
    1017             :   }
    1018           0 :   return result.str();
    1019             : }
    1020             : 
    1021             : template <class LTS_TYPE>
    1022           0 : std::string sim_partitioner<LTS_TYPE>::print_block(std::size_t b)
    1023             : {
    1024           0 :   std::stringstream result;
    1025             :   using namespace mcrl2::core;
    1026           0 :   for (ptrdiff_t i = contents_u[b]; i != LIST_END; i = state_buckets[i].next)
    1027             :   {
    1028           0 :     result << i << ",";
    1029             :   }
    1030           0 :   for (ptrdiff_t i = contents_t[b]; i != LIST_END; i = state_buckets[i].next)
    1031             :   {
    1032           0 :     result << i << ",";
    1033             :   }
    1034           0 :   return result.str();
    1035             : }
    1036             : 
    1037             : template <class LTS_TYPE>
    1038           0 : std::string sim_partitioner<LTS_TYPE>::print_relation(std::size_t s,
    1039             :     std::vector< std::vector<bool> > &R)
    1040             : {
    1041             :   using namespace mcrl2::core;
    1042           0 :   std::stringstream result;
    1043           0 :   result << "{";
    1044             :   std::size_t beta,gamma;
    1045           0 :   for (beta = 0; beta < s; ++beta)
    1046             :   {
    1047           0 :     for (gamma = 0; gamma < s; ++gamma)
    1048             :     {
    1049           0 :       if (R[beta][gamma])
    1050             :       {
    1051           0 :         result << "(" << beta << "," << gamma << "),";
    1052             :       }
    1053             :     }
    1054             :   }
    1055           0 :   result << "}" << std::endl;
    1056           0 :   return result.str();
    1057             : }
    1058             : 
    1059             : template <class LTS_TYPE>
    1060           0 : std::string sim_partitioner<LTS_TYPE>::print_structure(hash_table3* struc)
    1061             : {
    1062             :   using namespace mcrl2::core;
    1063           0 :   std::stringstream result;
    1064           0 :   result << "{";
    1065           0 :   hash_table3_iterator i(struc);
    1066           0 :   for (; !i.is_end(); ++i)
    1067             :   {
    1068           0 :     result << "(" << i.get_x() << "," << mcrl2::lts::pp(aut.action_label(i.get_y()))
    1069           0 :            << "," << i.get_z() << "),";
    1070             :   }
    1071           0 :   result << "}";
    1072           0 :   return result.str();
    1073             : }
    1074             : 
    1075             : template <class LTS_TYPE>
    1076           0 : std::string sim_partitioner<LTS_TYPE>::print_reverse_topological_sort(const std::vector<std::size_t> &Sort)
    1077             : {
    1078             :   using namespace mcrl2::core;
    1079           0 :   std::stringstream result;
    1080           0 :   result << "reverse topological sort is: [";
    1081           0 :   for (std::size_t i = 0; i < Sort.size(); ++i)
    1082             :     {
    1083           0 :       result << Sort[i];
    1084           0 :       if (i+1 < Sort.size())
    1085             :         {
    1086           0 :           result << ",";
    1087             :         }
    1088             :     }
    1089           0 :   result << "]" << std::endl;
    1090           0 :   return result.str();
    1091             : } 
    1092             : 
    1093             : 
    1094             : } // namespace detail
    1095             : } // namespace lts
    1096             : } // namespace mcrl2
    1097             : #endif

Generated by: LCOV version 1.13