Line data    Source code

       1             : // Author(s): Wieger Wesselink
       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             : #ifndef MCRL2_SYMBOLIC_SUMMAND_GROUP_H
      11             : #define MCRL2_SYMBOLIC_SUMMAND_GROUP_H
      12             : 
      13             : #ifdef MCRL2_ENABLE_SYLVAN
      14             : 
      15             : #include "mcrl2/atermpp/aterm_list.h"
      16             : #include "mcrl2/core/detail/print_utility.h"
      17             : #include "mcrl2/data/data_expression.h"
      18             : #include "mcrl2/symbolic/ordering.h"
      19             : #include "mcrl2/symbolic/utility.h"
      20             : 
      21             : #include <boost/dynamic_bitset.hpp>
      22             : 
      23             : #include <functional>
      24             : #include <iostream>
      25             : #include <vector>
      26             : 
      27             : namespace mcrl2::symbolic
      28             : {
      29             : 
      30             : /// \brief Computes for both the read and write parameters their positions in the zipped transition relation.
      31             : inline std::pair<std::vector<std::size_t>, std::vector<std::size_t>> compute_read_write_pos(const std::vector<std::size_t>& read, const std::vector<std::size_t>& write);
      32             : 
      33             : /// \brief Compact the vector to avoid repeated values at the end.
      34             : inline std::vector<std::uint32_t> optimise_project(const std::vector<std::uint32_t>& Ip_values);
      35             : 
      36             : /// \brief A transition relation over a single set of read and write parameters for a group of summands.
      37             : struct summand_group
      38             : {
      39             :   /// \brief The information of a single summand relevant for symbolic exploration.
      40             :   struct summand
      41             :   {
      42             :     data::data_expression condition;
      43             :     data::variable_list variables; // the summand variables
      44             :     std::vector<data::data_expression> next_state; // the projected next state vector
      45             :     std::vector<int> copy; // copy node information that is needed by sylvan::ldds::relprod
      46             : 
      47             :     summand(const data::data_expression& condition_, const data::variable_list& variables_, const std::vector<data::data_expression>& next_state_, const std::vector<int>& copy_)
      48             :       : condition(condition_), variables(variables_), next_state(next_state_), copy(copy_)
      49             :     {}
      50             :   };
      51             : 
      52             :   std::vector<summand> summands; // the summands of the group
      53             :   std::vector<data::variable> read_parameters; // the read parameters
      54             :   std::vector<std::size_t> read; // indices of the read parameters
      55             :   std::vector<std::size_t> read_pos; // indices of the read parameters in a zipped transition xy
      56             :   std::vector<data::variable> write_parameters; // the write parameters
      57             :   std::vector<std::size_t> write; // indices of the write parameters
      58             :   std::vector<std::size_t> write_pos; // indices of the write parameters in a zipped transition xy
      59             : 
      60             :   sylvan::ldds::ldd L; // the projected transition relation
      61             :   sylvan::ldds::ldd Ldomain; // the domain of L
      62             :   sylvan::ldds::ldd Ir; // meta data needed by sylvan::ldds::relprod
      63             :   sylvan::ldds::ldd Ip; // meta data needed by sylvan::ldds::project
      64             : 
      65             :   double learn_time = 0.0; // The time to learn the transitions for this group.
      66             :   std::size_t learn_calls = 0; // Number of learn transition calls.
      67             : 
      68             :   summand_group(const data::variable_list& process_parameters, const boost::dynamic_bitset<>& read_write_pattern, bool has_action)
      69             :   {
      70             :     using namespace sylvan::ldds;
      71             :     using utilities::detail::as_vector;
      72             : 
      73             :     std::size_t n = process_parameters.size();
      74             : 
      75             :     // Indicates for every position whether the parameter should be projected on (for read dependencies).
      76             :     std::vector<std::uint32_t> Ip_values;
      77             : 
      78             :     for (std::size_t j = 0; j < n; j++)
      79             :     {
      80             :       bool is_read = read_write_pattern[2*j];
      81             :       bool is_write = read_write_pattern[2*j + 1];
      82             :       Ip_values.push_back(is_read ? 1 : 0);
      83             :       if (is_read)
      84             :       {
      85             :         read.push_back(j);
      86             :       }
      87             :       if (is_write)
      88             :       {
      89             :         write.push_back(j);
      90             :       }
      91             :     }
      92             : 
      93             :     Ip_values = optimise_project(Ip_values);
      94             :     read_parameters = project(as_vector(process_parameters), read);
      95             :     write_parameters = project(as_vector(process_parameters), write);
      96             :     L = empty_set();
      97             :     Ldomain = empty_set();
      98             :     Ir = compute_meta(read, write, has_action); // Note, action is always added the end.
      99             :     Ip = cube(Ip_values);
     100             : 
     101             :     std::tie(read_pos, write_pos) = compute_read_write_pos(read, write);
     102             :   }
     103             : 
     104             :   // Construct a summand group from the given parameters, where read_parameters and write_parameters have the same order as process_parameters.
     105           0 :   summand_group(const data::variable_list& process_parameters, std::vector<data::variable> _read_parameters, std::vector<data::variable> _write_parameters, bool has_action)
     106           0 :   {
     107             :     using namespace sylvan::ldds;
     108           0 :     read_parameters = _read_parameters;
     109           0 :     write_parameters = _write_parameters;
     110             :     
     111           0 :     std::vector<std::uint32_t> Ip_values;
     112             : 
     113           0 :     std::size_t index = 0;
     114           0 :     std::size_t read_index = 0;
     115           0 :     std::size_t write_index = 0;
     116           0 :     for (const data::variable& parameter : process_parameters)
     117             :     {
     118           0 :       if (read_index < read_parameters.size() && parameter == read_parameters[read_index])
     119             :       {
     120           0 :         read_index++;
     121           0 :         read.emplace_back(index);
     122           0 :         Ip_values.emplace_back(1);
     123             :       }
     124             :       else
     125             :       {
     126           0 :         Ip_values.emplace_back(0);
     127             :       }
     128             : 
     129           0 :       if (write_index < write_parameters.size() && parameter == write_parameters[write_index])
     130             :       {
     131           0 :         write_index++;
     132           0 :         write.emplace_back(index);
     133             :       }
     134             : 
     135           0 :       ++index;
     136             :     }
     137             : 
     138           0 :     Ip_values = optimise_project(Ip_values);
     139             :     
     140           0 :     L = empty_set();
     141           0 :     Ldomain = empty_set();
     142           0 :     Ir = compute_meta(read, write, has_action); // Note, action is always added the end.
     143           0 :     Ip = cube(Ip_values);
     144             : 
     145           0 :     std::tie(read_pos, write_pos) = compute_read_write_pos(read, write);
     146           0 :   }
     147             : };
     148             : 
     149             : /// \brief Prints the information of this summand group.
     150             : inline
     151             : std::ostream& operator<<(std::ostream& out, const summand_group& x)
     152             : {
     153             :   using namespace sylvan::ldds;
     154             :   for (const auto& smd: x.summands)
     155             :   {
     156             :     out << "condition = " << smd.condition << std::endl;
     157             :     out << "variables = " << core::detail::print_list(smd.variables) << std::endl;
     158             :     out << "next state = " << core::detail::print_list(smd.next_state) << std::endl;
     159             :     out << "copy = " << core::detail::print_list(smd.copy) << std::endl;
     160             : 
     161             :     std::vector<std::string> assignments;
     162             :     auto vi = x.write_parameters.begin();
     163             :     auto ni = smd.next_state.begin();
     164             :     for (; vi != x.write_parameters.end(); ++vi, ++ni)
     165             :     {
     166             :       assignments.push_back(data::pp(*vi) + " := " + data::pp(*ni));
     167             :     }
     168             :     out << "assignments = " << core::detail::print_list(assignments) << std::endl;
     169             :   }
     170             :   out << "read = " << core::detail::print_list(x.read) << std::endl;
     171             :   out << "read parameters = " << core::detail::print_list(x.read_parameters) << std::endl;
     172             :   out << "write = " << core::detail::print_list(x.write) << std::endl;
     173             :   out << "write parameters = " << core::detail::print_list(x.write_parameters) << std::endl;
     174             :   out << "L = " << print_ldd(x.L) << std::endl;
     175             :   out << "Ir = " << print_ldd(x.Ir) << std::endl;
     176             :   out << "Ip = " << print_ldd(x.Ip) << std::endl;
     177             :   return out;
     178             : }
     179             : 
     180           0 : std::pair<std::vector<std::size_t>, std::vector<std::size_t>> compute_read_write_pos(const std::vector<std::size_t>& read, const std::vector<std::size_t>& write)
     181             : {
     182           0 :   std::vector<std::size_t> rpos;
     183           0 :   std::vector<std::size_t> wpos;
     184             : 
     185           0 :   auto ri = read.begin();
     186           0 :   auto wi = write.begin();
     187           0 :   std::size_t index = 0;
     188           0 :   while (ri != read.end() && wi != write.end())
     189             :   {
     190           0 :     if (*ri <= *wi)
     191             :     {
     192           0 :       rpos.push_back(index++);
     193           0 :       ri++;
     194             :     }
     195             :     else
     196             :     {
     197           0 :       wpos.push_back(index++);
     198           0 :       wi++;
     199             :     }
     200             :   }
     201           0 :   while (ri != read.end())
     202             :   {
     203           0 :     rpos.push_back(index++);
     204           0 :     ri++;
     205             :   }
     206           0 :   while (wi != write.end())
     207             :   {
     208           0 :     wpos.push_back(index++);
     209           0 :     wi++;
     210             :   }
     211             : 
     212           0 :   return { rpos, wpos };
     213           0 : }
     214             : 
     215             : 
     216           0 : std::vector<std::uint32_t> optimise_project(const std::vector<std::uint32_t>& Ip_values)
     217             : {
     218           0 :   if (Ip_values.size() > 1)
     219             :   {
     220             :     // The index after which all values in Ip_values are the same (at least two entries).
     221           0 :     int i = Ip_values.size() - 1;
     222           0 :     while (i > 0 && Ip_values[i] == Ip_values.back())
     223             :     {
     224           0 :       --i;
     225             :     }
     226             : 
     227           0 :     std::vector<std::uint32_t> result(Ip_values.begin(), Ip_values.begin() + i + 2);
     228           0 :     if (result.back() == 0)
     229             :     {
     230           0 :       result.back() = static_cast<std::uint32_t>(-2);
     231             :     }
     232             :     else
     233             :     {
     234           0 :       result.back() = static_cast<std::uint32_t>(-1);
     235             :     }
     236           0 :     return result;
     237           0 :   }
     238             : 
     239           0 :   return Ip_values;
     240             : }
     241             : 
     242             : } // namespace mcrl2::symbolic
     243             : 
     244             : #endif // MCRL2_ENABLE_SYLVAN
     245             : 
     246             : #endif // MCRL2_SYMBOLIC_SUMMAND_GROUP_H