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 mcrl2/modal_formula/is_monotonous.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_MODAL_FORMULA_IS_MONOTONOUS_H
13 : #define MCRL2_MODAL_FORMULA_IS_MONOTONOUS_H
14 :
15 : #include "mcrl2/core/detail/print_utility.h"
16 : #include "mcrl2/modal_formula/state_formula.h"
17 :
18 : namespace mcrl2
19 : {
20 :
21 : namespace state_formulas
22 : {
23 :
24 : /// \brief Returns true if the state formula is monotonous.
25 : /// \param f A modal formula.
26 : /// \param non_negated_variables Names of state variables that occur positively in the current scope.
27 : /// \param negated_variables Names of state variables that occur negatively in the current scope.
28 : /// \return True if the state formula is monotonous.
29 : inline
30 1735 : bool is_monotonous(const state_formula& f,
31 : const std::set<core::identifier_string>& non_negated_variables,
32 : const std::set<core::identifier_string>& negated_variables)
33 : {
34 : using utilities::detail::contains;
35 :
36 1735 : if (is_not(f))
37 : {
38 108 : return is_monotonous(atermpp::down_cast<not_>(f).operand(), negated_variables, non_negated_variables);
39 : }
40 1627 : else if (is_minus(f))
41 : {
42 0 : return is_monotonous(atermpp::down_cast<minus>(f).operand(), negated_variables, non_negated_variables);
43 : }
44 1627 : else if (data::is_data_expression(f))
45 : {
46 36 : return true;
47 : }
48 1591 : else if (is_true(f))
49 : {
50 182 : return true;
51 : }
52 1409 : else if (is_false(f))
53 : {
54 81 : return true;
55 : }
56 1328 : else if (is_and(f))
57 : {
58 152 : const and_& g = atermpp::down_cast<and_>(f);
59 304 : return is_monotonous(g.left(), non_negated_variables, negated_variables) &&
60 304 : is_monotonous(g.right(), non_negated_variables, negated_variables);
61 : }
62 1176 : else if (is_or(f))
63 : {
64 81 : const or_& g = atermpp::down_cast<or_>(f);
65 162 : return is_monotonous(g.left(), non_negated_variables, negated_variables) &&
66 162 : is_monotonous(g.right(), non_negated_variables, negated_variables);
67 : }
68 1095 : else if (is_imp(f))
69 : {
70 37 : const imp& g = atermpp::down_cast<imp>(f);
71 73 : return is_monotonous(g.left(), negated_variables, non_negated_variables) &&
72 73 : is_monotonous(g.right(), non_negated_variables, negated_variables);
73 : }
74 1058 : else if (is_plus(f))
75 : {
76 0 : const plus& g = atermpp::down_cast<plus>(f);
77 0 : return is_monotonous(g.left(), non_negated_variables, negated_variables) &&
78 0 : is_monotonous(g.right(), non_negated_variables, negated_variables);
79 : }
80 1058 : else if (is_const_multiply(f))
81 : {
82 1 : const const_multiply& g = atermpp::down_cast<const_multiply>(f);
83 1 : return is_monotonous(g.right(), non_negated_variables, negated_variables);
84 : }
85 1057 : else if (is_const_multiply_alt(f))
86 : {
87 1 : const const_multiply_alt& g = atermpp::down_cast<const_multiply_alt>(f);
88 1 : return is_monotonous(g.left(), non_negated_variables, negated_variables);
89 : }
90 1056 : else if (is_forall(f))
91 : {
92 24 : const forall& g = atermpp::down_cast<forall>(f);
93 24 : return is_monotonous(g.body(), non_negated_variables, negated_variables);
94 : }
95 1032 : else if (is_exists(f))
96 : {
97 12 : const exists& g = atermpp::down_cast<exists>(f);
98 12 : return is_monotonous(g.body(), non_negated_variables, negated_variables);
99 : }
100 1020 : else if (is_infimum(f))
101 : {
102 2 : const infimum& g = atermpp::down_cast<infimum>(f);
103 2 : return is_monotonous(g.body(), non_negated_variables, negated_variables);
104 : }
105 1018 : else if (is_supremum(f))
106 : {
107 1 : const supremum& g = atermpp::down_cast<supremum>(f);
108 1 : return is_monotonous(g.body(), non_negated_variables, negated_variables);
109 : }
110 1017 : else if (is_sum(f))
111 : {
112 1 : const sum& g = atermpp::down_cast<sum>(f);
113 1 : return is_monotonous(g.body(), non_negated_variables, negated_variables);
114 : }
115 1016 : else if (is_may(f))
116 : {
117 218 : const may& g = atermpp::down_cast<may>(f);
118 218 : return is_monotonous(g.operand(), non_negated_variables, negated_variables);
119 : }
120 798 : else if (is_must(f))
121 : {
122 237 : const must& g = atermpp::down_cast<must>(f);
123 237 : return is_monotonous(g.operand(), non_negated_variables, negated_variables);
124 : }
125 561 : else if (is_yaled_timed(f))
126 : {
127 3 : return true;
128 : }
129 558 : else if (is_yaled(f))
130 : {
131 0 : return true;
132 : }
133 558 : else if (is_delay_timed(f))
134 : {
135 3 : return true;
136 : }
137 555 : else if (is_delay(f))
138 : {
139 0 : return true;
140 : }
141 555 : else if (is_variable(f))
142 : {
143 261 : const variable& g = atermpp::down_cast<variable>(f);
144 261 : return !contains(negated_variables, g.name());
145 : }
146 294 : else if (is_mu(f))
147 : {
148 169 : const mu& g = atermpp::down_cast<mu>(f);
149 169 : std::set<core::identifier_string> non_neg = non_negated_variables;
150 169 : non_neg.insert(g.name());
151 169 : return is_monotonous(g.operand(), non_neg, negated_variables);
152 169 : }
153 125 : else if (is_nu(f))
154 : {
155 125 : const nu& g = atermpp::down_cast<nu>(f);
156 125 : std::set<core::identifier_string> non_neg = non_negated_variables;
157 125 : non_neg.insert(g.name());
158 125 : return is_monotonous(g.operand(), non_neg, negated_variables);
159 125 : }
160 :
161 0 : throw mcrl2::runtime_error(std::string("is_monotonous(state_formula) error: unknown argument ") + pp(f));
162 : return false;
163 : }
164 :
165 : /// \brief Returns true if the state formula is monotonous.
166 : /// \param f A modal formula
167 : /// \return True if the state formula is monotonous.
168 : inline
169 297 : bool is_monotonous(const state_formula& f)
170 : {
171 297 : std::set<core::identifier_string> non_negated_variables;
172 297 : std::set<core::identifier_string> negated_variables;
173 594 : return is_monotonous(f, non_negated_variables, negated_variables);
174 297 : }
175 :
176 : } // namespace state_formulas
177 :
178 : } // namespace mcrl2
179 :
180 : #endif // MCRL2_MODAL_FORMULA_IS_MONOTONOUS_H
|
