Merge branch 'decision-trees' into 0.4.0

.github/workflows/build.yml

@@ -0,0 +1,119 @@
+name: build
+on: [push]
+
+## At the moment, everything is running on nightly. Once Rocket 0.5 is out, stable/beta can be enabled.
+
+jobs:
+  # Check formatting
+  fmt:
+    name: Rustfmt
+    runs-on: ubuntu-latest
+    env:
+      RUSTFLAGS: "-D warnings"
+    steps:
+      - uses: actions/checkout@v2
+      - uses: actions-rs/toolchain@v1
+        with:
+          profile: minimal
+          toolchain: nightly
+          override: true
+      - run: rustup component add rustfmt
+      - uses: actions-rs/cargo@v1
+        with:
+          command: fmt
+          args: --all -- --check
+
+
+  # Run basic code validity check.
+  check:
+    needs: fmt
+    name: Check
+    runs-on: ubuntu-latest
+    env:
+      RUSTFLAGS: "-D warnings"
+    steps:
+      - uses: actions/checkout@v2
+      - uses: actions-rs/toolchain@v1
+        with:
+          profile: minimal
+          toolchain: nightly
+          override: true
+      - uses: actions-rs/cargo@v1
+        with:
+          command: check
+
+  # Run all tests
+  #test:
+  #  needs: check
+  #  name: Test Suite
+  #  runs-on: ubuntu-latest
+  #  env:
+  #    RUSTFLAGS: "-D warnings"
+  #  steps:
+  #    - uses: actions/checkout@v2
+  #    - uses: actions-rs/toolchain@v1
+  #      with:
+  #        profile: minimal
+  #        toolchain: stable
+  #        override: true
+  #    - uses: actions-rs/cargo@v1
+  #      with:
+  #        command: test
+  #        args: --features "shields_up"
+
+  # Run all tests, but with beta
+  #test-beta:
+  #  needs: check
+  #  name: Test Suite (Beta)
+  #  runs-on: ubuntu-latest
+  #  env:
+  #    RUSTFLAGS: "-D warnings"
+  #  steps:
+  #    - uses: actions/checkout@v2
+  #    - uses: actions-rs/toolchain@v1
+  #      with:
+  #        profile: minimal
+  #        toolchain: beta
+  #        override: true
+  #    - uses: actions-rs/cargo@v1
+  #      with:
+  #        command: test
+  #        args: --features "shields_up"
+
+  # Run all tests, but with nightly
+  test-nightly:
+    needs: check
+    name: Test Suite (Nightly)
+    runs-on: ubuntu-latest
+    env:
+      RUSTFLAGS: "-D warnings"
+    steps:
+      - uses: actions/checkout@v2
+      - uses: actions-rs/toolchain@v1
+        with:
+          profile: minimal
+          toolchain: nightly
+          override: true
+      - uses: actions-rs/cargo@v1
+        with:
+          command: test
+          args: --features "shields_up"
+
+  # Check code style
+  clippy:
+    needs: check
+    name: Clippy
+    runs-on: ubuntu-latest
+    env:
+      RUSTFLAGS: "-D warnings"
+    steps:
+      - uses: actions/checkout@v2
+      - uses: actions-rs/toolchain@v1
+        with:
+          profile: minimal
+          toolchain: nightly
+          override: true
+      - run: rustup component add clippy
+      - uses: actions-rs/cargo@v1
+        with:
+          command: clippy

Cargo.toml

@@ -16,15 +16,15 @@ debug = true
 #lto = true
 
 [dependencies]
-biodivine-lib-std = { git = "https://github.com/sybila/biodivine-lib-std.git" }
-biodivine-lib-param-bn = { git = "https://github.com/sybila/biodivine-lib-param-bn.git", tag = "v0.1.0-beta.2" }
-biodivine-lib-bdd = "0.2.0"
+biodivine-lib-bdd = "0.2.1"
+biodivine-lib-param-bn = "0.1.0"
 rocket = "0.4.6"
 rayon = "1.5.0"
 crossbeam = "0.8.0"
 lazy_static = "1.4.0"
 json = "0.12.4"
 regex = "1.4.2"
+rand = "0.8.1"
 
 [features]
 # With shields_up you enable explicit assertions of pre/post conditions and invariants in critical

bench.py

@@ -4,6 +4,7 @@
 
 re_bench = re.compile("\[v(\d+)\]__\[r(\d+)\]__\[(.+?)\]__\[(.+?)\]")
 re_var_count = re.compile("\[v(\d+)\]")
+re_elapsed = re.compile("Elapsed time: (\d+\.?\d*)s")
 
 def is_bench(benchmark):
 	return re_bench.match(benchmark) != None
@@ -16,11 +17,15 @@ def bench_cmp(benchmark):
 benchmarks = sorted(benchmarks, key=bench_cmp)
 
 
-out_dir = "bench" + str(int(time.time()))
+out_dir = "bench_run_" + str(int(time.time()))
 os.mkdir(out_dir)
 
+csv = open(out_dir + "/stats.csv", "w")
+csv.write("Benchmark, Time[s]\n")
+
+elapsed_times = {}
 i = 1
-for benchmark in benchmarks:	
+for benchmark in benchmarks:
 	bench_name = re_bench.match(benchmark).group(3)
 	print("Starting "+bench_name)
 	in_file = "./benchmark/" + benchmark + "/model.aeon"
@@ -30,5 +35,21 @@ def bench_cmp(benchmark):
 	with open(out_file, 'r') as f:
 		lines = f.read().splitlines()
 		time_line = lines[-1]
-		class_line = lines[-3]
-		print(class_line + " " + time_line)
+		if re_elapsed.match(time_line):
+			class_line = lines[-3]
+			print("Success: " + class_line + " " + time_line)
+			time = re_elapsed.match(time_line).group(1)
+			elapsed_times[bench_name] = time
+			csv.write(bench_name + ", " + str(time) + "\n")
+		else:
+			print("Failed!")
+			elapsed_times[bench_name] = "Fail"
+			csv.write(bench_name + ", " + "Fail" + "\n")
+		csv.flush()
+
+print "FINISHED"
+print "Benchmark, Time[s]"
+for bench, time in  elapsed_times.items():
+	print bench + ", " + str(time)
+
+csv.close()

src/_impl_graph_task_context.rs

@@ -0,0 +1,49 @@
+use crate::scc::ProgressTracker;
+use crate::GraphTaskContext;
+use biodivine_lib_param_bn::symbolic_async_graph::{GraphColoredVertices, SymbolicAsyncGraph};
+use std::sync::atomic::{AtomicBool, Ordering};
+
+impl Default for GraphTaskContext {
+    fn default() -> Self {
+        GraphTaskContext::new()
+    }
+}
+
+impl GraphTaskContext {
+    /// Create a new task context.
+    pub fn new() -> GraphTaskContext {
+        GraphTaskContext {
+            is_cancelled: AtomicBool::new(false),
+            progress: ProgressTracker::new(),
+        }
+    }
+
+    /// Re-initialize the task context with a fresh graph.
+    pub fn restart(&self, graph: &SymbolicAsyncGraph) {
+        self.progress.init_from_graph(graph);
+        self.is_cancelled.store(false, Ordering::SeqCst);
+    }
+
+    /// True if the task is cancelled.
+    pub fn is_cancelled(&self) -> bool {
+        self.is_cancelled.load(Ordering::SeqCst)
+    }
+
+    /// Set the status of this task to cancelled.
+    ///
+    /// Return true if the computation was set to cancelled by this call, false if it was
+    /// cancelled previously.
+    pub fn cancel(&self) -> bool {
+        !self.is_cancelled.swap(true, Ordering::SeqCst)
+    }
+
+    /// Indicate that the given set still needs to be processed by the task.
+    pub fn update_remaining(&self, remaining: &GraphColoredVertices) {
+        self.progress.update_remaining(remaining);
+    }
+
+    /// Output a string which represent the percentage of remaining state space.
+    pub fn get_percent_string(&self) -> String {
+        self.progress.get_percent_string()
+    }
+}

src/all/mod.rs

@@ -29,7 +29,7 @@ pub enum AttractorAtom {
 }
 
 #[derive(Clone, Debug, Eq, PartialEq)]
-pub enum ALLAtom {
+pub enum AllAtom {
     AllAttractors(AttractorFormula),
     SomeAttractor(AttractorFormula),
 }
@@ -38,7 +38,7 @@ pub type StateFormula = BooleanFormula<StateAtom>;
 
 pub type AttractorFormula = BooleanFormula<AttractorAtom>;
 
-pub type ALLFormula = BooleanFormula<ALLAtom>;
+pub type AllFormula = BooleanFormula<AllAtom>;
 /*
 impl ALLFormula {
     pub fn eval(

src/bdt/_attributes_for_network.rs

@@ -1,12 +1,12 @@
-use crate::bdt::{Attribute, BifurcationFunction, BDT};
+use crate::bdt::{Attribute, Bdt, BifurcationFunction};
 use crate::util::functional::Functional;
 use biodivine_lib_bdd::Bdd;
+use biodivine_lib_param_bn::biodivine_std::traits::Set;
 use biodivine_lib_param_bn::symbolic_async_graph::SymbolicAsyncGraph;
 use biodivine_lib_param_bn::{FnUpdate, VariableId};
-use biodivine_lib_std::param_graph::Params;
 
-impl BDT {
-    pub fn new_from_graph(classes: BifurcationFunction, graph: &SymbolicAsyncGraph) -> BDT {
+impl Bdt {
+    pub fn new_from_graph(classes: BifurcationFunction, graph: &SymbolicAsyncGraph) -> Bdt {
         let mut attributes = Vec::new();
         attributes_for_network_inputs(graph, &mut attributes);
         attributes_for_constant_parameters(graph, &mut attributes);
@@ -25,22 +25,22 @@ impl BDT {
                 is_not_empty
             })
             .collect();
-        BDT::new(classes, attributes)
+        Bdt::new(classes, attributes)
     }
 }
 
 /// **(internal)** Construct basic attributes for all input variables.
 fn attributes_for_network_inputs(graph: &SymbolicAsyncGraph, out: &mut Vec<Attribute>) {
-    for v in graph.network().variables() {
+    for v in graph.as_network().variables() {
         // v is input if it has no update function and no regulators
-        let is_input = graph.network().regulators(v).is_empty();
-        let is_input = is_input && graph.network().get_update_function(v).is_none();
+        let is_input = graph.as_network().regulators(v).is_empty();
+        let is_input = is_input && graph.as_network().get_update_function(v).is_none();
         if is_input {
             let bdd = graph
                 .symbolic_context()
-                .mk_implicit_function_is_true(v, &vec![]);
+                .mk_implicit_function_is_true(v, &[]);
             out.push(Attribute {
-                name: graph.network().get_variable_name(v).clone(),
+                name: graph.as_network().get_variable_name(v).clone(),
                 negative: graph.empty_colors().copy(bdd.not()),
                 positive: graph.empty_colors().copy(bdd),
             })
@@ -50,14 +50,14 @@ fn attributes_for_network_inputs(graph: &SymbolicAsyncGraph, out: &mut Vec<Attri
 
 /// **(internal)** Construct basic attributes for all constant parameters of the network.
 fn attributes_for_constant_parameters(graph: &SymbolicAsyncGraph, out: &mut Vec<Attribute>) {
-    for p in graph.network().parameters() {
-        if graph.network()[p].get_arity() == 0 {
+    for p in graph.as_network().parameters() {
+        if graph.as_network()[p].get_arity() == 0 {
             // Parameter is a constant
             let bdd = graph
                 .symbolic_context()
-                .mk_uninterpreted_function_is_true(p, &vec![]);
+                .mk_uninterpreted_function_is_true(p, &[]);
             out.push(Attribute {
-                name: graph.network()[p].get_name().clone(),
+                name: graph.as_network()[p].get_name().clone(),
                 negative: graph.empty_colors().copy(bdd.not()),
                 positive: graph.empty_colors().copy(bdd),
             })
@@ -68,9 +68,9 @@ fn attributes_for_constant_parameters(graph: &SymbolicAsyncGraph, out: &mut Vec<
 /// **(internal)** If some regulation has a missing static constraint, try to build it
 /// and add it as an attribute.
 fn attributes_for_missing_constraints(graph: &SymbolicAsyncGraph, out: &mut Vec<Attribute>) {
-    let network = graph.network();
+    let network = graph.as_network();
     let context = graph.symbolic_context();
-    for reg in graph.network().as_graph().regulations() {
+    for reg in graph.as_network().as_graph().regulations() {
         // This is straight up copied from static constraint analysis in lib-param-bn.
         // For more context, go there.
         let target = reg.get_target();
@@ -143,26 +143,26 @@ fn attributes_for_missing_constraints(graph: &SymbolicAsyncGraph, out: &mut Vec<
 /// **(internal)** Make an explicit attributes (like `f[1,0,1] = 1`) for every implicit update
 /// function row in the network.
 fn attributes_for_implicit_function_tables(graph: &SymbolicAsyncGraph, out: &mut Vec<Attribute>) {
-    for v in graph.network().variables() {
-        let is_implicit_function = graph.network().get_update_function(v).is_none();
+    for v in graph.as_network().variables() {
+        let is_implicit_function = graph.as_network().get_update_function(v).is_none();
         let is_implicit_function =
-            is_implicit_function && !graph.network().regulators(v).is_empty();
+            is_implicit_function && !graph.as_network().regulators(v).is_empty();
         if is_implicit_function {
             let table = graph.symbolic_context().get_implicit_function_table(v);
             for (ctx, var) in table {
                 let bdd = graph.symbolic_context().bdd_variable_set().mk_var(var);
                 let ctx: Vec<String> = ctx
                     .into_iter()
-                    .zip(graph.network().regulators(v))
+                    .zip(graph.as_network().regulators(v))
                     .map(|(b, r)| {
                         format!(
                             "{}{}",
                             if b { "" } else { "¬" },
-                            graph.network().get_variable_name(r)
+                            graph.as_network().get_variable_name(r)
                         )
                     })
                     .collect();
-                let name = format!("{}{:?}", graph.network().get_variable_name(v), ctx);
+                let name = format!("{}{:?}", graph.as_network().get_variable_name(v), ctx);
                 out.push(Attribute {
                     name: name.replace("\"", ""),
                     negative: graph.mk_empty_colors().copy(bdd.not()),
@@ -175,8 +175,8 @@ fn attributes_for_implicit_function_tables(graph: &SymbolicAsyncGraph, out: &mut
 
 /// **(internal)** Make an explicit argument for every explicit parameter function row in the network.
 fn attributes_for_explicit_function_tables(graph: &SymbolicAsyncGraph, out: &mut Vec<Attribute>) {
-    for p in graph.network().parameters() {
-        let parameter = graph.network().get_parameter(p);
+    for p in graph.as_network().parameters() {
+        let parameter = graph.as_network().get_parameter(p);
         if parameter.get_arity() > 0 {
             let table = graph.symbolic_context().get_explicit_function_table(p);
             let arg_names = (0..parameter.get_arity())
@@ -203,9 +203,9 @@ fn attributes_for_explicit_function_tables(graph: &SymbolicAsyncGraph, out: &mut
 /// Create "conditional observability" attributes for both implicit and explicit update functions.
 fn attributes_for_conditional_observability(graph: &SymbolicAsyncGraph, out: &mut Vec<Attribute>) {
     let context = graph.symbolic_context();
-    let network = graph.network();
-    for v in graph.network().variables() {
-        let regulators = graph.network().regulators(v);
+    let network = graph.as_network();
+    for v in graph.as_network().variables() {
+        let regulators = graph.as_network().regulators(v);
 
         // Bdd that is true when update function for this variable is true
         let fn_is_true = if let Some(function) = network.get_update_function(v) {