Line data Source code
1 : // Author(s): Wieger Wesselink 2 : // Copyright: see the accompanying file COPYING. 3 : // 4 : // Distributed under the Boost Software License, Version 1.0. 5 : // (See accompanying file LICENSE_1_0.txt or copy at 6 : // http://www.boost.org/LICENSE_1_0.txt) 7 : // 8 : /// \file remove_parameters_test.cpp 9 : /// \brief Tests for removing parameters. 10 : 11 : #define BOOST_TEST_MODULE remove_parameters_test 12 : #include <boost/test/included/unit_test.hpp> 13 : 14 : #include "mcrl2/pbes/detail/test_utility.h" 15 : #include "mcrl2/pbes/remove_parameters.h" 16 : 17 : using namespace mcrl2; 18 : using namespace mcrl2::pbes_system; 19 : using namespace mcrl2::pbes_system::detail; 20 : 21 2 : BOOST_AUTO_TEST_CASE(test_propositional_variable) 22 : { 23 6 : data::variable_list d = { nat("n"), pos("p"), bool_("b"), bool_("c") } ; 24 2 : propositional_variable X = propvar("X", d); 25 1 : std::vector<std::size_t> v; 26 1 : v.push_back(1); 27 1 : v.push_back(3); 28 1 : propositional_variable X1 = pbes_system::remove_parameters(X, v); 29 4 : data::variable_list d1 = { nat("n"), bool_("b") }; 30 1 : BOOST_CHECK(X1 == propvar("X", d1)); 31 1 : } 32 : 33 2 : BOOST_AUTO_TEST_CASE(test_propositional_variable_instantiation) 34 : { 35 6 : data::data_expression_list d = { nat("n"), pos("p"), bool_("b"), bool_("c") } ; 36 2 : propositional_variable_instantiation X = propvarinst("X", d); 37 1 : std::vector<std::size_t> v; 38 1 : v.push_back(1); 39 1 : v.push_back(3); 40 1 : propositional_variable_instantiation X1 = pbes_system::remove_parameters(X, v); 41 4 : data::data_expression_list d1 = { nat("n"), bool_("b") }; 42 1 : BOOST_CHECK(X1 == propvarinst("X", d1)); 43 1 : } 44 : 45 2 : BOOST_AUTO_TEST_CASE(test_pbes_expression) 46 : { 47 4 : data::variable_list d1 = { nat("m"), bool_("b") }; 48 5 : data::variable_list d2 = { nat("m"), bool_("b"), nat("p") } ; 49 2 : propositional_variable X1 = propvar("X1", d1); 50 2 : propositional_variable X2 = propvar("X2", d2); 51 : 52 4 : data::data_expression_list e1 = { data::sort_nat::plus(nat("m"), nat("n")), bool_("b") }; 53 5 : data::data_expression_list e2 = { data::sort_nat::times(nat("m"), nat("n")), bool_("b"), nat("p") }; 54 2 : propositional_variable_instantiation x1 = propvarinst("X1", e1); 55 2 : propositional_variable_instantiation x2 = propvarinst("X2", e2); 56 : 57 1 : pbes_expression p = and_(x1, x2); 58 : 59 1 : std::map<core::identifier_string, std::vector<std::size_t> > to_be_removed; 60 1 : std::vector<std::size_t> v1; 61 1 : v1.push_back(1); 62 1 : to_be_removed[X1.name()] = v1; 63 1 : std::vector<std::size_t> v2; 64 1 : v2.push_back(0); 65 1 : v2.push_back(2); 66 1 : to_be_removed[X2.name()] = v2; 67 : 68 1 : pbes_expression q = pbes_system::remove_parameters(p, to_be_removed); 69 : 70 1 : pbes_expression r; 71 : { 72 3 : data::variable_list d1 = { nat("m") }; 73 3 : data::variable_list d2 = { bool_("b") }; 74 2 : propositional_variable X1 = propvar("X1", d1); 75 2 : propositional_variable X2 = propvar("X2", d2); 76 : 77 3 : data::data_expression_list e1 = { data::data_expression(data::sort_nat::plus(nat("m"), nat("n"))) }; 78 3 : data::data_expression_list e2 = { data::data_expression(bool_("b")) }; 79 2 : propositional_variable_instantiation x1 = propvarinst("X1", e1); 80 2 : propositional_variable_instantiation x2 = propvarinst("X2", e2); 81 : 82 1 : r = and_(x1, x2); 83 1 : } 84 1 : BOOST_CHECK(q == r); 85 1 : }