Merge pull request #47 from sybila/dev-analysis-prototype

Prototype for analysis workflow

data/small_example.json

@@ -0,0 +1,186 @@
+{
+  "model": {
+    "variables": [
+      {
+        "id": "v_1",
+        "name": "v_1",
+        "update_fn": "f(v_3)"
+      },
+      {
+        "id": "v_2",
+        "name": "v_2",
+        "update_fn": "g(v_1)"
+      },
+      {
+        "id": "v_3",
+        "name": "v_3",
+        "update_fn": "h(v_1, v_2) | v_3"
+      }
+    ],
+    "regulations": [
+      {
+        "regulator": "v_1",
+        "target": "v_2",
+        "sign": "Unknown",
+        "essential": "Unknown"
+      },
+      {
+        "regulator": "v_1",
+        "target": "v_3",
+        "sign": "Activation",
+        "essential": "True"
+      },
+      {
+        "regulator": "v_2",
+        "target": "v_3",
+        "sign": "Unknown",
+        "essential": "True"
+      },
+      {
+        "regulator": "v_3",
+        "target": "v_1",
+        "sign": "Inhibition",
+        "essential": "True"
+      },
+      {
+        "regulator": "v_3",
+        "target": "v_3",
+        "sign": "Unknown",
+        "essential": "Unknown"
+      }
+    ],
+    "uninterpreted_fns": [
+      {
+        "id": "f",
+        "name": "fn_1",
+        "arguments": [
+          [
+            "Unknown",
+            "Unknown"
+          ]
+        ],
+        "expression": ""
+      },
+      {
+        "id": "g",
+        "name": "fn_1",
+        "arguments": [
+          [
+            "Unknown",
+            "Unknown"
+          ]
+        ],
+        "expression": ""
+      },
+      {
+        "id": "h",
+        "name": "fn_2",
+        "arguments": [
+          [
+            "Unknown",
+            "Unknown"
+          ],
+          [
+            "Unknown",
+            "Unknown"
+          ]
+        ],
+        "expression": ""
+      }
+    ],
+    "layouts": [
+      {
+        "id": "default",
+        "name": "default",
+        "nodes": [
+          {
+            "layout": "default",
+            "variable": "v_2",
+            "px": 503.0,
+            "py": 269.6
+          },
+          {
+            "layout": "default",
+            "variable": "v_3",
+            "px": 532.0,
+            "py": 109.6
+          },
+          {
+            "layout": "default",
+            "variable": "v_1",
+            "px": 344.0,
+            "py": 190.6
+          }
+        ]
+      }
+    ]
+  },
+  "datasets": [],
+  "dyn_properties": [
+    {
+      "id": "data_1",
+      "name": "Generic dynamic property",
+      "variant": "GenericDynProp",
+      "formula": "3{x}:@{x}: ~v_1 & ~v_2 & v_3 & AG EF {x}"
+    },
+    {
+      "id": "prior_knowledge",
+      "name": "Generic dynamic property",
+      "variant": "GenericDynProp",
+      "formula": "3{a}: (3{b}: (3{c}: (@{c}: ((EF {a}) & (EF {b}) & (@{a}: AG EF {a}) & (@{b}: (AG EF {b} & ~EF {a}))))))"
+    },
+    {
+      "id": "data_2",
+      "name": "Generic dynamic property",
+      "variant": "GenericDynProp",
+      "formula": "3{y}:@{y}: v_1 & v_2 & ~v_3 & AG EF {y}"
+    }
+  ],
+  "stat_properties": [
+    {
+      "id": "essentiality_v_3_v_1",
+      "name": "Regulation essentiality property",
+      "variant": "RegulationEssential",
+      "input": "v_3",
+      "target": "v_1",
+      "value": "True",
+      "context": null
+    },
+    {
+      "id": "essentiality_v_2_v_3",
+      "name": "Regulation essentiality property",
+      "variant": "RegulationEssential",
+      "input": "v_2",
+      "target": "v_3",
+      "value": "True",
+      "context": null
+    },
+    {
+      "id": "essentiality_v_1_v_3",
+      "name": "Regulation essentiality property",
+      "variant": "RegulationEssential",
+      "input": "v_1",
+      "target": "v_3",
+      "value": "True",
+      "context": null
+    },
+    {
+      "id": "monotonicity_v_1_v_3",
+      "name": "Regulation monotonicity property",
+      "variant": "RegulationMonotonic",
+      "input": "v_1",
+      "target": "v_3",
+      "value": "Activation",
+      "context": null
+    },
+    {
+      "id": "monotonicity_v_3_v_1",
+      "name": "Regulation monotonicity property",
+      "variant": "RegulationMonotonic",
+      "input": "v_3",
+      "target": "v_1",
+      "value": "Inhibition",
+      "context": null
+    }
+  ]
+}

src-tauri/Cargo.toml

@@ -13,13 +13,16 @@ tauri-build = { version = "1.5", features = [] }
 [dependencies]
 biodivine-lib-bdd = ">=0.5.13, <1.0.0"
 biodivine-lib-param-bn = ">=0.5.10, <1.0.0"
-biodivine-hctl-model-checker = ">=0.2.2, <1.0.0"
+biodivine-hctl-model-checker = ">=0.3.0, <1.0.0"
+chrono = "0.4.38"
 csv = "1.3"
 lazy_static = "1.4.0"
+rand = "0.8.5"
 regex = "1.10.2"
-tauri = { version = "1.6", features = [ "os-all", "dialog-all", "path-all", "shell-open", "window-close", "window-create", "window-set-focus", "window-set-size"] }
 serde = { version = "1.0", features = ["derive"] }
 serde_json = "1.0"
+tauri = { version = "1.6", features = [ "os-all", "dialog-all", "path-all", "shell-open", "window-close", "window-create", "window-set-focus", "window-set-size"] }
+zip = "0.6.3"
 
 [features]
 # this feature is used for production builds or when `devPath` points to the filesystem

src-tauri/src/algorithms/eval_dynamic/mod.rs

@@ -0,0 +1,4 @@
+// TODO
+
+/// Evaluate all template dynamic properties.
+pub mod template_eval;

src-tauri/src/algorithms/eval_dynamic/template_eval.rs

@@ -0,0 +1,22 @@
+use crate::sketchbook::properties::dynamic_props::DynPropertyType;
+use crate::sketchbook::properties::DynProperty;
+use biodivine_hctl_model_checker::model_checking::model_check_formula_dirty;
+use biodivine_lib_param_bn::symbolic_async_graph::{GraphColors, SymbolicAsyncGraph};
+
+pub fn eval_dyn_prop(
+    dyn_prop: DynProperty,
+    graph: &SymbolicAsyncGraph,
+) -> Result<GraphColors, String> {
+    match dyn_prop.get_prop_data() {
+        DynPropertyType::GenericDynProp(dyn_property) => {
+            let formula = dyn_property.processed_formula.to_string();
+            let mc_results = model_check_formula_dirty(&formula, graph)?;
+            Ok(mc_results.colors())
+        }
+        DynPropertyType::AttractorCount(_prop) => todo!(),
+        DynPropertyType::ExistsFixedPoint(_prop) => todo!(),
+        DynPropertyType::ExistsTrajectory(_prop) => todo!(),
+        DynPropertyType::ExistsTrapSpace(_prop) => todo!(),
+        DynPropertyType::HasAttractor(_prop) => todo!(),
+    }
+}

src-tauri/src/algorithms/eval_static/mod.rs

@@ -0,0 +1,4 @@
+// TODO
+
+/// Evaluate all template static properties.
+pub mod template_eval;

src-tauri/src/algorithms/eval_static/template_eval.rs

@@ -0,0 +1,94 @@
+use crate::sketchbook::bn_utils;
+use crate::sketchbook::model::Monotonicity;
+use crate::sketchbook::properties::static_props::StatPropertyType;
+use crate::sketchbook::properties::StatProperty;
+use biodivine_lib_bdd::Bdd;
+use biodivine_lib_param_bn::symbolic_async_graph::{
+    GraphColors, RegulationConstraint, SymbolicAsyncGraph,
+};
+use biodivine_lib_param_bn::BooleanNetwork;
+
+pub fn eval_static_prop(
+    static_prop: StatProperty,
+    network: &BooleanNetwork,
+    graph: &SymbolicAsyncGraph,
+) -> Result<GraphColors, String> {
+    // look into https://github.com/sybila/biodivine-lib-param-bn/blob/master/src/symbolic_async_graph/_impl_regulation_constraint.rs
+
+    let context = graph.symbolic_context();
+    // there might be some constraints already, and we only want to consider colors satisfying these too
+    let initial_unit_colors = graph.mk_unit_colors();
+    let unit_bdd = initial_unit_colors.as_bdd();
+
+    // For each variable, compute Bdd that is true exactly when its update function is true.
+    let update_function_is_true: Vec<Bdd> = network
+        .variables()
+        .map(|variable| {
+            if let Some(function) = network.get_update_function(variable) {
+                context.mk_fn_update_true(function)
+            } else {
+                context.mk_implicit_function_is_true(variable, &network.regulators(variable))
+            }
+        })
+        .collect();
+
+    match static_prop.get_prop_data() {
+        StatPropertyType::GenericStatProp(_prop) => todo!(),
+        StatPropertyType::FnInputEssential(_prop) => todo!(),
+        StatPropertyType::RegulationEssential(prop) => {
+            let input_name = prop.clone().input.unwrap();
+            let target_name = prop.clone().target.unwrap();
+            let input_var = network
+                .as_graph()
+                .find_variable(input_name.as_str())
+                .unwrap();
+            let target_var = network
+                .as_graph()
+                .find_variable(target_name.as_str())
+                .unwrap();
+
+            let fn_is_true = &update_function_is_true[target_var.to_index()];
+
+            let observable = bn_utils::essentiality_to_bool(prop.value);
+            let observability = if observable {
+                RegulationConstraint::mk_observability(context, fn_is_true, input_var)
+            } else {
+                context.mk_constant(true)
+            };
+            let valid_colors = GraphColors::new(observability.and(unit_bdd), context);
+            Ok(valid_colors)
+        }
+        StatPropertyType::RegulationEssentialContext(_prop) => todo!(),
+        StatPropertyType::RegulationMonotonic(prop) => {
+            let input_name = prop.clone().input.unwrap();
+            let target_name = prop.clone().target.unwrap();
+            let input_var = network
+                .as_graph()
+                .find_variable(input_name.as_str())
+                .unwrap();
+            let target_var = network
+                .as_graph()
+                .find_variable(target_name.as_str())
+                .unwrap();
+
+            let fn_is_true = &update_function_is_true[target_var.to_index()];
+
+            let monotonicity = match prop.value {
+                Monotonicity::Activation => {
+                    RegulationConstraint::mk_activation(context, fn_is_true, input_var)
+                }
+                Monotonicity::Inhibition => {
+                    RegulationConstraint::mk_inhibition(context, fn_is_true, input_var)
+                }
+                Monotonicity::Unknown => context.mk_constant(true),
+                Monotonicity::Dual => unimplemented!(),
+            };
+            let valid_colors = GraphColors::new(monotonicity.and(unit_bdd), context);
+            Ok(valid_colors)
+        }
+        StatPropertyType::RegulationMonotonicContext(_prop) => todo!(),
+        StatPropertyType::FnInputEssentialContext(_prop) => todo!(),
+        StatPropertyType::FnInputMonotonic(_prop) => todo!(),
+        StatPropertyType::FnInputMonotonicContext(_prop) => todo!(),
+    }
+}

src-tauri/src/algorithms/fo_logic/mod.rs

@@ -0,0 +1 @@
+// TODO

src-tauri/src/algorithms/mod.rs

@@ -0,0 +1,6 @@
+/// Evaluation of dynamic properties (by either HCTL model checker or special procedures).
+pub mod eval_dynamic;
+/// Evaluation of static properties (by either FO logic evaluator or special procedures).
+pub mod eval_static;
+/// Parsing and evaluation of first-order formulas.
+pub mod fo_logic;

src-tauri/src/analysis/analysis_results.rs

@@ -0,0 +1,34 @@
+use crate::sketchbook::JsonSerde;
+use serde::{Deserialize, Serialize};
+use std::time;
+use time::Duration;
+
+/// Object encompassing analysis results that are to be send to frontend.
+/// It does not contain any intermediate or raw results, these are kept on backend only.
+#[derive(Clone, Debug, PartialEq, Serialize, Deserialize)]
+pub struct AnalysisResults {
+    /// Number of satisfying networks.
+    num_sat_networks: u64,
+    /// Computation time in seconds.
+    comp_time: u64,
+    /// Any kind of string metadata to be displayed/logged on frontend.
+    metadata_log: String,
+}
+
+impl<'de> JsonSerde<'de> for AnalysisResults {}
+
+impl AnalysisResults {
+    /// Create new `AnalysisState` with a full sketch data.
+    pub fn new(num_sat_networks: u64, comp_time: Duration, metadata_log: &str) -> AnalysisResults {
+        AnalysisResults {
+            num_sat_networks,
+            comp_time: comp_time.as_secs(),
+            metadata_log: metadata_log.to_string(),
+        }
+    }
+
+    /// Append string to the end of current metadata.
+    pub fn append_metadata(&mut self, new_metadata: &str) {
+        self.metadata_log.push_str(new_metadata);
+    }
+}