mcrl2::lps::parelm_algorithm

Include file:

#include "mcrl2/lps/parelm.h

class mcrl2::lps::parelm_algorithm

Algorithm class for elimination of unused parameters from a linear process specification.

Private types

type mcrl2::lps::parelm_algorithm::super

typedef for lps::detail::lps_algorithm< Specification >

Protected member functions

void parelm1()

First version of parelm1.

void parelm2()

Second version of parelm that builds a dependency graph.

void report_results(const std::set<data::variable> &to_be_removed) const

std::set<data::variable> transition_variables()

Returns the data variables that are considered in the parelm algorithm.

Returns: The data variables that appear in the condition, action or time of the summands

Public member functions

parelm_algorithm(Specification &spec)

Constructor.

void run(bool variant1 = true)

Runs the parelm algorithm.