Include file:
#include "mcrl2/lps/untime.h
mcrl2::lps::
untime_algorithm
¶
action_summand_type
¶typedef for process_type::action_summand_type
process_type
¶typedef for Specification::process_type
super
¶typedef for detail::lps_algorithm< Specification >
m_add_invariants
¶
m_apply_fm
¶
m_identifier_generator
¶Identifier generator, for generating fresh identifiers.
m_time_invariant
¶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.
calculate_time_invariant
()¶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.
untime
(action_summand_type &s)¶Apply untime to an action summand.