ultimate_delay.h File Reference

This file defines the class ultimate_delay. An ultimate delay consists of a time variable t and expression exp(t,x) and free variables x. It can be read as a predicate on t of the form exists x.exp(t,x). If this is true for certain t, this indicates that a process can wait until time t.
More...

Go to the source code of this file.

Classes
class	mcrl2::lps::detail::ultimate_delay

Namespaces
namespace	mcrl2
	A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.
namespace	mcrl2::lps
	The main namespace for the LPS library.
namespace	mcrl2::lps::detail

Functions
ultimate_delay	mcrl2::lps::detail::combine_ultimate_delays (const ultimate_delay &delay1, const ultimate_delay &delay2)
	Returns the conjunction of the two delay conditions and the join of the variables, where the variables in delay2 are renamed to avoid conflict with those in delay1.

Detailed Description

This file defines the class ultimate_delay. An ultimate delay consists of a time variable t and expression exp(t,x) and free variables x. It can be read as a predicate on t of the form exists x.exp(t,x). If this is true for certain t, this indicates that a process can wait until time t.

Definition in file ultimate_delay.h.