taco_parser/
bymc.rs

1//! This module contains the parser for the ByMC specification format.
2//!
3//! The parser uses the [pest](https://pest.rs/) parser generator, with the
4//! grammar defined in `bymc_format.pest`. The grammar is based on the ByMC, but
5//! allows for more flexibility in the specification.
6
7use std::{collections::BTreeMap, fmt::Debug};
8
9use anyhow::{Context, Error, anyhow};
10use log::debug;
11use pest::{
12    Parser, Span, error,
13    iterators::{Pair, Pairs},
14    pratt_parser::{Assoc, PrattParser},
15};
16use pest_derive::Parser;
17use taco_model_checker::eltl::{ELTLExpression, ELTLSpecification, ELTLSpecificationBuilder};
18
19use taco_threshold_automaton::{
20    expressions::{
21        Atomic, BooleanConnective, BooleanExpression, ComparisonOp, IntegerExpression, IntegerOp,
22        IsDeclared, Location, Parameter, Variable,
23    },
24    general_threshold_automaton::{
25        Action, GeneralThresholdAutomaton,
26        builder::{
27            BuilderError, GeneralThresholdAutomatonBuilder,
28            InitializedGeneralThresholdAutomatonBuilder, RuleBuilder,
29        },
30    },
31};
32
33use crate::ParseTAWithLTL;
34
35use super::ParseTA;
36
37// Location of the grammar file and generation of parser
38#[allow(missing_docs)]
39#[derive(Parser)]
40#[grammar = "./bymc_format.pest"]
41struct PestByMCParser;
42
43// Pratt parser responsible for maintaining operator precedence
44//
45// Here we simply borrow them from C++
46// [see](https://en.cppreference.com/w/cpp/language/operator_precedence)
47//
48// Additionally, we define the precedence of the temporal operators
49// - `G` (Globally) and `F` (Eventually) have the highest precedence
50// - `!` (Not) has the second highest precedence
51lazy_static::lazy_static! {
52    static ref PRATT_PARSER: PrattParser<Rule> = {
53        use pest::pratt_parser::{Op};
54
55        // Precedence is defined lowest to highest
56        PrattParser::new()
57            .op(Op::infix(Rule::or, Assoc::Left))
58            .op(Op::infix(Rule::implication, Assoc::Right))
59            .op(Op::infix(Rule::and, Assoc::Left))
60            .op(Op::infix(Rule::equal, Assoc::Left) | Op::infix(Rule::n_equal, Assoc::Left))
61            .op(Op::infix(Rule::less_eq, Assoc::Left)
62                | Op::infix(Rule::less, Assoc::Left)
63                | Op::infix(Rule::greater_eq, Assoc::Left)
64                | Op::infix(Rule::greater, Assoc::Left))
65            .op(Op::infix(Rule::add, Assoc::Left) | Op::infix(Rule::sub, Assoc::Left))
66            .op(Op::infix(Rule::mul, Assoc::Left) | Op::infix(Rule::div, Assoc::Left))
67            .op(Op::prefix(Rule::negation))
68            .op(Op::prefix(Rule::not))
69            .op(Op::prefix(Rule::eventually) |  Op::prefix(Rule::globally))
70    };
71}
72
73/// Context to store the definitions of macros in
74struct ByMCParsingContext<'a> {
75    /// Macros for integer expressions
76    define_macro: BTreeMap<String, Pair<'a, Rule>>,
77}
78
79impl<'a> ByMCParsingContext<'a> {
80    fn new() -> Self {
81        Self {
82            define_macro: BTreeMap::new(),
83        }
84    }
85
86    fn add_macro(
87        &mut self,
88        name: String,
89        pair: Pair<'a, Rule>,
90    ) -> Result<(), Box<pest::error::Error<()>>> {
91        if self.define_macro.contains_key(&name) {
92            return Err(new_parsing_error(
93                format!("Duplicate macro with name '{}', second definition: ", name),
94                pair.as_span(),
95            ));
96        }
97        self.define_macro.insert(name, pair);
98        Ok(())
99    }
100}
101
102/// Parser for the ByMC format
103///
104/// This parser implements the `ParseToTA` trait and can be used to parse
105/// threshold automata given in the ByMC format as introduced by
106/// [BYMC](https://github.com/konnov/bymc).
107pub struct ByMCParser;
108
109impl ParseTA for ByMCParser {
110    /// Parse a string in the ByMC to a threshold automaton
111    ///
112    /// # Example
113    ///
114    /// ```
115    /// use crate::taco_parser::bymc::ByMCParser;
116    /// use crate::taco_parser::*;
117    ///
118    /// let spec = "skel Proc {
119    ///     parameters n;
120    ///     assumptions (1) {
121    ///         n >= 0;
122    ///     }
123    ///     locations (0) {}
124    ///     inits (0) {}
125    ///     rules (0) {}
126    /// }";
127    /// let parser = ByMCParser::new();
128    /// let ta = parser.parse_ta(spec).unwrap();
129    /// ```
130    fn parse_ta(&self, input: &str) -> Result<GeneralThresholdAutomaton, Error> {
131        let (ta, _, _) = self.parse_ta_and_return_left_pair(input)?;
132        Ok(ta)
133    }
134}
135
136impl ParseTAWithLTL for ByMCParser {
137    fn parse_ta_and_spec(
138        &self,
139        input: &str,
140    ) -> Result<(GeneralThresholdAutomaton, ELTLSpecification), Error> {
141        let (ta, mut pairs, ctx) = self.parse_ta_and_return_left_pair(input)?;
142
143        let ltl_spec = Self::parse_specification_and_add_expressions(
144            pairs
145                .next()
146                .ok_or_else(|| anyhow!("No specification found"))?,
147            ELTLSpecificationBuilder::new(&ta),
148            &ctx,
149        )?;
150        let ltl_spec = ltl_spec.build();
151
152        Ok((ta, ltl_spec))
153    }
154}
155
156impl Default for ByMCParser {
157    fn default() -> Self {
158        Self::new()
159    }
160}
161
162impl ByMCParser {
163    pub fn new() -> Self {
164        ByMCParser {}
165    }
166
167    fn parse_ta_and_return_left_pair<'a>(
168        &self,
169        input: &'a str,
170    ) -> Result<
171        (
172            GeneralThresholdAutomaton,
173            Pairs<'a, Rule>,
174            ByMCParsingContext<'a>,
175        ),
176        Error,
177    > {
178        let mut pairs = PestByMCParser::parse(Rule::bymc_spec, input)?;
179
180        let pair = pairs.next().expect("Missing: name of threshold automaton");
181        let name: String = parse_identifier_to_t(&pair);
182        let mut builder = GeneralThresholdAutomatonBuilder::new(name);
183
184        let error_msg_nxt_required = "Missing: parameters of threshold automaton";
185
186        let mut pair = pairs.next().expect(error_msg_nxt_required);
187
188        (builder, pair) =
189            Self::handle_local_vars(&mut pairs, pair, builder, error_msg_nxt_required);
190
191        (builder, pair) =
192            Self::parse_shared_variables(&mut pairs, pair, builder, error_msg_nxt_required)
193                .with_context(|| "Failed to parse shared variables:")?;
194
195        (builder, pair) = Self::parse_and_add_parameters(&mut pairs, pair, builder)
196            .with_context(|| "Failed to parse parameters: ")?;
197
198        let mut ctx = ByMCParsingContext::new();
199        (builder, pair) = Self::parse_and_add_define_macros(&mut pairs, pair, builder, &mut ctx)
200            .with_context(|| "Failed to parse macro definitions: ")?;
201
202        // Check for resilience conditions, delay the actual parsing after the builder initialization
203        let mut rc = None;
204        if pair.as_rule() == Rule::assumption_list {
205            rc = Some(pair);
206            pair = pairs
207                .next()
208                .expect("Missing: locations of threshold automaton");
209        }
210
211        (builder, pair) = Self::parse_and_add_locations(&mut pairs, pair, builder)
212            .with_context(|| "Failed to parse locations: ")?;
213
214        // Locations, Variables and Parameters are now fixed, initialize the builder
215        let mut builder = builder.initialize();
216
217        builder = Self::pares_and_add_potential_resilience_conditions(rc, builder, &ctx)?;
218
219        (builder, pair) =
220            Self::parse_and_add_location_and_var_constraints(&mut pairs, pair, builder, &ctx)?;
221
222        builder = Self::parse_and_add_rules(pair, builder, &ctx)?;
223
224        Ok((builder.build(), pairs, ctx))
225    }
226
227    /// Handle potential local variables of the threshold automaton and return next pair
228    ///
229    /// **NOTE**: Local variables are currently simply skipped
230    fn handle_local_vars<'a>(
231        pairs: &mut Pairs<'a, Rule>,
232        mut pair: Pair<'a, Rule>,
233        builder: GeneralThresholdAutomatonBuilder,
234        err_msg: &str,
235    ) -> (GeneralThresholdAutomatonBuilder, Pair<'a, Rule>) {
236        while pair.as_rule() == Rule::local_variables {
237            debug!("Local variables are not supported, skipping them!");
238            pair = pairs.next().expect(err_msg);
239        }
240
241        (builder, pair)
242    }
243
244    /// Parse shared variables and add them to the builder
245    ///
246    /// This function checks whether the current pair is a shared variable list,
247    /// parses the shared variable names and adds them to the builder.
248    /// Afterwards, it computes the next pair to be processed.
249    ///
250    /// If that pair is a again a shared variable list, the function continues
251    /// to parse until the next pair is not a shared variable list and returns
252    /// that pair and the modified builder.
253    fn parse_shared_variables<'a>(
254        pairs: &mut Pairs<'a, Rule>,
255        mut pair: Pair<'a, Rule>,
256        mut builder: GeneralThresholdAutomatonBuilder,
257        err_msg: &str,
258    ) -> Result<(GeneralThresholdAutomatonBuilder, Pair<'a, Rule>), BuilderError> {
259        while pair.as_rule() == Rule::shared_variables {
260            let vars = parse_identifier_list_to_t::<Variable>(pair.into_inner().next().unwrap());
261            builder = builder.with_variables(vars)?;
262
263            pair = pairs.next().expect(err_msg);
264        }
265
266        Ok((builder, pair))
267    }
268
269    /// Parse the list of parameters and add them to the builder
270    ///
271    /// A parameter list must exist by the grammar definition.
272    fn parse_and_add_parameters<'a>(
273        pairs: &mut Pairs<'a, Rule>,
274        pair: Pair<'a, Rule>,
275        builder: GeneralThresholdAutomatonBuilder,
276    ) -> Result<(GeneralThresholdAutomatonBuilder, Pair<'a, Rule>), BuilderError> {
277        debug_assert!(
278            pair.as_rule() == Rule::parameters,
279            "Got rule {:?} for {}",
280            pair.as_rule(),
281            pair.as_str(),
282        );
283
284        let mut pair = pair;
285        let mut builder = builder;
286
287        while pair.as_rule() == Rule::parameters {
288            let parameters =
289                parse_identifier_list_to_t::<Parameter>(pair.into_inner().next().unwrap());
290
291            builder = builder.with_parameters(parameters)?;
292
293            pair = pairs
294                .next()
295                .expect("Missing: locations of threshold automaton");
296        }
297
298        Ok((builder, pair))
299    }
300
301    fn parse_and_add_define_macros<'a>(
302        pairs: &mut Pairs<'a, Rule>,
303        pair: Pair<'a, Rule>,
304        builder: GeneralThresholdAutomatonBuilder,
305        ctx: &mut ByMCParsingContext<'a>,
306    ) -> Result<(GeneralThresholdAutomatonBuilder, Pair<'a, Rule>), Box<pest::error::Error<()>>>
307    {
308        let mut pair = pair;
309        while pair.as_rule() == Rule::define_statement {
310            let mut inners = pair.into_inner();
311
312            let ident_pair = inners.next().expect("Missing: define identifier");
313            let ident: String = parse_identifier_to_t(&ident_pair);
314
315            let int_pair = inners.next().expect("Missing: define integer expr");
316            ctx.add_macro(ident, int_pair)?;
317
318            pair = pairs.next().expect("Missing: location definition");
319        }
320        Ok((builder, pair))
321    }
322
323    /// Parse the list of locations and add them to the builder
324    ///
325    /// A location list must exist by the grammar definition.
326    fn parse_and_add_locations<'a>(
327        pairs: &mut Pairs<'a, Rule>,
328        pair: Pair<'a, Rule>,
329        mut builder: GeneralThresholdAutomatonBuilder,
330    ) -> Result<(GeneralThresholdAutomatonBuilder, Pair<'a, Rule>), BuilderError> {
331        debug_assert!(
332            pair.as_rule() == Rule::location_list,
333            "Got rule {:?} for {}",
334            pair.as_rule(),
335            pair.as_str(),
336        );
337
338        let locations = parse_location_list(pair);
339        builder = builder.with_locations(locations)?;
340
341        let pair = pairs.next().expect("Missing: rules of threshold automaton");
342
343        Ok((builder, pair))
344    }
345
346    /// Parse potential resilience conditions and add them to the builder
347    ///
348    /// This function checks whether the current pair is a resilience condition
349    /// list, if so it tries to parse the resilience conditions and adds them
350    /// to the builder.
351    fn pares_and_add_potential_resilience_conditions(
352        pair: Option<Pair<'_, Rule>>,
353        mut builder: InitializedGeneralThresholdAutomatonBuilder,
354        ctx: &ByMCParsingContext,
355    ) -> Result<InitializedGeneralThresholdAutomatonBuilder, anyhow::Error> {
356        if let Some(pair) = pair {
357            debug_assert!(
358                pair.as_rule() == Rule::assumption_list,
359                "Got rule {:?} for {}",
360                pair.as_rule(),
361                pair.as_str(),
362            );
363
364            let mut pairs = pair.into_inner();
365
366            // integer specifying the number of assumptions, ignoring since it is usually invalid
367            let _n_rc = parse_integer_const(pairs.next().unwrap());
368
369            let rc = parse_boolean_expr_list(pairs.next().unwrap(), &builder, ctx)
370                .with_context(|| "Failed to parse resilience conditions (assumptions):")?;
371
372            builder = builder
373                .with_resilience_conditions(rc)
374                .with_context(|| "Failed to validate resilience conditions (assumptions): ")?;
375        }
376
377        Ok(builder)
378    }
379
380    /// Parse potential location constraints and add them to the builder
381    ///
382    /// This function checks whether the current pair specifies initial
383    /// constraints. It then tries to parse it into a variable constraint. If
384    /// the constraint is not accepted by the initialized builder, it tries to
385    /// parse it into a location constraint and returns the result.
386    fn parse_and_add_location_and_var_constraints<'a>(
387        pairs: &mut Pairs<'a, Rule>,
388        mut pair: Pair<'a, Rule>,
389        mut builder: InitializedGeneralThresholdAutomatonBuilder,
390        ctx: &ByMCParsingContext,
391    ) -> Result<(InitializedGeneralThresholdAutomatonBuilder, Pair<'a, Rule>), anyhow::Error> {
392        if pair.as_rule() == Rule::initial_condition_list {
393            let mut inner_pairs = pair.into_inner();
394
395            // integer specifying the number of constraints, ignoring since it is usually invalid
396            let _n_loc_constr = parse_integer_const(inner_pairs.next().unwrap());
397
398            let inner_pair = inner_pairs
399                .next()
400                .expect("Missing: initial location / variable constraints (inits)");
401            debug_assert!(
402                inner_pair.as_rule() == Rule::boolean_expr_list,
403                "Got rule {:?} for {}",
404                inner_pair.as_rule(),
405                inner_pair.as_str(),
406            );
407            inner_pairs = inner_pair.into_inner();
408
409            for init_cond in inner_pairs {
410                let span = init_cond.as_span();
411                let var_cond: Result<BooleanExpression<Variable>, _> =
412                    parse_boolean_expr(init_cond.clone(), &builder, ctx);
413
414                if let Ok(var_cond) = var_cond {
415                    builder = builder
416                        .with_initial_variable_constraint(var_cond)
417                        .with_context(
418                            || "Failed to validate initial variable constraint (inits): ",
419                        )?;
420                    continue;
421                }
422
423                let loc_constraint: BooleanExpression<Location> =
424                    parse_boolean_expr(init_cond, &builder, ctx)
425                        .map_err(|err| {
426                            new_parsing_error(format!("Unknown identifier: {err}"), span)
427                        })
428                        .with_context(
429                            || "Failed to parse initial location / variable constraints (inits): ",
430                        )?;
431
432                builder = builder
433                    .with_initial_location_constraint(loc_constraint)
434                    .with_context(
435                        || "Failed to validate initial location / variable constraints (inits): ",
436                    )?;
437            }
438
439            pair = pairs
440                .next()
441                .expect("Missing: rules of the threshold automaton");
442        }
443
444        Ok((builder, pair))
445    }
446
447    /// Parse the list of rules and add them to the builder
448    fn parse_and_add_rules(
449        pair: Pair<'_, Rule>,
450        builder: InitializedGeneralThresholdAutomatonBuilder,
451        ctx: &ByMCParsingContext,
452    ) -> Result<InitializedGeneralThresholdAutomatonBuilder, anyhow::Error> {
453        debug_assert!(
454            pair.as_rule() == Rule::rule_list,
455            "Got rule {:?} for {}",
456            pair.as_rule(),
457            pair.as_str()
458        );
459
460        let mut pairs = pair.into_inner();
461
462        // integer specifying the number of rules, ignoring since it is usually invalid
463        let _n_rules = parse_integer_const(pairs.next().unwrap());
464
465        let rules = pairs
466            .map(|r| parse_rule(r, &builder, ctx))
467            .collect::<Result<Vec<_>, _>>()
468            .with_context(|| "Failed to parse rules: ")?;
469
470        builder
471            .with_rules(rules)
472            .with_context(|| "Failed to parse rules: ")
473    }
474
475    /// Parse specification list into ltl expressions
476    fn parse_specification_and_add_expressions<'a>(
477        pair: Pair<'_, Rule>,
478        mut builder: ELTLSpecificationBuilder<'a, GeneralThresholdAutomaton>,
479        ctx: &ByMCParsingContext,
480    ) -> Result<ELTLSpecificationBuilder<'a, GeneralThresholdAutomaton>, anyhow::Error> {
481        debug_assert!(
482            pair.as_rule() == Rule::specification_list,
483            "Got rule {:?} for {}",
484            pair.as_rule(),
485            pair.as_str()
486        );
487
488        let mut pairs = pair.into_inner();
489
490        // integer specifying the number of rules, ignoring since it is usually invalid
491        let _n_specs = parse_integer_const(pairs.next().unwrap());
492
493        let expressions = pairs
494            .map(|spec| parse_ltl_specification(spec, &builder, ctx))
495            .collect::<Result<Vec<_>, Error>>()
496            .with_context(|| "Failed to parse specifications: ")?;
497
498        builder
499            .add_expressions(expressions)
500            .with_context(|| "Specification failed validation: ")?;
501        Ok(builder)
502    }
503}
504
505/// Parse a single ltl specification
506///
507/// This function parses a single ltl specification and returns the name of the
508/// specification and the ltl expression.
509fn parse_ltl_specification<T>(
510    pair: Pair<'_, Rule>,
511    builder: &T,
512    ctx: &ByMCParsingContext,
513) -> Result<(String, ELTLExpression), Error>
514where
515    T: IsDeclared<Variable> + IsDeclared<Location> + IsDeclared<Parameter>,
516{
517    debug_assert!(
518        pair.as_rule() == Rule::specification,
519        "Expected a specification, got rule {:?} for {}",
520        pair.as_rule(),
521        pair.as_str()
522    );
523
524    let mut pairs = pair.into_inner();
525
526    let name: String = parse_identifier_to_t(&pairs.next().unwrap());
527
528    let expression = parse_ltl_expr(pairs.next().unwrap(), builder, ctx)?;
529
530    Ok((name, expression))
531}
532
533/// Parse an ltl expression into a single ltl expression
534///
535/// This function parses an ltl expression with operator precedence
536/// and returns the corresponding ltl expression.
537/// The function returns an error if the expression refers to an unknown location.
538fn parse_ltl_expr<T>(
539    pair: Pair<'_, Rule>,
540    builder: &T,
541    ctx: &ByMCParsingContext,
542) -> Result<ELTLExpression, Box<pest::error::Error<()>>>
543where
544    T: IsDeclared<Variable> + IsDeclared<Location> + IsDeclared<Parameter>,
545{
546    debug_assert!(
547        pair.as_rule() == Rule::ltl_expr,
548        "Expected an LTL expression, got rule {:?} for {}",
549        pair.as_rule(),
550        pair.as_str()
551    );
552
553    let pairs = pair.into_inner();
554    PRATT_PARSER
555        .map_primary(|atom| parse_ltl_atom(atom, builder, ctx))
556        .map_infix(|lhs, op, rhs| {
557            let lhs = lhs?;
558            let rhs = rhs?;
559
560            let op = match op.as_rule() {
561                Rule::and => ELTLExpression::And(Box::new(lhs), Box::new(rhs)),
562                Rule::or => ELTLExpression::Or(Box::new(lhs), Box::new(rhs)),
563                Rule::implication => ELTLExpression::Implies(Box::new(lhs), Box::new(rhs)),
564                _ => unreachable!(
565                    "Unknown rule for binary ltl operator {:?}: {}",
566                    op.as_rule(),
567                    op.as_str()
568                ),
569            };
570
571            Ok(op)
572        })
573        .map_prefix(|op, rhs| {
574            let rhs = rhs?;
575
576            match op.as_rule() {
577                Rule::not => Ok(ELTLExpression::Not(Box::new(rhs))),
578                Rule::globally => Ok(ELTLExpression::Globally(Box::new(rhs))),
579                Rule::eventually => Ok(ELTLExpression::Eventually(Box::new(rhs))),
580                _ => unreachable!(
581                    "Unknown rule for unary ltl operator {:?}: {}",
582                    op.as_rule(),
583                    op.as_str()
584                ),
585            }
586        })
587        .parse(pairs)
588}
589
590/// Parse an ltl atom into a single ltl expression
591///
592/// This function parses an ltl atom and returns the corresponding ltl expression.
593/// The function returns an error if the expression refers to an unknown location.
594fn parse_ltl_atom<T>(
595    pair: Pair<'_, Rule>,
596    builder: &T,
597    ctx: &ByMCParsingContext,
598) -> Result<ELTLExpression, Box<pest::error::Error<()>>>
599where
600    T: IsDeclared<Variable> + IsDeclared<Location> + IsDeclared<Parameter>,
601{
602    debug_assert!(
603        pair.as_rule() == Rule::ltl_atom,
604        "Expected an LTL atom, got rule {:?} for {}",
605        pair.as_rule(),
606        pair.as_str()
607    );
608
609    let mut pairs = pair.into_inner();
610    let pair = pairs.next().unwrap();
611
612    match pair.as_rule() {
613        Rule::ltl_expr => parse_ltl_expr(pair, builder, ctx),
614        Rule::ltl_unary_op => {
615            let op = pair.into_inner().next().unwrap();
616            let expr = pairs
617                .next()
618                .expect("Missing LTL expression after unary operator");
619            let expr = parse_ltl_atom(expr, builder, ctx)?;
620
621            match op.as_rule() {
622                Rule::not => Ok(ELTLExpression::Not(Box::new(expr))),
623                Rule::globally => Ok(ELTLExpression::Globally(Box::new(expr))),
624                Rule::eventually => Ok(ELTLExpression::Eventually(Box::new(expr))),
625                _ => unreachable!(
626                    "Unknown rule for unary operator {:?}: {}",
627                    op.as_rule(),
628                    op.as_str()
629                ),
630            }
631        }
632        Rule::comparison_expr => {
633            let span = pair.as_span();
634
635            // First: attempt to parse parameter expression !
636            // This is important as constraints purely on parameters are also
637            // valid for variable / location expressions
638            if let Ok((lhs, op, rhs)) =
639                parse_comparison_expr::<Parameter, T>(pair.clone(), builder, ctx)
640            {
641                return Ok(ELTLExpression::ParameterExpr(
642                    Box::new(lhs),
643                    op,
644                    Box::new(rhs),
645                ));
646            }
647
648            if let Ok((lhs, op, rhs)) =
649                parse_comparison_expr::<Variable, T>(pair.clone(), builder, ctx)
650            {
651                return Ok(ELTLExpression::VariableExpr(
652                    Box::new(lhs),
653                    op,
654                    Box::new(rhs),
655                ));
656            }
657
658            let (lhs, op, rhs) = parse_comparison_expr(pair, builder, ctx).map_err(|_err| {
659                new_parsing_error("Failed to parse inner ltl expression. This is most likely due to an unknown identifier".to_string(), span)
660            })?;
661            let expr = ELTLExpression::LocationExpr(Box::new(lhs), op, Box::new(rhs));
662            Ok(expr)
663        }
664        Rule::bool_const => {
665            let pair = pair.into_inner().next().unwrap();
666
667            match pair.as_rule() {
668                Rule::bool_true => Ok(ELTLExpression::True),
669                Rule::bool_false => Ok(ELTLExpression::False),
670                _ => unreachable!(
671                    "Unknown rule for boolean constant {:?}: {}",
672                    pair.as_rule(),
673                    pair.as_str()
674                ),
675            }
676        }
677        _ => unreachable!(
678            "Unknown rule for ltl atom {:?}: {}",
679            pair.as_rule(),
680            pair.as_str()
681        ),
682    }
683}
684
685/// Parse a location definition
686#[inline(always)]
687fn parse_location(pair: Pair<'_, Rule>) -> Location {
688    debug_assert!(
689        pair.as_rule() == Rule::location,
690        "Got rule {:?} for {}",
691        pair.as_rule(),
692        pair.as_str()
693    );
694
695    let id_pair = pair.into_inner().next().unwrap();
696
697    parse_identifier_to_t(&id_pair)
698
699    // ignoring integer(s) here, does not seem to have a semantic
700}
701
702/// Parse a list of location definitions
703fn parse_location_list(pair: Pair<'_, Rule>) -> Vec<Location> {
704    debug_assert!(
705        pair.as_rule() == Rule::location_list,
706        "Got rule {:?} for {}",
707        pair.as_rule(),
708        pair.as_str()
709    );
710
711    let mut pairs = pair.into_inner();
712
713    let n_locs = parse_integer_const(pairs.next().unwrap());
714
715    let locs = pairs.map(|loc| parse_location(loc)).collect::<Vec<_>>();
716
717    if n_locs != locs.len().try_into().unwrap() {
718        debug!(
719            "Specified number of locations {} does not match found number of locations {}",
720            n_locs,
721            locs.len()
722        )
723    }
724
725    locs
726}
727
728/// Parse an identifier into an object of type T
729#[inline(always)]
730fn parse_identifier_to_t<T: for<'a> From<&'a str>>(pair: &Pair<'_, Rule>) -> T {
731    debug_assert!(
732        pair.as_rule() == Rule::identifier,
733        "Got rule {:?} for {}",
734        pair.as_rule(),
735        pair.as_str()
736    );
737
738    T::from(pair.as_str())
739}
740
741/// Parse a list of identifiers into a vector of objects of type T
742#[inline(always)]
743fn parse_identifier_list_to_t<T: for<'a> From<&'a str>>(
744    pair: Pair<'_, Rule>,
745) -> impl Iterator<Item = T> {
746    debug_assert!(
747        pair.as_rule() == Rule::identifier_list,
748        "Got rule {:?} for {}",
749        pair.as_rule(),
750        pair.as_str()
751    );
752
753    pair.into_inner().map(|id| parse_identifier_to_t::<T>(&id))
754}
755
756/// Parse a reset expression into the corresponding list of actions
757fn parse_reset_expression(pair: Pair<'_, Rule>) -> Vec<Action> {
758    debug_assert!(
759        pair.as_rule() == Rule::reset_expr,
760        "Got rule {:?} for {}",
761        pair.as_rule(),
762        pair.as_str()
763    );
764
765    parse_identifier_list_to_t::<Variable>(pair.into_inner().next().unwrap())
766        .map(Action::new_reset)
767        .collect()
768}
769
770/// Parse an assignment expression of an action into the corresponding list of actions
771fn parse_assignment_expression<T>(
772    pair: Pair<'_, Rule>,
773    builder: &T,
774    ctx: &ByMCParsingContext,
775) -> Result<Action, Box<pest::error::Error<()>>>
776where
777    T: IsDeclared<Variable> + IsDeclared<Parameter>,
778{
779    debug_assert!(
780        pair.as_rule() == Rule::assignment_expr,
781        "Got rule {:?} for {}",
782        pair.as_rule(),
783        pair.as_str()
784    );
785    let span = pair.as_span();
786
787    let mut pairs = pair.into_inner();
788    let pair = pairs.next().unwrap();
789
790    let var = parse_identifier_to_t(&pair);
791    if !builder.is_declared(&var) {
792        return Err(new_parsing_error(
793            format!("Failed to parse action: Unknown identifier: {var}"),
794            span,
795        ));
796    }
797
798    let expr = parse_integer_expr(pairs.next().unwrap(), builder, ctx)
799        .map_err(|err| new_parsing_error(format!("Failed to parse action: {err}"), span))?;
800
801    Action::new(var, expr)
802        .map_err(|err| new_parsing_error(format!("Failed to parse effect of action: {err}"), span))
803}
804
805/// Parse an action expression into a list of actions
806fn parse_action_expr<T>(
807    pair: Pair<'_, Rule>,
808    builder: &T,
809    ctx: &ByMCParsingContext,
810) -> Result<Vec<Action>, Box<pest::error::Error<()>>>
811where
812    T: IsDeclared<Variable> + IsDeclared<Parameter>,
813{
814    debug_assert!(
815        pair.as_rule() == Rule::action_expr,
816        "Got rule {:?} for {}",
817        pair.as_rule(),
818        pair.as_str()
819    );
820
821    let pair = pair.into_inner().next().unwrap();
822
823    Ok(match pair.as_rule() {
824        Rule::unchanged_expr => vec![],
825        Rule::reset_expr => parse_reset_expression(pair),
826        Rule::assignment_expr => vec![parse_assignment_expression(pair, builder, ctx)?],
827        _ => unreachable!(
828            "Unknown rule for action expression {:?}: {}",
829            pair.as_rule(),
830            pair.as_str()
831        ),
832    })
833}
834
835/// Parse a list of action expressions into a combined list of actions
836#[inline(always)]
837fn parse_action_list<T>(
838    pair: Pair<'_, Rule>,
839    builder: &T,
840    ctx: &ByMCParsingContext,
841) -> Result<Vec<Action>, Box<pest::error::Error<()>>>
842where
843    T: IsDeclared<Variable> + IsDeclared<Parameter>,
844{
845    debug_assert!(
846        pair.as_rule() == Rule::action_list,
847        "Got rule {:?} for {}",
848        pair.as_rule(),
849        pair.as_str()
850    );
851
852    pair.into_inner()
853        .map(|action| parse_action_expr(action, builder, ctx))
854        .try_fold(vec![], |mut acc, x| {
855            acc.append(&mut x?);
856            Ok(acc)
857        })
858}
859
860/// Parse integer constant
861#[inline(always)]
862fn parse_integer_const(pair: Pair<'_, Rule>) -> u32 {
863    debug_assert!(
864        pair.as_rule() == Rule::integer_const,
865        "Got rule {:?} for {}",
866        pair.as_rule(),
867        pair.as_str()
868    );
869    pair.as_str().parse::<u32>().unwrap()
870}
871
872/// Parse an integer operator
873#[inline(always)]
874fn parse_integer_binary_op(pair: Pair<'_, Rule>) -> IntegerOp {
875    match pair.as_rule() {
876        Rule::add => IntegerOp::Add,
877        Rule::sub => IntegerOp::Sub,
878        Rule::mul => IntegerOp::Mul,
879        Rule::div => IntegerOp::Div,
880        _ => unreachable!(
881            "Unknown rule for operator {:?}: {}",
882            pair.as_rule(),
883            pair.as_str()
884        ),
885    }
886}
887
888/// Parse integer atom
889///
890/// Returns an integer expression if the pair is a constant, known identifier,
891/// or  could be parsed to an expression
892/// Returns an error if the identifier was not declared with the identifier name
893fn parse_integer_atom<T, U>(
894    pair: Pair<'_, Rule>,
895    builder: &U,
896    ctx: &ByMCParsingContext,
897) -> Result<IntegerExpression<T>, String>
898where
899    T: Atomic,
900    U: IsDeclared<T> + IsDeclared<Parameter>,
901{
902    debug_assert!(
903        pair.as_rule() == Rule::integer_atom,
904        "Got rule {:?} for {}",
905        pair.as_rule(),
906        pair.as_str()
907    );
908
909    let pair = pair.into_inner().next().unwrap();
910
911    match pair.as_rule() {
912        Rule::integer_const => Ok(IntegerExpression::Const(parse_integer_const(pair))),
913        Rule::identifier => {
914            let ident: String = parse_identifier_to_t(&pair);
915            if ctx.define_macro.contains_key(&ident) {
916                return parse_integer_expr(ctx.define_macro[&ident].clone(), builder, ctx);
917            }
918
919            let atom = parse_identifier_to_t(&pair);
920            if builder.is_declared(&atom) {
921                return Ok(IntegerExpression::Atom(atom));
922            }
923
924            let param = parse_identifier_to_t(&pair);
925            if builder.is_declared(&param) {
926                return Ok(IntegerExpression::Param(param));
927            }
928
929            Err(format!("Unknown identifier: {}", pair.as_str()))
930        }
931        Rule::integer_expr => parse_integer_expr(pair, builder, ctx),
932        _ => unreachable!(
933            "Unknown integer atom {:#?} : {}",
934            pair.as_rule(),
935            pair.as_str()
936        ),
937    }
938}
939
940/// Parse expression over integers into an integer expression
941fn parse_integer_expr<T, U>(
942    pair: Pair<'_, Rule>,
943    builder: &U,
944    ctx: &ByMCParsingContext,
945) -> Result<IntegerExpression<T>, String>
946where
947    T: Atomic,
948    U: IsDeclared<T> + IsDeclared<Parameter>,
949{
950    debug_assert!(
951        pair.as_rule() == Rule::integer_expr,
952        "Got rule {:?} for {}",
953        pair.as_rule(),
954        pair.as_str()
955    );
956    let pairs = pair.into_inner();
957
958    PRATT_PARSER
959        .map_primary(|atom| parse_integer_atom(atom, builder, ctx))
960        .map_infix(|lhs, op, rhs| {
961            let op = parse_integer_binary_op(op);
962
963            Ok(IntegerExpression::BinaryExpr(
964                Box::new(lhs?),
965                op,
966                Box::new(rhs?),
967            ))
968        })
969        .map_prefix(|op, rhs| match op.as_rule() {
970            Rule::negation => Ok(IntegerExpression::Neg(Box::new(rhs?))),
971            _ => unreachable!(
972                "Unknown integer unary operator {:?}: {}",
973                op.as_rule(),
974                op.as_str()
975            ),
976        })
977        .parse(pairs)
978}
979
980/// Parse boolean constant
981#[inline(always)]
982fn parse_boolean_const<T: Atomic>(pair: Pair<'_, Rule>) -> BooleanExpression<T> {
983    debug_assert!(
984        pair.as_rule() == Rule::bool_const,
985        "Got rule {:?} for {}",
986        pair.as_rule(),
987        pair.as_str()
988    );
989
990    let pair = pair
991        .into_inner()
992        .next()
993        .expect("Expected boolean constant to be non-empty");
994
995    match pair.as_rule() {
996        Rule::bool_true => BooleanExpression::True,
997        Rule::bool_false => BooleanExpression::False,
998        _ => unreachable!(
999            "Unexpected rule for boolean constant {:?}: {}",
1000            pair.as_rule(),
1001            pair.as_str()
1002        ),
1003    }
1004}
1005
1006/// Parse boolean connectives
1007#[inline(always)]
1008fn parse_boolean_con(pair: Pair<'_, Rule>) -> BooleanConnective {
1009    match pair.as_rule() {
1010        Rule::and => BooleanConnective::And,
1011        Rule::or => BooleanConnective::Or,
1012        _ => unreachable!(
1013            "Unknown rule for boolean connective {:?}: {}",
1014            pair.as_rule(),
1015            pair.as_str()
1016        ),
1017    }
1018}
1019
1020/// Parse comparison operator
1021#[inline(always)]
1022fn parse_comparison_op(pair: Pair<'_, Rule>) -> ComparisonOp {
1023    match pair.as_rule() {
1024        Rule::equal => ComparisonOp::Eq,
1025        Rule::n_equal => ComparisonOp::Neq,
1026        Rule::less_eq => ComparisonOp::Leq,
1027        Rule::less => ComparisonOp::Lt,
1028        Rule::greater_eq => ComparisonOp::Geq,
1029        Rule::greater => ComparisonOp::Gt,
1030        _ => unreachable!(
1031            "Unknown rule for comparison operator {:?}: {}",
1032            pair.as_rule(),
1033            pair.as_str()
1034        ),
1035    }
1036}
1037
1038/// Intermediate type for comparison expression of the form `lhs op rhs`
1039type CompExpr<T> = (IntegerExpression<T>, ComparisonOp, IntegerExpression<T>);
1040
1041/// Parse comparison expression, relating two integer expressions
1042fn parse_comparison_expr<T, U>(
1043    pair: Pair<'_, Rule>,
1044    builder: &U,
1045    ctx: &ByMCParsingContext,
1046) -> Result<CompExpr<T>, String>
1047where
1048    T: Atomic,
1049    U: IsDeclared<T> + IsDeclared<Parameter>,
1050{
1051    debug_assert!(
1052        pair.as_rule() == Rule::comparison_expr,
1053        "Got rule {:?} for {}",
1054        pair.as_rule(),
1055        pair.as_str()
1056    );
1057
1058    let mut pairs = pair.into_inner();
1059
1060    let lhs = parse_integer_expr(pairs.next().unwrap(), builder, ctx)?;
1061    let op = parse_comparison_op(pairs.next().unwrap());
1062    let rhs = parse_integer_expr(pairs.next().unwrap(), builder, ctx)?;
1063
1064    Ok((lhs, op, rhs))
1065}
1066
1067/// Parse a constraint from a boolean expression
1068fn parse_boolean_expr<T, U>(
1069    pair: Pair<'_, Rule>,
1070    builder: &U,
1071    ctx: &ByMCParsingContext,
1072) -> Result<BooleanExpression<T>, String>
1073where
1074    T: Atomic,
1075    U: IsDeclared<T> + IsDeclared<Parameter>,
1076{
1077    debug_assert!(
1078        pair.as_rule() == Rule::boolean_expr,
1079        "Got rule {:?} for {}",
1080        pair.as_rule(),
1081        pair.as_str()
1082    );
1083
1084    let pairs = pair.into_inner();
1085
1086    // utilize the precedence parser
1087    PRATT_PARSER
1088        .map_primary(|atom| parse_boolean_atom(atom, builder, ctx))
1089        .map_infix(|lhs, op, rhs| {
1090            let op = parse_boolean_con(op);
1091
1092            Ok(BooleanExpression::BinaryExpression(
1093                Box::new(lhs?),
1094                op,
1095                Box::new(rhs?),
1096            ))
1097        })
1098        .map_prefix(|op, rhs| match op.as_rule() {
1099            Rule::not => Ok(BooleanExpression::Not(Box::new(rhs?))),
1100            _ => unreachable!(
1101                "Unknown boolean unary operator {:?}: {}",
1102                op.as_rule(),
1103                op.as_str()
1104            ),
1105        })
1106        .parse(pairs)
1107}
1108
1109/// Parse boolean_atom
1110#[inline(always)]
1111fn parse_boolean_atom<T, U>(
1112    pair: Pair<'_, Rule>,
1113    builder: &U,
1114    ctx: &ByMCParsingContext,
1115) -> Result<BooleanExpression<T>, String>
1116where
1117    T: Atomic,
1118    U: IsDeclared<T> + IsDeclared<Parameter>,
1119{
1120    debug_assert!(
1121        pair.as_rule() == Rule::boolean_atom,
1122        "Got rule {:?} for {}",
1123        pair.as_rule(),
1124        pair.as_str()
1125    );
1126
1127    let pair = pair
1128        .into_inner()
1129        .next()
1130        .expect("Expected boolean atom to be non-empty");
1131
1132    match pair.as_rule() {
1133        Rule::bool_const => Ok(parse_boolean_const(pair)),
1134        Rule::boolean_expr => parse_boolean_expr(pair, builder, ctx),
1135        Rule::comparison_expr => {
1136            let (lhs, op, rhs) = parse_comparison_expr(pair, builder, ctx)?;
1137            Ok(BooleanExpression::ComparisonExpression(
1138                Box::new(lhs),
1139                op,
1140                Box::new(rhs),
1141            ))
1142        }
1143        _ => unreachable!(
1144            "Unknown rule for boolean atom {:?}: {}",
1145            pair.as_rule(),
1146            pair.as_str(),
1147        ),
1148    }
1149}
1150
1151/// Parse list of boolean expressions
1152#[inline(always)]
1153fn parse_boolean_expr_list<T, U>(
1154    pair: Pair<'_, Rule>,
1155    builder: &U,
1156    ctx: &ByMCParsingContext,
1157) -> Result<Vec<BooleanExpression<T>>, Box<pest::error::Error<()>>>
1158where
1159    T: Atomic,
1160    U: IsDeclared<T> + IsDeclared<Parameter>,
1161{
1162    debug_assert!(
1163        pair.as_rule() == Rule::boolean_expr_list,
1164        "Got rule {:?} for {}",
1165        pair.as_rule(),
1166        pair.as_str()
1167    );
1168
1169    pair.into_inner()
1170        .map(|expr| {
1171            let span = expr.as_span();
1172
1173            parse_boolean_expr(expr, builder, ctx).map_err(|err| new_parsing_error(err, span))
1174        })
1175        .collect()
1176}
1177
1178/// Parse a rule
1179fn parse_rule<T>(
1180    pair: Pair<'_, Rule>,
1181    builder: &T,
1182    ctx: &ByMCParsingContext,
1183) -> Result<taco_threshold_automaton::general_threshold_automaton::Rule, Box<pest::error::Error<()>>>
1184where
1185    T: IsDeclared<Variable> + IsDeclared<Parameter> + IsDeclared<Location>,
1186{
1187    debug_assert!(
1188        pair.as_rule() == Rule::rule,
1189        "Got rule {:?} for {}",
1190        pair.as_rule(),
1191        pair.as_str()
1192    );
1193
1194    let mut pairs = pair.into_inner();
1195
1196    let id = parse_integer_const(pairs.next().unwrap());
1197
1198    let pair = pairs.next().unwrap();
1199    let source: Location = parse_identifier_to_t(&pair);
1200
1201    let pair = pairs.next().unwrap();
1202    let target: Location = parse_identifier_to_t(&pair);
1203
1204    let mut rule_builder = RuleBuilder::new(id, source, target);
1205
1206    let pair = pairs.next().unwrap();
1207    let span = pair.as_span();
1208
1209    let guard = parse_boolean_expr(pair, builder, ctx).map_err(|err| {
1210        new_parsing_error(format!("Failed to parse guard of rule {id}: {err}"), span)
1211    })?;
1212
1213    rule_builder = rule_builder.with_guard(guard);
1214
1215    let actions = parse_action_list(pairs.next().unwrap(), builder, ctx)?;
1216    rule_builder = rule_builder.with_actions(actions);
1217
1218    Ok(rule_builder.build())
1219}
1220
1221/// Generate a new parsing error
1222#[inline(always)]
1223fn new_parsing_error(message: String, span: Span<'_>) -> Box<pest::error::Error<()>> {
1224    Box::new(error::Error::new_from_span(
1225        error::ErrorVariant::CustomError { message },
1226        span,
1227    ))
1228}
1229
1230#[cfg(test)]
1231mod test {
1232    use super::*;
1233
1234    // These tests do test private functions that are not exposed to a user, but they have been useful for debugging
1235    // and are kept for now.
1236    mod simple_parse_funcs {
1237        use super::*;
1238
1239        macro_rules! parse_func_test
1240         {
1241            ($name:ident, $($test_spec:expr, $expected_out:expr, $rule:expr, $parse_func:expr),+) => {
1242                #[test]
1243                fn $name() {
1244                    $(
1245                        let test_spec = $test_spec;
1246                        let mut parsed_pairs = PestByMCParser::parse($rule, test_spec).unwrap();
1247                        let exp_pair = parsed_pairs.next().unwrap();
1248                        let ctx = ByMCParsingContext::new();
1249
1250                        let builder = GeneralThresholdAutomatonBuilder::new("test_ta")
1251                                        .with_parameters(vec![Parameter::new("n"), Parameter::new("f")])
1252                                        .unwrap()
1253                                        .with_variables(vec![Variable::new("x"), Variable::new("y"), Variable::new("var1"), Variable::new("var2"), Variable::new("var3")])
1254                                        .unwrap()
1255                                        .with_locations(vec![Location::new("loc"), Location::new("loc1"), Location::new("loc2")])
1256                                        .unwrap()
1257                                        .initialize();
1258
1259                        let got_expr = $parse_func(exp_pair, &builder, &ctx);
1260                        let got_expr = got_expr.unwrap();
1261
1262                        assert_eq!(got_expr, $expected_out);
1263
1264                        assert!(parsed_pairs.next().is_none(), "Found more tokens: {:#?}", parsed_pairs);
1265                    )*
1266                }
1267
1268            };
1269        }
1270
1271        #[test]
1272        fn test_parse_identifier_list_to_string() {
1273            let test_spec = "a, b, c, abcdefg, gg, __gg, gg32";
1274            let mut parsed_pairs = PestByMCParser::parse(Rule::identifier_list, test_spec).unwrap();
1275            let pair = parsed_pairs.next().unwrap();
1276
1277            let got_expr: Vec<String> = parse_identifier_list_to_t(pair).collect();
1278
1279            let expected_expr = vec![
1280                "a".to_string(),
1281                "b".to_string(),
1282                "c".to_string(),
1283                "abcdefg".to_string(),
1284                "gg".to_string(),
1285                "__gg".to_string(),
1286                "gg32".to_string(),
1287            ];
1288
1289            assert_eq!(got_expr, expected_expr);
1290
1291            assert!(
1292                parsed_pairs.next().is_none(),
1293                "Found more tokens: {parsed_pairs:#?}"
1294            );
1295        }
1296
1297        #[test]
1298        fn parse_location_list_test() {
1299            let test_spec = "locations (3) {
1300                loc1 : [0];
1301                loc2 : [1];
1302                loc3 : [2];
1303            }
1304            ";
1305
1306            let expected_locs = vec![
1307                Location::new("loc1"),
1308                Location::new("loc2"),
1309                Location::new("loc3"),
1310            ];
1311
1312            print!(
1313                "{:#?}",
1314                PestByMCParser::parse(Rule::location_list, test_spec).err()
1315            );
1316
1317            let mut parsed_pairs = PestByMCParser::parse(Rule::location_list, test_spec).unwrap();
1318            let pair = parsed_pairs.next().unwrap();
1319
1320            let got_locs = parse_location_list(pair);
1321
1322            assert_eq!(expected_locs, got_locs);
1323
1324            assert!(
1325                parsed_pairs.next().is_none(),
1326                "Found more tokens: {parsed_pairs:#?}"
1327            );
1328        }
1329
1330        parse_func_test!(
1331            parse_action_expr_reset,
1332            "reset(x, y, z)",
1333            vec![
1334                Action::new_reset(Variable::new("x")),
1335                Action::new_reset(Variable::new("y")),
1336                Action::new_reset(Variable::new("z")),
1337            ],
1338            Rule::action_expr,
1339            parse_action_expr
1340        );
1341
1342        parse_func_test!(
1343            parse_action_expr_increment,
1344            "x' := x + 1",
1345            vec![
1346                Action::new(
1347                    Variable::new("x"),
1348                    IntegerExpression::Atom(Variable::new("x")) + IntegerExpression::Const(1),
1349                )
1350                .unwrap()
1351            ],
1352            Rule::action_expr,
1353            parse_action_expr
1354        );
1355
1356        parse_func_test!(
1357            parse_action_expr_unchanged,
1358            "unchanged(x, y, z)",
1359            Vec::<Action>::new(),
1360            Rule::action_expr,
1361            parse_action_expr
1362        );
1363
1364        parse_func_test!(
1365            parse_action_list_mixed,
1366            "reset(a,b,c); x' := x + 1, unchanged(p,q)",
1367            vec![
1368                Action::new_reset(Variable::new("a")),
1369                Action::new_reset(Variable::new("b")),
1370                Action::new_reset(Variable::new("c")),
1371                Action::new(
1372                    Variable::new("x"),
1373                    IntegerExpression::Atom(Variable::new("x")) + IntegerExpression::Const(1),
1374                )
1375                .unwrap(),
1376            ],
1377            Rule::action_list,
1378            parse_action_list
1379        );
1380
1381        parse_func_test!(
1382            parse_integer_expr_const,
1383            "5",
1384            IntegerExpression::<Location>::Const(5),
1385            Rule::integer_expr,
1386            parse_integer_expr
1387        );
1388
1389        parse_func_test!(
1390            parse_integer_expr_location,
1391            "loc",
1392            IntegerExpression::<Location>::Atom(Location::new("loc")),
1393            Rule::integer_expr,
1394            parse_integer_expr
1395        );
1396
1397        parse_func_test!(
1398            parse_integer_expr_parameter,
1399            "n",
1400            IntegerExpression::<Location>::Param(Parameter::new("n")),
1401            Rule::integer_expr,
1402            parse_integer_expr
1403        );
1404
1405        parse_func_test!(
1406            parse_integer_expr_add,
1407            "5 + 5",
1408            IntegerExpression::<Location>::BinaryExpr(
1409                Box::new(IntegerExpression::Const(5)),
1410                IntegerOp::Add,
1411                Box::new(IntegerExpression::Const(5)),
1412            ),
1413            Rule::integer_expr,
1414            parse_integer_expr
1415        );
1416
1417        parse_func_test!(
1418            parse_integer_operator_precedence_1,
1419            "5 + 5 * 5",
1420            IntegerExpression::<Parameter>::BinaryExpr(
1421                Box::new(IntegerExpression::Const(5)),
1422                IntegerOp::Add,
1423                Box::new(IntegerExpression::BinaryExpr(
1424                    Box::new(IntegerExpression::Const(5)),
1425                    IntegerOp::Mul,
1426                    Box::new(IntegerExpression::Const(5)),
1427                )),
1428            ),
1429            Rule::integer_expr,
1430            parse_integer_expr
1431        );
1432
1433        parse_func_test!(
1434            parse_integer_operator_precedence_2,
1435            "5 / 5 - 5",
1436            IntegerExpression::<Variable>::BinaryExpr(
1437                Box::new(IntegerExpression::BinaryExpr(
1438                    Box::new(IntegerExpression::Const(5)),
1439                    IntegerOp::Div,
1440                    Box::new(IntegerExpression::Const(5)),
1441                )),
1442                IntegerOp::Sub,
1443                Box::new(IntegerExpression::Const(5)),
1444            ),
1445            Rule::integer_expr,
1446            parse_integer_expr
1447        );
1448
1449        parse_func_test!(
1450            parse_integer_un_op,
1451            "-3",
1452            IntegerExpression::<Location>::Neg(Box::new(IntegerExpression::Const(3))),
1453            Rule::integer_expr,
1454            parse_integer_expr
1455        );
1456
1457        parse_func_test!(
1458            parse_integer_mixed,
1459            "-3 + n - loc",
1460            IntegerExpression::BinaryExpr(
1461                Box::new(IntegerExpression::BinaryExpr(
1462                    Box::new(IntegerExpression::<Location>::Neg(Box::new(
1463                        IntegerExpression::Const(3)
1464                    ))),
1465                    IntegerOp::Add,
1466                    Box::new(IntegerExpression::Param(Parameter::new("n")))
1467                )),
1468                IntegerOp::Sub,
1469                Box::new(IntegerExpression::Atom(Location::new("loc")))
1470            ),
1471            Rule::integer_expr,
1472            parse_integer_expr
1473        );
1474
1475        parse_func_test!(
1476            parse_boolean_const_true,
1477            "true",
1478            BooleanExpression::<Location>::True,
1479            Rule::boolean_expr,
1480            parse_boolean_expr
1481        );
1482
1483        parse_func_test!(
1484            parse_boolean_const_true1,
1485            "1",
1486            BooleanExpression::<Location>::True,
1487            Rule::boolean_expr,
1488            parse_boolean_expr
1489        );
1490
1491        parse_func_test!(
1492            parse_boolean_const_false,
1493            "false",
1494            BooleanExpression::<Location>::False,
1495            Rule::boolean_expr,
1496            parse_boolean_expr
1497        );
1498
1499        parse_func_test!(
1500            parse_boolean_comp_op_1,
1501            "x > 1",
1502            BooleanExpression::ComparisonExpression(
1503                Box::new(IntegerExpression::Atom(Variable::new("x"))),
1504                ComparisonOp::Gt,
1505                Box::new(IntegerExpression::Const(1)),
1506            ),
1507            Rule::boolean_expr,
1508            parse_boolean_expr
1509        );
1510
1511        parse_func_test!(
1512            parse_boolean_comp_op_2,
1513            "x <= 1",
1514            BooleanExpression::ComparisonExpression(
1515                Box::new(IntegerExpression::Atom(Variable::new("x"))),
1516                ComparisonOp::Leq,
1517                Box::new(IntegerExpression::Const(1)),
1518            ),
1519            Rule::boolean_expr,
1520            parse_boolean_expr
1521        );
1522
1523        parse_func_test!(
1524            parse_boolean_comp_op_negated,
1525            "!(x > 1)",
1526            BooleanExpression::Not(Box::new(BooleanExpression::ComparisonExpression(
1527                Box::new(IntegerExpression::Atom(Variable::new("x"))),
1528                ComparisonOp::Gt,
1529                Box::new(IntegerExpression::Const(1)),
1530            ))),
1531            Rule::boolean_expr,
1532            parse_boolean_expr
1533        );
1534
1535        parse_func_test!(
1536            parse_boolean_comp_op_complex,
1537            "var2 >=  1 && var2 < 1 || var3 != n",
1538            BooleanExpression::BinaryExpression(
1539                Box::new(BooleanExpression::BinaryExpression(
1540                    Box::new(BooleanExpression::ComparisonExpression(
1541                        Box::new(IntegerExpression::Atom(Variable::new("var2"))),
1542                        ComparisonOp::Geq,
1543                        Box::new(IntegerExpression::Const(1)),
1544                    )),
1545                    BooleanConnective::And,
1546                    Box::new(BooleanExpression::ComparisonExpression(
1547                        Box::new(IntegerExpression::Atom(Variable::new("var2"))),
1548                        ComparisonOp::Lt,
1549                        Box::new(IntegerExpression::Const(1)),
1550                    ))
1551                )),
1552                BooleanConnective::Or,
1553                Box::new(BooleanExpression::ComparisonExpression(
1554                    Box::new(IntegerExpression::Atom(Variable::new("var3"))),
1555                    ComparisonOp::Neq,
1556                    Box::new(IntegerExpression::Param(Parameter::new("n"))),
1557                ))
1558            ),
1559            Rule::boolean_expr,
1560            parse_boolean_expr
1561        );
1562
1563        parse_func_test!(
1564            parse_ltl_expr_simple_globally,
1565            "[](loc1 == 0 -> loc2 == 1)",
1566            ELTLExpression::Globally(Box::new(ELTLExpression::Implies(
1567                Box::new(ELTLExpression::LocationExpr(
1568                    Box::new(IntegerExpression::Atom(Location::new("loc1"))),
1569                    ComparisonOp::Eq,
1570                    Box::new(IntegerExpression::Const(0))
1571                )),
1572                Box::new(ELTLExpression::LocationExpr(
1573                    Box::new(IntegerExpression::Atom(Location::new("loc2"))),
1574                    ComparisonOp::Eq,
1575                    Box::new(IntegerExpression::Const(1))
1576                )),
1577            ))),
1578            Rule::ltl_expr,
1579            parse_ltl_expr
1580        );
1581
1582        parse_func_test!(
1583            parse_ltl_expr_simple_const,
1584            "0 == 0",
1585            ELTLExpression::ParameterExpr(
1586                Box::new(IntegerExpression::Const(0)),
1587                ComparisonOp::Eq,
1588                Box::new(IntegerExpression::Const(0))
1589            ),
1590            Rule::ltl_expr,
1591            parse_ltl_expr
1592        );
1593
1594        parse_func_test!(
1595            parse_ltl_expr_simple_true,
1596            "true",
1597            ELTLExpression::True,
1598            Rule::ltl_expr,
1599            parse_ltl_expr
1600        );
1601
1602        parse_func_test!(
1603            parse_ltl_expr_simple_false,
1604            "false",
1605            ELTLExpression::False,
1606            Rule::ltl_expr,
1607            parse_ltl_expr
1608        );
1609
1610        parse_func_test!(
1611            parse_ltl_expr_adv_globally,
1612            "[](loc1 == 0 -> loc2 == 1 + 3)",
1613            ELTLExpression::Globally(Box::new(ELTLExpression::Implies(
1614                Box::new(ELTLExpression::LocationExpr(
1615                    Box::new(IntegerExpression::Atom(Location::new("loc1"))),
1616                    ComparisonOp::Eq,
1617                    Box::new(IntegerExpression::Const(0))
1618                )),
1619                Box::new(ELTLExpression::LocationExpr(
1620                    Box::new(IntegerExpression::Atom(Location::new("loc2"))),
1621                    ComparisonOp::Eq,
1622                    Box::new(IntegerExpression::Const(1) + IntegerExpression::Const(3))
1623                )),
1624            ))),
1625            Rule::ltl_expr,
1626            parse_ltl_expr
1627        );
1628
1629        parse_func_test!(
1630            parse_ltl_expr_simple_eventually,
1631            "<>(loc1 == n -> !loc2 == 1)",
1632            ELTLExpression::Eventually(Box::new(ELTLExpression::Implies(
1633                Box::new(ELTLExpression::LocationExpr(
1634                    Box::new(IntegerExpression::Atom(Location::new("loc1"))),
1635                    ComparisonOp::Eq,
1636                    Box::new(IntegerExpression::Param(Parameter::new("n")))
1637                )),
1638                Box::new(ELTLExpression::Not(Box::new(ELTLExpression::LocationExpr(
1639                    Box::new(IntegerExpression::Atom(Location::new("loc2"))),
1640                    ComparisonOp::Eq,
1641                    Box::new(IntegerExpression::Const(1))
1642                )))),
1643            ))),
1644            Rule::ltl_expr,
1645            parse_ltl_expr
1646        );
1647
1648        parse_func_test!(
1649            parse_ltl_expr_simple_and,
1650            "[](loc1 == 0 -> loc2 == 1) && <>(loc1 == n -> !loc2 == 1)",
1651            ELTLExpression::And(
1652                Box::new(ELTLExpression::Globally(Box::new(ELTLExpression::Implies(
1653                    Box::new(ELTLExpression::LocationExpr(
1654                        Box::new(IntegerExpression::Atom(Location::new("loc1"))),
1655                        ComparisonOp::Eq,
1656                        Box::new(IntegerExpression::Const(0))
1657                    )),
1658                    Box::new(ELTLExpression::LocationExpr(
1659                        Box::new(IntegerExpression::Atom(Location::new("loc2"))),
1660                        ComparisonOp::Eq,
1661                        Box::new(IntegerExpression::Const(1))
1662                    )),
1663                )))),
1664                Box::new(ELTLExpression::Eventually(Box::new(
1665                    ELTLExpression::Implies(
1666                        Box::new(ELTLExpression::LocationExpr(
1667                            Box::new(IntegerExpression::Atom(Location::new("loc1"))),
1668                            ComparisonOp::Eq,
1669                            Box::new(IntegerExpression::Param(Parameter::new("n")))
1670                        )),
1671                        Box::new(ELTLExpression::Not(Box::new(ELTLExpression::LocationExpr(
1672                            Box::new(IntegerExpression::Atom(Location::new("loc2"))),
1673                            ComparisonOp::Eq,
1674                            Box::new(IntegerExpression::Const(1))
1675                        )))),
1676                    )
1677                )))
1678            ),
1679            Rule::ltl_expr,
1680            parse_ltl_expr
1681        );
1682
1683        parse_func_test!(
1684            parse_ltl_expr_simple_or,
1685            "[](loc1 == 0 -> loc2 == 1) || <>(loc1 == n -> !loc2 == 1)",
1686            ELTLExpression::Or(
1687                Box::new(ELTLExpression::Globally(Box::new(ELTLExpression::Implies(
1688                    Box::new(ELTLExpression::LocationExpr(
1689                        Box::new(IntegerExpression::Atom(Location::new("loc1"))),
1690                        ComparisonOp::Eq,
1691                        Box::new(IntegerExpression::Const(0))
1692                    )),
1693                    Box::new(ELTLExpression::LocationExpr(
1694                        Box::new(IntegerExpression::Atom(Location::new("loc2"))),
1695                        ComparisonOp::Eq,
1696                        Box::new(IntegerExpression::Const(1))
1697                    )),
1698                )))),
1699                Box::new(ELTLExpression::Eventually(Box::new(
1700                    ELTLExpression::Implies(
1701                        Box::new(ELTLExpression::LocationExpr(
1702                            Box::new(IntegerExpression::Atom(Location::new("loc1"))),
1703                            ComparisonOp::Eq,
1704                            Box::new(IntegerExpression::Param(Parameter::new("n")))
1705                        )),
1706                        Box::new(ELTLExpression::Not(Box::new(ELTLExpression::LocationExpr(
1707                            Box::new(IntegerExpression::Atom(Location::new("loc2"))),
1708                            ComparisonOp::Eq,
1709                            Box::new(IntegerExpression::Const(1))
1710                        )))),
1711                    )
1712                )))
1713            ),
1714            Rule::ltl_expr,
1715            parse_ltl_expr
1716        );
1717
1718        // Check that parameter constraints are parsed as parameter expressions
1719        parse_func_test!(
1720            parse_ltl_expr_param_as_variable_expr,
1721            "n == 0",
1722            ELTLExpression::ParameterExpr(
1723                Box::new(IntegerExpression::Atom(Parameter::new("n"))),
1724                ComparisonOp::Eq,
1725                Box::new(IntegerExpression::Const(0))
1726            ),
1727            Rule::ltl_expr,
1728            parse_ltl_expr
1729        );
1730    }
1731
1732    mod full_spec {
1733        use taco_threshold_automaton::{
1734            BooleanVarConstraint, LocationConstraint, ParameterConstraint,
1735        };
1736
1737        use super::*;
1738
1739        #[test]
1740        fn test_parse_skeleton_spec() {
1741            let test_spec = "
1742            skel Proc {
1743                parameters n;
1744
1745                assumptions (1) {
1746                    n >= 0;
1747                }
1748
1749                locations (2) {
1750                }
1751
1752                inits (3) {
1753                }
1754
1755                rules (4) {
1756                }
1757
1758                specifications (0) {
1759                }
1760            }
1761            ";
1762
1763            let expected_ta = GeneralThresholdAutomatonBuilder::new("Proc")
1764                .with_parameter(Parameter::new("n"))
1765                .unwrap()
1766                .initialize()
1767                .with_resilience_condition(BooleanExpression::ComparisonExpression(
1768                    Box::new(IntegerExpression::Param(Parameter::new("n"))),
1769                    ComparisonOp::Geq,
1770                    Box::new(IntegerExpression::Const(0)),
1771                ))
1772                .unwrap()
1773                .build();
1774
1775            let parser = ByMCParser::new();
1776            let (got_ta, got_spec) = parser.parse_ta_and_spec(test_spec).unwrap();
1777
1778            assert_eq!(got_ta, expected_ta);
1779
1780            let expected_spec = ELTLSpecificationBuilder::new(&got_ta).build();
1781
1782            assert_eq!(got_spec, expected_spec);
1783        }
1784
1785        #[test]
1786        fn test_parse_ta_1() {
1787            let test_spec = "
1788            skel test_ta1 {
1789                shared var1, var2, var3;
1790                parameters n, t, f;
1791                
1792                assumptions (1) {
1793                    n > 3 * f;
1794                }
1795
1796                locations (2) {
1797                    loc1 : [0];
1798                    loc2 : [1];
1799                    loc3 : [2];
1800                }
1801
1802                inits (1) {
1803                    loc1 == n - f  || loc2 == 0;
1804                    var1 == 0;
1805                    var2 == 0;
1806                    var3 == 0;
1807                }
1808
1809                rules (4) {
1810                    0: loc1 -> loc2
1811                        when(true)
1812                        do {};
1813                    1: loc2 -> loc3
1814                        when( var1 == 1 && var2 == n)
1815                        do { reset(var3); var1' == var1 + 1  };
1816                }
1817
1818                specifications (1) {
1819                }
1820            }
1821            ";
1822
1823            let expected_ta = GeneralThresholdAutomatonBuilder::new("test_ta1")
1824                .with_parameters(vec![
1825                    Parameter::new("n"),
1826                    Parameter::new("t"),
1827                    Parameter::new("f"),
1828                ])
1829                .unwrap()
1830                .with_variables(vec![
1831                    Variable::new("var1"),
1832                    Variable::new("var2"),
1833                    Variable::new("var3"),
1834                ])
1835                .unwrap()
1836                .with_locations(vec![
1837                    Location::new("loc1"),
1838                    Location::new("loc2"),
1839                    Location::new("loc3"),
1840                ])
1841                .unwrap()
1842                .initialize()
1843                .with_rules(vec![
1844                    RuleBuilder::new(0, Location::new("loc1"), Location::new("loc2")).build(),
1845                    RuleBuilder::new(1, Location::new("loc2"), Location::new("loc3"))
1846                        .with_guard(BooleanExpression::BinaryExpression(
1847                            Box::new(BooleanVarConstraint::ComparisonExpression(
1848                                Box::new(IntegerExpression::Atom(Variable::new("var1"))),
1849                                ComparisonOp::Eq,
1850                                Box::new(IntegerExpression::Const(1)),
1851                            )),
1852                            BooleanConnective::And,
1853                            Box::new(BooleanVarConstraint::ComparisonExpression(
1854                                Box::new(IntegerExpression::Atom(Variable::new("var2"))),
1855                                ComparisonOp::Eq,
1856                                Box::new(IntegerExpression::Param(Parameter::new("n"))),
1857                            )),
1858                        ))
1859                        .with_action(Action::new_reset(Variable::new("var3")))
1860                        .with_action(
1861                            Action::new(
1862                                Variable::new("var1"),
1863                                IntegerExpression::Atom(Variable::new("var1"))
1864                                    + IntegerExpression::Const(1),
1865                            )
1866                            .unwrap(),
1867                        )
1868                        .build(),
1869                ])
1870                .unwrap()
1871                .with_initial_location_constraint(LocationConstraint::BinaryExpression(
1872                    Box::new(LocationConstraint::ComparisonExpression(
1873                        Box::new(IntegerExpression::Atom(Location::new("loc1"))),
1874                        ComparisonOp::Eq,
1875                        Box::new(IntegerExpression::BinaryExpr(
1876                            Box::new(IntegerExpression::Param(Parameter::new("n"))),
1877                            IntegerOp::Sub,
1878                            Box::new(IntegerExpression::Param(Parameter::new("f"))),
1879                        )),
1880                    )),
1881                    BooleanConnective::Or,
1882                    Box::new(LocationConstraint::ComparisonExpression(
1883                        Box::new(IntegerExpression::Atom(Location::new("loc2"))),
1884                        ComparisonOp::Eq,
1885                        Box::new(IntegerExpression::Const(0)),
1886                    )),
1887                ))
1888                .unwrap()
1889                .with_initial_variable_constraints(vec![
1890                    BooleanVarConstraint::ComparisonExpression(
1891                        Box::new(IntegerExpression::Atom(Variable::new("var1"))),
1892                        ComparisonOp::Eq,
1893                        Box::new(IntegerExpression::Const(0)),
1894                    ),
1895                    BooleanVarConstraint::ComparisonExpression(
1896                        Box::new(IntegerExpression::Atom(Variable::new("var2"))),
1897                        ComparisonOp::Eq,
1898                        Box::new(IntegerExpression::Const(0)),
1899                    ),
1900                    BooleanVarConstraint::ComparisonExpression(
1901                        Box::new(IntegerExpression::Atom(Variable::new("var3"))),
1902                        ComparisonOp::Eq,
1903                        Box::new(IntegerExpression::Const(0)),
1904                    ),
1905                ])
1906                .unwrap()
1907                .with_resilience_condition(ParameterConstraint::ComparisonExpression(
1908                    Box::new(IntegerExpression::Param(Parameter::new("n"))),
1909                    ComparisonOp::Gt,
1910                    Box::new(IntegerExpression::BinaryExpr(
1911                        Box::new(IntegerExpression::Const(3)),
1912                        IntegerOp::Mul,
1913                        Box::new(IntegerExpression::Param(Parameter::new("f"))),
1914                    )),
1915                ))
1916                .unwrap()
1917                .build();
1918
1919            let parser = ByMCParser;
1920            let got_ta = parser.parse_ta(test_spec).unwrap();
1921
1922            assert_eq!(got_ta, expected_ta)
1923        }
1924
1925        #[test]
1926        fn test_parse_ta_1_with_define() {
1927            let test_spec = "
1928            skel test_ta1 {
1929                shared var1, var2, var3;
1930                parameters n, t, f;
1931                
1932                define THRESH_1 == n-f;
1933                define THRESH_2 == n;
1934
1935                assumptions (1) {
1936                    n > 3 * f;
1937                }
1938
1939                locations (2) {
1940                    loc1 : [0];
1941                    loc2 : [1];
1942                    loc3 : [2];
1943                }
1944
1945                inits (1) {
1946                    loc1 == THRESH_1  || loc2 == 0;
1947                    var1 == 0;
1948                    var2 == 0;
1949                    var3 == 0;
1950                }
1951
1952                rules (4) {
1953                    0: loc1 -> loc2
1954                        when(true)
1955                        do {};
1956                    1: loc2 -> loc3
1957                        when( var1 == 1 && var2 == THRESH_2)
1958                        do { reset(var3); var1' == var1 + 1  };
1959                }
1960
1961                specifications (1) {
1962                }
1963            }
1964            ";
1965
1966            let expected_ta = GeneralThresholdAutomatonBuilder::new("test_ta1")
1967                .with_parameters(vec![
1968                    Parameter::new("n"),
1969                    Parameter::new("t"),
1970                    Parameter::new("f"),
1971                ])
1972                .unwrap()
1973                .with_variables(vec![
1974                    Variable::new("var1"),
1975                    Variable::new("var2"),
1976                    Variable::new("var3"),
1977                ])
1978                .unwrap()
1979                .with_locations(vec![
1980                    Location::new("loc1"),
1981                    Location::new("loc2"),
1982                    Location::new("loc3"),
1983                ])
1984                .unwrap()
1985                .initialize()
1986                .with_rules(vec![
1987                    RuleBuilder::new(0, Location::new("loc1"), Location::new("loc2")).build(),
1988                    RuleBuilder::new(1, Location::new("loc2"), Location::new("loc3"))
1989                        .with_guard(BooleanExpression::BinaryExpression(
1990                            Box::new(BooleanVarConstraint::ComparisonExpression(
1991                                Box::new(IntegerExpression::Atom(Variable::new("var1"))),
1992                                ComparisonOp::Eq,
1993                                Box::new(IntegerExpression::Const(1)),
1994                            )),
1995                            BooleanConnective::And,
1996                            Box::new(BooleanVarConstraint::ComparisonExpression(
1997                                Box::new(IntegerExpression::Atom(Variable::new("var2"))),
1998                                ComparisonOp::Eq,
1999                                Box::new(IntegerExpression::Param(Parameter::new("n"))),
2000                            )),
2001                        ))
2002                        .with_action(Action::new_reset(Variable::new("var3")))
2003                        .with_action(
2004                            Action::new(
2005                                Variable::new("var1"),
2006                                IntegerExpression::Atom(Variable::new("var1"))
2007                                    + IntegerExpression::Const(1),
2008                            )
2009                            .unwrap(),
2010                        )
2011                        .build(),
2012                ])
2013                .unwrap()
2014                .with_initial_location_constraint(LocationConstraint::BinaryExpression(
2015                    Box::new(LocationConstraint::ComparisonExpression(
2016                        Box::new(IntegerExpression::Atom(Location::new("loc1"))),
2017                        ComparisonOp::Eq,
2018                        Box::new(IntegerExpression::BinaryExpr(
2019                            Box::new(IntegerExpression::Param(Parameter::new("n"))),
2020                            IntegerOp::Sub,
2021                            Box::new(IntegerExpression::Param(Parameter::new("f"))),
2022                        )),
2023                    )),
2024                    BooleanConnective::Or,
2025                    Box::new(LocationConstraint::ComparisonExpression(
2026                        Box::new(IntegerExpression::Atom(Location::new("loc2"))),
2027                        ComparisonOp::Eq,
2028                        Box::new(IntegerExpression::Const(0)),
2029                    )),
2030                ))
2031                .unwrap()
2032                .with_initial_variable_constraints(vec![
2033                    BooleanVarConstraint::ComparisonExpression(
2034                        Box::new(IntegerExpression::Atom(Variable::new("var1"))),
2035                        ComparisonOp::Eq,
2036                        Box::new(IntegerExpression::Const(0)),
2037                    ),
2038                    BooleanVarConstraint::ComparisonExpression(
2039                        Box::new(IntegerExpression::Atom(Variable::new("var2"))),
2040                        ComparisonOp::Eq,
2041                        Box::new(IntegerExpression::Const(0)),
2042                    ),
2043                    BooleanVarConstraint::ComparisonExpression(
2044                        Box::new(IntegerExpression::Atom(Variable::new("var3"))),
2045                        ComparisonOp::Eq,
2046                        Box::new(IntegerExpression::Const(0)),
2047                    ),
2048                ])
2049                .unwrap()
2050                .with_resilience_condition(ParameterConstraint::ComparisonExpression(
2051                    Box::new(IntegerExpression::Param(Parameter::new("n"))),
2052                    ComparisonOp::Gt,
2053                    Box::new(IntegerExpression::BinaryExpr(
2054                        Box::new(IntegerExpression::Const(3)),
2055                        IntegerOp::Mul,
2056                        Box::new(IntegerExpression::Param(Parameter::new("f"))),
2057                    )),
2058                ))
2059                .unwrap()
2060                .build();
2061
2062            let parser = ByMCParser;
2063            let got_ta = parser.parse_ta(test_spec).unwrap();
2064
2065            assert_eq!(got_ta, expected_ta)
2066        }
2067
2068        #[test]
2069        fn test_parse_ta_2() {
2070            let test_spec = "
2071            skel test_ta {
2072                local loc;
2073                shared sha;
2074                parameters n;
2075
2076                assumptions (1) {
2077                    n >= 1;
2078                }
2079
2080                locations (3) {
2081                    q0: [0];
2082                    q1: [1];
2083                    q2: [2];
2084                }/*loc*/
2085                inits (3) {
2086                    q0 == n;
2087                    q1 == 0;
2088                    q2 == 0;
2089                    sha == 0;
2090                }/*in */
2091                rules (1) {
2092                    0: q0 -> q1
2093                    when (true)
2094                    do { sha' == sha + 1 };
2095                }
2096
2097                specifications (0) {
2098
2099                }
2100            }
2101            ";
2102
2103            let expected_ta = GeneralThresholdAutomatonBuilder::new("test_ta")
2104                .with_variables(vec![Variable::new("sha")])
2105                .unwrap()
2106                .with_parameters(vec![Parameter::new("n")])
2107                .unwrap()
2108                .with_locations(vec![
2109                    Location::new("q0"),
2110                    Location::new("q1"),
2111                    Location::new("q2"),
2112                ])
2113                .unwrap()
2114                .initialize()
2115                .with_resilience_condition(ParameterConstraint::ComparisonExpression(
2116                    Box::new(IntegerExpression::Param(Parameter::new("n"))),
2117                    ComparisonOp::Geq,
2118                    Box::new(IntegerExpression::Const(1)),
2119                ))
2120                .unwrap()
2121                .with_initial_location_constraints(vec![
2122                    LocationConstraint::ComparisonExpression(
2123                        Box::new(IntegerExpression::Atom(Location::new("q0"))),
2124                        ComparisonOp::Eq,
2125                        Box::new(IntegerExpression::Param(Parameter::new("n"))),
2126                    ),
2127                    LocationConstraint::ComparisonExpression(
2128                        Box::new(IntegerExpression::Atom(Location::new("q1"))),
2129                        ComparisonOp::Eq,
2130                        Box::new(IntegerExpression::Const(0)),
2131                    ),
2132                    LocationConstraint::ComparisonExpression(
2133                        Box::new(IntegerExpression::Atom(Location::new("q2"))),
2134                        ComparisonOp::Eq,
2135                        Box::new(IntegerExpression::Const(0)),
2136                    ),
2137                ])
2138                .unwrap()
2139                .with_initial_variable_constraint(BooleanVarConstraint::ComparisonExpression(
2140                    Box::new(IntegerExpression::Atom(Variable::new("sha"))),
2141                    ComparisonOp::Eq,
2142                    Box::new(IntegerExpression::Const(0)),
2143                ))
2144                .unwrap()
2145                .with_rules(vec![
2146                    RuleBuilder::new(0, Location::new("q0"), Location::new("q1"))
2147                        .with_guard(BooleanExpression::True)
2148                        .with_action(
2149                            Action::new(
2150                                Variable::new("sha"),
2151                                IntegerExpression::Atom(Variable::new("sha"))
2152                                    + IntegerExpression::Const(1),
2153                            )
2154                            .unwrap(),
2155                        )
2156                        .build(),
2157                ])
2158                .unwrap()
2159                .build();
2160
2161            let parser = ByMCParser;
2162            let got_ta = parser.parse_ta(test_spec).unwrap();
2163
2164            assert_eq!(got_ta, expected_ta)
2165        }
2166
2167        #[test]
2168        fn test_parse_ta_2_invalid_component_numbers() {
2169            let test_spec = "
2170            skel test_ta {
2171                local loc;
2172                shared sha;
2173                parameters n;
2174
2175                assumptions (0) {
2176                    n >= 1;
2177                }
2178
2179                locations (0) {
2180                    q0: [0];
2181                    q1: [1];
2182                    q2: [2];
2183                }/*loc*/
2184
2185                inits (0) {
2186                    q0 == n;
2187                    q1 == 0;
2188                    q2 == 0;
2189                    sha == 0;
2190                }/*in */
2191
2192                rules (0) {
2193                    0: q0 -> q1
2194                    when (true)
2195                    do { sha' == sha + 1 };
2196                }
2197
2198                specifications (5) {
2199
2200                }
2201            }
2202            ";
2203
2204            let expected_ta = GeneralThresholdAutomatonBuilder::new("test_ta")
2205                .with_variables(vec![Variable::new("sha")])
2206                .unwrap()
2207                .with_parameters(vec![Parameter::new("n")])
2208                .unwrap()
2209                .with_locations(vec![
2210                    Location::new("q0"),
2211                    Location::new("q1"),
2212                    Location::new("q2"),
2213                ])
2214                .unwrap()
2215                .initialize()
2216                .with_resilience_condition(ParameterConstraint::ComparisonExpression(
2217                    Box::new(IntegerExpression::Param(Parameter::new("n"))),
2218                    ComparisonOp::Geq,
2219                    Box::new(IntegerExpression::Const(1)),
2220                ))
2221                .unwrap()
2222                .with_initial_location_constraints(vec![
2223                    LocationConstraint::ComparisonExpression(
2224                        Box::new(IntegerExpression::Atom(Location::new("q0"))),
2225                        ComparisonOp::Eq,
2226                        Box::new(IntegerExpression::Param(Parameter::new("n"))),
2227                    ),
2228                    LocationConstraint::ComparisonExpression(
2229                        Box::new(IntegerExpression::Atom(Location::new("q1"))),
2230                        ComparisonOp::Eq,
2231                        Box::new(IntegerExpression::Const(0)),
2232                    ),
2233                    LocationConstraint::ComparisonExpression(
2234                        Box::new(IntegerExpression::Atom(Location::new("q2"))),
2235                        ComparisonOp::Eq,
2236                        Box::new(IntegerExpression::Const(0)),
2237                    ),
2238                ])
2239                .unwrap()
2240                .with_initial_variable_constraint(BooleanVarConstraint::ComparisonExpression(
2241                    Box::new(IntegerExpression::Atom(Variable::new("sha"))),
2242                    ComparisonOp::Eq,
2243                    Box::new(IntegerExpression::Const(0)),
2244                ))
2245                .unwrap()
2246                .with_rules(vec![
2247                    RuleBuilder::new(0, Location::new("q0"), Location::new("q1"))
2248                        .with_guard(BooleanExpression::True)
2249                        .with_action(
2250                            Action::new(
2251                                Variable::new("sha"),
2252                                IntegerExpression::Atom(Variable::new("sha"))
2253                                    + IntegerExpression::Const(1),
2254                            )
2255                            .unwrap(),
2256                        )
2257                        .build(),
2258                ])
2259                .unwrap()
2260                .build();
2261
2262            let parser = ByMCParser::new();
2263            let got_ta = parser.parse_ta(test_spec).unwrap();
2264
2265            assert_eq!(got_ta, expected_ta)
2266        }
2267
2268        #[test]
2269        fn test_parse_ta_3() {
2270            let test_spec = "
2271            skel test_ta {
2272                shared sha, var1, var2, var3;
2273                parameters n, t, f, p;
2274
2275                assumptions (1) {
2276                    n >= 1;
2277                    n > 3 * f;
2278                    n < 3 * t;
2279                    p + n <= t / f;
2280                }
2281
2282                locations (3) {
2283                    q0: [0];
2284                    q1: [1];
2285                    q2: [2];
2286                }
2287
2288                // my comment
2289                inits (3) {
2290                    q0 == n + f;
2291                    q1 == 0;
2292                    q2 == 0;
2293                    sha == 0;
2294                    var1 < 1;
2295                    var2 <= 0;
2296                }
2297
2298                rules (1) {
2299                    0: q0 -> q1
2300                        when (true)
2301                        do { sha' == sha + 1 };
2302                    1: q0 -> q1
2303                        when (false)
2304                        do { unchanged(var1, var2, var3) };
2305                    2: q1 -> q2
2306                        when (var1 == 1 && var2 <= 0)
2307                        do { reset(var3); var1' == var1 + 1 };
2308                    3: q2 -> q1
2309                        when ( !(var1 < 1) || var3 <= n)
2310                        do { var3' == 0 };
2311                }
2312
2313                specifications (0) {
2314
2315                }
2316            }
2317            ";
2318
2319            let expected_ta = GeneralThresholdAutomatonBuilder::new("test_ta")
2320                .with_variables(vec![
2321                    Variable::new("sha"),
2322                    Variable::new("var1"),
2323                    Variable::new("var2"),
2324                    Variable::new("var3"),
2325                ])
2326                .unwrap()
2327                .with_parameters(vec![
2328                    Parameter::new("n"),
2329                    Parameter::new("t"),
2330                    Parameter::new("f"),
2331                    Parameter::new("p"),
2332                ])
2333                .unwrap()
2334                .with_locations(vec![
2335                    Location::new("q0"),
2336                    Location::new("q1"),
2337                    Location::new("q2"),
2338                ])
2339                .unwrap()
2340                .initialize()
2341                .with_resilience_conditions(vec![
2342                    ParameterConstraint::ComparisonExpression(
2343                        Box::new(IntegerExpression::Param(Parameter::new("n"))),
2344                        ComparisonOp::Geq,
2345                        Box::new(IntegerExpression::Const(1)),
2346                    ),
2347                    ParameterConstraint::ComparisonExpression(
2348                        Box::new(IntegerExpression::Param(Parameter::new("n"))),
2349                        ComparisonOp::Gt,
2350                        Box::new(IntegerExpression::BinaryExpr(
2351                            Box::new(IntegerExpression::Const(3)),
2352                            IntegerOp::Mul,
2353                            Box::new(IntegerExpression::Param(Parameter::new("f"))),
2354                        )),
2355                    ),
2356                    ParameterConstraint::ComparisonExpression(
2357                        Box::new(IntegerExpression::Param(Parameter::new("n"))),
2358                        ComparisonOp::Lt,
2359                        Box::new(IntegerExpression::BinaryExpr(
2360                            Box::new(IntegerExpression::Const(3)),
2361                            IntegerOp::Mul,
2362                            Box::new(IntegerExpression::Param(Parameter::new("t"))),
2363                        )),
2364                    ),
2365                    ParameterConstraint::ComparisonExpression(
2366                        Box::new(IntegerExpression::BinaryExpr(
2367                            Box::new(IntegerExpression::Param(Parameter::new("p"))),
2368                            IntegerOp::Add,
2369                            Box::new(IntegerExpression::Param(Parameter::new("n"))),
2370                        )),
2371                        ComparisonOp::Leq,
2372                        Box::new(IntegerExpression::BinaryExpr(
2373                            Box::new(IntegerExpression::Param(Parameter::new("t"))),
2374                            IntegerOp::Div,
2375                            Box::new(IntegerExpression::Param(Parameter::new("f"))),
2376                        )),
2377                    ),
2378                ])
2379                .unwrap()
2380                .with_initial_location_constraints(vec![
2381                    LocationConstraint::ComparisonExpression(
2382                        Box::new(IntegerExpression::Atom(Location::new("q0"))),
2383                        ComparisonOp::Eq,
2384                        Box::new(IntegerExpression::BinaryExpr(
2385                            Box::new(IntegerExpression::Param(Parameter::new("n"))),
2386                            IntegerOp::Add,
2387                            Box::new(IntegerExpression::Param(Parameter::new("f"))),
2388                        )),
2389                    ),
2390                    LocationConstraint::ComparisonExpression(
2391                        Box::new(IntegerExpression::Atom(Location::new("q1"))),
2392                        ComparisonOp::Eq,
2393                        Box::new(IntegerExpression::Const(0)),
2394                    ),
2395                    LocationConstraint::ComparisonExpression(
2396                        Box::new(IntegerExpression::Atom(Location::new("q2"))),
2397                        ComparisonOp::Eq,
2398                        Box::new(IntegerExpression::Const(0)),
2399                    ),
2400                ])
2401                .unwrap()
2402                .with_initial_variable_constraints(vec![
2403                    BooleanVarConstraint::ComparisonExpression(
2404                        Box::new(IntegerExpression::Atom(Variable::new("sha"))),
2405                        ComparisonOp::Eq,
2406                        Box::new(IntegerExpression::Const(0)),
2407                    ),
2408                    BooleanVarConstraint::ComparisonExpression(
2409                        Box::new(IntegerExpression::Atom(Variable::new("var1"))),
2410                        ComparisonOp::Lt,
2411                        Box::new(IntegerExpression::Const(1)),
2412                    ),
2413                    BooleanVarConstraint::ComparisonExpression(
2414                        Box::new(IntegerExpression::Atom(Variable::new("var2"))),
2415                        ComparisonOp::Leq,
2416                        Box::new(IntegerExpression::Const(0)),
2417                    ),
2418                ])
2419                .unwrap()
2420                .with_rules(vec![
2421                    RuleBuilder::new(0, Location::new("q0"), Location::new("q1"))
2422                        .with_guard(BooleanExpression::True)
2423                        .with_action(
2424                            Action::new(
2425                                Variable::new("sha"),
2426                                IntegerExpression::Atom(Variable::new("sha"))
2427                                    + IntegerExpression::Const(1),
2428                            )
2429                            .unwrap(),
2430                        )
2431                        .build(),
2432                    RuleBuilder::new(1, Location::new("q0"), Location::new("q1"))
2433                        .with_guard(BooleanExpression::False)
2434                        .build(),
2435                    RuleBuilder::new(2, Location::new("q1"), Location::new("q2"))
2436                        .with_guard(BooleanExpression::BinaryExpression(
2437                            Box::new(BooleanVarConstraint::ComparisonExpression(
2438                                Box::new(IntegerExpression::Atom(Variable::new("var1"))),
2439                                ComparisonOp::Eq,
2440                                Box::new(IntegerExpression::Const(1)),
2441                            )),
2442                            BooleanConnective::And,
2443                            Box::new(BooleanVarConstraint::ComparisonExpression(
2444                                Box::new(IntegerExpression::Atom(Variable::new("var2"))),
2445                                ComparisonOp::Leq,
2446                                Box::new(IntegerExpression::Const(0)),
2447                            )),
2448                        ))
2449                        .with_actions(vec![
2450                            Action::new_reset(Variable::new("var3")),
2451                            Action::new(
2452                                Variable::new("var1"),
2453                                IntegerExpression::Atom(Variable::new("var1"))
2454                                    + IntegerExpression::Const(1),
2455                            )
2456                            .unwrap(),
2457                        ])
2458                        .build(),
2459                    RuleBuilder::new(3, Location::new("q2"), Location::new("q1"))
2460                        .with_guard(BooleanExpression::BinaryExpression(
2461                            Box::new(BooleanExpression::Not(Box::new(
2462                                BooleanVarConstraint::ComparisonExpression(
2463                                    Box::new(IntegerExpression::Atom(Variable::new("var1"))),
2464                                    ComparisonOp::Lt,
2465                                    Box::new(IntegerExpression::Const(1)),
2466                                ),
2467                            ))),
2468                            BooleanConnective::Or,
2469                            Box::new(BooleanVarConstraint::ComparisonExpression(
2470                                Box::new(IntegerExpression::Atom(Variable::new("var3"))),
2471                                ComparisonOp::Leq,
2472                                Box::new(IntegerExpression::Param(Parameter::new("n"))),
2473                            )),
2474                        ))
2475                        .with_actions(vec![Action::new_reset(Variable::new("var3"))])
2476                        .build(),
2477                ])
2478                .unwrap()
2479                .build();
2480
2481            let parser = ByMCParser;
2482            let got_ta = parser.parse_ta(test_spec).unwrap();
2483
2484            assert_eq!(got_ta, expected_ta)
2485        }
2486
2487        #[test]
2488        fn test_parse_ta_3_with_define() {
2489            let test_spec = "
2490            skel test_ta {
2491                shared sha, var1, var2, var3;
2492                parameters n, t, f, p;
2493
2494                define THRESH_0 == 3 * f;
2495                define THRESH_1 == n + f;
2496                define THRESH_2 == 0;
2497                define THRESH_4 == n;
2498
2499                assumptions (1) {
2500                    n >= 1;
2501                    n > THRESH_0;
2502                    n < 3 * t;
2503                    p + n <= t / f;
2504                }
2505
2506                locations (3) {
2507                    q0: [0];
2508                    q1: [1];
2509                    q2: [2];
2510                }
2511
2512                // my comment
2513                inits (3) {
2514                    q0 == THRESH_1;
2515                    q1 == THRESH_2;
2516                    q2 == THRESH_2;
2517                    sha == THRESH_2;
2518                    var1 < 1;
2519                    var2 <= THRESH_2;
2520                }
2521
2522                rules (1) {
2523                    0: q0 -> q1
2524                        when (true)
2525                        do { sha' == sha + 1 };
2526                    1: q0 -> q1
2527                        when (false)
2528                        do { unchanged(var1, var2, var3) };
2529                    2: q1 -> q2
2530                        when (var1 == 1 && var2 <= THRESH_2)
2531                        do { reset(var3); var1' == var1 + 1 };
2532                    3: q2 -> q1
2533                        when ( !(var1 < 1) || var3 <= THRESH_4)
2534                        do { var3' == 0 };
2535                }
2536
2537                specifications (0) {
2538
2539                }
2540            }
2541            ";
2542
2543            let expected_ta = GeneralThresholdAutomatonBuilder::new("test_ta")
2544                .with_variables(vec![
2545                    Variable::new("sha"),
2546                    Variable::new("var1"),
2547                    Variable::new("var2"),
2548                    Variable::new("var3"),
2549                ])
2550                .unwrap()
2551                .with_parameters(vec![
2552                    Parameter::new("n"),
2553                    Parameter::new("t"),
2554                    Parameter::new("f"),
2555                    Parameter::new("p"),
2556                ])
2557                .unwrap()
2558                .with_locations(vec![
2559                    Location::new("q0"),
2560                    Location::new("q1"),
2561                    Location::new("q2"),
2562                ])
2563                .unwrap()
2564                .initialize()
2565                .with_resilience_conditions(vec![
2566                    ParameterConstraint::ComparisonExpression(
2567                        Box::new(IntegerExpression::Param(Parameter::new("n"))),
2568                        ComparisonOp::Geq,
2569                        Box::new(IntegerExpression::Const(1)),
2570                    ),
2571                    ParameterConstraint::ComparisonExpression(
2572                        Box::new(IntegerExpression::Param(Parameter::new("n"))),
2573                        ComparisonOp::Gt,
2574                        Box::new(IntegerExpression::BinaryExpr(
2575                            Box::new(IntegerExpression::Const(3)),
2576                            IntegerOp::Mul,
2577                            Box::new(IntegerExpression::Param(Parameter::new("f"))),
2578                        )),
2579                    ),
2580                    ParameterConstraint::ComparisonExpression(
2581                        Box::new(IntegerExpression::Param(Parameter::new("n"))),
2582                        ComparisonOp::Lt,
2583                        Box::new(IntegerExpression::BinaryExpr(
2584                            Box::new(IntegerExpression::Const(3)),
2585                            IntegerOp::Mul,
2586                            Box::new(IntegerExpression::Param(Parameter::new("t"))),
2587                        )),
2588                    ),
2589                    ParameterConstraint::ComparisonExpression(
2590                        Box::new(IntegerExpression::BinaryExpr(
2591                            Box::new(IntegerExpression::Param(Parameter::new("p"))),
2592                            IntegerOp::Add,
2593                            Box::new(IntegerExpression::Param(Parameter::new("n"))),
2594                        )),
2595                        ComparisonOp::Leq,
2596                        Box::new(IntegerExpression::BinaryExpr(
2597                            Box::new(IntegerExpression::Param(Parameter::new("t"))),
2598                            IntegerOp::Div,
2599                            Box::new(IntegerExpression::Param(Parameter::new("f"))),
2600                        )),
2601                    ),
2602                ])
2603                .unwrap()
2604                .with_initial_location_constraints(vec![
2605                    LocationConstraint::ComparisonExpression(
2606                        Box::new(IntegerExpression::Atom(Location::new("q0"))),
2607                        ComparisonOp::Eq,
2608                        Box::new(IntegerExpression::BinaryExpr(
2609                            Box::new(IntegerExpression::Param(Parameter::new("n"))),
2610                            IntegerOp::Add,
2611                            Box::new(IntegerExpression::Param(Parameter::new("f"))),
2612                        )),
2613                    ),
2614                    LocationConstraint::ComparisonExpression(
2615                        Box::new(IntegerExpression::Atom(Location::new("q1"))),
2616                        ComparisonOp::Eq,
2617                        Box::new(IntegerExpression::Const(0)),
2618                    ),
2619                    LocationConstraint::ComparisonExpression(
2620                        Box::new(IntegerExpression::Atom(Location::new("q2"))),
2621                        ComparisonOp::Eq,
2622                        Box::new(IntegerExpression::Const(0)),
2623                    ),
2624                ])
2625                .unwrap()
2626                .with_initial_variable_constraints(vec![
2627                    BooleanVarConstraint::ComparisonExpression(
2628                        Box::new(IntegerExpression::Atom(Variable::new("sha"))),
2629                        ComparisonOp::Eq,
2630                        Box::new(IntegerExpression::Const(0)),
2631                    ),
2632                    BooleanVarConstraint::ComparisonExpression(
2633                        Box::new(IntegerExpression::Atom(Variable::new("var1"))),
2634                        ComparisonOp::Lt,
2635                        Box::new(IntegerExpression::Const(1)),
2636                    ),
2637                    BooleanVarConstraint::ComparisonExpression(
2638                        Box::new(IntegerExpression::Atom(Variable::new("var2"))),
2639                        ComparisonOp::Leq,
2640                        Box::new(IntegerExpression::Const(0)),
2641                    ),
2642                ])
2643                .unwrap()
2644                .with_rules(vec![
2645                    RuleBuilder::new(0, Location::new("q0"), Location::new("q1"))
2646                        .with_guard(BooleanExpression::True)
2647                        .with_action(
2648                            Action::new(
2649                                Variable::new("sha"),
2650                                IntegerExpression::Atom(Variable::new("sha"))
2651                                    + IntegerExpression::Const(1),
2652                            )
2653                            .unwrap(),
2654                        )
2655                        .build(),
2656                    RuleBuilder::new(1, Location::new("q0"), Location::new("q1"))
2657                        .with_guard(BooleanExpression::False)
2658                        .build(),
2659                    RuleBuilder::new(2, Location::new("q1"), Location::new("q2"))
2660                        .with_guard(BooleanExpression::BinaryExpression(
2661                            Box::new(BooleanVarConstraint::ComparisonExpression(
2662                                Box::new(IntegerExpression::Atom(Variable::new("var1"))),
2663                                ComparisonOp::Eq,
2664                                Box::new(IntegerExpression::Const(1)),
2665                            )),
2666                            BooleanConnective::And,
2667                            Box::new(BooleanVarConstraint::ComparisonExpression(
2668                                Box::new(IntegerExpression::Atom(Variable::new("var2"))),
2669                                ComparisonOp::Leq,
2670                                Box::new(IntegerExpression::Const(0)),
2671                            )),
2672                        ))
2673                        .with_actions(vec![
2674                            Action::new_reset(Variable::new("var3")),
2675                            Action::new(
2676                                Variable::new("var1"),
2677                                IntegerExpression::Atom(Variable::new("var1"))
2678                                    + IntegerExpression::Const(1),
2679                            )
2680                            .unwrap(),
2681                        ])
2682                        .build(),
2683                    RuleBuilder::new(3, Location::new("q2"), Location::new("q1"))
2684                        .with_guard(BooleanExpression::BinaryExpression(
2685                            Box::new(BooleanExpression::Not(Box::new(
2686                                BooleanVarConstraint::ComparisonExpression(
2687                                    Box::new(IntegerExpression::Atom(Variable::new("var1"))),
2688                                    ComparisonOp::Lt,
2689                                    Box::new(IntegerExpression::Const(1)),
2690                                ),
2691                            ))),
2692                            BooleanConnective::Or,
2693                            Box::new(BooleanVarConstraint::ComparisonExpression(
2694                                Box::new(IntegerExpression::Atom(Variable::new("var3"))),
2695                                ComparisonOp::Leq,
2696                                Box::new(IntegerExpression::Param(Parameter::new("n"))),
2697                            )),
2698                        ))
2699                        .with_actions(vec![Action::new_reset(Variable::new("var3"))])
2700                        .build(),
2701                ])
2702                .unwrap()
2703                .build();
2704
2705            let parser = ByMCParser;
2706            let got_ta = parser.parse_ta(test_spec).unwrap();
2707
2708            assert_eq!(got_ta, expected_ta)
2709        }
2710    }
2711}
taco_parser/bymc.rs

taco_parser/
bymc.rs
