From 89f0338d79775afba24df636c7f39a8a3f9bc281 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ond=C5=99ej=20Huvar?= <492849@mail.muni.cz>
Date: Mon, 13 Nov 2023 20:37:05 +0100
Subject: [PATCH] Fix case study bug introduced by the newest engine version.

---
 README.md                  |  6 ++++--
 src/bin/case_study_tlgl.rs | 11 ++++++-----
 2 files changed, 10 insertions(+), 7 deletions(-)

diff --git a/README.md b/README.md
index 33d3456..6fda07d 100644
--- a/README.md
+++ b/README.md
@@ -89,10 +89,12 @@ By providing additional `OPTIONS` (CLI arguments), you can receive more detailed
 This enables, for example, to generate witness networks or summarize update functions of the satisfying BNs.
 To see the details regarding program's optional arguments, you can run 
 ```
-.\target\release\sketches-inference --help`
+.\target\release\sketches-inference --help
 ```
 
-
+See the section `Benchmarks and Evaluation` below on how to run more specialized inference cases,
+such as inference from attractor data. Note that everything can be run using the general inference script. 
+However, the specialized methods might provide further optimizations or simpler user interface.
 
 ## Benchmarks and Evaluation
 
diff --git a/src/bin/case_study_tlgl.rs b/src/bin/case_study_tlgl.rs
index 7ae5229..43f10de 100644
--- a/src/bin/case_study_tlgl.rs
+++ b/src/bin/case_study_tlgl.rs
@@ -5,7 +5,7 @@ use boolean_network_sketches::utils::{
 };
 
 use biodivine_hctl_model_checker::mc_utils::get_extended_symbolic_graph;
-use biodivine_hctl_model_checker::model_checking::model_check_formula;
+use biodivine_hctl_model_checker::model_checking::model_check_formula_dirty;
 
 use biodivine_lib_param_bn::biodivine_std::traits::Set;
 use biodivine_lib_param_bn::BooleanNetwork;
@@ -81,7 +81,7 @@ fn case_study_part_1() {
     println!("Analysing candidate set...");
 
     // compute attractors symbolically
-    let attrs_all_candidates = model_check_formula("!{x}: AG EF {x}".to_string(), &graph).unwrap();
+    let attrs_all_candidates = model_check_formula_dirty("!{x}: AG EF {x}".to_string(), &graph).unwrap();
     println!("Attractors for all candidates computed");
     println!(
         "Elapsed time from the start of this computation: {}ms",
@@ -91,7 +91,7 @@ fn case_study_part_1() {
 
     // check for candidates without attractor for programmed cell death
     let programmed_cell_death_formula = "Apoptosis_ & ~S1P & ~sFas & ~Fas & ~Ceramide_ & ~Caspase & ~MCL1 & ~BID_ & ~DISC_ & ~FLIP_ & ~CTLA4_ & ~TCR & ~IFNG_ & ~CREB & ~P2 & ~SMAD_ & ~GPCR_ & ~IAP_";
-    let pcd = model_check_formula(programmed_cell_death_formula.to_string(), &graph).unwrap();
+    let pcd = model_check_formula_dirty(programmed_cell_death_formula.to_string(), &graph).unwrap();
     let colors_not_pcd = graph
         .mk_unit_colors()
         .minus(&attrs_all_candidates.intersect(&pcd).colors());
@@ -107,7 +107,7 @@ fn case_study_part_1() {
 
     // check for candidates with unwanted attractor states
     let unwanted_state_formula = "Apoptosis_ & (S1P | sFas | Fas | Ceramide_ | Caspase  | MCL1 | BID_ | DISC_  | FLIP_ | CTLA4_ | TCR | IFNG_ | CREB  | P2 | SMAD_ | GPCR_ | IAP_)";
-    let unwanted_states = model_check_formula(unwanted_state_formula.to_string(), &graph).unwrap();
+    let unwanted_states = model_check_formula_dirty(unwanted_state_formula.to_string(), &graph).unwrap();
     let colors_with_unwanted_states = attrs_all_candidates.intersect(&unwanted_states).colors();
     println!(
         "{} candidates have unwanted states in attractors, such as:\n",
@@ -141,6 +141,7 @@ fn case_study_part_2(summarize_candidates: bool) {
     // create the partially specified BN object
     let bn = BooleanNetwork::try_from(aeon_string.as_str()).unwrap();
     println!("Loaded BN model with {} components.", bn.num_vars());
+    // create the STG object
     let mut graph = get_extended_symbolic_graph(&bn, 2).unwrap();
     println!(
         "Model has {} symbolic parameters.",
@@ -176,7 +177,7 @@ fn case_study_part_2(summarize_candidates: bool) {
         diseased_attractor.to_string(),
     ];
     let formula = mk_formula_forbid_other_attractors(attr_set);
-    let inferred_colors = model_check_formula(formula, &graph).unwrap().colors();
+    let inferred_colors = model_check_formula_dirty(formula, &graph).unwrap().colors();
     println!(
         "{} consistent candidate networks found in total",
         inferred_colors.approx_cardinality()