mCRL2
|
parameterized boolean equation system More...
#include <pbes.h>
Public Types | |
typedef pbes_equation | equation_type |
Public Member Functions | |
pbes ()=default | |
Constructor. | |
pbes (const data::data_specification &data, const std::vector< pbes_equation > &equations, propositional_variable_instantiation initial_state) | |
Constructor. | |
pbes (const data::data_specification &data, const std::set< data::variable > &global_variables, const std::vector< pbes_equation > &equations, propositional_variable_instantiation initial_state) | |
Constructor. | |
const data::data_specification & | data () const |
Returns the data specification. | |
data::data_specification & | data () |
Returns the data specification. | |
const std::vector< pbes_equation > & | equations () const |
Returns the equations. | |
std::vector< pbes_equation > & | equations () |
Returns the equations. | |
const std::set< data::variable > & | global_variables () const |
Returns the declared free variables of the pbes. | |
std::set< data::variable > & | global_variables () |
Returns the declared free variables of the pbes. | |
const propositional_variable_instantiation & | initial_state () const |
Returns the initial state. | |
propositional_variable_instantiation & | initial_state () |
Returns the initial state. | |
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. | |
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. | |
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. | |
bool | is_closed () const |
True if the pbes is closed. | |
bool | is_well_typed () const |
Checks if the PBES is well typed. | |
Protected Member Functions | |
std::set< propositional_variable > | compute_declared_variables () const |
Returns the predicate variables appearing in the left hand side of an equation. | |
template<typename Iter > | |
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). | |
Protected Attributes | |
data::data_specification | m_data |
The data specification. | |
std::vector< pbes_equation > | m_equations |
The sequence of pbes equations. | |
std::set< data::variable > | m_global_variables |
The set of global variables. | |
propositional_variable_instantiation | m_initial_state |
The initial state. | |
|
default |
Constructor.
|
inline |
|
inline |
|
inline |
|
inlineprotected |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inlineprotected |
Checks if the propositional variable instantiation v appears with the right type in the sequence of propositional variable declarations [first, last).
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. |
v
is matched correctly v | A propositional variable instantiation |
|
inline |
Checks if the PBES is well typed.
std::set< propositional_variable_instantiation > mcrl2::pbes_system::pbes::occurring_variable_instantiations | ( | ) | const |
|
inline |
|
protected |
|
protected |
|
protected |
|
protected |