sumelm.h File Reference

Provides an implementation of the sum elimination lemma, as well as the removal of unused summation variables. The sum elimination lemma is the following: sum d:D . d == e -> X(d) = X(e). Removal of unused summation variables is according to the following lemma: d not in x implies sum d:D . x = x. More...

Go to the source code of this file.

Classes
class	mcrl2::lps::sumelm_algorithm< Specification >
	Class implementing the sum elimination lemma. More...

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.

Functions
bool	mcrl2::lps::sumelm (action_summand &s)
	Apply the sum elimination lemma to summand s.
bool	mcrl2::lps::sumelm (stochastic_action_summand &s)
	Apply the sum elimination lemma to summand s.
bool	mcrl2::lps::sumelm (deadlock_summand &s)
	Apply the sum elimination lemma to summand s.

Detailed Description

Provides an implementation of the sum elimination lemma, as well as the removal of unused summation variables. The sum elimination lemma is the following: sum d:D . d == e -> X(d) = X(e). Removal of unused summation variables is according to the following lemma: d not in x implies sum d:D . x = x.

Definition in file sumelm.h.