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 find_test.cpp 10 : /// \brief Add your file description here. 11 : 12 : #define BOOST_TEST_MODULE find_test 13 : #include <boost/test/included/unit_test.hpp> 14 : 15 : #include "mcrl2/pbes/find.h" 16 : #include "mcrl2/pbes/detail/parse.h" 17 : #include "mcrl2/pbes/print.h" 18 : #include "mcrl2/pbes/txt2pbes.h" 19 : 20 : using namespace mcrl2; 21 : using namespace mcrl2::pbes_system; 22 : 23 : inline 24 4 : data::variable nat(const std::string& name) 25 : { 26 8 : return data::variable(core::identifier_string(name), data::sort_nat::nat()); 27 : } 28 : 29 : inline 30 : data::variable pos(const std::string& name) 31 : { 32 : return data::variable(core::identifier_string(name), data::sort_pos::pos()); 33 : } 34 : 35 : inline 36 : data::variable bool_(const std::string& name) 37 : { 38 : return data::variable(core::identifier_string(name), data::bool_()); 39 : } 40 : 41 2 : BOOST_AUTO_TEST_CASE(test_find) 42 : { 43 : const std::string VARSPEC = 44 : "datavar \n" 45 : " m: Nat; \n" 46 : " n: Nat; \n" 47 : " \n" 48 : "predvar \n" 49 : " X: Bool, Pos; \n" 50 1 : " Y: Nat; \n" 51 : ; 52 : 53 2 : pbes_expression x = parse_pbes_expression("X(true, 2) && Y(n+1) && Y(m)", VARSPEC); 54 : 55 : //--- find_all_variables ---// 56 2 : data::variable m = nat("m"); 57 2 : data::variable n = nat("n"); 58 1 : std::set<data::variable> v = pbes_system::find_all_variables(x); 59 5 : std::set<data::variable> v_expected = { m, n }; 60 1 : BOOST_CHECK(v == v_expected); 61 : 62 : //--- find_sort_expressions ---// 63 1 : std::set<data::sort_expression> s = pbes_system::find_sort_expressions(x); 64 1 : std::cout << "s = " << core::detail::print_set(s) << std::endl; 65 5 : std::set<data::sort_expression> s_expected = { data::sort_nat::nat(), data::sort_pos::pos() }; 66 1 : BOOST_CHECK(std::includes(s.begin(), s.end(), s_expected.begin(), s_expected.end())); 67 1 : } 68 : 69 2 : BOOST_AUTO_TEST_CASE(test_free_variables) 70 : { 71 : const std::string VARSPEC = 72 : "datavar \n" 73 : " n: Nat; \n" 74 : " \n" 75 : "predvar \n" 76 : " X: Bool, Pos; \n" 77 1 : " Y: Nat; \n" 78 : ; 79 : 80 2 : pbes_expression x = parse_pbes_expression("forall m:Nat.(X(true, 2) && Y(n+1) && Y(m))", VARSPEC); 81 2 : data::variable m = nat("m"); 82 2 : data::variable n = nat("n"); 83 : 84 1 : std::set<data::variable> v = pbes_system::find_free_variables(x); 85 4 : std::set<data::variable> v_expected = { n }; 86 1 : BOOST_CHECK(v == v_expected); 87 1 : } 88 : 89 2 : BOOST_AUTO_TEST_CASE(test_find_free_variables) 90 : { 91 : std::string test1 = 92 : "pbes \n" 93 : " \n" 94 : "nu X(b:Bool, n:Nat) = (val(b) => X(!b, n)) && (val(!b) => X(!b, n+1)); \n" 95 : "mu Y(c:Nat, d:Bool) = forall m:Nat. Y(c, true) || X(d, m); \n" 96 : " \n" 97 1 : "init X(true, 0); \n" 98 : ; 99 : 100 1 : pbes p = txt2pbes(test1); 101 : 102 1 : std::set<data::variable> v = find_free_variables(p); 103 1 : BOOST_CHECK(v.empty()); 104 : 105 1 : v = find_free_variables(p.equations()[0]); 106 1 : BOOST_CHECK(v.empty()); 107 : 108 1 : v = find_free_variables(p.equations()[1]); 109 1 : BOOST_CHECK(v.empty()); 110 : 111 1 : v = find_free_variables(p.equations()[0].formula()); 112 1 : BOOST_CHECK(v.size() == 2); 113 : 114 1 : v = find_free_variables(p.equations()[1].formula()); 115 1 : BOOST_CHECK(v.size() == 2); 116 1 : }