mCRL2
|
#include <untime.h>
Public Member Functions | |
untime_algorithm (Specification &spec, bool add_invariants, bool apply_fourier_motzkin, const data::rewriter &r) | |
void | run () |
![]() | |
lps_algorithm (Specification &spec) | |
Constructor. | |
bool | verbose () const |
Flag for verbose output. | |
data::data_expression | next_state (const action_summand &s, const data::variable &v) const |
Applies the next state substitution to the variable v. | |
void | instantiate_free_variables () |
Attempts to eliminate the free variables of the specification, by substituting a constant value for them. If no constant value is found for one of the variables, an exception is thrown. | |
void | remove_parameters (const std::set< data::variable > &to_be_removed) |
Removes formal parameters from the specification. | |
void | remove_singleton_sorts () |
Removes parameters with a singleton sort. | |
void | remove_trivial_summands () |
Removes summands with condition equal to false. | |
void | remove_unused_summand_variables () |
Removes unused summand variables. | |
Protected Types | |
typedef detail::lps_algorithm< Specification > | super |
typedef Specification::process_type | process_type |
typedef process_type::action_summand_type | action_summand_type |
Protected Member Functions | |
data::data_expression | calculate_time_invariant () |
Data expression expressing the invariant for variables relating to time. | |
void | untime (action_summand_type &s) |
Apply untime to an action summand. | |
![]() | |
void | sumelm_find_variables (const action_summand &s, std::set< data::variable > &result) const |
void | sumelm_find_variables (const deadlock_summand &s, std::set< data::variable > &result) const |
void | summand_remove_unused_summand_variables (SummandType &summand_) |
Protected Attributes | |
bool | m_add_invariants |
bool | m_apply_fm |
const data::rewriter & | m_rewriter |
data::variable | m_last_action_time |
Variable denoting the time at which the last action occurred. | |
data::data_expression | m_time_invariant |
Data expression expressing the invariant for variables relating to time. | |
data::set_identifier_generator | m_identifier_generator |
Identifier generator, for generating fresh identifiers. | |
![]() | |
Specification & | m_spec |
The specification that is processed by the algorithm. | |
|
protected |
|
protected |
|
protected |
|
inline |
|
inlineprotected |
Data expression expressing the invariant for variables relating to time.
For all parameters x relating to time, the expression 0<=x && x<=m_last_action_time is returned, provided that in the initial vector the variable x gets the value 0, and in each summand the new value for x is either x, or the value that is assigned to last action time, which is the time tag of the action in that summand.
|
inline |
|
inlineprotected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
Data expression expressing the invariant for variables relating to time.
For all parameters x relating to time, the expression 0<=x && x<=m_last_action_time, provided that in the initial vector the variable x gets the value 0, and in each summand the new value for x is either x, or the value that is assigned to last action time, which is the time tag of the action in that summand.