mCRL2
Loading...
Searching...
No Matches
mcrl2::lps::untime_algorithm< Specification > Class Template Reference

#include <untime.h>

Inheritance diagram for mcrl2::lps::untime_algorithm< Specification >:
mcrl2::lps::detail::lps_algorithm< Specification >

Public Member Functions

 untime_algorithm (Specification &spec, bool add_invariants, bool apply_fourier_motzkin, const data::rewriter &r)
 
void run ()
 
- Public Member Functions inherited from mcrl2::lps::detail::lps_algorithm< Specification >
 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.
 
- Protected Member Functions inherited from mcrl2::lps::detail::lps_algorithm< Specification >
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::rewriterm_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.
 
- Protected Attributes inherited from mcrl2::lps::detail::lps_algorithm< Specification >
Specification & m_spec
 The specification that is processed by the algorithm.
 

Detailed Description

template<typename Specification>
class mcrl2::lps::untime_algorithm< Specification >

Definition at line 45 of file untime.h.

Member Typedef Documentation

◆ action_summand_type

template<typename Specification >
typedef process_type::action_summand_type mcrl2::lps::untime_algorithm< Specification >::action_summand_type
protected

Definition at line 50 of file untime.h.

◆ process_type

template<typename Specification >
typedef Specification::process_type mcrl2::lps::untime_algorithm< Specification >::process_type
protected

Definition at line 49 of file untime.h.

◆ super

template<typename Specification >
typedef detail::lps_algorithm<Specification> mcrl2::lps::untime_algorithm< Specification >::super
protected

Definition at line 48 of file untime.h.

Constructor & Destructor Documentation

◆ untime_algorithm()

template<typename Specification >
mcrl2::lps::untime_algorithm< Specification >::untime_algorithm ( Specification &  spec,
bool  add_invariants,
bool  apply_fourier_motzkin,
const data::rewriter r 
)
inline

Definition at line 216 of file untime.h.

Member Function Documentation

◆ calculate_time_invariant()

template<typename Specification >
data::data_expression mcrl2::lps::untime_algorithm< Specification >::calculate_time_invariant ( )
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.

Definition at line 76 of file untime.h.

◆ run()

template<typename Specification >
void mcrl2::lps::untime_algorithm< Specification >::run ( )
inline

Definition at line 226 of file untime.h.

◆ untime()

template<typename Specification >
void mcrl2::lps::untime_algorithm< Specification >::untime ( action_summand_type s)
inlineprotected

Apply untime to an action summand.

Definition at line 134 of file untime.h.

Member Data Documentation

◆ m_add_invariants

template<typename Specification >
bool mcrl2::lps::untime_algorithm< Specification >::m_add_invariants
protected

Definition at line 53 of file untime.h.

◆ m_apply_fm

template<typename Specification >
bool mcrl2::lps::untime_algorithm< Specification >::m_apply_fm
protected

Definition at line 54 of file untime.h.

◆ m_identifier_generator

template<typename Specification >
data::set_identifier_generator mcrl2::lps::untime_algorithm< Specification >::m_identifier_generator
protected

Identifier generator, for generating fresh identifiers.

Definition at line 69 of file untime.h.

◆ m_last_action_time

template<typename Specification >
data::variable mcrl2::lps::untime_algorithm< Specification >::m_last_action_time
protected

Variable denoting the time at which the last action occurred.

Definition at line 59 of file untime.h.

◆ m_rewriter

template<typename Specification >
const data::rewriter& mcrl2::lps::untime_algorithm< Specification >::m_rewriter
protected

Definition at line 55 of file untime.h.

◆ m_time_invariant

template<typename Specification >
data::data_expression mcrl2::lps::untime_algorithm< Specification >::m_time_invariant
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.

Definition at line 66 of file untime.h.


The documentation for this class was generated from the following file: