From fedb32445b0a06c02e2a9addddea2d66b3255866 Mon Sep 17 00:00:00 2001
From: Samuel Pastva <sam.pastva@gmail.com>
Date: Tue, 19 Dec 2023 17:02:18 +0100
Subject: [PATCH] Do not require BN when sanitizing.

---
 Cargo.toml                       |  2 +-
 src/postprocessing/sanitizing.rs | 17 ++++-------------
 2 files changed, 5 insertions(+), 14 deletions(-)

diff --git a/Cargo.toml b/Cargo.toml
index eedd2ff..38698cc 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -27,7 +27,7 @@ path = "src/bin/convert_aeon_to_bnet.rs"
 
 [dependencies]
 biodivine-lib-bdd = ">=0.5.7, <1.0.0"
-biodivine-lib-param-bn = ">=0.5.0, <1.0.0"
+biodivine-lib-param-bn = ">=0.5.1, <1.0.0"
 clap = { version = "4.1.4", features = ["derive"] }
 rand = "0.8.5"
 termcolor = "1.1.2"
diff --git a/src/postprocessing/sanitizing.rs b/src/postprocessing/sanitizing.rs
index 5b32e1f..7adb3c1 100644
--- a/src/postprocessing/sanitizing.rs
+++ b/src/postprocessing/sanitizing.rs
@@ -1,7 +1,7 @@
 //! Contains operations to sanitize bdds of their additional symbolic variables,
 //! making them compatible with remaining biodivine libraries.
 use biodivine_lib_param_bn::symbolic_async_graph::{
-    GraphColoredVertices, GraphColors, GraphVertices, SymbolicAsyncGraph, SymbolicContext,
+    GraphColoredVertices, GraphColors, GraphVertices, SymbolicAsyncGraph,
 };
 
 /// Sanitize underlying BDD of a given coloured state set by removing the symbolic variables
@@ -11,10 +11,7 @@ pub fn sanitize_colored_vertices(
     stg: &SymbolicAsyncGraph,
     colored_vertices: &GraphColoredVertices,
 ) -> GraphColoredVertices {
-    let canonical_bn = stg.as_network().unwrap_or_else(|| {
-        panic!("Cannot normalize STG with no associated network.");
-    });
-    let canonical_context = SymbolicContext::new(canonical_bn).unwrap();
+    let canonical_context = stg.symbolic_context().as_canonical_context();
     let sanitized_result_bdd = canonical_context
         .transfer_from(colored_vertices.as_bdd(), stg.symbolic_context())
         .unwrap();
@@ -25,10 +22,7 @@ pub fn sanitize_colored_vertices(
 /// that were used for representing HCTL state-variables. At the moment, we remove all symbolic
 /// variables.
 pub fn sanitize_colors(stg: &SymbolicAsyncGraph, colors: &GraphColors) -> GraphColors {
-    let canonical_bn = stg.as_network().unwrap_or_else(|| {
-        panic!("Cannot normalize STG with no associated network.");
-    });
-    let canonical_context = SymbolicContext::new(canonical_bn).unwrap();
+    let canonical_context = stg.symbolic_context().as_canonical_context();
     let sanitized_result_bdd = canonical_context
         .transfer_from(colors.as_bdd(), stg.symbolic_context())
         .unwrap();
@@ -39,10 +33,7 @@ pub fn sanitize_colors(stg: &SymbolicAsyncGraph, colors: &GraphColors) -> GraphC
 /// that were used for representing HCTL state-variables. At the moment, we remove all symbolic
 /// variables.
 pub fn sanitize_vertices(stg: &SymbolicAsyncGraph, vertices: &GraphVertices) -> GraphVertices {
-    let canonical_bn = stg.as_network().unwrap_or_else(|| {
-        panic!("Cannot normalize STG with no associated network.");
-    });
-    let canonical_context = SymbolicContext::new(canonical_bn).unwrap();
+    let canonical_context = stg.symbolic_context().as_canonical_context();
     let sanitized_result_bdd = canonical_context
         .transfer_from(vertices.as_bdd(), stg.symbolic_context())
         .unwrap();