From 9e8c7ec6e0ae8b6c759a3f0993b46b1bcc69357a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ond=C5=99ej=20Huvar?= <492849@mail.muni.cz> Date: Sun, 14 Jul 2024 16:01:45 +0200 Subject: [PATCH 1/8] wip: Add prototype analysis window, restructure project. --- src-tauri/Cargo.toml | 3 +- src-tauri/src/algorithms/mod.rs | 1 + src-tauri/src/analysis/mod.rs | 40 ++++ .../state/analysis/_state_analysis_session.rs | 210 ++++++++++++++++++ src-tauri/src/app/state/analysis/mod.rs | 4 + .../app/state/editor/_state_editor_session.rs | 5 +- src-tauri/src/app/state/mod.rs | 2 + src-tauri/src/lib.rs | 7 + src-tauri/src/main.rs | 71 +++++- .../properties/dynamic_props/_hctl_formula.rs | 2 +- src/aeon_events.ts | 28 +++ src/html/analysis.html | 6 + .../analysis-component.less} | 0 .../analysis-component/analysis-component.ts | 71 ++++++ .../tauri_welcome.html | 0 .../analysis-tab/analysis-tab.less | 54 +++++ .../analysis-tab/analysis-tab.ts | 45 ++++ .../content-pane/content-pane.less | 0 .../content-pane/content-pane.ts | 1 + .../editor-tile/custom-ace.conf.ts | 0 .../editor-tile/editor-tile.less | 0 .../editor-tile/editor-tile.ts | 0 .../editor-tile/function-tile.ts | 0 .../editor-tile/variable-tile.ts | 0 .../functions-editor/functions-editor.less | 0 .../functions-editor/functions-editor.ts | 0 .../menu/menu.less | 0 .../menu/menu.ts | 0 .../nav-bar/nav-bar.less | 0 .../nav-bar/nav-bar.ts | 0 .../edit-observation/edit-observation.html | 0 .../edit-observation/edit-observation.less | 0 .../edit-observation/edit-observation.ts | 0 .../observations-editor.less | 0 .../observations-editor.ts | 2 +- .../observations-import.html | 0 .../observations-import.less | 0 .../observations-import.ts | 0 .../observations-set/observations-set.less | 0 .../observations-set/observations-set.ts | 2 +- .../observations-editor/tabulator-style.less | 0 .../observations-editor/tabulator-utility.ts | 0 .../abstract-property/abstract-property.less | 0 .../abstract-property/abstract-property.ts | 0 .../properties-editor/default-properties.ts | 0 .../dynamic/abstract-dynamic-property.ts | 0 .../dynamic-attractor-count.less | 0 .../dynamic-attractor-count.ts | 0 .../dynamic-generic/dynamic-generic.less | 0 .../dynamic-generic/dynamic-generic.ts | 0 .../dynamic-obs-selection.less | 0 .../dynamic-obs-selection.ts | 0 .../properties-editor/properties-editor.less | 0 .../properties-editor/properties-editor.ts | 0 .../static/abstract-static-property.ts | 0 .../static/static-generic/static-generic.less | 0 .../static/static-generic/static-generic.ts | 0 .../static-input-essential-condition.less | 0 .../static-input-essential-condition.ts | 0 .../static-input-essential.less | 0 .../static-input-essential.ts | 0 .../static-input-monotonic-condition.less | 0 .../static-input-monotonic-condition.ts | 0 .../static-input-monotonic.less | 0 .../static-input-monotonic.ts | 0 .../static/static-selectors-property.ts | 0 .../float-menu/float-menu.less | 0 .../float-menu/float-menu.ts | 0 .../regulations-editor.config.ts | 0 .../regulations-editor.less | 0 .../regulations-editor/regulations-editor.ts | 2 +- .../rename-dialog/rename-dialog.html | 0 .../rename-dialog/rename-dialog.less | 0 .../rename-dialog/rename-dialog.ts | 0 .../root-component/root-component.less | 42 ++++ .../root-component/root-component.ts | 0 .../search/search.less | 0 .../search/search.ts | 0 .../tab-bar/tab-bar.less | 0 .../tab-bar/tab-bar.ts | 0 src/html/component-editor/tauri_welcome.html | 29 +++ .../undo-redo/undo-redo.less | 0 .../undo-redo/undo-redo.ts | 0 src/html/signpost.html | 4 +- src/html/sketch-editor.html | 2 +- src/html/state-space-explorer.html | 2 +- src/html/util/config.ts | 12 +- 87 files changed, 620 insertions(+), 27 deletions(-) create mode 100644 src-tauri/src/algorithms/mod.rs create mode 100644 src-tauri/src/analysis/mod.rs create mode 100644 src-tauri/src/app/state/analysis/_state_analysis_session.rs create mode 100644 src-tauri/src/app/state/analysis/mod.rs create mode 100644 src/html/analysis.html rename src/html/{component/root-component/root-component.less => component-analysis/analysis-component/analysis-component.less} (100%) create mode 100644 src/html/component-analysis/analysis-component/analysis-component.ts rename src/html/{component => component-analysis}/tauri_welcome.html (100%) create mode 100644 src/html/component-editor/analysis-tab/analysis-tab.less create mode 100644 src/html/component-editor/analysis-tab/analysis-tab.ts rename src/html/{component => component-editor}/content-pane/content-pane.less (100%) rename src/html/{component => component-editor}/content-pane/content-pane.ts (97%) rename src/html/{component => component-editor}/functions-editor/editor-tile/custom-ace.conf.ts (100%) rename src/html/{component => component-editor}/functions-editor/editor-tile/editor-tile.less (100%) rename src/html/{component => component-editor}/functions-editor/editor-tile/editor-tile.ts (100%) rename src/html/{component => component-editor}/functions-editor/editor-tile/function-tile.ts (100%) rename src/html/{component => component-editor}/functions-editor/editor-tile/variable-tile.ts (100%) rename src/html/{component => component-editor}/functions-editor/functions-editor.less (100%) rename src/html/{component => component-editor}/functions-editor/functions-editor.ts (100%) rename src/html/{component => component-editor}/menu/menu.less (100%) rename src/html/{component => component-editor}/menu/menu.ts (100%) rename src/html/{component => component-editor}/nav-bar/nav-bar.less (100%) rename src/html/{component => component-editor}/nav-bar/nav-bar.ts (100%) rename src/html/{component => component-editor}/observations-editor/edit-observation/edit-observation.html (100%) rename src/html/{component => component-editor}/observations-editor/edit-observation/edit-observation.less (100%) rename src/html/{component => component-editor}/observations-editor/edit-observation/edit-observation.ts (100%) rename src/html/{component => component-editor}/observations-editor/observations-editor.less (100%) rename src/html/{component => component-editor}/observations-editor/observations-editor.ts (99%) rename src/html/{component => component-editor}/observations-editor/observations-import/observations-import.html (100%) rename src/html/{component => component-editor}/observations-editor/observations-import/observations-import.less (100%) rename src/html/{component => component-editor}/observations-editor/observations-import/observations-import.ts (100%) rename src/html/{component => component-editor}/observations-editor/observations-set/observations-set.less (100%) rename src/html/{component => component-editor}/observations-editor/observations-set/observations-set.ts (98%) rename src/html/{component => component-editor}/observations-editor/tabulator-style.less (100%) rename src/html/{component => component-editor}/observations-editor/tabulator-utility.ts (100%) rename src/html/{component => component-editor}/properties-editor/abstract-property/abstract-property.less (100%) rename src/html/{component => component-editor}/properties-editor/abstract-property/abstract-property.ts (100%) rename src/html/{component => component-editor}/properties-editor/default-properties.ts (100%) rename src/html/{component => component-editor}/properties-editor/dynamic/abstract-dynamic-property.ts (100%) rename src/html/{component => component-editor}/properties-editor/dynamic/dynamic-attractor-count/dynamic-attractor-count.less (100%) rename src/html/{component => component-editor}/properties-editor/dynamic/dynamic-attractor-count/dynamic-attractor-count.ts (100%) rename src/html/{component => component-editor}/properties-editor/dynamic/dynamic-generic/dynamic-generic.less (100%) rename src/html/{component => component-editor}/properties-editor/dynamic/dynamic-generic/dynamic-generic.ts (100%) rename src/html/{component => component-editor}/properties-editor/dynamic/dynamic-obs-selection/dynamic-obs-selection.less (100%) rename src/html/{component => component-editor}/properties-editor/dynamic/dynamic-obs-selection/dynamic-obs-selection.ts (100%) rename src/html/{component => component-editor}/properties-editor/properties-editor.less (100%) rename src/html/{component => component-editor}/properties-editor/properties-editor.ts (100%) rename src/html/{component => component-editor}/properties-editor/static/abstract-static-property.ts (100%) rename src/html/{component => component-editor}/properties-editor/static/static-generic/static-generic.less (100%) rename src/html/{component => component-editor}/properties-editor/static/static-generic/static-generic.ts (100%) rename src/html/{component => component-editor}/properties-editor/static/static-input-essential-condition/static-input-essential-condition.less (100%) rename src/html/{component => component-editor}/properties-editor/static/static-input-essential-condition/static-input-essential-condition.ts (100%) rename src/html/{component => component-editor}/properties-editor/static/static-input-essential/static-input-essential.less (100%) rename src/html/{component => component-editor}/properties-editor/static/static-input-essential/static-input-essential.ts (100%) rename src/html/{component => component-editor}/properties-editor/static/static-input-monotonic-condition/static-input-monotonic-condition.less (100%) rename src/html/{component => component-editor}/properties-editor/static/static-input-monotonic-condition/static-input-monotonic-condition.ts (100%) rename src/html/{component => component-editor}/properties-editor/static/static-input-monotonic/static-input-monotonic.less (100%) rename src/html/{component => component-editor}/properties-editor/static/static-input-monotonic/static-input-monotonic.ts (100%) rename src/html/{component => component-editor}/properties-editor/static/static-selectors-property.ts (100%) rename src/html/{component => component-editor}/regulations-editor/float-menu/float-menu.less (100%) rename src/html/{component => component-editor}/regulations-editor/float-menu/float-menu.ts (100%) rename src/html/{component => component-editor}/regulations-editor/regulations-editor.config.ts (100%) rename src/html/{component => component-editor}/regulations-editor/regulations-editor.less (100%) rename src/html/{component => component-editor}/regulations-editor/regulations-editor.ts (99%) rename src/html/{component => component-editor}/regulations-editor/rename-dialog/rename-dialog.html (100%) rename src/html/{component => component-editor}/regulations-editor/rename-dialog/rename-dialog.less (100%) rename src/html/{component => component-editor}/regulations-editor/rename-dialog/rename-dialog.ts (100%) create mode 100644 src/html/component-editor/root-component/root-component.less rename src/html/{component => component-editor}/root-component/root-component.ts (100%) rename src/html/{component => component-editor}/search/search.less (100%) rename src/html/{component => component-editor}/search/search.ts (100%) rename src/html/{component => component-editor}/tab-bar/tab-bar.less (100%) rename src/html/{component => component-editor}/tab-bar/tab-bar.ts (100%) create mode 100644 src/html/component-editor/tauri_welcome.html rename src/html/{component => component-editor}/undo-redo/undo-redo.less (100%) rename src/html/{component => component-editor}/undo-redo/undo-redo.ts (100%) diff --git a/src-tauri/Cargo.toml b/src-tauri/Cargo.toml index 52fef6a..cc196a4 100644 --- a/src-tauri/Cargo.toml +++ b/src-tauri/Cargo.toml @@ -13,13 +13,14 @@ 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" csv = "1.3" lazy_static = "1.4.0" 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" +chrono = "0.4.38" [features] # this feature is used for production builds or when `devPath` points to the filesystem diff --git a/src-tauri/src/algorithms/mod.rs b/src-tauri/src/algorithms/mod.rs new file mode 100644 index 0000000..70b786d --- /dev/null +++ b/src-tauri/src/algorithms/mod.rs @@ -0,0 +1 @@ +// TODO diff --git a/src-tauri/src/analysis/mod.rs b/src-tauri/src/analysis/mod.rs new file mode 100644 index 0000000..360292e --- /dev/null +++ b/src-tauri/src/analysis/mod.rs @@ -0,0 +1,40 @@ +use crate::app::event::Event; +use crate::app::state::{Consumed, SessionHelper, SessionState}; +use crate::app::DynError; +use crate::debug; +use crate::sketchbook::Sketch; +use serde::{Deserialize, Serialize}; + +/// Object encompassing all of the state components of the Analysis. +#[derive(Clone, Debug, PartialEq, Serialize, Deserialize)] +pub struct AnalysisState { + /// Boolean network sketch to run the analysis on. + sketch: Sketch, + // TODO +} + +impl AnalysisState { + pub fn new(sketch: Sketch) -> AnalysisState { + AnalysisState { sketch } + } +} + +impl SessionHelper for AnalysisState {} + +impl SessionState for AnalysisState { + fn perform_event(&mut self, event: &Event, at_path: &[&str]) -> Result { + debug!( + "Events for analysis not implemented! Can't process {:?} at {:?}", + event, at_path + ); + todo!() + } + + fn refresh(&self, full_path: &[String], at_path: &[&str]) -> Result { + debug!( + "Refresh for analysis not implemented! Can't process {:?} {:?}", + full_path, at_path + ); + todo!() + } +} diff --git a/src-tauri/src/app/state/analysis/_state_analysis_session.rs b/src-tauri/src/app/state/analysis/_state_analysis_session.rs new file mode 100644 index 0000000..d933354 --- /dev/null +++ b/src-tauri/src/app/state/analysis/_state_analysis_session.rs @@ -0,0 +1,210 @@ +use crate::analysis::AnalysisState; +use crate::app::event::{Event, StateChange, UserAction}; +use crate::app::state::_undo_stack::UndoStack; +use crate::app::state::{Consumed, Session, SessionHelper, SessionState}; +use crate::app::{AeonError, DynError}; +use crate::debug; +use crate::sketchbook::Sketch; + +/// The state of one editor session. +/// +/// An analysis session is the session where the process of the inference is run on a given model. +pub struct AnalysisSession { + id: String, + undo_stack: UndoStack, + analysis_state: AnalysisState, +} + +impl AnalysisSession { + pub fn new(id: &str, sketch: Sketch) -> AnalysisSession { + AnalysisSession { + id: id.to_string(), + undo_stack: UndoStack::default(), + analysis_state: AnalysisState::new(sketch), + } + } + + fn perform_action( + &mut self, + action: &UserAction, + ignore_stack: bool, + ) -> Result { + // Events that need to be consume (last to first) in order to complete this action. + let mut to_perform = action.events.clone(); + to_perform.reverse(); + + // The events representing successful state changes. + let mut state_changes: Vec = Vec::new(); + // The events that can be used to create a redo stack entry if the action is reversible. + let mut reverse: Option> = + if ignore_stack { None } else { Some(Vec::new()) }; + let mut reset_stack = false; + + while let Some(event) = to_perform.pop() { + let event_path = event.path.iter().map(|it| it.as_str()).collect::>(); + debug!( + "Executing event to session {}: `{:?}`.", + self.id, event_path + ); + let result = match self.perform_event(&event, &event_path) { + Ok(result) => result, + Err(error) => { + // TODO: + // We should probably first emit the state change and then the + // error, because now we are losing state of compound actions that fail. + return Err(error); + } + }; + match result { + Consumed::Reversible { + state_change, + perform_reverse, + } => { + state_changes.push(state_change); + if let Some(reverse) = reverse.as_mut() { + // If we can reverse this action, save the events. + reverse.push(perform_reverse); + } + } + Consumed::Irreversible { + state_change, + reset, + } => { + state_changes.push(state_change); + if reset { + // We cannot reverse this event, but the rest can be reversed. + reverse = None; + reset_stack = true; + } + } + Consumed::Restart(mut events) => { + // Just push the new events to the execution stack and continue + // to the next event. + events.reverse(); + while let Some(e) = events.pop() { + to_perform.push(e); + } + } + Consumed::InputError(error) => { + // TODO: + // The same as above. We should report this as a separate event from the + // state change that was performed. + return Err(error); + } + Consumed::NoChange => { + // Do nothing. + } + } + } + + // If the action is not irreversible, we should add an entry to the undo stack. + if let Some(events) = reverse { + if !events.is_empty() { + // Only add undo action if the stack is not empty. + let mut perform = Vec::new(); + let mut reverse = Vec::new(); + for (p, r) in events { + perform.push(p); + reverse.push(r); + } + // Obviously, the "reverse" events need to be execute in the opposite order + // compared to the "perform" events. + reverse.reverse(); + let perform = UserAction { events: perform }; + let reverse = UserAction { events: reverse }; + if !self.undo_stack.do_action(perform, reverse) { + // TODO: Not match we can do here, maybe except issuing a warning. + self.undo_stack.clear(); + } + + // Notify about the changes in the stack state. + // TODO: Maybe we don't need to emit this always. + self.append_stack_updates(&mut state_changes); + } + } else if !ignore_stack && reset_stack { + debug!("Back stack cleared due to irreversible action."); + self.undo_stack.clear(); + } + + Ok(StateChange { + events: state_changes, + }) + } + + fn append_stack_updates(&self, state_changes: &mut Vec) { + let can_undo = serde_json::to_string(&self.undo_stack.can_undo()); + let can_redo = serde_json::to_string(&self.undo_stack.can_redo()); + state_changes.push(Event::build( + &["undo_stack", "can_undo"], + Some(can_undo.unwrap().as_str()), + )); + state_changes.push(Event::build( + &["undo_stack", "can_redo"], + Some(can_redo.unwrap().as_str()), + )); + } +} + +impl Session for AnalysisSession { + fn perform_action(&mut self, action: &UserAction) -> Result { + // Explicit test for undo-stack actions. + // TODO: + // Figure out a nicer way to do this. Probably modify the `Consumed` enum? + // We basically need a way to say "restart with these events, but as an + // Irreversible action that won't reset the stack." + 'undo: { + if action.events.len() == 1 { + let event = &action.events[0]; + if event.path.len() == 2 && event.path[0] == "undo_stack" { + let action = match event.path[1].as_str() { + "undo" => { + let Some(undo) = self.undo_stack.undo_action() else { + return AeonError::throw("Nothing to undo."); + }; + undo + } + "redo" => { + let Some(redo) = self.undo_stack.redo_action() else { + return AeonError::throw("Nothing to redo."); + }; + redo + } + _ => break 'undo, + }; + let mut state_change = self.perform_action(&action, true)?; + self.append_stack_updates(&mut state_change.events); + return Ok(state_change); + } + } + } + self.perform_action(action, false) + } + + fn id(&self) -> &str { + self.id.as_str() + } +} + +impl SessionHelper for AnalysisSession {} + +impl SessionState for AnalysisSession { + fn perform_event(&mut self, event: &Event, at_path: &[&str]) -> Result { + if let Some(at_path) = Self::starts_with("undo_stack", at_path) { + self.undo_stack.perform_event(event, at_path) + } else if let Some(at_path) = Self::starts_with("analysis", at_path) { + self.analysis_state.perform_event(event, at_path) + } else { + Self::invalid_path_error_generic(at_path) + } + } + + fn refresh(&self, full_path: &[String], at_path: &[&str]) -> Result { + if let Some(at_path) = Self::starts_with("undo_stack", at_path) { + self.undo_stack.refresh(full_path, at_path) + } else if let Some(at_path) = Self::starts_with("analysis", at_path) { + self.analysis_state.refresh(full_path, at_path) + } else { + Self::invalid_path_error_generic(at_path) + } + } +} diff --git a/src-tauri/src/app/state/analysis/mod.rs b/src-tauri/src/app/state/analysis/mod.rs new file mode 100644 index 0000000..250d528 --- /dev/null +++ b/src-tauri/src/app/state/analysis/mod.rs @@ -0,0 +1,4 @@ +/// Declares [AnalysisSession]: the root state object of the sketchbook editor. +mod _state_analysis_session; + +pub use _state_analysis_session::AnalysisSession; diff --git a/src-tauri/src/app/state/editor/_state_editor_session.rs b/src-tauri/src/app/state/editor/_state_editor_session.rs index 3237155..1fa39cf 100644 --- a/src-tauri/src/app/state/editor/_state_editor_session.rs +++ b/src-tauri/src/app/state/editor/_state_editor_session.rs @@ -45,7 +45,10 @@ impl EditorSession { while let Some(event) = to_perform.pop() { let event_path = event.path.iter().map(|it| it.as_str()).collect::>(); - debug!("Executing event: `{:?}`.", event_path); + debug!( + "Executing event to session {}: `{:?}`.", + self.id, event_path + ); let result = match self.perform_event(&event, &event_path) { Ok(result) => result, Err(error) => { diff --git a/src-tauri/src/app/state/mod.rs b/src-tauri/src/app/state/mod.rs index 90a9d8a..4ec1556 100644 --- a/src-tauri/src/app/state/mod.rs +++ b/src-tauri/src/app/state/mod.rs @@ -7,6 +7,8 @@ mod _state_atomic; mod _state_map; pub mod _undo_stack; +/// Declares state objects that are unique to the sketchbook analysis window. +pub mod analysis; /// Declares state objects that are unique to the sketchbook editor window. pub mod editor; diff --git a/src-tauri/src/lib.rs b/src-tauri/src/lib.rs index 8c3c246..ed4a987 100644 --- a/src-tauri/src/lib.rs +++ b/src-tauri/src/lib.rs @@ -2,6 +2,13 @@ extern crate lazy_static; extern crate core; +/// Algorithms for the inference process. +pub mod algorithms; +/// State of the inference analysis tab. +pub mod analysis; +/// General functionality for window mechanism, event stack, tab management, and more. pub mod app; +/// Logging utilities. pub mod logging; +/// State of the sketchbook editor tab. pub mod sketchbook; diff --git a/src-tauri/src/main.rs b/src-tauri/src/main.rs index 1960a38..d67fcfa 100644 --- a/src-tauri/src/main.rs +++ b/src-tauri/src/main.rs @@ -2,10 +2,15 @@ #![cfg_attr(not(debug_assertions), windows_subsystem = "windows")] use aeon_sketchbook::app::event::{Event, UserAction}; +use aeon_sketchbook::app::state::analysis::AnalysisSession; use aeon_sketchbook::app::state::editor::EditorSession; use aeon_sketchbook::app::state::{AppState, DynSession}; use aeon_sketchbook::app::{AeonApp, AEON_ACTION, AEON_REFRESH, AEON_VALUE}; use aeon_sketchbook::debug; +use aeon_sketchbook::sketchbook::data_structs::SketchData; +use aeon_sketchbook::sketchbook::JsonSerde; +use aeon_sketchbook::sketchbook::Sketch; +use chrono::prelude::*; use serde::{Deserialize, Serialize}; use tauri::{command, Manager, State, Window}; @@ -59,18 +64,62 @@ fn main() { let action = UserAction { events: event.events, }; - let result = state.consume_event(&aeon, session_id.as_str(), &action); - if let Err(e) = result { - // TODO: This should be a normal error. - //panic!("Event error: {:?}", e); - // TODO: This is only a temporary solution to propagate the error message to frontend. - debug!("Error processing last event: `{}`.", e.to_string()); - // A crude way to escape the error message and wrap it in quotes. - let json_message = serde_json::Value::String(e.to_string()).to_string(); - let state_change = Event::build(&["error"], Some(&json_message)); - if aeon.tauri.emit_all(AEON_VALUE, vec![state_change]).is_err() { - panic!("Event error failed to be sent: {:?}", e); + // TODO: this part should be probably moved elsewhere, just a placeholder for now + // check for "new-session" events here + if action.events.len() == 1 && action.events[0].path == ["new-analysis-session"] { + let payload = action.events[0] + .payload + .clone() + .ok_or( + "This `new-analysis-session` event cannot carry empty payload." + .to_string(), + ) + .unwrap(); + let sketch_data = SketchData::from_json_str(&payload).unwrap(); + let sketch = Sketch::new_from_sketch_data(&sketch_data).unwrap(); + + let time_now = Utc::now(); + let timestamp = time_now.timestamp(); + let new_session_id = format!("analysis-{timestamp}"); + let new_window_id = format!("analysis-{timestamp}-window"); + let new_session: DynSession = + Box::new(AnalysisSession::new(&new_session_id, sketch)); + state.session_created(&new_session_id, new_session); + state.window_created(&new_window_id, &new_session_id); + + // Create a new window for the analysis session + let new_window = tauri::WindowBuilder::new( + &handle, + &new_window_id, // The unique window label + tauri::WindowUrl::App("src/html/analysis.html".into()), // The URL or path to the HTML file + ) + .title(format!( + "Inference Workflow (opened on {})", + time_now.to_rfc2822() + )) + .build(); + + match new_window { + Ok(_) => debug!( + "New session `{new_session_id}` and window `{new_window_id}` created." + ), + Err(e) => panic!("Failed to create new window: {:?}", e), + } + } else { + let result = state.consume_event(&aeon, session_id.as_str(), &action); + if let Err(e) = result { + // TODO: This should be a normal error. + //panic!("Event error: {:?}", e); + + // TODO: This is only a temporary solution to propagate the error message to frontend. + debug!("Error processing last event: `{}`.", e.to_string()); + // A crude way to escape the error message and wrap it in quotes. + let json_message = serde_json::Value::String(e.to_string()).to_string(); + let state_change = Event::build(&["error"], Some(&json_message)); + if aeon.tauri.emit_all(AEON_VALUE, vec![state_change]).is_err() { + panic!("Event error failed to be sent: {:?}", e); + } } } }); diff --git a/src-tauri/src/sketchbook/properties/dynamic_props/_hctl_formula.rs b/src-tauri/src/sketchbook/properties/dynamic_props/_hctl_formula.rs index d23f91c..c64dc92 100644 --- a/src-tauri/src/sketchbook/properties/dynamic_props/_hctl_formula.rs +++ b/src-tauri/src/sketchbook/properties/dynamic_props/_hctl_formula.rs @@ -1,7 +1,7 @@ use crate::sketchbook::model::ModelState; use crate::sketchbook::observations::{Dataset, Observation}; use crate::sketchbook::properties::dynamic_props::_mk_hctl_formulas::*; -use biodivine_hctl_model_checker::preprocessing::node::HctlTreeNode; +use biodivine_hctl_model_checker::preprocessing::hctl_tree::HctlTreeNode; use biodivine_hctl_model_checker::preprocessing::parser::parse_hctl_formula; use serde::{de, Deserialize, Deserializer, Serialize, Serializer}; use std::fmt; diff --git a/src/aeon_events.ts b/src/aeon_events.ts index 0255c5c..bc3a813 100644 --- a/src/aeon_events.ts +++ b/src/aeon_events.ts @@ -343,6 +343,13 @@ interface AeonState { /** Error message provided by backend. */ errorReceived: Observable } + + /** Events for creating new sessions. */ + new_session: { + /** Create a new analysis session. */ + // TODO: this is just a placeholder for now + createNewAnalysisSession: () => void + } } /** An object representing all relevant parts of the whole sketch. */ @@ -860,6 +867,27 @@ export const aeonState: AeonState = { error: { errorReceived: new Observable(['error']) }, + new_session: { + // TODO: this is just a placeholder for now + createNewAnalysisSession (): void { + const model: ModelData = { + variables: [], + regulations: [], + uninterpreted_fns: [], + layouts: [] + } + const sketch: SketchData = { + model, + datasets: [], + dyn_properties: [], + stat_properties: [] + } + aeonEvents.emitAction({ + path: ['new-analysis-session'], + payload: JSON.stringify(sketch) + }) + } + }, sketch: { sketchRefreshed: new Observable(['sketch', 'get_whole_sketch']), refreshSketch (): void { diff --git a/src/html/analysis.html b/src/html/analysis.html new file mode 100644 index 0000000..f5d4c8b --- /dev/null +++ b/src/html/analysis.html @@ -0,0 +1,6 @@ + + + + + + \ No newline at end of file diff --git a/src/html/component/root-component/root-component.less b/src/html/component-analysis/analysis-component/analysis-component.less similarity index 100% rename from src/html/component/root-component/root-component.less rename to src/html/component-analysis/analysis-component/analysis-component.less diff --git a/src/html/component-analysis/analysis-component/analysis-component.ts b/src/html/component-analysis/analysis-component/analysis-component.ts new file mode 100644 index 0000000..b35ccd9 --- /dev/null +++ b/src/html/component-analysis/analysis-component/analysis-component.ts @@ -0,0 +1,71 @@ +import { css, html, LitElement, type TemplateResult, unsafeCSS } from 'lit' +import { customElement, property } from 'lit/decorators.js' +import style_less from './analysis-component.less?inline' +import { + aeonState +} from '../../../aeon_events' +import { + ContentData +} from '../../util/data-interfaces' +import { dialog } from '@tauri-apps/api' + +@customElement('analysis-component') +export default class AnalysisComponent extends LitElement { + static styles = css`${unsafeCSS(style_less)}` + @property() data: ContentData = ContentData.create() + + constructor () { + super() + + // error event listener + aeonState.error.errorReceived.addEventListener((e) => { + void this.#onErrorMessage(e) + }) + } + + async #onErrorMessage (errorMessage: string): Promise { + await dialog.message(errorMessage, { + type: 'error', + title: 'Error' + }) + } + + private async confirmDialog (): Promise { + return await dialog.ask('Are you sure?', { + type: 'warning', + okLabel: 'Delete', + cancelLabel: 'Keep', + title: 'Delete' + }) + } + + private async dummyDialog (): Promise { + return await dialog.ask('Hello there.', { + type: 'info', + okLabel: 'OK', + cancelLabel: 'Cancel', + title: 'Hello there' + }) + } + + render (): TemplateResult { + return html` +
+
+
+
+

Inference

+
+
+ +
+
+
+
+ ` + } +} diff --git a/src/html/component/tauri_welcome.html b/src/html/component-analysis/tauri_welcome.html similarity index 100% rename from src/html/component/tauri_welcome.html rename to src/html/component-analysis/tauri_welcome.html diff --git a/src/html/component-editor/analysis-tab/analysis-tab.less b/src/html/component-editor/analysis-tab/analysis-tab.less new file mode 100644 index 0000000..9478f3e --- /dev/null +++ b/src/html/component-editor/analysis-tab/analysis-tab.less @@ -0,0 +1,54 @@ +@import '/src/uikit-theme'; + +.container { + container-name: inference; + container-type: inline-size; + height: 100%; + width: 100%; +} + +.inference { + display: flex; + flex-direction: row; + width: 100%; + height: 100%; + justify-content: center; + overflow: auto; +} + +.section { + min-width: 25em; + max-width: 40em; + overflow: auto; + width: 50%; +} + +/* + Header sticks to the top of the list. +*/ + +.header { + .uk-flex; + .uk-flex-row; + .uk-flex-between; + .uk-flex-middle; + .uk-box-shadow-small; + padding: 0.5em 1em; + position: sticky; + top: 0; + z-index: 99; +} + +@heading-bullet-border: @text-dark; +.header h3 { + color: @text-dark; +} + +@container inference (max-width: 52em) { + + .section { + width: 100%; + overflow: unset; + } + +} diff --git a/src/html/component-editor/analysis-tab/analysis-tab.ts b/src/html/component-editor/analysis-tab/analysis-tab.ts new file mode 100644 index 0000000..8c6c8b8 --- /dev/null +++ b/src/html/component-editor/analysis-tab/analysis-tab.ts @@ -0,0 +1,45 @@ +import { css, html, LitElement, type TemplateResult, unsafeCSS } from 'lit' +import { customElement, property } from 'lit/decorators.js' +import style_less from './analysis-tab.less?inline' +import { ContentData } from '../../util/data-interfaces' +import { + aeonState +} from '../../../aeon_events' + +@customElement('analysis-tab') +export class AnalysisTab extends LitElement { + static styles = css`${unsafeCSS(style_less)}` + @property() contentData: ContentData = ContentData.create() + + constructor () { + super() + + // just a placeholder event so that eslint does not complain because of empty constructor for now + this.addEventListener('run-inference', () => { this.runInference() }) + } + + runInference (): void { + aeonState.new_session.createNewAnalysisSession() + } + + protected render (): TemplateResult { + return html` +
+
+
+
+

Inference

+
+
+ +
+
+
+
+ ` + } +} diff --git a/src/html/component/content-pane/content-pane.less b/src/html/component-editor/content-pane/content-pane.less similarity index 100% rename from src/html/component/content-pane/content-pane.less rename to src/html/component-editor/content-pane/content-pane.less diff --git a/src/html/component/content-pane/content-pane.ts b/src/html/component-editor/content-pane/content-pane.ts similarity index 97% rename from src/html/component/content-pane/content-pane.ts rename to src/html/component-editor/content-pane/content-pane.ts index 62c5896..6ce4c39 100644 --- a/src/html/component/content-pane/content-pane.ts +++ b/src/html/component-editor/content-pane/content-pane.ts @@ -7,6 +7,7 @@ import '../regulations-editor/regulations-editor' import '../functions-editor/functions-editor' import '../observations-editor/observations-editor' import '../properties-editor/properties-editor' +import '../analysis-tab/analysis-tab' import { faLock, faLockOpen } from '@fortawesome/free-solid-svg-icons' import { aeonState } from '../../../aeon_events' import { ContentData } from '../../util/data-interfaces' diff --git a/src/html/component/functions-editor/editor-tile/custom-ace.conf.ts b/src/html/component-editor/functions-editor/editor-tile/custom-ace.conf.ts similarity index 100% rename from src/html/component/functions-editor/editor-tile/custom-ace.conf.ts rename to src/html/component-editor/functions-editor/editor-tile/custom-ace.conf.ts diff --git a/src/html/component/functions-editor/editor-tile/editor-tile.less b/src/html/component-editor/functions-editor/editor-tile/editor-tile.less similarity index 100% rename from src/html/component/functions-editor/editor-tile/editor-tile.less rename to src/html/component-editor/functions-editor/editor-tile/editor-tile.less diff --git a/src/html/component/functions-editor/editor-tile/editor-tile.ts b/src/html/component-editor/functions-editor/editor-tile/editor-tile.ts similarity index 100% rename from src/html/component/functions-editor/editor-tile/editor-tile.ts rename to src/html/component-editor/functions-editor/editor-tile/editor-tile.ts diff --git a/src/html/component/functions-editor/editor-tile/function-tile.ts b/src/html/component-editor/functions-editor/editor-tile/function-tile.ts similarity index 100% rename from src/html/component/functions-editor/editor-tile/function-tile.ts rename to src/html/component-editor/functions-editor/editor-tile/function-tile.ts diff --git a/src/html/component/functions-editor/editor-tile/variable-tile.ts b/src/html/component-editor/functions-editor/editor-tile/variable-tile.ts similarity index 100% rename from src/html/component/functions-editor/editor-tile/variable-tile.ts rename to src/html/component-editor/functions-editor/editor-tile/variable-tile.ts diff --git a/src/html/component/functions-editor/functions-editor.less b/src/html/component-editor/functions-editor/functions-editor.less similarity index 100% rename from src/html/component/functions-editor/functions-editor.less rename to src/html/component-editor/functions-editor/functions-editor.less diff --git a/src/html/component/functions-editor/functions-editor.ts b/src/html/component-editor/functions-editor/functions-editor.ts similarity index 100% rename from src/html/component/functions-editor/functions-editor.ts rename to src/html/component-editor/functions-editor/functions-editor.ts diff --git a/src/html/component/menu/menu.less b/src/html/component-editor/menu/menu.less similarity index 100% rename from src/html/component/menu/menu.less rename to src/html/component-editor/menu/menu.less diff --git a/src/html/component/menu/menu.ts b/src/html/component-editor/menu/menu.ts similarity index 100% rename from src/html/component/menu/menu.ts rename to src/html/component-editor/menu/menu.ts diff --git a/src/html/component/nav-bar/nav-bar.less b/src/html/component-editor/nav-bar/nav-bar.less similarity index 100% rename from src/html/component/nav-bar/nav-bar.less rename to src/html/component-editor/nav-bar/nav-bar.less diff --git a/src/html/component/nav-bar/nav-bar.ts b/src/html/component-editor/nav-bar/nav-bar.ts similarity index 100% rename from src/html/component/nav-bar/nav-bar.ts rename to src/html/component-editor/nav-bar/nav-bar.ts diff --git a/src/html/component/observations-editor/edit-observation/edit-observation.html b/src/html/component-editor/observations-editor/edit-observation/edit-observation.html similarity index 100% rename from src/html/component/observations-editor/edit-observation/edit-observation.html rename to src/html/component-editor/observations-editor/edit-observation/edit-observation.html diff --git a/src/html/component/observations-editor/edit-observation/edit-observation.less b/src/html/component-editor/observations-editor/edit-observation/edit-observation.less similarity index 100% rename from src/html/component/observations-editor/edit-observation/edit-observation.less rename to src/html/component-editor/observations-editor/edit-observation/edit-observation.less diff --git a/src/html/component/observations-editor/edit-observation/edit-observation.ts b/src/html/component-editor/observations-editor/edit-observation/edit-observation.ts similarity index 100% rename from src/html/component/observations-editor/edit-observation/edit-observation.ts rename to src/html/component-editor/observations-editor/edit-observation/edit-observation.ts diff --git a/src/html/component/observations-editor/observations-editor.less b/src/html/component-editor/observations-editor/observations-editor.less similarity index 100% rename from src/html/component/observations-editor/observations-editor.less rename to src/html/component-editor/observations-editor/observations-editor.less diff --git a/src/html/component/observations-editor/observations-editor.ts b/src/html/component-editor/observations-editor/observations-editor.ts similarity index 99% rename from src/html/component/observations-editor/observations-editor.ts rename to src/html/component-editor/observations-editor/observations-editor.ts index 761d867..4e0ff5b 100644 --- a/src/html/component/observations-editor/observations-editor.ts +++ b/src/html/component-editor/observations-editor/observations-editor.ts @@ -141,7 +141,7 @@ export default class ObservationsEditor extends LitElement { const pos = await appWindow.outerPosition() const size = await appWindow.outerSize() const importDialog = new WebviewWindow(`editObservation${Math.floor(Math.random() * 1000000)}`, { - url: 'src/html/component/observations-editor/observations-import/observations-import.html', + url: 'src/html/component-editor/observations-editor/observations-import/observations-import.html', title: 'Import observation set', alwaysOnTop: false, maximizable: false, diff --git a/src/html/component/observations-editor/observations-import/observations-import.html b/src/html/component-editor/observations-editor/observations-import/observations-import.html similarity index 100% rename from src/html/component/observations-editor/observations-import/observations-import.html rename to src/html/component-editor/observations-editor/observations-import/observations-import.html diff --git a/src/html/component/observations-editor/observations-import/observations-import.less b/src/html/component-editor/observations-editor/observations-import/observations-import.less similarity index 100% rename from src/html/component/observations-editor/observations-import/observations-import.less rename to src/html/component-editor/observations-editor/observations-import/observations-import.less diff --git a/src/html/component/observations-editor/observations-import/observations-import.ts b/src/html/component-editor/observations-editor/observations-import/observations-import.ts similarity index 100% rename from src/html/component/observations-editor/observations-import/observations-import.ts rename to src/html/component-editor/observations-editor/observations-import/observations-import.ts diff --git a/src/html/component/observations-editor/observations-set/observations-set.less b/src/html/component-editor/observations-editor/observations-set/observations-set.less similarity index 100% rename from src/html/component/observations-editor/observations-set/observations-set.less rename to src/html/component-editor/observations-editor/observations-set/observations-set.less diff --git a/src/html/component/observations-editor/observations-set/observations-set.ts b/src/html/component-editor/observations-editor/observations-set/observations-set.ts similarity index 98% rename from src/html/component/observations-editor/observations-set/observations-set.ts rename to src/html/component-editor/observations-editor/observations-set/observations-set.ts index 8163de9..9466bb5 100644 --- a/src/html/component/observations-editor/observations-set/observations-set.ts +++ b/src/html/component-editor/observations-editor/observations-set/observations-set.ts @@ -150,7 +150,7 @@ export default class ObservationsSet extends LitElement { return } const renameDialog = new WebviewWindow(`editObservation${Math.floor(Math.random() * 1000000)}`, { - url: 'src/html/component/observations-editor/edit-observation/edit-observation.html', + url: 'src/html/component-editor/observations-editor/edit-observation/edit-observation.html', title: `Edit observation (${obs.id} / ${obs.name})`, alwaysOnTop: true, maximizable: false, diff --git a/src/html/component/observations-editor/tabulator-style.less b/src/html/component-editor/observations-editor/tabulator-style.less similarity index 100% rename from src/html/component/observations-editor/tabulator-style.less rename to src/html/component-editor/observations-editor/tabulator-style.less diff --git a/src/html/component/observations-editor/tabulator-utility.ts b/src/html/component-editor/observations-editor/tabulator-utility.ts similarity index 100% rename from src/html/component/observations-editor/tabulator-utility.ts rename to src/html/component-editor/observations-editor/tabulator-utility.ts diff --git a/src/html/component/properties-editor/abstract-property/abstract-property.less b/src/html/component-editor/properties-editor/abstract-property/abstract-property.less similarity index 100% rename from src/html/component/properties-editor/abstract-property/abstract-property.less rename to src/html/component-editor/properties-editor/abstract-property/abstract-property.less diff --git a/src/html/component/properties-editor/abstract-property/abstract-property.ts b/src/html/component-editor/properties-editor/abstract-property/abstract-property.ts similarity index 100% rename from src/html/component/properties-editor/abstract-property/abstract-property.ts rename to src/html/component-editor/properties-editor/abstract-property/abstract-property.ts diff --git a/src/html/component/properties-editor/default-properties.ts b/src/html/component-editor/properties-editor/default-properties.ts similarity index 100% rename from src/html/component/properties-editor/default-properties.ts rename to src/html/component-editor/properties-editor/default-properties.ts diff --git a/src/html/component/properties-editor/dynamic/abstract-dynamic-property.ts b/src/html/component-editor/properties-editor/dynamic/abstract-dynamic-property.ts similarity index 100% rename from src/html/component/properties-editor/dynamic/abstract-dynamic-property.ts rename to src/html/component-editor/properties-editor/dynamic/abstract-dynamic-property.ts diff --git a/src/html/component/properties-editor/dynamic/dynamic-attractor-count/dynamic-attractor-count.less b/src/html/component-editor/properties-editor/dynamic/dynamic-attractor-count/dynamic-attractor-count.less similarity index 100% rename from src/html/component/properties-editor/dynamic/dynamic-attractor-count/dynamic-attractor-count.less rename to src/html/component-editor/properties-editor/dynamic/dynamic-attractor-count/dynamic-attractor-count.less diff --git a/src/html/component/properties-editor/dynamic/dynamic-attractor-count/dynamic-attractor-count.ts b/src/html/component-editor/properties-editor/dynamic/dynamic-attractor-count/dynamic-attractor-count.ts similarity index 100% rename from src/html/component/properties-editor/dynamic/dynamic-attractor-count/dynamic-attractor-count.ts rename to src/html/component-editor/properties-editor/dynamic/dynamic-attractor-count/dynamic-attractor-count.ts diff --git a/src/html/component/properties-editor/dynamic/dynamic-generic/dynamic-generic.less b/src/html/component-editor/properties-editor/dynamic/dynamic-generic/dynamic-generic.less similarity index 100% rename from src/html/component/properties-editor/dynamic/dynamic-generic/dynamic-generic.less rename to src/html/component-editor/properties-editor/dynamic/dynamic-generic/dynamic-generic.less diff --git a/src/html/component/properties-editor/dynamic/dynamic-generic/dynamic-generic.ts b/src/html/component-editor/properties-editor/dynamic/dynamic-generic/dynamic-generic.ts similarity index 100% rename from src/html/component/properties-editor/dynamic/dynamic-generic/dynamic-generic.ts rename to src/html/component-editor/properties-editor/dynamic/dynamic-generic/dynamic-generic.ts diff --git a/src/html/component/properties-editor/dynamic/dynamic-obs-selection/dynamic-obs-selection.less b/src/html/component-editor/properties-editor/dynamic/dynamic-obs-selection/dynamic-obs-selection.less similarity index 100% rename from src/html/component/properties-editor/dynamic/dynamic-obs-selection/dynamic-obs-selection.less rename to src/html/component-editor/properties-editor/dynamic/dynamic-obs-selection/dynamic-obs-selection.less diff --git a/src/html/component/properties-editor/dynamic/dynamic-obs-selection/dynamic-obs-selection.ts b/src/html/component-editor/properties-editor/dynamic/dynamic-obs-selection/dynamic-obs-selection.ts similarity index 100% rename from src/html/component/properties-editor/dynamic/dynamic-obs-selection/dynamic-obs-selection.ts rename to src/html/component-editor/properties-editor/dynamic/dynamic-obs-selection/dynamic-obs-selection.ts diff --git a/src/html/component/properties-editor/properties-editor.less b/src/html/component-editor/properties-editor/properties-editor.less similarity index 100% rename from src/html/component/properties-editor/properties-editor.less rename to src/html/component-editor/properties-editor/properties-editor.less diff --git a/src/html/component/properties-editor/properties-editor.ts b/src/html/component-editor/properties-editor/properties-editor.ts similarity index 100% rename from src/html/component/properties-editor/properties-editor.ts rename to src/html/component-editor/properties-editor/properties-editor.ts diff --git a/src/html/component/properties-editor/static/abstract-static-property.ts b/src/html/component-editor/properties-editor/static/abstract-static-property.ts similarity index 100% rename from src/html/component/properties-editor/static/abstract-static-property.ts rename to src/html/component-editor/properties-editor/static/abstract-static-property.ts diff --git a/src/html/component/properties-editor/static/static-generic/static-generic.less b/src/html/component-editor/properties-editor/static/static-generic/static-generic.less similarity index 100% rename from src/html/component/properties-editor/static/static-generic/static-generic.less rename to src/html/component-editor/properties-editor/static/static-generic/static-generic.less diff --git a/src/html/component/properties-editor/static/static-generic/static-generic.ts b/src/html/component-editor/properties-editor/static/static-generic/static-generic.ts similarity index 100% rename from src/html/component/properties-editor/static/static-generic/static-generic.ts rename to src/html/component-editor/properties-editor/static/static-generic/static-generic.ts diff --git a/src/html/component/properties-editor/static/static-input-essential-condition/static-input-essential-condition.less b/src/html/component-editor/properties-editor/static/static-input-essential-condition/static-input-essential-condition.less similarity index 100% rename from src/html/component/properties-editor/static/static-input-essential-condition/static-input-essential-condition.less rename to src/html/component-editor/properties-editor/static/static-input-essential-condition/static-input-essential-condition.less diff --git a/src/html/component/properties-editor/static/static-input-essential-condition/static-input-essential-condition.ts b/src/html/component-editor/properties-editor/static/static-input-essential-condition/static-input-essential-condition.ts similarity index 100% rename from src/html/component/properties-editor/static/static-input-essential-condition/static-input-essential-condition.ts rename to src/html/component-editor/properties-editor/static/static-input-essential-condition/static-input-essential-condition.ts diff --git a/src/html/component/properties-editor/static/static-input-essential/static-input-essential.less b/src/html/component-editor/properties-editor/static/static-input-essential/static-input-essential.less similarity index 100% rename from src/html/component/properties-editor/static/static-input-essential/static-input-essential.less rename to src/html/component-editor/properties-editor/static/static-input-essential/static-input-essential.less diff --git a/src/html/component/properties-editor/static/static-input-essential/static-input-essential.ts b/src/html/component-editor/properties-editor/static/static-input-essential/static-input-essential.ts similarity index 100% rename from src/html/component/properties-editor/static/static-input-essential/static-input-essential.ts rename to src/html/component-editor/properties-editor/static/static-input-essential/static-input-essential.ts diff --git a/src/html/component/properties-editor/static/static-input-monotonic-condition/static-input-monotonic-condition.less b/src/html/component-editor/properties-editor/static/static-input-monotonic-condition/static-input-monotonic-condition.less similarity index 100% rename from src/html/component/properties-editor/static/static-input-monotonic-condition/static-input-monotonic-condition.less rename to src/html/component-editor/properties-editor/static/static-input-monotonic-condition/static-input-monotonic-condition.less diff --git a/src/html/component/properties-editor/static/static-input-monotonic-condition/static-input-monotonic-condition.ts b/src/html/component-editor/properties-editor/static/static-input-monotonic-condition/static-input-monotonic-condition.ts similarity index 100% rename from src/html/component/properties-editor/static/static-input-monotonic-condition/static-input-monotonic-condition.ts rename to src/html/component-editor/properties-editor/static/static-input-monotonic-condition/static-input-monotonic-condition.ts diff --git a/src/html/component/properties-editor/static/static-input-monotonic/static-input-monotonic.less b/src/html/component-editor/properties-editor/static/static-input-monotonic/static-input-monotonic.less similarity index 100% rename from src/html/component/properties-editor/static/static-input-monotonic/static-input-monotonic.less rename to src/html/component-editor/properties-editor/static/static-input-monotonic/static-input-monotonic.less diff --git a/src/html/component/properties-editor/static/static-input-monotonic/static-input-monotonic.ts b/src/html/component-editor/properties-editor/static/static-input-monotonic/static-input-monotonic.ts similarity index 100% rename from src/html/component/properties-editor/static/static-input-monotonic/static-input-monotonic.ts rename to src/html/component-editor/properties-editor/static/static-input-monotonic/static-input-monotonic.ts diff --git a/src/html/component/properties-editor/static/static-selectors-property.ts b/src/html/component-editor/properties-editor/static/static-selectors-property.ts similarity index 100% rename from src/html/component/properties-editor/static/static-selectors-property.ts rename to src/html/component-editor/properties-editor/static/static-selectors-property.ts diff --git a/src/html/component/regulations-editor/float-menu/float-menu.less b/src/html/component-editor/regulations-editor/float-menu/float-menu.less similarity index 100% rename from src/html/component/regulations-editor/float-menu/float-menu.less rename to src/html/component-editor/regulations-editor/float-menu/float-menu.less diff --git a/src/html/component/regulations-editor/float-menu/float-menu.ts b/src/html/component-editor/regulations-editor/float-menu/float-menu.ts similarity index 100% rename from src/html/component/regulations-editor/float-menu/float-menu.ts rename to src/html/component-editor/regulations-editor/float-menu/float-menu.ts diff --git a/src/html/component/regulations-editor/regulations-editor.config.ts b/src/html/component-editor/regulations-editor/regulations-editor.config.ts similarity index 100% rename from src/html/component/regulations-editor/regulations-editor.config.ts rename to src/html/component-editor/regulations-editor/regulations-editor.config.ts diff --git a/src/html/component/regulations-editor/regulations-editor.less b/src/html/component-editor/regulations-editor/regulations-editor.less similarity index 100% rename from src/html/component/regulations-editor/regulations-editor.less rename to src/html/component-editor/regulations-editor/regulations-editor.less diff --git a/src/html/component/regulations-editor/regulations-editor.ts b/src/html/component-editor/regulations-editor/regulations-editor.ts similarity index 99% rename from src/html/component/regulations-editor/regulations-editor.ts rename to src/html/component-editor/regulations-editor/regulations-editor.ts index 5b06f40..16fea74 100644 --- a/src/html/component/regulations-editor/regulations-editor.ts +++ b/src/html/component-editor/regulations-editor/regulations-editor.ts @@ -243,7 +243,7 @@ export class RegulationsEditor extends LitElement { return } const renameDialog = new WebviewWindow(`renameDialog${Math.floor(Math.random() * 1000000)}`, { - url: 'src/html/component/regulations-editor/rename-dialog/rename-dialog.html', + url: 'src/html/component-editor/regulations-editor/rename-dialog/rename-dialog.html', title: `Edit node (${variableId} / ${variableName})`, alwaysOnTop: true, maximizable: false, diff --git a/src/html/component/regulations-editor/rename-dialog/rename-dialog.html b/src/html/component-editor/regulations-editor/rename-dialog/rename-dialog.html similarity index 100% rename from src/html/component/regulations-editor/rename-dialog/rename-dialog.html rename to src/html/component-editor/regulations-editor/rename-dialog/rename-dialog.html diff --git a/src/html/component/regulations-editor/rename-dialog/rename-dialog.less b/src/html/component-editor/regulations-editor/rename-dialog/rename-dialog.less similarity index 100% rename from src/html/component/regulations-editor/rename-dialog/rename-dialog.less rename to src/html/component-editor/regulations-editor/rename-dialog/rename-dialog.less diff --git a/src/html/component/regulations-editor/rename-dialog/rename-dialog.ts b/src/html/component-editor/regulations-editor/rename-dialog/rename-dialog.ts similarity index 100% rename from src/html/component/regulations-editor/rename-dialog/rename-dialog.ts rename to src/html/component-editor/regulations-editor/rename-dialog/rename-dialog.ts diff --git a/src/html/component-editor/root-component/root-component.less b/src/html/component-editor/root-component/root-component.less new file mode 100644 index 0000000..47e7bd3 --- /dev/null +++ b/src/html/component-editor/root-component/root-component.less @@ -0,0 +1,42 @@ +@import '/src/uikit-theme'; + +/* The height of the header based on the known theme settings. */ +@header-height: @button-line-height + (2 * @button-border-width); + +.root-component { + height: 100%; + display: contents; + overflow: hidden; +} + +.header { + height: @header-height; +} + +.content { + /* + Will cause the main content to wrap correctly into + rows if available width is exceeded. + */ + display: flex; + flex-direction: row; + + /* + The absolute positioning and 100% height are needed for the + Cytoscape editor to function properly. + */ + position: absolute; + top: @header-height + (2 * @margin-small-margin); + left: 0; + right: 0; + bottom: 0; +} + +@media only screen and (max-width: 800px) { + .inactive { + display: none; + } + .active { + width: 100vw; + } +} diff --git a/src/html/component/root-component/root-component.ts b/src/html/component-editor/root-component/root-component.ts similarity index 100% rename from src/html/component/root-component/root-component.ts rename to src/html/component-editor/root-component/root-component.ts diff --git a/src/html/component/search/search.less b/src/html/component-editor/search/search.less similarity index 100% rename from src/html/component/search/search.less rename to src/html/component-editor/search/search.less diff --git a/src/html/component/search/search.ts b/src/html/component-editor/search/search.ts similarity index 100% rename from src/html/component/search/search.ts rename to src/html/component-editor/search/search.ts diff --git a/src/html/component/tab-bar/tab-bar.less b/src/html/component-editor/tab-bar/tab-bar.less similarity index 100% rename from src/html/component/tab-bar/tab-bar.less rename to src/html/component-editor/tab-bar/tab-bar.less diff --git a/src/html/component/tab-bar/tab-bar.ts b/src/html/component-editor/tab-bar/tab-bar.ts similarity index 100% rename from src/html/component/tab-bar/tab-bar.ts rename to src/html/component-editor/tab-bar/tab-bar.ts diff --git a/src/html/component-editor/tauri_welcome.html b/src/html/component-editor/tauri_welcome.html new file mode 100644 index 0000000..e92d647 --- /dev/null +++ b/src/html/component-editor/tauri_welcome.html @@ -0,0 +1,29 @@ + +
+ + + + + + + + + +
+ +

Click on the Tauri logo to learn more about the framework

+ +
+ + +
+ +

\ No newline at end of file diff --git a/src/html/component/undo-redo/undo-redo.less b/src/html/component-editor/undo-redo/undo-redo.less similarity index 100% rename from src/html/component/undo-redo/undo-redo.less rename to src/html/component-editor/undo-redo/undo-redo.less diff --git a/src/html/component/undo-redo/undo-redo.ts b/src/html/component-editor/undo-redo/undo-redo.ts similarity index 100% rename from src/html/component/undo-redo/undo-redo.ts rename to src/html/component-editor/undo-redo/undo-redo.ts diff --git a/src/html/signpost.html b/src/html/signpost.html index 595bfb7..63ea411 100644 --- a/src/html/signpost.html +++ b/src/html/signpost.html @@ -3,7 +3,7 @@
- + @@ -25,7 +25,7 @@ - +
diff --git a/src/html/sketch-editor.html b/src/html/sketch-editor.html index 1330cca..df33c95 100644 --- a/src/html/sketch-editor.html +++ b/src/html/sketch-editor.html @@ -1,6 +1,6 @@ - + \ No newline at end of file diff --git a/src/html/state-space-explorer.html b/src/html/state-space-explorer.html index 2db6718..ec8e4aa 100644 --- a/src/html/state-space-explorer.html +++ b/src/html/state-space-explorer.html @@ -3,7 +3,7 @@

Welcome to Tauri!

- +
  • diff --git a/src/html/util/config.ts b/src/html/util/config.ts index a4efb6f..e434202 100644 --- a/src/html/util/config.ts +++ b/src/html/util/config.ts @@ -28,13 +28,13 @@ export const tabList: TabData[] = [ name: 'Properties', content: (contentData) => html``, icon: 'p' + }), + TabData.create({ + id: index++, + name: 'Analysis', + content: (contentData) => html``, + icon: 'a' }) - // TabData.create({ - // id: index++, - // name: 'Analysis', - // content: () => html`

    Content of analysis tab

    `, - // icon: 'a' - // }) ] export const functionDebounceTimer = 1000 From 2dfb72125dbbbf05f08e7892c4c10a397e3d2c2d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ond=C5=99ej=20Huvar?= <492849@mail.muni.cz> Date: Thu, 25 Jul 2024 21:09:25 +0200 Subject: [PATCH 2/8] Add communication between sessions, add sketch transfer from editor to analysis. --- src-tauri/src/analysis/mod.rs | 32 ++++- src-tauri/src/app/event.rs | 11 ++ src-tauri/src/app/event_wrappers.rs | 24 ++++ src-tauri/src/app/mod.rs | 11 ++ src-tauri/src/app/state/_state_app.rs | 94 ++++++++++++-- .../state/analysis/_state_analysis_session.rs | 58 ++++++++- .../app/state/editor/_state_editor_session.rs | 43 ++++++- src-tauri/src/app/state/mod.rs | 13 +- src-tauri/src/main.rs | 119 +++++++++++------- src-tauri/src/sketchbook/_sketch/mod.rs | 6 +- .../sketchbook/data_structs/_sketch_data.rs | 7 +- src/aeon_events.ts | 25 ++-- .../analysis-component/analysis-component.ts | 27 +++- 13 files changed, 382 insertions(+), 88 deletions(-) create mode 100644 src-tauri/src/app/event_wrappers.rs diff --git a/src-tauri/src/analysis/mod.rs b/src-tauri/src/analysis/mod.rs index 360292e..f935d41 100644 --- a/src-tauri/src/analysis/mod.rs +++ b/src-tauri/src/analysis/mod.rs @@ -8,14 +8,42 @@ use serde::{Deserialize, Serialize}; /// Object encompassing all of the state components of the Analysis. #[derive(Clone, Debug, PartialEq, Serialize, Deserialize)] pub struct AnalysisState { - /// Boolean network sketch to run the analysis on. + /// Boolean network sketch to run the analysis on. Can be a placeholder at the beginning. sketch: Sketch, + /// Flag signalling that the actual sketch data were received. + sketch_received: bool, // TODO } impl AnalysisState { + /// Create new `AnalysisState` with an empty placeholder sketch. + /// + /// This is used to create a placeholder instance before the actual sketch data are sent from + /// the editor session. + pub fn new_empty() -> AnalysisState { + AnalysisState { + sketch: Sketch::default(), + sketch_received: false, + } + } + + /// Create new `AnalysisState` with a full sketch data. pub fn new(sketch: Sketch) -> AnalysisState { - AnalysisState { sketch } + AnalysisState { + sketch, + sketch_received: true, + } + } + + /// Update the sketch data of this `AnalysisState`. + pub fn set_sketch(&mut self, sketch: Sketch) { + self.sketch = sketch; + self.sketch_received = true; + } + + /// Get reference to the sketch data of this `AnalysisState`. + pub fn get_sketch(&self) -> &Sketch { + &self.sketch } } diff --git a/src-tauri/src/app/event.rs b/src-tauri/src/app/event.rs index 51a45a3..dfc2fe3 100644 --- a/src-tauri/src/app/event.rs +++ b/src-tauri/src/app/event.rs @@ -32,6 +32,17 @@ pub struct StateChange { pub events: Vec, } +/// A [SessionMessage] represents a single event "message" that is exchanged between +/// different sessions (purely on backend). +/// +/// Typically, a [SessionMessage] is emitted as either "request" when one session needs a value +/// from another, or as a "answer", providing the requested value. Of course, the values might +/// also be sent automatically without requests. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct SessionMessage { + pub message: Event, +} + impl Event { pub fn build(path: &[&str], payload: Option<&str>) -> Event { Event { diff --git a/src-tauri/src/app/event_wrappers.rs b/src-tauri/src/app/event_wrappers.rs new file mode 100644 index 0000000..ecbbaad --- /dev/null +++ b/src-tauri/src/app/event_wrappers.rs @@ -0,0 +1,24 @@ +use crate::app::event::Event; +use serde::{Deserialize, Serialize}; + +/// Struct to wrap [UserAction] events sent from front-end to a particular session. +#[derive(Serialize, Deserialize)] +pub struct AeonAction { + pub session: String, + pub events: Vec, +} + +/// Struct to wrap [Refresh] requests sent from front-end to a particular session. +#[derive(Serialize, Deserialize)] +pub struct AeonRefresh { + pub session: String, + pub path: Vec, +} + +/// Struct to wrap [SessionMessage] events sent between particular sessions on back-end. +#[derive(Serialize, Deserialize)] +pub struct AeonMessage { + pub session_from: String, + pub session_to: String, + pub message: Event, +} diff --git a/src-tauri/src/app/mod.rs b/src-tauri/src/app/mod.rs index 90a8e37..1e01242 100644 --- a/src-tauri/src/app/mod.rs +++ b/src-tauri/src/app/mod.rs @@ -3,6 +3,7 @@ use std::error::Error; mod _aeon_app; mod _aeon_error; pub mod event; +pub mod event_wrappers; pub mod state; pub use _aeon_app::AeonApp; @@ -17,6 +18,16 @@ pub const AEON_VALUE: &str = "aeon-value"; /// Label for frontend events that are requesting a value retransmission. pub const AEON_REFRESH: &str = "aeon-refresh"; +/// Label for backend-only events for simple "request-answer" messaging between different sessions +/// to exchange predefined values. +pub const AEON_MESSAGE: &str = "aeon-message"; + +/// ID of the default initial editor session. +pub const DEFAULT_SESSION_ID: &str = "editor-1"; + +/// ID of the initial window of the default editor session. +pub const DEFAULT_WINDOW_ID: &str = "editor"; + /// A [DynError] is a "generic" heap-allocated trait object which implements [std::error::Error]. /// /// You can convert most standard "typed" errors into [DynError]. If you want to diff --git a/src-tauri/src/app/state/_state_app.rs b/src-tauri/src/app/state/_state_app.rs index 19f8a0e..4b9d0f5 100644 --- a/src-tauri/src/app/state/_state_app.rs +++ b/src-tauri/src/app/state/_state_app.rs @@ -1,6 +1,8 @@ -use crate::app::event::UserAction; +use crate::app::event::{SessionMessage, StateChange, UserAction}; +use crate::app::event_wrappers::AeonMessage; use crate::app::state::DynSession; -use crate::app::{AeonApp, AeonError, DynError, AEON_VALUE}; +use crate::app::{AeonApp, AeonError, DynError, AEON_MESSAGE, AEON_VALUE}; +use crate::{debug, warning}; use std::collections::HashMap; use std::ops::{Deref, DerefMut}; use std::sync::Mutex; @@ -31,6 +33,7 @@ impl Default for AppState { } impl AppState { + /// Register the newly created session to the AppState. pub fn session_created(&self, id: &str, session: impl Into) { let mut guard = self.session_state.lock().unwrap_or_else(|_e| { panic!("Main application state is poisoned. Cannot recover."); @@ -43,6 +46,7 @@ impl AppState { session_map.insert(id.to_string(), session.into()); } + /// Register the newly created window to the corresponding session in the AppState. pub fn window_created(&self, id: &str, session_id: &str) { let mut guard = self.window_to_session.lock().unwrap_or_else(|_e| { panic!("Main application state is poisoned. Cannot recover."); @@ -55,6 +59,7 @@ impl AppState { map.insert(id.to_string(), session_id.to_string()); } + /// Get the ID of the session that owns given Window. pub fn get_session_id(&self, window: &Window) -> String { let guard = self.window_to_session.lock().unwrap_or_else(|_e| { panic!("Main application state is poisoned. Cannot recover."); @@ -65,6 +70,44 @@ impl AppState { }) } + /// Get IDs of all windows corresponding to a given session. + pub fn get_windows_for_session(&self, session_id: &str) -> Vec { + let guard = self.window_to_session.lock().unwrap_or_else(|_e| { + panic!("Main application state is poisoned. Cannot recover."); + }); + let map = guard.deref(); + + map.iter() + .filter_map(|(window, session)| { + if session == session_id { + Some(window.clone()) + } else { + None + } + }) + .collect() + } + + /// Emit state change events to all front-end windows corresponding to a given session. + pub fn emit_to_session_windows( + &self, + app: &AeonApp, + session_id: &str, + state_change: StateChange, + ) -> Result<(), DynError> { + let window_ids = self.get_windows_for_session(session_id); + debug!("{:?}", window_ids); + if window_ids.is_empty() { + warning!("No windows correspond to provided session `{session_id}`.") + } + if let Err(e) = app.tauri.emit_filter(AEON_VALUE, state_change.events, |w| { + window_ids.contains(&w.label().to_string()) + }) { + return AeonError::throw_with_source("Error sending state-change event.", e); + } + Ok(()) + } + pub fn consume_event( &self, app: &AeonApp, @@ -79,10 +122,40 @@ impl AppState { panic!("Unknown session id {}.", session_id); }); let state_change = session.perform_action(action)?; - if let Err(e) = app.tauri.emit_all(AEON_VALUE, state_change.events) { - return AeonError::throw_with_source("Error sending state event.", e); - } + self.emit_to_session_windows(app, session_id, state_change) + } + + pub fn consume_message( + &self, + app: &AeonApp, + session_to_id: &str, + session_from_id: &str, + message: &SessionMessage, + ) -> Result<(), DynError> { + let mut guard = self + .session_state + .lock() + .unwrap_or_else(|_e| panic!("Main application state is poisoned. Cannot recover.")); + let session = guard.deref_mut().get_mut(session_to_id).unwrap_or_else(|| { + panic!("Unknown session id {}.", session_to_id); + }); + let (opt_response, opt_state_change) = session.process_message(message)?; + // if message requires a response, trigger it + if let Some(response_message) = opt_response { + // swap from/to IDs + let wrapped_message = AeonMessage { + session_from: session_to_id.to_string(), + session_to: session_from_id.to_string(), + message: response_message.message, + }; + let msg_serialized = serde_json::to_string(&wrapped_message)?; + app.tauri.trigger_global(AEON_MESSAGE, Some(msg_serialized)); + } + // if message requires a state change to be sent to frontend, emit it + if let Some(state_change) = opt_state_change { + return self.emit_to_session_windows(app, session_to_id, state_change); + } Ok(()) } @@ -100,11 +173,10 @@ impl AppState { panic!("Unknown session id {}.", session_id); }); let at_path = full_path.iter().map(|it| it.as_str()).collect::>(); - let state_change = session.refresh(full_path, &at_path)?; - if let Err(e) = app.tauri.emit_all(AEON_VALUE, vec![state_change]) { - return AeonError::throw_with_source("Error sending state event.", e); - } - - Ok(()) + let event = session.refresh(full_path, &at_path)?; + let state_change = StateChange { + events: vec![event], + }; + self.emit_to_session_windows(app, session_id, state_change) } } diff --git a/src-tauri/src/app/state/analysis/_state_analysis_session.rs b/src-tauri/src/app/state/analysis/_state_analysis_session.rs index d933354..027652c 100644 --- a/src-tauri/src/app/state/analysis/_state_analysis_session.rs +++ b/src-tauri/src/app/state/analysis/_state_analysis_session.rs @@ -1,10 +1,11 @@ use crate::analysis::AnalysisState; -use crate::app::event::{Event, StateChange, UserAction}; +use crate::app::event::{Event, SessionMessage, StateChange, UserAction}; use crate::app::state::_undo_stack::UndoStack; use crate::app::state::{Consumed, Session, SessionHelper, SessionState}; use crate::app::{AeonError, DynError}; use crate::debug; -use crate::sketchbook::Sketch; +use crate::sketchbook::data_structs::SketchData; +use crate::sketchbook::{JsonSerde, Sketch}; /// The state of one editor session. /// @@ -16,11 +17,11 @@ pub struct AnalysisSession { } impl AnalysisSession { - pub fn new(id: &str, sketch: Sketch) -> AnalysisSession { + pub fn new(id: &str) -> AnalysisSession { AnalysisSession { id: id.to_string(), undo_stack: UndoStack::default(), - analysis_state: AnalysisState::new(sketch), + analysis_state: AnalysisState::new_empty(), } } @@ -122,7 +123,10 @@ impl AnalysisSession { self.append_stack_updates(&mut state_changes); } } else if !ignore_stack && reset_stack { - debug!("Back stack cleared due to irreversible action."); + debug!( + "Back stack (of session {}) cleared due to irreversible action.", + self.id + ); self.undo_stack.clear(); } @@ -180,6 +184,50 @@ impl Session for AnalysisSession { self.perform_action(action, false) } + fn process_message( + &mut self, + message: &SessionMessage, + ) -> Result<(Option, Option), DynError> { + let path = message.message.path.clone(); + + // if the state changed due to message processing, we'll have to reset the undo-redo stack + // do not use messages that make these changes often + let mut reset_stack = false; + + // message with sketch data sent from Editor session + let result = if path == vec!["sketch_sent".to_string()] { + if let Some(sketch_payload) = message.message.payload.clone() { + let sketch = Sketch::from_json_str(&sketch_payload)?; + reset_stack = true; + self.analysis_state.set_sketch(sketch); + } else { + panic!("Message `sketch_sent` must always carry a payload.") + } + // no response is expected, but we must inform frontend about state change + let sketch_data = SketchData::new_from_sketch(self.analysis_state.get_sketch()); + let payload = sketch_data.to_json_str(); + let state_change = StateChange { + events: vec![Event::build( + &["analysis", "sketch_changed"], + Some(&payload), + )], + }; + Ok((None, Some(state_change))) + } else { + let error_msg = format!("`AnalysisSession` cannot process path {:?}.", path); + AeonError::throw(error_msg) + }; + + if reset_stack { + debug!( + "Back stack (of session {}) cleared due to backend change.", + self.id + ); + self.undo_stack.clear(); + } + result + } + fn id(&self) -> &str { self.id.as_str() } diff --git a/src-tauri/src/app/state/editor/_state_editor_session.rs b/src-tauri/src/app/state/editor/_state_editor_session.rs index 1fa39cf..5cd6f84 100644 --- a/src-tauri/src/app/state/editor/_state_editor_session.rs +++ b/src-tauri/src/app/state/editor/_state_editor_session.rs @@ -1,10 +1,10 @@ -use crate::app::event::{Event, StateChange, UserAction}; +use crate::app::event::{Event, SessionMessage, StateChange, UserAction}; use crate::app::state::_undo_stack::UndoStack; use crate::app::state::editor::TabBarState; use crate::app::state::{Consumed, Session, SessionHelper, SessionState}; use crate::app::{AeonError, DynError}; use crate::debug; -use crate::sketchbook::Sketch; +use crate::sketchbook::{JsonSerde, Sketch}; /// The state of one editor session. /// @@ -125,7 +125,10 @@ impl EditorSession { self.append_stack_updates(&mut state_changes); } } else if !ignore_stack && reset_stack { - debug!("Back stack cleared due to irreversible action."); + debug!( + "Back stack (of session {}) cleared due to irreversible action.", + self.id + ); self.undo_stack.clear(); } @@ -183,6 +186,40 @@ impl Session for EditorSession { self.perform_action(action, false) } + fn process_message( + &mut self, + message: &SessionMessage, + ) -> Result<(Option, Option), DynError> { + let path = message.message.path.clone(); + + // if the state changed due to message processing, we'll have to reset the undo-redo stack + // do not use messages that make these changes often + // todo: make this `mut` when we have some cases here that could mutate state + let reset_stack = false; + + // request from new Analysis session for sending a sketch + let result = if path == vec!["send_sketch".to_string()] { + let sketch_string = self.sketch.to_json_str(); + let response_msg = SessionMessage { + message: Event::build(&["sketch_sent"], Some(&sketch_string)), + }; + // response message; but no change in state for frontend + Ok((Some(response_msg), None)) + } else { + let error_msg = format!("`EditorSession` cannot process path {:?}.", path); + AeonError::throw(error_msg) + }; + + if reset_stack { + debug!( + "Back stack (of session {}) cleared due to backend change.", + self.id + ); + self.undo_stack.clear(); + } + result + } + fn id(&self) -> &str { self.id.as_str() } diff --git a/src-tauri/src/app/state/mod.rs b/src-tauri/src/app/state/mod.rs index 4ec1556..55030cd 100644 --- a/src-tauri/src/app/state/mod.rs +++ b/src-tauri/src/app/state/mod.rs @@ -1,4 +1,4 @@ -use crate::app::event::{Event, StateChange, UserAction}; +use crate::app::event::{Event, SessionMessage, StateChange, UserAction}; use crate::app::{AeonError, DynError}; mod _consumed; @@ -114,6 +114,17 @@ pub trait Session: SessionState { /// single [StateChange] entry. fn perform_action(&mut self, action: &UserAction) -> Result; + /// Process a message sent to this session state object. + /// + /// Depending on the message, an optional "response" [SessionMessage] might be returned. + /// This will be sent to the sender of the original message. + /// Similarly, if the processing of the message caused some changes to the state, an optional + /// "refresh" [SessionMessage] should be returned to then update the frontend. + fn process_message( + &mut self, + message: &SessionMessage, + ) -> Result<(Option, Option), DynError>; + /// Returns the string identifier of this particular session. Each session identifier must /// be unique within the application. fn id(&self) -> &str; diff --git a/src-tauri/src/main.rs b/src-tauri/src/main.rs index d67fcfa..072e4c6 100644 --- a/src-tauri/src/main.rs +++ b/src-tauri/src/main.rs @@ -1,17 +1,18 @@ // Prevents additional console window on Windows in release, DO NOT REMOVE!! #![cfg_attr(not(debug_assertions), windows_subsystem = "windows")] -use aeon_sketchbook::app::event::{Event, UserAction}; +use aeon_sketchbook::app::event::{Event, SessionMessage, StateChange, UserAction}; +use aeon_sketchbook::app::event_wrappers::{AeonAction, AeonMessage, AeonRefresh}; use aeon_sketchbook::app::state::analysis::AnalysisSession; use aeon_sketchbook::app::state::editor::EditorSession; use aeon_sketchbook::app::state::{AppState, DynSession}; -use aeon_sketchbook::app::{AeonApp, AEON_ACTION, AEON_REFRESH, AEON_VALUE}; +use aeon_sketchbook::app::{ + AeonApp, AEON_ACTION, AEON_MESSAGE, AEON_REFRESH, DEFAULT_SESSION_ID, DEFAULT_WINDOW_ID, +}; use aeon_sketchbook::debug; -use aeon_sketchbook::sketchbook::data_structs::SketchData; -use aeon_sketchbook::sketchbook::JsonSerde; -use aeon_sketchbook::sketchbook::Sketch; use chrono::prelude::*; -use serde::{Deserialize, Serialize}; +use std::thread; +use std::time::Duration; use tauri::{command, Manager, State, Window}; #[command] @@ -19,24 +20,13 @@ fn get_session_id(window: Window, state: State) -> String { state.get_session_id(&window) } -#[derive(Serialize, Deserialize)] -struct AeonAction { - session: String, - events: Vec, -} - -#[derive(Serialize, Deserialize)] -struct AeonRefresh { - session: String, - path: Vec, -} - fn main() { // Initialize empty app state. let state = AppState::default(); - let session: DynSession = Box::new(EditorSession::new("editor-1")); - state.session_created("editor-1", session); - state.window_created("editor", "editor-1"); + + let session: DynSession = Box::new(EditorSession::new(DEFAULT_SESSION_ID)); + state.session_created(DEFAULT_SESSION_ID, session); + state.window_created(DEFAULT_WINDOW_ID, DEFAULT_SESSION_ID); tauri::Builder::default() .manage(state) @@ -68,34 +58,23 @@ fn main() { // TODO: this part should be probably moved elsewhere, just a placeholder for now // check for "new-session" events here if action.events.len() == 1 && action.events[0].path == ["new-analysis-session"] { - let payload = action.events[0] - .payload - .clone() - .ok_or( - "This `new-analysis-session` event cannot carry empty payload." - .to_string(), - ) - .unwrap(); - let sketch_data = SketchData::from_json_str(&payload).unwrap(); - let sketch = Sketch::new_from_sketch_data(&sketch_data).unwrap(); - + // prepare (timestamped) session and window instances for AppState let time_now = Utc::now(); let timestamp = time_now.timestamp(); let new_session_id = format!("analysis-{timestamp}"); let new_window_id = format!("analysis-{timestamp}-window"); - let new_session: DynSession = - Box::new(AnalysisSession::new(&new_session_id, sketch)); + let new_session: DynSession = Box::new(AnalysisSession::new(&new_session_id)); state.session_created(&new_session_id, new_session); state.window_created(&new_window_id, &new_session_id); - // Create a new window for the analysis session + // create a new window for the analysis session in tauri let new_window = tauri::WindowBuilder::new( &handle, - &new_window_id, // The unique window label - tauri::WindowUrl::App("src/html/analysis.html".into()), // The URL or path to the HTML file + &new_window_id, + tauri::WindowUrl::App("src/html/analysis.html".into()), ) .title(format!( - "Inference Workflow (opened on {})", + "Inference Workflow (started on {})", time_now.to_rfc2822() )) .build(); @@ -106,18 +85,37 @@ fn main() { ), Err(e) => panic!("Failed to create new window: {:?}", e), } + + // todo: add better way + let sleep_duration = Duration::from_millis(1200); + thread::sleep(sleep_duration); + + // send request message "from" the new analysis session to the editor session + // asking to transfer Sketch data + let message = SessionMessage { + message: Event::build(&["send_sketch"], None), + }; + let res = + state.consume_message(&aeon, DEFAULT_SESSION_ID, &new_session_id, &message); + if let Err(e) = res { + panic!( + "Failed transferring sketch data from editor to analysis: {:?}", + e + ); + } } else { - let result = state.consume_event(&aeon, session_id.as_str(), &action); + let result = state.consume_event(&aeon, &session_id, &action); if let Err(e) = result { - // TODO: This should be a normal error. - //panic!("Event error: {:?}", e); - - // TODO: This is only a temporary solution to propagate the error message to frontend. + // TODO: This is only a temporary solution to propagate this kind of error message to frontend. debug!("Error processing last event: `{}`.", e.to_string()); // A crude way to escape the error message and wrap it in quotes. let json_message = serde_json::Value::String(e.to_string()).to_string(); - let state_change = Event::build(&["error"], Some(&json_message)); - if aeon.tauri.emit_all(AEON_VALUE, vec![state_change]).is_err() { + let state_change = StateChange { + events: vec![Event::build(&["error"], Some(&json_message))], + }; + let res_emit = + state.emit_to_session_windows(&aeon, &session_id, state_change); + if let Err(e) = res_emit { panic!("Event error failed to be sent: {:?}", e); } } @@ -146,6 +144,37 @@ fn main() { panic!("Event error: {:?}", e); } }); + let aeon = aeon_original.clone(); + app.listen_global(AEON_MESSAGE, move |e| { + let Some(payload) = e.payload() else { + // TODO: This should be an error. + panic!("No payload in backend message."); + }; + debug!("Received backend message: `{}`.", payload); + let event: AeonMessage = match serde_json::from_str::(payload) { + Ok(message) => message, + Err(e) => { + // TODO: This should be a normal error. + panic!("Payload deserialize error {:?}.", e); + } + }; + let state = aeon.tauri.state::(); + let session_from_id = event.session_from.clone(); + let session_to_id = event.session_to.clone(); + let message = SessionMessage { + message: event.message, + }; + let result = state.consume_message( + &aeon, + session_to_id.as_str(), + session_from_id.as_str(), + &message, + ); + if let Err(e) = result { + // TODO: This should be a normal error. + panic!("Event error: {:?}", e); + } + }); Ok(()) }) .invoke_handler(tauri::generate_handler![get_session_id]) diff --git a/src-tauri/src/sketchbook/_sketch/mod.rs b/src-tauri/src/sketchbook/_sketch/mod.rs index c7492c3..1d9b28e 100644 --- a/src-tauri/src/sketchbook/_sketch/mod.rs +++ b/src-tauri/src/sketchbook/_sketch/mod.rs @@ -16,9 +16,9 @@ mod _impl_sketch; /// modules is needed. #[derive(Clone, Debug, PartialEq, Serialize, Deserialize)] pub struct Sketch { - model: ModelState, - observations: ObservationManager, - properties: PropertyManager, + pub model: ModelState, + pub observations: ObservationManager, + pub properties: PropertyManager, } impl<'de> JsonSerde<'de> for Sketch {} diff --git a/src-tauri/src/sketchbook/data_structs/_sketch_data.rs b/src-tauri/src/sketchbook/data_structs/_sketch_data.rs index 9e9c851..bf25176 100644 --- a/src-tauri/src/sketchbook/data_structs/_sketch_data.rs +++ b/src-tauri/src/sketchbook/data_structs/_sketch_data.rs @@ -2,7 +2,7 @@ use crate::sketchbook::data_structs::{DatasetData, DynPropertyData, ModelData, S use crate::sketchbook::model::ModelState; use crate::sketchbook::observations::ObservationManager; use crate::sketchbook::properties::PropertyManager; -use crate::sketchbook::JsonSerde; +use crate::sketchbook::{JsonSerde, Sketch}; use serde::{Deserialize, Serialize}; /// Structure for sending/exporting data about the whole Sketch. @@ -43,4 +43,9 @@ impl SketchData { stat_properties, } } + + /// Create new `SketchData` instance given a reference to the `Sketch` instance. + pub fn new_from_sketch(sketch: &Sketch) -> SketchData { + Self::new(&sketch.model, &sketch.observations, &sketch.properties) + } } diff --git a/src/aeon_events.ts b/src/aeon_events.ts index bc3a813..ebe6bfa 100644 --- a/src/aeon_events.ts +++ b/src/aeon_events.ts @@ -338,6 +338,12 @@ interface AeonState { } } + /** The events regarding the analysis workflow. */ + analysis: { + /** Sketch data received. */ + sketchRefreshed: Observable + } + /** The information about errors occurring when processing events on backend. */ error: { /** Error message provided by backend. */ @@ -347,7 +353,6 @@ interface AeonState { /** Events for creating new sessions. */ new_session: { /** Create a new analysis session. */ - // TODO: this is just a placeholder for now createNewAnalysisSession: () => void } } @@ -868,23 +873,10 @@ export const aeonState: AeonState = { errorReceived: new Observable(['error']) }, new_session: { - // TODO: this is just a placeholder for now createNewAnalysisSession (): void { - const model: ModelData = { - variables: [], - regulations: [], - uninterpreted_fns: [], - layouts: [] - } - const sketch: SketchData = { - model, - datasets: [], - dyn_properties: [], - stat_properties: [] - } aeonEvents.emitAction({ path: ['new-analysis-session'], - payload: JSON.stringify(sketch) + payload: null }) } }, @@ -1355,5 +1347,8 @@ export const aeonState: AeonState = { }) } } + }, + analysis: { + sketchRefreshed: new Observable(['analysis', 'sketch_changed']) } } diff --git a/src/html/component-analysis/analysis-component/analysis-component.ts b/src/html/component-analysis/analysis-component/analysis-component.ts index b35ccd9..e1ac781 100644 --- a/src/html/component-analysis/analysis-component/analysis-component.ts +++ b/src/html/component-analysis/analysis-component/analysis-component.ts @@ -2,7 +2,8 @@ import { css, html, LitElement, type TemplateResult, unsafeCSS } from 'lit' import { customElement, property } from 'lit/decorators.js' import style_less from './analysis-component.less?inline' import { - aeonState + aeonState, + type SketchData } from '../../../aeon_events' import { ContentData @@ -21,6 +22,19 @@ export default class AnalysisComponent extends LitElement { aeonState.error.errorReceived.addEventListener((e) => { void this.#onErrorMessage(e) }) + + // underlying sketch data updated (should only happen at the beginning) + aeonState.analysis.sketchRefreshed.addEventListener((sketch) => { + void this.#onSketchRefreshed(sketch) + }) + } + + async #onSketchRefreshed (sketchData: SketchData): Promise { + const numVars = sketchData.model.variables.length + await dialog.message('Received sketch data, yay! It has ' + numVars.toString() + ' vars.', { + type: 'info', + title: 'Sketch received.' + }) } async #onErrorMessage (errorMessage: string): Promise { @@ -56,11 +70,20 @@ export default class AnalysisComponent extends LitElement {

    Inference

    + +
    + +
    +
From ba91f5c39a6532aefab49ffd080db2a71c3289e3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ond=C5=99ej=20Huvar?= <492849@mail.muni.cz> Date: Sat, 27 Jul 2024 19:09:52 +0200 Subject: [PATCH 3/8] Add placeholder events to start the inference and to receive results. --- src-tauri/src/analysis/analysis_state.rs | 100 ++++++++++++++++++ src-tauri/src/analysis/mod.rs | 69 +----------- src-tauri/src/app/state/_state_app.rs | 3 +- .../state/analysis/_state_analysis_session.rs | 11 +- src/aeon_events.ts | 54 +++++++++- .../analysis-component/analysis-component.ts | 94 ++++++++++++---- 6 files changed, 232 insertions(+), 99 deletions(-) create mode 100644 src-tauri/src/analysis/analysis_state.rs diff --git a/src-tauri/src/analysis/analysis_state.rs b/src-tauri/src/analysis/analysis_state.rs new file mode 100644 index 0000000..10fbc92 --- /dev/null +++ b/src-tauri/src/analysis/analysis_state.rs @@ -0,0 +1,100 @@ +use crate::app::event::Event; +use crate::app::state::{Consumed, SessionHelper, SessionState}; +use crate::app::DynError; +use crate::debug; +use crate::sketchbook::data_structs::SketchData; +use crate::sketchbook::{JsonSerde, Sketch}; +use serde::{Deserialize, Serialize}; + +/// Object encompassing all of the state components of the Analysis itself. +#[derive(Clone, Debug, PartialEq, Serialize, Deserialize)] +pub struct AnalysisState { + /// Boolean network sketch to run the analysis on. Can be a placeholder at the beginning. + sketch: Sketch, + /// Flag signalling that the actual sketch data were received from editor session. + sketch_received: bool, + // TODO +} + +impl AnalysisState { + /// Create new `AnalysisState` with an empty placeholder sketch. + /// + /// This is used to create a placeholder instance before the actual sketch data are sent from + /// the editor session. + pub fn new_empty() -> AnalysisState { + AnalysisState { + sketch: Sketch::default(), + sketch_received: false, + } + } + + /// Create new `AnalysisState` with a full sketch data. + pub fn new(sketch: Sketch) -> AnalysisState { + AnalysisState { + sketch, + sketch_received: true, + } + } + + /// Update the sketch data of this `AnalysisState`. + pub fn set_sketch(&mut self, sketch: Sketch) { + self.sketch = sketch; + self.sketch_received = true; + } + + /// Get reference to the sketch data of this `AnalysisState`. + pub fn get_sketch(&self) -> &Sketch { + &self.sketch + } +} + +impl SessionHelper for AnalysisState {} + +impl SessionState for AnalysisState { + fn perform_event(&mut self, event: &Event, at_path: &[&str]) -> Result { + let component = "analysis"; + + match at_path.first() { + Some(&"run_inference") => { + Self::assert_payload_empty(event, component)?; + debug!("Event `run_inference` received. It is not implemented at the moment."); + // TODO + + let state_change = Event::build(&["analysis", "inference_running"], Some("true")); + Ok(Consumed::Irreversible { + state_change, + reset: true, + }) + } + Some(&"run_static") => { + Self::assert_payload_empty(event, component)?; + debug!("Event `run_static` received. It is not implemented at the moment."); + // TODO + + let state_change = Event::build(&["analysis", "static_running"], Some("true")); + Ok(Consumed::Irreversible { + state_change, + reset: true, + }) + } + _ => Self::invalid_path_error_generic(at_path), + } + } + + fn refresh(&self, full_path: &[String], at_path: &[&str]) -> Result { + let component_name = "analysis"; + + // currently three options: get all datasets, a single dataset, a single observation + match at_path.first() { + Some(&"get_sketch") => { + Self::assert_path_length(at_path, 1, component_name)?; + let sketch_data = SketchData::new_from_sketch(&self.sketch); + Ok(Event { + path: full_path.to_vec(), + payload: Some(sketch_data.to_json_str()), + }) + } + _ => Self::invalid_path_error_generic(at_path), + } + } +} diff --git a/src-tauri/src/analysis/mod.rs b/src-tauri/src/analysis/mod.rs index f935d41..3a9e3f1 100644 --- a/src-tauri/src/analysis/mod.rs +++ b/src-tauri/src/analysis/mod.rs @@ -1,68 +1 @@ -use crate::app::event::Event; -use crate::app::state::{Consumed, SessionHelper, SessionState}; -use crate::app::DynError; -use crate::debug; -use crate::sketchbook::Sketch; -use serde::{Deserialize, Serialize}; - -/// Object encompassing all of the state components of the Analysis. -#[derive(Clone, Debug, PartialEq, Serialize, Deserialize)] -pub struct AnalysisState { - /// Boolean network sketch to run the analysis on. Can be a placeholder at the beginning. - sketch: Sketch, - /// Flag signalling that the actual sketch data were received. - sketch_received: bool, - // TODO -} - -impl AnalysisState { - /// Create new `AnalysisState` with an empty placeholder sketch. - /// - /// This is used to create a placeholder instance before the actual sketch data are sent from - /// the editor session. - pub fn new_empty() -> AnalysisState { - AnalysisState { - sketch: Sketch::default(), - sketch_received: false, - } - } - - /// Create new `AnalysisState` with a full sketch data. - pub fn new(sketch: Sketch) -> AnalysisState { - AnalysisState { - sketch, - sketch_received: true, - } - } - - /// Update the sketch data of this `AnalysisState`. - pub fn set_sketch(&mut self, sketch: Sketch) { - self.sketch = sketch; - self.sketch_received = true; - } - - /// Get reference to the sketch data of this `AnalysisState`. - pub fn get_sketch(&self) -> &Sketch { - &self.sketch - } -} - -impl SessionHelper for AnalysisState {} - -impl SessionState for AnalysisState { - fn perform_event(&mut self, event: &Event, at_path: &[&str]) -> Result { - debug!( - "Events for analysis not implemented! Can't process {:?} at {:?}", - event, at_path - ); - todo!() - } - - fn refresh(&self, full_path: &[String], at_path: &[&str]) -> Result { - debug!( - "Refresh for analysis not implemented! Can't process {:?} {:?}", - full_path, at_path - ); - todo!() - } -} +pub mod analysis_state; diff --git a/src-tauri/src/app/state/_state_app.rs b/src-tauri/src/app/state/_state_app.rs index 4b9d0f5..fe96016 100644 --- a/src-tauri/src/app/state/_state_app.rs +++ b/src-tauri/src/app/state/_state_app.rs @@ -2,7 +2,7 @@ use crate::app::event::{SessionMessage, StateChange, UserAction}; use crate::app::event_wrappers::AeonMessage; use crate::app::state::DynSession; use crate::app::{AeonApp, AeonError, DynError, AEON_MESSAGE, AEON_VALUE}; -use crate::{debug, warning}; +use crate::warning; use std::collections::HashMap; use std::ops::{Deref, DerefMut}; use std::sync::Mutex; @@ -96,7 +96,6 @@ impl AppState { state_change: StateChange, ) -> Result<(), DynError> { let window_ids = self.get_windows_for_session(session_id); - debug!("{:?}", window_ids); if window_ids.is_empty() { warning!("No windows correspond to provided session `{session_id}`.") } diff --git a/src-tauri/src/app/state/analysis/_state_analysis_session.rs b/src-tauri/src/app/state/analysis/_state_analysis_session.rs index 027652c..d4e9d76 100644 --- a/src-tauri/src/app/state/analysis/_state_analysis_session.rs +++ b/src-tauri/src/app/state/analysis/_state_analysis_session.rs @@ -1,4 +1,4 @@ -use crate::analysis::AnalysisState; +use crate::analysis::analysis_state::AnalysisState; use crate::app::event::{Event, SessionMessage, StateChange, UserAction}; use crate::app::state::_undo_stack::UndoStack; use crate::app::state::{Consumed, Session, SessionHelper, SessionState}; @@ -203,14 +203,13 @@ impl Session for AnalysisSession { } else { panic!("Message `sketch_sent` must always carry a payload.") } - // no response is expected, but we must inform frontend about state change + + // no backend response is expected, but we must send refresh event to inform frontend + // about the state change let sketch_data = SketchData::new_from_sketch(self.analysis_state.get_sketch()); let payload = sketch_data.to_json_str(); let state_change = StateChange { - events: vec![Event::build( - &["analysis", "sketch_changed"], - Some(&payload), - )], + events: vec![Event::build(&["analysis", "get_sketch"], Some(&payload))], }; Ok((None, Some(state_change))) } else { diff --git a/src/aeon_events.ts b/src/aeon_events.ts index ebe6bfa..8621d95 100644 --- a/src/aeon_events.ts +++ b/src/aeon_events.ts @@ -340,8 +340,25 @@ interface AeonState { /** The events regarding the analysis workflow. */ analysis: { - /** Sketch data received. */ + /** Sketch data transfered from backend (useful to initiate the state). */ sketchRefreshed: Observable + /** Ask for a sketch data (might be useful to update analysis window, or if automatic sketch + * transfer from backend does not work). */ + refreshSketch: () => void + + /** Start the full inference analysis. */ + startFullInference: () => void + /** Note that inference analysis was started. */ + inferenceStarted: Observable + /** Inference analysis results. */ + inferenceResultsReceived: Observable + + /** Start the static check analysis. */ + startStaticCheck: () => void + /** Note that static check analysis was started. */ + staticCheckStarted: Observable + /** Static check analysis results. */ + staticCheckResultsReceived: Observable } /** The information about errors occurring when processing events on backend. */ @@ -467,6 +484,18 @@ export interface DynPropIdUpdateData { original_id: string, new_id: string } /** An object representing information needed for static property's id change. */ export interface StatPropIdUpdateData { original_id: string, new_id: string } +/** An object representing all information regarding inference analysis results. */ +export interface InferenceResults { + numSatNetworks: number + computationTime: number +} + +/** An object representing all information regarding static check analysis results. */ +export interface StaticCheckResults { + numSatNetworks: number + computationTime: number +} + /** A function that is notified when a state value changes. */ export type OnStateValue = (value: T) => void @@ -1349,6 +1378,27 @@ export const aeonState: AeonState = { } }, analysis: { - sketchRefreshed: new Observable(['analysis', 'sketch_changed']) + sketchRefreshed: new Observable(['analysis', 'get_sketch']), + refreshSketch (): void { + aeonEvents.refresh(['analysis', 'get_sketch']) + }, + + inferenceResultsReceived: new Observable(['analysis', 'inference_results']), + staticCheckResultsReceived: new Observable(['analysis', 'static_results']), + inferenceStarted: new Observable(['analysis', 'inference_running']), + staticCheckStarted: new Observable(['analysis', 'static_running']), + + startFullInference (): void { + aeonEvents.emitAction({ + path: ['analysis', 'run_inference'], + payload: null + }) + }, + startStaticCheck (): void { + aeonEvents.emitAction({ + path: ['analysis', 'run_static'], + payload: null + }) + } } } diff --git a/src/html/component-analysis/analysis-component/analysis-component.ts b/src/html/component-analysis/analysis-component/analysis-component.ts index e1ac781..e199fce 100644 --- a/src/html/component-analysis/analysis-component/analysis-component.ts +++ b/src/html/component-analysis/analysis-component/analysis-component.ts @@ -3,17 +3,16 @@ import { customElement, property } from 'lit/decorators.js' import style_less from './analysis-component.less?inline' import { aeonState, - type SketchData + type SketchData, + type InferenceResults, + type StaticCheckResults } from '../../../aeon_events' -import { - ContentData -} from '../../util/data-interfaces' import { dialog } from '@tauri-apps/api' @customElement('analysis-component') export default class AnalysisComponent extends LitElement { static styles = css`${unsafeCSS(style_less)}` - @property() data: ContentData = ContentData.create() + @property() sketchData: SketchData | null = null constructor () { super() @@ -27,14 +26,36 @@ export default class AnalysisComponent extends LitElement { aeonState.analysis.sketchRefreshed.addEventListener((sketch) => { void this.#onSketchRefreshed(sketch) }) + + // updates regarding analyses received + aeonState.analysis.inferenceStarted.addEventListener( + this.#onInferenceStarted.bind(this) + ) + aeonState.analysis.staticCheckStarted.addEventListener( + this.#onStaticCheckStarted.bind(this) + ) + aeonState.analysis.inferenceResultsReceived.addEventListener( + this.#onInferenceResultsReceived.bind(this) + ) + aeonState.analysis.staticCheckResultsReceived.addEventListener( + this.#onStaticCheckResultsReceived.bind(this) + ) + + // ask for sketch data during initiation (just in case the automatic transfer fails) + aeonState.analysis.refreshSketch() } async #onSketchRefreshed (sketchData: SketchData): Promise { - const numVars = sketchData.model.variables.length - await dialog.message('Received sketch data, yay! It has ' + numVars.toString() + ' vars.', { - type: 'info', - title: 'Sketch received.' - }) + // currently we only accept the sketch data once, and it is frozen later + // if this changes and we want to allow re-writing sketch data, update this function + + if (this.sketchData === null) { + this.sketchData = sketchData + const numVars = sketchData.model.variables.length + console.log('Received sketch data. The sketch has ' + numVars.toString() + ' variables.') + } else { + console.log('Can\'t accept sketch data. Sketch was already set before.') + } } async #onErrorMessage (errorMessage: string): Promise { @@ -44,6 +65,34 @@ export default class AnalysisComponent extends LitElement { }) } + #onInferenceStarted (success: boolean): void { + if (success) { + console.log('Inference analysis sucessfully started.') + } else { + console.log('Error starting inference analysis.') + } + } + + #onStaticCheckStarted (success: boolean): void { + if (success) { + console.log('Static check analysis sucessfully started.') + } else { + console.log('Error starting static check analysis.') + } + } + + #onInferenceResultsReceived (results: InferenceResults): void { + console.log('Received full inference results.') + console.log('-> There are ' + results.numSatNetworks + ' satisfying networks.') + console.log('-> The computation took ' + results.computationTime + ' seconds.') + } + + #onStaticCheckResultsReceived (results: StaticCheckResults): void { + console.log('Received static check results.') + console.log('-> There are ' + results.numSatNetworks + ' satisfying networks.') + console.log('-> The computation took ' + results.computationTime + ' seconds.') + } + private async confirmDialog (): Promise { return await dialog.ask('Are you sure?', { type: 'warning', @@ -53,13 +102,16 @@ export default class AnalysisComponent extends LitElement { }) } - private async dummyDialog (): Promise { - return await dialog.ask('Hello there.', { - type: 'info', - okLabel: 'OK', - cancelLabel: 'Cancel', - title: 'Hello there' - }) + private runInference (): void { + console.log('Initiating inference analysis, wait a bit...') + aeonState.analysis.startFullInference() + // TODO + } + + private runStaticCheck (): void { + console.log('Initiating static check, wait a bit...') + aeonState.analysis.startStaticCheck() + // TODO } render (): TemplateResult { @@ -74,16 +126,16 @@ export default class AnalysisComponent extends LitElement {
From c0d6fd93c0913499f52e09d6cba6a15fca68a9fe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ond=C5=99ej=20Huvar?= <492849@mail.muni.cz> Date: Sun, 28 Jul 2024 12:41:51 +0200 Subject: [PATCH 4/8] Move common functionality between sessions to Session trait. --- .../state/analysis/_state_analysis_session.rs | 171 ++--------------- .../app/state/editor/_state_editor_session.rs | 171 ++--------------- src-tauri/src/app/state/mod.rs | 181 +++++++++++++++++- src-tauri/src/main.rs | 2 +- 4 files changed, 201 insertions(+), 324 deletions(-) diff --git a/src-tauri/src/app/state/analysis/_state_analysis_session.rs b/src-tauri/src/app/state/analysis/_state_analysis_session.rs index d4e9d76..2463c3a 100644 --- a/src-tauri/src/app/state/analysis/_state_analysis_session.rs +++ b/src-tauri/src/app/state/analysis/_state_analysis_session.rs @@ -1,7 +1,7 @@ use crate::analysis::analysis_state::AnalysisState; -use crate::app::event::{Event, SessionMessage, StateChange, UserAction}; +use crate::app::event::{Event, SessionMessage, StateChange}; use crate::app::state::_undo_stack::UndoStack; -use crate::app::state::{Consumed, Session, SessionHelper, SessionState}; +use crate::app::state::{Consumed, SessionHelper, SessionState, StackSession}; use crate::app::{AeonError, DynError}; use crate::debug; use crate::sketchbook::data_structs::SketchData; @@ -24,166 +24,9 @@ impl AnalysisSession { analysis_state: AnalysisState::new_empty(), } } - - fn perform_action( - &mut self, - action: &UserAction, - ignore_stack: bool, - ) -> Result { - // Events that need to be consume (last to first) in order to complete this action. - let mut to_perform = action.events.clone(); - to_perform.reverse(); - - // The events representing successful state changes. - let mut state_changes: Vec = Vec::new(); - // The events that can be used to create a redo stack entry if the action is reversible. - let mut reverse: Option> = - if ignore_stack { None } else { Some(Vec::new()) }; - let mut reset_stack = false; - - while let Some(event) = to_perform.pop() { - let event_path = event.path.iter().map(|it| it.as_str()).collect::>(); - debug!( - "Executing event to session {}: `{:?}`.", - self.id, event_path - ); - let result = match self.perform_event(&event, &event_path) { - Ok(result) => result, - Err(error) => { - // TODO: - // We should probably first emit the state change and then the - // error, because now we are losing state of compound actions that fail. - return Err(error); - } - }; - match result { - Consumed::Reversible { - state_change, - perform_reverse, - } => { - state_changes.push(state_change); - if let Some(reverse) = reverse.as_mut() { - // If we can reverse this action, save the events. - reverse.push(perform_reverse); - } - } - Consumed::Irreversible { - state_change, - reset, - } => { - state_changes.push(state_change); - if reset { - // We cannot reverse this event, but the rest can be reversed. - reverse = None; - reset_stack = true; - } - } - Consumed::Restart(mut events) => { - // Just push the new events to the execution stack and continue - // to the next event. - events.reverse(); - while let Some(e) = events.pop() { - to_perform.push(e); - } - } - Consumed::InputError(error) => { - // TODO: - // The same as above. We should report this as a separate event from the - // state change that was performed. - return Err(error); - } - Consumed::NoChange => { - // Do nothing. - } - } - } - - // If the action is not irreversible, we should add an entry to the undo stack. - if let Some(events) = reverse { - if !events.is_empty() { - // Only add undo action if the stack is not empty. - let mut perform = Vec::new(); - let mut reverse = Vec::new(); - for (p, r) in events { - perform.push(p); - reverse.push(r); - } - // Obviously, the "reverse" events need to be execute in the opposite order - // compared to the "perform" events. - reverse.reverse(); - let perform = UserAction { events: perform }; - let reverse = UserAction { events: reverse }; - if !self.undo_stack.do_action(perform, reverse) { - // TODO: Not match we can do here, maybe except issuing a warning. - self.undo_stack.clear(); - } - - // Notify about the changes in the stack state. - // TODO: Maybe we don't need to emit this always. - self.append_stack_updates(&mut state_changes); - } - } else if !ignore_stack && reset_stack { - debug!( - "Back stack (of session {}) cleared due to irreversible action.", - self.id - ); - self.undo_stack.clear(); - } - - Ok(StateChange { - events: state_changes, - }) - } - - fn append_stack_updates(&self, state_changes: &mut Vec) { - let can_undo = serde_json::to_string(&self.undo_stack.can_undo()); - let can_redo = serde_json::to_string(&self.undo_stack.can_redo()); - state_changes.push(Event::build( - &["undo_stack", "can_undo"], - Some(can_undo.unwrap().as_str()), - )); - state_changes.push(Event::build( - &["undo_stack", "can_redo"], - Some(can_redo.unwrap().as_str()), - )); - } } -impl Session for AnalysisSession { - fn perform_action(&mut self, action: &UserAction) -> Result { - // Explicit test for undo-stack actions. - // TODO: - // Figure out a nicer way to do this. Probably modify the `Consumed` enum? - // We basically need a way to say "restart with these events, but as an - // Irreversible action that won't reset the stack." - 'undo: { - if action.events.len() == 1 { - let event = &action.events[0]; - if event.path.len() == 2 && event.path[0] == "undo_stack" { - let action = match event.path[1].as_str() { - "undo" => { - let Some(undo) = self.undo_stack.undo_action() else { - return AeonError::throw("Nothing to undo."); - }; - undo - } - "redo" => { - let Some(redo) = self.undo_stack.redo_action() else { - return AeonError::throw("Nothing to redo."); - }; - redo - } - _ => break 'undo, - }; - let mut state_change = self.perform_action(&action, true)?; - self.append_stack_updates(&mut state_change.events); - return Ok(state_change); - } - } - } - self.perform_action(action, false) - } - +impl StackSession for AnalysisSession { fn process_message( &mut self, message: &SessionMessage, @@ -230,6 +73,14 @@ impl Session for AnalysisSession { fn id(&self) -> &str { self.id.as_str() } + + fn undo_stack_mut(&mut self) -> &mut UndoStack { + &mut self.undo_stack + } + + fn undo_stack(&self) -> &UndoStack { + &self.undo_stack + } } impl SessionHelper for AnalysisSession {} diff --git a/src-tauri/src/app/state/editor/_state_editor_session.rs b/src-tauri/src/app/state/editor/_state_editor_session.rs index 5cd6f84..b7d98f1 100644 --- a/src-tauri/src/app/state/editor/_state_editor_session.rs +++ b/src-tauri/src/app/state/editor/_state_editor_session.rs @@ -1,7 +1,7 @@ -use crate::app::event::{Event, SessionMessage, StateChange, UserAction}; +use crate::app::event::{Event, SessionMessage, StateChange}; use crate::app::state::_undo_stack::UndoStack; use crate::app::state::editor::TabBarState; -use crate::app::state::{Consumed, Session, SessionHelper, SessionState}; +use crate::app::state::{Consumed, SessionHelper, SessionState, StackSession}; use crate::app::{AeonError, DynError}; use crate::debug; use crate::sketchbook::{JsonSerde, Sketch}; @@ -26,166 +26,9 @@ impl EditorSession { sketch: Sketch::default(), } } - - fn perform_action( - &mut self, - action: &UserAction, - ignore_stack: bool, - ) -> Result { - // Events that need to be consume (last to first) in order to complete this action. - let mut to_perform = action.events.clone(); - to_perform.reverse(); - - // The events representing successful state changes. - let mut state_changes: Vec = Vec::new(); - // The events that can be used to create a redo stack entry if the action is reversible. - let mut reverse: Option> = - if ignore_stack { None } else { Some(Vec::new()) }; - let mut reset_stack = false; - - while let Some(event) = to_perform.pop() { - let event_path = event.path.iter().map(|it| it.as_str()).collect::>(); - debug!( - "Executing event to session {}: `{:?}`.", - self.id, event_path - ); - let result = match self.perform_event(&event, &event_path) { - Ok(result) => result, - Err(error) => { - // TODO: - // We should probably first emit the state change and then the - // error, because now we are losing state of compound actions that fail. - return Err(error); - } - }; - match result { - Consumed::Reversible { - state_change, - perform_reverse, - } => { - state_changes.push(state_change); - if let Some(reverse) = reverse.as_mut() { - // If we can reverse this action, save the events. - reverse.push(perform_reverse); - } - } - Consumed::Irreversible { - state_change, - reset, - } => { - state_changes.push(state_change); - if reset { - // We cannot reverse this event, but the rest can be reversed. - reverse = None; - reset_stack = true; - } - } - Consumed::Restart(mut events) => { - // Just push the new events to the execution stack and continue - // to the next event. - events.reverse(); - while let Some(e) = events.pop() { - to_perform.push(e); - } - } - Consumed::InputError(error) => { - // TODO: - // The same as above. We should report this as a separate event from the - // state change that was performed. - return Err(error); - } - Consumed::NoChange => { - // Do nothing. - } - } - } - - // If the action is not irreversible, we should add an entry to the undo stack. - if let Some(events) = reverse { - if !events.is_empty() { - // Only add undo action if the stack is not empty. - let mut perform = Vec::new(); - let mut reverse = Vec::new(); - for (p, r) in events { - perform.push(p); - reverse.push(r); - } - // Obviously, the "reverse" events need to be execute in the opposite order - // compared to the "perform" events. - reverse.reverse(); - let perform = UserAction { events: perform }; - let reverse = UserAction { events: reverse }; - if !self.undo_stack.do_action(perform, reverse) { - // TODO: Not match we can do here, maybe except issuing a warning. - self.undo_stack.clear(); - } - - // Notify about the changes in the stack state. - // TODO: Maybe we don't need to emit this always. - self.append_stack_updates(&mut state_changes); - } - } else if !ignore_stack && reset_stack { - debug!( - "Back stack (of session {}) cleared due to irreversible action.", - self.id - ); - self.undo_stack.clear(); - } - - Ok(StateChange { - events: state_changes, - }) - } - - fn append_stack_updates(&self, state_changes: &mut Vec) { - let can_undo = serde_json::to_string(&self.undo_stack.can_undo()); - let can_redo = serde_json::to_string(&self.undo_stack.can_redo()); - state_changes.push(Event::build( - &["undo_stack", "can_undo"], - Some(can_undo.unwrap().as_str()), - )); - state_changes.push(Event::build( - &["undo_stack", "can_redo"], - Some(can_redo.unwrap().as_str()), - )); - } } -impl Session for EditorSession { - fn perform_action(&mut self, action: &UserAction) -> Result { - // Explicit test for undo-stack actions. - // TODO: - // Figure out a nicer way to do this. Probably modify the `Consumed` enum? - // We basically need a way to say "restart with these events, but as an - // Irreversible action that won't reset the stack." - 'undo: { - if action.events.len() == 1 { - let event = &action.events[0]; - if event.path.len() == 2 && event.path[0] == "undo_stack" { - let action = match event.path[1].as_str() { - "undo" => { - let Some(undo) = self.undo_stack.undo_action() else { - return AeonError::throw("Nothing to undo."); - }; - undo - } - "redo" => { - let Some(redo) = self.undo_stack.redo_action() else { - return AeonError::throw("Nothing to redo."); - }; - redo - } - _ => break 'undo, - }; - let mut state_change = self.perform_action(&action, true)?; - self.append_stack_updates(&mut state_change.events); - return Ok(state_change); - } - } - } - self.perform_action(action, false) - } - +impl StackSession for EditorSession { fn process_message( &mut self, message: &SessionMessage, @@ -223,6 +66,14 @@ impl Session for EditorSession { fn id(&self) -> &str { self.id.as_str() } + + fn undo_stack_mut(&mut self) -> &mut UndoStack { + &mut self.undo_stack + } + + fn undo_stack(&self) -> &UndoStack { + &self.undo_stack + } } impl SessionHelper for EditorSession {} diff --git a/src-tauri/src/app/state/mod.rs b/src-tauri/src/app/state/mod.rs index 55030cd..b63d17d 100644 --- a/src-tauri/src/app/state/mod.rs +++ b/src-tauri/src/app/state/mod.rs @@ -12,13 +12,15 @@ pub mod analysis; /// Declares state objects that are unique to the sketchbook editor window. pub mod editor; +use crate::app::state::_undo_stack::UndoStack; +use crate::debug; pub use _consumed::Consumed; pub use _state_app::AppState; pub use _state_atomic::AtomicState; //pub use _state_map::MapState; pub type DynSessionState = Box<(dyn SessionState + Send + 'static)>; -pub type DynSession = Box<(dyn Session + Send + 'static)>; +pub type DynSession = Box<(dyn StackSession + Send + 'static)>; pub trait SessionState { /// Modify the session state using the provided `event`. The possible outcomes are @@ -108,11 +110,178 @@ pub trait SessionHelper { } } -pub trait Session: SessionState { +/// A Session with a [UndoStack] with events. +/// +/// Sessions perform user actions, or communicate with different sessions via messages. +pub trait StackSession: SessionState { /// Perform a user action on this session state object. This usually involves propagating /// the events to the internal [SessionState] objects and collecting the results into a /// single [StateChange] entry. - fn perform_action(&mut self, action: &UserAction) -> Result; + /// + /// In this top-level method, we explicitly test for undo-stack actions. Once that is done, + /// the processing continues via [perform_categorized_action]. + fn perform_action(&mut self, action: &UserAction) -> Result { + // Explicit test for undo-stack actions. + // TODO: + // Figure out a nicer way to do this. Probably modify the `Consumed` enum? + // We basically need a way to say "restart with these events, but as an + // Irreversible action that won't reset the stack." + 'undo: { + if action.events.len() == 1 { + let event = &action.events[0]; + if event.path.len() == 2 && event.path[0] == "undo_stack" { + let action = match event.path[1].as_str() { + "undo" => { + let Some(undo) = self.undo_stack_mut().undo_action() else { + return AeonError::throw("Nothing to undo."); + }; + undo + } + "redo" => { + let Some(redo) = self.undo_stack_mut().redo_action() else { + return AeonError::throw("Nothing to redo."); + }; + redo + } + _ => break 'undo, + }; + let mut state_change = self.perform_categorized_action(&action, true)?; + self.append_stack_updates(&mut state_change.events); + return Ok(state_change); + } + } + } + self.perform_categorized_action(action, false) + } + + /// Perform a user action on this session state object, with additional information whether + /// the action should bypass the undo-redo stack. + /// + /// This method assumes the action was already categorized into one of `undo` (stack should be + /// bypassed) or `regular` (goes to the undo stack). + /// If you want to run the full process including categorizing the action, use [perform_action]. + fn perform_categorized_action( + &mut self, + action: &UserAction, + ignore_stack: bool, + ) -> Result { + // Events that need to be consume (last to first) in order to complete this action. + let mut to_perform = action.events.clone(); + to_perform.reverse(); + + // The events representing successful state changes. + let mut state_changes: Vec = Vec::new(); + // The events that can be used to create a redo stack entry if the action is reversible. + let mut reverse: Option> = + if ignore_stack { None } else { Some(Vec::new()) }; + let mut reset_stack = false; + + while let Some(event) = to_perform.pop() { + let event_path = event.path.iter().map(|it| it.as_str()).collect::>(); + debug!( + "Executing event to session {}: `{:?}`.", + self.id(), + event_path + ); + let result = match self.perform_event(&event, &event_path) { + Ok(result) => result, + Err(error) => { + // TODO: + // We should probably first emit the state change and then the + // error, because now we are losing state of compound actions that fail. + return Err(error); + } + }; + match result { + Consumed::Reversible { + state_change, + perform_reverse, + } => { + state_changes.push(state_change); + if let Some(reverse) = reverse.as_mut() { + // If we can reverse this action, save the events. + reverse.push(perform_reverse); + } + } + Consumed::Irreversible { + state_change, + reset, + } => { + state_changes.push(state_change); + if reset { + // We cannot reverse this event, but the rest can be reversed. + reverse = None; + reset_stack = true; + } + } + Consumed::Restart(mut events) => { + // Just push the new events to the execution stack and continue + // to the next event. + events.reverse(); + while let Some(e) = events.pop() { + to_perform.push(e); + } + } + Consumed::InputError(error) => { + // TODO: + // The same as above. We should report this as a separate event from the + // state change that was performed. + return Err(error); + } + Consumed::NoChange => { + // Do nothing. + } + } + } + // If the action is not irreversible, we should add an entry to the undo stack. + if let Some(events) = reverse { + if !events.is_empty() { + // Only add undo action if the stack is not empty. + let mut perform = Vec::new(); + let mut reverse = Vec::new(); + for (p, r) in events { + perform.push(p); + reverse.push(r); + } + // Obviously, the "reverse" events need to be execute in the opposite order + // compared to the "perform" events. + reverse.reverse(); + let perform = UserAction { events: perform }; + let reverse = UserAction { events: reverse }; + if !self.undo_stack_mut().do_action(perform, reverse) { + // TODO: Not match we can do here, maybe except issuing a warning. + self.undo_stack_mut().clear(); + } + + // Notify about the changes in the stack state. + // TODO: Maybe we don't need to emit this always. + self.append_stack_updates(&mut state_changes); + } + } else if !ignore_stack && reset_stack { + debug!( + "Back stack (of session {}) cleared due to irreversible action.", + self.id() + ); + self.undo_stack_mut().clear(); + } + + Ok(StateChange { + events: state_changes, + }) + } + + fn append_stack_updates(&self, state_changes: &mut Vec) { + let can_undo = serde_json::to_string(&self.undo_stack().can_undo()); + let can_redo = serde_json::to_string(&self.undo_stack().can_redo()); + state_changes.push(Event::build( + &["undo_stack", "can_undo"], + Some(can_undo.unwrap().as_str()), + )); + state_changes.push(Event::build( + &["undo_stack", "can_redo"], + Some(can_redo.unwrap().as_str()), + )); + } /// Process a message sent to this session state object. /// @@ -128,4 +297,10 @@ pub trait Session: SessionState { /// Returns the string identifier of this particular session. Each session identifier must /// be unique within the application. fn id(&self) -> &str; + + /// Returns an immutable reference to session's undo stack. + fn undo_stack(&self) -> &UndoStack; + + /// Returns a mutable reference to session's undo stack. + fn undo_stack_mut(&mut self) -> &mut UndoStack; } diff --git a/src-tauri/src/main.rs b/src-tauri/src/main.rs index 072e4c6..0f6db7d 100644 --- a/src-tauri/src/main.rs +++ b/src-tauri/src/main.rs @@ -106,7 +106,7 @@ fn main() { } else { let result = state.consume_event(&aeon, &session_id, &action); if let Err(e) = result { - // TODO: This is only a temporary solution to propagate this kind of error message to frontend. + // TODO: This is a temporary solution to propagate this kind of error message to frontend. debug!("Error processing last event: `{}`.", e.to_string()); // A crude way to escape the error message and wrap it in quotes. let json_message = serde_json::Value::String(e.to_string()).to_string(); From 187d014e7193912fa6169a8ed17e848d96c61b0d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ond=C5=99ej=20Huvar?= <492849@mail.muni.cz> Date: Sun, 28 Jul 2024 20:22:35 +0200 Subject: [PATCH 5/8] Initial work-in-progress pipeline and structures for inference. --- src-tauri/src/algorithms/eval_dynamic/mod.rs | 1 + src-tauri/src/algorithms/eval_static/mod.rs | 1 + src-tauri/src/algorithms/fo_logic/mod.rs | 1 + src-tauri/src/algorithms/mod.rs | 7 +- src-tauri/src/analysis/analysis_results.rs | 26 +++ src-tauri/src/analysis/analysis_state.rs | 21 ++- src-tauri/src/analysis/inference_solver.rs | 171 ++++++++++++++++++ src-tauri/src/analysis/mod.rs | 2 + src/aeon_events.ts | 8 +- .../analysis-component/analysis-component.ts | 12 +- 10 files changed, 235 insertions(+), 15 deletions(-) create mode 100644 src-tauri/src/algorithms/eval_dynamic/mod.rs create mode 100644 src-tauri/src/algorithms/eval_static/mod.rs create mode 100644 src-tauri/src/algorithms/fo_logic/mod.rs create mode 100644 src-tauri/src/analysis/analysis_results.rs create mode 100644 src-tauri/src/analysis/inference_solver.rs diff --git a/src-tauri/src/algorithms/eval_dynamic/mod.rs b/src-tauri/src/algorithms/eval_dynamic/mod.rs new file mode 100644 index 0000000..70b786d --- /dev/null +++ b/src-tauri/src/algorithms/eval_dynamic/mod.rs @@ -0,0 +1 @@ +// TODO diff --git a/src-tauri/src/algorithms/eval_static/mod.rs b/src-tauri/src/algorithms/eval_static/mod.rs new file mode 100644 index 0000000..70b786d --- /dev/null +++ b/src-tauri/src/algorithms/eval_static/mod.rs @@ -0,0 +1 @@ +// TODO diff --git a/src-tauri/src/algorithms/fo_logic/mod.rs b/src-tauri/src/algorithms/fo_logic/mod.rs new file mode 100644 index 0000000..70b786d --- /dev/null +++ b/src-tauri/src/algorithms/fo_logic/mod.rs @@ -0,0 +1 @@ +// TODO diff --git a/src-tauri/src/algorithms/mod.rs b/src-tauri/src/algorithms/mod.rs index 70b786d..1f6ccdf 100644 --- a/src-tauri/src/algorithms/mod.rs +++ b/src-tauri/src/algorithms/mod.rs @@ -1 +1,6 @@ -// TODO +/// 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; diff --git a/src-tauri/src/analysis/analysis_results.rs b/src-tauri/src/analysis/analysis_results.rs new file mode 100644 index 0000000..e2c2a35 --- /dev/null +++ b/src-tauri/src/analysis/analysis_results.rs @@ -0,0 +1,26 @@ +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, +} + +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) -> AnalysisResults { + AnalysisResults { + num_sat_networks, + comp_time: comp_time.as_secs(), + } + } +} diff --git a/src-tauri/src/analysis/analysis_state.rs b/src-tauri/src/analysis/analysis_state.rs index 10fbc92..9ca0501 100644 --- a/src-tauri/src/analysis/analysis_state.rs +++ b/src-tauri/src/analysis/analysis_state.rs @@ -1,3 +1,5 @@ +use crate::analysis::analysis_results::AnalysisResults; +use crate::analysis::inference_solver::InferenceSolver; use crate::app::event::Event; use crate::app::state::{Consumed, SessionHelper, SessionState}; use crate::app::DynError; @@ -6,16 +8,21 @@ use crate::sketchbook::data_structs::SketchData; use crate::sketchbook::{JsonSerde, Sketch}; use serde::{Deserialize, Serialize}; -/// Object encompassing all of the state components of the Analysis itself. +/// Object encompassing all of the state components of the Analysis itself that are exchanged +/// with frontend (no raw low-level structures like symbolic graph or its colors) #[derive(Clone, Debug, PartialEq, Serialize, Deserialize)] pub struct AnalysisState { /// Boolean network sketch to run the analysis on. Can be a placeholder at the beginning. sketch: Sketch, /// Flag signalling that the actual sketch data were received from editor session. sketch_received: bool, + /// Potential results of the analysis. + results: Option, // TODO } +impl<'de> JsonSerde<'de> for AnalysisState {} + impl AnalysisState { /// Create new `AnalysisState` with an empty placeholder sketch. /// @@ -25,6 +32,7 @@ impl AnalysisState { AnalysisState { sketch: Sketch::default(), sketch_received: false, + results: None, } } @@ -33,6 +41,7 @@ impl AnalysisState { AnalysisState { sketch, sketch_received: true, + results: None, } } @@ -57,10 +66,14 @@ impl SessionState for AnalysisState { match at_path.first() { Some(&"run_inference") => { Self::assert_payload_empty(event, component)?; - debug!("Event `run_inference` received. It is not implemented at the moment."); + debug!("Event `run_inference` received. It is not fully implemented yet."); // TODO - let state_change = Event::build(&["analysis", "inference_running"], Some("true")); + let mut inference_solver = InferenceSolver::new(); + let results = inference_solver.run_computation_prototype(self.sketch.clone())?; + + let payload = results.to_json_str(); + let state_change = Event::build(&["analysis", "inference_results"], Some(&payload)); Ok(Consumed::Irreversible { state_change, reset: true, @@ -68,7 +81,7 @@ impl SessionState for AnalysisState { } Some(&"run_static") => { Self::assert_payload_empty(event, component)?; - debug!("Event `run_static` received. It is not implemented at the moment."); + debug!("Event `run_static` received. It is not implemented at the moment. Only dummy message will be sent"); // TODO let state_change = Event::build(&["analysis", "static_running"], Some("true")); diff --git a/src-tauri/src/analysis/inference_solver.rs b/src-tauri/src/analysis/inference_solver.rs new file mode 100644 index 0000000..2b9a828 --- /dev/null +++ b/src-tauri/src/analysis/inference_solver.rs @@ -0,0 +1,171 @@ +use crate::analysis::analysis_results::AnalysisResults; +use crate::sketchbook::properties::dynamic_props::DynPropertyType; +use crate::sketchbook::properties::{FirstOrderFormula, HctlFormula}; +use crate::sketchbook::Sketch; +use biodivine_lib_param_bn::symbolic_async_graph::{GraphColors, SymbolicAsyncGraph}; +use biodivine_lib_param_bn::BooleanNetwork; +use std::time::SystemTime; + +/// Status of the computation, together with a timestamp. +#[derive(Clone)] +pub enum InferenceStatus { + Created(SystemTime), + Started(SystemTime), + ProcessedInputs(SystemTime), + GeneratedGraph(SystemTime), + EvaluatedStatic(SystemTime), + EvaluatedDynamic(SystemTime), + Finished(SystemTime), + Error(SystemTime), +} + +/// Object encompassing the process of the full BN inference. +/// +/// It tracks the intermediate results and low-level structures, and it provides hooks to the +/// actual algorithms. +/// +/// By tracking the intermediate results, we may be able to observe the computation, and potentially +/// "fork" or re-use parts of the computation in future. For now we do not run the computation +/// itself on a special thread, but in future, we may. +#[derive(Clone)] +pub struct InferenceSolver { + /// Boolean Network instance. + bn: Option, + /// Symbolic transition graph for the system. + graph: Option, + /// Static properties converted to FO logic. + static_props: Option>, + /// Dynamic properties converted to HCTL. + dynamic_props: Option>, + /// Intermediate set of candidate colors, gradually updated during computation. + raw_intermediate_colors: Option, + /// Set of final satisfying colors (once computed). + raw_sat_colors: Option, + /// Vector with all time-stamped status updates. The last is the latest status. + status_updates: Vec, +} + +impl InferenceSolver { + fn bn(&self) -> Result<&BooleanNetwork, String> { + if let Some(bn) = &self.bn { + Ok(bn) + } else { + Err("Boolean network not yet computed.".to_string()) + } + } + + fn graph(&self) -> Result<&SymbolicAsyncGraph, String> { + if let Some(graph) = &self.graph { + Ok(graph) + } else { + Err("Transition graph not yet computed.".to_string()) + } + } + + fn sat_colors(&self) -> Result<&GraphColors, String> { + if let Some(colors) = &self.raw_sat_colors { + Ok(colors) + } else { + Err("Satisfying colors not yet computed.".to_string()) + } + } +} + +impl InferenceSolver { + /// Prepares new "empty" `InferenceSolver` instance. + /// The computation is started by [start_computing] later. + pub fn new() -> InferenceSolver { + InferenceSolver { + bn: None, + graph: None, + static_props: None, + dynamic_props: None, + raw_intermediate_colors: None, + raw_sat_colors: None, + status_updates: vec![InferenceStatus::Created(SystemTime::now())], + } + } + + /// Partially process the sketch into individual components. + /// + /// WARNING: This is only a prototype, and considers just parts of the sketch that are easy to + /// process at the moment. Some parts are lost, including "dual regulations", some kinds of + /// static properties, all but generic dynamic properties. + fn process_inputs_prototype( + sketch: Sketch, + ) -> Result<(BooleanNetwork, Vec, Vec), String> { + // todo: at the moment we just use HCTL dynamic properties, and no static properties + let bn = sketch.model.to_bn(); + let static_properties = vec![]; + + let mut dynamic_properties = vec![]; + for (_, dyn_prop) in sketch.properties.dyn_props() { + if let DynPropertyType::GenericDynProp(prop) = dyn_prop.get_prop_data() { + dynamic_properties.push(prop.clone().processed_formula) + } + } + Ok((bn, static_properties, dynamic_properties)) + } + + /// Run the prototype version of the inference. + /// This wraps the [run_computation_prototype_inner] to also log potential errors. + /// + /// WARNING: This is only a prototype, and considers just parts of the sketch that are easy to + /// process at the moment. Some parts are lost, including "dual regulations", some kinds of + /// static properties, all but generic dynamic properties. + pub fn run_computation_prototype(&mut self, sketch: Sketch) -> Result { + let results = self.run_computation_prototype_inner(sketch); + if results.is_err() { + self.status_updates + .push(InferenceStatus::Error(SystemTime::now())); + } + results + } + + /// Run the prototype version of the inference. + /// + /// WARNING: This is only a prototype, and considers just parts of the sketch that are easy to + /// process at the moment. Some parts are lost, including "dual regulations", some kinds of + /// static properties, all but generic dynamic properties. + fn run_computation_prototype_inner( + &mut self, + sketch: Sketch, + ) -> Result { + let start_time = SystemTime::now(); + self.status_updates + .push(InferenceStatus::Started(start_time)); + + // step 1: process basic components of the sketch to be used + let (bn, static_props, dynamic_props) = Self::process_inputs_prototype(sketch)?; + self.bn = Some(bn); + self.static_props = Some(static_props); + self.dynamic_props = Some(dynamic_props); + self.status_updates + .push(InferenceStatus::ProcessedInputs(SystemTime::now())); + + // step 2: make default symbolic transition graph + self.graph = Some(SymbolicAsyncGraph::new(self.bn()?)?); + self.raw_intermediate_colors = Some(self.graph()?.mk_unit_colors()); + self.status_updates + .push(InferenceStatus::GeneratedGraph(SystemTime::now())); + + // step 3: todo: evaluate static properties, restrict colors + self.status_updates + .push(InferenceStatus::EvaluatedStatic(SystemTime::now())); + + // step 4: todo: evaluate dynamic properties, restrict colors + self.status_updates + .push(InferenceStatus::EvaluatedDynamic(SystemTime::now())); + + // step 5: process results, compute few statistics, return some results struct + let finish_time = SystemTime::now(); + self.raw_sat_colors = self.raw_intermediate_colors.clone(); + self.status_updates + .push(InferenceStatus::Finished(finish_time)); + + let num_sat_networks = self.sat_colors()?.approx_cardinality() as u64; + let total_time = finish_time.duration_since(start_time).unwrap(); + let results = AnalysisResults::new(num_sat_networks, total_time); + Ok(results) + } +} diff --git a/src-tauri/src/analysis/mod.rs b/src-tauri/src/analysis/mod.rs index 3a9e3f1..b683e24 100644 --- a/src-tauri/src/analysis/mod.rs +++ b/src-tauri/src/analysis/mod.rs @@ -1 +1,3 @@ +pub mod analysis_results; pub mod analysis_state; +mod inference_solver; diff --git a/src/aeon_events.ts b/src/aeon_events.ts index 8621d95..96d233c 100644 --- a/src/aeon_events.ts +++ b/src/aeon_events.ts @@ -486,14 +486,14 @@ export interface StatPropIdUpdateData { original_id: string, new_id: string } /** An object representing all information regarding inference analysis results. */ export interface InferenceResults { - numSatNetworks: number - computationTime: number + num_sat_networks: number + comp_time: number } /** An object representing all information regarding static check analysis results. */ export interface StaticCheckResults { - numSatNetworks: number - computationTime: number + num_sat_networks: number + comp_time: number } /** A function that is notified when a state value changes. */ diff --git a/src/html/component-analysis/analysis-component/analysis-component.ts b/src/html/component-analysis/analysis-component/analysis-component.ts index e199fce..cbc90c9 100644 --- a/src/html/component-analysis/analysis-component/analysis-component.ts +++ b/src/html/component-analysis/analysis-component/analysis-component.ts @@ -67,7 +67,7 @@ export default class AnalysisComponent extends LitElement { #onInferenceStarted (success: boolean): void { if (success) { - console.log('Inference analysis sucessfully started.') + console.log('DUMMY MESSAGE: Inference analysis sucessfully started.') } else { console.log('Error starting inference analysis.') } @@ -75,7 +75,7 @@ export default class AnalysisComponent extends LitElement { #onStaticCheckStarted (success: boolean): void { if (success) { - console.log('Static check analysis sucessfully started.') + console.log('DUMMY MESSAGE: Static check analysis sucessfully started.') } else { console.log('Error starting static check analysis.') } @@ -83,14 +83,14 @@ export default class AnalysisComponent extends LitElement { #onInferenceResultsReceived (results: InferenceResults): void { console.log('Received full inference results.') - console.log('-> There are ' + results.numSatNetworks + ' satisfying networks.') - console.log('-> The computation took ' + results.computationTime + ' seconds.') + console.log('-> There are ' + results.num_sat_networks + ' satisfying networks.') + console.log('-> The computation took ' + results.comp_time + ' seconds.') } #onStaticCheckResultsReceived (results: StaticCheckResults): void { console.log('Received static check results.') - console.log('-> There are ' + results.numSatNetworks + ' satisfying networks.') - console.log('-> The computation took ' + results.computationTime + ' seconds.') + console.log('-> There are ' + results.num_sat_networks + ' satisfying networks.') + console.log('-> The computation took ' + results.comp_time + ' seconds.') } private async confirmDialog (): Promise { From 99e54beffd1600d3e958f5e1fae6634db5bae48b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ond=C5=99ej=20Huvar?= <492849@mail.muni.cz> Date: Sun, 4 Aug 2024 21:37:46 +0200 Subject: [PATCH 6/8] Finish prototype inference pipeline and add network sampling. --- data/small_example.json | 186 +++++++++++++++ src-tauri/Cargo.toml | 6 +- src-tauri/src/algorithms/eval_dynamic/mod.rs | 3 + .../algorithms/eval_dynamic/template_eval.rs | 22 ++ src-tauri/src/algorithms/eval_static/mod.rs | 3 + .../algorithms/eval_static/template_eval.rs | 92 ++++++++ src-tauri/src/analysis/analysis_results.rs | 10 +- src-tauri/src/analysis/analysis_state.rs | 70 +++++- .../analysis/data_structs/_sampling_data.rs | 23 ++ src-tauri/src/analysis/data_structs/mod.rs | 4 + src-tauri/src/analysis/inference_solver.rs | 216 +++++++++++++----- src-tauri/src/analysis/mod.rs | 10 + src-tauri/src/analysis/sampling_networks.rs | 155 +++++++++++++ src-tauri/src/sketchbook/bn_utils.rs | 48 ++++ src-tauri/src/sketchbook/mod.rs | 2 + .../model/_model_state/_impl_convert_bn.rs | 78 +++++-- .../_model_state/_impl_convert_reg_graph.rs | 106 ++++----- src/aeon_events.ts | 29 ++- .../analysis-component/analysis-component.ts | 159 +++++++++++-- src/html/util/analysis-interfaces.ts | 4 + 20 files changed, 1061 insertions(+), 165 deletions(-) create mode 100644 data/small_example.json create mode 100644 src-tauri/src/algorithms/eval_dynamic/template_eval.rs create mode 100644 src-tauri/src/algorithms/eval_static/template_eval.rs create mode 100644 src-tauri/src/analysis/data_structs/_sampling_data.rs create mode 100644 src-tauri/src/analysis/data_structs/mod.rs create mode 100644 src-tauri/src/analysis/sampling_networks.rs create mode 100644 src-tauri/src/sketchbook/bn_utils.rs create mode 100644 src/html/util/analysis-interfaces.ts diff --git a/data/small_example.json b/data/small_example.json new file mode 100644 index 0000000..c0984a8 --- /dev/null +++ b/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 + } + ] +} \ No newline at end of file diff --git a/src-tauri/Cargo.toml b/src-tauri/Cargo.toml index cc196a4..60ed7bd 100644 --- a/src-tauri/Cargo.toml +++ b/src-tauri/Cargo.toml @@ -14,13 +14,15 @@ tauri-build = { version = "1.5", features = [] } biodivine-lib-bdd = ">=0.5.13, <1.0.0" biodivine-lib-param-bn = ">=0.5.10, <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" -chrono = "0.4.38" +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 diff --git a/src-tauri/src/algorithms/eval_dynamic/mod.rs b/src-tauri/src/algorithms/eval_dynamic/mod.rs index 70b786d..cf3cee1 100644 --- a/src-tauri/src/algorithms/eval_dynamic/mod.rs +++ b/src-tauri/src/algorithms/eval_dynamic/mod.rs @@ -1 +1,4 @@ // TODO + +/// Evaluate all template dynamic properties. +pub mod template_eval; diff --git a/src-tauri/src/algorithms/eval_dynamic/template_eval.rs b/src-tauri/src/algorithms/eval_dynamic/template_eval.rs new file mode 100644 index 0000000..a16e458 --- /dev/null +++ b/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 { + 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!(), + } +} diff --git a/src-tauri/src/algorithms/eval_static/mod.rs b/src-tauri/src/algorithms/eval_static/mod.rs index 70b786d..330f93e 100644 --- a/src-tauri/src/algorithms/eval_static/mod.rs +++ b/src-tauri/src/algorithms/eval_static/mod.rs @@ -1 +1,4 @@ // TODO + +/// Evaluate all template static properties. +pub mod template_eval; diff --git a/src-tauri/src/algorithms/eval_static/template_eval.rs b/src-tauri/src/algorithms/eval_static/template_eval.rs new file mode 100644 index 0000000..ef51c7a --- /dev/null +++ b/src-tauri/src/algorithms/eval_static/template_eval.rs @@ -0,0 +1,92 @@ +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, +) -> GraphColors { + // 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 = 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) + }; + GraphColors::new(observability.and(unit_bdd), context) + } + 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!(), + }; + GraphColors::new(monotonicity.and(unit_bdd), context) + } + StatPropertyType::RegulationMonotonicContext(_prop) => todo!(), + StatPropertyType::FnInputEssentialContext(_prop) => todo!(), + StatPropertyType::FnInputMonotonic(_prop) => todo!(), + StatPropertyType::FnInputMonotonicContext(_prop) => todo!(), + } +} diff --git a/src-tauri/src/analysis/analysis_results.rs b/src-tauri/src/analysis/analysis_results.rs index e2c2a35..8e8a296 100644 --- a/src-tauri/src/analysis/analysis_results.rs +++ b/src-tauri/src/analysis/analysis_results.rs @@ -11,16 +11,24 @@ pub struct AnalysisResults { 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) -> AnalysisResults { + 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); + } } diff --git a/src-tauri/src/analysis/analysis_state.rs b/src-tauri/src/analysis/analysis_state.rs index 9ca0501..9679093 100644 --- a/src-tauri/src/analysis/analysis_state.rs +++ b/src-tauri/src/analysis/analysis_state.rs @@ -1,28 +1,30 @@ use crate::analysis::analysis_results::AnalysisResults; +use crate::analysis::data_structs::SamplingData; use crate::analysis::inference_solver::InferenceSolver; +use crate::analysis::sampling_networks::download_witnesses; use crate::app::event::Event; use crate::app::state::{Consumed, SessionHelper, SessionState}; -use crate::app::DynError; +use crate::app::{AeonError, DynError}; use crate::debug; use crate::sketchbook::data_structs::SketchData; use crate::sketchbook::{JsonSerde, Sketch}; -use serde::{Deserialize, Serialize}; -/// Object encompassing all of the state components of the Analysis itself that are exchanged -/// with frontend (no raw low-level structures like symbolic graph or its colors) -#[derive(Clone, Debug, PartialEq, Serialize, Deserialize)] +/// Object encompassing all of the components of the Analysis itself +/// That inludes boths the components that are exchanged with frontend +/// and also raw low-level structures like symbolic graph or its colors. +#[derive(Clone)] pub struct AnalysisState { /// Boolean network sketch to run the analysis on. Can be a placeholder at the beginning. sketch: Sketch, /// Flag signalling that the actual sketch data were received from editor session. sketch_received: bool, + /// Potential analysis solver instance. + solver: Option, /// Potential results of the analysis. results: Option, // TODO } -impl<'de> JsonSerde<'de> for AnalysisState {} - impl AnalysisState { /// Create new `AnalysisState` with an empty placeholder sketch. /// @@ -32,6 +34,7 @@ impl AnalysisState { AnalysisState { sketch: Sketch::default(), sketch_received: false, + solver: None, results: None, } } @@ -41,10 +44,17 @@ impl AnalysisState { AnalysisState { sketch, sketch_received: true, + solver: None, results: None, } } + /// Reset the results and analyses of this `AnalysisState`. + /// The sketch data stays the same. + pub fn reset(&mut self) { + self.results = None; + } + /// Update the sketch data of this `AnalysisState`. pub fn set_sketch(&mut self, sketch: Sketch) { self.sketch = sketch; @@ -67,10 +77,17 @@ impl SessionState for AnalysisState { Some(&"run_inference") => { Self::assert_payload_empty(event, component)?; debug!("Event `run_inference` received. It is not fully implemented yet."); - // TODO - let mut inference_solver = InferenceSolver::new(); - let results = inference_solver.run_computation_prototype(self.sketch.clone())?; + if !self.sketch_received || self.sketch.model.num_vars() == 0 { + return AeonError::throw("Cannot run analysis on empty sketch."); + } + + self.solver = Some(InferenceSolver::new()); + let results = self + .solver + .as_mut() + .unwrap() + .run_computation_prototype(self.sketch.clone())?; let payload = results.to_json_str(); let state_change = Event::build(&["analysis", "inference_results"], Some(&payload)); @@ -81,7 +98,8 @@ impl SessionState for AnalysisState { } Some(&"run_static") => { Self::assert_payload_empty(event, component)?; - debug!("Event `run_static` received. It is not implemented at the moment. Only dummy message will be sent"); + debug!("Event `run_static` received. It is not implemented at the moment. Only dummy message will be sent back."); + // TODO let state_change = Event::build(&["analysis", "static_running"], Some("true")); @@ -90,6 +108,36 @@ impl SessionState for AnalysisState { reset: true, }) } + Some(&"reset_analysis") => { + Self::assert_payload_empty(event, component)?; + + self.reset(); + + let state_change = Event::build(&["analysis", "analysis_reset"], Some("true")); + Ok(Consumed::Irreversible { + state_change, + reset: true, + }) + } + Some(&"sample_networks") => { + let payload = Self::clone_payload_str(event, component)?; + let sampling_data = SamplingData::from_json_str(&payload)?; + + if let Some(solver) = &self.solver { + download_witnesses( + &sampling_data.path, + solver.sat_colors()?.clone(), + solver.graph()?, + sampling_data.count, + sampling_data.seed, + )?; + Ok(Consumed::NoChange {}) + } else { + AeonError::throw( + "Cannot sample networks because there are no inference results.", + ) + } + } _ => Self::invalid_path_error_generic(at_path), } } diff --git a/src-tauri/src/analysis/data_structs/_sampling_data.rs b/src-tauri/src/analysis/data_structs/_sampling_data.rs new file mode 100644 index 0000000..d285241 --- /dev/null +++ b/src-tauri/src/analysis/data_structs/_sampling_data.rs @@ -0,0 +1,23 @@ +use crate::sketchbook::JsonSerde; +use serde::{Deserialize, Serialize}; + +/// Structure for receiving data about network sampling details from the frontend. +#[derive(Clone, Debug, Serialize, Deserialize)] +pub struct SamplingData { + pub count: usize, + pub seed: Option, + pub path: String, +} + +impl<'de> JsonSerde<'de> for SamplingData {} + +impl SamplingData { + /// Create new `SamplingData` object given all its fields. + pub fn new(count: usize, seed: Option, path: &str) -> SamplingData { + SamplingData { + count, + seed, + path: path.to_string(), + } + } +} diff --git a/src-tauri/src/analysis/data_structs/mod.rs b/src-tauri/src/analysis/data_structs/mod.rs new file mode 100644 index 0000000..1ea0dc5 --- /dev/null +++ b/src-tauri/src/analysis/data_structs/mod.rs @@ -0,0 +1,4 @@ +/// **(internal)** Definition and utility methods for `SamplingData`. +mod _sampling_data; + +pub use _sampling_data::SamplingData; diff --git a/src-tauri/src/analysis/inference_solver.rs b/src-tauri/src/analysis/inference_solver.rs index 2b9a828..bd043cd 100644 --- a/src-tauri/src/analysis/inference_solver.rs +++ b/src-tauri/src/analysis/inference_solver.rs @@ -1,22 +1,25 @@ +use crate::algorithms::eval_dynamic::template_eval::eval_dyn_prop; +use crate::algorithms::eval_static::template_eval::eval_static_prop; use crate::analysis::analysis_results::AnalysisResults; -use crate::sketchbook::properties::dynamic_props::DynPropertyType; -use crate::sketchbook::properties::{FirstOrderFormula, HctlFormula}; +use crate::log; +use crate::sketchbook::properties::{DynProperty, StatProperty}; use crate::sketchbook::Sketch; +use biodivine_hctl_model_checker::mc_utils::get_extended_symbolic_graph; use biodivine_lib_param_bn::symbolic_async_graph::{GraphColors, SymbolicAsyncGraph}; use biodivine_lib_param_bn::BooleanNetwork; use std::time::SystemTime; /// Status of the computation, together with a timestamp. -#[derive(Clone)] +#[derive(Clone, Debug)] pub enum InferenceStatus { - Created(SystemTime), - Started(SystemTime), - ProcessedInputs(SystemTime), - GeneratedGraph(SystemTime), - EvaluatedStatic(SystemTime), - EvaluatedDynamic(SystemTime), - Finished(SystemTime), - Error(SystemTime), + Created, + Started, + ProcessedInputs, + GeneratedGraph, + EvaluatedStatic, + EvaluatedDynamic, + Finished, + Error, } /// Object encompassing the process of the full BN inference. @@ -32,21 +35,22 @@ pub struct InferenceSolver { /// Boolean Network instance. bn: Option, /// Symbolic transition graph for the system. + /// Its set of unit colors is gradually updated during computation, and it consists of + /// currently remaining valid candidate colors. graph: Option, - /// Static properties converted to FO logic. - static_props: Option>, - /// Dynamic properties converted to HCTL. - dynamic_props: Option>, - /// Intermediate set of candidate colors, gradually updated during computation. - raw_intermediate_colors: Option, + /// Static properties. + static_props: Option>, + /// Dynamic properties. + dynamic_props: Option>, /// Set of final satisfying colors (once computed). raw_sat_colors: Option, /// Vector with all time-stamped status updates. The last is the latest status. - status_updates: Vec, + status_updates: Vec<(InferenceStatus, SystemTime)>, } impl InferenceSolver { - fn bn(&self) -> Result<&BooleanNetwork, String> { + /// Reference getter for a Boolean network. + pub fn bn(&self) -> Result<&BooleanNetwork, String> { if let Some(bn) = &self.bn { Ok(bn) } else { @@ -54,7 +58,8 @@ impl InferenceSolver { } } - fn graph(&self) -> Result<&SymbolicAsyncGraph, String> { + /// Reference getter for a transition graph. + pub fn graph(&self) -> Result<&SymbolicAsyncGraph, String> { if let Some(graph) = &self.graph { Ok(graph) } else { @@ -62,13 +67,74 @@ impl InferenceSolver { } } - fn sat_colors(&self) -> Result<&GraphColors, String> { + /// Reference getter for a vector of formulas for static properties. + pub fn stat_props(&self) -> Result<&Vec, String> { + if let Some(stat_props) = &self.static_props { + Ok(stat_props) + } else { + Err("Static properties not yet processed.".to_string()) + } + } + + /// Reference getter for a vector of formulas for dynamic properties. + pub fn dyn_props(&self) -> Result<&Vec, String> { + if let Some(dyn_props) = &self.dynamic_props { + Ok(dyn_props) + } else { + Err("Dynamic properties not yet processed.".to_string()) + } + } + + /// Reference getter for a set with satisfying graph colors. + pub fn sat_colors(&self) -> Result<&GraphColors, String> { if let Some(colors) = &self.raw_sat_colors { Ok(colors) } else { Err("Satisfying colors not yet computed.".to_string()) } } + + /// Get a current set of valid candidate colors. + /// This is gradually updated during computation. + pub fn current_candidate_colors(&self) -> Result { + Ok(self.graph()?.mk_unit_colors()) + } + + fn status_update(&mut self, status: InferenceStatus) { + let now = SystemTime::now(); + self.status_updates.push((status.clone(), now)); + + let start_time = self.start_time().unwrap(); + let duration_since_start = now.duration_since(start_time).unwrap(); + log!( + "0", + "Inference status update: {:?}, {}s", + status, + duration_since_start.as_secs() + ); + } + + /// Getter for a start time of the actual computation. + pub fn start_time(&self) -> Result { + if self.status_updates.len() > 1 { + Ok(self.status_updates[1].1) + } else { + Err("Computation not yet started.".to_string()) + } + } + + /// Getter for a finish time of the actual computation. + pub fn finish_time(&self) -> Result { + // there is always some status (since one is given during initialization) + let (last_status, last_time) = self.status_updates.last().unwrap(); + if let InferenceStatus::Finished = last_status { + Ok(*last_time) + } else if let InferenceStatus::Error = last_status { + Err("Computation failed to finish.".to_string()) + } else { + Err("Computation not yet finished.".to_string()) + } + } } impl InferenceSolver { @@ -80,29 +146,25 @@ impl InferenceSolver { graph: None, static_props: None, dynamic_props: None, - raw_intermediate_colors: None, raw_sat_colors: None, - status_updates: vec![InferenceStatus::Created(SystemTime::now())], + status_updates: vec![(InferenceStatus::Created, SystemTime::now())], } } - /// Partially process the sketch into individual components. - /// - /// WARNING: This is only a prototype, and considers just parts of the sketch that are easy to - /// process at the moment. Some parts are lost, including "dual regulations", some kinds of - /// static properties, all but generic dynamic properties. - fn process_inputs_prototype( + /// Extract and convert relevant components from the sketch (boolean network, properties). + fn extract_inputs( sketch: Sketch, - ) -> Result<(BooleanNetwork, Vec, Vec), String> { - // todo: at the moment we just use HCTL dynamic properties, and no static properties - let bn = sketch.model.to_bn(); - let static_properties = vec![]; + ) -> Result<(BooleanNetwork, Vec, Vec), String> { + // todo: at the moment we just use HCTL dynamic properties, and all static properties + let bn = sketch.model.to_bn_with_plain_regulations(); + let mut static_properties = vec![]; + for (_, stat_prop) in sketch.properties.stat_props() { + static_properties.push(stat_prop.clone()); + } let mut dynamic_properties = vec![]; for (_, dyn_prop) in sketch.properties.dyn_props() { - if let DynPropertyType::GenericDynProp(prop) = dyn_prop.get_prop_data() { - dynamic_properties.push(prop.clone().processed_formula) - } + dynamic_properties.push(dyn_prop.clone()); } Ok((bn, static_properties, dynamic_properties)) } @@ -116,8 +178,7 @@ impl InferenceSolver { pub fn run_computation_prototype(&mut self, sketch: Sketch) -> Result { let results = self.run_computation_prototype_inner(sketch); if results.is_err() { - self.status_updates - .push(InferenceStatus::Error(SystemTime::now())); + self.status_update(InferenceStatus::Error); } results } @@ -131,41 +192,74 @@ impl InferenceSolver { &mut self, sketch: Sketch, ) -> Result { - let start_time = SystemTime::now(); - self.status_updates - .push(InferenceStatus::Started(start_time)); + let mut metadata = String::new(); + self.status_update(InferenceStatus::Started); // step 1: process basic components of the sketch to be used - let (bn, static_props, dynamic_props) = Self::process_inputs_prototype(sketch)?; + let (bn, static_props, dynamic_props) = Self::extract_inputs(sketch)?; self.bn = Some(bn); self.static_props = Some(static_props); self.dynamic_props = Some(dynamic_props); - self.status_updates - .push(InferenceStatus::ProcessedInputs(SystemTime::now())); + self.status_update(InferenceStatus::ProcessedInputs); + + // step 2: todo: check how many HCTL propositions we need to eval the formulae + let num_hctl_vars = 3; - // step 2: make default symbolic transition graph - self.graph = Some(SymbolicAsyncGraph::new(self.bn()?)?); - self.raw_intermediate_colors = Some(self.graph()?.mk_unit_colors()); - self.status_updates - .push(InferenceStatus::GeneratedGraph(SystemTime::now())); + // step 3: make default symbolic transition graph + self.graph = Some(get_extended_symbolic_graph(self.bn()?, num_hctl_vars)?); + self.status_update(InferenceStatus::GeneratedGraph); + let msg = format!( + "After graph generating: {}\n", + self.current_candidate_colors()?.approx_cardinality() + ); + metadata.push_str(&msg); - // step 3: todo: evaluate static properties, restrict colors - self.status_updates - .push(InferenceStatus::EvaluatedStatic(SystemTime::now())); + // step 4: todo: evaluate static properties, restrict colors + for stat_property in self.stat_props()?.clone() { + let inferred_colors = eval_static_prop(stat_property, self.bn()?, self.graph()?); - // step 4: todo: evaluate dynamic properties, restrict colors - self.status_updates - .push(InferenceStatus::EvaluatedDynamic(SystemTime::now())); + let new_graph: SymbolicAsyncGraph = SymbolicAsyncGraph::with_custom_context( + self.graph()?.as_network().unwrap(), + self.graph()?.symbolic_context().clone(), + inferred_colors.as_bdd().clone(), + )?; + self.graph = Some(new_graph); + } + self.status_update(InferenceStatus::EvaluatedStatic); + let msg = format!( + "After static props: {}\n", + self.current_candidate_colors()?.approx_cardinality() + ); + metadata.push_str(&msg); + + // step 5: todo: evaluate dynamic properties, restrict colors + for dyn_property in self.dyn_props()?.clone() { + let inferred_colors = eval_dyn_prop(dyn_property, self.graph()?)?; + + let new_graph: SymbolicAsyncGraph = SymbolicAsyncGraph::with_custom_context( + self.graph()?.as_network().unwrap(), + self.graph()?.symbolic_context().clone(), + inferred_colors.as_bdd().clone(), + )?; + self.graph = Some(new_graph); + } + self.status_update(InferenceStatus::EvaluatedDynamic); + let msg = format!( + "After dynamic props: {}\n", + self.current_candidate_colors()?.approx_cardinality() + ); + metadata.push_str(&msg); // step 5: process results, compute few statistics, return some results struct - let finish_time = SystemTime::now(); - self.raw_sat_colors = self.raw_intermediate_colors.clone(); - self.status_updates - .push(InferenceStatus::Finished(finish_time)); + self.raw_sat_colors = Some(self.graph()?.mk_unit_colors()); + self.status_update(InferenceStatus::Finished); let num_sat_networks = self.sat_colors()?.approx_cardinality() as u64; - let total_time = finish_time.duration_since(start_time).unwrap(); - let results = AnalysisResults::new(num_sat_networks, total_time); + let total_time = self + .finish_time()? + .duration_since(self.start_time()?) + .unwrap(); + let results = AnalysisResults::new(num_sat_networks, total_time, &metadata); Ok(results) } } diff --git a/src-tauri/src/analysis/mod.rs b/src-tauri/src/analysis/mod.rs index b683e24..d5d7bb0 100644 --- a/src-tauri/src/analysis/mod.rs +++ b/src-tauri/src/analysis/mod.rs @@ -1,3 +1,13 @@ +/// Structures and utilities to track results of analysis. pub mod analysis_results; +/// Structures and utilities to track the whole state of analysis. pub mod analysis_state; +/// Structs and utility methods that can be used for communication with frontend. +pub mod data_structs; + +/// Structures and methods to run the whole inference process. +/// This involves the general workflow, the details are in a separate module [analysis]. mod inference_solver; +/// Utilities to sample and download networks. +/// Some functionality is taken from our repository [biodivine-bn-classifier]. +mod sampling_networks; diff --git a/src-tauri/src/analysis/sampling_networks.rs b/src-tauri/src/analysis/sampling_networks.rs new file mode 100644 index 0000000..b642024 --- /dev/null +++ b/src-tauri/src/analysis/sampling_networks.rs @@ -0,0 +1,155 @@ +use biodivine_lib_bdd::BddPartialValuation; +use biodivine_lib_param_bn::biodivine_std::traits::Set; +use biodivine_lib_param_bn::symbolic_async_graph::{GraphColors, SymbolicAsyncGraph}; + +use rand::prelude::StdRng; +use rand::SeedableRng; +use std::fs::File; +use std::io::Write; +use std::path::Path; +use zip::write::{FileOptions, ZipWriter}; + +/// Randomly select a color from the given set of colors. +/// This is a workaround that should be modified in the future. +pub fn pick_random_color( + rng: &mut StdRng, + graph: &SymbolicAsyncGraph, + color_set: &GraphColors, +) -> GraphColors { + let ctx = graph.symbolic_context(); + let random_witness = color_set.as_bdd().random_valuation(rng).unwrap(); + let mut partial_valuation = BddPartialValuation::empty(); + for var in ctx.parameter_variables() { + partial_valuation.set_value(*var, random_witness[*var]); + } + let singleton_bdd = ctx + .bdd_variable_set() + .mk_conjunctive_clause(&partial_valuation); + // We can use the "raw copy" function because into the new BDD, we only carried over + // the BDD variables that encode network parameters. + color_set.copy(singleton_bdd) +} + +pub fn download_witnesses( + path: &str, + mut color_set: GraphColors, + graph: &SymbolicAsyncGraph, + witness_count: usize, + seed: Option, +) -> Result<(), String> { + // Prepare the archive first + let archive_path = Path::new(path); + // If there are some non existing dirs in path, create them. + let prefix = archive_path.parent().unwrap(); + std::fs::create_dir_all(prefix).map_err(|e| format!("{e:?}"))?; + // Create a zip writer for the desired archive. + let archive = File::create(archive_path).map_err(|e| format!("{e:?}"))?; + let mut zip_writer = ZipWriter::new(archive); + + let mut i = 0; + let mut random_state: Option = seed.map(StdRng::seed_from_u64); + + // collect `num_witnesses` networks + while i < witness_count && !color_set.is_empty() { + // get singleton color for the witness + let witness_color = if let Some(std_rng) = random_state.as_mut() { + // For random networks, we need to be a bit more creative... (although, support for + // this in lib-param-bn would be nice). + pick_random_color(std_rng, graph, &color_set) + } else { + // The `SymbolicAsyncGraph::pick_singleton` should be deterministic. + color_set.pick_singleton() + }; + assert!(witness_color.is_singleton()); + + // remove the color from the set + color_set = color_set.minus(&witness_color); + i += 1; + + // Write the network into the zip. + let file_content = graph.pick_witness(&witness_color).to_string(); + zip_writer + .start_file(format!("witness_{i}.aeon"), FileOptions::default()) + .map_err(|e| format!("{e:?}"))?; + writeln!(zip_writer, "{file_content}").map_err(|e| format!("{e:?}"))?; + } + + zip_writer.finish().map_err(|e| format!("{e:?}"))?; + Ok(()) +} + +/* +pub fn save_file(path: &str, content: &str) -> Result<(), String> { + std::fs::write(path, content).map_err(|e| format!("{e:?}")) +} + +/// Create a zip archive containing multiple AEON witness networks. +pub fn save_zip_archive(path: &str, list_file_contents: Vec<&str>) -> Result<(), String> { + // Prepare the archive first + let archive_path = Path::new(path); + // If there are some non existing dirs in path, create them. + let prefix = archive_path.parent().unwrap(); + std::fs::create_dir_all(prefix).map_err(|e| format!("{e:?}"))?; + // Create a zip writer for the desired archive. + let archive = File::create(archive_path).map_err(|e| format!("{e:?}"))?; + let mut zip_writer = ZipWriter::new(archive); + + for (i, file_content) in list_file_contents.iter().enumerate() { + zip_writer + .start_file(format!("witness_{i}.aeon"), FileOptions::default()) + .map_err(|e| format!("{e:?}"))?; + writeln!(zip_writer, "{file_content}").map_err(|e| format!("{e:?}"))?; + } + + zip_writer.finish().map_err(|e| format!("{e:?}"))?; + Ok(()) +} + +/// Wrapper to only get a single witness +pub fn get_witness( + graph: &SymbolicAsyncGraph, + std_rng: &mut StdRng, + color_set: GraphColors, + randomize: bool, +) -> Result { + let singleton_witness = + get_n_witnesses(graph, std_rng, color_set, 1, randomize)?; + assert_eq!(singleton_witness.len(), 1); + Ok(singleton_witness.into_iter().next().unwrap()) +} + +pub fn get_n_witnesses( + graph: &SymbolicAsyncGraph, + std_rng: &mut StdRng, + mut color_set: GraphColors, + num_witnesses: i32, + randomize: bool, +) -> Result, String> { + let mut witnesses_bns: Vec = Vec::new(); + let mut i = 0; + + // just to make it explicit (this condition is also checked before this function is called) + assert!((num_witnesses as f64) <= color_set.approx_cardinality()); + + // collect `num_witnesses` networks + while i < num_witnesses && !color_set.is_empty() { + // get singleton color for the witness + let witness_color = if !randomize { + // The `SymbolicAsyncGraph::pick_singleton` should be deterministic. + color_set.pick_singleton() + } else { + // For random networks, we need to be a bit more creative... (although, support for + // this in lib-param-bn would be nice). + pick_random_color(std_rng, &graph, &color_set) + }; + assert!(witness_color.is_singleton()); + witnesses_bns.push(graph.pick_witness(&witness_color)); + + // remove the color from the set + color_set = color_set.minus(&witness_color); + i += 1; + } + + Ok(witnesses_bns.into_iter().map(|it| it.to_string()).collect()) +} +*/ diff --git a/src-tauri/src/sketchbook/bn_utils.rs b/src-tauri/src/sketchbook/bn_utils.rs new file mode 100644 index 0000000..df58feb --- /dev/null +++ b/src-tauri/src/sketchbook/bn_utils.rs @@ -0,0 +1,48 @@ +use crate::sketchbook::model::{Essentiality, Monotonicity}; +use biodivine_lib_param_bn::Monotonicity as Lib_Pbn_Monotonicity; + +/// **(internal)** Static utility method to convert regulation sign given by `Monotonicity` +/// used by `lib_param_bn` into the type `Monotonicity` used here. +/// TODO: note that `lib-param-bn` currently cannot express `Dual` variant of `Monotonicity`. +pub fn sign_from_monotonicity(monotonicity: Option) -> Monotonicity { + match monotonicity { + Some(m) => match m { + Lib_Pbn_Monotonicity::Activation => Monotonicity::Activation, + Lib_Pbn_Monotonicity::Inhibition => Monotonicity::Inhibition, + }, + None => Monotonicity::Unknown, + } +} + +/// **(internal)** Static utility method to convert regulation sign from the type +/// `Monotonicity` used here into the type `Monotonicity` used in `lib_param_bn`. +/// TODO: note that `lib-param-bn` currently cannot express `Dual` variant of `Monotonicity` and `Unknown` is used instead. +pub fn sign_to_monotonicity(regulation_sign: &Monotonicity) -> Option { + match regulation_sign { + Monotonicity::Activation => Some(Lib_Pbn_Monotonicity::Activation), + Monotonicity::Inhibition => Some(Lib_Pbn_Monotonicity::Inhibition), + Monotonicity::Unknown => None, + // todo: fix + Monotonicity::Dual => None, + } +} + +/// **(internal)** Static utility method to convert `Essentiality` from boolean. +/// TODO: note that `lib-param-bn` currently cannot distinguish between `False` and `Unknown` variants of `Essentiality`. +pub fn essentiality_from_bool(essentiality: bool) -> Essentiality { + match essentiality { + true => Essentiality::True, + // todo: fix, this is how it works now in `lib-param-bn` + false => Essentiality::Unknown, + } +} + +/// **(internal)** Static utility method to convert `Essentiality` to boolean. +/// TODO: note that `lib-param-bn` currently cannot distinguish between `False` and `Unknown` variants of `Essentiality`. +pub fn essentiality_to_bool(essentiality: Essentiality) -> bool { + match essentiality { + Essentiality::True => true, + Essentiality::Unknown => false, + Essentiality::False => false, + } +} diff --git a/src-tauri/src/sketchbook/mod.rs b/src-tauri/src/sketchbook/mod.rs index 3b8cc40..8f75f12 100644 --- a/src-tauri/src/sketchbook/mod.rs +++ b/src-tauri/src/sketchbook/mod.rs @@ -17,6 +17,8 @@ pub mod observations; /// Classes and utility methods regarding properties. #[macro_use] pub mod properties; +/// Utilities regarding conversion of BN components and similar. +pub mod bn_utils; /// The main `Sketch` manager object and its utilities. mod _sketch; diff --git a/src-tauri/src/sketchbook/model/_model_state/_impl_convert_bn.rs b/src-tauri/src/sketchbook/model/_model_state/_impl_convert_bn.rs index 9f07795..e0bb26c 100644 --- a/src-tauri/src/sketchbook/model/_model_state/_impl_convert_bn.rs +++ b/src-tauri/src/sketchbook/model/_model_state/_impl_convert_bn.rs @@ -3,25 +3,61 @@ use biodivine_lib_param_bn::{BooleanNetwork, RegulatoryGraph}; /// Methods for converting between `ModelState` and `BooleanNetwork` (from the `lib-param-bn`). impl ModelState { + /// Internal function to convert the `ModelState` into a variant of `BooleanNetwork` with + /// specified information to be included. + /// + /// By default, all variables and regulations are included. You can choose the following: + /// - `regulation_types`: include types of regulations + /// - `parameters`: include all parameters for uninterpreted functions + /// - `update_fns`: include all update functions + /// + /// It is up to you to make the selection reasonable (e.g., when including update functions + /// that contain parameters, you must also include parameters, and so on...). + fn to_bn_with_options( + &self, + regulation_types: bool, + parameters: bool, + update_fns: bool, + ) -> Result { + let reg_graph = if regulation_types { + self.to_reg_graph() + } else { + self.to_reg_graph_with_unspecified_regs() + }; + let mut bn = BooleanNetwork::new(reg_graph); + + if parameters { + for (fn_id, uninterpreted_fn) in self.uninterpreted_fns.iter() { + // uninterpreted fns always have unique valid IDs, so we can unwrap + bn.add_parameter(fn_id.as_str(), uninterpreted_fn.get_arity() as u32) + .unwrap(); + } + } + + if update_fns { + for (var_id, update_fn) in self.update_fns.iter() { + if !update_fn.is_unspecified() { + bn.add_string_update_function(var_id.as_str(), update_fn.get_fn_expression())?; + } + } + } + Ok(bn) + } + /// Convert the `ModelState` into the corresponding "default" `BooleanNetwork` object. /// The resulting BN covers the variables and regulations, but it has empty update functions, - /// and does not cover parameters. + /// and does not cover any parameters. pub fn to_empty_bn(&self) -> BooleanNetwork { - let reg_graph = self.to_reg_graph(); - BooleanNetwork::new(reg_graph) + // this is a safe combination that cannot result in errors + self.to_bn_with_options(true, false, false).unwrap() } /// Convert the `ModelState` into the corresponding "default" `BooleanNetwork` object with added /// parameters. /// The resulting BN covers the variables, parameters, and regulations, but it has empty update functions. pub fn to_empty_bn_with_params(&self) -> BooleanNetwork { - let mut bn = self.to_empty_bn(); - for (fn_id, uninterpreted_fn) in self.uninterpreted_fns.iter() { - // uninterpreted fns always have unique valid IDs, so we can unwrap - bn.add_parameter(fn_id.as_str(), uninterpreted_fn.get_arity() as u32) - .unwrap(); - } - bn + // this is a safe combination that cannot result in errors + self.to_bn_with_options(true, true, false).unwrap() } /// Generate a `BooleanNetwork` with a only given number of "placeholder" (fake) variables. @@ -52,15 +88,19 @@ impl ModelState { /// Note that currently the `BooleanNetwork` class does not support all features of the `ModelState` (such as /// various regulation types or details of uninterpreted functions) -- these will be lost during the conversion. pub fn to_bn(&self) -> BooleanNetwork { - let mut bn = self.to_empty_bn_with_params(); - for (var_id, update_fn) in self.update_fns.iter() { - if !update_fn.is_unspecified() { - // var_id is surely a valid variable, we can safely unwrap - bn.add_string_update_function(var_id.as_str(), update_fn.get_fn_expression()) - .unwrap(); - } - } - bn + // this is a safe combination that cannot result in errors + self.to_bn_with_options(true, true, true).unwrap() + } + + /// Convert the `ModelState` into the corresponding `BooleanNetwork` object (that will contain all of the + /// variables, (plain) regulations, update functions, and uninterpreted functions). However, + /// the types of regulations (both monotonicity and essentiality) are ignored, and instead used as + /// unspecified. + /// + /// This might be useful if we want to process regulation types later via static properties. + pub fn to_bn_with_plain_regulations(&self) -> BooleanNetwork { + // this is a safe combination that cannot result in errors + self.to_bn_with_options(false, true, true).unwrap() } } diff --git a/src-tauri/src/sketchbook/model/_model_state/_impl_convert_reg_graph.rs b/src-tauri/src/sketchbook/model/_model_state/_impl_convert_reg_graph.rs index 113df8c..ff50188 100644 --- a/src-tauri/src/sketchbook/model/_model_state/_impl_convert_reg_graph.rs +++ b/src-tauri/src/sketchbook/model/_model_state/_impl_convert_reg_graph.rs @@ -1,22 +1,44 @@ +use crate::sketchbook::bn_utils; use crate::sketchbook::ids::VarId; -use crate::sketchbook::model::{Essentiality, ModelState, Monotonicity}; -use biodivine_lib_param_bn::Monotonicity as Lib_Pbn_Monotonicity; +use crate::sketchbook::model::ModelState; use biodivine_lib_param_bn::RegulatoryGraph; /// Methods for converting between `ModelState` and `RegulatoryGraph` (from the `lib-param-bn`). impl ModelState { - /// Convert the `ModelState` (the current state of the regulation graph) into the - /// corresponding `RegulatoryGraph` object. Sorted variable IDs of the `ModelState` are - /// used for variable names in `RegulatoryGraph`. + /// Extract the regulatory graph (`RegulatoryGraph` object) from the `ModelState`. + /// Sorted variable IDs of the `ModelState` are used for variable names in `RegulatoryGraph`. /// /// The conversion might loose some information, as the `RegulatoryGraph` does not support - /// all the variants of `Monotonicity` and `Essentiality`. See also [ModelState::sign_to_monotonicity]. + /// all the variants of `Monotonicity` and `Essentiality`. See also [bn_utils::sign_to_monotonicity]. /// /// Note that we can convert the resulting `RegulatoryGraph` back, but the conversion loses /// some information, like the original variable names and layout information. /// Also, all of the other model components, such as `update functions` or `uninterpreted functions` /// are not part of the `RegulatoryGraph`. pub fn to_reg_graph(&self) -> RegulatoryGraph { + self._to_reg_graph(true) + } + + /// Extract the regulatory graph (`RegulatoryGraph` object) from the `ModelState`. + /// Sorted variable IDs of the `ModelState` are used for variable names in `RegulatoryGraph`. + /// + /// The types of regulations (their essentiality and monotonicity) are ignored, and unspecified + /// versions are used instead. + /// + /// This might be useful in inference, if we want to process regulation types later via static + /// properties. + pub fn to_reg_graph_with_unspecified_regs(&self) -> RegulatoryGraph { + self._to_reg_graph(false) + } + + /// Internal utility to extract the regulatory graph (`RegulatoryGraph` object) from the + /// `ModelState`. Sorted variable IDs of the `ModelState` are used for variable names in + /// `RegulatoryGraph`. + /// + /// There are two modes based on `include_reg_types` argument. If it is set to `true`, the + /// types of regulations (their essentiality and monotonicity) are preserved. If it is set to + /// `false`, they are ignored, and unspecified versions are used instead. + fn _to_reg_graph(&self, include_reg_types: bool) -> RegulatoryGraph { // create `RegulatoryGraph` from a list of variable ID strings (these are unique and // can be mapped back) let mut variable_vec = self @@ -31,15 +53,29 @@ impl ModelState { // regulations for r in self.regulations() { - reg_graph - .add_regulation( - r.get_regulator().as_str(), - r.get_target().as_str(), - r.is_essential(), - ModelState::sign_to_monotonicity(r.get_sign()), - ) - .unwrap(); - // we can use unwrap, cause the regulation will always be unique and correctly added + if include_reg_types { + // add the regulation with its original monotonicity and essentiality (as far as conversion allows) + reg_graph + .add_regulation( + r.get_regulator().as_str(), + r.get_target().as_str(), + r.is_essential(), + bn_utils::sign_to_monotonicity(r.get_sign()), + ) + .unwrap(); + // we can use unwrap, cause the regulation is ensured to be unique and correctly added + } else { + // add the regulation unspecified monotonicity and essentiality + reg_graph + .add_regulation( + r.get_regulator().as_str(), + r.get_target().as_str(), + false, + None, + ) + .unwrap(); + // we can use unwrap, cause the regulation is ensured to be unique and correctly added + } } reg_graph } @@ -66,48 +102,12 @@ impl ModelState { model.add_regulation( VarId::new(name_regulator.as_str())?, VarId::new(name_target.as_str())?, - ModelState::essentiality_from_bool(r.is_observable()), - ModelState::sign_from_monotonicity(r.get_monotonicity()), + bn_utils::essentiality_from_bool(r.is_observable()), + bn_utils::sign_from_monotonicity(r.get_monotonicity()), )?; } Ok(model) } - - /// **(internal)** Static utility method to convert regulation sign given by `Monotonicity` - /// used by `lib_param_bn` into the type `Monotonicity` used here. - /// TODO: note that `lib-param-bn` currently cannot express `Dual` variant of `Monotonicity`. - fn sign_from_monotonicity(monotonicity: Option) -> Monotonicity { - match monotonicity { - Some(m) => match m { - Lib_Pbn_Monotonicity::Activation => Monotonicity::Activation, - Lib_Pbn_Monotonicity::Inhibition => Monotonicity::Inhibition, - }, - None => Monotonicity::Unknown, - } - } - - /// **(internal)** Static utility method to convert regulation sign from the type - /// `Monotonicity` used here into the type `Monotonicity` used in `lib_param_bn`. - /// TODO: note that `lib-param-bn` currently cannot express `Dual` variant of `Monotonicity` and `Unknown` is used instead. - fn sign_to_monotonicity(regulation_sign: &Monotonicity) -> Option { - match regulation_sign { - Monotonicity::Activation => Some(Lib_Pbn_Monotonicity::Activation), - Monotonicity::Inhibition => Some(Lib_Pbn_Monotonicity::Inhibition), - Monotonicity::Unknown => None, - // todo: fix - Monotonicity::Dual => None, - } - } - - /// **(internal)** Static utility method to convert `Essentiality` from boolean. - /// TODO: note that `lib-param-bn` currently cannot distinguish between `False` and `Unknown` variants of `Essentiality`. - fn essentiality_from_bool(essentiality: bool) -> Essentiality { - match essentiality { - true => Essentiality::True, - // todo: fix, this is how it works now in `lib-param-bn` - false => Essentiality::Unknown, - } - } } #[cfg(test)] diff --git a/src/aeon_events.ts b/src/aeon_events.ts index 96d233c..1c80d43 100644 --- a/src/aeon_events.ts +++ b/src/aeon_events.ts @@ -345,17 +345,26 @@ interface AeonState { /** Ask for a sketch data (might be useful to update analysis window, or if automatic sketch * transfer from backend does not work). */ refreshSketch: () => void + /** Fully reset the analysis and start again. The same sketch will be used. */ + resetAnalysis: () => void + /** Information that analysis was reset. */ + analysisReset: Observable + /** Sample given number of Boolean networks from the results, either dereministically + * or randomly. The networks are saved in a zip archive at given path. */ + sampleNetworks: (count: number, seed: number | null, path: string) => void /** Start the full inference analysis. */ startFullInference: () => void - /** Note that inference analysis was started. */ + /** Information that inference analysis was started. + * Currently not utilized. */ inferenceStarted: Observable /** Inference analysis results. */ inferenceResultsReceived: Observable /** Start the static check analysis. */ startStaticCheck: () => void - /** Note that static check analysis was started. */ + /** Information that static check analysis was started. + * Currently not utilized. */ staticCheckStarted: Observable /** Static check analysis results. */ staticCheckResultsReceived: Observable @@ -488,12 +497,14 @@ export interface StatPropIdUpdateData { original_id: string, new_id: string } export interface InferenceResults { num_sat_networks: number comp_time: number + metadata_log: string } /** An object representing all information regarding static check analysis results. */ export interface StaticCheckResults { num_sat_networks: number comp_time: number + metadata_log: string } /** A function that is notified when a state value changes. */ @@ -1379,9 +1390,23 @@ export const aeonState: AeonState = { }, analysis: { sketchRefreshed: new Observable(['analysis', 'get_sketch']), + analysisReset: new Observable(['analysis', 'analysis_reset']), + refreshSketch (): void { aeonEvents.refresh(['analysis', 'get_sketch']) }, + resetAnalysis () { + aeonEvents.emitAction({ + path: ['analysis', 'reset_analysis'], + payload: null + }) + }, + sampleNetworks (count: number, seed: number | null, path: string): void { + aeonEvents.emitAction({ + path: ['analysis', 'sample_networks'], + payload: JSON.stringify({ count, seed, path }) + }) + }, inferenceResultsReceived: new Observable(['analysis', 'inference_results']), staticCheckResultsReceived: new Observable(['analysis', 'static_results']), diff --git a/src/html/component-analysis/analysis-component/analysis-component.ts b/src/html/component-analysis/analysis-component/analysis-component.ts index cbc90c9..e7c2d1a 100644 --- a/src/html/component-analysis/analysis-component/analysis-component.ts +++ b/src/html/component-analysis/analysis-component/analysis-component.ts @@ -1,5 +1,5 @@ import { css, html, LitElement, type TemplateResult, unsafeCSS } from 'lit' -import { customElement, property } from 'lit/decorators.js' +import { customElement, property, state } from 'lit/decorators.js' import style_less from './analysis-component.less?inline' import { aeonState, @@ -7,6 +7,9 @@ import { type InferenceResults, type StaticCheckResults } from '../../../aeon_events' +import { + AnalysisType +} from '../../util/analysis-interfaces' import { dialog } from '@tauri-apps/api' @customElement('analysis-component') @@ -14,6 +17,10 @@ export default class AnalysisComponent extends LitElement { static styles = css`${unsafeCSS(style_less)}` @property() sketchData: SketchData | null = null + @state() selected_analysis: AnalysisType | null = null + @state() results: InferenceResults | StaticCheckResults | null = null + @state() isRandomizeChecked: boolean = false // Track the state of the "Randomize" checkbox + constructor () { super() @@ -82,12 +89,14 @@ export default class AnalysisComponent extends LitElement { } #onInferenceResultsReceived (results: InferenceResults): void { + this.results = results console.log('Received full inference results.') console.log('-> There are ' + results.num_sat_networks + ' satisfying networks.') console.log('-> The computation took ' + results.comp_time + ' seconds.') } #onStaticCheckResultsReceived (results: StaticCheckResults): void { + this.results = results console.log('Received static check results.') console.log('-> There are ' + results.num_sat_networks + ' satisfying networks.') console.log('-> The computation took ' + results.comp_time + ' seconds.') @@ -105,13 +114,74 @@ export default class AnalysisComponent extends LitElement { private runInference (): void { console.log('Initiating inference analysis, wait a bit...') aeonState.analysis.startFullInference() - // TODO + this.selected_analysis = AnalysisType.Inference } private runStaticCheck (): void { console.log('Initiating static check, wait a bit...') aeonState.analysis.startStaticCheck() - // TODO + this.selected_analysis = AnalysisType.StaticCheck + } + + // Method to format the results for display + private formatResults (results: InferenceResults | StaticCheckResults): string { + return ` + Number of satisfying networks: ${results.num_sat_networks} + Computation time: ${results.comp_time} seconds + + Computation metadata: + -------------- + ${results.metadata_log} + ` + } + + private resetAnalysis (): void { + // Reset analysis settings and clear the results + console.log('Resetting analysis.') + aeonState.analysis.resetAnalysis() + + this.selected_analysis = null + this.results = null + } + + private async sampleNetworks (): Promise { + const witnessCountInput = this.shadowRoot?.getElementById('witness-count') as HTMLInputElement + if (witnessCountInput === null) { + console.error('Failed to get input elements to sample networks.') + return + } + + const witnessCount = parseInt(witnessCountInput.value, 10) + const randomSeedInput = this.shadowRoot?.getElementById('random-seed') as HTMLInputElement | null + const randomSeed = this.isRandomizeChecked && randomSeedInput !== null ? parseInt(randomSeedInput.value, 10) : null + + console.log(`Sampling networks - witness count: ${witnessCount}, randomize: ${this.isRandomizeChecked}, random seed: ${randomSeed}`) + + const archiveName = `sat_networks_${witnessCount}.zip` + const handle = await dialog.save({ + defaultPath: archiveName, + filters: [{ + name: 'ZIP', + extensions: ['zip'] + }] + }) + if (handle === null) return + + let fileName + if (Array.isArray(handle)) { + fileName = handle.pop() ?? 'unknown' + } else { + fileName = handle + } + + console.log(`Generating network archive at: ${fileName}`) + aeonState.analysis.sampleNetworks(witnessCount, randomSeed, fileName) + } + + // Add a handler to update the checkbox state + private handleRandomizeChange (event: Event): void { + const checkbox = event.target as HTMLInputElement + this.isRandomizeChecked = checkbox.checked } render (): TemplateResult { @@ -120,24 +190,81 @@ export default class AnalysisComponent extends LitElement {
-

Inference

-
- -
- +

Inference

- -
+ + +
+ + + ${this.selected_analysis === null +? html` +
+ +
+ + +
+ +
+ +
+ ` +: ''} + + + ${this.selected_analysis !== null +? html` +
+ + + + ${this.results !== null +? html` +
+ +
+ + + + + + + + ${this.isRandomizeChecked +? html` + + + ` +: ''} +
+ +
+ ` +: ''} +
+ ` +: ''}
diff --git a/src/html/util/analysis-interfaces.ts b/src/html/util/analysis-interfaces.ts new file mode 100644 index 0000000..0b250ed --- /dev/null +++ b/src/html/util/analysis-interfaces.ts @@ -0,0 +1,4 @@ +export enum AnalysisType { + Inference = 'Inference', + StaticCheck = 'StaticCheck' +} From cb77e7998f4f02728a2004ceecabe5bee1815204 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ond=C5=99ej=20Huvar?= <492849@mail.muni.cz> Date: Wed, 7 Aug 2024 20:32:42 +0200 Subject: [PATCH 7/8] Add explicit option for generating self-loops. --- .../float-menu/float-menu.ts | 24 ++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) diff --git a/src/html/component-editor/regulations-editor/float-menu/float-menu.ts b/src/html/component-editor/regulations-editor/float-menu/float-menu.ts index 2483a0d..af0edf0 100644 --- a/src/html/component-editor/regulations-editor/float-menu/float-menu.ts +++ b/src/html/component-editor/regulations-editor/float-menu/float-menu.ts @@ -13,7 +13,8 @@ import { faPen, faPlus, faRightLeft, - faTrash + faTrash, + faRotateLeft } from '@fortawesome/free-solid-svg-icons' import { type Position } from 'cytoscape' import { map } from 'lit/directives/map.js' @@ -56,6 +57,9 @@ export default class FloatMenu extends LitElement { case 'A': this.addEdge() break + case 'S': + this.addSelfLoop() + break case 'F': this.focusFunction() break @@ -90,6 +94,11 @@ export default class FloatMenu extends LitElement { label: () => 'Add Edge (A)', click: this.addEdge }, + { + icon: () => icon(faRotateLeft).node[0], + label: () => 'Add self-loop (S)', + click: this.addSelfLoop + }, { icon: () => icon(faCalculator).node[0], label: () => 'Edit update function (F)', @@ -232,6 +241,19 @@ export default class FloatMenu extends LitElement { })) } + private addSelfLoop (): void { + this.dispatchEvent(new CustomEvent('add-regulation', { + detail: { + source: this.data?.id, + target: this.data?.id, + essential: Essentiality.TRUE, + monotonicity: Monotonicity.UNSPECIFIED + }, + bubbles: true, + composed: true + })) + } + private focusFunction (): void { window.dispatchEvent(new CustomEvent('focus-function-field', { detail: { From 6910ce566d8b0f4b34e43b80f485e19fe4b61a65 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ond=C5=99ej=20Huvar?= <492849@mail.muni.cz> Date: Wed, 7 Aug 2024 21:33:53 +0200 Subject: [PATCH 8/8] Slight refactoring and modularizing of inference pipeline. --- .../algorithms/eval_static/template_eval.rs | 8 +- src-tauri/src/analysis/analysis_state.rs | 2 +- src-tauri/src/analysis/inference_solver.rs | 118 +++++++++++------- .../analysis-component/analysis-component.ts | 17 +-- 4 files changed, 82 insertions(+), 63 deletions(-) diff --git a/src-tauri/src/algorithms/eval_static/template_eval.rs b/src-tauri/src/algorithms/eval_static/template_eval.rs index ef51c7a..0fae2d0 100644 --- a/src-tauri/src/algorithms/eval_static/template_eval.rs +++ b/src-tauri/src/algorithms/eval_static/template_eval.rs @@ -12,7 +12,7 @@ pub fn eval_static_prop( static_prop: StatProperty, network: &BooleanNetwork, graph: &SymbolicAsyncGraph, -) -> GraphColors { +) -> Result { // 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(); @@ -55,7 +55,8 @@ pub fn eval_static_prop( } else { context.mk_constant(true) }; - GraphColors::new(observability.and(unit_bdd), context) + let valid_colors = GraphColors::new(observability.and(unit_bdd), context); + Ok(valid_colors) } StatPropertyType::RegulationEssentialContext(_prop) => todo!(), StatPropertyType::RegulationMonotonic(prop) => { @@ -82,7 +83,8 @@ pub fn eval_static_prop( Monotonicity::Unknown => context.mk_constant(true), Monotonicity::Dual => unimplemented!(), }; - GraphColors::new(monotonicity.and(unit_bdd), context) + let valid_colors = GraphColors::new(monotonicity.and(unit_bdd), context); + Ok(valid_colors) } StatPropertyType::RegulationMonotonicContext(_prop) => todo!(), StatPropertyType::FnInputEssentialContext(_prop) => todo!(), diff --git a/src-tauri/src/analysis/analysis_state.rs b/src-tauri/src/analysis/analysis_state.rs index 9679093..6222eae 100644 --- a/src-tauri/src/analysis/analysis_state.rs +++ b/src-tauri/src/analysis/analysis_state.rs @@ -87,7 +87,7 @@ impl SessionState for AnalysisState { .solver .as_mut() .unwrap() - .run_computation_prototype(self.sketch.clone())?; + .run_whole_inference_prototype(self.sketch.clone())?; let payload = results.to_json_str(); let state_change = Event::build(&["analysis", "inference_results"], Some(&payload)); diff --git a/src-tauri/src/analysis/inference_solver.rs b/src-tauri/src/analysis/inference_solver.rs index bd043cd..5ee9a1f 100644 --- a/src-tauri/src/analysis/inference_solver.rs +++ b/src-tauri/src/analysis/inference_solver.rs @@ -5,7 +5,9 @@ use crate::log; use crate::sketchbook::properties::{DynProperty, StatProperty}; use crate::sketchbook::Sketch; use biodivine_hctl_model_checker::mc_utils::get_extended_symbolic_graph; -use biodivine_lib_param_bn::symbolic_async_graph::{GraphColors, SymbolicAsyncGraph}; +use biodivine_lib_param_bn::symbolic_async_graph::{ + GraphColoredVertices, GraphColors, SymbolicAsyncGraph, +}; use biodivine_lib_param_bn::BooleanNetwork; use std::time::SystemTime; @@ -49,6 +51,19 @@ pub struct InferenceSolver { } impl InferenceSolver { + /// Prepares new "empty" `InferenceSolver` instance. + /// The computation is started by one of the `run_` methods later. + pub fn new() -> InferenceSolver { + InferenceSolver { + bn: None, + graph: None, + static_props: None, + dynamic_props: None, + raw_sat_colors: None, + status_updates: vec![(InferenceStatus::Created, SystemTime::now())], + } + } + /// Reference getter for a Boolean network. pub fn bn(&self) -> Result<&BooleanNetwork, String> { if let Some(bn) = &self.bn { @@ -137,18 +152,23 @@ impl InferenceSolver { } } +/// Computation-related methods. impl InferenceSolver { - /// Prepares new "empty" `InferenceSolver` instance. - /// The computation is started by [start_computing] later. - pub fn new() -> InferenceSolver { - InferenceSolver { - bn: None, - graph: None, - static_props: None, - dynamic_props: None, - raw_sat_colors: None, - status_updates: vec![(InferenceStatus::Created, SystemTime::now())], + /// Run the prototype version of the inference. + /// This wraps the [run_computation_prototype_inner] to also log potential errors. + /// + /// WARNING: This is only a prototype, and considers just parts of the sketch that are easy to + /// process at the moment. Some parts are lost, including "dual regulations", some kinds of + /// static properties, all but generic dynamic properties. + pub fn run_whole_inference_prototype( + &mut self, + sketch: Sketch, + ) -> Result { + let results = self.run_whole_inference_prototype_inner(sketch); + if results.is_err() { + self.status_update(InferenceStatus::Error); } + results } /// Extract and convert relevant components from the sketch (boolean network, properties). @@ -169,18 +189,40 @@ impl InferenceSolver { Ok((bn, static_properties, dynamic_properties)) } - /// Run the prototype version of the inference. - /// This wraps the [run_computation_prototype_inner] to also log potential errors. + /// Evaluate previously collected static properties, and restrict the unit set of the + /// graph to the set of valid colors. /// - /// WARNING: This is only a prototype, and considers just parts of the sketch that are easy to - /// process at the moment. Some parts are lost, including "dual regulations", some kinds of - /// static properties, all but generic dynamic properties. - pub fn run_computation_prototype(&mut self, sketch: Sketch) -> Result { - let results = self.run_computation_prototype_inner(sketch); - if results.is_err() { - self.status_update(InferenceStatus::Error); + /// TODO: function `eval_static_prop` needs to be finished. + fn eval_static(&mut self) -> Result<(), String> { + for stat_property in self.stat_props()?.clone() { + let inferred_colors = eval_static_prop(stat_property, self.bn()?, self.graph()?)?; + let colored_vertices = GraphColoredVertices::new( + inferred_colors.into_bdd(), + self.graph()?.symbolic_context(), + ); + let new_graph: SymbolicAsyncGraph = self.graph()?.restrict(&colored_vertices); + self.graph = Some(new_graph); } - results + self.status_update(InferenceStatus::EvaluatedStatic); + Ok(()) + } + + /// Evaluate previously collected dynamic properties, and restrict the unit set of the + /// graph to the set of valid colors. + /// + /// TODO: function `eval_dyn_prop` needs to be finished. + fn eval_dynamic(&mut self) -> Result<(), String> { + for dyn_property in self.dyn_props()?.clone() { + let inferred_colors = eval_dyn_prop(dyn_property, self.graph()?)?; + let colored_vertices = GraphColoredVertices::new( + inferred_colors.into_bdd(), + self.graph()?.symbolic_context(), + ); + let new_graph: SymbolicAsyncGraph = self.graph()?.restrict(&colored_vertices); + self.graph = Some(new_graph); + } + self.status_update(InferenceStatus::EvaluatedDynamic); + Ok(()) } /// Run the prototype version of the inference. @@ -188,7 +230,7 @@ impl InferenceSolver { /// WARNING: This is only a prototype, and considers just parts of the sketch that are easy to /// process at the moment. Some parts are lost, including "dual regulations", some kinds of /// static properties, all but generic dynamic properties. - fn run_computation_prototype_inner( + fn run_whole_inference_prototype_inner( &mut self, sketch: Sketch, ) -> Result { @@ -209,43 +251,23 @@ impl InferenceSolver { self.graph = Some(get_extended_symbolic_graph(self.bn()?, num_hctl_vars)?); self.status_update(InferenceStatus::GeneratedGraph); let msg = format!( - "After graph generating: {}\n", + "N. of candidates before evaluating any properties: {}\n", self.current_candidate_colors()?.approx_cardinality() ); metadata.push_str(&msg); // step 4: todo: evaluate static properties, restrict colors - for stat_property in self.stat_props()?.clone() { - let inferred_colors = eval_static_prop(stat_property, self.bn()?, self.graph()?); - - let new_graph: SymbolicAsyncGraph = SymbolicAsyncGraph::with_custom_context( - self.graph()?.as_network().unwrap(), - self.graph()?.symbolic_context().clone(), - inferred_colors.as_bdd().clone(), - )?; - self.graph = Some(new_graph); - } - self.status_update(InferenceStatus::EvaluatedStatic); + self.eval_static()?; let msg = format!( - "After static props: {}\n", + "N. of candidates after evaluating static props: {}\n", self.current_candidate_colors()?.approx_cardinality() ); metadata.push_str(&msg); - // step 5: todo: evaluate dynamic properties, restrict colors - for dyn_property in self.dyn_props()?.clone() { - let inferred_colors = eval_dyn_prop(dyn_property, self.graph()?)?; - - let new_graph: SymbolicAsyncGraph = SymbolicAsyncGraph::with_custom_context( - self.graph()?.as_network().unwrap(), - self.graph()?.symbolic_context().clone(), - inferred_colors.as_bdd().clone(), - )?; - self.graph = Some(new_graph); - } - self.status_update(InferenceStatus::EvaluatedDynamic); + // step 5: evaluate dynamic properties + self.eval_dynamic()?; let msg = format!( - "After dynamic props: {}\n", + "N. of candidates after evaluating dynamic props: {}\n", self.current_candidate_colors()?.approx_cardinality() ); metadata.push_str(&msg); diff --git a/src/html/component-analysis/analysis-component/analysis-component.ts b/src/html/component-analysis/analysis-component/analysis-component.ts index e7c2d1a..80a4b8f 100644 --- a/src/html/component-analysis/analysis-component/analysis-component.ts +++ b/src/html/component-analysis/analysis-component/analysis-component.ts @@ -125,14 +125,11 @@ export default class AnalysisComponent extends LitElement { // Method to format the results for display private formatResults (results: InferenceResults | StaticCheckResults): string { - return ` - Number of satisfying networks: ${results.num_sat_networks} - Computation time: ${results.comp_time} seconds - - Computation metadata: - -------------- - ${results.metadata_log} - ` + return `Number of satisfying networks: ${results.num_sat_networks}\n` + + `Computation time: ${results.comp_time} seconds\n\n\n` + + 'Computation metadata:\n' + + '--------------\n' + + `${results.metadata_log}\n` } private resetAnalysis (): void { @@ -230,9 +227,7 @@ export default class AnalysisComponent extends LitElement { ${this.selected_analysis !== null ? html`
- + ${this.results !== null