mcrl2/lps/parse.h

Include file:

#include "mcrl2/lps/parse.h"

add your file description here.

Functions

process::action mcrl2::lps::parse_action(const std::string &text, const process::action_label_list &action_decls, const data::data_specification &data_spec = data::detail::default_specification())

Parses an action from a string.

Parameters:

• text A string containing an action
• action_decls An action declaration
• data_spec A data specification used for sort normalization

Returns: An action exception * mcrl2::runtime_error when the input does not match the syntax of an action.

action_rename_specification mcrl2::lps::parse_action_rename_specification(const std::string &spec_string, const lps::stochastic_specification &spec)

Parses an action rename specification. Parses an acion rename specification. If the action rename specification contains data types that are not present in the data specification of spec they are added to it.

Parameters:

• spec_string A string containing an action rename specification.
• spec A linear process specification

Returns: An action rename specification

action_rename_specification mcrl2::lps::parse_action_rename_specification(std::istream &in, const lps::stochastic_specification &spec)

Parses a process specification from an input stream.

Parameters:

• in An input stream
• spec A linear process specification.

Returns: The parse result

specification mcrl2::lps::parse_linear_process_specification(const std::string &text)

Parses a linear process specification from a string.

Parameters:

• text A string containing a linear process specification

Returns: The parsed specification exception * non_linear_process if a non-linear sub-expression is encountered.

• mcrl2::runtime_error in the following cases: The number of equations is not equal to one The initial process is not a process instance, or it does not match with the equation A sequential process is found with a right hand side that is not a process instance, or it doesn’t match the equation

specification mcrl2::lps::parse_linear_process_specification(std::istream &spec_stream)

Parses a linear process specification from an input stream.

Parameters:

• spec_stream An input stream containing a linear process specification

Returns: The parsed specification exception * non_linear_process if a non-linear sub-expression is encountered.

• mcrl2::runtime_error in the following cases: The number of equations is not equal to one The initial process is not a process instance, or it does not match with the equation A sequential process is found with a right hand side that is not a process instance, or it doesn’t match the equation

void mcrl2::lps::parse_lps(const std::string &text, Specification &result)

void mcrl2::lps::parse_lps(std::istream&, Specification&)

template<>
void mcrl2::lps::parse_lps<specification>(std::istream &from, specification &result)

template<>
void mcrl2::lps::parse_lps<stochastic_specification>(std::istream &from, stochastic_specification &result)

Parses a stochastic linear process specification from an input stream.

Parameters:

• from An input stream containing a linear process specification.
• result An output parameter in which the parsed stochastic process is put.

Returns: The parsed specification. exception * non_linear_process if a non-linear sub-expression is encountered.

• mcrl2::runtime_error in the following cases: The number of equations is not equal to one. The initial process is not a process instance, or it does not match with the equation. A sequential process is found with a right hand side that is not a process instance, or it doesn’t match the equation.

multi_action mcrl2::lps::parse_multi_action(const std::string &text, const process::action_label_list &action_decls, const data::data_specification &data_spec = data::detail::default_specification())

Parses a multi_action from a string.

Parameters:

• text A string containing a multi_action
• action_decls A list of allowed action labels that is used for type checking.
• data_spec The data specification that is used for type checking.

Returns: The parsed multi_actionexception * mcrl2::runtime_error when the input does not match the syntax of a multi action.

multi_action mcrl2::lps::parse_multi_action(const std::string &text, multi_action_type_checker &typechecker, const data::data_specification &data_spec = data::detail::default_specification())

Parses a multi_action from a string.

Parameters:

• text A string containing a multi_action
• typechecker Typechecker used to check the action.
• data_spec The data specification that is used for type checking.

Returns: The parsed multi_actionexception * mcrl2::runtime_error when the input does not match the syntax of a multi action.

multi_action mcrl2::lps::parse_multi_action(std::stringstream &in, const process::action_label_list &action_decls, const data::data_specification &data_spec = data::detail::default_specification())

Parses a multi_action from an input stream.

Parameters:

• in An input stream containing a multi_action
• action_decls A list of allowed action labels that is used for type checking.
• data_spec The data specification that is used for type checking.

Returns: The parsed multi_actionexception * mcrl2::runtime_error when the input does not match the syntax of a multi action.

multi_action mcrl2::lps::parse_multi_action(std::stringstream &in, multi_action_type_checker &typechecker, const data::data_specification &data_spec = data::detail::default_specification())

Parses a multi_action from an input stream.

Parameters:

• in An input stream containing a multi_action
• typechecker Typechecker used to check the action.
• data_spec The data specification that is used for type checking.

Returns: The parsed multi_actionexception * mcrl2::runtime_error when the input does not match the syntax of a multi action.