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 multi_action_test.cpp
10 : /// \brief Add your file description here.
11 :
12 : //#define MCRL2_LPS_PARELM_DEBUG
13 :
14 : #define BOOST_TEST_MODULE multi_action_test
15 : #include <boost/test/included/unit_test.hpp>
16 :
17 : #include "mcrl2/data/consistency.h"
18 : #include "mcrl2/data/detail/test_rewriters.h"
19 : #include "mcrl2/lps/print.h"
20 :
21 : using namespace mcrl2;
22 : using namespace mcrl2::data;
23 : using namespace mcrl2::lps;
24 :
25 : /// \brief Returns a data variable of type Nat with a given name
26 : /// \param name A string
27 : /// \return A data variable of type Nat with a given name
28 6 : data::variable nat(const std::string& name)
29 : {
30 12 : return data::variable(core::identifier_string(name), data::sort_nat::nat());
31 : }
32 :
33 25 : process::action act(const std::string& name, data_expression_list parameters)
34 : {
35 25 : std::vector<sort_expression> sorts;
36 50 : for (const auto & parameter : parameters)
37 : {
38 25 : sorts.push_back(parameter.sort());
39 : }
40 25 : process::action_label label(name, sort_expression_list(sorts.begin(), sorts.end()));
41 50 : return process::action(label, parameters);
42 25 : }
43 :
44 10 : void test_multi_actions(const process::action_list& a, const process::action_list& b, const data_expression& expected_result = data::undefined_data_expression())
45 : {
46 10 : std::cout << "--- test_multi_actions ---" << std::endl;
47 20 : data_expression result = equal_multi_actions(multi_action(a), multi_action(b));
48 10 : std::cout << "a = " << lps::pp(a) << std::endl;
49 10 : std::cout << "b = " << lps::pp(b) << std::endl;
50 10 : std::cout << "result = " << lps::pp(result) << std::endl;
51 10 : std::cout << "expected_result = " << lps::pp(expected_result) << std::endl;
52 10 : BOOST_CHECK(expected_result == data::undefined_data_expression() || result == expected_result);
53 10 : }
54 :
55 1 : void test_equal_multi_actions()
56 : {
57 : namespace d = data;
58 :
59 2 : data_expression d1 = nat("d1");
60 2 : data_expression d2 = nat("d2");
61 2 : data_expression d3 = nat("d3");
62 2 : data_expression d4 = nat("d4");
63 4 : process::action_list a1 ( { act("a", data_expression_list({ d1 })) });
64 4 : process::action_list a2 ( { act("a", data_expression_list({ d2 })) });
65 4 : process::action_list b1 ( { act("b", data_expression_list({ d1 })) });
66 4 : process::action_list b2 ( { act("b", data_expression_list({ d2 })) });
67 7 : process::action_list a11 ( { act("a", data_expression_list({ d1 })), act("a", data_expression_list({ d1 })) });
68 7 : process::action_list a12 ( { act("a", data_expression_list({ d1 })), act("a", data_expression_list({ d2 })) });
69 7 : process::action_list a21 ( { act("a", data_expression_list({ d2 })), act("a", data_expression_list({ d1 })) });
70 7 : process::action_list a22 ( { act("a", data_expression_list({ d2 })), act("a", data_expression_list({ d2 })) });
71 7 : process::action_list a34 ( { act("a", data_expression_list({ d3 })), act("a", data_expression_list({ d4 })) });
72 10 : process::action_list a12b1 ( { act("a", data_expression_list({ d1 })), act("a", data_expression_list({ d2 })), act("b", data_expression_list({ d1 })) });
73 10 : process::action_list a34b2 ( { act("a", data_expression_list({ d3 })), act("a", data_expression_list({ d4 })), act("b", data_expression_list({ d2 })) });
74 1 : test_multi_actions(a1, a1, d::true_());
75 1 : test_multi_actions(a1, a2, d::equal_to(d1, d2));
76 1 : test_multi_actions(a11, a11, d::true_());
77 1 : test_multi_actions(a12, a21, d::true_());
78 1 : test_multi_actions(a21, a12, d::true_());
79 1 : test_multi_actions(a11, a22, d::equal_to(d1, d2));
80 1 : test_multi_actions(a1, a12, d::false_());
81 1 : test_multi_actions(a1, b1, d::false_());
82 1 : test_multi_actions(a12, a34);
83 1 : test_multi_actions(a12b1, a34b2);
84 :
85 2 : data_expression m1 = equal_multi_actions(multi_action(a12), multi_action(a34));
86 2 : data_expression m2 = equal_multi_actions(multi_action(a34), multi_action(a12));
87 1 : data_expression n1 = data::detail::normalize_equality(m1);
88 1 : data_expression n2 = data::detail::normalize_equality(m2);
89 1 : data_expression p1 = data::detail::normalize_and_or(n1);
90 1 : data_expression p2 = data::detail::normalize_and_or(n2);
91 1 : std::cout << "m1 = " << data::pp(m1) << std::endl;
92 1 : std::cout << "m2 = " << data::pp(m2) << std::endl;
93 1 : std::cout << "n1 = " << data::pp(n1) << std::endl;
94 1 : std::cout << "n2 = " << data::pp(n2) << std::endl;
95 1 : std::cout << "p1 = " << data::pp(p1) << std::endl;
96 1 : std::cout << "p2 = " << data::pp(p2) << std::endl;
97 1 : BOOST_CHECK(p1 == p2);
98 1 : }
99 :
100 1 : void test_pp()
101 : {
102 2 : data_expression d1 = nat("d1");
103 2 : data_expression d2 = nat("d2");
104 4 : process::action_list a1 ( { act("a", data_expression_list({ d1 })) });
105 4 : process::action_list a2 ( { act("a", data_expression_list({ d2 })) });
106 4 : process::action_list b1 ( { act("b", data_expression_list({ d1 })) });
107 7 : process::action_list a11 ( { act("a", data_expression_list({ d1 })), act("a", data_expression_list({ d1 })) });
108 1 : multi_action m(a11);
109 1 : std::string s = lps::pp(m);
110 1 : std::cout << "s = " << s << std::endl;
111 1 : BOOST_CHECK(s == "a(d1)|a(d1)");
112 1 : }
113 :
114 2 : BOOST_AUTO_TEST_CASE(test_main)
115 : {
116 1 : test_equal_multi_actions();
117 1 : test_pp();
118 1 : }
|
