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 print_test.cpp
10 : /// \brief Test for parser + pretty printer
11 :
12 : #define BOOST_TEST_MODULE lps_print_test
13 : #include <boost/test/included/unit_test.hpp>
14 :
15 : #include "mcrl2/lps/linearise.h"
16 : #include "mcrl2/lps/parse.h"
17 :
18 : using namespace mcrl2;
19 : using namespace mcrl2::lps;
20 :
21 2 : BOOST_AUTO_TEST_CASE(rational)
22 : {
23 : std::string input(
24 : "% This is an mCRL2 process specification which can be used for testing\n"
25 : "% operations on rational numbers.\n"
26 : "\n"
27 : "% Tests for unary operations floor, ceil, round, succ, pred, -, abs, succ, pred\n"
28 : "act unary_operations : Real # Int # Int # Int # Real # Real # Real # Real;\n"
29 : "proc Test_unary_operations =\n"
30 : " sum x: Int, p: Pos, r: Real. (x >= -5 && x <= 5 && p <= 10 && r == x/p)\n"
31 : " -> unary_operations(r, floor(r), ceil(r), round(r), abs(r), -r, succ(r), pred(r))\n"
32 : " <> delta;\n"
33 : "\n"
34 : "% Tests for binary operations <, <=, >=, >, max, min, +, -, *, /\n"
35 : "act binary_operations: Real # Real # Bool # Bool # Bool # Bool # Real # Real # Real # Real # Real # Real;\n"
36 : " left_operand: Real;\n"
37 : "proc Test_binary_operations =\n"
38 : " sum x: Int, p: Pos, r: Real. (x >= -5 && x <= 5 && p <= 10 && r == x/p) ->\n"
39 : " left_operand(r) .\n"
40 : " (sum y: Int, q: Pos, s: Real. (y >= -5 && y <= 5 && q <= 10 && s == y/q)\n"
41 : " -> binary_operations(r, s, r < s, r <= s, r >= s, r > s, min(r, s), max(r, s), r + s, r - s, r * s, r / s)\n"
42 : " <> delta\n"
43 : " )\n"
44 : " <> delta;\n"
45 : "\n"
46 : "% Tests for exponentation\n"
47 : "act base: Real;\n"
48 : " exponent: Real # Int # Real;\n"
49 : "proc Test_exponentation =\n"
50 : " sum x: Int, p: Pos, r: Real. (x >= -5 && x <= 5 && p <= 10 && r == x/p)\n"
51 : " -> (base(r) . (sum y: Int. (y >= -5 && y <= 5) -> exponent(r, y, exp(r, y)) <> delta))\n"
52 : " <> delta;\n"
53 : "\n"
54 : "init Test_unary_operations + Test_binary_operations + Test_exponentation;\n"
55 1 : );
56 :
57 1 : specification s=remove_stochastic_operators(linearise(input));
58 :
59 1 : std::string output;
60 1 : output = lps::pp(s);
61 :
62 : // Check whether the symbol @ occurs in the pretty printed output. If this is
63 : // the case, still some internal symbol is exposed. As a result, our parsers
64 : // will not be able to handle the specification as input.
65 1 : BOOST_CHECK(output.find('@') == std::string::npos);
66 1 : }
67 :
68 2 : BOOST_AUTO_TEST_CASE(no_summands)
69 : {
70 1 : specification spec;
71 1 : std::string s = lps::pp(spec);
72 1 : std::cout << "--- no_summands ---\n" << s << std::endl;
73 1 : BOOST_CHECK(s.find("delta @ 0") != std::string::npos);
74 1 : }
75 :
76 : #ifdef MCRL2_PRINT_PROBLEM_CASES
77 : void test_specification(const std::string& spec_text)
78 : {
79 : specification x = parse_linear_process_specification(spec_text);
80 :
81 : std::string s1 = lps::pp(x);
82 : std::string s2 = lps::print(x);
83 : if (s1 != s2)
84 : {
85 : std::clog << "--- testing spec ---" << std::endl;
86 : std::clog << "<pp> " << s1 << std::endl;
87 : std::clog << "<print>" << s2 << std::endl;
88 : BOOST_CHECK(s1 == s2);
89 : }
90 : }
91 :
92 : BOOST_AUTO_TEST_CASE(problem_cases)
93 : {
94 : std::string SPEC;
95 :
96 : SPEC =
97 : "act a: Bool; \n"
98 : "proc P = a(true) . P;\n"
99 : "init P; \n"
100 : ;
101 : test_specification(SPEC);
102 : }
103 : #endif
104 :
105 2 : BOOST_AUTO_TEST_CASE(ticket_1208)
106 : {
107 : std::string text =
108 : "act a:Nat; \n"
109 1 : "init a(n whr n=m, m=3 end); \n"
110 : ;
111 : try
112 : {
113 1 : specification x = parse_linear_process_specification(text);
114 0 : }
115 1 : catch (const mcrl2::runtime_error& e)
116 : {
117 2 : std::string s = e.what();
118 1 : BOOST_CHECK(s.find("n whr n=m, m=3 end") != std::string::npos);
119 1 : }
120 1 : }
121 :
122 2 : BOOST_AUTO_TEST_CASE(ticket_1267)
123 : {
124 : std::string text =
125 : "act a: Nat; \n"
126 : "proc loop(n: Nat) = a(n) . loop((n + 1) mod 10); \n"
127 1 : "init loop(0); \n"
128 : ;
129 1 : specification x = parse_linear_process_specification(text);
130 1 : auto const& a = x.process().action_summands().front().multi_action();
131 1 : std::string s = lps::pp(a);
132 1 : std::cout << "s = " << s << std::endl;
133 1 : BOOST_CHECK(s == "a(n)");
134 1 : }
135 :
|
