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_ALTERNATIVE_RELPROD_H
      11             : #define MCRL2_SYMBOLIC_ALTERNATIVE_RELPROD_H
      12             : 
      13             : #ifdef MCRL2_ENABLE_SYLVAN
      14             : 
      15             : #include "mcrl2/symbolic/summand_group.h"
      16             : 
      17             : #include <sylvan_ldd.hpp>
      18             : 
      19             : #include <limits>
      20             : #include <stdint.h>
      21             : #include <vector>
      22             : 
      23             : namespace mcrl2::symbolic
      24             : {
      25             : 
      26             : constexpr std::uint32_t relprod_ignore = std::numeric_limits<std::uint32_t>::max(); // used by alternative_relprod/relprev
      27             : 
      28             : // A very inefficient implementation of relprod, that matches the specification closely
      29           0 : sylvan::ldds::ldd alternative_relprod(const sylvan::ldds::ldd& todo, const summand_group& R)
      30             : {
      31             :   using namespace sylvan::ldds;
      32             : 
      33           0 :   auto split = [&](const std::vector<std::uint32_t>& xy)
      34             :   {
      35           0 :     std::vector<std::uint32_t> x;
      36           0 :     std::vector<std::uint32_t> y;
      37           0 :     for (std::size_t j: R.read_pos)
      38             :     {
      39           0 :       x.push_back(xy[j]);
      40             :     }
      41           0 :     for (std::size_t j: R.write_pos)
      42             :     {
      43           0 :       y.push_back(xy[j]);
      44             :     }
      45           0 :     return std::make_pair(x, y);
      46           0 :   };
      47             : 
      48           0 :   auto match = [&](const std::vector<std::uint32_t>& x, const std::vector<std::uint32_t>& x_)
      49             :   {
      50           0 :     for (std::size_t j = 0; j < x_.size(); j++)
      51             :     {
      52           0 :       if (x[R.read[j]] != x_[j])
      53             :       {
      54           0 :         return false;
      55             :       }
      56             :     }
      57           0 :     return true;
      58           0 :   };
      59             : 
      60           0 :   auto replace = [&](std::vector<std::uint32_t> x, const std::vector<std::uint32_t>& y_)
      61             :   {
      62           0 :     for (std::size_t j = 0; j < y_.size(); j++)
      63             :     {
      64           0 :       if (y_[j] != relprod_ignore)
      65             :       {
      66           0 :         x[R.write[j]] = y_[j];
      67             :       }
      68             :     }
      69           0 :     return x;
      70           0 :   };
      71             : 
      72           0 :   ldd result = empty_set();
      73             : 
      74           0 :   auto todo_elements = ldd_solutions(todo);
      75           0 :   for (const std::vector<std::uint32_t>& xy: ldd_solutions(R.L))
      76             :   {
      77           0 :     auto [x_, y_] = split(xy);
      78           0 :     for (const auto& x: todo_elements)
      79             :     {
      80           0 :       if (match(x, x_))
      81             :       {
      82           0 :         auto y = replace(x, y_);
      83           0 :         result = union_cube(result, y);
      84           0 :       }
      85             :     }
      86           0 :   }
      87           0 :   return result;
      88           0 : }
      89             : 
      90             : // A very inefficient implementation of relprev, that matches the specification closely
      91           0 : sylvan::ldds::ldd alternative_relprev(const sylvan::ldds::ldd& Y, const summand_group& R, const sylvan::ldds::ldd& X)
      92             : {
      93             :   using namespace sylvan::ldds;
      94             : 
      95           0 :   ldd result = empty_set();
      96           0 :   for (const std::vector<std::uint32_t>& x_values: ldd_solutions(X))
      97             :   {
      98           0 :     ldd x = cube(x_values);
      99           0 :     ldd y = alternative_relprod(x, R);
     100           0 :     if (intersect(y, Y) != empty_set())
     101             :     {
     102           0 :       result = union_(result, x);
     103             :     }
     104           0 :   }
     105           0 :   return result;
     106           0 : }
     107             : 
     108             : } // namespace mcrl2::symbolic
     109             : 
     110             : #endif // MCRL2_ENABLE_SYLVAN
     111             : 
     112             : #endif // MCRL2_SYMBOLIC_ALTERNATIVE_RELPROD_H