mcrl2::pbes_system::pbes¶

Include file:

#include "mcrl2/pbes/pbes.h

class mcrl2::pbes_system::pbes

parameterized boolean equation system

Public types¶

type mcrl2::pbes_system::pbes::equation_type

typedef for pbes_equation

Protected attributes¶

data::data_specification mcrl2::pbes_system::pbes::m_data

The data specification.

std::vector<pbes_equation> mcrl2::pbes_system::pbes::m_equations

The sequence of pbes equations.

std::set<data::variable> mcrl2::pbes_system::pbes::m_global_variables

The set of global variables.

propositional_variable_instantiation mcrl2::pbes_system::pbes::m_initial_state

The initial state.

Protected member functions¶

std::set<propositional_variable> compute_declared_variables() const

Returns the predicate variables appearing in the left hand side of an equation.

Returns: The predicate variables appearing in the left hand side of an equation.

void init_term(const atermpp::aterm_appl &t)

Initialize the pbes from an aterm.

Parameters:

• t A term

bool is_declared_in(Iter first, Iter last, const propositional_variable_instantiation &v, const data::data_specification &data_spec) const

Checks if the propositional variable instantiation v appears with the right type in the sequence of propositional variable declarations [first, last).

Parameters:

• first Start of a sequence of propositional variable declarations

• last End of a sequence of propositional variable declarations

• v A propositional variable instantation

• data_spec A data specification.

Returns: True if the type of v is matched correctly

Parameters:

• v A propositional variable instantiation

Public member functions¶

std::set<propositional_variable> binding_variables() const

Returns the set of binding variables of the pbes. This is the set variables that occur on the left hand side of an equation.

Returns: The set of binding variables of the pbes.

const data::data_specification &data() const

Returns the data specification.

Returns: The data specification of the pbes

data::data_specification &data()

Returns the data specification.

Returns: The data specification of the pbes

const std::vector<pbes_equation> &equations() const

Returns the equations.

Returns: The equations.

std::vector<pbes_equation> &equations()

Returns the equations.

Returns: The equations.

const std::set<data::variable> &global_variables() const

Returns the declared free variables of the pbes.

Returns: The declared free variables of the pbes.

std::set<data::variable> &global_variables()

Returns the declared free variables of the pbes.

Returns: The declared free variables of the pbes.

const propositional_variable_instantiation &initial_state() const

Returns the initial state.

Returns: The initial state.

propositional_variable_instantiation &initial_state()

Returns the initial state.

Returns: The initial state.

bool is_closed() const

True if the pbes is closed.

Returns: Returns true if all occurring variables are binding variables, and the initial state variable is a binding variable.

bool is_well_typed() const

Checks if the PBES is well typed.

Returns: True if the sorts occurring in the free variables of the equations are declared in the data specification the sorts occurring in the binding variable parameters are declared in the data specification the sorts occurring in the quantifier variables of the equations are declared in the data specification the binding variables of the equations have unique names (well formedness) the global variables occurring in the equations are declared in global_variables()the global variables occurring in the equations with the same name are identical the declared global variables and the quantifier variables occurring in the equations have different names the predicate variable instantiations occurring in the equations match with their declarations the predicate variable instantiation occurring in the initial state matches with the declaration the data specification is well typed

N.B. Conflicts between the types of instantiations and declarations of binding variables are not checked!

void load(std::istream &stream, bool binary = true, const std::string &source = "")

Reads the parameterized boolean equation system from a stream.

Parameters:

• stream The stream to read from.

• binary An indicator whether the stream is binary or textual.

• source The source from which the stream originates. Used for error messages.

std::set<propositional_variable_instantiation> occurring_variable_instantiations() const

Returns the set of occurring propositional variable instantiations of the pbes. This is the set of variables that occur in the right hand side of an equation.

Returns: The occurring propositional variable instantiations of the pbes

std::set<propositional_variable> occurring_variables() const

Returns the set of occurring propositional variable declarations of the pbes, i.e. the propositional variable declarations that occur in the right hand side of an equation.

Returns: The occurring propositional variable declarations of the pbes

pbes() = default

Constructor.

pbes(atermpp::aterm_appl t, const bool data_specification_is_type_checked = true)

Constructor.

Parameters:

• t An aterm representing a pbes_specification.

• data_specification_is_type_checked A boolean that indicates whether the data specification in the term has been type checked. If so, the internal data specification data structures will be set up. Otherwise, the function declare_data_specification_to_be_type_checked must be invoked after type checking, before the data specification can be used.

pbes(data::data_specification const &data, const std::vector<pbes_equation> &equations, propositional_variable_instantiation initial_state)

Constructor.

Parameters:

• data A data specification

• equations A sequence of pbes equations

• initial_state A propositional variable instantiation

pbes(data::data_specification const &data, const std::vector<pbes_equation> &equations, const std::set<data::variable> &global_variables, propositional_variable_instantiation initial_state)

Constructor.

Parameters:

• data A data specification

• equations A sequence of pbes equations

• global_variables A sequence of free variables

• initial_state A propositional variable instantiation

void save(std::ostream &stream, bool binary = true) const

Writes the pbes to a stream.

Parameters:

• stream The stream to which the pbes is written.

• binary If binary is true the pbes is saved in compressed binary format. Otherwise an ascii representation is saved. In general the binary format is much more compact than the ascii representation.