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.
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.
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.
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.