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 resolve_name_clash_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE resolve_name_clash_test
      13             : #include <boost/test/included/unit_test.hpp>
      14             : 
      15             : #include "mcrl2/lps/parse.h"
      16             : #include "mcrl2/lps/resolve_name_clashes.h"
      17             : 
      18             : using namespace mcrl2;
      19             : 
      20           1 : std::set<data::variable> find_summand_variables(const lps::specification& spec)
      21             : {
      22           1 :   std::set<data::variable> result;
      23             : 
      24           1 :   const lps::linear_process& proc = spec.process();
      25           1 :   auto action_summands = proc.action_summands();
      26           3 :   for (auto & action_summand : action_summands)
      27             :   {
      28           2 :     auto variables = action_summand.summation_variables();
      29           2 :     result.insert(variables.begin(), variables.end());
      30           2 :   }
      31           1 :   auto deadlock_summands = proc.deadlock_summands();
      32           2 :   for (auto & deadlock_summand : deadlock_summands)
      33             :   {
      34           1 :     auto variables = deadlock_summand.summation_variables();
      35           1 :     result.insert(variables.begin(), variables.end());
      36           1 :   }
      37             : 
      38           2 :   return result;
      39           1 : }
      40             : 
      41           1 : void test_resolve_name_clashes()
      42             : {
      43             :   std::string SPEC =
      44             :     "act  a;                                 \n"
      45             :     "                                        \n"
      46             :     "proc P(b: Bool, m: Nat, n: Pos) =       \n"
      47             :     "       sum m: Bool.                     \n"
      48             :     "         m ->                           \n"
      49             :     "         a .                            \n"
      50             :     "         P(b = m, m = 1, n = 2)         \n"
      51             :     "     + sum n: Nat.                      \n"
      52             :     "         a .                            \n"
      53             :     "         P(b = true, m = n + 1, n = 3)  \n"
      54             :     "     + delta;                           \n"
      55             :     "                                        \n"
      56           1 :     "init P(true, 4, 5);                     \n"
      57             :     ;
      58           1 :   lps::specification spec = lps::parse_linear_process_specification(SPEC);
      59           1 :   lps::resolve_summand_variable_name_clashes(spec);
      60           1 :   std::set<data::variable> summation_variables = find_summand_variables(spec);
      61           1 :   auto process_parameters = spec.process().process_parameters();
      62           4 :   for (const auto & process_parameter : process_parameters)
      63             :   {
      64           3 :     BOOST_CHECK(summation_variables.find(process_parameter) == summation_variables.end());
      65             :   }
      66           1 : }
      67             : 
      68           2 : BOOST_AUTO_TEST_CASE(test_main)
      69             : {
      70           1 :   test_resolve_name_clashes();
      71           1 : }