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 rename_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE rename_test
      13             : #include <boost/test/included/unit_test.hpp>
      14             : 
      15             : #include "mcrl2/lps/linearise.h"
      16             : 
      17             : using namespace mcrl2;
      18             : using namespace mcrl2::core;
      19             : using namespace mcrl2::data;
      20             : using namespace mcrl2::lps;
      21             : using namespace mcrl2::lps::detail;
      22             : 
      23             : const std::string SPECIFICATION =
      24             :   "% Test Case 3                                                     \n"
      25             :   "%                                                                 \n"
      26             :   "% rename:                                                         \n"
      27             :   "% var                                                             \n"
      28             :   "%   x:Bool;                                                       \n"
      29             :   "%   y:Nat;                                                        \n"
      30             :   "%   z:Nat;                                                        \n"
      31             :   "% rename                                                          \n"
      32             :   "%   a(x,y) => a(x,y);                                             \n"
      33             :   "                                                                  \n"
      34             :   "act                                                               \n"
      35             :   "  a: Bool#Nat;                                                    \n"
      36             :   "                                                                  \n"
      37             :   "proc                                                              \n"
      38             :   "  X(x:Bool, y:Nat)= sum z:Nat. (y<=z && z<3) -> a(x,y).X(!x,y+1); \n"
      39             :   "                                                                  \n"
      40             :   "init                                                              \n"
      41             :   "  X(true,0);                                                      \n"
      42             :   ;
      43             : 
      44             : const std::string SPECIFICATION2 =
      45             :   "act a:Nat;                              \n"
      46             :   "                                        \n"
      47             :   "map smaller: Nat#Nat -> Bool;           \n"
      48             :   "                                        \n"
      49             :   "var x,y : Nat;                          \n"
      50             :   "                                        \n"
      51             :   "eqn smaller(x,y) = x < y;               \n"
      52             :   "                                        \n"
      53             :   "proc P(n:Nat) = sum m: Nat. a(m). P(m); \n"
      54             :   "                                        \n"
      55             :   "init P(0);                              \n"
      56             :   ;
      57             : 
      58             : const std::string SPECIFICATION3 =
      59             :   "act a;                                  \n"
      60             :   "                                        \n"
      61             :   "proc P(b:Bool) = a. P(b);               \n"
      62             :   "                                        \n"
      63             :   "init P(false);                          \n"
      64             :   ;
      65             : 
      66           1 : void test_lps_rename()
      67             : {
      68           1 :   specification spec=remove_stochastic_operators(linearise(SPECIFICATION));
      69           1 :   linear_process p = spec.process();
      70           1 :   std::set<identifier_string> forbidden_names;
      71           1 :   forbidden_names.insert(identifier_string("x"));
      72           1 :   forbidden_names.insert(identifier_string("y"));
      73           1 :   forbidden_names.insert(identifier_string("z"));
      74             :   // linear_process q = rename_summation_variables(p, forbidden_names, "_S");
      75             : 
      76             :   // summand_list summands = q.summands();
      77             :   // for (summand_list::iterator i = summands.begin(); i != summands.end(); ++i)
      78             :   // {
      79             :   //   variable_list summation_variables(i->summation_variables());
      80             :   //   for (variable_list::iterator j = summation_variables.begin(); j != summation_variables.end(); ++j)
      81             :   //   {
      82             :   //     BOOST_CHECK(std::find(forbidden_names.begin(), forbidden_names.end(), j->name()) == forbidden_names.end());
      83             :   //   }
      84             :   // }
      85             : 
      86             :   // p = rename_process_parameters(p, forbidden_names, "_P");
      87             :   // spec = rename_process_parameters(spec, forbidden_names, "_S");
      88           1 : }
      89             : 
      90           1 : void test_rename()
      91             : {
      92           1 :   specification spec=remove_stochastic_operators(linearise(SPECIFICATION3));
      93           1 :   std::set<identifier_string> forbidden_names;
      94             :   // specification spec2 = rename_process_parameters(spec, forbidden_names, "_A");
      95             :   // std::cout << "<spec>"  << lps::pp(spec) << std::endl;
      96             :   // std::cout << "<spec2>" << lps::pp(spec2) << std::endl;
      97             :   // BOOST_CHECK(spec2.process().process_parameters().size() == 1);
      98             :   // BOOST_CHECK(spec.process().process_parameters().front().name() == spec2.process().process_parameters().front().name());
      99           1 : }
     100             : 
     101           2 : BOOST_AUTO_TEST_CASE(test_main)
     102             : {
     103           1 :   test_rename();
     104           1 :   test_lps_rename();
     105           1 : }