Module tla 

TLA+ Parser module

This module implements the parse for TLA+ specification files. You can find more information on the supported syntax under ./docs/tla-to-ta.md

Modules

integer_exprs 🔒

Module declaring helper functions to parse expressions over integers, including boolean expressions over integers

Structs

PestTLAParser 🔒

TLAParser

Parser for supported subset of TLA+

TLAParsingContext 🔒

Helper context for storing information such as declared integer macros during parsing

Enums

Rule

Constants

LOCATIONS_SET 🔒

Variable that is used to specify the set of locations

N_CORR_PROC 🔒

Constant for specifying the number of correct processes

PROC_SET 🔒

Constant for representing set of processes

_PEST_GRAMMAR_PestTLAParser 🔒

Functions

new_parsing_error 🔒

Generate a new parsing error

new_parsing_error_with_ctx 🔒

Generate a new parsing error and add context

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_initial_loc_constr 🔒

Parse a constraint over ProcessesLocations into the set of initial locations

parse_map_entry_into_map_ident_and_proc_ident 🔒

Parses a map_entry into the name of the map and the identifier of the element used as an index in the map

parse_map_update_to_target_location 🔒

Parse a map update / map redefinition to the target location of a rule

parse_next_expr 🔒

Parse all rule ids appearing in a Next expression

parse_rule_body_exprs 🔒

Parse all rule body expressions

parse_rule_ident_to_id_and_proc_ident 🔒

Parse the rule id out of the rule name and collect the name of the identifier used for specifying the process identifier

parse_set_of_locations 🔒

Parse the location declaration in ‘TypeOk’ or in ‘Init’ into a set of locations

split_conjunct_bool_expr 🔒

Split a conjunction of boolean expressions into a vector

try_parse_map_entry_constr_loc 🔒

Parses a map_boolean_expr into a [Location]

try_parse_map_redef_to_target_loc 🔒

Helper function to parse_map_update_to_target_location

validate_and_add_n_corr_proc_constr 🔒

Validate and remove constraints on special parameter N_CORR_PROC