Line data    Source code

       1             : /// Author(s): # Carlos Gregorio-Rodriguez, Luis LLana, Rafael Martinez-Torres.
       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_ready_sim.h
      10             : /// \brief Header file for the ready-simulation preorder algorithm
      11             : 
      12             : #ifndef MCRL2_LTS_LIBLTS_READY_SIM_H
      13             : #define MCRL2_LTS_LIBLTS_READY_SIM_H
      14             : 
      15             : #include "mcrl2/lts/detail/liblts_sim.h"
      16             : 
      17             : 
      18             : namespace mcrl2
      19             : {
      20             : namespace lts
      21             : {
      22             : namespace detail
      23             : {
      24             : 
      25             : template <class LTS_TYPE>
      26             :   class ready_sim_partitioner : public sim_partitioner<LTS_TYPE>
      27             : {
      28             :  public:
      29          16 :   ready_sim_partitioner(LTS_TYPE& l) : sim_partitioner<LTS_TYPE>(l)
      30             :   {
      31          16 :     exists2 = new hash_table2(1000);
      32          16 :     forall2 = new hash_table2(1000);
      33          16 :   };
      34             : 
      35             :     /**
      36             :      * Computes the ready-simulation equivalence
      37             :      * classes and preorder relations of the LTS
      38             :      */  
      39             :   virtual void partitioning_algorithm();
      40             :     /** Destroys this partitioner. */
      41             :   ~ready_sim_partitioner();
      42             :  private :
      43             :   // Non inherited data members...
      44             :   hash_table2* exists2;
      45             :   hash_table2* forall2;  
      46             : 
      47             :   // Non inherited methods...
      48             :     /**
      49             :      * Drives the partition pair <Universal,Id>
      50             :      * into appropriate ready partition-pair
      51             :      * for furhter input into GCPP.
      52             :      * \pre : true
      53             :      */          
      54             :   void ready2sim_reduction();
      55             : 
      56             :   /**
      57             :    * Splits Universal partition
      58             :    * into classes alpha where either
      59             :    * { N } A<-l- alpha or
      60             :    * not { N } <-l- alpha
      61             :    * for some L
      62             :    * \pre : initialise_datastructures called.
      63             :    */
      64             :   void refinei() ;
      65             : 
      66             :   /*
      67             :    * Induce P on Pi, then
      68             :    * drops those pairs (alpha, beta)
      69             :    * such that
      70             :    *  {N} E<-l- Beta and not {N} A<-l- Alpha
      71             :    * \pre : refinei  called 
      72             :    */
      73             :   void updatei();
      74             : 
      75             : 
      76             :   // Non inherited auxiliary methods...
      77             :   std::string print_structure(hash_table2* struc);  
      78             :   
      79             :   // Inherited data members...
      80             :   using sim_partitioner<LTS_TYPE>::aut;
      81             :   using sim_partitioner<LTS_TYPE>::s_Pi;
      82             :   using sim_partitioner<LTS_TYPE>::s_Sigma;  
      83             :   using sim_partitioner<LTS_TYPE>::block_Pi;
      84             :   using sim_partitioner<LTS_TYPE>::children;
      85             :   using sim_partitioner<LTS_TYPE>::parent;
      86             :   using sim_partitioner<LTS_TYPE>::Q;
      87             :   using sim_partitioner<LTS_TYPE>::P;  
      88             :   using sim_partitioner<LTS_TYPE>::contents_t;
      89             :   using sim_partitioner<LTS_TYPE>::contents_u;
      90             :   using sim_partitioner<LTS_TYPE>::touched_blocks;  
      91             :   using sim_partitioner<LTS_TYPE>::block_touched;
      92             :   using sim_partitioner<LTS_TYPE>::state_buckets;
      93             : 
      94             :   // Inherited methods
      95             :   using sim_partitioner<LTS_TYPE>::induce_P_on_Pi;
      96             :   using sim_partitioner<LTS_TYPE>::initialise_Sigma;    
      97             :   using sim_partitioner<LTS_TYPE>::initialise_datastructures;  
      98             :   using sim_partitioner<LTS_TYPE>::partitioning_algorithmG;
      99             :   using sim_partitioner<LTS_TYPE>::touch;
     100             :   using sim_partitioner<LTS_TYPE>::untouch;
     101             : 
     102             :   // Auxiliary inherited methods
     103             :   using sim_partitioner<LTS_TYPE>::print_relation;
     104             :   using sim_partitioner<LTS_TYPE>::print_Sigma_P;
     105             :   using sim_partitioner<LTS_TYPE>::print_Pi_Q;
     106             : 
     107             : };
     108             : 
     109             : 
     110             : /* Pre : true */
     111             : template <class LTS_TYPE>
     112          16 : void ready_sim_partitioner<LTS_TYPE>::ready2sim_reduction()
     113             : {
     114          16 :   initialise_datastructures();
     115          16 :   refinei();
     116          16 :   updatei();
     117          16 :   s_Sigma = s_Pi; // <== Key!!
     118          16 :   P.swap(Q);      // <== Key!!
     119          16 :   mCRL2log(log::debug) << "--------------------- READY PRE-REDUCTION-------------------------" << std::endl;
     120          16 :   mCRL2log(log::debug) << "  prereduction; number of blocks: " << s_Sigma << std::endl;
     121          16 : }
     122             : 
     123             : /* ----------------- PARTITIONING ALGORITHM ------------------------- */
     124             : /* Pre : true */
     125             : template <class LTS_TYPE>
     126          16 : void ready_sim_partitioner<LTS_TYPE>::partitioning_algorithm()
     127             : {
     128             :   // ready_sim problem amounts to GCPP previous reduction
     129          16 :   ready2sim_reduction();
     130          16 :   partitioning_algorithmG();
     131          16 : }
     132             : 
     133             : /* ----------------- REFINE ----------------------------------------- */
     134             : 
     135             : /* PRE: s_Sigma = s_Pi = 1 */
     136             : template <class LTS_TYPE>
     137          16 : void ready_sim_partitioner<LTS_TYPE>::refinei()
     138             : {
     139             :   using namespace mcrl2::core;  
     140             :   /* Initialise the parent and children functions */
     141          16 :   std::vector<std::size_t> v;
     142          16 :   children.clear();
     143          16 :   children.assign(s_Pi,v);
     144          16 :   parent.clear();
     145          16 :   parent.assign(s_Pi,UNIVERSAL_PART);
     146             :   std::size_t alpha;
     147          32 :   for (alpha = 0; alpha < s_Pi; ++alpha)
     148             :   {
     149          16 :     children[alpha].push_back(alpha);
     150          16 :     parent[alpha] = alpha;
     151             :   }
     152             : 
     153          16 :   if (mCRL2logEnabled(log::debug))
     154             :   {
     155           0 :     mCRL2log(log::debug) << "---------------- Refinei ---------------------------------------" << std::endl;
     156           0 :     mCRL2log(log::debug) << print_Sigma_P();
     157             :   }
     158             : 
     159             :   /* Some local variables */
     160          16 :   std::vector<std::size_t>::iterator alphai, last;
     161             :   std::size_t l;  
     162             : 
     163             :   /* The main loop */  
     164          80 :   for (l = 0; l < aut.num_action_labels(); ++l)
     165             :   {
     166          64 :     mCRL2log(log::debug) << "---------------------------------------------------" << std::endl;
     167          64 :     mCRL2log(log::debug) << "Label = \"" << mcrl2::lts::pp(aut.action_label(l)) << "\"" << std::endl;
     168             : 
     169          64 :     touched_blocks.clear();
     170          64 :     initialise_Sigma(UNIVERSAL_PART,l);  // Interested on {N} E<-l- alpha
     171             :     
     172             :     /* iterate over all alpha such that {N} E<-l- alpha  */
     173          64 :     last = touched_blocks.end();
     174         125 :     for (alphai = touched_blocks.begin(); alphai != last; ++alphai)
     175             :       {
     176          61 :         alpha = *alphai;
     177             :         /* if {N} A<-l- alpha then alpha cannot be split */
     178          61 :         if (contents_u[alpha] != LIST_END)
     179             :           {
     180             :             /* split alpha; new block will be s_Pi */
     181          58 :             children[parent[alpha]].push_back(s_Pi);  
     182          58 :             parent.push_back(parent[alpha]);
     183          58 :             block_touched.push_back(false);
     184          58 :             contents_t.push_back(LIST_END);
     185             :               
     186             :             /* assign the untouched contents of alpha to s_Pi */
     187          58 :             contents_u.push_back(contents_u[alpha]);
     188          58 :             contents_u[alpha] = LIST_END;
     189             :               
     190             :             /* update the block information for the moved states */
     191         389 :             for (ptrdiff_t i = contents_u[s_Pi]; i != LIST_END;
     192         331 :                  i = state_buckets[i].next)
     193             :               {
     194         331 :                 block_Pi[i] = s_Pi;
     195             :               }
     196          58 :             ++s_Pi;
     197             :           }
     198          61 :         untouch(alpha); 
     199             :       }
     200             :   }
     201          16 : }
     202             : 
     203             :  
     204             : /* ----------------- UPDATEI ----------------------------------------- */
     205             : template <class LTS_TYPE>
     206          16 : void ready_sim_partitioner<LTS_TYPE>::updatei()
     207             : {
     208             :   using namespace mcrl2::core;
     209          16 :   mCRL2log(log::debug) << "---------------  Updatei ---------------------------------------" << std::endl;
     210             :   
     211             :   std::size_t l,alpha,gamma;
     212          16 :   std::vector<std::size_t>::iterator alphai, last;
     213             : 
     214          16 :   induce_P_on_Pi(); 
     215             : 
     216          16 :   exists2->clear();
     217          16 :   forall2->clear();
     218             : 
     219          80 :   for (l = 0; l < aut.num_action_labels(); ++l)
     220             :   {
     221         128 :     for (gamma = 0; gamma < s_Sigma; ++gamma) 
     222             :     {
     223          64 :       touched_blocks.clear();
     224          64 :       initialise_Sigma(gamma,l); 
     225          64 :       last = touched_blocks.end(); 
     226         138 :       for (alphai = touched_blocks.begin(); alphai != last; ++alphai)
     227             :       {
     228          74 :         alpha = *alphai;
     229          74 :         exists2->add(alpha,l); 
     230          74 :         if (contents_u[alpha] == LIST_END)
     231             :           {
     232          74 :             forall2->add(alpha,l);
     233             :           }
     234          74 :         untouch(alpha);
     235             :       }
     236             :     }
     237             :   }
     238             : 
     239          16 :   mCRL2log(log::debug) << "------ Before Filter ------\nExists2: ";
     240          16 :   mCRL2log(log::debug) << print_structure(exists2);
     241          16 :   mCRL2log(log::debug) << "\nForall2: ";
     242          16 :   mCRL2log(log::debug) << print_structure(forall2);
     243          16 :   mCRL2log(log::debug) << "\nReady Preorder: ";
     244          16 :   mCRL2log(log::debug) << print_relation(s_Pi,Q);  
     245             : 
     246             :   std::size_t beta;
     247             : 
     248             :   /* Apply the filtering to discard non "ready-init" pairs,
     249             :    * in Q[alpha][beta], i.e.,  when
     250             :    * {N} E<-l- Beta and not {N} A<-l- Alpha
     251             :    */
     252          80 :   for (l = 0; l < aut.num_action_labels(); ++l)
     253             :   {
     254         360 :     for (beta = 0; beta < s_Pi; ++beta) 
     255             :     {
     256         296 :       if (exists2->find(beta,l)) 
     257             :         {
     258         420 :           for (alpha = 0; alpha < s_Pi; ++alpha)
     259         346 :           if (Q[alpha][beta] && !forall2->find(alpha,l))
     260         191 :             Q[alpha][beta] = false ;
     261             :         }
     262             :     }
     263             :   };
     264             : 
     265          16 :   mCRL2log(log::debug) << "-----  After Filter ------\nExists2: ";
     266          16 :   mCRL2log(log::debug) << print_structure(exists2);
     267          16 :   mCRL2log(log::debug) << "\nForall2: ";
     268          16 :   mCRL2log(log::debug) << print_structure(forall2);
     269          16 :   mCRL2log(log::debug) << "\nReady Preorder: ";
     270          16 :   mCRL2log(log::debug) << print_relation(s_Pi,Q);  
     271          16 : }
     272             : 
     273             : template <class LTS_TYPE>
     274           0 : std::string ready_sim_partitioner<LTS_TYPE>::print_structure(hash_table2* struc)
     275             : {
     276             :   using namespace mcrl2::core;
     277           0 :   std::stringstream result;
     278           0 :   result << "{";
     279           0 :   hash_table2_iterator i(struc);
     280           0 :   for (; !i.is_end(); ++i)
     281             :   {
     282           0 :     result << "(" << i.get_x() << "," << mcrl2::lts::pp(aut.action_label(i.get_y()))<< "),";
     283             :   }
     284           0 :   result << "}";
     285           0 :   return result.str();  
     286           0 : }
     287             : 
     288             : template <class LTS_TYPE>
     289          16 : ready_sim_partitioner<LTS_TYPE>::~ready_sim_partitioner()
     290             : {
     291          16 :   delete exists2;
     292          16 :   delete forall2;
     293          32 : }
     294             : 
     295             :  
     296             : } // namespace detail
     297             : } // namespace lts
     298             : } // namespacemcrl2
     299             : #endif