Include file:
#include "mcrl2/pbes/pbes.h
mcrl2::pbes_system::
pbes
¶parameterized boolean equation system
equation_type
¶typedef for pbes_equation
m_equations
¶The sequence of pbes equations.
m_initial_state
¶The initial state.
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.
init_term
(const atermpp::aterm_appl &t)¶Initialize the pbes from an aterm.
Parameters:
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:
Returns: True if the type of v is matched correctly
Parameters:
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.
data
() const¶Returns the data specification.
Returns: The data specification of the pbes
data
()¶Returns the data specification.
Returns: The data specification of the pbes
equations
() const¶Returns the equations.
Returns: The equations.
equations
()¶Returns the equations.
Returns: The equations.
global_variables
() const¶Returns the declared free variables of the pbes.
Returns: The declared free variables of the pbes.
global_variables
()¶Returns the declared free variables of the pbes.
Returns: The declared free variables of the pbes.
initial_state
() const¶Returns the initial state.
Returns: The initial state.
initial_state
()¶Returns the initial state.
Returns: The initial state.
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.
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!
load
(std::istream &stream, bool binary = true, const std::string &source = "")¶Reads the parameterized boolean equation system from a stream.
Parameters:
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
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:
pbes
(data::data_specification const &data, const std::vector<pbes_equation> &equations, propositional_variable_instantiation initial_state)¶Constructor.
Parameters:
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:
save
(std::ostream &stream, bool binary = true) const¶Writes the pbes to a stream.
Parameters: