mcrl2/lps/sumelm.h

Include file:

#include "mcrl2/lps/sumelm.h"

Provides an implemenation 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.

Functions

bool mcrl2::lps::sumelm(action_summand &s)

Apply the sum elimination lemma to summand s.

Parameters:

  • s an action summand

Returns: true if any summation variables have been removed, or false otherwise.

bool mcrl2::lps::sumelm(stochastic_action_summand &s)

Apply the sum elimination lemma to summand s.

Parameters:

  • s a stochastic action summand

Returns: true if any summation variables have been removed, or false otherwise.

bool mcrl2::lps::sumelm(deadlock_summand &s)

Apply the sum elimination lemma to summand s.

Parameters:

  • s a deadlock summand

Returns: true if any summation variables have been removed, or false otherwise.