Include file:
#include "mcrl2/pbes/parse.h"
Parser for pbes expressions.
mcrl2::pbes_system::
operator>>
(std::istream &from, pbes &result)¶Reads a PBES from an input stream.
Parameters:
from An input stream
result A PBES
Returns: The input stream
mcrl2::pbes_system::
parse_pbes_expression
(const std::string &text, const data::data_specification &dataspec, const VariableContainer &variables, const PropositionalVariableContainer &propositional_variables, bool type_check = true, bool translate_user_notation = true, bool normalize_sorts = true)¶Parse a pbes expression. Throws an exception if something went wrong.
Parameters:
text A string containing a pbes expression.
variables A sequence of data variables that may appear in x.
propositional_variables A sequence of propositional variables that may appear in x.
dataspec A data specification.
type_check If true the parsed input is also typechecked.
Returns: The parsed PBES expression.
mcrl2::pbes_system::
parse_pbes_expression
(const std::string &text, const pbes &pbesspec, const VariableContainer &variables, bool type_check = true, bool translate_user_notation = true, bool normalize_sorts = true)¶Parse a pbes expression. Throws an exception if something went wrong.
Parameters:
text A string containing a pbes expression.
pbesspec A PBES used as context.
variables A sequence of data variables that may appear in x.
type_check If true the parsed input is also typechecked.
Returns: The parsed PBES expression.
mcrl2::pbes_system::
parse_propositional_variable
(const std::string &text, const VariableContainer &variables, const data::data_specification &dataspec = data::data_specification())¶parse_pbes_expression
(const std::string &text)¶parse_pbes_expression_new
(const std::string &text)¶parse_pbes_new
(const std::string &text)¶parse_propositional_variable
(const std::string &text)¶