Include file:
#include "mcrl2/lps/untime.h
mcrl2::lps::
untime_algorithm
¶mcrl2::lps::untime_algorithm::
action_summand_type
¶typedef for process_type::action_summand_type
mcrl2::lps::untime_algorithm::
process_type
¶typedef for Specification::process_type
mcrl2::lps::untime_algorithm::
super
¶typedef for detail::lps_algorithm< Specification >
mcrl2::lps::untime_algorithm::
m_add_invariants
¶mcrl2::lps::untime_algorithm::
m_apply_fm
¶mcrl2::lps::untime_algorithm::
m_identifier_generator
¶Identifier generator, for generating fresh identifiers.
mcrl2::lps::untime_algorithm::
m_last_action_time
¶Variable denoting the time at which the last action occurred.
mcrl2::lps::untime_algorithm::
m_rewriter
¶mcrl2::lps::untime_algorithm::
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.