From 4a661896e78b78dae512ee3ee1a3e4a6b733d893 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ond=C5=99ej=20Huvar?= <492849@mail.muni.cz>
Date: Mon, 18 Dec 2023 21:29:01 +0100
Subject: [PATCH] Add missing method for dirty eval of extended formulae.

---
 src/model_checking.rs | 35 +++++++++++++++++++++++++++++++++--
 1 file changed, 33 insertions(+), 2 deletions(-)

diff --git a/src/model_checking.rs b/src/model_checking.rs
index 86a5da2..1ae6ee7 100644
--- a/src/model_checking.rs
+++ b/src/model_checking.rs
@@ -179,12 +179,13 @@ fn parse_extended_and_validate(
     Ok(parsed_trees)
 }
 
-/// Perform the model checking for list of `extended` HCTL formulae on a given transition `graph`.
+/// Perform the model checking for list of `extended` HCTL formulae on a given transition `graph`,
+/// but do not sanitize the results.
 /// Return the resulting sets of colored vertices (in the same order as input formulae).
 /// The `graph` object MUST support enough symbolic variables to represent all occurring HCTL vars.
 ///
 /// The `substitution context` is a mapping determining how `wild-card propositions` are evaluated.
-pub fn model_check_multiple_extended_formulae(
+pub fn model_check_multiple_extended_formulae_dirty(
     formulae: Vec<String>,
     stg: &SymbolicAsyncGraph,
     substitution_context: HashMap<String, GraphColoredVertices>,
@@ -211,6 +212,21 @@ pub fn model_check_multiple_extended_formulae(
             &self_loop_states,
         ));
     }
+    Ok(results)
+}
+
+/// Perform the model checking for list of `extended` HCTL formulae on a given transition `graph`.
+/// Return the resulting sets of colored vertices (in the same order as input formulae).
+/// The `graph` object MUST support enough symbolic variables to represent all occurring HCTL vars.
+///
+/// The `substitution context` is a mapping determining how `wild-card propositions` are evaluated.
+pub fn model_check_multiple_extended_formulae(
+    formulae: Vec<String>,
+    stg: &SymbolicAsyncGraph,
+    substitution_context: HashMap<String, GraphColoredVertices>,
+) -> Result<Vec<GraphColoredVertices>, String> {
+    let results =
+        model_check_multiple_extended_formulae_dirty(formulae, stg, substitution_context)?;
 
     // sanitize the results' bdds - get rid of additional bdd vars used for HCTL vars
     let sanitized_results: Vec<GraphColoredVertices> = results
@@ -233,6 +249,21 @@ pub fn model_check_extended_formula(
     Ok(result[0].clone())
 }
 
+/// Perform the model checking for a given `extended` HCTL formula on a given transition `graph`,
+/// but do not sanitize the results.
+/// The `graph` object MUST support enough symbolic variables to represent all occurring HCTL vars.
+///
+/// The `substitution context` is a mapping determining how `wild-card propositions` are evaluated.
+pub fn model_check_extended_formula_dirty(
+    formula: String,
+    stg: &SymbolicAsyncGraph,
+    substitution_context: HashMap<String, GraphColoredVertices>,
+) -> Result<GraphColoredVertices, String> {
+    let result =
+        model_check_multiple_extended_formulae_dirty(vec![formula], stg, substitution_context)?;
+    Ok(result[0].clone())
+}
+
 /// Model check HCTL `formula` on a given transition `graph`.
 /// This version does not compute with self-loops. They are thus ignored in EX computation, which
 /// might fine for some formulae, but can be incorrect for others. It is an UNSAFE optimisation,