Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Refactor and extend dataset handling #53

Merged
merged 4 commits into from
Oct 30, 2024
Merged

Refactor and extend dataset handling #53

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
74baa34
Add time-series handling, indices to observations on FE, automatic co…
ondrej33 Oct 29, 2024
4be0113
Formatting
ondrej33 Oct 29, 2024
7975f36
Add test case for trajectory properties.
ondrej33 Oct 29, 2024
6a3fa40
Allow editing dataset variables.
ondrej33 Oct 30, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions data/test_data/data_time_series.csv
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
ID,A,B,C,D
a,1,0,0,0
b,1,1,0,0
c,1,1,1,0
d,1,1,1,1
159 changes: 100 additions & 59 deletions data/test_data/test_model_with_data.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
{
"annotation": "",
"model": {
"variables": [
{
Expand Down Expand Up @@ -124,9 +123,9 @@
"nodes": [
{
"layout": "default",
"variable": "D",
"px": 642.49677,
"py": 185.15988
"variable": "B",
"px": 0.0,
"py": 0.0
},
{
"layout": "default",
Expand All @@ -136,39 +135,53 @@
},
{
"layout": "default",
"variable": "A",
"px": 346.89832,
"py": 183.03789
"variable": "D",
"px": 642.49677,
"py": 185.15988
},
{
"layout": "default",
"variable": "B",
"px": 0.0,
"py": 0.0
"variable": "A",
"px": 346.89832,
"py": 183.03789
}
]
}
]
},
"datasets": [
{
"id": "data_mts",
"name": "data_mts",
"annotation":"",
"name": "data_time_series",
"id": "data_time_series",
"annotation": "",
"observations": [
{
"id": "abc",
"name": "abc",
"annotation":"",
"dataset": "data_mts",
"values": "111*"
"id": "a",
"name": "a",
"annotation": "",
"dataset": "data_time_series",
"values": "1000"
},
{
"id": "ab",
"name": "ab",
"annotation":"",
"dataset": "data_mts",
"values": "11**"
"id": "b",
"name": "b",
"annotation": "",
"dataset": "data_time_series",
"values": "1100"
},
{
"id": "c",
"name": "c",
"annotation": "",
"dataset": "data_time_series",
"values": "1110"
},
{
"id": "d",
"name": "d",
"annotation": "",
"dataset": "data_time_series",
"values": "1111"
}
],
"variables": [
Expand All @@ -179,21 +192,21 @@
]
},
{
"id": "data_fp",
"name": "data_fp",
"annotation":"",
"id": "data_fp",
"annotation": "",
"observations": [
{
"id": "ones",
"name": "ones",
"annotation":"",
"annotation": "",
"dataset": "data_fp",
"values": "1111"
},
{
"id": "zeros",
"name": "zeros",
"annotation":"",
"annotation": "",
"dataset": "data_fp",
"values": "0000"
}
Expand All @@ -204,58 +217,75 @@
"C",
"D"
]
},
{
"name": "data_mts",
"id": "data_mts",
"annotation": "",
"observations": [
{
"id": "abc",
"name": "abc",
"annotation": "",
"dataset": "data_mts",
"values": "111*"
},
{
"id": "ab",
"name": "ab",
"annotation": "",
"dataset": "data_mts",
"values": "11**"
}
],
"variables": [
"A",
"B",
"C",
"D"
]
}
],
"dyn_properties": [],
"stat_properties": [
{
"id": "essentiality_D_B",
"id": "essentiality_A_B",
"name": "Regulation essentiality property",
"annotation": "",
"variant": "RegulationEssential",
"input": "D",
"input": "A",
"target": "B",
"value": "True",
"context": null
},
{
"id": "essentiality_A_B",
"id": "essentiality_D_D",
"name": "Regulation essentiality property",
"annotation": "",
"variant": "RegulationEssential",
"input": "A",
"target": "B",
"input": "D",
"target": "D",
"value": "True",
"context": null
},
{
"id": "monotonicity_A_B",
"name": "Regulation monotonicity property",
"annotation": "",
"variant": "RegulationMonotonic",
"input": "A",
"target": "B",
"value": "Activation",
"context": null
},
{
"id": "essentiality_D_D",
"id": "essentiality_D_B",
"name": "Regulation essentiality property",
"annotation": "",
"variant": "RegulationEssential",
"input": "D",
"target": "D",
"target": "B",
"value": "True",
"context": null
},
{
"id": "essentiality_B_C",
"name": "Regulation essentiality property",
"id": "monotonicity_B_C",
"name": "Regulation monotonicity property",
"annotation": "",
"variant": "RegulationEssential",
"variant": "RegulationMonotonic",
"input": "B",
"target": "C",
"value": "True",
"value": "Activation",
"context": null
},
{
Expand All @@ -269,13 +299,13 @@
"context": null
},
{
"id": "monotonicity_B_C",
"name": "Regulation monotonicity property",
"id": "essentiality_B_C",
"name": "Regulation essentiality property",
"annotation": "",
"variant": "RegulationMonotonic",
"variant": "RegulationEssential",
"input": "B",
"target": "C",
"value": "Activation",
"value": "True",
"context": null
},
{
Expand All @@ -288,6 +318,16 @@
"value": "Inhibition",
"context": null
},
{
"id": "monotonicity_A_B",
"name": "Regulation monotonicity property",
"annotation": "",
"variant": "RegulationMonotonic",
"input": "A",
"target": "B",
"value": "Activation",
"context": null
},
{
"id": "essentiality_A_C",
"name": "Regulation essentiality property",
Expand All @@ -299,24 +339,25 @@
"context": null
},
{
"id": "monotonicity_A_C",
"id": "monotonicity_D_B",
"name": "Regulation monotonicity property",
"annotation": "",
"variant": "RegulationMonotonic",
"input": "A",
"target": "C",
"input": "D",
"target": "B",
"value": "Activation",
"context": null
},
{
"id": "monotonicity_D_B",
"id": "monotonicity_A_C",
"name": "Regulation monotonicity property",
"annotation": "",
"variant": "RegulationMonotonic",
"input": "D",
"target": "B",
"input": "A",
"target": "C",
"value": "Activation",
"context": null
}
]
],
"annotation": ""
}
9 changes: 6 additions & 3 deletions src-tauri/src/algorithms/eval_dynamic/encode.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,12 +7,14 @@ use std::fmt::Write;
/// Encode a dataset of observations as a single HCTL formula. The particular formula
/// template is chosen depending on the type of data (attractor data, fixed-points, ...).
///
/// a) Fixed-point dataset is encoded as a conjunction of "steady-state formulas",
/// a) Fixed-point dataset is encoded with a conjunction of "steady-state formulas"
/// (see [mk_formula_fixed_point_list]) that ensures each observation correspond to a fixed point.
/// b) Attractor dataset is encoded as a conjunction of "attractor formulas",
/// b) Attractor dataset is encoded with a conjunction of "attractor formulas"
/// (see [mk_formula_attractor_list]) that ensures each observation correspond to an attractor.
/// b) Trap-space dataset is encoded as a conjunction of "trap-space formulas",
/// c) Trap-space dataset is encoded with a conjunction of "trap-space formulas"
/// (see [mk_formula_trap_space_list]) that ensures each observation correspond to a trap space.
/// d) Time-series dataset is encoded with a "reachability chain" formula,
/// (see [mk_formula_reachability_chain]) ensuring there is path between each consecutive observations.
pub fn encode_dataset_hctl_str(
dataset: &Dataset,
observation_id: Option<ObservationId>,
Expand All @@ -36,6 +38,7 @@ pub fn encode_dataset_hctl_str(
DataEncodingType::Attractor => Ok(mk_formula_attractor_list(&encoded_observations)),
DataEncodingType::FixedPoint => Ok(mk_formula_fixed_point_list(&encoded_observations)),
DataEncodingType::TrapSpace => Ok(mk_formula_trap_space_list(&encoded_observations)),
DataEncodingType::TimeSeries => Ok(mk_formula_reachability_chain(&encoded_observations)),
}
}

Expand Down
4 changes: 1 addition & 3 deletions src-tauri/src/algorithms/eval_dynamic/eval.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,9 +9,7 @@ use biodivine_hctl_model_checker::model_checking::model_check_formula_dirty;
use biodivine_lib_param_bn::biodivine_std::traits::Set;
use biodivine_lib_param_bn::symbolic_async_graph::{GraphColors, SymbolicAsyncGraph};

/// Evaluate given dynamic property given the transition graph.
///
/// TODO: We still need to handle time-series properties.
/// Evaluate given dynamic property given the symbolic transition graph.
pub fn eval_dyn_prop(
dyn_prop: ProcessedDynProp,
graph: &SymbolicAsyncGraph,
Expand Down
18 changes: 11 additions & 7 deletions src-tauri/src/algorithms/eval_dynamic/processed_props.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,12 +3,13 @@ use crate::sketchbook::observations::Dataset;
use crate::sketchbook::properties::dynamic_props::DynPropertyType;
use crate::sketchbook::Sketch;

/// Enum of possible variants of data to encode.
/// Enum of possible variants of data encodings via HCTL.
#[derive(Clone, Debug, Eq, PartialEq, Copy)]
pub enum DataEncodingType {
Attractor,
FixedPoint,
TrapSpace,
TimeSeries,
}

/// Property requiring that a particular HCTL formula is satisfied.
Expand Down Expand Up @@ -102,8 +103,6 @@ pub fn process_dynamic_props(sketch: &Sketch) -> Result<Vec<ProcessedDynProp>, S

let mut processed_props = Vec::new();
for (id, dyn_prop) in dynamic_props {
// TODO: currently, some types of properties (like time-series) are still not implemented

// we translate as many types of properties into HCTL, but we also treat some
// as special cases (these will have their own optimized evaluation)

Expand Down Expand Up @@ -136,7 +135,7 @@ pub fn process_dynamic_props(sketch: &Sketch) -> Result<Vec<ProcessedDynProp>, S
DynPropertyType::GenericDynProp(prop) => {
ProcessedDynProp::mk_hctl(id.as_str(), prop.processed_formula.as_str())
}
// translate to generic HCTL
// encode fixed-points HCTL formula
DynPropertyType::ExistsFixedPoint(prop) => {
// TODO: maybe encode as multiple formulae if we have more than one observation (instead of a conjunction)?
let dataset_id = prop.dataset.clone().unwrap();
Expand All @@ -148,7 +147,7 @@ pub fn process_dynamic_props(sketch: &Sketch) -> Result<Vec<ProcessedDynProp>, S
)?;
ProcessedDynProp::mk_hctl(id.as_str(), &formula)
}
// translate to generic HCTL
// encode attractors with HCTL formula
DynPropertyType::HasAttractor(prop) => {
// TODO: maybe encode as multiple formulae if we have more than one observation (instead of a conjunction)?
let dataset_id = prop.dataset.clone().unwrap();
Expand All @@ -160,8 +159,13 @@ pub fn process_dynamic_props(sketch: &Sketch) -> Result<Vec<ProcessedDynProp>, S
)?;
ProcessedDynProp::mk_hctl(id.as_str(), &formula)
}
// TODO: finish handling of time-series
DynPropertyType::ExistsTrajectory(..) => todo!(),
// encode time series with HCTL formula
DynPropertyType::ExistsTrajectory(prop) => {
let dataset_id = prop.dataset.clone().unwrap();
let dataset = sketch.observations.get_dataset(&dataset_id)?;
let formula = encode_dataset_hctl_str(dataset, None, DataEncodingType::TimeSeries)?;
ProcessedDynProp::mk_hctl(id.as_str(), &formula)
}
};
processed_props.push(dyn_prop_processed);
}
Expand Down
Loading