Module bymc 

This module contains the parser for the ByMC specification format.

The parser uses the pest parser generator, with the grammar defined in bymc_format.pest. The grammar is based on the ByMC, but allows for more flexibility in the specification.

Structs

ByMCParser

Parser for the ByMC format

ByMCParsingContext 🔒

Context to store the definitions of macros in

PRATT_PARSER 🔒

PestByMCParser 🔒

Enums

Rule

This file specifies a pest grammar for the specification format introduced by BYMC (https://github.com/konnov/bymc).

Constants

_PEST_GRAMMAR_PestByMCParser 🔒

Functions

new_parsing_error 🔒

Generate a new parsing error

parse_action_expr 🔒

Parse an action expression into a list of actions

parse_action_list 🔒

Parse a list of action expressions into a combined list of actions

parse_assignment_expression 🔒

Parse an assignment expression of an action into the corresponding list of actions

parse_boolean_atom 🔒

Parse boolean_atom

parse_boolean_con 🔒

Parse boolean connectives

parse_boolean_const 🔒

Parse boolean constant

parse_boolean_expr 🔒

Parse a constraint from a boolean expression

parse_boolean_expr_list 🔒

Parse list of boolean expressions

parse_comparison_expr 🔒

Parse comparison expression, relating two integer expressions

parse_comparison_op 🔒

Parse comparison operator

parse_identifier_list_to_t 🔒

Parse a list of identifiers into a vector of objects of type T

parse_identifier_to_t 🔒

Parse an identifier into an object of type T

parse_integer_atom 🔒

Parse integer atom

parse_integer_binary_op 🔒

Parse an integer operator

parse_integer_const 🔒

Parse integer constant

parse_integer_expr 🔒

Parse expression over integers into an integer expression

parse_location 🔒

Parse a location definition

parse_location_list 🔒

Parse a list of location definitions

parse_ltl_atom 🔒

Parse an ltl atom into a single ltl expression

parse_ltl_expr 🔒

Parse an ltl expression into a single ltl expression

parse_ltl_specification 🔒

Parse a single ltl specification

parse_reset_expression 🔒

Parse a reset expression into the corresponding list of actions

parse_rule 🔒

Parse a rule

Type Aliases

CompExpr 🔒

Intermediate type for comparison expression of the form lhs op rhs