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 one_point_condition_rewriter_test.cpp
10 : /// \brief Tests for rewriter that uses LPS condition to simplify the right
11 : /// hand side of a summand.
12 :
13 : #define BOOST_TEST_MODULE one_point_condition_rewriter_test
14 : #include <boost/test/included/unit_test.hpp>
15 :
16 : #include "mcrl2/data/detail/parse_substitution.h"
17 : #include "mcrl2/lps/detail/specification_property_map.h"
18 : #include "mcrl2/lps/rewriters/one_point_condition_rewrite.h"
19 : #include "mcrl2/lps/parse.h"
20 : #include "mcrl2/lps/rewrite.h"
21 :
22 : using namespace mcrl2;
23 : using namespace mcrl2::data;
24 : using namespace mcrl2::data::detail;
25 : using namespace mcrl2::lps;
26 : using namespace mcrl2::lps::detail;
27 :
28 : // Checks if rewriting the specification src with the substitutions sigma
29 : // results in the specification dest.
30 2 : void test_one_point_condition_rewriter(const std::string& src_text, const std::string& dest_text)
31 : {
32 2 : lps::specification src = parse_linear_process_specification(src_text);
33 2 : lps::specification dest = parse_linear_process_specification(dest_text);
34 :
35 : // rewrite the specification src
36 2 : data::rewriter R(src.data());
37 2 : lps::one_point_condition_rewrite(src, R);
38 :
39 2 : if (src != dest)
40 : {
41 0 : std::cerr << "--- test failed ---" << std::endl;
42 0 : std::cerr << lps::pp(src) << std::endl;
43 0 : std::cerr << "-------------------" << std::endl;
44 0 : std::cerr << lps::pp(dest) << std::endl;
45 : }
46 2 : BOOST_CHECK(src == dest);
47 2 : }
48 :
49 1 : void test_one_point_condition_rule_rewriter()
50 : {
51 : std::string src =
52 : "act a: Nat;\n"
53 : "\n"
54 : "proc P(n: Nat) = (n == 0) -> a(n + 1). P(n + 2);\n"
55 : "\n"
56 1 : "init P(0);\n";
57 :
58 : std::string expected_result =
59 : "act a: Nat;\n"
60 : "\n"
61 : "proc P(n: Nat) = (n == 0) -> a(1). P(2);\n"
62 : "\n"
63 1 : "init P(0);\n";
64 :
65 1 : test_one_point_condition_rewriter(src, expected_result);
66 1 : }
67 :
68 1 : void test_parunfold_example()
69 : {
70 : std::string src =
71 : "sort ListNat;\n"
72 : "\n"
73 : "cons c_,c_1: ListNat;\n"
74 : "\n"
75 : "map C_ListNat: ListNat # List(Nat) # List(Nat) -> List(Nat);\n"
76 : "Det_ListNat: List(Nat) -> ListNat;\n"
77 : "pi_ListNat: List(Nat) -> Nat;\n"
78 : "pi_ListNat1: List(Nat) -> List(Nat);\n"
79 : "C_ListNat: ListNat # Bool # Bool -> Bool;\n"
80 : "C_ListNat: ListNat # ListNat # ListNat -> ListNat;\n"
81 : "C_ListNat: ListNat # Nat # Nat -> Nat;\n"
82 : "\n"
83 : "var d1,d2: List(Nat);\n"
84 : "d,d6,d7: ListNat;\n"
85 : "d3,d8: Nat;\n"
86 : "d4,d5: Bool;\n"
87 : "eqn C_ListNat(c_, d1, d2) = d1;\n"
88 : "C_ListNat(c_1, d1, d2) = d2;\n"
89 : "C_ListNat(d, d2, d2) = d2;\n"
90 : "Det_ListNat([]) = c_;\n"
91 : "Det_ListNat(d3 |> d1) = c_1;\n"
92 : "pi_ListNat(d3 |> d1) = d3;\n"
93 : "pi_ListNat([]) = 0;\n"
94 : "pi_ListNat1(d3 |> d1) = d1;\n"
95 : "pi_ListNat1([]) = [];\n"
96 : "C_ListNat(c_, d4, d5) = d4;\n"
97 : "C_ListNat(c_1, d4, d5) = d5;\n"
98 : "C_ListNat(d, d5, d5) = d5;\n"
99 : "C_ListNat(d, d4, d5) = d4 && d == c_ || d5 && d == c_1;\n"
100 : "C_ListNat(c_, d6, d7) = d6;\n"
101 : "C_ListNat(c_1, d6, d7) = d7;\n"
102 : "C_ListNat(d, d7, d7) = d7;\n"
103 : "C_ListNat(c_, d3, d8) = d3;\n"
104 : "C_ListNat(c_1, d3, d8) = d8;\n"
105 : "C_ListNat(d, d8, d8) = d8;\n"
106 : "\n"
107 : "act a: Nat;\n"
108 : "\n"
109 : "proc P(stack_pp: ListNat, stack_pp1: Nat, stack_pp2: List(Nat)) =\n"
110 : " (stack_pp == c_1) ->\n"
111 : " a(C_ListNat(stack_pp, head([]), stack_pp1)) .\n"
112 : " P(stack_pp = C_ListNat(stack_pp, Det_ListNat(tail([])), Det_ListNat(stack_pp2)), stack_pp1 = C_ListNat(stack_pp, pi_ListNat(tail([])), pi_ListNat(stack_pp2)), stack_pp2 = C_ListNat(stack_pp, pi_ListNat1(tail([])), pi_ListNat1(stack_pp2)));\n"
113 : "\n"
114 1 : "init P(c_1, 1, []);\n";
115 :
116 : std::string expected_result =
117 : "sort ListNat;\n"
118 : "\n"
119 : "cons c_,c_1: ListNat;\n"
120 : "\n"
121 : "map C_ListNat: ListNat # List(Nat) # List(Nat) -> List(Nat);\n"
122 : "Det_ListNat: List(Nat) -> ListNat;\n"
123 : "pi_ListNat: List(Nat) -> Nat;\n"
124 : "pi_ListNat1: List(Nat) -> List(Nat);\n"
125 : "C_ListNat: ListNat # Bool # Bool -> Bool;\n"
126 : "C_ListNat: ListNat # ListNat # ListNat -> ListNat;\n"
127 : "C_ListNat: ListNat # Nat # Nat -> Nat;\n"
128 : "\n"
129 : "var d1,d2: List(Nat);\n"
130 : "d,d6,d7: ListNat;\n"
131 : "d3,d8: Nat;\n"
132 : "d4,d5: Bool;\n"
133 : "eqn C_ListNat(c_, d1, d2) = d1;\n"
134 : "C_ListNat(c_1, d1, d2) = d2;\n"
135 : "C_ListNat(d, d2, d2) = d2;\n"
136 : "Det_ListNat([]) = c_;\n"
137 : "Det_ListNat(d3 |> d1) = c_1;\n"
138 : "pi_ListNat(d3 |> d1) = d3;\n"
139 : "pi_ListNat([]) = 0;\n"
140 : "pi_ListNat1(d3 |> d1) = d1;\n"
141 : "pi_ListNat1([]) = [];\n"
142 : "C_ListNat(c_, d4, d5) = d4;\n"
143 : "C_ListNat(c_1, d4, d5) = d5;\n"
144 : "C_ListNat(d, d5, d5) = d5;\n"
145 : "C_ListNat(d, d4, d5) = d4 && d == c_ || d5 && d == c_1;\n"
146 : "C_ListNat(c_, d6, d7) = d6;\n"
147 : "C_ListNat(c_1, d6, d7) = d7;\n"
148 : "C_ListNat(d, d7, d7) = d7;\n"
149 : "C_ListNat(c_, d3, d8) = d3;\n"
150 : "C_ListNat(c_1, d3, d8) = d8;\n"
151 : "C_ListNat(d, d8, d8) = d8;\n"
152 : "\n"
153 : "act a: Nat;\n"
154 : "\n"
155 : "proc P(stack_pp: ListNat, stack_pp1: Nat, stack_pp2: List(Nat)) =\n"
156 : " (stack_pp == c_1) ->\n"
157 : " a(stack_pp1) .\n"
158 : " P(stack_pp = Det_ListNat(stack_pp2), stack_pp1 = pi_ListNat(stack_pp2), stack_pp2 = pi_ListNat1(stack_pp2));\n"
159 : "\n"
160 1 : "init P(c_1, 1, []);\n";
161 :
162 1 : test_one_point_condition_rewriter(src, expected_result);
163 1 : }
164 :
165 2 : BOOST_AUTO_TEST_CASE(test_main)
166 : {
167 1 : test_one_point_condition_rule_rewriter();
168 1 : test_parunfold_example();
169 1 : }
|
