Line data Source code
1 : // Author(s): Jeroen Keiren
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 sort_expression_test.cpp
10 : /// \brief Basic regression test for sort expressions.
11 :
12 : #define BOOST_TEST_MODULE sort_expression_test
13 : #include <boost/test/included/unit_test.hpp>
14 :
15 : #include "mcrl2/atermpp/aterm_io.h"
16 : #include "mcrl2/data/alias.h"
17 : #include "mcrl2/data/structured_sort.h"
18 :
19 : using namespace mcrl2;
20 : using namespace mcrl2::data;
21 :
22 2 : BOOST_AUTO_TEST_CASE(basic_sort_test)
23 : {
24 2 : basic_sort s("S");
25 :
26 1 : BOOST_CHECK(is_basic_sort(s));
27 1 : BOOST_CHECK(!is_function_sort(s));
28 1 : BOOST_CHECK(!is_alias(s));
29 1 : BOOST_CHECK(!is_structured_sort(s));
30 1 : BOOST_CHECK(!is_container_sort(s));
31 :
32 1 : BOOST_CHECK_EQUAL(pp(s.name()), "S");
33 1 : BOOST_CHECK_EQUAL(s, s);
34 :
35 2 : basic_sort t("T");
36 1 : BOOST_CHECK(s != t);
37 1 : BOOST_CHECK(s.name() != t.name());
38 :
39 1 : const sort_expression& t_e(t);
40 1 : basic_sort t_e_(t_e);
41 1 : BOOST_CHECK_EQUAL(t_e_, t);
42 1 : BOOST_CHECK_EQUAL(t_e_.name(), t.name());
43 1 : }
44 :
45 2 : BOOST_AUTO_TEST_CASE(function_sort_test)
46 : {
47 2 : basic_sort s0("S0");
48 2 : basic_sort s1("S1");
49 2 : basic_sort s("S");
50 :
51 3 : sort_expression_list s01 = { s0, s1 };
52 1 : function_sort fs(s01, s);
53 1 : BOOST_CHECK(!is_basic_sort(fs));
54 1 : BOOST_CHECK(is_function_sort(fs));
55 1 : BOOST_CHECK(!is_alias(fs));
56 1 : BOOST_CHECK(!is_structured_sort(fs));
57 1 : BOOST_CHECK(!is_container_sort(fs));
58 1 : BOOST_CHECK_EQUAL(fs, fs);
59 1 : BOOST_CHECK_EQUAL(fs.domain().size(), static_cast< std::size_t >(s01.size()));
60 :
61 : // Element wise check
62 1 : sort_expression_list::const_iterator i = s01.begin();
63 1 : sort_expression_list::iterator j = fs.domain().begin();
64 3 : while (i != s01.end() && j != fs.domain().end())
65 : {
66 2 : BOOST_CHECK_EQUAL(*i, *j);
67 2 : ++i;
68 2 : ++j;
69 : }
70 :
71 1 : BOOST_CHECK_EQUAL(fs.domain(), s01);
72 1 : BOOST_CHECK_EQUAL(fs.codomain(), s);
73 :
74 1 : const sort_expression& fs_e(fs);
75 1 : function_sort fs_e_(fs_e);
76 1 : BOOST_CHECK_EQUAL(fs_e_, fs);
77 1 : BOOST_CHECK_EQUAL(fs_e_.domain(), fs.domain());
78 1 : BOOST_CHECK_EQUAL(fs_e_.codomain(), fs.codomain());
79 :
80 1 : BOOST_CHECK_EQUAL(fs, make_function_sort_(s0, s1, s));
81 1 : BOOST_CHECK_EQUAL(fs.domain(), make_function_sort_(s0, s1, s).domain());
82 1 : }
83 :
84 2 : BOOST_AUTO_TEST_CASE(alias_test)
85 : {
86 2 : basic_sort s0("S0");
87 :
88 2 : basic_sort s0_name("other_S");
89 1 : alias s0_(s0_name, s0);
90 1 : BOOST_CHECK(is_alias(s0_));
91 1 : BOOST_CHECK_EQUAL(s0_.name(), s0_name);
92 1 : BOOST_CHECK_EQUAL(s0_.reference(), s0);
93 :
94 1 : const alias& s0_e_(s0_);
95 1 : BOOST_CHECK_EQUAL(s0_e_, s0_);
96 1 : BOOST_CHECK_EQUAL(s0_e_.name(), s0_.name());
97 1 : BOOST_CHECK_EQUAL(s0_e_.reference(), s0_.reference());
98 1 : }
99 :
100 2 : BOOST_AUTO_TEST_CASE(structured_sort_test)
101 : {
102 2 : basic_sort s0("S0");
103 2 : basic_sort s1("S1");
104 1 : structured_sort_constructor_argument p0("p0", s0);
105 1 : structured_sort_constructor_argument p1(s1);
106 1 : BOOST_CHECK_EQUAL(pp(p0.name()), "p0");
107 1 : BOOST_CHECK_EQUAL(p1.name(), core::empty_identifier_string());
108 1 : BOOST_CHECK_EQUAL(p0.sort(), s0);
109 1 : BOOST_CHECK_EQUAL(p1.sort(), s1);
110 :
111 1 : structured_sort_constructor_argument_vector a1;
112 1 : a1.push_back(p0);
113 1 : a1.push_back(p1);
114 1 : structured_sort_constructor_argument_vector a2;
115 1 : a2.push_back(p0);
116 :
117 1 : structured_sort_constructor c1("c1", a1, "is_c1");
118 2 : structured_sort_constructor c2("c2", a2);
119 1 : BOOST_CHECK_EQUAL(pp(c1.name()), "c1");
120 1 : BOOST_CHECK(structured_sort_constructor_argument_vector(c1.arguments().begin(),c1.arguments().end()) == a1);
121 1 : BOOST_CHECK_EQUAL(pp(c1.recogniser()), "is_c1");
122 1 : BOOST_CHECK_EQUAL(pp(c2.name()), "c2");
123 1 : BOOST_CHECK(structured_sort_constructor_argument_vector(c2.arguments().begin(),c2.arguments().end()) == a2);
124 1 : BOOST_CHECK_EQUAL(c2.recogniser(), core::empty_identifier_string());
125 :
126 3 : structured_sort_constructor_list cs = { c1, c2 };
127 :
128 1 : structured_sort s(cs);
129 :
130 1 : BOOST_CHECK(!is_basic_sort(s));
131 1 : BOOST_CHECK(!is_function_sort(s));
132 1 : BOOST_CHECK(!is_alias(s));
133 1 : BOOST_CHECK(is_structured_sort(s));
134 1 : BOOST_CHECK(!is_container_sort(s));
135 :
136 1 : BOOST_CHECK_EQUAL(s.constructors(), cs);
137 :
138 1 : const sort_expression& s_e(s);
139 1 : structured_sort s_e_(s_e);
140 1 : BOOST_CHECK_EQUAL(s_e_, s);
141 1 : BOOST_CHECK_EQUAL(s_e_.constructors(), s.constructors());
142 :
143 3 : structured_sort_constructor_argument_vector nv {structured_sort_constructor_argument(static_cast<sort_expression const&>(sort_nat::nat()))};
144 3 : structured_sort_constructor_argument_vector bv {structured_sort_constructor_argument(static_cast<sort_expression const&>(sort_bool::bool_()))};
145 2 : structured_sort_constructor b("B", nv);
146 2 : structured_sort_constructor c("C", bv);
147 5 : structured_sort bc(structured_sort_constructor_list({b,c}));
148 :
149 3 : BOOST_CHECK_EQUAL(bc.constructors(), structured_sort_constructor_list({ b, c }));
150 1 : structured_sort_constructor_vector bc_constructors(bc.constructors().begin(), bc.constructors().end());
151 1 : BOOST_CHECK_EQUAL(bc_constructors[0], b);
152 1 : BOOST_CHECK_EQUAL(bc_constructors[1], c);
153 1 : BOOST_CHECK(!bc_constructors[0].arguments().empty());
154 1 : BOOST_CHECK(!bc_constructors[1].arguments().empty());
155 1 : BOOST_CHECK(sort_nat::is_nat(bc_constructors[0].arguments().begin()->sort()));
156 1 : BOOST_CHECK(sort_bool::is_bool(bc_constructors[1].arguments().begin()->sort()));
157 1 : }
158 :
159 2 : BOOST_AUTO_TEST_CASE(container_sort_test)
160 : {
161 2 : basic_sort s0("S0");
162 2 : basic_sort s1("S1");
163 1 : container_sort ls0(list_container(), s0);
164 2 : container_sort ls1(list_container(), s1);
165 :
166 1 : BOOST_CHECK_EQUAL(ls0.container_name(), list_container());
167 1 : BOOST_CHECK_EQUAL(ls0.element_sort(), s0);
168 1 : BOOST_CHECK_EQUAL(ls1.element_sort(), s1);
169 1 : BOOST_CHECK(ls0.element_sort() != ls1.element_sort());
170 1 : }
171 :
|
