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

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.