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_par.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_DETAIL_LPS2PBES_PAR_H
      13             : #define MCRL2_PBES_DETAIL_LPS2PBES_PAR_H
      14             : 
      15             : #include "mcrl2/modal_formula/traverser.h"
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace pbes_system {
      20             : 
      21             : namespace detail {
      22             : 
      23             : data::variable_list Par(const core::identifier_string& X, const data::variable_list& l, const state_formulas::state_formula& x);
      24             : 
      25             : struct par_traverser: public state_formulas::state_formula_traverser<par_traverser>
      26             : {
      27             :   typedef state_formulas::state_formula_traverser<par_traverser> super;
      28             :   using super::enter;
      29             :   using super::leave;
      30             :   using super::apply;
      31             : 
      32             :   const core::identifier_string& X;
      33             :   const data::variable_list& l;
      34             :   std::vector<data::variable_list> result_stack;
      35             : 
      36        2827 :   par_traverser(const core::identifier_string& X_, const data::variable_list& l_)
      37        2827 :     : X(X_), l(l_)
      38        2827 :   {}
      39             : 
      40        9029 :   void push(const data::variable_list& x)
      41             :   {
      42        9029 :     result_stack.push_back(x);
      43        9029 :   }
      44             : 
      45        9029 :   const data::variable_list& top() const
      46             :   {
      47        9029 :     return result_stack.back();
      48             :   }
      49             : 
      50        6202 :   data::variable_list pop()
      51             :   {
      52        6202 :     data::variable_list result = top();
      53        6202 :     result_stack.pop_back();
      54        6202 :     return result;
      55             :   }
      56             : 
      57             :   // join the two topmost elements on the stack
      58        3101 :   void join()
      59             :   {
      60        3101 :     data::variable_list right = pop();
      61        3101 :     data::variable_list left = pop();
      62        3101 :     push(left + right);
      63        3101 :   }
      64             : 
      65          30 :   void leave(const data::data_expression&)
      66             :   {
      67          30 :     push(data::variable_list());
      68          30 :   }
      69             : 
      70         259 :   void leave(const state_formulas::true_&)
      71             :   {
      72         259 :     push(data::variable_list());
      73         259 :   }
      74             : 
      75         917 :   void leave(const state_formulas::false_&)
      76             :   {
      77         917 :     push(data::variable_list());
      78         917 :   }
      79             : 
      80           0 :   void leave(const state_formulas::not_&)
      81             :   {
      82             :     // skip
      83           0 :   }
      84             : 
      85        1820 :   void leave(const state_formulas::and_&)
      86             :   {
      87        1820 :     join();
      88        1820 :   }
      89             : 
      90        1281 :   void leave(const state_formulas::or_&)
      91             :   {
      92        1281 :     join();
      93        1281 :   }
      94             : 
      95           0 :   void leave(const state_formulas::imp&)
      96             :   {
      97           0 :     join();
      98           0 :   }
      99             : 
     100          21 :   void apply(const state_formulas::forall& x)
     101             :   {
     102          21 :     push(Par(X, l + x.variables(), x.body()));
     103          21 :   }
     104             : 
     105           3 :   void apply(const state_formulas::exists& x)
     106             :   {
     107           3 :     push(Par(X, l + x.variables(), x.body()));
     108           3 :   }
     109             : 
     110        1942 :   void leave(const state_formulas::must&)
     111             :   {
     112             :     // skip
     113        1942 :   }
     114             : 
     115        1472 :   void leave(const state_formulas::may&)
     116             :   {
     117             :     // skip
     118        1472 :   }
     119             : 
     120           0 :   void leave(const state_formulas::yaled&)
     121             :   {
     122           0 :     push(data::variable_list());
     123           0 :   }
     124             : 
     125           0 :   void leave(const state_formulas::yaled_timed&)
     126             :   {
     127           0 :     push(data::variable_list());
     128           0 :   }
     129             : 
     130           0 :   void leave(const state_formulas::delay&)
     131             :   {
     132           0 :     push(data::variable_list());
     133           0 :   }
     134             : 
     135           0 :   void leave(const state_formulas::delay_timed&)
     136             :   {
     137           0 :     push(data::variable_list());
     138           0 :   }
     139             : 
     140        1895 :   void leave(const state_formulas::variable&)
     141             :   {
     142        1895 :     push(data::variable_list());
     143        1895 :   }
     144             : 
     145        1605 :   void apply(const state_formulas::nu& x)
     146             :   {
     147        1605 :     if (x.name() == X)
     148             :     {
     149         547 :       push(l);
     150             :     }
     151             :     else
     152             :     {
     153        1058 :       push(Par(X, l + data::left_hand_sides(x.assignments()), x.operand()));
     154             :     }
     155        1605 :   }
     156             : 
     157        1198 :   void apply(const state_formulas::mu& x)
     158             :   {
     159        1198 :     if (x.name() == X)
     160             :     {
     161         275 :       push(l);
     162             :     }
     163             :     else
     164             :     {
     165         923 :       push(Par(X, l + data::left_hand_sides(x.assignments()), x.operand()));
     166             :     }
     167        1198 :   }
     168             : };
     169             : 
     170             : inline
     171        2827 : data::variable_list Par(const core::identifier_string& X, const data::variable_list& l, const state_formulas::state_formula& x)
     172             : {
     173        2827 :   par_traverser f(X, l);
     174        2827 :   f.apply(x);
     175        5654 :   return f.top();
     176        2827 : }
     177             : 
     178             : } // namespace detail
     179             : 
     180             : } // namespace pbes_system
     181             : 
     182             : } // namespace mcrl2
     183             : 
     184             : #endif // MCRL2_PBES_DETAIL_LPS2PBES_PAR_H