LCOV - code coverage report
Current view: top level - lps/test - replace_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 86 86 100.0 %
Date: 2020-09-22 00:46:14 Functions: 10 10 100.0 %
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 replace_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE replace_test
      13             : #include "mcrl2/data/consistency.h"
      14             : #include "mcrl2/lps/parse.h"
      15             : #include "mcrl2/lps/replace.h"
      16             : 
      17             : #include <boost/test/included/unit_test_framework.hpp>
      18             : 
      19             : using namespace mcrl2;
      20             : using namespace mcrl2::data;
      21             : using namespace mcrl2::lps;
      22             : 
      23           1 : const std::string SPEC =
      24             :   "act  a;                  \n"
      25             :   "                         \n"
      26             :   "proc P(b: Bool) =        \n"
      27             :   "       sum c: Bool.      \n"
      28             :   "         (b == c) ->     \n"
      29             :   "         a .             \n"
      30             :   "         P(c);           \n"
      31             :   "                         \n"
      32             :   "init P(true);            \n"
      33             :   ;
      34             : 
      35           1 : void test_replace()
      36             : {
      37           2 :   specification spec = parse_linear_process_specification(SPEC);
      38           2 :   action_summand s = spec.process().action_summands().front();
      39           2 :   variable b("b", sort_bool::bool_());
      40           2 :   variable c("c", sort_bool::bool_());
      41           2 :   variable d("d", sort_bool::bool_());
      42           2 :   assignment a(c, d);
      43           1 :   const action_summand& t = s;
      44           1 : }
      45             : 
      46           1 : std::string SPEC1a =
      47             :   "act  action: Nat;         \n"
      48             :   "                          \n"
      49             :   "proc P(s: Pos, i: Nat) =  \n"
      50             :   "       (s == 2) ->        \n"
      51             :   "         action(i) .      \n"
      52             :   "         P(1, i)          \n"
      53             :   "     + (s == 1) ->        \n"
      54             :   "         action(i) .      \n"
      55             :   "         P(2, i)          \n"
      56             :   "     + true ->            \n"
      57             :   "         delta;           \n"
      58             :   "                          \n"
      59             :   "init P(1, 0);             \n"
      60             :   ;
      61             : 
      62           1 : std::string SPEC1b =
      63             :   "act  action: Nat;         \n"
      64             :   "                          \n"
      65             :   "proc P(s: Pos, i: Nat) =  \n"
      66             :   "       (3 == 2) ->        \n"
      67             :   "         action(4) .      \n"
      68             :   "         P(1, 4)          \n"
      69             :   "     + (3 == 1) ->        \n"
      70             :   "         action(4) .      \n"
      71             :   "         P(2, 4)          \n"
      72             :   "     + true ->            \n"
      73             :   "         delta;           \n"
      74             :   "                          \n"
      75             :   "init P(1, 0);             \n"
      76             :   ;
      77             : 
      78           1 : void test_lps_substituter()
      79             : {
      80           2 :   specification spec1 = parse_linear_process_specification(SPEC1a);
      81           2 :   specification spec2 = parse_linear_process_specification(SPEC1b);
      82           2 :   data::mutable_map_substitution<> sigma;
      83           1 :   sigma[variable("s", sort_pos::pos())] = sort_pos::pos(3);
      84           1 :   sigma[variable("i", sort_nat::nat())] = sort_nat::nat(4);
      85             : 
      86           1 :   lps::replace_variables(spec1, sigma);
      87           1 :   std::cerr << lps::pp(spec1.process()) << std::endl;
      88           1 :   std::cerr << "-------------------------------------" << std::endl;
      89           1 :   std::cerr << lps::pp(spec2.process()) << std::endl;
      90           1 :   BOOST_CHECK(lps::pp(spec1.process()) == lps::pp(spec2.process()));
      91           1 : }
      92             : 
      93           1 : void test_lps_substitute()
      94             : {
      95           2 :   data::variable v("v", data::bool_());
      96           1 :   const data::data_expression& w = data::true_();
      97           2 :   data::mutable_map_substitution<> sigma;
      98           1 :   sigma[v] = w;
      99           2 :   data::data_expression e = v;
     100           1 :   e = lps::replace_free_variables(e, sigma);
     101           1 : }
     102             : 
     103           1 : void test_replace_process_parameters()
     104             : {
     105             :   std::string SPEC =
     106             :     "act a;                        \n"
     107             :     "proc P(b:Bool) = a.P(b = !b); \n"
     108           2 :     "init P(true);                 \n"
     109             :     ;
     110           2 :   specification spec = parse_linear_process_specification(SPEC);
     111           2 :   data::mutable_map_substitution<> sigma;
     112           2 :   data::variable b("b", data::bool_());
     113           2 :   data::variable b0("b0", data::bool_());
     114           1 :   sigma[b] = b0;
     115           1 :   lps::replace_process_parameters(spec, sigma);
     116           2 :   std::set<data::variable> variables = lps::find_all_variables(spec);
     117           1 :   BOOST_CHECK(variables.find(b) == variables.end());
     118           1 : }
     119             : 
     120           1 : void test_replace_summand_variables()
     121             : {
     122             :   std::string SPEC =
     123             :     "act a;                                   \n"
     124             :     "proc P(b:Bool) = sum c:Bool. a.P(b = c); \n"
     125           2 :     "init P(true);                            \n"
     126             :     ;
     127           2 :   specification spec = parse_linear_process_specification(SPEC);
     128           2 :   data::mutable_map_substitution<> sigma;
     129           2 :   data::variable c("c", data::bool_());
     130           2 :   data::variable c0("c0", data::bool_());
     131           1 :   sigma[c] = c0;
     132           1 :   lps::replace_summand_variables(spec, sigma);
     133           1 :   std::cout << lps::pp(spec) << std::endl;
     134           2 :   std::set<data::variable> variables = lps::find_all_variables(spec);
     135           1 :   BOOST_CHECK(variables.find(c) == variables.end());
     136           1 : }
     137             : 
     138           1 : void test_action_list()
     139             : {
     140           2 :   sort_expression_list s;
     141           1 :   s.push_front(sort_expression(sort_nat::nat()));
     142           2 :   process::action_label label(core::identifier_string("a"), s);
     143             : 
     144           2 :   variable b("b", data::bool_());
     145           2 :   variable c("c", data::bool_());
     146           2 :   data_expression_list e1;
     147           1 :   e1.push_front(data_expression(data::and_(b, c)));
     148           2 :   data_expression_list e2;
     149           1 :   e2.push_front(data_expression(data::and_(c, c)));
     150             : 
     151           2 :   process::action_list l1;
     152           2 :   process::action a1(label, e1);
     153           1 :   l1.push_front(a1);
     154             : 
     155           2 :   process::action_list l2;
     156           2 :   process::action a2(label, e2);
     157           1 :   l2.push_front(a2);
     158             : 
     159           2 :   data::mutable_map_substitution<> sigma;
     160           1 :   sigma[b] = c;
     161             : 
     162           1 :   l1 = process::replace_variables_capture_avoiding(l1, sigma);
     163           1 :   BOOST_CHECK(l1 == l2);
     164             : 
     165           1 :   l1 = process::replace_variables(l1, sigma);
     166           1 :   l1 = process::replace_variables_capture_avoiding(l1, sigma);
     167           1 : }
     168             : 
     169           3 : BOOST_AUTO_TEST_CASE(test_main)
     170             : {
     171           1 :   test_replace();
     172           1 :   test_lps_substituter();
     173           1 :   test_lps_substitute();
     174           1 :   test_replace_process_parameters();
     175           1 :   test_replace_summand_variables();
     176           1 :   test_action_list();
     177           4 : }

Generated by: LCOV version 1.13