Line data Source code
1 : // Author(s): Jeroen Keiren
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 untime.h
10 : /// \brief Removes time from a linear process.
11 :
12 : #ifndef MCRL2_LPS_UNTIME_H
13 : #define MCRL2_LPS_UNTIME_H
14 :
15 : #include "mcrl2/data/fourier_motzkin.h"
16 : #include "mcrl2/lps/detail/lps_algorithm.h"
17 :
18 : namespace mcrl2
19 : {
20 :
21 : namespace lps
22 : {
23 :
24 : namespace detail
25 : {
26 :
27 : template <class INITIALIZER>
28 : INITIALIZER make_process_initializer(const data::data_expression_list& expressions, const INITIALIZER& init);
29 :
30 : template <>
31 3 : process_initializer make_process_initializer(const data::data_expression_list& expressions, const process_initializer& /* init */)
32 : {
33 3 : return lps::process_initializer(expressions);
34 : }
35 :
36 : template <>
37 0 : stochastic_process_initializer make_process_initializer(const data::data_expression_list& expressions, const stochastic_process_initializer& init)
38 : {
39 0 : return stochastic_process_initializer(expressions, init.distribution());
40 : }
41 :
42 : } // namespace detail
43 :
44 : template <typename Specification>
45 : class untime_algorithm: public detail::lps_algorithm<Specification>
46 : {
47 : protected:
48 : typedef typename detail::lps_algorithm<Specification> super;
49 : typedef typename Specification::process_type process_type;
50 : typedef typename process_type::action_summand_type action_summand_type;
51 : using super::m_spec;
52 :
53 : bool m_add_invariants;
54 : bool m_apply_fm;
55 : const data::rewriter& m_rewriter;
56 :
57 : protected:
58 : /// \brief Variable denoting the time at which the last action occurred
59 : data::variable m_last_action_time;
60 :
61 : /// \brief Data expression expressing the invariant for variables relating to time
62 : /// \details For all parameters x relating to time, the expression 0<=x && x<=m_last_action_time,
63 : /// provided that in the initial vector the variable x gets the value 0, and in each summand the
64 : /// new value for x is either x, or the value that is assigned to last action time, which is the time
65 : /// tag of the action in that summand.
66 : data::data_expression m_time_invariant;
67 :
68 : /// \brief Identifier generator, for generating fresh identifiers.
69 : data::set_identifier_generator m_identifier_generator;
70 :
71 : /// \brief Data expression expressing the invariant for variables relating to time
72 : ///\details For all parameters x relating to time, the expression 0<=x && x<=m_last_action_time is returned,
73 : /// provided that in the initial vector the variable x gets the value 0, and in each summand the
74 : /// new value for x is either x, or the value that is assigned to last action time, which is the time
75 : /// tag of the action in that summand.
76 3 : data::data_expression calculate_time_invariant()
77 : {
78 3 : const data::data_expression real_zero= data::sort_real::real_(0);
79 :
80 : // The vector below contains exactly one boolean for each parameter. As long as the value
81 : // for the elements in the vector is true, it is a candidate time variable.
82 3 : std::vector <bool> time_variable_candidates(m_spec.process().process_parameters().size(),true);
83 3 : std::vector <bool>::iterator j=time_variable_candidates.begin() ;
84 3 : mCRL2log(log::verbose) << "For untiming to function optimally, it is assumed that the input lps is rewritten to normal form" << std::endl;
85 :
86 3 : const data::data_expression_list& process_parameters = m_spec.initial_process().expressions();
87 6 : for (data::data_expression_list::const_iterator k = process_parameters.begin(); k != process_parameters.end(); ++j, ++k)
88 : {
89 3 : if (*k != real_zero)
90 : {
91 3 : (*j) = false;
92 : }
93 : }
94 :
95 3 : assert(j == time_variable_candidates.end());
96 :
97 3 : auto const& summands = m_spec.process().action_summands();
98 11 : for (auto i = summands.begin(); i != summands.end(); ++i)
99 : {
100 8 : const data::data_expression_list summand_arguments = i->next_state(m_spec.process().process_parameters());
101 8 : std::vector <bool>::iterator j = time_variable_candidates.begin();
102 8 : data::variable_list::const_iterator l=m_spec.process().process_parameters().begin();
103 16 : for (data::data_expression_list::const_iterator k=summand_arguments.begin() ;
104 24 : k!=summand_arguments.end(); ++j, ++k, l++)
105 : {
106 8 : if ((*k!=real_zero)&&(*k!=*l)&&(*k!=i->multi_action().time()))
107 : {
108 8 : (*j)=false;
109 : }
110 : }
111 8 : assert(j==time_variable_candidates.end());
112 : }
113 :
114 3 : data::data_expression time_invariant(data::sort_bool::true_());
115 3 : j=time_variable_candidates.begin();
116 3 : for (data::variable_list::const_iterator k=m_spec.process().process_parameters().begin();
117 6 : k!=m_spec.process().process_parameters().end() ; ++j, ++k)
118 : {
119 3 : if (*j)
120 : {
121 0 : data::variable kvar(*k);
122 0 : data::variable lat(m_last_action_time);
123 0 : time_invariant=data::lazy::and_(time_invariant,
124 : data::lazy::and_(data::less_equal(real_zero,kvar),
125 : data::less_equal(kvar,lat)));
126 0 : }
127 : }
128 3 : assert(j==time_variable_candidates.end());
129 3 : mCRL2log(log::verbose) << "Time invariant " << data::pp(time_invariant) << std::endl;
130 6 : return time_invariant;
131 3 : }
132 :
133 : /// \brief Apply untime to an action summand.
134 8 : void untime(action_summand_type& s)
135 : {
136 : using namespace mcrl2::data;
137 8 : if (s.has_time())
138 : {
139 : // Extend the original condition with an additional argument t.i(d,e.i)>m_last_action_time && t.i(d,e.i) > 0
140 18 : s.condition() = lazy::and_(s.condition(),
141 6 : lazy::and_(greater(s.multi_action().time(),m_last_action_time),
142 6 : greater(s.multi_action().time(), sort_real::real_(0))));
143 :
144 : // Extend original assignments to include m_last_action_time := t.i(d,e.i)
145 6 : s.assignments()=push_back(s.assignments(),assignment(m_last_action_time,s.multi_action().time()));
146 :
147 : // Remove time
148 6 : s.multi_action() = multi_action(s.multi_action().actions());
149 :
150 : // Try to apply Fourier-Motzkin elimination to simplify
151 6 : std::set< variable > variables_in_action = process::find_all_variables(s.multi_action());
152 6 : std::set< variable > variables_in_assignments = process::find_all_variables(s.assignments());
153 : // Split the variables that do/do not occur in actions and assignments.
154 6 : variable_list do_occur, do_not_occur;
155 :
156 12 : for(const variable& v: s.summation_variables())
157 : {
158 0 : if (variables_in_action.count(v)>0 || variables_in_assignments.count(v)>0)
159 : {
160 0 : do_occur.push_front(v);
161 : }
162 : else
163 : {
164 0 : do_not_occur.push_front(v);
165 : }
166 : }
167 :
168 : // Only apply Fourier Motzkin elimination to the new condition if the user
169 : // explicitly asked for it.
170 : // The application of Fourier Motzkin can change the structure of the
171 : // condition significantly. Therefore, its application hides the real
172 : // outcome of the untime algorithm.
173 6 : if(m_apply_fm)
174 : {
175 : try
176 : {
177 0 : variable_list remaining_variables;
178 0 : data_expression new_condition;
179 0 : fourier_motzkin(s.condition(), do_not_occur, new_condition, remaining_variables, m_rewriter);
180 0 : s.condition() = new_condition;
181 0 : s.summation_variables() = do_occur + remaining_variables;
182 0 : }
183 0 : catch(mcrl2::runtime_error& e)
184 : {
185 : // The application of Fourier Motzkin failed because of mixed Real and
186 : // non-Real variables. We leave the original condition, but show a
187 : // warning to the user
188 0 : mCRL2log(log::debug) << "Application of Fourier Motzkin failed with the message\n" << e.what() << std::endl;
189 : }
190 : }
191 6 : }
192 : else
193 : {
194 : // Add a new summation variable (this is allowed because according to an axiom the following equality holds):
195 : // c -> a . X == sum t:Real . c -> a@t . X
196 4 : variable time_var(m_identifier_generator("time_var"), sort_real::real_());
197 2 : s.summation_variables().push_front(time_var);
198 :
199 : // Extend the original condition with an additional argument time_var > m_last_action_time && time_var > 0
200 2 : s.condition() = lazy::and_(s.condition(),
201 : lazy::and_(greater(time_var, m_last_action_time),
202 : greater(time_var, sort_real::real_(0))));
203 :
204 : // Extend original assignments to include m_last_action_time := time_var
205 2 : s.assignments()=push_back(s.assignments(),assignment(m_last_action_time, time_var));
206 2 : } // s.has_time()
207 :
208 : // Add the condition m_last_action_time>=0, which holds, and which is generally a useful fact for further processing.
209 8 : s.condition() = lazy::and_(s.condition(),m_time_invariant);
210 8 : }
211 :
212 :
213 :
214 :
215 : public:
216 4 : untime_algorithm(Specification& spec, bool add_invariants, bool apply_fourier_motzkin, const data::rewriter& r)
217 : : detail::lps_algorithm<Specification>(spec),
218 4 : m_add_invariants(add_invariants),
219 4 : m_apply_fm(apply_fourier_motzkin),
220 4 : m_rewriter(r)
221 : {
222 4 : m_identifier_generator.add_identifiers(lps::find_identifiers(spec));
223 4 : m_identifier_generator.add_identifiers(data::function_and_mapping_identifiers(spec.data()));
224 4 : }
225 :
226 4 : void run()
227 : {
228 4 : m_spec.process().deadlock_summands() = deadlock_summand_vector();
229 8 : m_spec.process().deadlock_summands().push_back(
230 8 : deadlock_summand(data::variable_list(), data::sort_bool::true_(), deadlock()));
231 :
232 4 : if (m_spec.process().has_time())
233 : {
234 3 : mCRL2log(log::verbose) << "Untiming " << m_spec.process().summand_count() << " summands" << std::endl;
235 :
236 : // Create extra parameter m_last_action_time and add it to the list of process parameters,
237 : // m_last_action_time is used later on in the code
238 3 : m_last_action_time = data::variable(m_identifier_generator("last_action_time"), data::sort_real::real_());
239 3 : mCRL2log(log::verbose) << "Introduced variable " << data::pp(m_last_action_time) << " to denote time of last action" << std::endl;
240 :
241 : // Should happen before updating the process
242 3 : m_time_invariant = m_add_invariants ? calculate_time_invariant() : (data::data_expression) data::sort_bool::true_();
243 :
244 3 : m_spec.process().process_parameters()=push_back(m_spec.process().process_parameters(),m_last_action_time);
245 3 : data::data_expression_list init = m_spec.initial_process().expressions();
246 3 : init = push_back(init, data::sort_real::real_(0));
247 3 : m_spec.initial_process() = detail::make_process_initializer(init, m_spec.initial_process());
248 :
249 11 : for(action_summand_type& s: m_spec.process().action_summands())
250 : {
251 8 : untime(s);
252 : }
253 3 : }
254 4 : }
255 : };
256 :
257 : } // namespace lps
258 :
259 : } // namespace mcrl2
260 :
261 : #endif // MCRL2_LPS_UNTIME_H
|
