LCOV - code coverage report
Current view: top level - modal_formula/source - regfrmtrans.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 71 89 79.8 %
Date: 2020-07-11 00:44:39 Functions: 4 4 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             : static 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         147 : state_formula translate_reg_frms(const state_formula &state_frm)
      41             : {
      42         294 :   xyz_identifier_generator xyz_generator(find_identifiers(state_frm));
      43         294 :   return translate_reg_frms_appl(state_frm, xyz_generator);
      44             : }
      45             : 
      46         796 : static state_formula translate_reg_frms_appl(state_formula part, xyz_identifier_generator& xyz_generator)
      47             : {
      48        2369 :   if (data::is_data_expression(part) ||
      49        1554 :       lps::is_multi_action(part) ||
      50        1413 :       state_formulas::is_variable(part) ||
      51        1272 :       data::is_assignment(part) ||
      52        1189 :       state_formulas::is_true(part) ||
      53        1073 :       state_formulas::is_false(part) ||
      54        1040 :       state_formulas::is_yaled(part) ||
      55        1039 :       state_formulas::is_yaled_timed(part) ||
      56        1834 :       state_formulas::is_delay(part) ||
      57         519 :       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         518 :   else if (state_formulas::is_must(part))
      64             :   {
      65             :     //part is the must operator; return equivalent non-regular formula
      66         274 :     const regular_formula reg_frm = must(part).formula();
      67         274 :     const state_formula phi = must(part).operand();
      68         137 :     if (regular_formulas::is_seq(reg_frm))
      69             :     {
      70           6 :       const regular_formula R1 = seq(reg_frm).left();
      71           6 :       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             :     }
      75         134 :     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             :              );
      84             :     }
      85         134 :     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             :     }
      91         134 :     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          14 :       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             :                ));
     101             :     }
     102             :     else
     103             :     {
     104             :       //reg_frm is an action formula; reduce phi
     105         120 :       part = must(reg_frm, translate_reg_frms_appl(phi,xyz_generator));
     106             :     }
     107             :   }
     108         381 :   else if (state_formulas::is_may(part))
     109             :   {
     110             :     //part is the may operator; return equivalent non-regular formula
     111         156 :     regular_formula reg_frm = may(part).formula();
     112         156 :     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             :     }
     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             :              );
     129             :     }
     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             :     }
     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           7 :       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             :                ));
     146             :     }
     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             :   }
     153         303 :   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         274 :   else if (state_formulas::is_and(part))
     159             :   {
     160          67 :     part = state_formulas::and_(translate_reg_frms_appl(state_formulas::and_(part).left(),xyz_generator),
     161         134 :                 translate_reg_frms_appl(state_formulas::and_(part).right(),xyz_generator));
     162             :   }
     163         207 :   else if (state_formulas::is_or(part))
     164             :   {
     165          20 :     part = state_formulas::or_(translate_reg_frms_appl(state_formulas::or_(part).left(),xyz_generator),
     166          40 :                translate_reg_frms_appl(state_formulas::or_(part).right(),xyz_generator));
     167             :   }
     168         187 :   else if (state_formulas::is_imp(part))
     169             :   {
     170          23 :     part = state_formulas::imp(translate_reg_frms_appl(state_formulas::imp(part).left(),xyz_generator),
     171          46 :                 translate_reg_frms_appl(state_formulas::imp(part).right(),xyz_generator));
     172             :   }
     173         164 :   else if (state_formulas::is_forall(part))
     174             :   {
     175          15 :     part = mcrl2::state_formulas::forall(mcrl2::state_formulas::forall(part).variables(),
     176          30 :                   translate_reg_frms_appl(mcrl2::state_formulas::forall(part).body(),xyz_generator));
     177             :   }
     178         149 :   else if (state_formulas::is_exists(part))
     179             :   {
     180           6 :     part = mcrl2::state_formulas::exists(mcrl2::state_formulas::exists(part).variables(),
     181          12 :                   translate_reg_frms_appl(mcrl2::state_formulas::exists(part).body(),xyz_generator));
     182             :   }
     183         143 :   else if (state_formulas::is_nu(part))
     184             :   {
     185         114 :     const nu nu_part(part);
     186          57 :     part = nu(nu_part.name(),nu_part.assignments(),
     187         114 :                   translate_reg_frms_appl(nu_part.operand(),xyz_generator));
     188             :   }
     189          86 :   else if (state_formulas::is_mu(part))
     190             :   {
     191         172 :     const mu mu_part(part);
     192          86 :     part = mu(mu_part.name(),mu_part.assignments(),
     193         172 :                   translate_reg_frms_appl(mu_part.operand(),xyz_generator));
     194             :   }
     195             :   else
     196             :   {
     197           0 :     assert(0); //Unexpected state_formula.
     198             :   }
     199             : 
     200         796 :   return part;
     201             : }
     202             : 
     203             : }   // namespace detail
     204             : }   // namespace regular_formulas
     205         138 : }     // namespace mcrl2

Generated by: LCOV version 1.13