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/significant_variables.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_SIGNIFICANT_VARIABLES_H
      13             : #define MCRL2_PBES_SIGNIFICANT_VARIABLES_H
      14             : 
      15             : #include "mcrl2/pbes/traverser.h"
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace pbes_system {
      20             : 
      21             : namespace detail {
      22             : 
      23             : struct significant_variables_traverser: public pbes_expression_traverser<significant_variables_traverser>
      24             : {
      25             :   typedef pbes_expression_traverser<significant_variables_traverser> super;
      26             :   using super::enter;
      27             :   using super::leave;
      28             :   using super::apply;
      29             : 
      30             :   std::vector<std::set<data::variable> > result_stack;
      31             : 
      32             :   // Push a sig set to result_stack
      33          38 :   void push(const std::set<data::variable>& v)
      34             :   {
      35          38 :     result_stack.push_back(v);
      36          38 :   }
      37             : 
      38             :   // Pop the top element of result_stack and return it
      39          28 :   std::set<data::variable> pop()
      40             :   {
      41          28 :     std::set<data::variable> result = result_stack.back();
      42          28 :     result_stack.pop_back();
      43          28 :     return result;
      44             :   }
      45             : 
      46             :   // Return the top element of result_stack
      47           2 :   std::set<data::variable>& top()
      48             :   {
      49           2 :     return result_stack.back();
      50             :   }
      51             : 
      52             :   // Return the top element of result_stack
      53             :   const std::set<data::variable>& top() const
      54             :   {
      55             :     return result_stack.back();
      56             :   }
      57             : 
      58             :   // Pops two elements A1 and A2 from the stack, and pushes back union(A1, A2)
      59          14 :   void join()
      60             :   {
      61          14 :     std::set<data::variable> right = pop();
      62          14 :     std::set<data::variable> left = pop();
      63          14 :     push(utilities::detail::set_union(left, right));
      64          14 :   }
      65             : 
      66           8 :   void leave(const and_& /* x */)
      67             :   {
      68           8 :     join();
      69           8 :   }
      70             : 
      71           0 :   void leave(const or_& /* x */)
      72             :   {
      73           0 :     join();
      74           0 :   }
      75             : 
      76           6 :   void leave(const imp& /* x */)
      77             :   {
      78           6 :     join();
      79           6 :   }
      80             : 
      81           0 :   void leave(const exists& x)
      82             :   {
      83           0 :     for (const data::variable& v: x.variables())
      84             :     {
      85           0 :       top().erase(v);
      86             :     }
      87           0 :   }
      88             : 
      89           2 :   void leave(const forall& x)
      90             :   {
      91           4 :     for (const data::variable& v: x.variables())
      92             :     {
      93           2 :       top().erase(v);
      94             :     }
      95           2 :   }
      96             : 
      97           9 :   void leave(const propositional_variable_instantiation&)
      98             :   {
      99           9 :     push(std::set<data::variable>());
     100           9 :   }
     101             : 
     102          15 :   void leave(const data::data_expression& x)
     103             :   {
     104          15 :     push(data::find_free_variables(x));
     105          15 :   }
     106             : };
     107             : 
     108             : } // namespace detail
     109             : 
     110             : inline
     111          10 : std::set<data::variable> significant_variables(const pbes_expression& x)
     112             : {
     113          10 :   detail::significant_variables_traverser f;
     114          10 :   f.apply(x);
     115          20 :   return f.result_stack.back();
     116          10 : }
     117             : 
     118             : } // namespace pbes_system
     119             : 
     120             : } // namespace mcrl2
     121             : 
     122             : #endif // MCRL2_PBES_SIGNIFICANT_VARIABLES_H