mcrl2::lps::untime_algorithm

Include file:

#include "mcrl2/lps/untime.h

class mcrl2::lps::untime_algorithm

Protected types

type mcrl2::lps::untime_algorithm::action_summand_type

typedef for process_type::action_summand_type

type mcrl2::lps::untime_algorithm::process_type

typedef for Specification::process_type

type mcrl2::lps::untime_algorithm::super

typedef for detail::lps_algorithm< Specification >

Protected attributes

bool mcrl2::lps::untime_algorithm::m_add_invariants

bool mcrl2::lps::untime_algorithm::m_apply_fm

data::set_identifier_generator mcrl2::lps::untime_algorithm::m_identifier_generator

Identifier generator, for generating fresh identifiers.

data::variable mcrl2::lps::untime_algorithm::m_last_action_time

Variable denoting the time at which the last action occurred.

const data::rewriter &mcrl2::lps::untime_algorithm::m_rewriter

data::data_expression 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.

Protected member functions

data::data_expression 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.

void untime(action_summand_type &s)

Apply untime to an action summand.

Public member functions

void run()

untime_algorithm(Specification &spec, bool add_invariants, bool apply_fourier_motzkin, const data::rewriter &r)