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 sort_traverser_test.cpp
10 : /// \brief Add your file description here.
11 :
12 : #define BOOST_TEST_MODULE sort_traverser_test
13 : #include <boost/test/included/unit_test.hpp>
14 : #include "mcrl2/pbes/find.h"
15 : #include "mcrl2/pbes/txt2pbes.h"
16 :
17 : using namespace mcrl2;
18 : using namespace mcrl2::pbes_system;
19 :
20 14 : void test_pbes(const std::string& text)
21 : {
22 14 : pbes p = txt2pbes(text);
23 14 : std::set<data::sort_expression> sorts;
24 14 : pbes_system::find_sort_expressions(p, std::inserter(sorts, sorts.end()));
25 14 : std::cerr << "sorts: " << data::pp(data::sort_expression_list(sorts.begin(), sorts.end())) << std::endl;
26 14 : }
27 :
28 2 : BOOST_AUTO_TEST_CASE(test1)
29 : {
30 : std::string t1 =
31 : "% simple test, n is constant \n"
32 : " \n"
33 : "pbes nu X(n: Nat) = \n"
34 : " X(n); \n"
35 : " \n"
36 1 : "init X(0); \n"
37 : ;
38 :
39 : std::string t2 =
40 : "% simple test, n is NOT constant \n"
41 : " \n"
42 : "pbes nu X(n: Nat) = \n"
43 : " X(n + 1); \n"
44 : " \n"
45 1 : "init X(0); \n"
46 : ;
47 :
48 : std::string t3 =
49 : "% multiple parameters: n1 is constant, n2 is not \n"
50 : " \n"
51 : "pbes nu X(n1,n2: Nat) = \n"
52 : " X(n1, n2 + 1); \n"
53 : " \n"
54 1 : "init X(0, 1); \n"
55 : ;
56 :
57 : std::string t4 =
58 : "% conditions: n is not constant, even if conditions are enabled\n"
59 : " \n"
60 : "pbes nu X(n: Nat) = \n"
61 : " val(2 < n) || X(n + 1); \n"
62 : " \n"
63 1 : "init X(0); \n"
64 : ;
65 :
66 : std::string t5 =
67 : "% conditions: n is constant if conditions are enabled \n"
68 : " \n"
69 : "pbes nu X(n: Nat) = \n"
70 : " val(2 < n) || X(n + 1); \n"
71 : " \n"
72 1 : "init X(5); \n"
73 : ;
74 :
75 : std::string t6 =
76 : "% reachability: n1 is not constant, equation Y is not reachable and should be removed \n"
77 : " \n"
78 : "pbes nu X(n1: Nat) = X(n1+1); \n"
79 : " mu Y(n2: Nat) = Y(n2+1); \n"
80 : " \n"
81 1 : "init X(5); \n"
82 : ;
83 :
84 : std::string t7 =
85 : "% multiple edges from one vertex, one edge invalidates the assertion of the other: no constants should be found \n"
86 : " \n"
87 : "pbes \n"
88 : " mu X1(n1,m1:Nat) = X2(n1) || X2(m1); \n"
89 : " mu X2(n2:Nat) = X1(n2,n2); \n"
90 : "init \n"
91 1 : " X1(2,1); \n"
92 : ;
93 :
94 : std::string t8 =
95 : "% conditions: parameters b,c and d will always be removed, with conditions on, parameter \n"
96 : "% n will NOT be removed. changing b,c or d to false or n to a bigger number \n"
97 : "% then 5 WILL result in the removal of n \n"
98 : " \n"
99 : "pbes nu X(b,c,d:Bool, n:Nat) = \n"
100 : " val(b) || ( val(c) && ( val(d) && (val(n > 5) || X(b,c,d,n+1)))); \n"
101 : " \n"
102 : "init \n"
103 1 : "X(false,true,true,5); \n"
104 : ;
105 :
106 : std::string t9 =
107 : "% conditions: universal quantification which can be solved, n1 and n2 are \n"
108 : "% constants if conditions are enabled \n"
109 : " \n"
110 : "pbes mu X(n1,n2:Nat) = \n"
111 : " forall m:Nat. (val(n1>n2) && X(n1+1,n2+1)); \n"
112 : " \n"
113 1 : "init X(1,2); \n"
114 : ;
115 :
116 : std::string t10 =
117 : "% conditions: existential quantification which can be solved, n1 and n2 \n"
118 : "% are constants if conditions are enabled \n"
119 : " \n"
120 : "pbes mu X(n1,n2:Nat) = \n"
121 : " exists m:Nat. (val(n1>n2) && X(n1+1,n2+1)); \n"
122 : " \n"
123 1 : "init X(1,2); \n"
124 : ;
125 :
126 : std::string t11 =
127 : "% conditions: universal quantification which cannot be solved \n"
128 : "% (by the current rewriter), n1 and n2 are constants, but not \n"
129 : "% detected as such \n"
130 : " \n"
131 : "pbes mu X(n1,n2:Nat) = \n"
132 : " forall m:Nat. (val(m>n2) && X(n1+1,n2+1)); \n"
133 : " \n"
134 1 : "init X(1,2); \n"
135 : ;
136 :
137 : std::string t12 =
138 : "% example 4.2.1 from \"Tools for PBES\" report \n"
139 : "% constants without conditions: o4, n2, n4, o4 \n"
140 : "% constants with conditions: everything (equations X1,X2,X3 and X4 are removed) \n"
141 : " \n"
142 : "pbes \n"
143 : " mu X1(n1,m1,o1,p1:Nat) = (val(n1<m1) || X2(o1,p1)) && X3(n1) && X1(n1,m1,4,p1); \n"
144 : " mu X2(n2,m2:Nat) = X5(n2,m2) || X5(m2,n2); \n"
145 : " nu X3(n3:Nat) = val(n3<3) || X1(n3,n3,4,n3+1); \n"
146 : " nu X4(n4,m4,o4:Nat) = val(n4 <= m4+o4) || (X3(n4) && X4(n4,m4+1,n4)); \n"
147 : " mu X5(n5,m5:Nat) = val(n5>m5) || X3(n5); \n"
148 : " \n"
149 : "init \n"
150 1 : " X4(0,0,0); \n"
151 : ;
152 :
153 : std::string t13 =
154 : "pbes nu X = \n"
155 : " Y(true); \n"
156 : " mu Y(b: Bool) = \n"
157 : " X; \n"
158 : " \n"
159 1 : "init X; \n"
160 : ;
161 :
162 : std::string t14 =
163 : "pbes nu X(m:Nat) = \n"
164 : " forall n:Nat . X(n); \n"
165 : " \n"
166 1 : "init X(0); \n"
167 : ;
168 :
169 1 : test_pbes(t1);
170 1 : test_pbes(t2);
171 1 : test_pbes(t3);
172 1 : test_pbes(t4);
173 1 : test_pbes(t5);
174 1 : test_pbes(t6);
175 1 : test_pbes(t7);
176 1 : test_pbes(t8);
177 1 : test_pbes(t9);
178 1 : test_pbes(t10);
179 1 : test_pbes(t11);
180 1 : test_pbes(t12);
181 1 : test_pbes(t13);
182 1 : test_pbes(t14);
183 1 : }
|
