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 remove_parameters_test.cpp 10 : /// \brief Add your file description here. 11 : 12 : #define BOOST_TEST_MODULE remove_parameters_test 13 : #include <boost/test/included/unit_test.hpp> 14 : 15 : #include "mcrl2/lps/detail/lps_algorithm.h" 16 : #include "mcrl2/lps/detail/specification_property_map.h" 17 : #include "mcrl2/lps/detail/test_input.h" 18 : #include "mcrl2/lps/linearise.h" 19 : #include "mcrl2/lps/parse.h" 20 : 21 : using namespace mcrl2; 22 : using namespace mcrl2::data; 23 : using namespace mcrl2::lps; 24 : 25 : std::string SPEC = 26 : "act action: Nat; \n" 27 : " \n" 28 : "proc P(s: Pos, i: Nat) = \n" 29 : " (s == 2) -> \n" 30 : " action(3) . \n" 31 : " P(1, 4) \n" 32 : " + (s == 1) -> \n" 33 : " action(4) . \n" 34 : " P(2, 4) \n" 35 : " + true -> \n" 36 : " delta; \n" 37 : " \n" 38 : "init P(1, 0); \n" 39 : ; 40 : 41 1 : void test_remove_parameters() 42 : { 43 1 : specification spec = parse_linear_process_specification(SPEC); 44 : // remove parameters 45 1 : std::set<data::variable> to_be_removed; 46 1 : to_be_removed.insert(variable("s", sort_pos::pos())); 47 1 : to_be_removed.insert(variable("i", sort_nat::nat())); 48 : 49 : // check the result 50 1 : std::string expected_result = "process_parameter_names ="; 51 1 : lps::detail::specification_property_map<> info(spec); 52 : 53 1 : specification spec2 = parse_linear_process_specification(SPEC); 54 1 : remove_parameters(spec2, to_be_removed); 55 1 : lps::detail::specification_property_map<> info2(spec2); 56 1 : BOOST_CHECK(data::detail::compare_property_maps("test_remove_parameters", info2, expected_result)); 57 1 : } 58 : 59 1 : void test_instantiate_free_variables() 60 : { 61 2 : specification spec = remove_stochastic_operators(linearise(lps::detail::ABP_SPECIFICATION())); 62 1 : lps::detail::lps_algorithm<> algorithm(spec); 63 1 : algorithm.instantiate_free_variables(); 64 1 : } 65 : 66 1 : void test_remove_redundant_assignments() 67 : { 68 : std::string lpsspec_text = 69 : "act a;\n" 70 : "proc P(x: Nat) = a.P(x = x);\n" 71 1 : "init P(0);" 72 : ; 73 : std::string expected_result_text = 74 : "act a;\n" 75 : "proc P(x: Nat) = a.P();\n" 76 1 : "init P(0);" 77 : ; 78 : 79 1 : specification result = parse_linear_process_specification(lpsspec_text); 80 1 : remove_redundant_assignments(result); 81 1 : specification expected_result = parse_linear_process_specification(expected_result_text); 82 1 : BOOST_CHECK(result == expected_result); 83 : 84 : lpsspec_text = 85 : "act a;\n" 86 : "proc P(x: Nat) = sum x: Nat. a.P(x = x);\n" 87 1 : "init P(0);" 88 : ; 89 : expected_result_text = 90 : "act a;\n" 91 : "proc P(x: Nat) = sum x: Nat. a.P(x = x);\n" 92 1 : "init P(0);" 93 : ; 94 1 : result = parse_linear_process_specification(lpsspec_text); 95 1 : remove_redundant_assignments(result); 96 1 : expected_result = parse_linear_process_specification(expected_result_text); 97 1 : BOOST_CHECK(result == expected_result); 98 1 : } 99 : 100 2 : BOOST_AUTO_TEST_CASE(test_main) 101 : { 102 1 : test_remove_parameters(); 103 1 : test_instantiate_free_variables(); 104 1 : test_remove_redundant_assignments(); 105 1 : }