taco_parser/tla/
integer_exprs.rs

1//! Module declaring helper functions to parse expressions over integers,
2//! including boolean expressions over integers
3//!
4//! This module implements the parsing of expressions involving integers, such
5//! as for example boolean expressions over integers or update expressions over
6//! integers.
7
8use std::any::TypeId;
9
10use anyhow::Context;
11use pest::{
12    iterators::Pair,
13    pratt_parser::{Assoc, PrattParser},
14};
15use taco_model_checker::eltl::ELTLExpression;
16use taco_threshold_automaton::{
17    expressions::{
18        Atomic, BooleanConnective, BooleanExpression, ComparisonOp, IntegerExpression, IntegerOp,
19        IsDeclared, Location, Parameter, Variable,
20    },
21    general_threshold_automaton::Action,
22};
23
24use crate::tla::{
25    N_CORR_PROC, PROC_SET, Rule, TLAParsingContext, new_parsing_error, parse_identifier_to_t,
26    try_parse_map_entry_constr_loc,
27};
28
29// Pratt parser responsible for maintaining operator precedence
30//
31// Here we simply borrow them from C++
32// [see](https://en.cppreference.com/w/cpp/language/operator_precedence)
33//
34// Additionally, we define the precedence of the temporal operators
35// - `G` (Globally) and `F` (Eventually) have the highest precedence
36// - `!` (Not) has the second highest precedence
37lazy_static::lazy_static! {
38   pub(crate) static ref PRATT_PARSER: PrattParser<Rule> = {
39        use pest::pratt_parser::{Op};
40
41        // Precedence is defined lowest to highest
42        PrattParser::new()
43            .op(Op::infix(Rule::or, Assoc::Left))
44            .op(Op::infix(Rule::implication, Assoc::Right))
45            .op(Op::infix(Rule::and, Assoc::Left))
46            .op(Op::infix(Rule::equal, Assoc::Left) | Op::infix(Rule::not_equal, Assoc::Left))
47            .op(Op::infix(Rule::less_eq, Assoc::Left)
48                | Op::infix(Rule::less, Assoc::Left)
49                | Op::infix(Rule::greater_eq, Assoc::Left)
50                | Op::infix(Rule::greater, Assoc::Left))
51            .op(Op::infix(Rule::add, Assoc::Left) | Op::infix(Rule::sub, Assoc::Left))
52            .op(Op::infix(Rule::mul, Assoc::Left) | Op::infix(Rule::div, Assoc::Left))
53            .op(Op::prefix(Rule::negation))
54            .op(Op::prefix(Rule::not))
55            .op(Op::prefix(Rule::eventually) |  Op::prefix(Rule::globally))
56    };
57}
58
59/// Parse a single ltl specification
60///
61/// This function parses a single ltl specification and returns the name of the
62/// specification and the ltl expression.
63pub(crate) fn parse_ltl_specification<T>(
64    pair: Pair<'_, Rule>,
65    builder: &T,
66    ctx: &TLAParsingContext<'_>,
67) -> Result<(String, ELTLExpression), anyhow::Error>
68where
69    T: IsDeclared<Variable> + IsDeclared<Location> + IsDeclared<Parameter>,
70{
71    debug_assert!(
72        pair.as_rule() == Rule::ltl_spec_declaration,
73        "Expected a specification, got rule {:?} for {}",
74        pair.as_rule(),
75        pair.as_str()
76    );
77
78    let mut pairs = pair.into_inner();
79
80    let name: String = parse_identifier_to_t(&pairs.next().unwrap());
81
82    let expression = parse_ltl_expr(pairs.next().unwrap(), builder, ctx)?;
83
84    Ok((name, expression))
85}
86
87/// Parse an ltl expression into a single ltl expression
88///
89/// This function parses an ltl expression with operator precedence
90/// and returns the corresponding ltl expression.
91/// The function returns an error if the expression refers to an unknown location
92pub(crate) fn parse_ltl_expr<T>(
93    pair: Pair<'_, Rule>,
94    builder: &T,
95    ctx: &TLAParsingContext<'_>,
96) -> Result<ELTLExpression, Box<pest::error::Error<()>>>
97where
98    T: IsDeclared<Variable> + IsDeclared<Location> + IsDeclared<Parameter>,
99{
100    debug_assert!(
101        pair.as_rule() == Rule::ltl_expr,
102        "Expected an LTL expression, got rule {:?} for {}",
103        pair.as_rule(),
104        pair.as_str()
105    );
106
107    let pairs = pair.into_inner();
108    PRATT_PARSER
109        .map_primary(|atom| parse_ltl_atom(atom, builder, ctx))
110        .map_infix(|lhs, op, rhs| {
111            let lhs = lhs?;
112            let rhs = rhs?;
113
114            let op = match op.as_rule() {
115                Rule::and => ELTLExpression::And(Box::new(lhs), Box::new(rhs)),
116                Rule::or => ELTLExpression::Or(Box::new(lhs), Box::new(rhs)),
117                Rule::implication => ELTLExpression::Implies(Box::new(lhs), Box::new(rhs)),
118                _ => unreachable!(
119                    "Unknown rule for binary ltl operator {:?}: {}",
120                    op.as_rule(),
121                    op.as_str()
122                ),
123            };
124
125            Ok(op)
126        })
127        .map_prefix(|op, rhs| {
128            let rhs = rhs?;
129
130            match op.as_rule() {
131                Rule::not => Ok(ELTLExpression::Not(Box::new(rhs))),
132                Rule::globally => Ok(ELTLExpression::Globally(Box::new(rhs))),
133                Rule::eventually => Ok(ELTLExpression::Eventually(Box::new(rhs))),
134                _ => unreachable!(
135                    "Unknown rule for unary ltl operator {:?}: {}",
136                    op.as_rule(),
137                    op.as_str()
138                ),
139            }
140        })
141        .parse(pairs)
142}
143
144/// Parse an ltl atom into a single ltl expression
145///
146/// This function parses an ltl atom and returns the corresponding ltl expression.
147/// The function returns an error if the expression refers to an unknown location.
148fn parse_ltl_atom<T>(
149    pair: Pair<'_, Rule>,
150    builder: &T,
151    ctx: &TLAParsingContext<'_>,
152) -> Result<ELTLExpression, Box<pest::error::Error<()>>>
153where
154    T: IsDeclared<Variable> + IsDeclared<Location> + IsDeclared<Parameter>,
155{
156    debug_assert!(
157        pair.as_rule() == Rule::ltl_atom,
158        "Expected an LTL atom, got rule {:?} for {}",
159        pair.as_rule(),
160        pair.as_str()
161    );
162
163    let mut pairs = pair.into_inner();
164    let pair = pairs.next().unwrap();
165
166    match pair.as_rule() {
167        Rule::ltl_expr => parse_ltl_expr(pair, builder, ctx),
168        Rule::ltl_unary_op => {
169            let op = pair.into_inner().next().unwrap();
170            let expr = pairs
171                .next()
172                .expect("Missing LTL expression after unary operator");
173            let expr = parse_ltl_atom(expr, builder, ctx)?;
174
175            match op.as_rule() {
176                Rule::not => Ok(ELTLExpression::Not(Box::new(expr))),
177                Rule::globally => Ok(ELTLExpression::Globally(Box::new(expr))),
178                Rule::eventually => Ok(ELTLExpression::Eventually(Box::new(expr))),
179                _ => unreachable!(
180                    "Unknown rule for unary operator {:?}: {}",
181                    op.as_rule(),
182                    op.as_str()
183                ),
184            }
185        }
186        Rule::comparison_expr => {
187            let span = pair.as_span();
188
189            // First: attempt to parse parameter expression !
190            // This is important as constraints purely on parameters are also
191            // valid for variable / location expressions
192            if let Ok((lhs, op, rhs)) =
193                parse_comparison_expr::<Parameter, T>(pair.clone(), builder, ctx)
194            {
195                return Ok(ELTLExpression::ParameterExpr(
196                    Box::new(lhs),
197                    op,
198                    Box::new(rhs),
199                ));
200            }
201
202            if let Ok((lhs, op, rhs)) =
203                parse_comparison_expr::<Variable, T>(pair.clone(), builder, ctx)
204            {
205                return Ok(ELTLExpression::VariableExpr(
206                    Box::new(lhs),
207                    op,
208                    Box::new(rhs),
209                ));
210            }
211
212            let (lhs, op, rhs) = parse_comparison_expr(pair, builder, ctx).map_err(|_err| {
213                new_parsing_error("Failed to parse inner ltl expression. This is most likely due to an unknown identifier", span)
214            })?;
215            let expr = ELTLExpression::LocationExpr(Box::new(lhs), op, Box::new(rhs));
216            Ok(expr)
217        }
218        Rule::bool_const => {
219            let pair = pair.into_inner().next().unwrap();
220
221            match pair.as_rule() {
222                Rule::bool_true => Ok(ELTLExpression::True),
223                Rule::bool_false => Ok(ELTLExpression::False),
224                _ => unreachable!(
225                    "Unknown rule for boolean constant {:?}: {}",
226                    pair.as_rule(),
227                    pair.as_str()
228                ),
229            }
230        }
231        _ => unreachable!(
232            "Unknown rule for ltl atom {:?}: {}",
233            pair.as_rule(),
234            pair.as_str()
235        ),
236    }
237}
238
239/// Parse boolean_atom
240#[inline(always)]
241fn parse_boolean_atom<T, U>(
242    pair: Pair<'_, Rule>,
243    builder: &U,
244    ctx: &TLAParsingContext,
245) -> Result<BooleanExpression<T>, anyhow::Error>
246where
247    T: Atomic + 'static,
248    U: IsDeclared<T> + IsDeclared<Parameter>,
249{
250    debug_assert!(
251        pair.as_rule() == Rule::int_bool_atom,
252        "Got rule {:?} for {}",
253        pair.as_rule(),
254        pair.as_str()
255    );
256
257    let pair = pair
258        .into_inner()
259        .next()
260        .expect("Expected boolean atom to be non-empty");
261
262    match pair.as_rule() {
263        Rule::bool_const => Ok(parse_boolean_const(pair)),
264        Rule::int_bool_expr => parse_int_boolean_expr(pair, builder, ctx),
265        Rule::comparison_expr => {
266            let (lhs, op, rhs) = parse_comparison_expr(pair, builder, ctx)?;
267            Ok(BooleanExpression::ComparisonExpression(
268                Box::new(lhs),
269                op,
270                Box::new(rhs),
271            ))
272        }
273        _ => unreachable!(
274            "Unknown rule for boolean atom {:?}: {}",
275            pair.as_rule(),
276            pair.as_str(),
277        ),
278    }
279}
280
281/// Parse integer constant
282///
283/// Parses a pair of type `integer_const` into a `u32`
284#[inline(always)]
285pub(crate) fn parse_integer_const(pair: Pair<'_, Rule>) -> u32 {
286    debug_assert!(
287        pair.as_rule() == Rule::integer_const,
288        "Got rule {:?} for {}",
289        pair.as_rule(),
290        pair.as_str()
291    );
292    pair.as_str().parse::<u32>().unwrap()
293}
294
295/// Parse an integer operator
296#[inline(always)]
297fn parse_integer_binary_op(pair: Pair<'_, Rule>) -> IntegerOp {
298    match pair.as_rule() {
299        Rule::add => IntegerOp::Add,
300        Rule::sub => IntegerOp::Sub,
301        Rule::mul => IntegerOp::Mul,
302        Rule::div => IntegerOp::Div,
303        _ => unreachable!(
304            "Unknown rule for operator {:?}: {}",
305            pair.as_rule(),
306            pair.as_str()
307        ),
308    }
309}
310/// Parses a constraint of the form
311///     `Cardinality({p \in Processes : ProcessesLocations[p] = "loc0"})`
312/// into an `IntegerExpression::Atom(Location::new("loc0"))`
313///
314/// This function panics if you attempt to parse it into a type other then
315/// `IntegerExpression<Location`
316fn parse_cardinality_expr<T>(pair: Pair<'_, Rule>) -> Result<IntegerExpression<T>, anyhow::Error>
317where
318    T: Atomic + 'static,
319{
320    debug_assert!(
321        pair.as_rule() == Rule::cardinality_expr,
322        "Got rule {:?} for {}",
323        pair.as_rule(),
324        pair.as_str()
325    );
326
327    // Cardinality constraints are a special case.
328    // We only support parsing them into a location
329    if TypeId::of::<T>() != TypeId::of::<Location>() {
330        let parse_err = new_parsing_error(
331            "Cardinality constraint can only be parsed into a constraint over locations.",
332            pair.as_span(),
333        );
334        return Err(parse_err).with_context(|| "Error while parsing cardinality");
335    }
336
337    let mut inner_pairs = pair.into_inner();
338
339    let elem_pair = inner_pairs.next().expect("Missing: Process identifier");
340    let elem_ident: String = parse_identifier_to_t(&elem_pair);
341
342    let set_ident_pair = inner_pairs.next().expect("Missing: Process set identifier");
343    let set_ident: String = parse_identifier_to_t(&set_ident_pair);
344    if set_ident != PROC_SET {
345        let parse_err = new_parsing_error(
346            format!("Cardinality constraint should be over the set of processes '{PROC_SET}'"),
347            set_ident_pair.as_span(),
348        );
349        return Err(parse_err).with_context(|| "Error while parsing cardinality constraint: ");
350    }
351
352    let set_locs: Vec<T> = inner_pairs
353        .map(|p| try_parse_map_entry_constr_loc(p, &elem_ident))
354        .collect::<Result<Vec<_>, _>>()
355        .with_context(|| "Error while parsing cardinality constraint: ")?;
356
357    debug_assert!(!set_locs.is_empty());
358
359    let mut it_set_locs = set_locs.into_iter();
360    let first = IntegerExpression::Atom(it_set_locs.next().unwrap());
361    let res = it_set_locs.fold(first, |acc, x| {
362        IntegerExpression::BinaryExpr(
363            Box::new(acc),
364            IntegerOp::Add,
365            Box::new(IntegerExpression::Atom(x)),
366        )
367    });
368
369    Ok(res)
370}
371
372/// Parse integer atom
373///
374/// Returns an integer expression if the pair is a constant, known identifier,
375/// cardinality expression or could be parsed to an expression.
376///
377/// Returns an error if the identifier was not declared with the identifier name
378fn parse_integer_atom<T, U>(
379    pair: Pair<'_, Rule>,
380    builder: &U,
381    ctx: &TLAParsingContext,
382) -> Result<IntegerExpression<T>, anyhow::Error>
383where
384    T: Atomic + 'static,
385    U: IsDeclared<T> + IsDeclared<Parameter>,
386{
387    debug_assert!(
388        pair.as_rule() == Rule::integer_atom,
389        "Got rule {:?} for {}",
390        pair.as_rule(),
391        pair.as_str()
392    );
393
394    let pair = pair.into_inner().next().unwrap();
395
396    match pair.as_rule() {
397        Rule::integer_const => Ok(IntegerExpression::Const(parse_integer_const(pair))),
398        Rule::identifier => {
399            // Check whether an integer macro has been declared
400            let name: String = parse_identifier_to_t(&pair);
401            if ctx.int_macro.contains_key(&name) {
402                return parse_integer_expr(ctx.int_macro[&name].clone(), builder, ctx);
403            }
404
405            // Try to parse it into the atom and check whether it is declared
406            let atom = parse_identifier_to_t(&pair);
407            if builder.is_declared(&atom) {
408                return Ok(IntegerExpression::Atom(atom));
409            }
410
411            // Try to parse it into the atom and check whether it is declared
412            let param = parse_identifier_to_t(&pair);
413            if builder.is_declared(&param) || pair.as_str() == N_CORR_PROC {
414                return Ok(IntegerExpression::Param(param));
415            }
416
417            let parse_err = new_parsing_error(
418                format!("Unknown identifier: '{}'", pair.as_str()),
419                pair.as_span(),
420            );
421
422            Err(parse_err).with_context(|| "Failed to parse integer expression: ")
423        }
424        Rule::integer_expr => parse_integer_expr(pair, builder, ctx),
425        Rule::cardinality_expr => parse_cardinality_expr(pair),
426        _ => unreachable!(
427            "Unknown integer atom {:#?} : {}",
428            pair.as_rule(),
429            pair.as_str()
430        ),
431    }
432}
433
434/// Parse expression over integers into an integer expression
435fn parse_integer_expr<T, U>(
436    pair: Pair<'_, Rule>,
437    builder: &U,
438    ctx: &TLAParsingContext,
439) -> Result<IntegerExpression<T>, anyhow::Error>
440where
441    T: Atomic + 'static,
442    U: IsDeclared<T> + IsDeclared<Parameter>,
443{
444    debug_assert!(
445        pair.as_rule() == Rule::integer_expr,
446        "Got rule {:?} for {}",
447        pair.as_rule(),
448        pair.as_str()
449    );
450    let pairs = pair.into_inner();
451
452    PRATT_PARSER
453        .map_primary(|atom| parse_integer_atom(atom, builder, ctx))
454        .map_infix(|lhs, op, rhs| {
455            let op = parse_integer_binary_op(op);
456
457            Ok(IntegerExpression::BinaryExpr(
458                Box::new(lhs?),
459                op,
460                Box::new(rhs?),
461            ))
462        })
463        .map_prefix(|op, rhs| match op.as_rule() {
464            Rule::negation => Ok(IntegerExpression::Neg(Box::new(rhs?))),
465            _ => unreachable!(
466                "Unknown integer unary operator {:?}: {}",
467                op.as_rule(),
468                op.as_str()
469            ),
470        })
471        .parse(pairs)
472}
473
474/// Parse boolean constant
475#[inline(always)]
476fn parse_boolean_const<T: Atomic>(pair: Pair<'_, Rule>) -> BooleanExpression<T> {
477    debug_assert!(
478        pair.as_rule() == Rule::bool_const,
479        "Got rule {:?} for {}",
480        pair.as_rule(),
481        pair.as_str()
482    );
483
484    let pair = pair
485        .into_inner()
486        .next()
487        .expect("Expected boolean constant to be non-empty");
488
489    match pair.as_rule() {
490        Rule::bool_true => BooleanExpression::True,
491        Rule::bool_false => BooleanExpression::False,
492        _ => unreachable!(
493            "Unexpected rule for boolean constant {:?}: {}",
494            pair.as_rule(),
495            pair.as_str()
496        ),
497    }
498}
499
500/// Parse boolean connectives
501#[inline(always)]
502fn parse_boolean_con(pair: Pair<'_, Rule>) -> BooleanConnective {
503    match pair.as_rule() {
504        Rule::and => BooleanConnective::And,
505        Rule::or => BooleanConnective::Or,
506        _ => unreachable!(
507            "Unknown rule for boolean connective {:?}: {}",
508            pair.as_rule(),
509            pair.as_str()
510        ),
511    }
512}
513
514/// Parse comparison operator
515#[inline(always)]
516fn parse_comparison_op(pair: Pair<'_, Rule>) -> ComparisonOp {
517    match pair.as_rule() {
518        Rule::equal => ComparisonOp::Eq,
519        Rule::not_equal => ComparisonOp::Neq,
520        Rule::less_eq => ComparisonOp::Leq,
521        Rule::less => ComparisonOp::Lt,
522        Rule::greater_eq => ComparisonOp::Geq,
523        Rule::greater => ComparisonOp::Gt,
524        _ => unreachable!(
525            "Unknown rule for comparison operator {:?}: {}",
526            pair.as_rule(),
527            pair.as_str()
528        ),
529    }
530}
531
532/// Intermediate type for comparison expression of the form `lhs op rhs`
533type CompExpr<T> = (IntegerExpression<T>, ComparisonOp, IntegerExpression<T>);
534
535/// Parse a pair of type `comparison_expr` into a [CompExpr]
536pub fn parse_comparison_expr<T, U>(
537    pair: Pair<'_, Rule>,
538    builder: &U,
539    ctx: &TLAParsingContext,
540) -> Result<CompExpr<T>, anyhow::Error>
541where
542    T: Atomic + 'static,
543    U: IsDeclared<T> + IsDeclared<Parameter>,
544{
545    debug_assert!(
546        pair.as_rule() == Rule::comparison_expr,
547        "Got rule {:?} for {}",
548        pair.as_rule(),
549        pair.as_str()
550    );
551
552    let mut pairs = pair.into_inner();
553
554    let lhs = parse_integer_expr(pairs.next().unwrap(), builder, ctx)?;
555    let op = parse_comparison_op(pairs.next().unwrap());
556    let rhs = parse_integer_expr(pairs.next().unwrap(), builder, ctx)?;
557
558    Ok((lhs, op, rhs))
559}
560
561/// Parse an expression of type `int_bool_expr` into a `BooleanExpression`
562pub(crate) fn parse_int_boolean_expr<T, U>(
563    pair: Pair<'_, Rule>,
564    builder: &U,
565    ctx: &TLAParsingContext,
566) -> Result<BooleanExpression<T>, anyhow::Error>
567where
568    T: Atomic + 'static,
569    U: IsDeclared<T> + IsDeclared<Parameter>,
570{
571    debug_assert!(
572        pair.as_rule() == Rule::int_bool_expr,
573        "Got rule {:?} for {}",
574        pair.as_rule(),
575        pair.as_str()
576    );
577
578    let pairs = pair.into_inner();
579
580    // utilize the precedence parser
581    PRATT_PARSER
582        .map_primary(|atom| parse_boolean_atom(atom, builder, ctx))
583        .map_infix(|lhs, op, rhs| {
584            let op = parse_boolean_con(op);
585
586            Ok(BooleanExpression::BinaryExpression(
587                Box::new(lhs?),
588                op,
589                Box::new(rhs?),
590            ))
591        })
592        .map_prefix(|op, rhs| match op.as_rule() {
593            Rule::not => Ok(BooleanExpression::Not(Box::new(rhs?))),
594            _ => unreachable!(
595                "Unknown boolean unary operator {:?}: {}",
596                op.as_rule(),
597                op.as_str()
598            ),
599        })
600        .parse(pairs)
601}
602
603/// Parse an assignment expression of an action into the corresponding list of
604/// actions
605fn parse_assignment_expression<T>(
606    pair: Pair<'_, Rule>,
607    builder: &T,
608    ctx: &TLAParsingContext,
609) -> Result<Vec<Action>, Box<pest::error::Error<()>>>
610where
611    T: IsDeclared<Variable> + IsDeclared<Parameter>,
612{
613    debug_assert!(
614        pair.as_rule() == Rule::assignment_expr,
615        "Got rule {:?} for {}",
616        pair.as_rule(),
617        pair.as_str()
618    );
619    let span = pair.as_span();
620
621    let mut pairs = pair.into_inner();
622    let pair = pairs.next().unwrap();
623
624    let var = parse_identifier_to_t(&pair);
625    if !builder.is_declared(&var) {
626        return Err(new_parsing_error(
627            format!("Failed to parse action: Unknown identifier: {var}"),
628            span,
629        ));
630    }
631
632    let expr = parse_integer_expr(pairs.next().unwrap(), builder, ctx)
633        .map_err(|err| new_parsing_error(format!("Failed to parse action: {err}"), span))?;
634
635    let act = Action::new(var, expr);
636
637    if let Err(err) = act {
638        return Err(new_parsing_error(
639            format!("Failed to parse effect of action: {err}"),
640            span,
641        ));
642    }
643
644    Ok(vec![act.unwrap()])
645}
646
647/// Parse a pair of type `integer_update` into an [Action]
648pub(crate) fn parse_integer_update_expr<T>(
649    pair: Pair<'_, Rule>,
650    builder: &T,
651    ctx: &TLAParsingContext,
652) -> Result<Vec<Action>, Box<pest::error::Error<()>>>
653where
654    T: IsDeclared<Variable> + IsDeclared<Parameter>,
655{
656    debug_assert!(
657        pair.as_rule() == Rule::integer_update,
658        "Got rule {:?} for {}",
659        pair.as_rule(),
660        pair.as_str()
661    );
662
663    let pair = pair.into_inner().next().unwrap();
664
665    match pair.as_rule() {
666        Rule::unchanged_expr => Ok(vec![]),
667        Rule::assignment_expr => parse_assignment_expression(pair, builder, ctx),
668        _ => unreachable!(
669            "Unknown rule for action expression {:?}: {}",
670            pair.as_rule(),
671            pair.as_str()
672        ),
673    }
674}
675
676#[cfg(test)]
677mod tests {
678
679    use pest::Parser;
680    use taco_model_checker::eltl::ELTLExpression;
681    use taco_threshold_automaton::{
682        expressions::{
683            BooleanConnective, BooleanExpression, ComparisonOp, IntegerExpression, IntegerOp,
684            Location, Parameter, Variable,
685        },
686        general_threshold_automaton::{Action, builder::GeneralThresholdAutomatonBuilder},
687    };
688
689    use crate::tla::{
690        PestTLAParser, Rule, TLAParsingContext,
691        integer_exprs::{
692            parse_cardinality_expr, parse_int_boolean_expr, parse_integer_const,
693            parse_integer_update_expr, parse_ltl_specification,
694        },
695    };
696
697    #[test]
698    fn test_parse_integer_const() {
699        let input = "42";
700
701        let mut pairs = PestTLAParser::parse(Rule::integer_const, input).unwrap();
702        let pair = pairs.next().unwrap();
703
704        let loc = parse_integer_const(pair);
705
706        assert_eq!(loc, 42);
707    }
708
709    #[test]
710    fn test_parse_int_bool() {
711        let input = "var1 = 42";
712
713        let mut pairs = PestTLAParser::parse(Rule::int_bool_expr, input).unwrap();
714        let pair = pairs.next().unwrap();
715
716        let builder = GeneralThresholdAutomatonBuilder::new("test")
717            .with_variable(Variable::new("var1"))
718            .unwrap()
719            .initialize();
720
721        let ctx = TLAParsingContext::new();
722
723        let loc = parse_int_boolean_expr(pair, &builder, &ctx).unwrap();
724
725        assert_eq!(
726            loc,
727            BooleanExpression::ComparisonExpression(
728                Box::new(IntegerExpression::Atom(Variable::new("var1"))),
729                ComparisonOp::Eq,
730                Box::new(IntegerExpression::Const(42))
731            )
732        );
733    }
734
735    #[test]
736    fn test_parse_int_bool_div() {
737        let input = "var1 <= 42 / -2";
738
739        let mut pairs = PestTLAParser::parse(Rule::int_bool_expr, input).unwrap();
740        let pair = pairs.next().unwrap();
741
742        let builder = GeneralThresholdAutomatonBuilder::new("test")
743            .with_variable(Variable::new("var1"))
744            .unwrap()
745            .initialize();
746
747        let ctx = TLAParsingContext::new();
748
749        let loc = parse_int_boolean_expr(pair, &builder, &ctx).unwrap();
750
751        assert_eq!(
752            loc,
753            BooleanExpression::ComparisonExpression(
754                Box::new(IntegerExpression::Atom(Variable::new("var1"))),
755                ComparisonOp::Leq,
756                Box::new(IntegerExpression::BinaryExpr(
757                    Box::new(IntegerExpression::Const(42)),
758                    IntegerOp::Div,
759                    Box::new(IntegerExpression::Neg(Box::new(IntegerExpression::Const(
760                        2
761                    ))))
762                ))
763            )
764        );
765    }
766
767    #[test]
768    fn test_parse_int_bool_const() {
769        let input = "TRUE";
770
771        let mut pairs = PestTLAParser::parse(Rule::int_bool_expr, input).unwrap();
772        let pair = pairs.next().unwrap();
773
774        let builder = GeneralThresholdAutomatonBuilder::new("test").initialize();
775
776        let ctx = TLAParsingContext::new();
777
778        let loc: BooleanExpression<Variable> =
779            parse_int_boolean_expr(pair, &builder, &ctx).unwrap();
780
781        assert_eq!(loc, BooleanExpression::True);
782
783        let input = "FALSE";
784
785        let mut pairs = PestTLAParser::parse(Rule::int_bool_expr, input).unwrap();
786        let pair = pairs.next().unwrap();
787
788        let builder = GeneralThresholdAutomatonBuilder::new("test").initialize();
789
790        let ctx = TLAParsingContext::new();
791
792        let loc: BooleanExpression<Variable> =
793            parse_int_boolean_expr(pair, &builder, &ctx).unwrap();
794
795        assert_eq!(loc, BooleanExpression::False);
796    }
797
798    #[test]
799    fn test_parse_int_bool_disj_conj() {
800        let input = "TRUE \\/ FALSE";
801
802        let mut pairs = PestTLAParser::parse(Rule::int_bool_expr, input).unwrap();
803        let pair = pairs.next().unwrap();
804
805        let builder = GeneralThresholdAutomatonBuilder::new("test").initialize();
806
807        let ctx = TLAParsingContext::new();
808
809        let loc: BooleanExpression<Variable> =
810            parse_int_boolean_expr(pair, &builder, &ctx).unwrap();
811
812        assert_eq!(
813            loc,
814            BooleanExpression::BinaryExpression(
815                Box::new(BooleanExpression::True),
816                BooleanConnective::Or,
817                Box::new(BooleanExpression::False)
818            )
819        );
820
821        let input = "TRUE /\\ FALSE";
822
823        let mut pairs = PestTLAParser::parse(Rule::int_bool_expr, input).unwrap();
824        let pair = pairs.next().unwrap();
825
826        let builder = GeneralThresholdAutomatonBuilder::new("test").initialize();
827
828        let ctx = TLAParsingContext::new();
829
830        let loc: BooleanExpression<Variable> =
831            parse_int_boolean_expr(pair, &builder, &ctx).unwrap();
832
833        assert_eq!(
834            loc,
835            BooleanExpression::BinaryExpression(
836                Box::new(BooleanExpression::True),
837                BooleanConnective::And,
838                Box::new(BooleanExpression::False)
839            )
840        );
841
842        let input = "~(TRUE /\\ FALSE)";
843
844        let mut pairs = PestTLAParser::parse(Rule::int_bool_expr, input).unwrap();
845        let pair = pairs.next().unwrap();
846
847        let builder = GeneralThresholdAutomatonBuilder::new("test").initialize();
848
849        let ctx = TLAParsingContext::new();
850
851        let loc: BooleanExpression<Variable> =
852            parse_int_boolean_expr(pair, &builder, &ctx).unwrap();
853
854        assert_eq!(
855            loc,
856            BooleanExpression::Not(Box::new(BooleanExpression::BinaryExpression(
857                Box::new(BooleanExpression::True),
858                BooleanConnective::And,
859                Box::new(BooleanExpression::False)
860            )))
861        );
862    }
863
864    #[test]
865    fn test_parse_int_update() {
866        let input = "var1' = var1 + (42 + 0)";
867
868        let mut pairs = PestTLAParser::parse(Rule::integer_update, input).unwrap();
869        let pair = pairs.next().unwrap();
870
871        let builder = GeneralThresholdAutomatonBuilder::new("test")
872            .with_variable(Variable::new("var1"))
873            .unwrap()
874            .initialize();
875
876        let ctx = TLAParsingContext::new();
877
878        let loc = parse_integer_update_expr(pair, &builder, &ctx).unwrap();
879
880        assert_eq!(
881            loc,
882            vec![
883                Action::new(
884                    Variable::new("var1"),
885                    IntegerExpression::BinaryExpr(
886                        Box::new(IntegerExpression::Atom(Variable::new("var1"))),
887                        IntegerOp::Add,
888                        Box::new(IntegerExpression::Const(42)),
889                    )
890                )
891                .unwrap()
892            ]
893        );
894    }
895
896    #[test]
897    fn test_parse_int_update_err() {
898        let input = "var1' = unknown";
899
900        let mut pairs = PestTLAParser::parse(Rule::integer_update, input).unwrap();
901        let pair = pairs.next().unwrap();
902
903        let builder = GeneralThresholdAutomatonBuilder::new("test")
904            .with_variable(Variable::new("var1"))
905            .unwrap()
906            .initialize();
907
908        let ctx = TLAParsingContext::new();
909
910        let loc = parse_integer_update_expr(pair, &builder, &ctx);
911        assert!(loc.is_err(), "Got: {:?}", loc.unwrap());
912    }
913
914    #[test]
915    fn test_parse_cardinality() {
916        let input = "Cardinality({p \\in Processes : ProcessesLocations[p] = \"loc0\"})";
917
918        let mut pairs = PestTLAParser::parse(Rule::cardinality_expr, input).unwrap();
919        let pair = pairs.next().unwrap();
920
921        let loc = parse_cardinality_expr(pair).unwrap();
922
923        assert_eq!(loc, IntegerExpression::Atom(Location::new("loc0")));
924    }
925
926    #[test]
927    fn test_parse_cardinality_err_on_unkown_proc() {
928        let input = "Cardinality({p \\in Something : ProcessesLocations[p] = \"loc0\"})";
929
930        let mut pairs = PestTLAParser::parse(Rule::cardinality_expr, input).unwrap();
931        let pair = pairs.next().unwrap();
932
933        let loc: Result<IntegerExpression<Location>, anyhow::Error> = parse_cardinality_expr(pair);
934        assert!(loc.is_err())
935    }
936
937    #[test]
938    fn test_parse_cardinality_disj() {
939        let input = "Cardinality({p \\in Processes : ProcessesLocations[p] = \"loc0\" \\/ ProcessesLocations[p] = \"loc1\"})";
940
941        let mut pairs = PestTLAParser::parse(Rule::cardinality_expr, input).unwrap();
942        let pair = pairs.next().unwrap();
943
944        let loc = parse_cardinality_expr(pair).unwrap();
945
946        assert_eq!(
947            loc,
948            IntegerExpression::BinaryExpr(
949                Box::new(IntegerExpression::Atom(Location::new("loc0"))),
950                IntegerOp::Add,
951                Box::new(IntegerExpression::Atom(Location::new("loc1")))
952            )
953        );
954    }
955
956    #[test]
957    #[should_panic]
958    fn test_parse_card_param_panics() {
959        let input = "Cardinality({p \\in Processes : ProcessesLocations[p] = \"loc0\"})";
960
961        let mut pairs = PestTLAParser::parse(Rule::cardinality_expr, input).unwrap();
962        let pair = pairs.next().unwrap();
963
964        let loc = parse_cardinality_expr(pair).unwrap();
965
966        assert_eq!(loc, IntegerExpression::Atom(Parameter::new("loc0")));
967    }
968
969    #[test]
970    fn test_ltl_spec_parses() {
971        let input = "unforg == 
972        var1 = 0 => ([] (loc0 = 0) \\/ ~(<>( Cardinality({p \\in Processes : ProcessesLocations[p] = \"loc0\"}) > 1)))
973        ";
974
975        let mut pairs = PestTLAParser::parse(Rule::ltl_spec_declaration, input).unwrap();
976
977        let builder = GeneralThresholdAutomatonBuilder::new("test")
978            .with_variable(Variable::new("var1"))
979            .unwrap()
980            .with_location(Location::new("loc0"))
981            .unwrap()
982            .initialize();
983
984        let ctx = TLAParsingContext::new();
985
986        let got_ltl_spec = parse_ltl_specification(pairs.next().unwrap(), &builder, &ctx).unwrap();
987
988        let expected_ltl_spec = (
989            "unforg".to_string(),
990            ELTLExpression::Implies(
991                Box::new(ELTLExpression::VariableExpr(
992                    Box::new(IntegerExpression::Atom(Variable::new("var1"))),
993                    ComparisonOp::Eq,
994                    Box::new(IntegerExpression::Const(0)),
995                )),
996                Box::new(ELTLExpression::Or(
997                    Box::new(ELTLExpression::Globally(Box::new(
998                        ELTLExpression::LocationExpr(
999                            Box::new(IntegerExpression::Atom(Location::new("loc0"))),
1000                            ComparisonOp::Eq,
1001                            Box::new(IntegerExpression::Const(0)),
1002                        ),
1003                    ))),
1004                    Box::new(ELTLExpression::Not(Box::new(ELTLExpression::Eventually(
1005                        Box::new(ELTLExpression::LocationExpr(
1006                            Box::new(IntegerExpression::Atom(Location::new("loc0"))),
1007                            ComparisonOp::Gt,
1008                            Box::new(IntegerExpression::Const(1)),
1009                        )),
1010                    )))),
1011                )),
1012            ),
1013        );
1014
1015        assert_eq!(got_ltl_spec, expected_ltl_spec)
1016    }
1017
1018    #[test]
1019    fn test_ltl_spec_parses_bool_const() {
1020        let input = "unforg == TRUE
1021        ";
1022
1023        let mut pairs = PestTLAParser::parse(Rule::ltl_spec_declaration, input).unwrap();
1024
1025        let builder = GeneralThresholdAutomatonBuilder::new("test")
1026            .with_variable(Variable::new("var1"))
1027            .unwrap()
1028            .with_location(Location::new("loc0"))
1029            .unwrap()
1030            .initialize();
1031
1032        let ctx = TLAParsingContext::new();
1033
1034        let got_ltl_spec = parse_ltl_specification(pairs.next().unwrap(), &builder, &ctx).unwrap();
1035
1036        let expected_ltl_spec = ("unforg".to_string(), ELTLExpression::True);
1037
1038        assert_eq!(got_ltl_spec, expected_ltl_spec);
1039
1040        let input = "unforg == FALSE
1041        ";
1042
1043        let mut pairs = PestTLAParser::parse(Rule::ltl_spec_declaration, input).unwrap();
1044
1045        let builder = GeneralThresholdAutomatonBuilder::new("test")
1046            .with_variable(Variable::new("var1"))
1047            .unwrap()
1048            .with_location(Location::new("loc0"))
1049            .unwrap()
1050            .initialize();
1051
1052        let ctx = TLAParsingContext::new();
1053
1054        let got_ltl_spec = parse_ltl_specification(pairs.next().unwrap(), &builder, &ctx).unwrap();
1055
1056        let expected_ltl_spec = ("unforg".to_string(), ELTLExpression::False);
1057
1058        assert_eq!(got_ltl_spec, expected_ltl_spec)
1059    }
1060}
taco_parser/tla/integer_exprs.rs

taco_parser/tla/
integer_exprs.rs
