Struct TLAParser 

pub struct TLAParser {}

Parser for supported subset of TLA+

This parser is designed to parse TLA+ specifications that fall into the translatable fragment

Implementations

impl TLAParser

pub fn new() -> Self

Create a new parser for TLA specifications

fn parse_specification_and_add_expressions<'a>( &self, pair: Vec<Pair<'a, Rule>>, builder: ELTLSpecificationBuilder<'a, GeneralThresholdAutomaton>, ctx: TLAParsingContext<'_>, ) -> Result<ELTLSpecificationBuilder<'a, GeneralThresholdAutomaton>, Error>

Parse specification list into ltl expressions

fn parse_ta_and_return_ltl_pairs<'a>( &self, input: &'a str, ) -> Result<(GeneralThresholdAutomaton, Vec<Pair<'a, Rule>>, TLAParsingContext<'a>), Error>

fn validate_module_imports<'a>( pairs: &mut Pairs<'a, Rule>, pair: Pair<'a, Rule>, ) -> Pair<'a, Rule>

Validate the imports appearing in the TLA file

This function will not fail, it will only produce warnings on TLC compatibility

fn parse_constant_declaration<'a>( pairs: &mut Pairs<'a, Rule>, pair: Pair<'a, Rule>, builder: GeneralThresholdAutomatonBuilder, ) -> Result<(Pair<'a, Rule>, GeneralThresholdAutomatonBuilder), Error>

Parses all constant declarations

This block will parse all consecutive constant_declarations pairs. Every such block is CONSTANT declaration and declares the parameters of a threshold automaton. Additionally, the constants NbOfCorrProcesses and Processes should be declared.

fn parse_assume_declaration<'a>( pair: Pair<'a, Rule>, builder: InitializedGeneralThresholdAutomatonBuilder, ctx: &mut TLAParsingContext<'_>, ) -> Result<InitializedGeneralThresholdAutomatonBuilder, Error>

Parse and validate an ASSUME block, i.e. a resilience condition

This function parses one ASSUME definition, but there can be potentially multiple ones

fn parse_variable_declaration<'a>( pairs: &mut Pairs<'a, Rule>, pair: Pair<'a, Rule>, builder: GeneralThresholdAutomatonBuilder, ) -> Result<(Pair<'a, Rule>, GeneralThresholdAutomatonBuilder), Error>

Parse a variable declaration, i.e. the VARIABLE / VARIABLES declaration of of a TLA file

This declaration needs to declare all shared variables of the resulting TA, as well as the variable ‘ProcessesLocations’ which is the function from process identifiers to their current location.

fn parse_type_ok<'a>( pairs: &mut Pairs<'a, Rule>, pair: Pair<'a, Rule>, builder: GeneralThresholdAutomatonBuilder, ) -> Result<(Pair<'a, Rule>, InitializedGeneralThresholdAutomatonBuilder), Error>

Parse the TypeOk block into the set of locations and validates that it declares a type for all shared variables, that should be declared as type ‘Nat’.

fn parse_initial_constraint_declaration<'a>( pairs: &mut Pairs<'a, Rule>, pair: Pair<'a, Rule>, builder: InitializedGeneralThresholdAutomatonBuilder, ctx: &mut TLAParsingContext<'_>, ) -> Result<(Option<Pair<'a, Rule>>, InitializedGeneralThresholdAutomatonBuilder), Error>

Parse the initial constraints of an Init block

fn parse_int_macro_declarations<'a>( pairs: &mut Pairs<'a, Rule>, pair: Option<Pair<'a, Rule>>, ctx: &mut TLAParsingContext<'a>, ) -> Option<Pair<'a, Rule>>

Parse all consecutive declaration of integer macros

fn parse_rule_declarations<'a>( pairs: &mut Pairs<'a, Rule>, pair: Pair<'a, Rule>, builder: InitializedGeneralThresholdAutomatonBuilder, ctx: &mut TLAParsingContext<'a>, ) -> Result<(Option<Pair<'a, Rule>>, InitializedGeneralThresholdAutomatonBuilder), Error>

Parse all consecutive declarations of rules

fn parse_next_declaration<'a>( pairs: &mut Pairs<'a, Rule>, pair: Option<Pair<'a, Rule>>, ctx: &mut TLAParsingContext<'_>, ) -> Result<Option<Pair<'a, Rule>>, Error>

Parse a Next declaration and extract all appearing rules

fn validate_spec_declaration<'a>( pairs: &mut Pairs<'a, Rule>, pair: Option<Pair<'a, Rule>>, ctx: &mut TLAParsingContext<'_>, builder: &InitializedGeneralThresholdAutomatonBuilder, ) -> Result<Option<Pair<'a, Rule>>, Error>

Parse a Spec declaration and validate that it is consistent

Trait Implementations

impl Default for TLAParser

fn default() -> Self

Returns the “default value” for a type.

impl ParseTA for TLAParser

fn parse_ta(&self, input: &str) -> Result<GeneralThresholdAutomaton, Error>

Try to parse the threshold automaton from a string.

impl ParseTAWithLTL for TLAParser

fn parse_ta_and_spec( &self, input: &str, ) -> Result<(GeneralThresholdAutomaton, ELTLSpecification), Error>

Try to parse the threshold automaton and LTL specification from a string.