LCOV - code coverage report
Current view: top level - bes/include/mcrl2/bes - normal_forms.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 81 95 85.3 %
Date: 2020-10-20 00:45:57 Functions: 15 18 83.3 %
Legend: Lines: hit not hit

          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/bes/normal_forms.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_BES_NORMAL_FORMS_H
      13             : #define MCRL2_BES_NORMAL_FORMS_H
      14             : 
      15             : #include "mcrl2/bes/traverser.h"
      16             : 
      17             : namespace mcrl2
      18             : {
      19             : 
      20             : namespace bes
      21             : {
      22             : 
      23             : namespace detail
      24             : {
      25             : 
      26             : enum standard_form_type
      27             : {
      28             :   standard_form_both,
      29             :   standard_form_and,
      30             :   standard_form_or
      31             : };
      32             : 
      33             : typedef std::pair<boolean_expression, standard_form_type> standard_form_pair;
      34             : 
      35             : /// \brief Traverser that implements the standard form normalization.
      36           8 : class standard_form_traverser: public bes::boolean_expression_traverser<standard_form_traverser>
      37             : {
      38             :   public:
      39             :     typedef bes::boolean_expression_traverser<standard_form_traverser> super;
      40             : 
      41             :     using super::apply;
      42             :     using super::enter;
      43             :     using super::leave;
      44             : 
      45             :     /// \brief If true, the result will be in standard recursive normal form, otherwise in standard form.
      46             :     bool m_recursive_form;
      47             : 
      48             :     /// \brief The fixpoint symbol of the current equation.
      49             :     fixpoint_symbol m_symbol;
      50             : 
      51             :     /// \brief The name of the variable of the current equation, with a trailing underscore added.
      52             :     std::string m_name;
      53             : 
      54             :     /// \brief Is set to true if the value true is encountered in the BES.
      55             :     bool m_has_true;
      56             : 
      57             :     /// \brief Is set to true if the value false is encountered in the BES.
      58             :     bool m_has_false;
      59             : 
      60             :     /// \brief For generating fresh variables.
      61             :     utilities::number_postfix_generator m_generator;
      62             : 
      63             :     /// \brief A stack containing sub-terms.
      64             :     std::vector<standard_form_pair> m_expression_stack;
      65             : 
      66             :     /// \brief A vector containing generated equations.
      67             :     std::vector<boolean_equation> m_equations;
      68             : 
      69             :     /// \brief A vector containing generated equations with new variables.
      70             :     std::vector<boolean_equation> m_equations2;
      71             : 
      72             :     /// \brief Maps right hand sides of equations to their corresponding left hand side.
      73             :     std::map<boolean_expression, boolean_variable> m_table;
      74             : 
      75             :     /// \brief The expression corresponding to true.
      76             :     boolean_expression m_true;
      77             : 
      78             :     /// \brief The expression corresponding to false.
      79             :     boolean_expression m_false;
      80             : 
      81             :     /// \brief Pops the stack and returns the popped element
      82          47 :     standard_form_pair pop()
      83             :     {
      84          47 :       standard_form_pair result = m_expression_stack.back();
      85          47 :       m_expression_stack.pop_back();
      86          47 :       return result;
      87             :     }
      88             : 
      89             :     /// \brief Pushes (first, second) on the stack.
      90          55 :     void push(const boolean_expression& first, standard_form_type second)
      91             :     {
      92          55 :       m_expression_stack.push_back(standard_form_pair(first, second));
      93          55 :     }
      94             : 
      95             :     /// \brief Generates a fresh boolean variable.
      96          14 :     boolean_variable fresh_variable(const std::string& hint)
      97             :     {
      98          28 :       core::identifier_string s = m_generator(hint);
      99          28 :       return boolean_variable(s);
     100             :     }
     101             : 
     102             :     /// \brief Generates an equation var=expr for the expression expr (if it does not exist).
     103             :     /// \return The variable var.
     104           2 :     boolean_variable create_variable(const boolean_expression& expr, standard_form_type type, const std::string& hint)
     105             :     {
     106           2 :       std::map<boolean_expression, boolean_variable>::iterator i = m_table.find(expr);
     107           2 :       if (i != m_table.end())
     108             :       {
     109           0 :         return i->second;
     110             :       }
     111           4 :       boolean_variable var = fresh_variable(hint);
     112           2 :       m_table[expr] = var;
     113           2 :       if (type == standard_form_and)
     114             :       {
     115           2 :         m_equations2.push_back(boolean_equation(m_symbol, var, expr));
     116             :       }
     117             :       else
     118             :       {
     119           0 :         m_equations2.push_back(boolean_equation(m_symbol, var, expr));
     120             :       }
     121           2 :       return var;
     122             :     }
     123             : 
     124             :     /// \brief Constructor.
     125             :     /// \param recursive_form Determines whether or not the result will be in standard recursive normal form.
     126           8 :     standard_form_traverser(bool recursive_form = false)
     127           8 :       : m_recursive_form(recursive_form),
     128             :         m_has_true(false),
     129           8 :         m_has_false(false)
     130             :     {
     131           8 :       if (m_recursive_form)
     132             :       {
     133           6 :         m_true = fresh_variable("True");
     134           6 :         m_false = fresh_variable("False");
     135             :       }
     136             :       else
     137             :       {
     138           2 :         m_true = true_();
     139           2 :         m_false = false_();
     140             :       }
     141           8 :     }
     142             : 
     143             :     /// \brief Returns the top element of the expression stack, which is the result of the normalization.
     144             :     boolean_expression result() const
     145             :     {
     146             :       return m_expression_stack.back().first;
     147             :     }
     148             : 
     149             :     /// \brief Returns the generated equations.
     150             :     const std::vector<boolean_equation>& equations() const
     151             :     {
     152             :       return m_equations;
     153             :     }
     154             : 
     155             :     /// \brief Enter true node.
     156             :     /// \param x A term.
     157           2 :     void enter(const true_& x)
     158             :     {
     159             :       (void)x; // Suppress a non used variable warning.
     160           2 :       m_has_true = true;
     161           2 :       push(m_true, standard_form_both);
     162           2 :     }
     163             : 
     164             :     /// \brief Enter false node
     165             :     /// \param x A term
     166           0 :     void enter(const false_& x)
     167             :     {
     168             :       (void)x; // Suppress a non used variable warning.
     169           0 :       m_has_false = true;
     170           0 :       push(m_false, standard_form_both);
     171           0 :     }
     172             : 
     173             :     /// \brief Enter boolean_variable node.
     174             :     /// \param x A boolean variable.
     175          38 :     void enter(const boolean_variable& x)
     176             :     {
     177          38 :       push(x, standard_form_both);
     178          38 :     }
     179             : 
     180             :     /// \brief Leave not node.
     181           0 :     void leave(const not_& /* x */)
     182             :     {
     183           0 :       throw mcrl2::runtime_error("negation is not supported in standard recursive form algorithm");
     184             :     }
     185             : 
     186             :     /// \brief Leave and node
     187           8 :     void leave(const and_& /* x */)
     188             :     {
     189          16 :       standard_form_pair right = pop();
     190          16 :       standard_form_pair left = pop();
     191           8 :       if (left.second == standard_form_or)
     192             :       {
     193           0 :         left.first = create_variable(left.first, standard_form_or, m_name);
     194             :       }
     195           8 :       if (right.second == standard_form_or)
     196             :       {
     197           0 :         right.first = create_variable(right.first, standard_form_or, m_name);
     198             :       }
     199           8 :       push(and_(left.first, right.first), standard_form_and);
     200           8 :     }
     201             : 
     202             :     /// \brief Leave or node
     203           7 :     void leave(const or_& /* x */)
     204             :     {
     205          14 :       standard_form_pair right = pop();
     206          14 :       standard_form_pair left = pop();
     207           7 :       if (left.second == standard_form_and)
     208             :       {
     209           0 :         left.first = create_variable(left.first, standard_form_and, m_name);
     210             :       }
     211           7 :       if (right.second == standard_form_and)
     212             :       {
     213           2 :         right.first = create_variable(right.first, standard_form_and, m_name);
     214             :       }
     215           7 :       push(or_(left.first, right.first), standard_form_or);
     216           7 :     }
     217             : 
     218             :     /// \brief Leave imp node
     219           0 :     void leave(const imp& /* x */)
     220             :     {
     221           0 :       throw mcrl2::runtime_error("implication is not supported in standard recursive form algorithm");
     222             :     }
     223             : 
     224             :     /// \brief Enter an equation
     225          17 :     void enter(const boolean_equation& eq)
     226             :     {
     227          17 :       m_symbol = eq.symbol();
     228          17 :       m_name = std::string(eq.variable().name()) + '_';
     229          17 :     }
     230             : 
     231             :     /// \brief Leave an equation
     232          17 :     void leave(const boolean_equation& eq)
     233             :     {
     234          34 :       standard_form_pair p = pop();
     235          17 :       m_equations.push_back(boolean_equation(eq.symbol(), eq.variable(), p.first));
     236             :       // m_table[p.first] = eq.variable();
     237          17 :     }
     238             : 
     239             :     /// \brief Enter a boolean equation system.
     240           8 :     void enter(const boolean_equation_system& x)
     241             :     {
     242           8 :       assert(!x.equations().empty());
     243          25 :       for (const boolean_equation& eqn: x.equations())
     244             :       {
     245          17 :         m_generator.add_identifier(std::string(eqn.variable().name()));
     246             :       }
     247           8 :     }
     248             : 
     249             :     /// \brief Leave a boolean equation system.
     250           8 :     void leave(const boolean_equation_system&)
     251             :     {
     252             :       // set the fixpoint symbol for the added equations m_equations2, and move them to m_equations
     253           8 :       assert(!m_equations.empty());
     254          16 :       fixpoint_symbol sigma = m_equations.back().symbol();
     255          10 :       for (boolean_equation& eqn: m_equations2)
     256             :       {
     257           2 :         eqn.symbol() = sigma;
     258             :       }
     259           8 :       std::copy(m_equations2.begin(), m_equations2.end(), std::back_inserter(m_equations));
     260             : 
     261             :       // add equations for true and false if needed
     262           8 :       if (m_recursive_form)
     263             :       {
     264           6 :         if (m_has_true)
     265             :         {
     266           1 :           m_equations.push_back(boolean_equation(fixpoint_symbol::nu(), boolean_variable(m_true), m_true));
     267             :         }
     268           6 :         if (m_has_false)
     269             :         {
     270           0 :           m_equations.push_back(boolean_equation(fixpoint_symbol::mu(), boolean_variable(m_false), m_false));
     271             :         }
     272             :       }
     273           8 :     }
     274             : 
     275             : };
     276             : 
     277             : } // namespace detail
     278             : 
     279             : /// \brief Transforms a BES into standard form.
     280             : /// \param eqn A boolean equation system
     281             : /// \param recursive_form Determines whether or not the result will be in standard recursive normal form
     282             : inline
     283           8 : void make_standard_form(boolean_equation_system& eqn, bool recursive_form = false)
     284             : {
     285          16 :   detail::standard_form_traverser t(recursive_form);
     286           8 :   t.apply(eqn);
     287           8 :   assert(!is_boolean_variable(eqn.initial_state()) || eqn.equations().begin()->variable() == boolean_variable(eqn.initial_state()));
     288           8 :   assert(!is_boolean_variable(eqn.initial_state()) || t.m_equations.begin()->variable() == boolean_variable(eqn.initial_state()));
     289           8 :   eqn.equations() = t.m_equations;
     290           8 : }
     291             : 
     292             : } // namespace bes
     293             : 
     294             : } // namespace mcrl2
     295             : 
     296             : #endif // MCRL2_BES_NORMAL_FORMS_H

Generated by: LCOV version 1.13