Extended AEON format for sketch import/export (#57)

* Add export to customized AEON format (work-in-progress).

* Update the AEON import and export to cover full sketch.

* Update biodivine dependencies.

data/test_data/test_model_with_data.aeon

@@ -0,0 +1,35 @@
+C -?? A
+C -| C
+D -> B
+D -? D
+B -> C
+A -> C
+A -> B
+$A: h(C)
+$B: f(A, D)
+$C: A & g(C, B)
+#position:A:346.89832,183.03789
+#position:C:504.7078,101.93903
+#position:B:0,0
+#position:D:642.49677,185.15988
+#!dataset:data_fp:#`{"name":"data_fp","id":"data_fp","annotation":"","observations":[{"id":"ones","name":"ones","annotation":"","dataset":"data_fp","values":"1111"},{"id":"zeros","name":"zeros","annotation":"","dataset":"data_fp","values":"0000"}],"variables":["A","B","C","D"]}`#
+#!dataset:data_mts:#`{"name":"data_mts","id":"data_mts","annotation":"","observations":[{"id":"abc","name":"abc","annotation":"","dataset":"data_mts","values":"111*"},{"id":"ab","name":"ab","annotation":"","dataset":"data_mts","values":"11**"}],"variables":["A","B","C","D"]}`#
+#!dataset:data_time_series:#`{"name":"data_time_series","id":"data_time_series","annotation":"","observations":[{"id":"a","name":"a","annotation":"","dataset":"data_time_series","values":"1000"},{"id":"b","name":"b","annotation":"","dataset":"data_time_series","values":"1100"},{"id":"c","name":"c","annotation":"","dataset":"data_time_series","values":"1110"},{"id":"d","name":"d","annotation":"","dataset":"data_time_series","values":"1111"}],"variables":["A","B","C","D"]}`#
+#!function:f:#`{"id":"f","name":"f","annotation":"","arguments":[["Unknown","Unknown"],["Unknown","Unknown"]],"expression":""}`#
+#!function:g:#`{"id":"g","name":"g","annotation":"","arguments":[["Unknown","Unknown"],["Unknown","Unknown"]],"expression":""}`#
+#!function:h:#`{"id":"h","name":"h","annotation":"","arguments":[["Unknown","Unknown"]],"expression":""}`#
+#!static_property:essentiality_A_B:#`{"id":"essentiality_A_B","name":"Regulation essentiality property","annotation":"","variant":"RegulationEssential","input":"A","target":"B","value":"True","context":null}`#
+#!static_property:essentiality_A_C:#`{"id":"essentiality_A_C","name":"Regulation essentiality property","annotation":"","variant":"RegulationEssential","input":"A","target":"C","value":"True","context":null}`#
+#!static_property:essentiality_B_C:#`{"id":"essentiality_B_C","name":"Regulation essentiality property","annotation":"","variant":"RegulationEssential","input":"B","target":"C","value":"True","context":null}`#
+#!static_property:essentiality_C_C:#`{"id":"essentiality_C_C","name":"Regulation essentiality property","annotation":"","variant":"RegulationEssential","input":"C","target":"C","value":"True","context":null}`#
+#!static_property:essentiality_D_B:#`{"id":"essentiality_D_B","name":"Regulation essentiality property","annotation":"","variant":"RegulationEssential","input":"D","target":"B","value":"True","context":null}`#
+#!static_property:essentiality_D_D:#`{"id":"essentiality_D_D","name":"Regulation essentiality property","annotation":"","variant":"RegulationEssential","input":"D","target":"D","value":"True","context":null}`#
+#!static_property:monotonicity_A_B:#`{"id":"monotonicity_A_B","name":"Regulation monotonicity property","annotation":"","variant":"RegulationMonotonic","input":"A","target":"B","value":"Activation","context":null}`#
+#!static_property:monotonicity_A_C:#`{"id":"monotonicity_A_C","name":"Regulation monotonicity property","annotation":"","variant":"RegulationMonotonic","input":"A","target":"C","value":"Activation","context":null}`#
+#!static_property:monotonicity_B_C:#`{"id":"monotonicity_B_C","name":"Regulation monotonicity property","annotation":"","variant":"RegulationMonotonic","input":"B","target":"C","value":"Activation","context":null}`#
+#!static_property:monotonicity_C_C:#`{"id":"monotonicity_C_C","name":"Regulation monotonicity property","annotation":"","variant":"RegulationMonotonic","input":"C","target":"C","value":"Inhibition","context":null}`#
+#!static_property:monotonicity_D_B:#`{"id":"monotonicity_D_B","name":"Regulation monotonicity property","annotation":"","variant":"RegulationMonotonic","input":"D","target":"B","value":"Activation","context":null}`#
+#!variable:A:#`{"id":"A","name":"A","annotation":"","update_fn":"h(C)"}`#
+#!variable:B:#`{"id":"B","name":"B","annotation":"","update_fn":"f(A, D)"}`#
+#!variable:C:#`{"id":"C","name":"C","annotation":"","update_fn":"A & g(C, B)"}`#
+#!variable:D:#`{"id":"D","name":"D","annotation":"","update_fn":""}`#

src-tauri/Cargo.toml

@@ -12,9 +12,9 @@ readme = "README.md"
 tauri-build = { version = "1.5", features = [] }
 
 [dependencies]
-biodivine-lib-bdd = ">=0.5.19, <1.0.0"
-biodivine-lib-param-bn = ">=0.5.11, <1.0.0"
-biodivine-hctl-model-checker = ">=0.3.0, <1.0.0"
+biodivine-lib-bdd = ">=0.5.22, <1.0.0"
+biodivine-lib-param-bn = ">=0.5.13, <1.0.0"
+biodivine-hctl-model-checker = ">=0.3.1, <1.0.0"
 chrono = "0.4.38"
 csv = "1.3"
 lazy_static = "1.5.0"

src-tauri/src/analysis/results_export.rs

@@ -9,12 +9,14 @@ use std::path::Path;
 use zip::write::{FileOptions, ZipWriter};
 
 /// Export archive with complete results to the given path.
+/// The output archive is tailored for a case where sketch is satisfiable.
+///
 /// The results archive include:
 /// - a summary report (basically information tracked by the `InferenceResults` struct)
 /// - original sketch in JSON format for replicability in SketchBook
 /// - BDD with satisfying colors
 /// - a PSBN model derived from the sketch (in aeon format) that can be used as a context for the BDD
-/// - a folder with update function variants per variable
+/// - a folder with admissible update function variants per variable
 pub fn export_results(
     path: &str,
     finished_solver: &FinishedInferenceSolver,
@@ -81,6 +83,8 @@ fn write_to_zip(
     Ok(())
 }
 
+/// Prepare a formated summary of inference results, basically a "report" on the
+/// computation progress and results.
 fn format_inference_results(results: &InferenceResults) -> String {
     let mut output = String::new();
 
@@ -129,7 +133,8 @@ fn format_inference_results(results: &InferenceResults) -> String {
 }
 
 /// For a given variable, get all valid interpretations of its update function present in the
-/// satisfying `colors` (taken from the results of the solver). Variable must be present in the network.
+/// satisfying `colors` (taken from the results of the solver).
+/// Variable must be present in the network.
 pub fn get_update_fn_variants_from_solver(
     solver: &FinishedInferenceSolver,
     var_name: &str,

src-tauri/src/sketchbook/_sketch/_impl_export.rs

@@ -1,4 +1,8 @@
-use crate::sketchbook::data_structs::SketchData;
+use biodivine_lib_param_bn::ModelAnnotation;
+
+use crate::sketchbook::data_structs::{
+    DatasetData, DynPropertyData, SketchData, StatPropertyData, UninterpretedFnData, VariableData,
+};
 use crate::sketchbook::{JsonSerde, Sketch};
 use std::fs::File;
 use std::io::Write;
@@ -24,3 +28,78 @@ impl Sketch {
         Ok(())
     }
 }
+
+impl Sketch {
+    /// Convert the sketch instance into a customized version of AEON model format.
+    ///
+    /// This format includes the standard AEON format for PSBN and layout.
+    /// This format is compatible with other biodivine tools, but might not cover all
+    /// parts of the sketch.
+    ///
+    /// Apart from that, most remaining details of the sketch are given via model annotations.
+    /// Currently the annotations are given simpy as
+    ///   #!entity_type: ID: #`json_string`#
+    /// These entities can be variables, functions, static/dynamic properties, and datasets.
+    pub fn to_aeon(&self) -> String {
+        // for standard part of aeon format, we use the transformation into aeon BN
+        // this loses some info (like new regulation types), but that is preserved via annotations
+        let bn = self.model.to_bn();
+        let mut aeon_str = bn.to_string();
+
+        // set layout info
+        let default_layout = self.model.get_default_layout();
+        for (var_id, node) in default_layout.layout_nodes() {
+            // write position in format #position:ID:X,Y
+            let pos = node.get_position();
+            let node_layout_str = format!("#position:{var_id}:{},{}\n", pos.0, pos.1);
+            aeon_str.push_str(&node_layout_str);
+        }
+
+        // set the rest using aeon model annotations
+        let mut annotation = ModelAnnotation::new();
+
+        // set static properties
+        for (id, stat_prop) in self.properties.stat_props() {
+            let prop_data_json = StatPropertyData::from_property(id, stat_prop).to_json_str();
+            annotation.ensure_value(&["static_property", id.as_str()], &prop_data_json);
+        }
+        // set dynamic properties
+        for (id, dyn_prop) in self.properties.dyn_props() {
+            let prop_data_json = DynPropertyData::from_property(id, dyn_prop).to_json_str();
+            annotation.ensure_value(&["dynamic_property", id.as_str()], &prop_data_json);
+        }
+        // set datasets
+        for (id, dataset) in self.observations.datasets() {
+            let dataset_data_json = DatasetData::from_dataset(id, dataset).to_json_str();
+            annotation.ensure_value(&["dataset", id.as_str()], &dataset_data_json);
+        }
+        // set variable details
+        for (var_id, variable) in self.model.variables() {
+            let update_fn = self.model.get_update_fn(var_id).unwrap();
+            let var_data_json = VariableData::from_var(var_id, variable, update_fn).to_json_str();
+            annotation.ensure_value(&["variable", var_id.as_str()], &var_data_json);
+        }
+        // set function details
+        for (fn_id, uninterpreted_fn) in self.model.uninterpreted_fns() {
+            let fn_data_json = UninterpretedFnData::from_fn(fn_id, uninterpreted_fn).to_json_str();
+            annotation.ensure_value(&["function", fn_id.as_str()], &fn_data_json);
+        }
+
+        // push the annotations to the aeon string
+        let annotation_str = annotation.to_string();
+        aeon_str.push_str(&annotation_str);
+        aeon_str
+    }
+
+    /// Export the sketch instance into a customized version of AEON model format.
+    ///
+    /// See [Sketch::to_aeon] for details on the actual conversion.
+    pub fn export_to_aeon(&self, filepath: &str) -> Result<(), String> {
+        let aeon_str = self.to_aeon();
+        let mut file = File::create(filepath).map_err(|e| e.to_string())?;
+        // write sketch in AEON to the file
+        file.write_all(aeon_str.as_bytes())
+            .map_err(|e| e.to_string())?;
+        Ok(())
+    }
+}