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.hpp>
      18             : 
      19             : using namespace mcrl2;
      20             : using namespace mcrl2::data;
      21             : using namespace mcrl2::lps;
      22             : 
      23             : 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           1 :   specification spec = parse_linear_process_specification(SPEC);
      38           1 :   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           1 :   assignment a(c, d);
      43           1 :   const action_summand& t = s;
      44           1 :   BOOST_CHECK(t==s);
      45           1 : }
      46             : 
      47             : std::string SPEC1a =
      48             :   "act  action: Nat;         \n"
      49             :   "                          \n"
      50             :   "proc P(s: Pos, i: Nat) =  \n"
      51             :   "       (s == 2) ->        \n"
      52             :   "         action(i) .      \n"
      53             :   "         P(1, i)          \n"
      54             :   "     + (s == 1) ->        \n"
      55             :   "         action(i) .      \n"
      56             :   "         P(2, i)          \n"
      57             :   "     + true ->            \n"
      58             :   "         delta;           \n"
      59             :   "                          \n"
      60             :   "init P(1, 0);             \n"
      61             :   ;
      62             : 
      63             : std::string SPEC1b =
      64             :   "act  action: Nat;         \n"
      65             :   "                          \n"
      66             :   "proc P(s: Pos, i: Nat) =  \n"
      67             :   "       (3 == 2) ->        \n"
      68             :   "         action(4) .      \n"
      69             :   "         P(1, 4)          \n"
      70             :   "     + (3 == 1) ->        \n"
      71             :   "         action(4) .      \n"
      72             :   "         P(2, 4)          \n"
      73             :   "     + true ->            \n"
      74             :   "         delta;           \n"
      75             :   "                          \n"
      76             :   "init P(1, 0);             \n"
      77             :   ;
      78             : 
      79           1 : void test_lps_substituter()
      80             : {
      81           1 :   specification spec1 = parse_linear_process_specification(SPEC1a);
      82           1 :   specification spec2 = parse_linear_process_specification(SPEC1b);
      83           1 :   data::mutable_map_substitution<> sigma;
      84           1 :   sigma[variable("s", sort_pos::pos())] = sort_pos::pos(3);
      85           1 :   sigma[variable("i", sort_nat::nat())] = sort_nat::nat(4);
      86             : 
      87           1 :   lps::replace_variables(spec1, sigma);
      88           1 :   std::cerr << lps::pp(spec1.process()) << std::endl;
      89           1 :   std::cerr << "-------------------------------------" << std::endl;
      90           1 :   std::cerr << lps::pp(spec2.process()) << std::endl;
      91           1 :   BOOST_CHECK(lps::pp(spec1.process()) == lps::pp(spec2.process()));
      92           1 : }
      93             : 
      94           1 : void test_lps_substitute()
      95             : {
      96           2 :   data::variable v("v", data::bool_());
      97           1 :   const data::data_expression& w = data::true_();
      98           1 :   data::mutable_map_substitution<> sigma;
      99           1 :   sigma[v] = w;
     100           1 :   data::data_expression e = v;
     101           1 :   e = lps::replace_free_variables(e, sigma);
     102           1 : }
     103             : 
     104           1 : void test_replace_process_parameters()
     105             : {
     106             :   std::string SPEC =
     107             :     "act a;                        \n"
     108             :     "proc P(b:Bool) = a.P(b = !b); \n"
     109           1 :     "init P(true);                 \n"
     110             :     ;
     111           1 :   specification spec = parse_linear_process_specification(SPEC);
     112           1 :   data::mutable_map_substitution<> sigma;
     113           2 :   data::variable b("b", data::bool_());
     114           2 :   data::variable b0("b0", data::bool_());
     115           1 :   sigma[b] = b0;
     116           1 :   lps::replace_process_parameters(spec, sigma);
     117           1 :   std::set<data::variable> variables = lps::find_all_variables(spec);
     118           1 :   BOOST_CHECK(variables.find(b) == variables.end());
     119           1 : }
     120             : 
     121           1 : void test_replace_summand_variables()
     122             : {
     123             :   std::string SPEC =
     124             :     "act a;                                   \n"
     125             :     "proc P(b:Bool) = sum c:Bool. a.P(b = c); \n"
     126           1 :     "init P(true);                            \n"
     127             :     ;
     128           1 :   specification spec = parse_linear_process_specification(SPEC);
     129           1 :   data::mutable_map_substitution<> sigma;
     130           2 :   data::variable c("c", data::bool_());
     131           2 :   data::variable c0("c0", data::bool_());
     132           1 :   sigma[c] = c0;
     133           1 :   lps::replace_summand_variables(spec, sigma);
     134           1 :   std::cout << lps::pp(spec) << std::endl;
     135           1 :   std::set<data::variable> variables = lps::find_all_variables(spec);
     136           1 :   BOOST_CHECK(variables.find(c) == variables.end());
     137           1 : }
     138             : 
     139           1 : void test_action_list()
     140             : {
     141           1 :   sort_expression_list s;
     142           1 :   s.push_front(sort_expression(sort_nat::nat()));
     143           2 :   process::action_label label(core::identifier_string("a"), s);
     144             : 
     145           2 :   variable b("b", data::bool_());
     146           2 :   variable c("c", data::bool_());
     147           1 :   data_expression_list e1;
     148           1 :   e1.push_front(data_expression(data::and_(b, c)));
     149           1 :   data_expression_list e2;
     150           1 :   e2.push_front(data_expression(data::and_(c, c)));
     151             : 
     152           1 :   process::action_list l1;
     153           1 :   process::action a1(label, e1);
     154           1 :   l1.push_front(a1);
     155             : 
     156           1 :   process::action_list l2;
     157           1 :   process::action a2(label, e2);
     158           1 :   l2.push_front(a2);
     159             : 
     160           1 :   data::mutable_map_substitution<> sigma;
     161           1 :   sigma[b] = c;
     162             : 
     163           1 :   l1 = process::replace_variables_capture_avoiding(l1, sigma);
     164           1 :   BOOST_CHECK(l1 == l2);
     165             : 
     166           1 :   l1 = process::replace_variables(l1, sigma);
     167           1 :   l1 = process::replace_variables_capture_avoiding(l1, sigma);
     168           1 : }
     169             : 
     170           2 : BOOST_AUTO_TEST_CASE(test_main)
     171             : {
     172           1 :   test_replace();
     173           1 :   test_lps_substituter();
     174           1 :   test_lps_substitute();
     175           1 :   test_replace_process_parameters();
     176           1 :   test_replace_summand_variables();
     177           1 :   test_action_list();
     178           1 : }