mcrl2/pbes/parse.h

Include file:

#include "mcrl2/pbes/parse.h"

Parser for pbes expressions.

Classes

  • mcrl2::pbes_system::detail::pbes_actions
  • mcrl2::pbes_system::untyped_pbes

Functions

std::istream &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

pbes mcrl2::pbes_system::parse_pbes(std::istream &in)
pbes mcrl2::pbes_system::parse_pbes(const std::string &text)
pbes_expression 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.

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.

propositional_variable mcrl2::pbes_system::parse_propositional_variable(const std::string &text, const VariableContainer &variables, const data::data_specification &dataspec = data::data_specification())

Functions

void mcrl2::pbes_system::detail::complete_pbes(pbes &x)
pbes_expression mcrl2::pbes_system::detail::parse_pbes_expression_new(const std::string &text)
untyped_pbes mcrl2::pbes_system::detail::parse_pbes_new(const std::string &text)