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             : /// \file mcrl2/pbes/detail/lps2pbes_sat.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_DETAIL_LPS2PBES_SAT_H
      13             : #define MCRL2_PBES_DETAIL_LPS2PBES_SAT_H
      14             : 
      15             : #include "mcrl2/data/detail/data_utility.h"
      16             : #include "mcrl2/data/detail/find.h"
      17             : #include "mcrl2/modal_formula/replace.h"
      18             : #include "mcrl2/pbes/detail/lps2pbes_utility.h"
      19             : 
      20             : namespace mcrl2 {
      21             : 
      22             : namespace pbes_system {
      23             : 
      24             : namespace detail {
      25             : 
      26             : template <typename TermTraits>
      27             : typename TermTraits::term_type Sat(const lps::multi_action& a,
      28             :                                    const action_formulas::action_formula& x,
      29             :                                    data::set_identifier_generator& id_generator,
      30             :                                    TermTraits tr
      31             :                                   );
      32             : 
      33             : template <typename Derived, typename TermTraits>
      34             : struct sat_traverser: public action_formulas::action_formula_traverser<Derived>
      35             : {
      36             :   typedef action_formulas::action_formula_traverser<Derived> super;
      37             :   typedef TermTraits tr;
      38             :   typedef typename tr::term_type expression_type;
      39             : 
      40             :   using super::enter;
      41             :   using super::leave;
      42             :   using super::apply;
      43             : 
      44             :   const lps::multi_action& a;
      45             :   data::set_identifier_generator& id_generator;
      46             :   std::vector<expression_type> result_stack;
      47             : 
      48        1213 :   sat_traverser(const lps::multi_action& a_, data::set_identifier_generator& id_generator_, TermTraits)
      49        1213 :     : a(a_), id_generator(id_generator_)
      50        1213 :   {}
      51             : 
      52             :   Derived& derived()
      53             :   {
      54             :     return static_cast<Derived&>(*this);
      55             :   }
      56             : 
      57        1315 :   void push(const expression_type& x)
      58             :   {
      59        1315 :     result_stack.push_back(x);
      60        1315 :   }
      61             : 
      62        1315 :   const expression_type& top() const
      63             :   {
      64        1315 :     return result_stack.back();
      65             :   }
      66             : 
      67         102 :   expression_type pop()
      68             :   {
      69         102 :     expression_type result = top();
      70         102 :     result_stack.pop_back();
      71         102 :     return result;
      72             :   }
      73             : 
      74           0 :   void leave(const data::data_expression& x)
      75             :   {
      76           0 :     push(x);
      77           0 :   }
      78             : 
      79         813 :   void leave(const action_formulas::multi_action& x)
      80             :   {
      81         813 :     push(lps::equal_multi_actions(a, lps::multi_action(x.actions())));
      82         813 :   }
      83             : 
      84         291 :   void leave(const action_formulas::true_&)
      85             :   {
      86         291 :     push(true_());
      87         291 :   }
      88             : 
      89          25 :   void leave(const action_formulas::false_&)
      90             :   {
      91          25 :     push(false_());
      92          25 :   }
      93             : 
      94         126 :   void apply(const action_formulas::not_& x)
      95             :   {
      96         126 :     push(tr::not_(Sat(a, x.operand(), id_generator, TermTraits())));
      97         126 :   }
      98             : 
      99          39 :   void leave(const action_formulas::and_&)
     100             :   {
     101          39 :     expression_type right = pop();
     102          39 :     expression_type left = pop();
     103          39 :     push(tr::and_(left, right));
     104          39 :   }
     105             : 
     106          12 :   void leave(const action_formulas::or_&)
     107             :   {
     108          12 :     expression_type right = pop();
     109          12 :     expression_type left = pop();
     110          12 :     push(tr::or_(left, right));
     111          12 :   }
     112             : 
     113           0 :   void leave(const action_formulas::imp&)
     114             :   {
     115           0 :     expression_type right = pop();
     116           0 :     expression_type left = pop();
     117           0 :     push(tr::imp(left, right));
     118           0 :   }
     119             : 
     120           6 :   void apply(const action_formulas::forall& x)
     121             :   {
     122           6 :     data::mutable_map_substitution<> sigma_x = pbes_system::detail::make_fresh_variable_substitution(x.variables(), id_generator, false);
     123           6 :     const action_formulas::action_formula& alpha = x.body();
     124           6 :     data::variable_list y = data::replace_variables(x.variables(), sigma_x);
     125             :     
     126           6 :     pbes_expression result;
     127           6 :     tr::make_forall(result, y, Sat(a, action_formulas::replace_variables_capture_avoiding(alpha, sigma_x), id_generator, TermTraits()));
     128           6 :     push(result);
     129           6 :   }
     130             : 
     131           3 :   void apply(const action_formulas::exists& x)
     132             :   {
     133           3 :     data::mutable_map_substitution<> sigma_x = pbes_system::detail::make_fresh_variable_substitution(x.variables(), id_generator, false);
     134           3 :     const action_formulas::action_formula& alpha = x.body();
     135           3 :     data::variable_list y = data::replace_variables(x.variables(), sigma_x);
     136             : 
     137           3 :     pbes_expression result;
     138           3 :     tr::make_exists(result, y, Sat(a, action_formulas::replace_variables_capture_avoiding(alpha, sigma_x), id_generator, TermTraits()));
     139           3 :     push(result);
     140           3 :   }
     141             : 
     142           0 :   void apply(const action_formulas::at& x)
     143             :   {
     144           0 :     data::data_expression t = a.time();
     145           0 :     const action_formulas::action_formula& alpha = x.operand();
     146           0 :     const data::data_expression& u = x.time_stamp();
     147           0 :     push(tr::and_(Sat(a, alpha, id_generator, TermTraits()), data::equal_to(t, u)));
     148           0 :   }
     149             : };
     150             : 
     151             : template <template <class, class> class Traverser, typename TermTraits>
     152             : struct apply_sat_traverser: public Traverser<apply_sat_traverser<Traverser, TermTraits>, TermTraits>
     153             : {
     154             :   typedef Traverser<apply_sat_traverser<Traverser, TermTraits>, TermTraits> super;
     155             :   using super::enter;
     156             :   using super::leave;
     157             :   using super::apply;
     158             :   using super::top;
     159             : 
     160        1213 :   apply_sat_traverser(const lps::multi_action& a, data::set_identifier_generator& id_generator, TermTraits tr)
     161        1213 :     : super(a, id_generator, tr)
     162        1213 :   {}
     163             : };
     164             : 
     165             : template <typename TermTraits>
     166        1213 : typename TermTraits::term_type Sat(const lps::multi_action& a,
     167             :                                    const action_formulas::action_formula& x,
     168             :                                    data::set_identifier_generator& id_generator,
     169             :                                    TermTraits tr
     170             :                                   )
     171             : {
     172        1213 :   apply_sat_traverser<sat_traverser, TermTraits> f(a, id_generator, tr);
     173        1213 :   f.apply(x);
     174        2426 :   return f.top();
     175        1213 : }
     176             : 
     177             : } // namespace detail
     178             : 
     179             : } // namespace pbes_system
     180             : 
     181             : } // namespace mcrl2
     182             : 
     183             : #endif // MCRL2_PBES_DETAIL_LPS2PBES_SAT_H