Instance verifier

Author: GBathie

src/bin/experiments.rs

@@ -78,7 +78,7 @@ fn get_name_time_sol<P: BoolAlgoParams + Clone>(
 #[derive(Parser)]
 // #[command(version, about, long_about = None)]
 struct CliArgs {
-    /// Name of the .trace file to read.
+    /// Name of the .json file to read.
     input_filename: PathBuf,
     /// Run LTL enumeration until `max_size_ltl`
     /// before switching to boolean algorithm.

src/bin/verifier.rs

@@ -0,0 +1,29 @@
+use std::path::PathBuf;
+
+use clap::Parser;
+
+use bolt::ltl::trace::traces_from_file;
+use log::info;
+
+fn main() {
+    env_logger::init();
+
+    let args = CliArgs::parse();
+    info!("Reading file '{}'", args.input_filename.display());
+
+    let instance = traces_from_file(&args.input_filename);
+
+    let f = instance
+        .formula
+        .expect("This instance does not contain a smallest_known_formula");
+
+    assert_eq!(f.eval(&instance.traces).accepted_vec(), instance.target);
+    info!("All checks succesful!");
+    println!("All checks were succesful");
+}
+
+#[derive(Parser)]
+struct CliArgs {
+    /// Name of the .json file to read.
+    input_filename: PathBuf,
+}

src/formula/tree.rs

@@ -85,7 +85,7 @@ lazy_static::lazy_static! {
 
         // Precedence is defined lowest to highest
         PrattParser::new()
-            // Addition and subtract have equal precedence
+            // Implies and Equivalent have equal precedence
             .op(Op::infix(implies, Right) | Op::infix(equiv, Right))
             .op(Op::infix(or, Left))
             .op(Op::infix(and, Left))
@@ -96,7 +96,10 @@ lazy_static::lazy_static! {
     };
 }
 
-pub fn parse_expr(expr: &str, atomic_props: &[String]) -> Result<FormulaTree, LtlParsingError> {
+pub fn parse_ltl_formula(
+    expr: &str,
+    atomic_props: &[String],
+) -> Result<FormulaTree, LtlParsingError> {
     let mut pairs = LtlParser::parse(Rule::ltl_expr, expr)?;
     let res = parse_pairs(
         pairs
@@ -125,7 +128,7 @@ fn parse_pairs(
             }
             Rule::expr => parse_pairs(primary.into_inner(), atomic_props),
             rule => unreachable!(
-                "FormulaTree::parse expected atom, found {:?} {}",
+                "FormulaTree::parse expected prop or expr, found {:?} {}",
                 rule,
                 primary.as_str()
             ),

src/ltl/trace.rs

@@ -2,7 +2,10 @@ use std::{collections::HashMap, fs::File, io::Read, path::Path};
 
 use serde::Deserialize;
 
-use crate::ops::{binary::LtlBinaryOp, unary::LtlUnaryOp};
+use crate::{
+    formula::tree::{FormulaTree, parse_ltl_formula},
+    ops::{binary::LtlBinaryOp, unary::LtlUnaryOp},
+};
 
 use super::cs::CharSeq;
 
@@ -12,6 +15,7 @@ pub struct Instance {
     pub atomic_propositions: Vec<String>,
     pub target: Vec<bool>,
     pub operators: Operators,
+    pub formula: Option<FormulaTree>,
 }
 
 /// Stores the [`CharSeq`] of each atomic_proposition on a given trace.
@@ -84,11 +88,18 @@ pub fn parse_traces(buf: &str) -> Instance {
     // Operators filtering is not implemented in current input format.
     let operators = Operators::all();
 
+    let formula = parsed_input
+        .smallest_known_formula
+        .into_iter()
+        .flat_map(|expr| parse_ltl_formula(&expr, &parsed_input.atomic_propositions))
+        .next();
+
     Instance {
         traces,
         atomic_propositions: parsed_input.atomic_propositions,
         target,
         operators,
+        formula,
     }
 }
 
@@ -126,6 +137,7 @@ pub struct ParsedInput {
     positive_traces: Vec<ParsedTrace>,
     negative_traces: Vec<ParsedTrace>,
     atomic_propositions: Vec<String>,
+    smallest_known_formula: Option<String>,
     number_positive_traces: usize,
     number_negative_traces: usize,
     max_length_traces: usize,

src/tests/formula_parser.rs

@@ -1,5 +1,5 @@
 use crate::{
-    formula::tree::parse_expr,
+    formula::tree::parse_ltl_formula,
     tests::{G, Not},
 };
 
@@ -18,7 +18,7 @@ fn test_parsing_fixed() {
         ("G(a0)", G(a0())),
         ("G(!(a0))", G(Not(a0()))),
     ] {
-        let f = parse_expr(expr, &atomic_props).unwrap();
+        let f = parse_ltl_formula(expr, &atomic_props).unwrap();
         assert_eq!(f, expected)
     }
 }
@@ -33,7 +33,7 @@ fn test_parsing_gfand() {
     let p2 = || build_atom("p2", 1);
     let p3 = || build_atom("p3", 2);
     for (expr, expected) in [("G p1 && F p2 && F p3", AND(AND(G(p1()), F(p2())), F(p3())))] {
-        let f = parse_expr(expr, &atomic_props).unwrap();
+        let f = parse_ltl_formula(expr, &atomic_props).unwrap();
         assert_eq!(f, expected)
     }
 }