Inference progress and results handling (#51)

* Fix issues with vite config, add license and some details.

* Modify the way how computation progress/results are displayed.

* Slightly refactor analysis, clean redundant parts.

* Refactor inference progress/results handling.

* Add sanitizing & bdd dumping, modify window sizes, change unsat messages.

LICENSE

@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2023 Sybila
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

src-tauri/Cargo.toml

@@ -1,11 +1,12 @@
 [package]
 name = "aeon-sketchbook"
 version = "0.0.0"
-description = "A Tauri App"
-authors = ["you"]
-license = ""
-repository = ""
+description = "A multi-platform application for designing and analysing large-scale logical models."
+authors = ["Ondrej Huvar <[email protected]>", "Samuel Pastva <[email protected]>", "Petr Ivicic"]
+license = "MIT"
+repository = "https://github.com/sybila/biodivine-aeon-sketchbook"
 edition = "2021"
+readme = "README.md"
 
 [build-dependencies]
 tauri-build = { version = "1.5", features = [] }
@@ -21,10 +22,11 @@ rand = "0.8.5"
 regex = "1.10.6"
 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"] }
+tauri = { version = "1.6", features = ["dialog-all", "os-all", "path-all", "shell-open", "window-close", "window-create", "window-set-focus", "window-set-size"] }
 tokio = { version = "1.40.0", features = ["sync"] }
 zip = "0.6.3"
 num-bigint = "0.4.4"
+num-traits = "0.2.19"
 
 [features]
 # this feature is used for production builds or when `devPath` points to the filesystem

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

@@ -1,6 +1,6 @@
 use crate::algorithms::eval_dynamic::encode::encode_dataset_hctl_str;
 use crate::sketchbook::observations::Dataset;
-use crate::sketchbook::properties::dynamic_props::{DynProperty, DynPropertyType};
+use crate::sketchbook::properties::dynamic_props::DynPropertyType;
 use crate::sketchbook::Sketch;
 
 /// Enum of possible variants of data to encode.
@@ -14,13 +14,15 @@ pub enum DataEncodingType {
 /// Property requiring that a particular HCTL formula is satisfied.
 #[derive(Clone, Debug, Eq, PartialEq)]
 pub struct ProcessedHctlFormula {
+    pub id: String,
     pub formula: String,
 }
 
 /// Property requiring that observations in a particular dataset are trap spaces.
 /// The trap space might be required to be `minimal` or `non-percolable`.
 #[derive(Clone, Debug, Eq, PartialEq)]
 pub struct ProcessedTrapSpace {
+    pub id: String,
     pub dataset: Dataset,
     pub minimal: bool,
     pub nonpercolable: bool,
@@ -29,6 +31,7 @@ pub struct ProcessedTrapSpace {
 /// Property requiring that the number of attractors falls into the range <minimal, maximal>.
 #[derive(Clone, Debug, Eq, PartialEq)]
 pub struct ProcessedAttrCount {
+    pub id: String,
     pub minimal: usize,
     pub maximal: usize,
 }
@@ -44,17 +47,24 @@ pub enum ProcessedDynProp {
 /// Simplified constructors for processed dynamic properties.
 impl ProcessedDynProp {
     /// Create HCTL `ProcessedDynProp` instance.
-    pub fn mk_hctl(formula: &str) -> ProcessedDynProp {
+    pub fn mk_hctl(id: &str, formula: &str) -> ProcessedDynProp {
         let property = ProcessedHctlFormula {
+            id: id.to_string(),
             formula: formula.to_string(),
         };
         ProcessedDynProp::ProcessedHctlFormula(property)
     }
 
     /// Create trap-space `ProcessedDynProp` instance.
     /// To encode single observation, make a singleton dataset.
-    pub fn mk_trap_space(dataset: Dataset, minimal: bool, nonpercolable: bool) -> ProcessedDynProp {
+    pub fn mk_trap_space(
+        id: &str,
+        dataset: Dataset,
+        minimal: bool,
+        nonpercolable: bool,
+    ) -> ProcessedDynProp {
         let property = ProcessedTrapSpace {
+            id: id.to_string(),
             dataset,
             minimal,
             nonpercolable,
@@ -63,23 +73,35 @@ impl ProcessedDynProp {
     }
 
     /// Create attractor-count `ProcessedDynProp` instance.
-    pub fn mk_attr_count(minimal: usize, maximal: usize) -> ProcessedDynProp {
-        let property = ProcessedAttrCount { minimal, maximal };
+    pub fn mk_attr_count(id: &str, minimal: usize, maximal: usize) -> ProcessedDynProp {
+        let property = ProcessedAttrCount {
+            id: id.to_string(),
+            minimal,
+            maximal,
+        };
         ProcessedDynProp::ProcessedAttrCount(property)
     }
+
+    /// Get ID of the underlying processed property.
+    pub fn id(&self) -> &str {
+        match &self {
+            ProcessedDynProp::ProcessedHctlFormula(prop) => &prop.id,
+            ProcessedDynProp::ProcessedAttrCount(prop) => &prop.id,
+            ProcessedDynProp::ProcessedTrapSpace(prop) => &prop.id,
+        }
+    }
 }
 
+/// Process dynamic properties in a sketch, converting them into one of the supported
+/// `ProcessedDynProp` variants. That usually means encoding them into HCTL, or doing
+/// some other preprocessing.
 pub fn process_dynamic_props(sketch: &Sketch) -> Result<Vec<ProcessedDynProp>, String> {
     let mut dynamic_props = sketch.properties.dyn_props().collect::<Vec<_>>();
     // sort properties by IDs for deterministic computation times (and get rid of the IDs)
     dynamic_props.sort_by(|(a_id, _), (b_id, _)| a_id.cmp(b_id));
-    let dynamic_props: Vec<DynProperty> = dynamic_props
-        .into_iter()
-        .map(|(_, prop)| prop.clone())
-        .collect();
 
     let mut processed_props = Vec::new();
-    for dyn_prop in dynamic_props {
+    for (id, dyn_prop) in dynamic_props {
         // TODO: currently, some types of properties (like time-series) are still not implemented
 
         // we translate as many types of properties into HCTL, but we also treat some
@@ -88,7 +110,7 @@ pub fn process_dynamic_props(sketch: &Sketch) -> Result<Vec<ProcessedDynProp>, S
         let dyn_prop_processed = match dyn_prop.get_prop_data() {
             // handled as a special case
             DynPropertyType::AttractorCount(prop) => {
-                ProcessedDynProp::mk_attr_count(prop.minimal, prop.maximal)
+                ProcessedDynProp::mk_attr_count(id.as_str(), prop.minimal, prop.maximal)
             }
             // handled as a special case
             DynPropertyType::ExistsTrapSpace(prop) => {
@@ -103,11 +125,16 @@ pub fn process_dynamic_props(sketch: &Sketch) -> Result<Vec<ProcessedDynProp>, S
                     dataset = Dataset::new(vec![observation], var_names_ref)?;
                 }
 
-                ProcessedDynProp::mk_trap_space(dataset, prop.minimal, prop.nonpercolable)
+                ProcessedDynProp::mk_trap_space(
+                    id.as_str(),
+                    dataset,
+                    prop.minimal,
+                    prop.nonpercolable,
+                )
             }
             // default generic HCTL
             DynPropertyType::GenericDynProp(prop) => {
-                ProcessedDynProp::mk_hctl(prop.processed_formula.as_str())
+                ProcessedDynProp::mk_hctl(id.as_str(), prop.processed_formula.as_str())
             }
             // translate to generic HCTL
             DynPropertyType::ExistsFixedPoint(prop) => {
@@ -119,7 +146,7 @@ pub fn process_dynamic_props(sketch: &Sketch) -> Result<Vec<ProcessedDynProp>, S
                     prop.observation.clone(),
                     DataEncodingType::FixedPoint,
                 )?;
-                ProcessedDynProp::mk_hctl(&formula)
+                ProcessedDynProp::mk_hctl(id.as_str(), &formula)
             }
             // translate to generic HCTL
             DynPropertyType::HasAttractor(prop) => {
@@ -131,7 +158,7 @@ pub fn process_dynamic_props(sketch: &Sketch) -> Result<Vec<ProcessedDynProp>, S
                     prop.observation.clone(),
                     DataEncodingType::Attractor,
                 )?;
-                ProcessedDynProp::mk_hctl(&formula)
+                ProcessedDynProp::mk_hctl(id.as_str(), &formula)
             }
             // TODO: finish handling of time-series
             DynPropertyType::ExistsTrajectory(..) => todo!(),

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

@@ -1,5 +1,5 @@
 use crate::algorithms::eval_static::encode::*;
-use crate::sketchbook::properties::static_props::{StatProperty, StatPropertyType};
+use crate::sketchbook::properties::static_props::StatPropertyType;
 use crate::sketchbook::Sketch;
 
 use biodivine_lib_param_bn::BooleanNetwork;
@@ -10,37 +10,43 @@ use biodivine_lib_param_bn::BooleanNetwork;
 /// the one used for dynamic props).
 #[derive(Clone, Debug, Eq, PartialEq)]
 pub struct ProcessedStatProp {
+    pub id: String,
     pub formula: String,
 }
 
 /// Simplified constructors for processed dynamic properties.
 impl ProcessedStatProp {
     /// Create FOL `ProcessedStatProp` instance.
-    pub fn mk_fol(formula: &str) -> ProcessedStatProp {
+    pub fn mk_fol(id: &str, formula: &str) -> ProcessedStatProp {
         ProcessedStatProp {
+            id: id.to_string(),
             formula: formula.to_string(),
         }
     }
+
+    /// Get ID of the processed property.
+    pub fn id(&self) -> &str {
+        &self.id
+    }
 }
 
+/// Process static properties from a sketch, converting them into one of the supported
+/// `ProcessedStatProp` variants. Currently, all properties are encoded into FOL, but we
+/// might support some other preprocessing in future.
 pub fn process_static_props(
     sketch: &Sketch,
     bn: &BooleanNetwork,
 ) -> Result<Vec<ProcessedStatProp>, String> {
     let mut static_props = sketch.properties.stat_props().collect::<Vec<_>>();
     // sort properties by IDs for deterministic computation times (and get rid of the IDs)
     static_props.sort_by(|(a_id, _), (b_id, _)| a_id.cmp(b_id));
-    let static_props: Vec<StatProperty> = static_props
-        .into_iter()
-        .map(|(_, prop)| prop.clone())
-        .collect();
 
     let mut processed_props = Vec::new();
-    for stat_prop in static_props {
+    for (id, stat_prop) in static_props {
         // currently, everything is encoded into first-order logic (into a "generic" property)
         let stat_prop_processed = match stat_prop.get_prop_data() {
             StatPropertyType::GenericStatProp(prop) => {
-                ProcessedStatProp::mk_fol(prop.processed_formula.as_str())
+                ProcessedStatProp::mk_fol(id.as_str(), prop.processed_formula.as_str())
             }
             StatPropertyType::RegulationEssential(prop)
             | StatPropertyType::RegulationEssentialContext(prop) => {
@@ -55,7 +61,7 @@ pub fn process_static_props(
                 if let Some(context_formula) = &prop.context {
                     formula = encode_property_in_context(context_formula, &formula);
                 }
-                ProcessedStatProp::mk_fol(&formula)
+                ProcessedStatProp::mk_fol(id.as_str(), &formula)
             }
             StatPropertyType::RegulationMonotonic(prop)
             | StatPropertyType::RegulationMonotonicContext(prop) => {
@@ -70,7 +76,7 @@ pub fn process_static_props(
                 if let Some(context_formula) = &prop.context {
                     formula = encode_property_in_context(context_formula, &formula);
                 }
-                ProcessedStatProp::mk_fol(&formula)
+                ProcessedStatProp::mk_fol(id.as_str(), &formula)
             }
             StatPropertyType::FnInputEssential(prop)
             | StatPropertyType::FnInputEssentialContext(prop) => {
@@ -86,7 +92,7 @@ pub fn process_static_props(
                 if let Some(context_formula) = &prop.context {
                     formula = encode_property_in_context(context_formula, &formula);
                 }
-                ProcessedStatProp::mk_fol(&formula)
+                ProcessedStatProp::mk_fol(id.as_str(), &formula)
             }
             StatPropertyType::FnInputMonotonic(prop)
             | StatPropertyType::FnInputMonotonicContext(prop) => {
@@ -102,7 +108,7 @@ pub fn process_static_props(
                 if let Some(context_formula) = &prop.context {
                     formula = encode_property_in_context(context_formula, &formula);
                 }
-                ProcessedStatProp::mk_fol(&formula)
+                ProcessedStatProp::mk_fol(id.as_str(), &formula)
             }
         };
         processed_props.push(stat_prop_processed)

src-tauri/src/analysis/_test_inference/utils.rs

@@ -1,6 +1,6 @@
-use crate::analysis::analysis_results::AnalysisResults;
-use crate::analysis::analysis_type::AnalysisType;
+use crate::analysis::inference_results::InferenceResults;
 use crate::analysis::inference_solver::InferenceSolver;
+use crate::analysis::inference_type::InferenceType;
 use crate::app::event::Event;
 use crate::app::state::{Consumed, SessionState};
 use crate::sketchbook::properties::{DynProperty, StatProperty};
@@ -20,7 +20,7 @@ pub fn load_test_model() -> Sketch {
 }
 
 /// Wrapper to create an inference solver, run the inference on a given sketch, and return results.
-pub fn run_inference(sketch: Sketch) -> AnalysisResults {
+pub fn run_inference(sketch: Sketch) -> InferenceResults {
     run_inference_check_statuses(sketch, None)
 }
 
@@ -31,10 +31,10 @@ pub fn run_inference(sketch: Sketch) -> AnalysisResults {
 pub fn run_inference_check_statuses(
     sketch: Sketch,
     num_statuses: Option<usize>,
-) -> AnalysisResults {
+) -> InferenceResults {
     let (send_channel, rec_channel): (Sender<String>, Receiver<String>) = mpsc::channel();
     let mut solver = InferenceSolver::new(send_channel);
-    let results = solver.run_inference_modular(AnalysisType::Inference, sketch, true, true);
+    let results = solver.run_inference_modular(InferenceType::FullInference, sketch, true, true);
 
     // test cases are always valid sketches, so we just unwrap
     if let Some(expected_num) = num_statuses {
@@ -65,7 +65,7 @@ pub fn apply_event_fully(sketch: &mut Sketch, event: &Event, at_path: &[&str]) {
 
 /// Wrapper to add a given dynamic property to the model, run the inference, and return the number  
 /// of satisfying candidates.
-pub fn add_dyn_prop_and_infer(mut sketch: Sketch, property: DynProperty, id_str: &str) -> u64 {
+pub fn add_dyn_prop_and_infer(mut sketch: Sketch, property: DynProperty, id_str: &str) -> u128 {
     sketch
         .properties
         .add_raw_dynamic_by_str(id_str, property)
@@ -76,7 +76,7 @@ pub fn add_dyn_prop_and_infer(mut sketch: Sketch, property: DynProperty, id_str:
 
 /// Wrapper to add a given static property to the model, run the inference, and return the number  
 /// of satisfying candidates.
-pub fn add_stat_prop_and_infer(mut sketch: Sketch, property: StatProperty, id_str: &str) -> u64 {
+pub fn add_stat_prop_and_infer(mut sketch: Sketch, property: StatProperty, id_str: &str) -> u128 {
     sketch
         .properties
         .add_raw_static_by_str(id_str, property)