LCOV - code coverage report
Current view: top level - modal_formula/include/mcrl2/modal_formula - normalize.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 119 171 69.6 %
Date: 2024-03-08 02:52:28 Functions: 22 29 75.9 %
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/modal_formula/normalize.h
      10             : /// \brief Add your file description here.
      11             : 
      12             : #ifndef MCRL2_MODAL_FORMULA_NORMALIZE_H
      13             : #define MCRL2_MODAL_FORMULA_NORMALIZE_H
      14             : 
      15             : #include "mcrl2/modal_formula/negate_variables.h"
      16             : #include "mcrl2/modal_formula/traverser.h"
      17             : 
      18             : namespace mcrl2
      19             : {
      20             : 
      21             : namespace state_formulas
      22             : {
      23             : 
      24             : /// \cond INTERNAL_DOCS
      25             : // \brief Visitor for checking if a state formula is normalized.
      26             : struct is_normalized_traverser: public state_formula_traverser<is_normalized_traverser>
      27             : {
      28             :   typedef state_formula_traverser<is_normalized_traverser> super;
      29             :   using super::enter;
      30             :   using super::leave;
      31             :   using super::apply;
      32             : 
      33             :   bool result;
      34             : 
      35         198 :   is_normalized_traverser()
      36         198 :     : result(true)
      37         198 :   {}
      38             : 
      39             :   /// \brief Visit not node
      40          61 :   void enter(const not_& /* x */)
      41             :   {
      42          61 :     result = false;
      43          61 :   }
      44             : 
      45             :   /// \brief Visit minus node
      46           0 :   void enter(const minus& /* x */)
      47             :   {
      48           0 :     result = false;
      49           0 :   }
      50             : 
      51             :   /// \brief Visit imp node
      52          14 :   void enter(const imp& /* x */)
      53             :   {
      54          14 :     result = false;
      55          14 :   }
      56             : };
      57             : /// \endcond
      58             : 
      59             : /// \cond INTERNAL_DOCS
      60             : 
      61             : // \brief Visitor for normalizing a state formula.
      62             : struct normalize_builder: public state_formula_builder<normalize_builder>
      63             : {
      64             :   typedef state_formula_builder<normalize_builder> super;
      65             :   using super::enter;
      66             :   using super::leave;
      67             :   using super::update;
      68             :   using super::apply;
      69             : 
      70             :   bool m_quantitative;
      71             :   bool m_negated;
      72             : 
      73             :   // negated indicates that the formulas is under a negation.
      74             :   // quantitative indicates that the formula yields a real value, 
      75             :   // in which case forall, exists and not are replaced by supremum, infimum and minus. 
      76          63 :   normalize_builder(bool quantitative, bool negated)
      77          63 :     : m_quantitative(quantitative),
      78          63 :       m_negated(negated)
      79          63 :   {}
      80             : 
      81             :   template <class T>
      82          14 :   void apply(T& result, const data::data_expression& x)
      83             :   {
      84          14 :     if (m_quantitative)
      85             :     {
      86           0 :       if (m_negated)
      87             :       {
      88           0 :         if (x.sort()==data::sort_bool::bool_()) 
      89             :         {
      90           0 :           result = data::sort_bool::not_(x);
      91             :         }
      92             :         else
      93             :         {
      94           0 :           result = data::sort_real::negate(x);
      95             :         }
      96             :       }
      97             :       else
      98             :       {
      99           0 :         result = x;
     100             :       }
     101             :     }
     102             :     else // x is an ordinary modal formula.
     103             :     {
     104          14 :       assert(x.sort()==data::sort_bool::bool_());
     105          14 :       result = m_negated ? data::sort_bool::not_(x) : x;
     106             :     }
     107          14 :   }
     108             : 
     109             :   template <class T>
     110          37 :   void apply(T& result, const true_& /*x*/)
     111             :   {
     112          37 :     if (m_negated)
     113             :     {
     114          31 :       result = false_();
     115             :     }
     116             :     else
     117             :     {
     118           6 :       result = true_();
     119             :     }
     120          37 :   }
     121             : 
     122             :   template <class T>
     123          19 :   void apply(T& result, const false_& /*x*/)
     124             :   {
     125          19 :     if (m_negated)
     126             :     {
     127          18 :       result = true_();
     128             :     }
     129             :     else
     130             :     {
     131           1 :       result = false_();
     132             :     }
     133          19 :   }
     134             : 
     135             :   template <class T>
     136         103 :   void apply(T& result, const not_& x)
     137             :   {
     138         103 :     assert(!m_quantitative);
     139         103 :     m_negated=!m_negated;
     140         103 :     apply(result, x.operand());
     141         103 :     m_negated=!m_negated;
     142         103 :   }
     143             : 
     144             :   template <class T>
     145           0 :   void apply(T& result, const minus& x)
     146             :   {
     147           0 :     assert(m_quantitative);
     148           0 :     m_negated=!m_negated;
     149           0 :     apply(result, x.operand());
     150           0 :     m_negated=!m_negated;
     151           0 :   }
     152             : 
     153             :   template <class T>
     154          30 :   void apply(T& result, const and_& x)
     155             :   {
     156          30 :     state_formula left, right;
     157          30 :     apply(left, x.left());
     158          30 :     apply(right, x.right()); 
     159          30 :     if (m_negated)
     160             :     {
     161          22 :       make_or_(result, left, right);
     162             :     }
     163             :     else
     164             :     {
     165           8 :       make_and_(result, left, right);
     166             :     }
     167          30 :   }
     168             : 
     169             :   template <class T>
     170          20 :   void apply(T& result, const or_& x)
     171             :   {
     172          20 :     state_formula left, right;
     173          20 :     apply(left, x.left());
     174          20 :     apply(right, x.right()); 
     175          20 :     if (m_negated)
     176             :     {
     177          10 :       make_and_(result, left, right);
     178             :     }
     179             :     else
     180             :     {
     181          10 :       make_or_(result, left, right);
     182             :     }
     183          20 :   }
     184             : 
     185             :   template <class T>
     186           0 :   void apply(T& result, const plus& x)
     187             :   {
     188           0 :     state_formula left, right;
     189           0 :     apply(left, x.left());
     190           0 :     apply(right, x.right()); 
     191           0 :     if (m_negated)
     192             :     {
     193             :       // The plus operator can be inverted if for instance the operator eq_mininf(x) is present, being equal to -infinity
     194             :       // if x is minus infinity, and being plus infinity otherwise. 
     195             :       // The dual plus then is: e1 dual+ e2 = eq_mininf(e1) && eq_mininf(e2) && (e1+e2).
     196           0 :       throw mcrl2::runtime_error("Cannot negate the plus operator in quantitative modal formulas: " + pp(x) + ".");
     197             :     }
     198             :     else
     199             :     {
     200           0 :       make_plus(result, left, right);
     201             :     }
     202           0 :   }
     203             : 
     204             :   template <class T>
     205          15 :   void apply(T& result, const imp& x)
     206             :   {
     207          30 :     state_formula y = m_quantitative ?
     208           0 :                         or_(minus(x.left()), x.right()) :
     209          45 :                         or_(not_(x.left()), x.right());
     210          15 :     apply(result, y);
     211          15 :   }
     212             : 
     213             :   template <class T>
     214           3 :   void apply(T& result, const forall& x)
     215             :   {
     216           3 :     state_formula body;
     217           3 :     apply(body, x.body());
     218           3 :     if (m_negated)
     219             :     {
     220           1 :       make_exists(result, x.variables(), body); 
     221             :     }
     222             :     else
     223             :     {
     224           2 :       make_forall(result, x.variables(), body);
     225             :     }
     226           3 :   }
     227             : 
     228             :   template <class T>
     229           3 :   void apply(T& result, const exists& x)
     230             :   {
     231           3 :     state_formula body;
     232           3 :     apply(body, x.body());
     233           3 :     if (m_negated)
     234             :     {
     235           3 :       make_forall(result, x.variables(), body); 
     236             :     }
     237             :     else
     238             :     {
     239           0 :       make_exists(result, x.variables(), body);
     240             :     }
     241           3 :   }
     242             : 
     243             :   template <class T>
     244           0 :   void apply(T& result, const supremum& x)
     245             :   {
     246           0 :     state_formula body;
     247           0 :     apply(body, x.body());
     248           0 :     if (m_negated)
     249             :     {
     250           0 :       make_infimum(result, x.variables(), body);
     251             :     }
     252             :     else
     253             :     {
     254           0 :       make_supremum(result, x.variables(), body); 
     255             :     }
     256           0 :   }
     257             : 
     258             :   template <class T>
     259           0 :   void apply(T& result, const infimum& x)
     260             :   {
     261           0 :     state_formula body;
     262           0 :     apply(body, x.body());
     263           0 :     if (m_negated)
     264             :     {
     265           0 :       make_supremum(result, x.variables(), body); 
     266             :     }
     267             :     else
     268             :     {
     269           0 :       make_infimum(result, x.variables(), body);
     270             :     }
     271           0 :   }
     272             : 
     273             :   template <class T>
     274          41 :   void apply(T& result, const variable& x)
     275             :   {
     276          41 :     if (m_negated)
     277             :     {
     278           0 :       throw mcrl2::runtime_error(std::string("normalize error: illegal argument ") + pp(x));
     279             :     }
     280          41 :     result = x;
     281          41 :   }
     282             : 
     283             :   template <class T>
     284          46 :   void apply(T& result, const must& x)
     285             :   {
     286          46 :     state_formula operand;
     287          46 :     apply(operand, x.operand());
     288          46 :     if (m_negated)
     289             :     {
     290          36 :       make_may(result, x.formula(), operand);
     291             :     }
     292             :     else
     293             :     {
     294          10 :       make_must(result, x.formula(), operand);
     295             :     }
     296          46 :   }
     297             : 
     298             :   template <class T>
     299          40 :   void apply(T& result, const may& x)
     300             :   {
     301          40 :     state_formula operand;
     302          40 :     apply(operand, x.operand());
     303          40 :     if (m_negated)
     304             :     {
     305          35 :       make_must(result, x.formula(), operand);
     306             :     }
     307             :     else
     308             :     {
     309           5 :       make_may(result, x.formula(), operand);
     310             :     }
     311          40 :   }
     312             : 
     313             :   template <class T>
     314          20 :   void apply(T& result, const mu& x)
     315             :   {
     316          20 :     state_formula operand;
     317          20 :     if (m_negated)
     318             :     {
     319          14 :       apply(operand, negate_variables(x.name(), m_quantitative, x.operand()));
     320          14 :       make_nu(result, x.name(), x.assignments(), operand);
     321             :     }
     322             :     else
     323             :     {
     324           6 :       apply(operand, x.operand());
     325           6 :       make_mu(result, x.name(), x.assignments(), operand);
     326             :     }
     327          20 :   }
     328             : 
     329             :   template <class T>
     330          21 :   void apply(T& result, const nu& x)
     331             :   {
     332          21 :     state_formula operand;
     333          21 :     if (m_negated)
     334             :     {
     335          13 :       apply(operand, negate_variables(x.name(), m_quantitative, x.operand()));
     336          13 :       make_mu(result, x.name(), x.assignments(), operand);
     337             :     }
     338             :     else
     339             :     {
     340           8 :       apply(operand, x.operand());
     341           8 :       make_nu(result, x.name(), x.assignments(), operand);
     342             :     }
     343          21 :   }
     344             : 
     345             :   template <class T>
     346           0 :   void apply(T& result, const delay& x)
     347             :   {
     348           0 :     if (m_negated)
     349             :     {
     350           0 :       result=yaled();
     351             :     }
     352             :     else
     353             :     {
     354           0 :       result=x;
     355             :     }
     356           0 :   }
     357             : 
     358             :   template <class T>
     359           1 :   void apply(T& result, const delay_timed& x)
     360             :   {
     361           1 :     if (m_negated)
     362             :     {
     363           1 :       make_yaled_timed(result, x.time_stamp());
     364             :     }
     365             :     else
     366             :     {
     367           0 :       result=x;
     368             :     }
     369           1 :   }
     370             : 
     371             :   template <class T>
     372           0 :   void apply(T& result, const yaled& x)
     373             :   {
     374           0 :     if (m_negated)
     375             :     {
     376           0 :       result=delay();
     377             :     }
     378             :     else
     379             :     {
     380           0 :       result=x;
     381             :     }
     382           0 :   }
     383             : 
     384             :   template <class T>
     385           1 :   void apply(T& result,  const yaled_timed& x)
     386             :   {
     387           1 :     if (m_negated)
     388             :     {
     389           1 :       make_delay_timed(result, x.time_stamp());
     390             :     }
     391             :     else
     392             :     {
     393           0 :       result=x;
     394             :     }
     395           1 :   }
     396             : };
     397             : /// \endcond
     398             : 
     399             : /// \brief Checks if a state formula is normalized.
     400             : /// \param x A PBES expression.
     401             : /// \return True if the state formula is normalized.
     402             : template <typename T>
     403         198 : bool is_normalized(const T& x)
     404             : {
     405         198 :   is_normalized_traverser f;
     406         198 :   f.apply(x);
     407         198 :   return f.result;
     408             : }
     409             : 
     410             : /// \brief The function normalize brings (embedded) state formulas into positive normal form,
     411             : /// i.e. a formula without any occurrences of ! or =>.
     412             : /// \param x an object containing state formulas.
     413             : /// \param quantitative Indication whether the formula is a quantitative boolean formula.
     414             : /// \param negated Indication whether the formula must be interpreted as being negated.
     415             : template <typename T>
     416             : void normalize(T& x, bool quantitative = false, bool negated = false, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr)
     417             : {
     418             :   normalize_builder f(quantitative, negated);
     419             :   f.update(x);
     420             : }
     421             : 
     422             : /// \brief The function normalize brings (embedded) state formulas into positive normal form,
     423             : /// i.e. a formula without any occurrences of ! or =>.
     424             : /// \param x an object containing state formulas
     425             : /// \param quantitative Indication whether the formula is a quantitative boolean formula.
     426             : /// \param negated Indication whether the formula must be interpreted as being negated.
     427             : template <typename T>
     428          63 : T normalize(const T& x, bool quantitative = false, bool negated = false, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr)
     429             : {
     430          63 :   T result;
     431          63 :   normalize_builder f(quantitative, negated);
     432          63 :   f.apply(result, x);
     433         126 :   return result;
     434           0 : }
     435             : 
     436             : } // namespace state_formulas
     437             : 
     438             : } // namespace mcrl2
     439             : 
     440             : #endif // MCRL2_MODAL_FORMULA_NORMALIZE_H

Generated by: LCOV version 1.14