Line data Source code
1 : // Author(s): Gijs Kant
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/pbes/pbes_explorer.h
10 : /// \brief
11 : #ifndef MCRL2_PBES_PBES_EXPLORER_H
12 : #define MCRL2_PBES_PBES_EXPLORER_H
13 :
14 : #define PBES_EXPLORER_VERSION 1
15 :
16 : #include "mcrl2/pbes/detail/pbes_greybox_interface.h"
17 : #include "mcrl2/pbes/detail/ppg_rewriter.h"
18 : #include "mcrl2/pbes/detail/ppg_traverser.h"
19 :
20 : using mcrl2::data::data_expression;
21 : using mcrl2::data::variable;
22 :
23 : namespace mcrl2
24 : {
25 :
26 : namespace pbes_system
27 : {
28 :
29 : namespace detail
30 : {
31 : template <typename MapContainer>
32 : typename MapContainer::mapped_type map_at(const MapContainer& m, typename MapContainer::key_type key);
33 : } // namespace detail
34 :
35 :
36 :
37 : /// \brief
38 : class lts_type {
39 : int state_length;
40 : std::vector<std::string> state_names;
41 : std::vector<std::string> state_types;
42 : std::vector<std::string> state_type_list;
43 : std::map<std::string,int> state_type_index;
44 : std::vector<int> state_type_no;
45 : std::vector<std::string> state_label_names;
46 : std::vector<std::string> state_label_types;
47 : std::vector<std::string> edge_label_names;
48 : std::vector<std::string> edge_label_types;
49 :
50 : public:
51 : /// \brief Contructor.
52 : /// \param state_length
53 : lts_type(int state_length);
54 :
55 : /// \brief Destructor.
56 : ~lts_type();
57 :
58 : /// \brief Returns the state length.
59 : int get_state_length() const;
60 :
61 : /// \brief Returns the number of state types.
62 : std::size_t get_number_of_state_types() const;
63 :
64 : /// \brief Returns the sequence of state part names.
65 : const std::vector<std::string>& get_state_names() const;
66 :
67 : /// \brief Returns the sequence of state part types.
68 : const std::vector<std::string>& get_state_types() const;
69 :
70 : /// \brief Returns the state type index for the state part <tt>part</tt>.
71 : /// \param part the state part number.
72 : int get_state_type_no(int part) const;
73 :
74 : /// \brief Returns the name of the state type with number <tt>type_no</tt>.
75 : /// \param type_no the state type number.
76 : std::string get_state_type_name(int type_no) const;
77 :
78 : /// \brief Returns the number of state labels.
79 : std::size_t get_number_of_state_labels() const;
80 :
81 : /// \brief Returns the sequence of state labels.
82 : const std::vector<std::string>& get_state_labels() const;
83 :
84 : /// \brief Returns the sequence of state label types.
85 : const std::vector<std::string>& get_state_label_types() const;
86 :
87 : /// \brief Returns the number of edge labels.
88 : std::size_t get_number_of_edge_labels() const;
89 :
90 : /// \brief Returns the sequence of edge labels.
91 : const std::vector<std::string>& get_edge_labels() const;
92 :
93 : /// \brief Returns the sequence of edge label types.
94 : const std::vector<std::string>& get_edge_label_types() const;
95 :
96 : /// \brief Adds a state part of type <tt>type</tt> with name <tt>name</tt>.
97 : /// \param name the name of the state part.
98 : /// \param type the type of the state part.
99 : void add_state(const std::string& name, const std::string& type);
100 :
101 : /// \brief Adds a state label of type <tt>type</tt> with name <tt>name</tt>.
102 : /// \param name the name of the state label.
103 : /// \param type the type of the state label.
104 : void add_state_label(const std::string& name, const std::string& type);
105 :
106 : /// \brief Adds an edge label of type <tt>type</tt> with name <tt>name</tt>.
107 : /// \param name the name of the edge label.
108 : /// \param type the type of the edge label.
109 : void add_edge_label(const std::string& name, const std::string& type);
110 : };
111 :
112 :
113 :
114 :
115 : /// \brief
116 : class ltsmin_state {
117 :
118 : friend class lts_info;
119 : friend class explorer;
120 :
121 : public:
122 : typedef parity_game_generator::operation_type operation_type;
123 :
124 : private:
125 : int priority; // Priority (depends on fixpoint operator and equation order)
126 : std::string var; // Propositional variable name
127 : operation_type type; // player or type (And/Or, Abelard/Eloise, Odd/Even)
128 : std::vector<data_expression> param_values; // List of parameter values
129 :
130 : protected:
131 : /// \brief Constructor.
132 : /// \param varname the propositional variable of the state.
133 : /// \param e a propositional variable instantiation.
134 : ltsmin_state(const std::string& varname, const pbes_expression& e);
135 :
136 : /// \brief Returns the list of parameter values.
137 : const std::vector<data_expression>& get_parameter_values() const;
138 :
139 : /// \brief Adds a parameter value to the list of parameter values.
140 : void add_parameter_value(const data_expression&);
141 :
142 : /// \brief Returns a PBES expression representing the state.
143 : pbes_expression to_pbes_expression() const;
144 :
145 : public:
146 : /// \brief Constructor.
147 : /// \param varname the name of the propositional variable of the state.
148 : ltsmin_state(const std::string& varname);
149 :
150 : /// \brief Compares two PBES_State objects. Uses lexicographical ordering on priority, type, variable and parameter values.
151 : /// \param other an other PBES_State object.
152 : /// \return true if this.priority < other.priority || (this.priority==other.priority && (this.type < other.type ||
153 : /// (this.type==other.type && this.var < other.var || (this.var==other.var && this.param_values < other.param_values) ) ) ).
154 : bool operator<( const ltsmin_state& other ) const;
155 :
156 : /// \brief Checks if two PBES_State objects are equal.
157 : /// \param other an other PBES_State object.
158 : /// \return true if this.priority==other.priority && this.type==other.type && this.var==other.var
159 : /// && param_values==param_values.
160 : bool operator==( const ltsmin_state& other ) const;
161 :
162 : /// \brief Returns the priority for the state, which depends on the fixpoint operator of
163 : /// the equation of the propositional variable of the state and on the equation order.
164 : //int get_priority() const;
165 :
166 : /// \brief Returns a string representation of the propositional variable of the state.
167 : std::string get_variable() const;
168 :
169 : /// \brief Returns the player or type of the state (And/Or, Abelard/Eloise, Odd/Even).
170 : //operation_type get_type() const;
171 :
172 : /// \brief Returns a string representation of the state.
173 : std::string state_to_string() const;
174 : };
175 :
176 :
177 :
178 :
179 : /// \brief
180 : class lts_info {
181 :
182 : friend class ltsmin_state;
183 : friend class explorer;
184 :
185 : public:
186 : /// \brief The variable sequence type
187 : typedef parity_game_generator::operation_type operation_type;
188 : private:
189 : pbes& p;
190 : detail::pbes_greybox_interface* pgg;
191 : bool reset_option;
192 : bool always_split_option;
193 : lts_type type;
194 : std::map<int,std::vector<bool> > read_matrix;
195 : std::map<int,std::vector<bool> > write_matrix;
196 : std::map<int,std::vector<bool> > matrix;
197 : std::map<std::string,int> param_index;
198 : std::vector<data_expression> param_default_values;
199 : int number_of_groups;
200 : std::vector<pbes_expression> transition_expression;
201 : std::vector<pbes_expression> transition_expression_plain;
202 : std::vector<std::string> transition_variable_name;
203 : std::vector<operation_type> transition_type;
204 : std::map<std::string, propositional_variable> variables;
205 : std::map<std::string, operation_type> variable_type;
206 : std::map<std::string, fixpoint_symbol> variable_symbol;
207 : std::map<std::string, int> variable_priority;
208 : std::map<std::string, pbes_expression> variable_expression;
209 : std::map<std::string, data::variable_list> variable_parameters;
210 : std::map<std::string, std::vector<std::string> > variable_parameter_signatures;
211 : std::map<std::string, std::vector<int> > variable_parameter_indices;
212 : std::map<std::string, std::map<int,int> > variable_parameter_index_positions;
213 :
214 : static std::map<variable,std::string> variable_signatures;
215 :
216 : /// \brief Counts the number of propositional variables in an expression.
217 : /// \returns the number of variable occurences or INT_MAX if a variable
218 : /// occurs within the scope of a quantifier.
219 : int count_variables(const pbes_expression& e);
220 :
221 : /// \brief Determines if the propositional variable instantiation is one that
222 : /// only copies parameters from the current state.
223 : bool is_pass_through_state(const propositional_variable_instantiation& propvar);
224 :
225 : /// \brief Splits the expression into parts (disjuncts or conjuncts) and recursively tries to
226 : /// substitute the propositional variables with the parts of the right hand side of the
227 : /// equation for the variable.
228 : /// \param e the expression
229 : /// \param current_priority the priority of the current equation for which the parts are computed
230 : /// \param current_type the operation type (AND/OR) of the current equation for which the parts are computed
231 : /// \param vars_stack used for detection of infinite recursion. Please, initialise to the empty set.
232 : std::vector<pbes_expression> split_expression_and_substitute_variables(const pbes_expression& e, int current_priority, operation_type current_type, std::set<std::string> vars_stack);
233 :
234 : /// \brief Computes LTS Type from PBES.
235 : void compute_lts_type();
236 :
237 : /// \brief Computes transition groups from PBES.
238 : void compute_transition_groups();
239 :
240 : /// \brief Computes dependency matrix from PBES.
241 : void compute_dependency_matrix();
242 :
243 : protected:
244 :
245 : /// \brief Returns the map from transition group number to the expression of the transition group.
246 : const std::vector<pbes_expression>& get_transition_expressions() const;
247 :
248 : /// \brief Returns the map from variable names to the variable object for the variable.
249 : const std::map<std::string, propositional_variable>& get_variables() const;
250 :
251 : /// \brief Returns the map from variable names to the fixpoint operator of the equation for the variable.
252 : const std::map<std::string, fixpoint_symbol>& get_variable_symbols() const;
253 :
254 : /// \brief Returns the map from variable names to the sequence of parameters for the variable.
255 : const std::map<std::string, data::variable_list>& get_variable_parameters() const;
256 :
257 : /// \brief Determines if the term phi contains a branch that directly results in
258 : /// <tt>true</tt> or <tt>false</tt> (not a variable).
259 : /// \param phi a PBES expression
260 : static bool tf(const pbes_expression& phi);
261 :
262 : /// \brief Computes the propositional variables used in an expression.
263 : /// \param expr
264 : static std::set<std::string> occ(const pbes_expression& expr);
265 :
266 : /// \brief Computes the free variables read in an expression.
267 : /// \param expr
268 : static std::set<std::string> free(const pbes_expression& expr);
269 :
270 : /// \brief Computes the free variables actually used, not only passed through, in an expression.
271 : /// \param expr
272 : std::set<std::string> used(const pbes_expression& expr);
273 :
274 : /// \brief Computes the free variables actually used, not only passed through, in an expression.
275 : /// \param expr
276 : /// \param L
277 : std::set<std::string> used(const pbes_expression& expr, const std::set<std::string>& L);
278 :
279 : /// \brief Computes the free variables which are copied/passed through (to a recursive variable) in an expression.
280 : /// \param expr
281 : std::set<std::string> copied(const pbes_expression& expr);
282 :
283 : /// \brief Computes the free variables which are copied/passed through (to a recursive variable) in an expression.
284 : /// \param expr
285 : /// \param L
286 : std::set<std::string> copied(const pbes_expression& expr, const std::set<std::string>& L);
287 :
288 : /// \brief Computes the set of parameters changed in the expression.
289 : /// \param phi
290 : std::set<std::string> changed(const pbes_expression& phi);
291 :
292 : /// \brief Computes the set of parameters changed in the expression.
293 : /// \param phi
294 : /// \param L
295 : std::set<std::string> changed(const pbes_expression& phi, const std::set<std::string>& L);
296 :
297 : /// \brief Computes the set of parameters reset in the expression.
298 : /// \param phi
299 : /// \param d
300 : std::set<std::string> reset(const pbes_expression& phi, const std::set<std::string>& d);
301 :
302 : /// \brief Converts a variable_sequence_type into a set of parameter signatures.
303 : /// \param params a sequence of variables.
304 : static std::set<std::string> get_param_set(const data::variable_list& params);
305 :
306 : /// \brief Converts a variable_sequence_type into a sequence of parameter signatures.
307 : /// \param params a sequence of variables.
308 : static std::vector<std::string> get_param_sequence(const data::variable_list& params);
309 :
310 : /// \brief Converts a variable_sequence_type into a sequence of indices of parameter signatures
311 : /// in the list of parameter signatures for the system.
312 : /// \param params a sequence of variables.
313 : std::vector<int> get_param_indices(const data::variable_list& params);
314 :
315 : /// \brief Converts a variable_sequence_type into a map from indices of parameter signatures
316 : /// (in the list of parameter signatures for the system) to the index of the type of the parameter
317 : /// (in the list of types for the system).
318 : /// \param params a sequence of variables.
319 : std::map<int,int> get_param_index_positions(const data::variable_list& params);
320 :
321 : /// \brief Returns a signature for parameter <tt>param</tt>.
322 : /// \param param a parameter.
323 : static inline std::string get_param_signature(const variable& param);
324 :
325 : /// \brief Returns a default value for the sort of a parameter signature.
326 : /// \param index the index of the parameter signature.
327 : /// \return a default value for the sort of the parameter.
328 : const data_expression& get_default_value(int index);
329 :
330 : /// \brief Constructor
331 : /// \param p
332 : /// \param pgg
333 : /// \param reset
334 : /// \param always_split
335 : lts_info(pbes& p, detail::pbes_greybox_interface* pgg, bool reset, bool always_split);
336 :
337 : public:
338 :
339 : /// \brief Returns if the reset option is set.
340 : bool get_reset_option() const;
341 :
342 : /// \brief Returns the number of transition groups.
343 : int get_number_of_groups() const;
344 :
345 : /// \brief Returns the map from transition group number to the variable name of the equation to which
346 : /// the transition group belongs.
347 : const std::vector<std::string>& get_transition_variable_names() const;
348 :
349 : /// \brief Returns the map from transition group number to the type of the right hand side of the
350 : /// equation to which the transition group belongs.
351 : const std::vector<operation_type>& get_transition_types() const;
352 :
353 : /// \brief Returns the map from variable names to the type of the right hand side of the equation for
354 : /// the variable.
355 : const std::map<std::string, operation_type>& get_variable_types() const;
356 :
357 : /// \brief Returns the map from variable names to the priority of the equation for the variable.
358 : const std::map<std::string, int>& get_variable_priorities() const;
359 :
360 : /// \brief Returns the map from variable names to the list of parameters signatures for the variable.
361 : const std::map<std::string, std::vector<std::string> >& get_variable_parameter_signatures() const;
362 :
363 : /// \brief Returns the map from variable names to the list of indices of the parameters signatures for the variable
364 : /// according the order in the list of parameter signatures for the system.
365 : const std::map<std::string, std::vector<int> >& get_variable_parameter_indices() const;
366 :
367 : /// \brief Returns the map from variable names to the map from indices of parameter signatures for the variable
368 : /// (according to the list of parameter signatures for the system) to the index of the type of the parameter
369 : /// (in the list of types for the system).
370 : const std::map<std::string, std::map<int,int> >& get_variable_parameter_index_positions() const;
371 :
372 : /// \brief Returns the LTS Type.
373 : const lts_type& get_lts_type() const;
374 :
375 : /// \brief Returns the dependency matrix.
376 : const std::map<int,std::vector<bool> >& get_dependency_matrix() const;
377 :
378 : /// \brief Returns the read dependency matrix.
379 : const std::map<int,std::vector<bool> >& get_read_matrix() const;
380 :
381 : /// \brief Returns the write dependency matrix.
382 : const std::map<int,std::vector<bool> >& get_write_matrix() const;
383 :
384 : /// \brief Returns the index for a parameter signature in the list of parameter signatures
385 : /// for the system.
386 : /// \param signature The parameter signature.
387 : int get_index(const std::string& signature);
388 :
389 : /// \brief Determines if <tt>group</tt> is read dependent on the propositional variable.
390 : /// Returns true, because the propositional variable is needed to determine if the group belongs
391 : /// to the variable.
392 : /// \param group the number of the transition group.
393 : /// \return true.
394 : bool is_read_dependent_propvar(int group);
395 :
396 : /// \brief Determines if <tt>group</tt> is read dependent on part <tt>part</tt> of the state vector.
397 : /// Returns true if the parameter represented by <tt>part</tt> is in the set of parameters of the
398 : /// state variable for the group or in the set of data variables used in the expression of for the group.
399 : /// \param group the number of the transition group.
400 : /// \param part the number of the state part.
401 : /// \return true if param_part in ( params(var(group)) union used(expr(group)) ).
402 : bool is_read_dependent_parameter(int group, int part);
403 :
404 : /// \brief Determines if <tt>group</tt> is write dependent on the propositional variable.
405 : /// Returns true if propositional variables other than the group variable occur in the group expression
406 : /// or the group expression may directly evaluate to <tt>true</tt> or <tt>false</tt>.
407 : /// \param group the number of the transition group.
408 : /// \return true if ( occ(expr(group)) - {var(group)} ) is not empty or tf(expr(group)).
409 : bool is_write_dependent_propvar(int group);
410 :
411 : /// \brief Determines if <tt>group</tt> is read dependent on part <tt>part</tt> of the state vector.
412 : /// Returns true if the parameter represented by <tt>part</tt> is in the set of data variables
413 : /// changed by the expression for the group.
414 : /// \param group the number of the transition group.
415 : /// \param part the number of the state part.
416 : /// \return true if param_part in changed(expr(group)).
417 : bool is_write_dependent_parameter(int group, int part);
418 :
419 : /// \brief Returns a string representation for state <tt>state</tt>.
420 : /// \param state
421 : std::string state_to_string(const ltsmin_state& state);
422 :
423 : /// \brief Returns a signature using name and type of a parameter.
424 : /// \param paramname the parameter name.
425 : /// \param paramtype the parameter type.
426 : static inline std::string get_param_signature(const std::string& paramname, const std::string& paramtype);
427 : };
428 :
429 :
430 :
431 :
432 : /// \brief
433 : class explorer {
434 :
435 : public:
436 : /// \brief The expression type of the equation.
437 : typedef parity_game_generator::operation_type operation_type;
438 :
439 : private:
440 : pbes p;
441 : lts_info* info;
442 : std::map<std::string,int> localmap_string2int;
443 : std::vector<std::string> localmap_int2string;
444 : std::vector<std::map<data_expression,int> > localmaps_data2int;
445 : std::vector<std::vector<data_expression> > localmaps_int2data;
446 :
447 : protected:
448 : /// \brief Returns a PBES_State object for <tt>expr</tt>.
449 : /// \param expr a propositional variable instantiation expression.
450 : ltsmin_state get_state(const propositional_variable_instantiation& expr) const;
451 :
452 : /// \brief Returns a string representation for the data expression <tt>e</tt>.
453 : /// \param e a PBES expression that may be in internal format.
454 : /// \return a string representation without internal rewriter quirks.
455 : std::string data_to_string(const data::data_expression& e);
456 :
457 : /// \brief Returns a data expression for the string representation <tt>s</tt>.
458 : /// \param s a string representation of a data expression.
459 : /// \return the data expression (possibly in internal format) that s represents.
460 : data::data_expression string_to_data(const std::string& s);
461 :
462 : /// \brief Returns the index of <tt>value</tt> in the local store for the data type
463 : /// with number <tt>type_no</tt>.
464 : /// The value is added to the store if it is not already present.
465 : /// \param type_no the number of the value type.
466 : /// \param value the data value.
467 : /// \return the index of <tt>value</tt> in local store <tt>type_no</tt>.
468 : int get_value_index(int type_no, const data_expression& value);
469 :
470 : /// \brief Returns the value at position <tt>index</tt> in the local store for the data type
471 : /// with number <tt>type_no</tt>.
472 : /// An exception is thrown if the index does not exist in the store.
473 : /// \param type_no the number of the value type.
474 : /// \param index an index.
475 : /// \return the value at position <tt>index</tt> in local store <tt>type_no</tt>.
476 : const data_expression& get_data_value(int type_no, int index);
477 :
478 : /// \brief the PBES greybox interface
479 : detail::pbes_greybox_interface* pgg;
480 :
481 : public:
482 : /// \brief Constructor.
483 : /// \param filename the name of a PBES file.
484 : /// \param rewrite_strategy the name of the data rewrite strategy to use.
485 : /// \param reset_flag if set, irrelevant parts of the state vector will be reset to a default value
486 : /// \param always_split_flag if set, equations will always be split into conjuncts or disjuncts to form transition groups,
487 : /// if not set (default) the explorer assumes the pbes to be generated with lps2pbes -p and splits accordingly.
488 : explorer(const std::string& filename, const std::string& rewrite_strategy, bool reset_flag, bool always_split_flag);
489 :
490 : /// \brief Constructor.
491 : /// \param p_ a PBES.
492 : /// \param rewrite_strategy String representing the rewrite strategy to use for the data rewriter.
493 : /// \param reset_flag if set, irrelevant parts of the state vector will be reset to a default value
494 : /// \param always_split_flag if set, equations will always be split into conjuncts or disjuncts to form transition groups,
495 : /// if not set (default) the explorer assumes the pbes to be generated with lps2pbes -p and splits accordingly.
496 : explorer(const pbes& p_, const std::string& rewrite_strategy, bool reset_flag, bool always_split_flag);
497 :
498 : /// \brief Destructor.
499 : ~explorer();
500 :
501 : /// \brief Returns the PBES_Info object.
502 : lts_info* get_info() const;
503 :
504 : /// \brief Returns the initial state.
505 : ltsmin_state get_initial_state() const;
506 :
507 : void initial_state(int* state);
508 :
509 : /// \brief Returns the state representing <tt>true</tt>.
510 : static inline ltsmin_state true_state();
511 :
512 : /// \brief Returns the state representing <tt>false</tt>.
513 : static inline ltsmin_state false_state();
514 :
515 : /// \brief Returns the index of <tt>value</tt> in the local store for the data type
516 : /// with number <tt>type_no</tt>. Type 0 is reserved for the string representations
517 : /// of variable names.
518 : /// The value is added to the store if it is not already present.
519 : /// \param type_no The number of the value type.
520 : /// \param s A string representation of the data value.
521 : /// \return The index of <tt>value</tt> in local store <tt>type_no</tt>.
522 : int get_index(int type_no, const std::string& s);
523 :
524 : /// \brief Returns the index of <tt>s</tt> in the local store for string values.
525 : /// This store is reserved for the string representations of variable names.
526 : /// The value is added to the store if it is not already present.
527 : /// \param s The string for which the index needs to be retrieved.
528 : /// \return the index of <tt>s</tt> in the local store for string values.
529 : int get_string_index(const std::string& s);
530 :
531 : /// \brief Transforms a PBES state to a state vector, represented by an array of integers.
532 : /// \param dst_state the new PBES state object
533 : /// \param dst the int array to which the state vector is written
534 : /// \param src_state the source PBES state object, used to check which fields have been changed.
535 : /// \param src an array which is used for default values, to prevent unused variables for being reset.
536 : /// the non-resetting behaviour can be turned off by the --reset option.
537 : void to_state_vector(const ltsmin_state& dst_state, int* dst, const ltsmin_state& src_state, int* const& src);
538 :
539 : /// \brief Returns the value at position <tt>index</tt> in the local store for the data type
540 : /// with number <tt>type_no</tt>. Type 0 is reserved for the string representations
541 : /// of variable names.
542 : /// An exception is thrown if the index does not exist in the store.
543 : /// \param type_no the number of the value type.
544 : /// \param index an index.
545 : /// \return a string representation of the value at position <tt>index</tt> in local store <tt>type_no</tt>.
546 : std::string get_value(int type_no, int index);
547 :
548 : /// \brief Returns the string at position <tt>index</tt> in the local store for string values.
549 : /// An exception is thrown if the index does not exist in the store.
550 : /// \param index an index.
551 : /// \return the string value at position <tt>index</tt> in the local store for string values.
552 : const std::string& get_string_value(int index);
553 :
554 : /// \brief Transforms a state vector <tt>src</tt> into a PBES_State object
555 : /// object containing the variable and parameter values that are represented
556 : /// by the indices in <tt>src</tt>.
557 : /// \param src an int array containg the indices of the state values.
558 : /// \return a PBES_State object containing the variable and parameter values that are represented
559 : /// by the indices in <tt>src</tt>.
560 : ltsmin_state from_state_vector(int* const& src);
561 :
562 : /// \brief Computes successor states for a state. Serves as a wrapper around the get_successors
563 : /// function of the pbes_greybox_interface.
564 : /// \param state the source state.
565 : /// \return a list of successor states.
566 : std::vector<ltsmin_state> get_successors(const ltsmin_state& state);
567 :
568 : /// \brief Iterates over the successors of a state and invokes a callback
569 : /// function for each successor state.
570 : /// \param src an int array containg the indices of the state values.
571 : /// \param cb a callback function that must provide the function operator() with the following interface:
572 : ///
573 : /// \code
574 : /// void operator()(int* const& next_state, int group);
575 : /// \endcode
576 : /// where
577 : /// - next_state is the target state of the transition
578 : /// - group is the number of the transition group, or -1 if it is unknown which group
579 : template <typename callback>
580 866 : void next_state_all(int* const& src, callback& cb)
581 : {
582 866 : int state_length = this->info->get_lts_type().get_state_length();
583 866 : ltsmin_state state = this->from_state_vector(src);
584 : //std::clog << "next_state_all: " << state->to_string() << std::endl;
585 866 : std::vector<ltsmin_state> successors = this->get_successors(state);
586 : // int dst[state_length]; N.B. This is not portable C++
587 866 : int* dst = MCRL2_SPECIFIC_STACK_ALLOCATOR(int, state_length);
588 2546 : for (auto & successor : successors) {
589 :
590 1680 : this->to_state_vector(successor, dst, state, src);
591 1680 : cb(dst);
592 : //std::clog << " succ: " << (*succ)->to_string() << std::endl;
593 : }
594 866 : }
595 :
596 : /// \brief Computes successor states for a state as defined in transition group <tt>group</tt>.
597 : /// Serves as a wrapper around the get_successors function of the pbes_greybox_interface.
598 : /// \param state the source state.
599 : /// \param group the group for which the successor states are computed.
600 : /// \return a list of successor states.
601 : std::vector<ltsmin_state> get_successors(const ltsmin_state& state, int group);
602 :
603 : /// \brief Iterates over the successors of a state for a certain transition group
604 : /// and invokes a callback function for each successor state.
605 : /// \param src an int array containg the indices of the state values.
606 : /// \param group the transition group
607 : /// \param cb a callback function that must provide the function operator() with the following interface:
608 : ///
609 : /// \code
610 : /// void operator()(int* const& next_state, int group);
611 : /// \endcode
612 : /// where
613 : /// - next_state is the target state of the transition
614 : /// - group is the number of the transition group, or -1 if it is unknown which group
615 : template <typename callback>
616 4302 : void next_state_long(int* const& src, int group, callback& cb)
617 : {
618 4302 : int state_length = this->info->get_lts_type().get_state_length();
619 4302 : std::string group_varname = info->get_transition_variable_names()[group];
620 4302 : std::string varname = this->get_string_value(src[0]);
621 4302 : if (varname==group_varname)
622 : {
623 866 : ltsmin_state state = this->from_state_vector(src);
624 866 : std::vector<ltsmin_state> successors = this->get_successors(state, group);
625 : // int dst[state_length]; N.B. This is not portable C++
626 866 : int* dst = MCRL2_SPECIFIC_STACK_ALLOCATOR(int, state_length);
627 2546 : for (auto & successor : successors) {
628 1680 : this->to_state_vector(successor, dst, state, src);
629 1680 : cb(dst, group);
630 : }
631 866 : }
632 4302 : }
633 :
634 : };
635 :
636 : } // namespace pbes_system
637 :
638 : } // namespace mcrl2
639 :
640 : #endif // MCRL2_PBES_PBES_EXPLORER_H
|
