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 monotonicity_test.cpp
10 : /// \brief Tests for the is_monotonous function for state formulas.
11 :
12 : #define BOOST_TEST_MODULE modal_formula_monotonicity_test
13 : #include <boost/test/included/unit_test.hpp>
14 :
15 : #include "mcrl2/lps/detail/test_input.h"
16 : #include "mcrl2/lps/linearise.h"
17 : #include "mcrl2/modal_formula/parse.h"
18 :
19 : using namespace mcrl2;
20 : using namespace mcrl2::lps;
21 : using namespace mcrl2::state_formulas;
22 :
23 30 : void run_monotonicity_test_case(const std::string& formula, const specification& lpsspec, const bool expect_success = true)
24 : {
25 30 : specification lpscopy(lpsspec);
26 :
27 30 : parse_state_formula_options options;
28 30 : options.check_monotonicity = false;
29 30 : options.resolve_name_clashes = false;
30 30 : state_formula f = parse_state_formula(formula, lpscopy, false, options);
31 30 : if (state_formulas::has_state_variable_name_clashes(f))
32 : {
33 6 : std::cerr << "Error: " << state_formulas::pp(f) << " has name clashes" << std::endl;
34 6 : f = state_formulas::resolve_state_variable_name_clashes(f);
35 6 : std::cerr << "resolved to " << state_formulas::pp(f) << std::endl;
36 : }
37 30 : BOOST_TEST(is_monotonous(f) == expect_success);
38 30 : }
39 :
40 2 : BOOST_AUTO_TEST_CASE(test_abp)
41 : {
42 1 : std::string lpstext = lps::detail::ABP_SPECIFICATION();
43 1 : specification lpsspec = remove_stochastic_operators(linearise(lpstext));
44 :
45 1 : run_monotonicity_test_case("true", lpsspec, true);
46 1 : run_monotonicity_test_case("[true*]<true*>true", lpsspec, true);
47 1 : run_monotonicity_test_case("mu X. !!X", lpsspec, true);
48 1 : run_monotonicity_test_case("nu X. ([true]X && <true>true)", lpsspec, true);
49 1 : run_monotonicity_test_case("nu X. ([true]X && forall d:D. [r1(d)] mu Y. (<true>Y || <s4(d)>true))", lpsspec, true);
50 1 : run_monotonicity_test_case("forall d:D. nu X. (([!r1(d)]X && [s4(d)]false))", lpsspec, true);
51 1 : run_monotonicity_test_case("nu X. ([true]X && forall d:D. [r1(d)]nu Y. ([!r1(d) && !s4(d)]Y && [r1(d)]false))", lpsspec, true);
52 1 : run_monotonicity_test_case("mu X. !X", lpsspec, false);
53 1 : run_monotonicity_test_case("mu X. nu Y. (X => Y)", lpsspec, false);
54 1 : run_monotonicity_test_case("mu X. X || mu X. X", lpsspec, true);
55 1 : run_monotonicity_test_case("mu X. (X || mu X. X)", lpsspec, true);
56 1 : run_monotonicity_test_case("mu X. (X || mu Y. Y)", lpsspec, true);
57 1 : run_monotonicity_test_case("!(mu X. X || mu X. X)", lpsspec, true);
58 1 : run_monotonicity_test_case("!(mu X. (X || mu X. X))", lpsspec, true);
59 1 : run_monotonicity_test_case("!(mu X. (X || mu Y. Y))", lpsspec, true);
60 1 : }
61 :
62 : // Test case provided by Jeroen Keiren, 10-9-2010
63 2 : BOOST_AUTO_TEST_CASE(test_elevator)
64 : {
65 : std::string lpstext =
66 :
67 : "% Model of an elevator for n floors. \n"
68 : "% Originally described in 'Solving Parity Games in Practice' by Oliver \n"
69 : "% Friedmann and Martin Lange. \n"
70 : "% \n"
71 : "% This is the version with a first in first out policy \n"
72 : " \n"
73 : "sort Floor = Pos; \n"
74 : " DoorStatus = struct open | closed; \n"
75 : " Requests = List(Floor); \n"
76 : " \n"
77 : "map maxFloor: Floor; \n"
78 : "eqn maxFloor = 3; \n"
79 : " \n"
80 : "map addRequest : Requests # Floor -> Requests; \n"
81 : " \n"
82 : "var r: Requests; \n"
83 : " f,g: Floor; \n"
84 : " % FIFO behaviour! \n"
85 : "eqn addRequest([], f) = [f]; \n"
86 : " (f == g) -> addRequest(g |> r, f) = g |> r; \n"
87 : " (f != g) -> addRequest(g |> r, f) = g |> addRequest(r, f); \n"
88 : " \n"
89 : "map removeRequest : Requests -> Requests; \n"
90 : "var r: Requests; \n"
91 : " f: Floor; \n"
92 : "eqn removeRequest(f |> r) = r; \n"
93 : " \n"
94 : "map getNext : Requests -> Floor; \n"
95 : "var r: Requests; \n"
96 : " f: Floor; \n"
97 : "eqn getNext(f |> r) = f; \n"
98 : " \n"
99 : "act isAt: Floor; \n"
100 : " request: Floor; \n"
101 : " close, open, up, down; \n"
102 : " \n"
103 : "proc Elevator(at: Floor, status: DoorStatus, reqs: Requests, moving: Bool) = \n"
104 : " isAt(at) . Elevator() \n"
105 : " + sum f: Floor. (f <= maxFloor) -> request(f) . Elevator(reqs = addRequest(reqs, f)) \n"
106 : " + (status == open) -> close . Elevator(status = closed) \n"
107 : " + (status == closed && reqs != [] && getNext(reqs) > at) -> up . Elevator(at = at + 1, moving = true) \n"
108 : " + (status == closed && reqs != [] && getNext(reqs) < at) -> down . Elevator(at = Int2Pos(at - 1), moving = true) \n"
109 : " + (status == closed && getNext(reqs) == at) -> open. Elevator(status = open, reqs = removeRequest(reqs), moving = false); \n"
110 : " \n"
111 1 : "init Elevator(1, open, [], false); \n"
112 : ;
113 1 : specification lpsspec = remove_stochastic_operators(linearise(lpstext));
114 :
115 1 : run_monotonicity_test_case("nu U. [true] U && ((mu V . nu W. !([!request(maxFloor)]!W && [request(maxFloor)]!V)) || (nu X . mu Y. [!isAt(maxFloor)] Y && [isAt(maxFloor)]X))", lpsspec, true);
116 1 : run_monotonicity_test_case("nu U. [true] U && ((nu V . mu W. ([!request(maxFloor)]W && [request(maxFloor)]V)) => (nu X . mu Y. [!isAt(maxFloor)] Y && [isAt(maxFloor)]X))", lpsspec, true);
117 1 : run_monotonicity_test_case("nu U. [true] U && (!(nu V . mu W. ([!request(maxFloor)]W && [request(maxFloor)]V)) || (nu X . mu Y. [!isAt(maxFloor)] Y && [isAt(maxFloor)]X))", lpsspec, true);
118 1 : run_monotonicity_test_case("(nu X . mu Y. X) => true", lpsspec, true);
119 1 : run_monotonicity_test_case("!(nu X . mu Y. X)", lpsspec, true);
120 1 : run_monotonicity_test_case("mu X . X", lpsspec, true);
121 1 : run_monotonicity_test_case("nu X . X", lpsspec, true);
122 1 : run_monotonicity_test_case("mu X . !X", lpsspec, false);
123 1 : run_monotonicity_test_case("nu X . !X", lpsspec, false);
124 1 : run_monotonicity_test_case("!(mu X . X)", lpsspec, true);
125 1 : run_monotonicity_test_case("!(nu X . X)", lpsspec, true);
126 1 : run_monotonicity_test_case("(mu X . X) => true", lpsspec, true);
127 1 : run_monotonicity_test_case("(nu X . X) => true", lpsspec, true);
128 1 : run_monotonicity_test_case("!(mu X. (mu X. X))", lpsspec, true);
129 : // trac ticket #1320
130 1 : run_monotonicity_test_case("!mu X. [true]X && mu X. [true]X", lpsspec, true);
131 1 : }
|