LCOV - code coverage report
Current view: top level - modal_formula/source - regfrmtrans.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 90 123 73.2 %
Date: 2024-03-08 02:52:28 Functions: 2 2 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Aad Mathijssen
       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 regfrmtrans.cpp
      10             : 
      11             : #include "mcrl2/data/xyz_identifier_generator.h"
      12             : #include "mcrl2/modal_formula/translate_regular_formulas.h"
      13             : 
      14             : using namespace mcrl2::core;
      15             : using namespace mcrl2::core::detail;
      16             : using namespace mcrl2::data;
      17             : using namespace mcrl2::state_formulas;
      18             : using namespace mcrl2::regular_formulas;
      19             : 
      20             : namespace mcrl2
      21             : {
      22             : namespace regular_formulas
      23             : {
      24             : namespace detail
      25             : {
      26             : 
      27             : //local declarations
      28             : //------------------
      29             : 
      30             : inline state_formula translate_reg_frms_appl(state_formula part, xyz_identifier_generator &xyz_generator);
      31             : /*Pre: part represents a part of a state formula
      32             :  *     after the data implementation phase
      33             :  *Ret: part in which all regular formulas are translated in terms of state and
      34             :  *     action formulas
      35             :  */
      36             : 
      37             : //implementation
      38             : //--------------
      39             : 
      40         151 : state_formula translate_reg_frms(const state_formula &state_frm)
      41             : {
      42         151 :   xyz_identifier_generator xyz_generator(find_identifiers(state_frm));
      43         302 :   return translate_reg_frms_appl(state_frm, xyz_generator);
      44         151 : }
      45             : 
      46         807 : inline state_formula translate_reg_frms_appl(state_formula part, xyz_identifier_generator& xyz_generator)
      47             : {
      48         807 :   if (data::is_data_expression(part) ||
      49         787 :       lps::is_multi_action(part) ||
      50         787 :       state_formulas::is_variable(part) ||
      51         644 :       data::is_assignment(part) ||
      52         644 :       state_formulas::is_true(part) ||
      53         560 :       state_formulas::is_false(part) ||
      54         527 :       state_formulas::is_yaled(part) ||
      55         527 :       state_formulas::is_yaled_timed(part) ||
      56        2120 :       state_formulas::is_delay(part) ||
      57         526 :       state_formulas::is_delay_timed(part)
      58             :      )
      59             :   {
      60             :     //part is a data expression, a multiaction, a state variable or a data
      61             :     //variable declaration (with or without initialisation); return part
      62             :   }
      63         525 :   else if (state_formulas::is_must(part))
      64             :   {
      65             :     //part is the must operator; return equivalent non-regular formula
      66         138 :     const regular_formula reg_frm = must(part).formula();
      67         138 :     const state_formula phi = must(part).operand();
      68         138 :     if (regular_formulas::is_seq(reg_frm))
      69             :     {
      70           3 :       const regular_formula R1 = seq(reg_frm).left();
      71           3 :       const regular_formula R2 = seq(reg_frm).right();
      72             :       //red([R1.R2]phi) -> red([R1][R2]phi)
      73           3 :       part = translate_reg_frms_appl(must(R1, must(R2, phi)),xyz_generator);
      74           3 :     }
      75         135 :     else if (regular_formulas::is_alt(reg_frm))
      76             :     {
      77           0 :       const regular_formula R1 = alt(reg_frm).left();
      78           0 :       const regular_formula R2 = alt(reg_frm).right();
      79             :       //red([R1+R2]phi) -> red([R1]phi) && red([R2]phi)
      80           0 :       part = state_formulas::and_(
      81           0 :                translate_reg_frms_appl(must(R1,phi),xyz_generator),
      82           0 :                translate_reg_frms_appl(must(R2,phi),xyz_generator)
      83           0 :              );
      84           0 :     }
      85         135 :     else if (regular_formulas::is_trans(reg_frm))
      86             :     {
      87           0 :       const regular_formula R = trans(atermpp::aterm_appl(reg_frm)).operand();
      88             :       //red([R+]phi) -> red([R.R*]phi)
      89           0 :       part = translate_reg_frms_appl(must(seq(R,trans_or_nil(R)),phi),xyz_generator);
      90           0 :     }
      91         135 :     else if (regular_formulas::is_trans_or_nil(reg_frm))
      92             :     {
      93          28 :       const regular_formula R = trans_or_nil(atermpp::aterm_appl(reg_frm)).operand();
      94             :       //red([R*]phi) -> nu X. red(phi) && red([R]X),
      95             :       //where X does not occur free in phi and R
      96          28 :       const identifier_string X = xyz_generator("X");
      97          28 :       part = nu(X, assignment_list(), state_formulas::and_(
      98          28 :                      translate_reg_frms_appl(phi,xyz_generator),
      99          28 :                      translate_reg_frms_appl(must(R,mcrl2::state_formulas::variable(X, data_expression_list())),xyz_generator)
     100          14 :                ));
     101          14 :     }
     102             :     else
     103             :     {
     104             :       //reg_frm is an action formula; reduce phi
     105         121 :       part = must(reg_frm, translate_reg_frms_appl(phi,xyz_generator));
     106             :     }
     107         138 :   }
     108         387 :   else if (state_formulas::is_may(part))
     109             :   {
     110             :     //part is the may operator; return equivalent non-regular formula
     111          78 :     regular_formula reg_frm = may(part).formula();
     112          78 :     state_formula phi = may(part).operand();
     113          78 :     if (regular_formulas::is_seq(reg_frm))
     114             :     {
     115           0 :       const regular_formula R1 = seq(reg_frm).left();
     116           0 :       const regular_formula R2 = seq(reg_frm).right();
     117             :       //red(<R1.R2>phi) -> red(<R1><R2>phi)
     118           0 :       part = translate_reg_frms_appl(may(R1, may(R2, phi)),xyz_generator);
     119           0 :     }
     120          78 :     else if (regular_formulas::is_alt(reg_frm))
     121             :     {
     122           0 :       const regular_formula R1 = alt(reg_frm).left();
     123           0 :       const regular_formula R2 = alt(reg_frm).right();
     124             :       //red(<R1+R2>phi) -> red(<R1>phi) || red(<R2>phi)
     125           0 :       part = state_formulas::or_(
     126           0 :                translate_reg_frms_appl(may(R1,phi),xyz_generator),
     127           0 :                translate_reg_frms_appl(may(R2,phi),xyz_generator)
     128           0 :              );
     129           0 :     }
     130          78 :     else if (regular_formulas::is_trans(reg_frm))
     131             :     {
     132           0 :       const regular_formula R = trans(atermpp::aterm_appl(reg_frm)).operand();
     133             :       //red(<R+>phi) -> red(<R.R*>phi)
     134           0 :       part = translate_reg_frms_appl(may(seq(R,trans_or_nil(R)),phi),xyz_generator);
     135           0 :     }
     136          78 :     else if (regular_formulas::is_trans_or_nil(reg_frm))
     137             :     {
     138          14 :       const regular_formula R = trans_or_nil(atermpp::aterm_appl(reg_frm)).operand();
     139             :       //red(<R*>phi) -> mu X. red(phi) || red(<R>X),
     140             :       //where X does not occur free in phi and R
     141          14 :       const identifier_string X =xyz_generator("X");
     142          14 :       part = mu(X, assignment_list(), state_formulas::or_(
     143          14 :                      translate_reg_frms_appl(phi,xyz_generator),
     144          14 :                      translate_reg_frms_appl(may(R,mcrl2::state_formulas::variable(X, data_expression_list())),xyz_generator)
     145           7 :                ));
     146           7 :     }
     147             :     else
     148             :     {
     149             :       //reg_frm is an action formula; reduce phi
     150          71 :       part = may(reg_frm, translate_reg_frms_appl(phi,xyz_generator));
     151             :     }
     152          78 :   }
     153         309 :   else if (state_formulas::is_not(part))
     154             :   {
     155          29 :     const state_formulas::not_& not_part = atermpp::down_cast<state_formulas::not_>(part);
     156          29 :     part = state_formulas::not_(translate_reg_frms_appl(not_part.operand(),xyz_generator));
     157             :   }
     158         280 :   else if (state_formulas::is_minus(part))
     159             :   {
     160           0 :     const state_formulas::minus& minus_part = atermpp::down_cast<state_formulas::minus>(part);
     161           0 :     part = state_formulas::minus(translate_reg_frms_appl(minus_part.operand(),xyz_generator));
     162             :   }
     163         280 :   else if (state_formulas::is_and(part))
     164             :   {
     165         134 :     part = state_formulas::and_(translate_reg_frms_appl(state_formulas::and_(part).left(),xyz_generator),
     166         201 :                 translate_reg_frms_appl(state_formulas::and_(part).right(),xyz_generator));
     167             :   }
     168         213 :   else if (state_formulas::is_or(part))
     169             :   {
     170          40 :     part = state_formulas::or_(translate_reg_frms_appl(state_formulas::or_(part).left(),xyz_generator),
     171          60 :                translate_reg_frms_appl(state_formulas::or_(part).right(),xyz_generator));
     172             :   }
     173         193 :   else if (state_formulas::is_imp(part))
     174             :   {
     175          46 :     part = state_formulas::imp(translate_reg_frms_appl(state_formulas::imp(part).left(),xyz_generator),
     176          69 :                 translate_reg_frms_appl(state_formulas::imp(part).right(),xyz_generator));
     177             :   }
     178         170 :   else if (state_formulas::is_plus(part))
     179             :   {
     180           0 :     part = state_formulas::plus(translate_reg_frms_appl(state_formulas::plus(part).left(),xyz_generator),
     181           0 :                 translate_reg_frms_appl(state_formulas::plus(part).right(),xyz_generator));
     182             :   }
     183         170 :   else if (state_formulas::is_const_multiply(part))
     184             :   {
     185           0 :     part = state_formulas::const_multiply(state_formulas::const_multiply(part).left(),
     186           0 :                 translate_reg_frms_appl(state_formulas::const_multiply(part).right(),xyz_generator));
     187             :   }
     188         170 :   else if (state_formulas::is_const_multiply_alt(part))
     189             :   {
     190           0 :     part = state_formulas::const_multiply_alt(translate_reg_frms_appl(state_formulas::const_multiply_alt(part).left(),xyz_generator),
     191           0 :                 state_formulas::const_multiply_alt(part).right());
     192             :   }
     193         170 :   else if (state_formulas::is_forall(part))
     194             :   {
     195          30 :     part = mcrl2::state_formulas::forall(mcrl2::state_formulas::forall(part).variables(),
     196          45 :                   translate_reg_frms_appl(mcrl2::state_formulas::forall(part).body(),xyz_generator));
     197             :   }
     198         155 :   else if (state_formulas::is_exists(part))
     199             :   {
     200          12 :     part = mcrl2::state_formulas::exists(mcrl2::state_formulas::exists(part).variables(),
     201          18 :                   translate_reg_frms_appl(mcrl2::state_formulas::exists(part).body(),xyz_generator));
     202             :   }
     203         149 :   else if (state_formulas::is_infimum(part))
     204             :   {
     205           2 :     part = mcrl2::state_formulas::infimum(mcrl2::state_formulas::infimum(part).variables(),
     206           3 :                   translate_reg_frms_appl(mcrl2::state_formulas::infimum(part).body(),xyz_generator));
     207             :   }
     208         148 :   else if (state_formulas::is_supremum(part))
     209             :   {
     210           2 :     part = mcrl2::state_formulas::supremum(mcrl2::state_formulas::supremum(part).variables(),
     211           3 :                   translate_reg_frms_appl(mcrl2::state_formulas::supremum(part).body(),xyz_generator));
     212             :   }
     213         147 :   else if (state_formulas::is_nu(part))
     214             :   {
     215          59 :     const nu nu_part(part);
     216         118 :     part = nu(nu_part.name(),nu_part.assignments(),
     217         177 :                   translate_reg_frms_appl(nu_part.operand(),xyz_generator));
     218          59 :   }
     219          88 :   else if (state_formulas::is_mu(part))
     220             :   {
     221          88 :     const mu mu_part(part);
     222         176 :     part = mu(mu_part.name(),mu_part.assignments(),
     223         264 :                   translate_reg_frms_appl(mu_part.operand(),xyz_generator));
     224          88 :   }
     225             :   else
     226             :   {
     227           0 :     assert(0); //Unexpected state_formula.
     228             :   }
     229             : 
     230         807 :   return part;
     231             : }
     232             : 
     233             : }   // namespace detail
     234             : }   // namespace regular_formulas
     235             : }     // namespace mcrl2

Generated by: LCOV version 1.14