Line data Source code
1 : #include "mcrl2/lps/linearise.h"
2 : #include "mcrl2/lps/parelm.h"
3 :
4 : using namespace mcrl2;
5 :
6 0 : void test_parelm(const std::string& spec_text)
7 : {
8 0 : lps::stochastic_specification spec1 = lps::linearise(spec_text);
9 0 : lps::stochastic_specification spec2 = spec1;
10 0 : lps::parelm(spec2);
11 0 : std::cout << "<before>\n" << lps::pp(spec1.process()) << std::endl;
12 0 : std::cout << "<after>\n" << lps::pp(spec2.process()) << std::endl;
13 0 : std::cout << "------------------------------------------------------------------------" << std::endl;
14 0 : }
15 :
16 : std::string SPEC1 =
17 : "% Test Case 1 \n"
18 : "% \n"
19 : "% Process parameter i should be removed. \n"
20 : " \n"
21 : "act a; \n"
22 : " \n"
23 : "proc X(i: Nat) = a.X(i); \n"
24 : " \n"
25 : "init X(2); \n"
26 : ;
27 :
28 : std::string SPEC2 =
29 : "% Test Case 2 \n"
30 : "% \n"
31 : "% Process parameter j should be removed \n"
32 : " \n"
33 : "act a: Nat; \n"
34 : " \n"
35 : "proc X(i,j: Nat) = a(i). X(i,j); \n"
36 : " \n"
37 : "init X(0,1); \n"
38 : ;
39 :
40 : std::string SPEC3 =
41 : "% Test Case 3 \n"
42 : "% \n"
43 : "% Process parameter j should be removed \n"
44 : " \n"
45 : "act a; \n"
46 : " \n"
47 : "proc X(i,j: Nat) = (i == 5) -> a. X(i,j); \n"
48 : " \n"
49 : "init X(0,1); \n"
50 : ;
51 :
52 : std::string SPEC4 =
53 : "% Test Case 4 \n"
54 : "% \n"
55 : "% Process parameter j should be removed \n"
56 : " \n"
57 : "act a; \n"
58 : " \n"
59 : "proc X(i,j: Nat) = a@i.X(i,j); \n"
60 : " \n"
61 : "init X(0,4); \n"
62 : ;
63 :
64 : std::string SPEC5 =
65 : "% Test Case 5 \n"
66 : "% \n"
67 : "% No process parameter should be removed \n"
68 : " \n"
69 : "act a: Nat; \n"
70 : "act b; \n"
71 : " \n"
72 : "proc X(i,j,k: Nat) = a(i).X(k,j,k) + \n"
73 : " b.X(j,j,k); \n"
74 : " \n"
75 : "init X(1,2,3); \n"
76 : ;
77 :
78 : std::string SPEC6 =
79 : "% Test Case 6 \n"
80 : "% \n"
81 : "% The following LPS is generated: \n"
82 : "% \n"
83 : "% proc P(s3: Pos, i,j: Nat) = \n"
84 : "% (s3 == 1 && i < 5) -> \n"
85 : "% act1(i) . \n"
86 : "% P(s3 := 1, i := i + 1, j := freevar0) \n"
87 : "% + (s3 == 1 && i == 5) -> \n"
88 : "% act3(i) . \n"
89 : "% P(s3 := 2, j := i) \n"
90 : "% + (s3 == 2) -> \n"
91 : "% act2(j) . \n"
92 : "% P(s3 := 2, j := j + 1); \n"
93 : "% \n"
94 : "% var freevar: Nat; \n"
95 : "% init P(s3 := 1, i := 0, j := freevar); \n"
96 : "% \n"
97 : "% from this mcrl2 specification: \n"
98 : " \n"
99 : "act act1, act2, act3: Nat; \n"
100 : " \n"
101 : "proc X(i: Nat) = (i < 5) -> act1(i).X(i+1) + \n"
102 : " (i == 5) -> act3(i).Y(i, i); \n"
103 : " Y(i,j: Nat) = act2(j).Y(i,j+1); \n"
104 : " \n"
105 : "init X(0); \n"
106 : " \n"
107 : "% In this LPS no process parameters can be eliminated \n"
108 : "% Because all process parameters are used \n"
109 : "% \n"
110 : "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \n"
111 : "%% NOTE: %% \n"
112 : "%% ===== %% \n"
113 : "%% %% \n"
114 : "%% Use: mcrl22lps --no-cluster $DIR$/case6.mcrl2 %% \n"
115 : "%% %% \n"
116 : "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \n"
117 : ;
118 :
119 : std::string SPEC7 =
120 : "% Test Case 7 \n"
121 : "% \n"
122 : "% The following LPS is generated: \n"
123 : "% \n"
124 : "% act act1,act2,act3: Nat; \n"
125 : "% \n"
126 : "% proc P(i,z,j: Nat) = \n"
127 : "% (i == 5) -> \n"
128 : "% act3(i) . \n"
129 : "% P(z := j,j := 4) \n"
130 : "% + (i < 5) -> \n"
131 : "% act1(i) @ Nat2Real(z) . \n"
132 : "% P(i := i + 1); \n"
133 : "% \n"
134 : "% init P(i := 0, z := Pos2Nat(5), j := Pos2Nat(1)); \n"
135 : "% \n"
136 : "% from this mcrl2 specification: \n"
137 : " \n"
138 : "act act1, act2, act3: Nat; \n"
139 : " \n"
140 : "proc X(i,z,j: Nat) = (i < 5) -> act1(i)@z.X(i+1,z, j) + \n"
141 : " (i == 5) -> act3(i).X(i, j, 4); \n"
142 : " \n"
143 : "init X(0,5, 1); \n"
144 : " \n"
145 : "% No process parameters are removed. z is dependent of j. \n"
146 : "% \n"
147 : "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \n"
148 : "%% NOTE: %% \n"
149 : "%% ===== %% \n"
150 : "%% %% \n"
151 : "%% Use: mcrl22lps --no-cluster $DIR$/case7.mcrl2 %% \n"
152 : "%% %% \n"
153 : "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \n"
154 : ;
155 :
156 0 : void test_stochastic_specification()
157 : {
158 : std::string text =
159 : "% Test Case 1 \n"
160 : "% \n"
161 : "% Process parameter i should be removed. \n"
162 : " \n"
163 : "act a; \n"
164 : " \n"
165 : "proc X(i: Nat) = a.X(i); \n"
166 : " \n"
167 0 : "init X(2); \n"
168 : ;
169 0 : lps::stochastic_specification spec1 = lps::linearise(text);
170 0 : lps::stochastic_specification spec2 = spec1;
171 0 : lps::parelm(spec2);
172 0 : std::cout << "<before>\n" << lps::pp(spec1.process()) << std::endl;
173 0 : std::cout << "<after>\n" << lps::pp(spec2.process()) << std::endl;
174 0 : }
175 :
176 0 : int main(int /* argc*/, char** /* argv*/ )
177 : {
178 0 : test_parelm(SPEC1);
179 0 : test_parelm(SPEC2);
180 0 : test_parelm(SPEC3);
181 0 : test_parelm(SPEC4);
182 0 : test_parelm(SPEC5);
183 0 : test_parelm(SPEC6);
184 0 : test_parelm(SPEC7);
185 0 : test_stochastic_specification();
186 :
187 0 : return 0;
188 : }
|
