Line data    Source code

       1             : // Author(s): Gijs Kant
       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 mcrl2/pbes/detail/pbes_greybox_interface.h
      10             : /// \brief The pbes_greybox_interface class provides a wrapper for the
      11             : /// parity_game_generator classes, for use in the PBES explorer.
      12             : 
      13             : #ifndef MCRL2_PBES_DETAIL_PBES_GREYBOX_INTERFACE_H
      14             : #define MCRL2_PBES_DETAIL_PBES_GREYBOX_INTERFACE_H
      15             : 
      16             : #include "mcrl2/pbes/parity_game_generator.h"
      17             : 
      18             : // This include is necessary for ltsmin related workarounds.
      19             : #include "mcrl2/lps/ltsmin.h"
      20             : 
      21             : namespace mcrl2 {
      22             : 
      23             : namespace pbes_system {
      24             : 
      25             : namespace detail {
      26             : 
      27             :   /// A class that provides initial state and successors functions for PBESs,
      28             :   /// allowing to explore the PBES as a transition system, where states are
      29             :   /// instantiated propositional variables.
      30             :   class pbes_greybox_interface: public parity_game_generator
      31             :   {
      32             :     protected:
      33             :       data::rewriter datar;
      34             :       pbes_system::enumerate_quantifiers_rewriter pbes_rewriter;
      35             : 
      36             :     public:
      37             :     /// \brief Constructor.
      38             :     /// \param p A PBES
      39             :     /// \param true_false_dependencies If true, nodes are generated for the values <tt>true</tt> and <tt>false</tt>.
      40             :     /// \param is_min_parity If true a min-parity game is produced, otherwise a max-parity game
      41             :     /// \param rewrite_strategy The rewrite engine to use. (Default: jitty)
      42           6 :     pbes_greybox_interface(pbes& p, bool true_false_dependencies = false, bool is_min_parity = true, data::rewriter::strategy rewrite_strategy = data::jitty)
      43           6 :       : parity_game_generator(p, true_false_dependencies, is_min_parity, rewrite_strategy),
      44           6 :         datar(p.data()),
      45          12 :         pbes_rewriter(datar, p.data(), true)
      46             :     {
      47           6 :       initialize_generation();
      48           6 :     }
      49             : 
      50          12 :     virtual ~pbes_greybox_interface() {}
      51             : 
      52             :     /// \brief Returns the initial state, rewritten and simplified.
      53             :     /// \return the initial state.
      54          12 :     propositional_variable_instantiation get_initial_state()
      55             :     {
      56             :       //std::clog << "get_initial_state()" << std::endl;
      57          12 :       propositional_variable_instantiation phi = atermpp::down_cast<propositional_variable_instantiation>(rewrite_and_simplify_expression(m_pbes.initial_state()));
      58             :       //std::clog << "  phi = " << phi << std::endl;
      59          12 :       return phi;
      60             :     }
      61             : 
      62             :     /// \brief Rewrites and simplifies an expression.
      63             :     /// \param e a PBES expression.
      64             :     /// \return the result of the rewrite.
      65          52 :     pbes_expression rewrite_and_simplify_expression(const pbes_expression& e, const bool /* convert_data_to_pbes */ = true)
      66             :     {
      67          52 :       data::rewriter::substitution_type sigma;
      68          52 :       pbes_expression phi = pbes_rewriter(e, sigma);
      69         104 :       return phi;
      70          52 :     }
      71             : 
      72             :     /// \brief Returns the equation for variable s.
      73             :     /// \param s the identifier string of a variable.
      74             :     /// \return the equation for variable s.
      75          14 :     pbes_equation get_pbes_equation(const core::identifier_string& s)
      76             :     {
      77          14 :       const pbes_equation& e = *m_pbes_equation_index[s];
      78          14 :       return e;
      79             :     }
      80             : 
      81             :     /// \brief Returns the successors of a state, which is a instantiated propositional variable.
      82             :     /// Fetches the right hand side of the equation for the variable of the state,
      83             :     /// Substitutes the variables in the right hand side with the parameter variables in the state
      84             :     /// and rewrites the expression.
      85             :     /// \param phi An instantiated propositional variable
      86             :     /// \return The set of variable instantiations (successor states) that appear in the rewritten
      87             :     /// right hand side expression.
      88         866 :     std::set<pbes_expression> get_successors(const pbes_expression& phi)
      89             :     {
      90             :       //std::clog << "get_successors(psi)" << std::endl;
      91         866 :       initialize_generation();
      92             : 
      93         866 :       std::set<pbes_expression> result;
      94         866 :       mCRL2log(log::debug) << "Generating equation for expression " << phi << std::endl;
      95             : 
      96             :       // expand the right hand side if needed
      97         866 :       pbes_expression psi = expand_rhs(phi);
      98             : 
      99             :       // top_flatten
     100         866 :       if (is_propositional_variable_instantiation(psi))
     101             :       {
     102         512 :         result.insert(psi);
     103             :       }
     104         354 :       else if (is_and(psi))
     105             :       {
     106         354 :         std::set<pbes_expression> terms = split_and(psi);
     107        1522 :         for (const auto & term : terms)
     108             :         {
     109        1168 :           result.insert(term);
     110             :         }
     111         354 :       }
     112           0 :       else if (is_or(psi))
     113             :       {
     114           0 :         std::set<pbes_expression> terms = split_or(psi);
     115           0 :         for (const auto & term : terms)
     116             :         {
     117           0 :           result.insert(term);
     118             :         }
     119           0 :       }
     120           0 :       else if (is_true(psi))
     121             :       {
     122           0 :         if (m_true_false_dependencies)
     123             :         {
     124           0 :           result.insert(true_());
     125             :         }
     126             :       }
     127           0 :       else if (is_false(psi))
     128             :       {
     129           0 :         if (m_true_false_dependencies)
     130             :         {
     131           0 :           result.insert(false_());
     132             :         }
     133             :       }
     134             :       else
     135             :       {
     136           0 :         throw(std::runtime_error("Error in pbes_greybox_interface: unexpected expression " + pbes_system::pp(psi) + "\n" + pp(psi)));
     137             :       }
     138         866 :       mCRL2log(log::debug) << print_successors(result);
     139        1732 :       return result;
     140         866 :     }
     141             : 
     142             :     /// \brief Expands a formula expr for a instantiated state variable psi, which means
     143             :     /// substituting the variables in expr by the parameter values in psi and rewriting the
     144             :     /// expression.
     145             :     /// \param psi the instantiated propositional variable.
     146             :     /// \param expr the expression to be expanded.
     147             :     /// \return the result of the expansion.
     148             :     virtual
     149         866 :     pbes_expression expand_group(const pbes_expression& psi, const pbes_expression& expr)
     150             :     {
     151             :       // expand the right hand side if needed
     152         866 :       if (is_propositional_variable_instantiation(psi))
     153             :       {
     154         866 :         const pbes_equation& pbes_eqn = *m_pbes_equation_index[atermpp::down_cast<propositional_variable_instantiation>(psi).name()];
     155             : 
     156         866 :         mCRL2log(log::trace) << "Expanding right hand side of formula " << psi << std::endl << "  rhs: " << expr << " into ";
     157             : 
     158         866 :         pbes_expression result;
     159             : 
     160         866 :         data::rewriter::substitution_type sigma;
     161         866 :         make_substitution(pbes_eqn.variable().parameters(), atermpp::down_cast<propositional_variable_instantiation>(psi).parameters(),sigma);
     162         866 :         result = pbes_rewriter(expr,sigma);
     163             : 
     164         866 :         mCRL2log(log::trace) << result << std::endl;
     165         866 :         return result;
     166         866 :       }
     167           0 :       return psi;
     168             :     }
     169             : 
     170             :     /// \brief Prints the set of successors states
     171             :     /// \param successors a set of successor expressions.
     172             :     /// \return a string representation of successors.
     173             :     virtual
     174        1732 :     std::string print_successors(const std::set<pbes_expression>& successors)
     175             :     {
     176        1732 :       std::ostringstream out;
     177        1732 :       out << "-- print_successors --" << std::endl;
     178        5092 :       for (const auto & successor : successors)
     179             :       {
     180        3360 :         out << " * " << successor << std::endl;
     181             :       }
     182        3464 :       return out.str();
     183        1732 :     }
     184             : 
     185             :     /// \brief Returns the successors of a state, which is a instantiated propositional variable,
     186             :     /// for a certain 'transition group'.
     187             :     /// Checks if the name of the state variable equals the variable associated with the transition group
     188             :     /// var. If so, in the expression expr the variables are substituted with the parameter variables in the state
     189             :     /// and the expression is rewritten.
     190             :     /// \param phi An instantiated propositional variable
     191             :     /// \param var The variable name associated with the transition group.
     192             :     /// \param expr The expression associated with the transition group.
     193             :     /// \return The set of variable instantiations (successor states) that appear in the rewritten
     194             :     /// expression.
     195         866 :     std::set<pbes_expression> get_successors(const pbes_expression& phi, const std::string& var, const pbes_expression& expr)
     196             :     {
     197         866 :       initialize_generation();
     198             : 
     199         866 :       std::set<pbes_expression> result;
     200        1732 :       mCRL2log(log::debug) << "Generating equation for expression "  << phi << " (var = " << var
     201         866 :                                                                                                << ", expr = " << expr << ")" <<std::endl;
     202             : 
     203         866 :       assert(is_propositional_variable_instantiation(phi));
     204         866 :       std::string varname = atermpp::down_cast<propositional_variable_instantiation>(phi).name();
     205             :       // check that varname for current group equals varname.
     206         866 :       if (varname==var)
     207             :       {
     208             :         // expand the right hand side if needed
     209         866 :         pbes_expression psi = expand_group(phi, expr);
     210             : 
     211             :         // top_flatten
     212         866 :         if (is_propositional_variable_instantiation(psi))
     213             :         {
     214         512 :           result.insert(psi);
     215             :         }
     216         354 :         else if (is_and(psi))
     217             :         {
     218         354 :           std::set<pbes_expression> terms = split_and(psi);
     219        1522 :           for (const auto & term : terms)
     220             :           {
     221        1168 :             result.insert(term);
     222             :           }
     223         354 :         }
     224           0 :         else if (is_or(psi))
     225             :         {
     226           0 :           std::set<pbes_expression> terms = split_or(psi);
     227           0 :           for (const auto & term : terms)
     228             :           {
     229           0 :             result.insert(term);
     230             :           }
     231           0 :         }
     232           0 :         else if (is_true(psi))
     233             :         {
     234           0 :           if (m_true_false_dependencies)
     235             :           {
     236           0 :             result.insert(true_());
     237             :           }
     238             :         }
     239           0 :         else if (is_false(psi))
     240             :         {
     241           0 :           if (m_true_false_dependencies)
     242             :           {
     243           0 :             result.insert(false_());
     244             :           }
     245             :         }
     246             :         else
     247             :         {
     248           0 :           throw(std::runtime_error("Error in pbes_greybox_interface: unexpected expression " + pbes_system::pp(psi)));
     249             :         }
     250         866 :       }
     251         866 :       mCRL2log(log::debug) << print_successors(result);
     252        1732 :       return result;
     253         866 :     }
     254             : 
     255             : 
     256             :   };
     257             : 
     258             : } // namespace detail
     259             : 
     260             : } // namespace pbes_system
     261             : 
     262             : } // namespace mcrl2
     263             : 
     264             : #endif // MCRL2_PBES_DETAIL_PBES_GREYBOX_INTERFACE_H