taco_parser/
lib.rs

1//! Traits for parsers that can parse specifications and threshold automata.
2//!
3//! This module contains traits that parsers for threshold automata and LTL
4//! specifications should implement. The traits are:
5//! - `ParseTA`, for parsing threshold automata,
6//! - `ParseLTLSpec`, for parsing LTL specifications,
7//! - `ParseTAWithLTL`, for parsing threshold automata and LTL specifications.
8
9use anyhow::Error;
10use taco_model_checker::eltl::ELTLSpecification;
11use taco_threshold_automaton::general_threshold_automaton::GeneralThresholdAutomaton;
12
13// The pest derive generates errors as the doc comments are missing
14#[allow(missing_docs)]
15pub mod bymc;
16
17// The pest derive generates errors as the doc comments are missing
18#[allow(missing_docs)]
19pub mod tla;
20
21/// Parse a threshold automaton from a string.
22///
23/// Parsers for threshold automata should implement this trait.
24pub trait ParseTA {
25    /// Try to parse the threshold automaton from a string.
26    fn parse_ta(&self, input: &str) -> Result<GeneralThresholdAutomaton, Error>;
27}
28
29/// Parse a threshold automaton and an LTL specification from a string.
30///
31/// If you know a file or input includes both a threshold automaton and an LTL specification, prefer using this
32/// trait. Parsers for threshold automata and LTL specifications should implement
33/// this trait.
34pub trait ParseTAWithLTL {
35    /// Try to parse the threshold automaton and LTL specification from a string.
36    ///
37    /// Returns a tuple of the threshold automaton and the LTL specification.
38    fn parse_ta_and_spec(
39        &self,
40        input: &str,
41    ) -> Result<(GeneralThresholdAutomaton, ELTLSpecification), Error>;
42}