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 parelm_test.cpp
10 : /// \brief Add your file description here.
11 :
12 : //#define MCRL2_LPS_PARELM_DEBUG
13 :
14 : #define BOOST_TEST_MODULE parelm_test
15 : #include <boost/algorithm/string.hpp>
16 : #include <boost/test/included/unit_test.hpp>
17 :
18 : #include "mcrl2/lps/detail/specification_property_map.h"
19 : #include "mcrl2/lps/parelm.h"
20 : #include "mcrl2/lps/parse.h"
21 :
22 : using namespace mcrl2;
23 : using namespace mcrl2::data;
24 : using namespace mcrl2::lps;
25 :
26 : const std::string case_1(
27 : "act a;\n\n"
28 : "proc X(i: Nat) = a.X(i);\n\n"
29 : "init X(2);\n");
30 : const std::string expected_1 = "process_parameter_names = ";
31 :
32 : const std::string case_2(
33 : "act a: Nat;\n\n"
34 : "proc X(i,j: Nat) = a(i). X(i,j);\n\n"
35 : "init X(0,1);\n");
36 : const std::string expected_2 = "process_parameter_names = i";
37 :
38 : const std::string case_3(
39 : "act a;\n\n"
40 : "proc X(i,j: Nat) = (i == 5) -> a. X(i,j);\n\n"
41 : "init X(0,1);\n");
42 : const std::string expected_3 = "process_parameter_names = i";
43 :
44 : const std::string case_4(
45 : "act a;\n\n"
46 : "proc X(i,j: Nat) = a@i.X(i,j);\n\n"
47 : "init X(0,4);\n");
48 : const std::string expected_4 = "process_parameter_names = i";
49 :
50 : const std::string case_5(
51 : "act a: Nat;\n"
52 : "act b;\n\n"
53 : "proc X(i,j,k: Nat) = a(i).X(k,j,k) +\n"
54 : " b.X(j,j,k);\n\n"
55 : "init X(1,2,3);");
56 : const std::string expected_5 = "process_parameter_names = i, j, k";
57 :
58 : // % non-linear process corresponding to case 6
59 : // act act1, act2, act3: Nat;
60 : // proc X(i: Nat) = (i < 5) -> act1(i).X(i+1) +
61 : // (i == 5) -> act3(i).Y(i, i);
62 : // Y(i,j: Nat) = act2(j).Y(i,j+1);
63 : // init X(0);
64 : const std::string case_6 =
65 : "act act1,act2,act3: Nat; \n"
66 : " \n"
67 : "var dc1: Nat; \n"
68 : "proc P(s3_X: Pos, i_X,j_X: Nat) = \n"
69 : " (s3_X == 1 && i_X == 5) -> \n"
70 : " act3(i_X) . \n"
71 : " P(2, i_X, i_X) \n"
72 : " + (s3_X == 1 && i_X < 5) -> \n"
73 : " act1(i_X) . \n"
74 : " P(1, i_X + 1, dc1) \n"
75 : " + (s3_X == 2) -> \n"
76 : " act2(j_X) . \n"
77 : " P(2, i_X, j_X + 1); \n"
78 : " \n"
79 : "var dc: Nat; \n"
80 : "init P(1, 0, dc); \n"
81 : ;
82 :
83 : const std::string case_7(
84 : "act act1, act2, act3: Nat;\n\n"
85 : "proc X(i,z,j: Nat) = (i < 5) -> act1(i)@z.X(i+1,z, j) +\n"
86 : " (i == 5) -> act3(i).X(i, j, 4);\n\n"
87 : "init X(0,5, 1);\n"
88 : );
89 : const std::string expected_7 = "process_parameter_names = i, z, j";
90 :
91 : // Example given by Jan Friso. Parameter xi08 is erroneously found.
92 : const std::string case_8 =
93 : "sort Comp = struct smaller?is_smaller | equal?is_equal | larger?is_larger; \n"
94 : " \n"
95 : "map k: Real; \n"
96 : " \n"
97 : "eqn k = 2; \n"
98 : " \n"
99 : "act get,_get,__get,set,_set,__set: Nat; \n"
100 : " cs_in,cs_out: Pos; \n"
101 : " \n"
102 : "proc P(s32_P_init1,s31_P_init1: Pos, id_ID: Nat, xi,xi00,xi01,xi02,xi03,xi04,xi05,xi06,xi07,xi08: Comp) = \n"
103 : " ((((!is_smaller(xi08) && !is_smaller(xi04)) && !is_smaller(xi03)) && !is_smaller(xi02)) && !is_smaller(xi00)) -> \n"
104 : " delta; \n"
105 : " \n"
106 : " init P(1, 1, 0, equal, equal, equal, larger, equal, larger, equal, equal, equal, equal); \n"
107 : ;
108 : const std::string expected_8 = "process_parameter_names = xi00, xi02, xi03, xi04, xi08";
109 :
110 7 : void test_parelm(const std::string& message, const std::string& spec_text, const std::string& expected_result)
111 : {
112 7 : specification spec1 = parse_linear_process_specification(spec_text);
113 7 : specification spec2 = spec1;
114 7 : parelm(spec1, true);
115 7 : parelm(spec2, false);
116 7 : lps::detail::specification_property_map<> info1(spec1);
117 7 : lps::detail::specification_property_map<> info2(spec2);
118 7 : BOOST_CHECK(data::detail::compare_property_maps(message + "a", info1, expected_result));
119 7 : BOOST_CHECK(data::detail::compare_property_maps(message + "b", info2, expected_result));
120 7 : }
121 :
122 1 : void test_parelm()
123 : {
124 1 : test_parelm("case_1", case_1, expected_1);
125 1 : test_parelm("case_2", case_2, expected_2);
126 1 : test_parelm("case_3", case_3, expected_3);
127 1 : test_parelm("case_4", case_4, expected_4);
128 1 : test_parelm("case_5", case_5, expected_5);
129 1 : test_parelm("case_7", case_7, expected_7);
130 1 : test_parelm("case_8", case_8, expected_8);
131 1 : }
132 :
133 2 : BOOST_AUTO_TEST_CASE(test_main)
134 : {
135 1 : test_parelm();
136 1 : }
|
