mcrl2/modal_formula/parse.h

Include file:

#include "mcrl2/modal_formula/parse.h"

add your file description here.

Classes

  • mcrl2::action_formulas::detail::action_formula_actions
  • mcrl2::state_formulas::parse_state_formula_options
  • mcrl2::regular_formulas::detail::regular_formula_actions
  • mcrl2::state_formulas::detail::state_formula_actions
  • mcrl2::state_formulas::detail::untyped_state_formula_specification

Functions

action_formula mcrl2::action_formulas::parse_action_formula(const std::string &text, const data::data_specification &dataspec, const VariableContainer &variables, const ActionLabelContainer &actions)
action_formula mcrl2::action_formulas::parse_action_formula(const std::string &text, const lps::specification &lpsspec)

Functions

action_formula mcrl2::action_formulas::detail::parse_action_formula(const std::string &text)

Functions

regular_formula mcrl2::regular_formulas::parse_regular_formula(const std::string &text, const data::data_specification &dataspec, const VariableContainer &variables, const ActionLabelContainer &actions)
regular_formula mcrl2::regular_formulas::parse_regular_formula(const std::string &text, const lps::specification &lpsspec)

Functions

regular_formula mcrl2::regular_formulas::detail::parse_regular_formula(const std::string &text)

Functions

state_formula mcrl2::state_formulas::parse_state_formula(const std::string &text, lps::specification &lpsspec, parse_state_formula_options options = parse_state_formula_options())

Parses a state formula from an input stream.

Parameters:

  • text A string.
  • lpsspec A linear process specification used as context. The data specification of lpsspec is extended with sorts appearing in the formula.
  • options A set of options guiding parsing.

Returns: The parse result.

state_formula mcrl2::state_formulas::parse_state_formula(std::istream &in, lps::specification &lpsspec, parse_state_formula_options options = parse_state_formula_options())

Parses a state formula from an input stream.

Parameters:

  • in A stream.
  • lpsspec A linear process specification used as context. The data specification of lpsspec is extended with sorts appearing in the formula.
  • options A set of options guiding parsing.

Returns: The parse result.

state_formula_specification mcrl2::state_formulas::parse_state_formula_specification(const std::string &text, parse_state_formula_options options = parse_state_formula_options())

Parses a state formula specification from a string.

Parameters:

  • text A string.
  • options A set of options guiding parsing.

Returns: The parse result.

state_formula_specification mcrl2::state_formulas::parse_state_formula_specification(std::istream &in, parse_state_formula_options options = parse_state_formula_options())

Parses a state formula specification from an input stream.

Parameters:

  • in An input stream.
  • options A set of options guiding parsing.

Returns: The parse result.

state_formula_specification mcrl2::state_formulas::parse_state_formula_specification(const std::string &text, lps::specification &lpsspec, parse_state_formula_options options = parse_state_formula_options())

Parses a state formula specification from a string.

Parameters:

  • text A string
  • lpsspec A linear process containing data and action declarations necessary to type check the state formula.
  • options A set of options guiding parsing.

Returns: The parse result

state_formula_specification mcrl2::state_formulas::parse_state_formula_specification(std::istream &in, lps::specification &lpsspec, parse_state_formula_options options = parse_state_formula_options())

Parses a state formula specification from an input stream.

Parameters:

  • in An input stream.
  • lpsspec A linear process containing data and action declarations necessary to type check the state formula.
  • options A set of options guiding parsing.

Returns: The parse result.

state_formula mcrl2::state_formulas::post_process_state_formula(const state_formula &formula, parse_state_formula_options options = parse_state_formula_options())

Functions

void mcrl2::state_formulas::detail::check_actions(const state_formulas::state_formula &formula, const lps::specification &lpsspec)

Prints a warning if formula contains an action that is not used in lpsspec.

state_formula mcrl2::state_formulas::detail::parse_state_formula(const std::string &text)
state_formula_specification mcrl2::state_formulas::detail::parse_state_formula_specification(const std::string &text)