mcrl2/pbes/pbesinst_finite_algorithm.h

Include file:

#include "mcrl2/pbes/pbesinst_finite_algorithm.h"

add your file description here.

Classes

Typedefs

type mcrl2::pbes_system::pbesinst_index_map

typedef for std::map< core::identifier_string, std::vector< std::size_t > >

Data structure for storing the indices of the variables that should be expanded by the finite pbesinst algorithm.

type mcrl2::pbes_system::pbesinst_variable_map

typedef for std::map< core::identifier_string, std::vector< data::variable > >

Data structure for storing the variables that should be expanded by the finite pbesinst algorithm.

Functions

void mcrl2::pbes_system::pbesinst_finite(pbes &p, data::rewrite_strategy rewrite_strategy, const std::string &finite_parameter_selection)

Functions

void mcrl2::pbes_system::detail::split_parameters(const PropositionalVariable &X, const pbesinst_index_map &index_map, std::vector<Parameter> &finite, std::vector<Parameter> &infinite)

Computes the subset with variables of finite sort and infinite.

Parameters:

  • X A propositional variable instantiation

  • index_map a container storing the indices of the variables that should be expanded by the finite pbesinst algorithm.

  • finite A sequence of data expressions

  • infinite A sequence of data expressions