Merge branch 'rewrite'

.github/workflows/build.yml

@@ -14,7 +14,7 @@ env:
   # A fixed version used for testing, so that the builds don't
   # spontaneously break after a few years.
   # Make sure to update this from time to time.
-  RUST_VERSION: "1.65.0"
+  RUST_VERSION: "1.75.0"
 jobs:
   # Check formatting
   fmt:
@@ -56,7 +56,7 @@ jobs:
       - name: Install Rust toolchain.
         run: curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain ${{ env.RUST_VERSION }}
       - name: Run tests.
-        run: cargo test --all-features
+        run: cargo test --all-features --release
 
   # Check code style
   clippy:

.gitignore

@@ -20,5 +20,4 @@ Cargo.lock
 
 .idea
 
-/data/large
 /data/faulty

Cargo.toml

@@ -10,12 +10,12 @@ name = "biodivine_lib_logical_models"
 path = "src/lib.rs"
 
 [dependencies]
-biodivine-lib-bdd = "0.5.3"
+biodivine-lib-bdd = "0.5.7"
 debug-ignore = "1.0.5"
 dyn-clonable = "0.9.0"
 rayon = "1.8.0"
 serde = { version = "1.0", features = ["derive"] }
 serde-xml-rs = "0.6.0"
 thiserror = "1.0.40"
 xml-rs = "0.8.14"
-num-bigint = "0.4.4"
+num-bigint = "0.4.4"

data/data_process.py

@@ -0,0 +1,50 @@
+import os
+import re
+import csv
+
+"""
+A simple script that will take data from results-fwd-test and make a nicer CSV summary
+that reflects how many BDD nodes were used in each iteration of the reachability benchmark.
+"""
+
+if not os.path.exists('./results-fwd-summarised'):
+     os.makedirs('./results-fwd-summarised')
+
+for result_file in os.listdir('./results-fwd-test'):
+	if not result_file.endswith('.txt'):
+		continue	
+	with open(f"./results-fwd-test/{result_file}") as file:		
+		print(f"Loaded result file: {result_file}")
+		step = 0	
+		completed_iterations = 0	
+		accumulated = []
+		max_bdd_size = [0,0,0,0]
+		for line in file:
+			if line.startswith('Completed one wave'):
+				# Restart once new wave is found.
+				step = 0
+				completed_iterations += 1
+				continue
+
+			step_line = re.match(" \\> BDD sizes\\: Some\\((\d+)\\) Some\\((\d+)\\) Some\\((\d+)\\) Some\\((\d+)\\)", line)
+			if step_line is not None:
+				# Found one step line.				
+				if len(accumulated) <= step:
+					# reached_by, size_1, .. size_4
+					accumulated.append([0,0,0,0,0])
+				line_sizes = [int(step_line[i + 1]) for i in range(4)]
+				max_bdd_size = [max(max_bdd_size[i], line_sizes[i]) for i in range(4)]
+				accumulated[step][0] += 1
+				accumulated[step][1] += line_sizes[0]
+				accumulated[step][2] += line_sizes[1]
+				accumulated[step][3] += line_sizes[2]
+				accumulated[step][4] += line_sizes[3]
+				step += 1
+		print(f"  >> Fully completed iterations: {completed_iterations}")
+		print(f"  >> Max. iterations lnegth: {len(accumulated)}")
+		print(f"  >> Max. BDD size: {max_bdd_size}")
+		with open(f"./results-fwd-summarised/{result_file.replace('.txt', '.csv')}", 'w') as outfile:
+			writer = csv.writer(outfile)
+			writer.writerow(['iteration', 'unary', 'binary', 'gray', 'petri'])
+			for row in accumulated:
+				writer.writerow(row)

data/manual/basic_transition.sbml

@@ -29,11 +29,11 @@
                     <!-- 255 is the maximum accepted value; limit of u8 -->
                     <qual:defaultTerm qual:resultLevel="3">
                     </qual:defaultTerm>
-                    <!-- <qual:functionTerm qual:resultLevel="0">
+                    <qual:functionTerm qual:resultLevel="0">
                         <math xmlns="http://www.w3.org/1998/Math/MathML">
                             <apply>
                                 <eq />
-                                <ci> renamed </ci>
+                                <ci> the_only_variable </ci>
                                 <cn type="integer"> 0 </cn>
                             </apply>
                         </math>
@@ -42,7 +42,7 @@
                         <math xmlns="http://www.w3.org/1998/Math/MathML">
                             <apply>
                                 <eq />
-                                <ci> renamed </ci>
+                                <ci> the_only_variable </ci>
                                 <cn type="integer"> 1 </cn>
                             </apply>
                         </math>
@@ -51,11 +51,11 @@
                         <math xmlns="http://www.w3.org/1998/Math/MathML">
                             <apply>
                                 <eq />
-                                <ci> renamed </ci>
+                                <ci> the_only_variable </ci>
                                 <cn type="integer"> 2 </cn>
                             </apply>
                         </math>
-                    </qual:functionTerm> -->
+                    </qual:functionTerm>
                 </qual:listOfFunctionTerms>
             </qual:transition>
         </qual:listOfTransitions>

examples/reachability.rs

@@ -1,15 +1,26 @@
-use biodivine_lib_logical_models::{BinaryIntegerDomain, GrayCodeIntegerDomain, PetriNetIntegerDomain, reachability_benchmark, UnaryIntegerDomain};
+use biodivine_lib_logical_models::benchmarks::reachability::reachability_benchmark;
+// use biodivine_lib_logical_models::prelude::old_symbolic_domain::{
+//     BinaryIntegerDomain, GrayCodeIntegerDomain, PetriNetIntegerDomain, UnaryIntegerDomain,
+// };
+
+use biodivine_lib_logical_models::prelude::symbolic_domain::{
+    BinaryIntegerDomain, GrayCodeIntegerDomain, PetriNetIntegerDomain, UnaryIntegerDomain,
+};
 
 fn main() {
     let args = std::env::args().collect::<Vec<_>>();
     let representation = args[1].clone();
     let sbml_path = args[2].clone();
 
+    let now = std::time::Instant::now();
+
     match representation.as_str() {
         "unary" => reachability_benchmark::<UnaryIntegerDomain>(sbml_path.as_str()),
         "binary" => reachability_benchmark::<BinaryIntegerDomain<u8>>(sbml_path.as_str()),
         "petri_net" => reachability_benchmark::<PetriNetIntegerDomain>(sbml_path.as_str()),
         "gray" | "grey" => reachability_benchmark::<GrayCodeIntegerDomain<u8>>(sbml_path.as_str()),
         _ => panic!("Unknown representation: {}.", representation),
     }
-}
+
+    println!("Time: {}s", now.elapsed().as_secs());
+}

examples/rewritten_reachability.rs

@@ -0,0 +1,27 @@
+use biodivine_lib_logical_models::{
+    benchmarks::rewritten_reachability::reachability_benchmark,
+    prelude::symbolic_domain::{
+        BinaryIntegerDomain, GrayCodeIntegerDomain, PetriNetIntegerDomain, UnaryIntegerDomain,
+    },
+};
+// use biodivine_lib_logical_models::prelude::old_symbolic_domain::{
+//     BinaryIntegerDomain, GrayCodeIntegerDomain, PetriNetIntegerDomain, UnaryIntegerDomain,
+// };
+
+fn main() {
+    let args = std::env::args().collect::<Vec<_>>();
+    let representation = args[1].clone();
+    let sbml_path = args[2].clone();
+
+    let now = std::time::Instant::now();
+
+    match representation.as_str() {
+        "unary" => reachability_benchmark::<UnaryIntegerDomain>(sbml_path.as_str()),
+        "binary" => reachability_benchmark::<BinaryIntegerDomain<u8>>(sbml_path.as_str()),
+        "petri_net" => reachability_benchmark::<PetriNetIntegerDomain>(sbml_path.as_str()),
+        "gray" | "grey" => reachability_benchmark::<GrayCodeIntegerDomain<u8>>(sbml_path.as_str()),
+        _ => panic!("Unknown representation: {}.", representation),
+    }
+
+    println!("Time: {}s", now.elapsed().as_secs());
+}

examples/test_reachability_bwd.rs

@@ -1,6 +1,5 @@
 use biodivine_lib_logical_models::test_utils::ComputationStep;
 
-
 /// This binary is testing the implementation correctness by running reachability on the
 /// input model and validating that the set of reachable states has the same cardinality
 /// in every step.
@@ -20,7 +19,10 @@ fn main() {
             cmp.perform_bwd_step();
             cmp.check_consistency();
         }
-        println!("Completed one wave of reachability. Reinitializing with {} states remaining.", cmp.remaining());
+        println!(
+            "Completed one wave of reachability. Reinitializing with {} states remaining.",
+            cmp.remaining()
+        );
     }
     println!("Test completed successfully. Whole state space explored.");
 }

examples/test_reachability_fwd.rs

@@ -1,6 +1,5 @@
 use biodivine_lib_logical_models::test_utils::ComputationStep;
 
-
 /// This binary is testing the implementation correctness by running reachability on the
 /// input model and validating that the set of reachable states has the same cardinality
 /// in every step.
@@ -20,7 +19,10 @@ fn main() {
             cmp.perform_fwd_step();
             cmp.check_consistency();
         }
-        println!("Completed one wave of reachability. Reinitializing with {} states remaining.", cmp.remaining());
+        println!(
+            "Completed one wave of reachability. Reinitializing with {} states remaining.",
+            cmp.remaining()
+        );
     }
     println!("Test completed successfully. Whole state space explored.");
 }

src/benchmarks/mod.rs

@@ -0,0 +1,2 @@
+pub mod reachability;
+pub mod rewritten_reachability;

src/prototype/reachability.rs → src/benchmarks/reachability.rs

@@ -1,27 +1,40 @@
-use std::fmt::Debug;
 use biodivine_lib_bdd::Bdd;
-use crate::{count_states, log_percent, pick_state_bdd, SmartSystemUpdateFn, SymbolicDomain};
+use std::fmt::Debug;
+
+// use crate::{
+//     prototype::symbolic_domain::SymbolicDomain,
+//     prototype::{count_states, find_start_of, log_percent, pick_state_bdd, SmartSystemUpdateFn},
+// };
+
+use crate::symbolic_domains::symbolic_domain::SymbolicDomainOrd;
+use crate::update::update_fn::SmartSystemUpdateFn;
+use crate::utils::{count_states, log_percent, pick_state_bdd};
+use crate::xml_parsing::utils::find_start_of;
 
-pub fn reachability_benchmark<D: SymbolicDomain<u8> + Debug>(sbml_path: &str) {
+pub fn reachability_benchmark<D: SymbolicDomainOrd<u8> + Debug>(sbml_path: &str) {
     let smart_system_update_fn = {
-        let file = std::fs::File::open(sbml_path.clone())
-            .expect("Cannot open SBML file.");
+        let file = std::fs::File::open(sbml_path).expect("Cannot open SBML file.");
         let reader = std::io::BufReader::new(file);
         let mut xml = xml::reader::EventReader::new(reader);
 
-        crate::find_start_of(&mut xml, "listOfTransitions")
+        find_start_of(&mut xml, "listOfTransitions")
             .expect("Cannot find transitions in the SBML file.");
 
-        let smart_system_update_fn = SmartSystemUpdateFn::<D, u8>::try_from_xml(&mut xml)
-                .expect("Loading system fn update failed.");
-
-        smart_system_update_fn
+        SmartSystemUpdateFn::<D, u8>::try_from_xml(&mut xml)
+            .expect("Loading system fn update failed.")
     };
 
     let unit = smart_system_update_fn.unit_vertex_set();
     let system_var_count = smart_system_update_fn.get_system_variables().len();
-    println!("Variables: {}, expected states {}", system_var_count, 1 << system_var_count);
-    println!("Computed state count: {}", count_states(&smart_system_update_fn, &unit));
+    println!(
+        "Variables: {}, expected states {}",
+        system_var_count,
+        1 << system_var_count
+    );
+    println!(
+        "Computed state count: {}",
+        count_states(&smart_system_update_fn, &unit)
+    );
     let mut universe = unit.clone();
     while !universe.is_false() {
         let mut weak_scc = pick_state_bdd(&smart_system_update_fn, &universe);
@@ -31,13 +44,21 @@ pub fn reachability_benchmark<D: SymbolicDomain<u8> + Debug>(sbml_path: &str) {
 
             // FWD/BWD reachable set is not a subset of weak SCC, meaning the SCC can be expanded.
             if !fwd_bwd_reachable.imp(&weak_scc).is_true() {
-                println!(" + SCC increased to (states={}, size={})", count_states(&smart_system_update_fn, &weak_scc), weak_scc.size());
+                println!(
+                    " + SCC increased to (states={}, size={})",
+                    count_states(&smart_system_update_fn, &weak_scc),
+                    weak_scc.size()
+                );
                 weak_scc = fwd_bwd_reachable;
             } else {
                 break;
             }
         }
-        println!(" + Found weak SCC (states={}, size={})", count_states(&smart_system_update_fn, &weak_scc), weak_scc.size());
+        println!(
+            " + Found weak SCC (states={}, size={})",
+            count_states(&smart_system_update_fn, &weak_scc),
+            weak_scc.size()
+        );
         // Remove the SCC from the universe set and start over.
         universe = universe.and_not(&weak_scc);
         println!(
@@ -52,22 +73,30 @@ pub fn reachability_benchmark<D: SymbolicDomain<u8> + Debug>(sbml_path: &str) {
 ///
 /// The result BDD contains a vertex `x` if and only if there is a (possibly zero-length) path
 /// from some vertex `x' \in initial` into `x`, i.e. `x' -> x`.
-pub fn reach_fwd<D: SymbolicDomain<u8> + Debug>(system: &SmartSystemUpdateFn<D, u8>, initial: &Bdd, universe: &Bdd) -> Bdd {
+pub fn reach_fwd<D: SymbolicDomainOrd<u8> + Debug>(
+    system: &SmartSystemUpdateFn<D, u8>,
+    initial: &Bdd,
+    universe: &Bdd,
+) -> Bdd {
     // The list of system variables, sorted in descending order (i.e. opposite order compared
     // to the ordering inside BDDs).
     let sorted_variables = system.get_system_variables();
     let mut result = initial.clone();
-    println!("Start forward reachability: (states={}, size={})", count_states(system, &result), result.size());
+    println!(
+        "Start forward reachability: (states={}, size={})",
+        count_states(system, &result),
+        result.size()
+    );
     'fwd: loop {
         for var in sorted_variables.iter().rev() {
-            let successors = system.transition_under_variable(var.as_str(), &result);
+            let successors = system.successors_async(var.as_str(), &result);
 
             // Should be equivalent to "successors \not\subseteq result".
             if !successors.imp(&result).is_true() {
                 result = result.or(&successors);
                 println!(
                     " >> (progress={:.2}%%, states={}, size={})",
-                    log_percent(&result, &universe),
+                    log_percent(&result, universe),
                     count_states(system, &result),
                     result.size()
                 );
@@ -76,7 +105,11 @@ pub fn reach_fwd<D: SymbolicDomain<u8> + Debug>(system: &SmartSystemUpdateFn<D,
         }
 
         // No further successors were computed across all variables. We are done.
-        println!(" >> Done. (states={}, size={})", count_states(system, &result), result.size());
+        println!(
+            " >> Done. (states={}, size={})",
+            count_states(system, &result),
+            result.size()
+        );
         return result;
     }
 }
@@ -85,20 +118,28 @@ pub fn reach_fwd<D: SymbolicDomain<u8> + Debug>(system: &SmartSystemUpdateFn<D,
 ///
 /// The result BDD contains a vertex `x` if and only if there is a (possibly zero-length) path
 /// from `x` into some vertex `x' \in initial`, i.e. `x -> x'`.
-pub fn reach_bwd<D: SymbolicDomain<u8> + Debug>(system: &SmartSystemUpdateFn<D, u8>, initial: &Bdd, universe: &Bdd) -> Bdd {
+pub fn reach_bwd<D: SymbolicDomainOrd<u8> + Debug>(
+    system: &SmartSystemUpdateFn<D, u8>,
+    initial: &Bdd,
+    universe: &Bdd,
+) -> Bdd {
     let sorted_variables = system.get_system_variables();
     let mut result = initial.clone();
-    println!("Start backward reachability: (states={}, size={})", count_states(system, &result), result.size());
+    println!(
+        "Start backward reachability: (states={}, size={})",
+        count_states(system, &result),
+        result.size()
+    );
     'bwd: loop {
         for var in sorted_variables.iter().rev() {
-            let predecessors = system.predecessors_under_variable(var.as_str(), &result);
+            let predecessors = system.predecessors_async(var.as_str(), result.to_owned());
 
             // Should be equivalent to "predecessors \not\subseteq result".
             if !predecessors.imp(&result).is_true() {
                 result = result.or(&predecessors);
                 println!(
                     " >> (progress={:.2}%%, states={}, size={})",
-                    log_percent(&result, &universe),
+                    log_percent(&result, universe),
                     count_states(system, &result),
                     result.size()
                 );
@@ -107,7 +148,11 @@ pub fn reach_bwd<D: SymbolicDomain<u8> + Debug>(system: &SmartSystemUpdateFn<D,
         }
 
         // No further predecessors were computed across all variables. We are done.
-        println!(" >> Done. (states={}, size={})", count_states(system, &result), result.size());
+        println!(
+            " >> Done. (states={}, size={})",
+            count_states(system, &result),
+            result.size()
+        );
         return result;
     }
 }