LCOV - code coverage report
Current view: top level - lps/test - action_rename_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 112 112 100.0 %
Date: 2020-07-04 00:44:36 Functions: 23 23 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Jan Friso Groote
       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 action_rename_test.cpp
      10             : /// \brief Action rename test.
      11             : 
      12             : #define BOOST_TEST_MODULE action_rename_test
      13             : #include "mcrl2/lps/linearise.h"
      14             : #include "mcrl2/lps/parse.h"
      15             : #include "mcrl2/lps/remove.h"
      16             : #include "mcrl2/lps/rewrite.h"
      17             : #include <boost/test/included/unit_test_framework.hpp>
      18             : 
      19             : using namespace mcrl2;
      20             : using lps::stochastic_specification;
      21             : using lps::action_rename_specification;
      22             : using lps::action_summand;
      23             : using lps::action_summand_vector;
      24             : using lps::deadlock_summand;
      25             : 
      26           1 : void test1()
      27             : {
      28             :   // Check a renaming when more than one renaming rule
      29             :   // for one action is present.
      30             :   const std::string SPEC =
      31             :     "act a:Nat;                               \n"
      32             :     "proc P(n:Nat) = sum m: Nat. a(m). P(m);  \n"
      33           2 :     "init P(0);                               \n";
      34             : 
      35             :   const std::string AR_SPEC =
      36             :     "act b,c:Nat;\n"
      37             :     "var n:Nat;\n"
      38             :     "rename \n"
      39             :     "  (n>4)  -> a(n) => b(n); \n"
      40           2 :     "  (n<22) -> a(n) => c(n); \n";
      41             : 
      42           2 :   stochastic_specification spec=lps::linearise(SPEC);
      43           2 :   std::istringstream ar_spec_stream(AR_SPEC);
      44           2 :   action_rename_specification ar_spec = parse_action_rename_specification(ar_spec_stream, spec);
      45           2 :   stochastic_specification new_spec = action_rename(ar_spec,spec);
      46           1 :   BOOST_CHECK(new_spec.process().summand_count()==3);
      47           1 : }
      48             : 
      49           1 : void test2()
      50             : {
      51             :   // Check whether new declarations in the rename file
      52             :   // are read properly. Check for renamings of more than one action.
      53             :   const std::string SPEC =
      54             :     "act a,b:Nat;                             \n"
      55             :     "proc P(n:Nat) = sum m: Nat. a(m). P(m);  \n"
      56           2 :     "init P(0);                               \n";
      57             : 
      58             :   const std::string AR_SPEC =
      59             :     "map f:Nat->Nat; \n"
      60             :     "var n':Nat; \n"
      61             :     "eqn f(n')=3; \n"
      62             :     "act c:Nat; \n"
      63             :     "var n:Nat; \n"
      64             :     "rename \n"
      65             :     "  (f(n)>23) -> a(n) => b(n); \n"
      66           2 :     "  b(n) => c(n); \n";
      67             : 
      68           2 :   stochastic_specification spec=lps::linearise(SPEC);
      69           2 :   std::istringstream ar_spec_stream(AR_SPEC);
      70           2 :   action_rename_specification ar_spec = parse_action_rename_specification(ar_spec_stream, spec);
      71           2 :   stochastic_specification new_spec = action_rename(ar_spec,spec);
      72           1 :   BOOST_CHECK(new_spec.process().summand_count()==2);
      73           1 : }
      74             : 
      75           1 : void test3()
      76             : {
      77             :   // Check whether constants in an action_rename file are properly translated.
      78             :   const std::string SPEC =
      79             :     "act a,b:Nat;                             \n"
      80             :     "proc P(n:Nat) = a(1). P(n)+b(1).P(1);  \n"
      81           2 :     "init P(0);                               \n";
      82             : 
      83             :   const std::string AR_SPEC =
      84             :     "rename \n"
      85           2 :     "  a(1) => delta; \n";
      86             : 
      87           2 :   stochastic_specification spec=lps::linearise(SPEC);
      88           2 :   std::istringstream ar_spec_stream(AR_SPEC);
      89           2 :   action_rename_specification ar_spec = parse_action_rename_specification(ar_spec_stream, spec);
      90           2 :   data::rewriter R (spec.data(), mcrl2::data::rewriter::strategy());
      91           2 :   stochastic_specification new_spec = action_rename(ar_spec,spec);
      92           1 :   lps::rewrite(new_spec, R);
      93           1 :   lps::remove_trivial_summands(new_spec);
      94           1 :   BOOST_CHECK(new_spec.process().summand_count()==2);
      95           1 : }
      96             : 
      97           1 : void test4()
      98             : {
      99             :   const std::string SPEC =
     100             :     "sort D = struct d1 | d2;\n"
     101             :     "     E = D;\n"
     102             :     "\n"
     103             :     "act a : E;\n"
     104             :     "\n"
     105             :     "proc P(d:D) = a(d) . P(d1);\n"
     106             :     "\n"
     107           2 :     "init P(d2);\n";
     108             : 
     109             :   const std::string AR_SPEC =
     110             :     "var e : E;\n"
     111             :     "rename\n"
     112           2 :     "(e==d1) -> a(e) => tau;\n";
     113             : 
     114           2 :   stochastic_specification spec=lps::linearise(SPEC);
     115           2 :   std::istringstream ar_spec_stream(AR_SPEC);
     116           2 :   action_rename_specification ar_spec = parse_action_rename_specification(ar_spec_stream, spec);
     117           2 :   data::rewriter R (spec.data(), mcrl2::data::rewriter::strategy());
     118           2 :   stochastic_specification new_spec = action_rename(ar_spec,spec);
     119           1 :   lps::rewrite(new_spec, R);
     120           1 :   lps::remove_trivial_summands(new_spec);
     121           1 :   BOOST_CHECK(new_spec.process().summand_count()==2);
     122           1 : }
     123             : 
     124           1 : void test5() // Test whether partial renaming to delta is going well. See bug report #1009.
     125             : {
     126             :   const std::string SPEC =
     127             :     "sort Command = struct com1 | com2;\n"
     128             :     "sort State = struct st1 | st2;\n"
     129             :     "\n"
     130             :     "proc Parent(id: Nat, children: List(Nat)) =\n"
     131             :     "  sum child: Nat, command: Command . (child in children) -> sc(id, child, command) . Parent()\n"
     132             :     "+ sum child: Nat, state: State . (child in children) -> rs(child, id, state) . Parent();\n"
     133             :     "\n"
     134             :     "proc Child(id: Nat, parent: Nat) =\n"
     135             :     "  sum command: Command . rc(parent, id, command) . Child()\n"
     136             :     "+ sum state: State . ss(id, parent, state) . Child();\n"
     137             :     "\n"
     138             :     "act sc, rc, cc: Nat # Nat # Command;\n"
     139             :     "    rs, ss, cs: Nat # Nat # State;\n"
     140             :     "\n"
     141             :     "act none;\n"
     142             :     "\n"
     143             :     "init\n"
     144             :     "  allow({cc, cs, sc, rs},\n"
     145             :     "  comm({sc|rc -> cc, rs|ss->cs},\n"
     146             :     "    Parent(0, [1, 2]) ||\n"
     147             :     "    Child(1, 0) ||\n"
     148             :     "    Child(2, 0)\n"
     149           2 :     "  ));\n";
     150             : 
     151             : 
     152             :   const std::string AR_SPEC =
     153             :     "var c: Command;\n"
     154             :     "    s: State;\n"
     155             :     "rename\n"
     156             :     "  sc(0, 1, c) => delta;\n"
     157           2 :     "  rs(1, 0, s) => delta;\n";
     158             : 
     159             : 
     160           2 :   stochastic_specification spec=lps::linearise(SPEC);
     161           2 :   std::istringstream ar_spec_stream(AR_SPEC);
     162           2 :   action_rename_specification ar_spec = parse_action_rename_specification(ar_spec_stream, spec);
     163           2 :   data::rewriter R (spec.data(), mcrl2::data::rewriter::strategy());
     164           2 :   stochastic_specification new_spec = action_rename(ar_spec,spec);
     165           1 :   lps::rewrite(new_spec, R);
     166           1 :   lps::remove_trivial_summands(new_spec);
     167           1 :   BOOST_CHECK(new_spec.process().summand_count()==8);
     168           1 : }
     169             : 
     170             : // Check whether renaming with a regular expression works well
     171           1 : static void test_regex1()
     172             : {
     173             :   const std::string SPEC =
     174             :   "act a_out, b_out, cout, ab_out, ac_out;\n"
     175           2 :   "init a_out|ab_out . b_out . cout . delta;";
     176             : 
     177           2 :   stochastic_specification spec = lps::linearise(SPEC);
     178             :   // This should rename a_out and ac_out, leaving the rest
     179           2 :   stochastic_specification new_spec = action_rename(std::regex("^([^b]*)_out"), "out_$1", spec);
     180             : 
     181           1 :   BOOST_CHECK(std::string(new_spec.action_labels().front().name()) == "out_a");
     182           1 :   BOOST_CHECK(std::string(new_spec.action_labels().tail().front().name()) == "b_out");
     183           1 :   BOOST_CHECK(std::string(new_spec.action_labels().tail().tail().front().name()) == "cout");
     184           1 :   BOOST_CHECK(std::string(new_spec.action_labels().tail().tail().tail().front().name()) == "ab_out");
     185           1 :   BOOST_CHECK(std::string(new_spec.action_labels().tail().tail().tail().tail().front().name()) == "out_ac");
     186             : 
     187           4 :   BOOST_CHECK(std::any_of(new_spec.process().action_summands().begin(), new_spec.process().action_summands().end(),
     188             :                               [](const action_summand& as){ return lps::pp(as.multi_action()) == "out_a|ab_out"; }));
     189           3 :   BOOST_CHECK(std::any_of(new_spec.process().action_summands().begin(), new_spec.process().action_summands().end(),
     190             :                               [](const action_summand& as){ return lps::pp(as.multi_action()) == "b_out"; }));
     191           2 :   BOOST_CHECK(std::any_of(new_spec.process().action_summands().begin(), new_spec.process().action_summands().end(),
     192             :                               [](const action_summand& as){ return lps::pp(as.multi_action()) == "cout"; }));
     193           1 : }
     194             : 
     195             : // Check whether renaming some actions to delta works
     196           1 : void test_regex2()
     197             : {
     198             :   const std::string SPEC =
     199             :   "act a_out, b_out, cout, ab_out, ac_out;\n"
     200           2 :   "init a_out|ab_out . b_out . cout . delta;";
     201             : 
     202           2 :   stochastic_specification spec = lps::linearise(SPEC);
     203             :   // This should rename a_out, leaving the rest
     204           2 :   stochastic_specification new_spec = action_rename(std::regex("^a_out"), "delta", spec);
     205             : 
     206           1 :   BOOST_CHECK(std::string(new_spec.action_labels().front().name()) == "b_out");
     207           1 :   BOOST_CHECK(std::string(new_spec.action_labels().tail().front().name()) == "cout");
     208           1 :   BOOST_CHECK(std::string(new_spec.action_labels().tail().tail().front().name()) == "ab_out");
     209             : 
     210           3 :   BOOST_CHECK(std::any_of(new_spec.process().action_summands().begin(), new_spec.process().action_summands().end(),
     211             :                               [](const action_summand& as){ return lps::pp(as.multi_action()) == "b_out"; }));
     212           2 :   BOOST_CHECK(std::any_of(new_spec.process().action_summands().begin(), new_spec.process().action_summands().end(),
     213             :                               [](const action_summand& as){ return lps::pp(as.multi_action()) == "cout"; }));
     214             : 
     215           1 :   BOOST_CHECK(new_spec.process().deadlock_summands().size() == 2);
     216           2 :   auto find_result = std::find_if(spec.process().action_summands().begin(), spec.process().action_summands().end(),
     217           5 :     [](const action_summand& as){ return lps::pp(as.multi_action()) == "a_out|ab_out"; });
     218           1 :   BOOST_CHECK(find_result != spec.process().action_summands().end());
     219           1 :   if(find_result != spec.process().action_summands().end())
     220             :   {
     221           3 :     BOOST_CHECK(std::any_of(new_spec.process().deadlock_summands().begin(), new_spec.process().deadlock_summands().end(),
     222             :                                 [&find_result](const deadlock_summand& ds){ return ds.condition() == find_result->condition(); }));
     223             :   }
     224           1 : }
     225             : 
     226             : // Check whether renaming some actions to tau works
     227           1 : void test_regex3()
     228             : {
     229             :   const std::string SPEC =
     230             :   "act a_out, b_out, cout, ab_out, ac_out;\n"
     231           2 :   "init a_out|ab_out . b_out . cout . delta;";
     232             : 
     233           2 :   stochastic_specification spec = lps::linearise(SPEC);
     234             :   // This should rename a_out and cout, leaving the rest
     235           2 :   stochastic_specification new_spec = action_rename(std::regex("^(a_out|cout)$"), "tau", spec);
     236             : 
     237           1 :   BOOST_CHECK(std::string(new_spec.action_labels().front().name()) == "b_out");
     238           1 :   BOOST_CHECK(std::string(new_spec.action_labels().tail().front().name()) == "ab_out");
     239           1 :   BOOST_CHECK(std::string(new_spec.action_labels().tail().tail().front().name()) == "ac_out");
     240             : 
     241           4 :   BOOST_CHECK(std::any_of(new_spec.process().action_summands().begin(), new_spec.process().action_summands().end(),
     242             :                               [](const action_summand& as){ return lps::pp(as.multi_action()) == "ab_out"; }));
     243           3 :   BOOST_CHECK(std::any_of(new_spec.process().action_summands().begin(), new_spec.process().action_summands().end(),
     244             :                               [](const action_summand& as){ return lps::pp(as.multi_action()) == "b_out"; }));
     245           2 :   BOOST_CHECK(std::any_of(new_spec.process().action_summands().begin(), new_spec.process().action_summands().end(),
     246             :                               [](const action_summand& as){ return lps::pp(as.multi_action()) == "tau"; }));
     247           1 : }
     248             : 
     249             : // Check whether the list of actions contains no duplicates after renaming multiple actions
     250             : // to one action.
     251           1 : void test_regex4()
     252             : {
     253             :   const std::string SPEC =
     254             :   "act a_out, b_out;\n"
     255           2 :   "init a_out . b_out . delta;";
     256             : 
     257           2 :   stochastic_specification spec = lps::linearise(SPEC);
     258             :   // This should rename both actions to 'out'
     259           2 :   stochastic_specification new_spec = action_rename(std::regex("^(a|b)_out$"), "out", spec);
     260             : 
     261           1 :   BOOST_CHECK(new_spec.action_labels().size() == 1);
     262           1 :   BOOST_CHECK(std::string(new_spec.action_labels().front().name()) == "out");
     263           1 : }
     264             : 
     265           3 : BOOST_AUTO_TEST_CASE(test_main)
     266             : {
     267           1 :   test1();
     268           1 :   test2();
     269           1 :   test3();
     270           1 :   test4();
     271           1 :   test5();
     272             : 
     273           1 :   test_regex1();
     274           1 :   test_regex2();
     275           1 :   test_regex3();
     276           1 :   test_regex4();
     277           4 : }

Generated by: LCOV version 1.13