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/modal_formula/maximal_closed_subformula.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_MODAL_FORMULA_MAXIMAL_CLOSED_SUBFORMULA_H
      13             : #define MCRL2_MODAL_FORMULA_MAXIMAL_CLOSED_SUBFORMULA_H
      14             : 
      15             : #include "mcrl2/modal_formula/traverser.h"
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace state_formulas {
      20             : 
      21             : namespace detail {
      22             : 
      23             : inline
      24          32 : std::size_t child_count(const state_formula& x)
      25             : {
      26          32 :   if (data::is_data_expression(x))            { return 0; }
      27          26 :   else if (state_formulas::is_true(x))        { return 0; }
      28          22 :   else if (state_formulas::is_false(x))       { return 0; }
      29          19 :   else if (state_formulas::is_not(x))         { return 1; }
      30          19 :   else if (state_formulas::is_and(x))         { return 2; }
      31          11 :   else if (state_formulas::is_or(x))          { return 2; }
      32           8 :   else if (state_formulas::is_imp(x))         { return 2; }
      33           8 :   else if (state_formulas::is_forall(x))      { return 1; }
      34           6 :   else if (state_formulas::is_exists(x))      { return 1; }
      35           5 :   else if (state_formulas::is_must(x))        { return 1; }
      36           5 :   else if (state_formulas::is_may(x))         { return 1; }
      37           5 :   else if (state_formulas::is_yaled(x))       { return 0; }
      38           5 :   else if (state_formulas::is_yaled_timed(x)) { return 0; }
      39           5 :   else if (state_formulas::is_delay(x))       { return 0; }
      40           5 :   else if (state_formulas::is_delay_timed(x)) { return 0; }
      41           5 :   else if (state_formulas::is_variable(x))    { return 0; }
      42           3 :   else if (state_formulas::is_nu(x))          { return 1; }
      43           2 :   else if (state_formulas::is_mu(x))          { return 1; }
      44           0 :   throw mcrl2::runtime_error("child_count: unknown argument");
      45             :   return 0;
      46             : }
      47             : 
      48             : template <template <class> class Traverser, class Node, class Derived>
      49             : struct bottom_up_traverser: public Traverser<Derived>
      50             : {
      51             :   typedef Traverser<Derived> super;
      52             :   using super::enter;
      53             :   using super::apply;
      54             : 
      55          32 :   Derived& derived()
      56             :   {
      57          32 :     return static_cast<Derived&>(*this);
      58             :   }
      59             : 
      60             :   // Maintain a stack with nodes, used to store intermediate results
      61             :   std::vector<Node> node_stack;
      62             :   typedef typename std::vector<Node>::const_iterator node_iterator;
      63             : 
      64             :   // Push a node to node_stack
      65          32 :   void push(const Node& node)
      66             :   {
      67          32 :     node_stack.push_back(node);
      68          32 :     mCRL2log(log::debug) << "<push>" << node << std::endl;
      69          32 :   }
      70             : 
      71             :   // Pop the top element of node_stack and return it
      72             :   Node pop()
      73             :   {
      74             :     Node result = node_stack.back();
      75             :     node_stack.pop_back();
      76             :     return result;
      77             :   }
      78             : 
      79             :   // Return the top element of node_stack
      80           4 :   Node& top()
      81             :   {
      82           4 :     return node_stack.back();
      83             :   }
      84             : 
      85             :   // Return the top element of node_stack
      86             :   const Node& top() const
      87             :   {
      88             :     return node_stack.back();
      89             :   }
      90             : 
      91             :   template <typename T>
      92             :   void join(const T& /* x */, node_iterator /* first */, node_iterator /* last */, Node& /* result */)
      93             :   {
      94             :   }
      95             : 
      96             :   // Override the leave function, such that it combines the results of child nodes
      97             :   template <typename T>
      98          32 :   void leave(const T& x)
      99             :   {
     100          64 :     Node result;
     101          32 :     std::size_t n = child_count(x);
     102          32 :     derived().join(x, node_stack.end() - n, node_stack.end(), result);
     103          32 :     node_stack.erase(node_stack.end() - n, node_stack.end());
     104          32 :     push(result);
     105          32 :   }
     106             : 
     107             :   // This leave function needs to be disabled.
     108             :   // TODO: It seems more logical that the call to this leave function is not generated in
     109             :   // the traverser, to avoid that the same term is visited twice.
     110          32 :   void leave(const state_formulas::state_formula&)
     111             :   {
     112          32 :   }
     113             : };
     114             : 
     115             : struct free_variables_node
     116             : {
     117             :   std::set<data::variable> variables;
     118             : 
     119          32 :   free_variables_node(const std::set<data::variable>& variables_ = std::set<data::variable>())
     120          32 :     : variables(variables_)
     121          32 :   { }
     122             : };
     123             : 
     124             : struct maximal_closed_subformula_node: public free_variables_node
     125             : {
     126             :   std::set<state_formulas::state_formula> formulas;
     127             : 
     128          32 :   maximal_closed_subformula_node(const std::set<data::variable>& variables = std::set<data::variable>(),
     129             :                                  const std::set<state_formulas::state_formula>& formulas_ = std::set<state_formulas::state_formula>()
     130             :                                 )
     131          32 :     : free_variables_node(variables),
     132          32 :       formulas(formulas_)
     133          32 :   { }
     134             : };
     135             : 
     136          32 : std::ostream& operator<<(std::ostream& out, const maximal_closed_subformula_node& node)
     137             : {
     138          32 :   out << "<node>variables = ";
     139          52 :   for (const data::variable& v: node.variables)
     140             :   {
     141          20 :     out << v << " ";
     142             :   }
     143          32 :   out << " formulas = ";
     144          66 :   for (const state_formula& f: node.formulas)
     145             :   {
     146          34 :     out << f << " ";
     147             :   }
     148          32 :   return out;
     149             : }
     150             : 
     151             : template <typename Derived>
     152             : struct maximal_closed_subformula_traverser: public bottom_up_traverser<state_formulas::state_formula_traverser, maximal_closed_subformula_node, Derived>
     153             : {
     154             :   typedef bottom_up_traverser<state_formulas::state_formula_traverser, maximal_closed_subformula_node, Derived> super;
     155             :   using super::enter;
     156             :   using super::leave;
     157             :   using super::apply;
     158             :   using super::push;
     159             :   using super::pop;
     160             :   using super::top;
     161             :   using super::node_stack;
     162             : 
     163             :   typedef typename super::node_iterator node_iterator;
     164             : 
     165             :   Derived& derived()
     166             :   {
     167             :     return static_cast<Derived&>(*this);
     168             :   }
     169             : 
     170             :   template <typename T>
     171          21 :   void update_free_variables(const T& /* x */, maximal_closed_subformula_node& /* result */)
     172          21 :   { }
     173             : 
     174           6 :   void update_free_variables(const data::data_expression& x, maximal_closed_subformula_node& result)
     175             :   {
     176           6 :     data::find_free_variables(x, std::inserter(result.variables, result.variables.end()));
     177           6 :   }
     178             : 
     179           2 :   void update_free_variables(const state_formulas::forall& x, maximal_closed_subformula_node& result)
     180             :   {
     181           6 :     for (const data::variable& v: x.variables())
     182             :     {
     183           2 :       result.variables.erase(v);
     184             :     }
     185           2 :   }
     186             : 
     187           1 :   void update_free_variables(const state_formulas::exists& x, maximal_closed_subformula_node& result)
     188             :   {
     189           3 :     for (const data::variable& v: x.variables())
     190             :     {
     191           1 :       result.variables.erase(v);
     192             :     }
     193           1 :   }
     194             : 
     195           2 :   void update_free_variables(const state_formulas::variable& x, maximal_closed_subformula_node& result)
     196             :   {
     197           4 :     for (const data::data_expression& e: x.arguments())
     198             :     {
     199           0 :       data::find_free_variables(e, std::inserter(result.variables, result.variables.end()));
     200             :     }
     201           2 :   }
     202             : 
     203             :   template <typename T>
     204             :   void update_maximal_closed_formulas(const T& x, maximal_closed_subformula_node& result)
     205             :   {
     206             :     if (result.variables.empty())
     207             :     {
     208             :       result.formulas.clear();
     209             :       result.formulas.insert(x);
     210             :     }
     211             :   }
     212             : 
     213             :   template <typename T>
     214          32 :   void join(const T& x, node_iterator first, node_iterator last, maximal_closed_subformula_node& result)
     215             :   {
     216          60 :     for (node_iterator i = first; i != last; ++i)
     217             :     {
     218          28 :       result.variables.insert(i->variables.begin(), i->variables.end());
     219             :     }
     220          32 :     update_free_variables(x, result);
     221          32 :     if (result.variables.empty())
     222             :     {
     223          15 :       result.formulas.insert(x);
     224             :     }
     225             :     else
     226             :     {
     227          37 :       for (node_iterator i = first; i != last; ++i)
     228             :       {
     229          20 :         result.formulas.insert(i->formulas.begin(), i->formulas.end());
     230             :       }
     231             :     }
     232          32 :   }
     233             : };
     234             : 
     235             : struct apply_maximal_closed_subformula_traverser: public maximal_closed_subformula_traverser<apply_maximal_closed_subformula_traverser>
     236             : {
     237             :   typedef maximal_closed_subformula_traverser<apply_maximal_closed_subformula_traverser> super;
     238             :   using super::enter;
     239             :   using super::leave;
     240             :   using super::apply;
     241             :   using super::top;
     242             : };
     243             : 
     244             : }; // namespace detail
     245             : 
     246             : inline
     247           4 : std::set<state_formulas::state_formula> maximal_closed_subformulas(const state_formula& x)
     248             : {
     249           4 :   detail::apply_maximal_closed_subformula_traverser f;
     250           4 :   f.apply(x);
     251           8 :   return f.top().formulas;
     252           4 : }
     253             : 
     254             : } // namespace state_formulas
     255             : 
     256             : } // namespace mcrl2
     257             : 
     258             : #endif // MCRL2_MODAL_FORMULA_MAXIMAL_CLOSED_SUBFORMULA_H