Rewrite ATL parsing for better parse errors and more flexibility

cgaal-cli/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "cgaal"
-version = "1.0.0"
+version = "1.0.1"
 authors = [
     "d702e20 <[email protected]>",
     "d802f21 <[email protected]>",
@@ -26,4 +26,4 @@ tracing-subscriber = "0.2.17"
 serde_json = "1.0.83"
 regex = { version = "1", features = ["unicode-case"] }
 humantime = "2.1.0"
-cgaal-engine = { path = "../cgaal-engine", version = "1.0.0" }
+cgaal-engine = { path = "../cgaal-engine", version = "1.0.1" }

cgaal-cli/src/main.rs

@@ -18,7 +18,8 @@ use tracing::trace;
 use cgaal_engine::algorithms::global::multithread::MultithreadedGlobalAlgorithm;
 use cgaal_engine::algorithms::global::singlethread::SinglethreadedGlobalAlgorithm;
 use cgaal_engine::analyse::analyse;
-use cgaal_engine::atl::{AtlExpressionParser, Phi};
+use cgaal_engine::atl::convert::convert_expr_to_phi;
+use cgaal_engine::atl::Phi;
 use cgaal_engine::edg::atledg::vertex::AtlVertex;
 use cgaal_engine::edg::atledg::AtlDependencyGraph;
 use cgaal_engine::edg::ExtendedDependencyGraph;
@@ -27,6 +28,8 @@ use cgaal_engine::game_structure::lcgs::ir::intermediate::IntermediateLcgs;
 use cgaal_engine::game_structure::lcgs::ir::symbol_table::Owner;
 use cgaal_engine::game_structure::lcgs::parse::parse_lcgs;
 use cgaal_engine::game_structure::{EagerGameStructure, GameStructure};
+use cgaal_engine::parsing::errors::ErrorLog;
+use cgaal_engine::parsing::parse_atl;
 #[cfg(feature = "graph-printer")]
 use cgaal_engine::printer::print_graph;
 
@@ -335,11 +338,7 @@ fn main_inner() -> Result<(), String> {
 /// Reads a formula in JSON format from a file and returns the formula as a string
 /// and as a parsed Phi struct.
 /// This function will exit the program if it encounters an error.
-fn load_formula<A: AtlExpressionParser>(
-    path: &str,
-    formula_type: FormulaType,
-    expr_parser: &A,
-) -> Phi {
+fn load_formula(path: &str, formula_type: FormulaType, game: Option<&IntermediateLcgs>) -> Phi {
     let mut file = File::open(path).unwrap_or_else(|err| {
         eprintln!("Failed to open formula file\n\nError:\n{}", err);
         exit(1);
@@ -357,11 +356,20 @@ fn load_formula<A: AtlExpressionParser>(
             exit(1);
         }),
         FormulaType::Atl => {
-            let result = cgaal_engine::atl::parse_phi(expr_parser, &raw_phi);
-            result.unwrap_or_else(|err| {
-                eprintln!("Invalid ATL formula provided:\n\n{}", err);
+            let game = game.unwrap_or_else(|| {
+                eprintln!("Cannot use ATL formula for non-LCGS models");
                 exit(1)
-            })
+            });
+            let mut errors = ErrorLog::new();
+            parse_atl(&raw_phi, &mut errors)
+                .and_then(|expr| convert_expr_to_phi(&expr, game, &mut errors))
+                .unwrap_or_else(|| {
+                    eprint!(
+                        "Invalid ATL formula provided:\n{}",
+                        errors.to_string(&raw_phi)
+                    );
+                    exit(1)
+                })
         }
     }
 }
@@ -457,7 +465,7 @@ fn load(
             let game_structure = serde_json::from_str(content.as_str())
                 .map_err(|err| format!("Failed to deserialize input model.\n{}", err))?;
 
-            let phi = load_formula(formula_path, formula_format, &game_structure);
+            let phi = load_formula(formula_path, formula_format, None);
 
             Ok(ModelAndFormula::Json {
                 model: game_structure,
@@ -471,7 +479,7 @@ fn load(
             let game_structure = IntermediateLcgs::create(lcgs)
                 .map_err(|err| format!("Invalid LCGS program.\n{}", err))?;
 
-            let phi = load_formula(formula_path, formula_format, &game_structure);
+            let phi = load_formula(formula_path, formula_format, Some(&game_structure));
 
             Ok(ModelAndFormula::Lcgs {
                 model: game_structure,

cgaal-engine/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "cgaal-engine"
-version = "1.0.0"
+version = "1.0.1"
 authors = [
     "Asger Weirsøe <[email protected]>",
     "Falke Carlsen <[email protected]>",

cgaal-engine/src/atl/convert.rs

@@ -0,0 +1,244 @@
+use crate::atl::Phi;
+use crate::game_structure::lcgs::ast::DeclKind;
+use crate::game_structure::lcgs::ir::intermediate::IntermediateLcgs;
+use crate::game_structure::lcgs::ir::symbol_table::Owner;
+use crate::game_structure::Player;
+use crate::parsing::ast::{BinaryOpKind, Coalition, CoalitionKind, Expr, ExprKind, UnaryOpKind};
+use crate::parsing::errors::ErrorLog;
+
+/// Convert an ATL expression to a Phi formula.
+/// Players and labels must be defined in the game and are compiled to their respective indexes.
+/// Returns None if there were errors. See the error log for details.
+pub fn convert_expr_to_phi(
+    expr: &Expr,
+    game: &IntermediateLcgs,
+    errors: &mut ErrorLog,
+) -> Option<Phi> {
+    let Expr { span, kind } = expr;
+    match kind {
+        ExprKind::True => Some(Phi::True),
+        ExprKind::False => Some(Phi::False),
+        ExprKind::Paren(e) => convert_expr_to_phi(e, game, errors),
+        ExprKind::Ident(ident) => {
+            let decl = game.get_decl(&Owner::Global.symbol_id(ident));
+            match &decl.map(|d| &d.kind) {
+                Some(DeclKind::Label(l)) => Some(Phi::Proposition(l.index)),
+                Some(d) => {
+                    errors.log(
+                        *span,
+                        format!(
+                            "Expected proposition label, '{}' is a {}",
+                            ident,
+                            d.kind_name()
+                        ),
+                    );
+                    None
+                }
+                None => {
+                    errors.log(
+                        *span,
+                        format!("Expected proposition label, '{}' is not defined", ident),
+                    );
+                    None
+                }
+            }
+        }
+        ExprKind::Unary(op, e) => match op {
+            UnaryOpKind::Not => Some(Phi::Not(convert_expr_to_phi(e, game, errors)?.into())),
+            UnaryOpKind::Next | UnaryOpKind::Eventually | UnaryOpKind::Invariantly => {
+                errors.log(
+                    *span,
+                    "Temporal operators are only allowed after a coalition".to_string(),
+                );
+                None
+            }
+        },
+        ExprKind::Binary(op, lhs, rhs) => match op {
+            BinaryOpKind::And => Some(Phi::And(
+                convert_expr_to_phi(lhs, game, errors)?.into(),
+                convert_expr_to_phi(rhs, game, errors)?.into(),
+            )),
+            BinaryOpKind::Or => Some(Phi::Or(
+                convert_expr_to_phi(lhs, game, errors)?.into(),
+                convert_expr_to_phi(rhs, game, errors)?.into(),
+            )),
+            BinaryOpKind::Dot => {
+                let ExprKind::Ident(owner) = &lhs.kind else {
+                    errors.log(lhs.span, "Expected player name".to_string());
+                    return None;
+                };
+                let ExprKind::Ident(prop) = &rhs.kind else {
+                    errors.log(rhs.span, "Expected proposition label".to_string());
+                    return None;
+                };
+                match game
+                    .get_decl(&Owner::Global.symbol_id(owner))
+                    .map(|d| &d.kind)
+                {
+                    Some(DeclKind::Player(_)) => {
+                        let symb = Owner::Player(owner.clone()).symbol_id(prop);
+                        let decl = game.get_decl(&symb);
+                        match decl.map(|d| &d.kind) {
+                            Some(DeclKind::Label(l)) => Some(Phi::Proposition(l.index)),
+                            Some(d) => {
+                                errors.log(
+                                    rhs.span,
+                                    format!(
+                                        "Expected proposition label, '{}' is a {}",
+                                        prop,
+                                        d.kind_name(),
+                                    ),
+                                );
+                                None
+                            }
+                            None => {
+                                errors.log(
+                                    rhs.span,
+                                    format!(
+                                        "Expected proposition label, '{}' is not defined",
+                                        symb,
+                                    ),
+                                );
+                                None
+                            }
+                        }
+                    }
+                    Some(d) => {
+                        errors.log(
+                            lhs.span,
+                            format!("Expected player, '{}' is a {}", owner, d.kind_name()),
+                        );
+                        None
+                    }
+                    None => {
+                        errors.log(
+                            lhs.span,
+                            format!("Expected player, '{}' is not defined", owner),
+                        );
+                        None
+                    }
+                }
+            }
+            BinaryOpKind::Until => {
+                errors.log(
+                    *span,
+                    "Temporal operators are only allowed after a coalition".to_string(),
+                );
+                None
+            }
+        },
+        ExprKind::Coalition(Coalition {
+            players,
+            kind,
+            expr: path_expr,
+            ..
+        }) => match (kind, &path_expr.kind) {
+            (CoalitionKind::Enforce, ExprKind::Unary(UnaryOpKind::Next, sub_expr)) => {
+                let phi = convert_expr_to_phi(sub_expr, game, errors)?;
+                Some(Phi::EnforceNext {
+                    players: convert_players(players, game, errors)?,
+                    formula: phi.into(),
+                })
+            }
+            (CoalitionKind::Despite, ExprKind::Unary(UnaryOpKind::Next, sub_expr)) => {
+                let phi = convert_expr_to_phi(sub_expr, game, errors)?;
+                Some(Phi::DespiteNext {
+                    players: convert_players(players, game, errors)?,
+                    formula: phi.into(),
+                })
+            }
+            (CoalitionKind::Enforce, ExprKind::Unary(UnaryOpKind::Eventually, sub_expr)) => {
+                let phi = convert_expr_to_phi(sub_expr, game, errors)?;
+                Some(Phi::EnforceEventually {
+                    players: convert_players(players, game, errors)?,
+                    formula: phi.into(),
+                })
+            }
+            (CoalitionKind::Despite, ExprKind::Unary(UnaryOpKind::Eventually, sub_expr)) => {
+                let phi = convert_expr_to_phi(sub_expr, game, errors)?;
+                Some(Phi::DespiteEventually {
+                    players: convert_players(players, game, errors)?,
+                    formula: phi.into(),
+                })
+            }
+            (CoalitionKind::Enforce, ExprKind::Unary(UnaryOpKind::Invariantly, sub_expr)) => {
+                let phi = convert_expr_to_phi(sub_expr, game, errors)?;
+                Some(Phi::EnforceInvariant {
+                    players: convert_players(players, game, errors)?,
+                    formula: phi.into(),
+                })
+            }
+            (CoalitionKind::Despite, ExprKind::Unary(UnaryOpKind::Invariantly, sub_expr)) => {
+                let phi = convert_expr_to_phi(sub_expr, game, errors)?;
+                Some(Phi::DespiteInvariant {
+                    players: convert_players(players, game, errors)?,
+                    formula: phi.into(),
+                })
+            }
+            (CoalitionKind::Enforce, ExprKind::Binary(BinaryOpKind::Until, lhs, rhs)) => {
+                let lhs_phi = convert_expr_to_phi(lhs, game, errors)?;
+                let rhs_phi = convert_expr_to_phi(rhs, game, errors)?;
+                Some(Phi::EnforceUntil {
+                    players: convert_players(players, game, errors)?,
+                    pre: lhs_phi.into(),
+                    until: rhs_phi.into(),
+                })
+            }
+            (CoalitionKind::Despite, ExprKind::Binary(BinaryOpKind::Until, lhs, rhs)) => {
+                let lhs_phi = convert_expr_to_phi(lhs, game, errors)?;
+                let rhs_phi = convert_expr_to_phi(rhs, game, errors)?;
+                Some(Phi::DespiteUntil {
+                    players: convert_players(players, game, errors)?,
+                    pre: lhs_phi.into(),
+                    until: rhs_phi.into(),
+                })
+            }
+            _ => {
+                errors.log(
+                    path_expr.span,
+                    "Coalitions must be followed by a path formula".to_string(),
+                );
+                None
+            }
+        },
+        ExprKind::Error => None,
+    }
+}
+
+/// Helper function for converting a list of player names to a list of player indexes.
+/// Returns None if there were errors. See the error log for details.
+fn convert_players(
+    players: &[Expr],
+    game: &IntermediateLcgs,
+    errors: &mut ErrorLog,
+) -> Option<Vec<Player>> {
+    players
+        .iter()
+        .map(|expr| match &expr.kind {
+            ExprKind::Ident(name) => match game
+                .get_decl(&Owner::Global.symbol_id(name))
+                .map(|d| &d.kind)
+            {
+                Some(DeclKind::Player(p)) => Some(p.index),
+                Some(d) => {
+                    errors.log(
+                        expr.span,
+                        format!("Expected player, '{}' is a {}", name, d.kind_name()),
+                    );
+                    None
+                }
+                None => {
+                    errors.log(
+                        expr.span,
+                        format!("Expected player, '{}' is not defined", name),
+                    );
+                    None
+                }
+            },
+            _ => {
+                errors.log(expr.span, "Expected player name".to_string());
+                None
+            }
+        })
+        .collect()
+}

cgaal-engine/src/atl/game_formula.rs

@@ -11,11 +11,11 @@ use crate::game_structure::GameStructure;
 /// Given a Phi `formula` (`<<p1>> G p1.alive`) and a IntermediateLCGS `game_Structure`, you can
 /// create a GamePhi with `formula.in_context_of(&game_structure)`. Using this in a print statement
 /// like
-/// ```ignore
+/// ```md
 /// println!("{}", formula.in_context_of(&game_structure))
 /// ```
 /// will print "`<<p1>> G p1.alive`" as opposed to "`<<0>> G 1`", which happens when you just write
-/// ```ignore
+/// ```md
 /// println!("{}", formula)
 /// ```
 pub struct GamePhi<'a, G: GameStructure> {

cgaal-engine/src/atl/mod.rs

@@ -5,11 +5,10 @@ use std::sync::Arc;
 use joinery::prelude::*;
 
 use crate::atl::game_formula::GamePhi;
-pub use crate::atl::parser::*;
 use crate::game_structure::{GameStructure, Player, Proposition};
 
+pub mod convert;
 pub mod game_formula;
-pub mod parser;
 
 /// Alternating-time Temporal Logic formula
 #[derive(Hash, Eq, PartialEq, Clone, Debug, Deserialize, Serialize)]
@@ -317,11 +316,11 @@ impl Phi {
     /// Given a Phi `formula` (`<<p1>> G p1.alive`) and a IntermediateLCGS `game_Structure`, you can
     /// create a GamePhi with `formula.in_context_of(&game_structure)`. Using this in a print statement
     /// like
-    /// ```ignore
+    /// ```md
     /// println!("{}", formula.in_context_of(&game_structure))
     /// ```
     /// will print "`<<p1>> G p1.alive`" as opposed to "`<<0>> G 1`", which happens when you just write
-    /// ```ignore
+    /// ```md
     /// println!("{}", formula)
     /// ```
     pub fn in_context_of<'a, G: GameStructure>(&'a self, game_structure: &'a G) -> GamePhi<'a, G> {