Struct ByMCParser 

pub struct ByMCParser;

Parser for the ByMC format

This parser implements the ParseToTA trait and can be used to parse threshold automata given in the ByMC format as introduced by BYMC.

Implementations

impl ByMCParser

pub fn new() -> Self

fn parse_ta_and_return_left_pair<'a>( &self, input: &'a str, ) -> Result<(GeneralThresholdAutomaton, Pairs<'a, Rule>, ByMCParsingContext<'a>), Error>

fn handle_local_vars<'a>( pairs: &mut Pairs<'a, Rule>, pair: Pair<'a, Rule>, builder: GeneralThresholdAutomatonBuilder, err_msg: &str, ) -> (GeneralThresholdAutomatonBuilder, Pair<'a, Rule>)

Handle potential local variables of the threshold automaton and return next pair

NOTE: Local variables are currently simply skipped

fn parse_shared_variables<'a>( pairs: &mut Pairs<'a, Rule>, pair: Pair<'a, Rule>, builder: GeneralThresholdAutomatonBuilder, err_msg: &str, ) -> Result<(GeneralThresholdAutomatonBuilder, Pair<'a, Rule>), BuilderError>

Parse shared variables and add them to the builder

This function checks whether the current pair is a shared variable list, parses the shared variable names and adds them to the builder. Afterwards, it computes the next pair to be processed.

If that pair is a again a shared variable list, the function continues to parse until the next pair is not a shared variable list and returns that pair and the modified builder.

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

Parse the list of parameters and add them to the builder

A parameter list must exist by the grammar definition.

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

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

Parse the list of locations and add them to the builder

A location list must exist by the grammar definition.

fn pares_and_add_potential_resilience_conditions( pair: Option<Pair<'_, Rule>>, builder: InitializedGeneralThresholdAutomatonBuilder, ctx: &ByMCParsingContext<'_>, ) -> Result<InitializedGeneralThresholdAutomatonBuilder, Error>

Parse potential resilience conditions and add them to the builder

This function checks whether the current pair is a resilience condition list, if so it tries to parse the resilience conditions and adds them to the builder.

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

Parse potential location constraints and add them to the builder

This function checks whether the current pair specifies initial constraints. It then tries to parse it into a variable constraint. If the constraint is not accepted by the initialized builder, it tries to parse it into a location constraint and returns the result.

fn parse_and_add_rules( pair: Pair<'_, Rule>, builder: InitializedGeneralThresholdAutomatonBuilder, ctx: &ByMCParsingContext<'_>, ) -> Result<InitializedGeneralThresholdAutomatonBuilder, Error>

Parse the list of rules and add them to the builder

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

Parse specification list into ltl expressions

Trait Implementations

impl Default for ByMCParser

fn default() -> Self

Returns the “default value” for a type.

impl ParseTA for ByMCParser

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

Parse a string in the ByMC to a threshold automaton

Example

use crate::taco_parser::bymc::ByMCParser;
use crate::taco_parser::*;

let spec = "skel Proc {
    parameters n;
    assumptions (1) {
        n >= 0;
    }
    locations (0) {}
    inits (0) {}
    rules (0) {}
}";
let parser = ByMCParser::new();
let ta = parser.parse_ta(spec).unwrap();

impl ParseTAWithLTL for ByMCParser

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

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