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_LPS_SYMBOLIC_PRINT_H
      11             : #define MCRL2_LPS_SYMBOLIC_PRINT_H
      12             : 
      13             : #ifdef MCRL2_ENABLE_SYLVAN
      14             : 
      15             : 
      16             : #include "mcrl2/data/data_expression.h"
      17             : #include "mcrl2/data/undefined.h"
      18             : #include "mcrl2/symbolic/print.h"
      19             : #include "mcrl2/symbolic/alternative_relprod.h"
      20             : #include "mcrl2/symbolic/data_index.h"
      21             : 
      22             : #include <sylvan_ldd.hpp>
      23             : 
      24             : #include <vector>
      25             : #include <cmath>
      26             : #include <cfenv>
      27             : 
      28             : namespace mcrl2::symbolic {
      29             : 
      30             : namespace 
      31             : {
      32             : 
      33             : /// \brief Converts a state vector of indices to a vector of the corresponding data expressions. 
      34           0 : std::vector<data::data_expression> ldd2state(const std::vector<data_expression_index>& data_index, const std::vector<std::uint32_t>& x)
      35             : {
      36           0 :   std::vector<data::data_expression> result;
      37           0 :   for (std::size_t i = 0; i < x.size(); i++)
      38             :   {
      39           0 :     if (x[i] == relprod_ignore)
      40             :     {
      41           0 :       result.push_back(data::undefined_data_expression());
      42             :     }
      43             :     else
      44             :     {
      45           0 :       result.push_back(data_index[i][x[i]]);
      46             :     }
      47             :   }
      48           0 :   return result;
      49           0 : }
      50             : 
      51             : /// \brief Converts a state vector of indices projected on used to a vector of the corresponding data expressions. 
      52           0 : std::vector<data::data_expression> ldd2state(const std::vector<data_expression_index>& data_index, const std::vector<std::uint32_t>& x, const std::vector<std::size_t>& used)
      53             : {
      54           0 :   std::vector<data::data_expression> result;
      55           0 :   for (std::size_t i = 0; i < used.size(); i++)
      56             :   {
      57           0 :     if (x[i] == relprod_ignore)
      58             :     {
      59           0 :       result.push_back(data::undefined_data_expression());
      60             :     }
      61             :     else
      62             :     {
      63           0 :       result.push_back(data_index[used[i]][x[i]]);
      64             :     }
      65             :   }
      66           0 :   return result;
      67           0 : }
      68             : 
      69             : /// \brief Prints a state vector of indices as a list of the corresponding data expressions. 
      70             : inline
      71           0 : std::string print_state(const std::vector<data_expression_index>& data_index, const std::vector<std::uint32_t>& x)
      72             : {
      73           0 :   return core::detail::print_list(ldd2state(data_index, x));
      74             : }
      75             : 
      76             : /// \brief Prints a state vector of indices projected on used as a list of the corresponding data expressions. 
      77             : inline
      78           0 : std::string print_state(const std::vector<data_expression_index>& data_index, const std::vector<std::uint32_t>& x, const std::vector<std::size_t>& used)
      79             : {
      80           0 :   return core::detail::print_list(ldd2state(data_index, x, used));
      81             : }
      82             : 
      83             : } // internal
      84             : 
      85             : /// \brief Prints the set of state vectors represented by x.
      86             : inline
      87           0 : std::string print_states(const std::vector<data_expression_index>& data_index, const sylvan::ldds::ldd& x)
      88             : {
      89           0 :   std::ostringstream out;
      90           0 :   auto solutions = ldd_solutions(x);
      91           0 :   bool multiline = solutions.size() > 1;
      92           0 :   std::string sep = multiline ? ",\n" : ", ";
      93             : 
      94           0 :   out << "{" << (multiline ? "\n" : " ");
      95           0 :   for (std::size_t i = 0; i < solutions.size(); i++)
      96             :   {
      97           0 :     if (i > 0)
      98             :     {
      99           0 :       out << sep;
     100             :     }
     101           0 :     out << print_state(data_index, solutions[i]);
     102             :   }
     103           0 :   out << (multiline ? "\n" : " ") << "}";
     104           0 :   return out.str();
     105           0 : }
     106             : 
     107             : /// \brief Prints the set of state vectors represented by x projected on indices in used.
     108             : inline
     109             : std::string print_states(const std::vector<data_expression_index>& data_index, const sylvan::ldds::ldd& x, const std::vector<std::size_t>& used)
     110             : {
     111             :   std::ostringstream out;
     112             :   auto solutions = ldd_solutions(x);
     113             :   bool multiline = solutions.size() > 1;
     114             :   std::string sep = multiline ? ",\n" : ", ";
     115             : 
     116             :   out << "{" << (multiline ? "\n" : " ");
     117             :   for (std::size_t i = 0; i < solutions.size(); i++)
     118             :   {
     119             :     if (i > 0)
     120             :     {
     121             :       out << sep;
     122             :     }
     123             :     out << print_state(data_index, solutions[i], used);
     124             :   }
     125             :   out << (multiline ? "\n" : " ") << "}";
     126             :   return out.str();
     127             : }
     128             : 
     129             : namespace 
     130             : {
     131             : 
     132             : /// \brief Print a transition vector as 'x -> y' where x is the from vector and y the to vector.
     133             : /* This funcion is not used. 
     134             : std::string print_transition(const std::vector<data_expression_index>& data_index, const std::vector<std::uint32_t>& xy)
     135             : {
     136             :   std::size_t n = xy.size() / 2;
     137             :   std::vector<std::uint32_t> x(n);
     138             :   std::vector<std::uint32_t> y(n);
     139             :   for (std::size_t i = 0; i < n; i++)
     140             :   {
     141             :     x[i] = xy[2*i];
     142             :     y[i] = xy[2*i+1];
     143             :   }
     144             :   return print_state(data_index, x) + " -> " + print_state(data_index, y);
     145             : }
     146             : */
     147             : 
     148             : } // internal
     149             : 
     150             : /// \brief Print a transition vector as 'x -> y' where x is the from vector and y the to vector based on the read and write indices.
     151           0 : std::string print_transition(const std::vector<data_expression_index>& data_index, const std::uint32_t* xy, const std::vector<std::size_t>& read, const std::vector<std::size_t>& write)
     152             : {
     153           0 :   std::vector<std::uint32_t> x;
     154           0 :   std::vector<std::uint32_t> y;
     155           0 :   auto ri = read.begin();
     156           0 :   auto wi = write.begin();
     157           0 :   auto xyi = xy;
     158           0 :   while (ri != read.end() && wi != write.end())
     159             :   {
     160           0 :     if (*ri <= *wi)
     161             :     {
     162           0 :       ri++;
     163           0 :       x.push_back(*xyi++);
     164             :     }
     165             :     else
     166             :     {
     167           0 :       wi++;
     168           0 :       y.push_back(*xyi++);
     169             :     }
     170             :   }
     171           0 :   while (ri != read.end())
     172             :   {
     173           0 :     ri++;
     174           0 :     x.push_back(*xyi++);
     175             :   }
     176           0 :   while (wi != write.end())
     177             :   {
     178           0 :     wi++;
     179           0 :     y.push_back(*xyi++);
     180             :   }
     181           0 :   return print_state(data_index, x, read) + " -> " + print_state(data_index, y, write);
     182           0 : }
     183             : 
     184             : /// \brief Prints a short vector transition relation R explicitly as 'x -> y' for every transition  where x is the from vector and y the to vector based on the read and write indices.
     185           0 : std::string print_relation(const std::vector<data_expression_index>& data_index, const sylvan::ldds::ldd& R, const std::vector<std::size_t>& read, const std::vector<std::size_t>& write)
     186             : {
     187           0 :   std::ostringstream out;
     188           0 :   for (const std::vector<std::uint32_t>& xy: ldd_solutions(R))
     189             :   {
     190           0 :     out << print_transition(data_index, xy.data(), read, write) << std::endl;
     191           0 :   }
     192           0 :   return out.str();
     193           0 : }
     194             : 
     195             : /// \brief Prints the number of elements represented by the ldd L and optionally also include the number of nodes of L.
     196           0 : std::string print_size(const sylvan::ldds::ldd& L, bool print_exact, bool print_nodecount)
     197             : {
     198           0 :   std::ostringstream out;
     199           0 :   if (print_exact)
     200             :   {
     201             :     // Use this ugly construct to figure out if the conversion succeeded, should have been an exception or sum type.
     202             :     std::fenv_t save_env;
     203           0 :     std::feholdexcept(&save_env);
     204             : 
     205           0 :     std::feclearexcept(FE_ALL_EXCEPT);
     206           0 :     long long exact = std::llround(satcount(L));
     207           0 :     if (std::fetestexcept(FE_INVALID))
     208             :     {
     209             :       //  the result of the rounding is outside the range of the return type.
     210           0 :       out << satcount(L);
     211             :     }
     212             :     else
     213             :     {
     214           0 :       out << exact;
     215             :     }
     216             :     
     217           0 :     std::feupdateenv(&save_env);
     218             :   }
     219             :   else
     220             :   {
     221           0 :     out << satcount(L);
     222             :   }
     223             : 
     224           0 :   if (print_nodecount)
     225             :   {
     226           0 :     out << "[" << nodecount(L) << "]";
     227             :   }
     228           0 :   return out.str();
     229           0 : }
     230             : 
     231             : } // namespace mcrl2::symbolic
     232             : 
     233             : #endif // MCRL2_ENABLE_SYLVAN
     234             : 
     235             : #endif // MCRL2_LPS_SYMBOLIC_PRINT_H