Line data Source code
1 : // Author(s): Unknown
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 confcheck_test.cpp
10 : /// \brief Add your file description here.
11 :
12 : #define BOOST_TEST_MODULE confcheck_test
13 : #include <boost/test/included/unit_test.hpp>
14 :
15 : #include "mcrl2/lps/confluence_checker.h"
16 : #include "mcrl2/lps/parse.h"
17 :
18 :
19 : using namespace mcrl2;
20 : using namespace mcrl2::data;
21 : using namespace mcrl2::core;
22 : using namespace mcrl2::lps;
23 : using namespace mcrl2::lps::detail;
24 :
25 : //static bool check_for_ctau(lps::specification const& s) .
26 5 : static std::size_t count_ctau(specification const& s)
27 : {
28 5 : std::size_t result = 0;
29 5 : auto const& v_summands = s.process().action_summands();
30 :
31 25 : for (const auto & v_summand : v_summands)
32 : {
33 20 : const process::action_list al=v_summand.multi_action().actions();
34 20 : if (al.size()==1)
35 : {
36 17 : const process::action_label lab=al.front().label();
37 17 : if (pp(lab.name())=="ctau")
38 : {
39 6 : ++result;
40 : }
41 17 : }
42 20 : }
43 5 : return result;
44 : }
45 :
46 : static
47 5 : void run_confluence_test_case(const std::string& s, const std::size_t ctau_count)
48 : {
49 : using namespace mcrl2::lps;
50 :
51 5 : specification s0 = parse_linear_process_specification(s);
52 10 : Confluence_Checker<specification> checker1(s0);
53 : // Check confluence for all summands and
54 : // replace confluents tau's by ctau's.
55 5 : checker1.check_confluence_and_mark(data::sort_bool::true_(),0);
56 :
57 5 : BOOST_CHECK_EQUAL(count_ctau(s0), ctau_count);
58 5 : }
59 :
60 2 : BOOST_AUTO_TEST_CASE(case_1)
61 : {
62 : /*
63 : act a, b;
64 : init tau.a + tau.b;
65 : */
66 : const std::string s(
67 : "act Terminate,a,b;\n"
68 : "proc P(s3: Pos) =\n"
69 : " (s3 == 5) ->\n"
70 : " b .\n"
71 : " P(s3 = 3)\n"
72 : " + (s3 == 3) ->\n"
73 : " Terminate .\n"
74 : " P(s3 = 4)\n"
75 : " + (s3 == 2) ->\n"
76 : " a .\n"
77 : " P(s3 = 3)\n"
78 : " + sum e: Bool.\n"
79 : " (if(e, true, true) && s3 == 1) ->\n"
80 : " tau .\n"
81 : " P(s3 = if(e, 5, 2))\n"
82 : " + delta;\n"
83 : "init P(1);\n"
84 1 : );
85 :
86 1 : run_confluence_test_case(s,0);
87 1 : }
88 :
89 :
90 2 : BOOST_AUTO_TEST_CASE(case_2)
91 : {
92 : /*
93 : act a, b;
94 : init a.tau.b.delta;
95 : */
96 : const std::string s(
97 : "act a,b;\n"
98 : "proc P(s3: Pos) =\n"
99 : " (s3 == 3) ->\n"
100 : " b .\n"
101 : " P(s3 = 4)\n"
102 : " + (s3 == 2) ->\n"
103 : " tau .\n"
104 : " P(s3 = 3)\n"
105 : " + (s3 == 1) ->\n"
106 : " a .\n"
107 : " P(s3 = 2)\n"
108 : " + delta;\n"
109 : "init P(1);\n"
110 1 : );
111 :
112 1 : run_confluence_test_case(s,1);
113 1 : }
114 :
115 2 : BOOST_AUTO_TEST_CASE(case_3)
116 : {
117 : /*
118 : act a, b;
119 : init a.b.delta;
120 : */
121 : const std::string s(
122 : "act a,b;\n"
123 : "proc P(s3: Pos) =\n"
124 : " (s3 == 2) ->\n"
125 : " b .\n"
126 : " P(s3 = 3)\n"
127 : " + (s3 == 1) ->\n"
128 : " a .\n"
129 : " P(s3 = 2)\n"
130 : " + delta;\n"
131 : "init P(1);\n"
132 1 : );
133 1 : run_confluence_test_case(s,0);
134 1 : }
135 :
136 : // The following test case unearthed an assertion failure when applying
137 : // substitutions.
138 2 : BOOST_AUTO_TEST_CASE(case_4)
139 : {
140 : const std::string s(
141 : "proc P(m: Int) =\n"
142 : " (m == 1) ->\n"
143 : " tau .\n"
144 : " P(m = m - 1)\n"
145 : " + (m == 1) ->\n"
146 : " tau .\n"
147 : " P()\n"
148 : " + delta;\n"
149 : "\n"
150 : "init P(0);\n"
151 1 : );
152 1 : run_confluence_test_case(s,0);
153 1 : }
154 :
155 : // Test case provided by Jaco van der Pol
156 : // in some versions the algorithm hangs on this example.
157 2 : BOOST_AUTO_TEST_CASE(case_5)
158 : {
159 : const std::string s(
160 : "sort Byte = struct ESC | END | OTHER;\n"
161 : " Enum3 = struct e2_3 | e1_3 | e0_3;\n"
162 : " Enum4 = struct e3_4 | e2_4 | e1_4 | e0_4;\n"
163 : "map special: Byte -> Bool;\n"
164 : "var b: Byte;\n"
165 : "eqn special(b) = b == ESC || b == END;\n"
166 : "act r,s,r1,s1,r2,s2,c1,c2: Byte;\n"
167 : "proc P(s3_S: Enum3, b_S: Byte, s30_C: Bool, b_C: Byte, s31_R: Enum4, b_R,b0_R: Byte) =\n"
168 : " sum b1_S: Byte.\n"
169 : " (s3_S == e2_3 && !(b1_S == ESC || b1_S == END)) ->\n"
170 : " r(b1_S) .\n"
171 : " P(s3_S = e0_3, b_S = b1_S)\n"
172 : " + sum b2_S: Byte.\n"
173 : " (s3_S == e2_3 && (b2_S == ESC || b2_S == END)) ->\n"
174 : " r(b2_S) .\n"
175 : " P(s3_S = e1_3, b_S = b2_S)\n"
176 : " + ((s30_C && s31_R == e3_4) && ESC == b_C) ->\n"
177 : " tau .\n"
178 : " P(s30_C = false, b_C = ESC, s31_R = e2_4, b_R = ESC, b0_R = ESC)\n"
179 : " + ((s30_C && s31_R == e3_4) && !(b_C == ESC)) ->\n"
180 : " tau .\n"
181 : " P(s30_C = false, b_C = ESC, s31_R = e0_4, b_R = b_C, b0_R = ESC)\n"
182 : " + (s30_C && s31_R == e2_4) ->\n"
183 : " tau .\n"
184 : " P(s30_C = false, b_C = ESC, s31_R = e1_4, b_R = ESC, b0_R = b_C)\n"
185 : " + (s31_R == e1_4) ->\n"
186 : " s(b0_R) .\n"
187 : " P(s31_R = e3_4, b_R = ESC, b0_R = ESC)\n"
188 : " + (s31_R == e0_4) ->\n"
189 : " s(b_R) .\n"
190 : " P(s31_R = e3_4, b_R = ESC, b0_R = ESC)\n"
191 : " + (s3_S == e0_3 && !s30_C) ->\n"
192 : " tau .\n"
193 : " P(s3_S = e2_3, b_S = ESC, s30_C = true, b_C = b_S)\n"
194 : " + (s3_S == e1_3 && !s30_C) ->\n"
195 : " tau .\n"
196 : " P(s3_S = e0_3, s30_C = true, b_C = ESC)\n"
197 : " + delta;\n"
198 : "init P(e2_3, ESC, false, ESC, e3_4, ESC, ESC);\n"
199 1 : );
200 1 : run_confluence_test_case(s,5);
201 1 : }
202 :
|