mcrl2/pbes/pbesinst_algorithm.h

Include file:

#include "mcrl2/pbes/pbesinst_algorithm.h"

Algorithm for instantiating a PBES.

Classes

Functions

void mcrl2::pbes_system::make_pbesinst_substitution(const data::variable_list &v, const data::data_expression_list &e, data::rewriter::substitution_type &sigma)

Creates a substitution function for the pbesinst rewriter.

Parameters:

  • v A sequence of data variables
  • e A sequence of data expressions
  • sigma The substitution that maps the i-th element of v to the i-th element of e
bool mcrl2::pbes_system::pbesinst_is_constant(const pbes_expression &x)