-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Start working on analysis of HCTL with placeholders.
- Loading branch information
Showing
14 changed files
with
839 additions
and
35 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,100 @@ | ||
| use biodivine_hctl_model_checker::mc_utils::get_extended_symbolic_graph; | ||
| use biodivine_hctl_model_checker::model_checking::{ | ||
| model_check_formula, model_check_formula_dirty, | ||
| }; | ||
| use biodivine_lib_param_bn::symbolic_async_graph::SymbolicAsyncGraph; | ||
| use biodivine_lib_param_bn::BooleanNetwork; | ||
| use boolean_network_sketches::data_processing::data_encoding::encode_observation; | ||
| use boolean_network_sketches::data_processing::observations::Observation; | ||
| use boolean_network_sketches::hctl_with_holes::reachability_one_hole::{ | ||
| general_to_specific_on_the_fly_eval, general_to_specific_precomp_eval, naive_eval, | ||
| specific_to_general_eval, | ||
| }; | ||
| use boolean_network_sketches::hctl_with_holes::utils::encode_obs_weight_pairs; | ||
| #[allow(unused_imports)] | ||
| use boolean_network_sketches::hctl_with_holes::{MODEL_20V, MODEL_53V}; | ||
| use std::time::SystemTime; | ||
|
|
||
| fn main() { | ||
| let use_large = true; | ||
|
|
||
| let mut model = MODEL_20V; | ||
| let mut start_from_ones = false; | ||
| if use_large { | ||
| model = MODEL_53V; | ||
| start_from_ones = true; | ||
| } | ||
|
|
||
| let bn = BooleanNetwork::try_from(model).unwrap(); | ||
| let props_vec: Vec<_> = bn | ||
| .variables() | ||
| .map(|v| bn.get_variable_name(v).clone()) | ||
| .collect(); | ||
|
|
||
| // for the first two methods, we must use new STG and sets with symbolic variables (for HCTL model checking) | ||
| let stg = get_extended_symbolic_graph(&bn, 1).unwrap(); | ||
|
|
||
| // fixed initial observation (either ones or zeros) | ||
| let init_observation = if start_from_ones { | ||
| Observation::new_full_true(props_vec.len()) | ||
| } else { | ||
| Observation::new_full_false(props_vec.len()) | ||
| }; | ||
| let init_observation_str = encode_observation(&init_observation, &props_vec).unwrap(); | ||
| let init_observation_set = | ||
| model_check_formula_dirty(init_observation_str.as_str(), &stg).unwrap(); | ||
| // variants of the second observation and their weights | ||
| let second_observation_weight_pairs = | ||
| encode_obs_weight_pairs(&props_vec, !start_from_ones).unwrap(); | ||
|
|
||
| let start = SystemTime::now(); | ||
| println!("naive_eval"); | ||
| let best_weight = naive_eval( | ||
| &stg, | ||
| start, | ||
| &init_observation_set, | ||
| second_observation_weight_pairs.clone(), | ||
| ); | ||
| println!("TOTAL ELAPSED: {}", start.elapsed().unwrap().as_millis()); | ||
| println!("BEST WEIGHT: {:?}", best_weight); | ||
| print!("\n\n\n"); | ||
|
|
||
| let start = SystemTime::now(); | ||
| println!("specific_to_general_eval"); | ||
| let best_weight = specific_to_general_eval( | ||
| &stg, | ||
| start, | ||
| &init_observation_set, | ||
| second_observation_weight_pairs.clone(), | ||
| ); | ||
| println!("TOTAL ELAPSED: {}", start.elapsed().unwrap().as_millis()); | ||
| println!("BEST WEIGHT: {:?}", best_weight); | ||
| print!("\n\n\n"); | ||
|
|
||
| // for the following methods, we must use new STG and sets without symbolic variables | ||
| let stg = SymbolicAsyncGraph::new(&bn).unwrap(); | ||
| let init_observation_set = model_check_formula(init_observation_str.as_str(), &stg).unwrap(); | ||
|
|
||
| let start = SystemTime::now(); | ||
| println!("general_to_specific_precomp_eval"); | ||
| let best_weight = general_to_specific_precomp_eval( | ||
| &stg, | ||
| start, | ||
| &init_observation_set, | ||
| second_observation_weight_pairs.clone(), | ||
| ); | ||
| println!("TOTAL ELAPSED: {}", start.elapsed().unwrap().as_millis()); | ||
| println!("BEST WEIGHT: {:?}", best_weight); | ||
| print!("\n\n\n"); | ||
|
|
||
| let start = SystemTime::now(); | ||
| println!("general_to_specific_on_the_fly_eval"); | ||
| let best_weight = general_to_specific_on_the_fly_eval( | ||
| &stg, | ||
| start, | ||
| &init_observation_set, | ||
| second_observation_weight_pairs.clone(), | ||
| ); | ||
| println!("TOTAL ELAPSED: {}", start.elapsed().unwrap().as_millis()); | ||
| println!("BEST WEIGHT: {:?}", best_weight); | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,41 @@ | ||
| use biodivine_lib_param_bn::symbolic_async_graph::SymbolicAsyncGraph; | ||
| use biodivine_lib_param_bn::BooleanNetwork; | ||
| use boolean_network_sketches::hctl_with_holes::reachability_two_holes::two_hole_analysis; | ||
| use boolean_network_sketches::hctl_with_holes::utils::encode_obs_weight_pairs; | ||
| #[allow(unused_imports)] | ||
| use boolean_network_sketches::hctl_with_holes::{MODEL_20V, MODEL_53V}; | ||
| use std::time::SystemTime; | ||
|
|
||
| fn main() { | ||
| let use_large = false; | ||
|
|
||
| let mut model = MODEL_20V; | ||
| let mut start_from_ones = true; | ||
| if use_large { | ||
| model = MODEL_53V; | ||
| start_from_ones = false; | ||
| } | ||
|
|
||
| let bn = BooleanNetwork::try_from(model).unwrap(); | ||
| let props_vec: Vec<_> = bn | ||
| .variables() | ||
| .map(|v| bn.get_variable_name(v).clone()) | ||
| .collect(); | ||
| let stg = SymbolicAsyncGraph::new(&bn).unwrap(); | ||
|
|
||
| let start_time = SystemTime::now(); | ||
|
|
||
| // variants of each observation and their weights (one being ones, the other zeros) | ||
| let observation1_weight_pairs = encode_obs_weight_pairs(&props_vec, start_from_ones).unwrap(); | ||
| let observation2_weight_pairs = encode_obs_weight_pairs(&props_vec, !start_from_ones).unwrap(); | ||
|
|
||
| let best_weight = two_hole_analysis( | ||
| &stg, | ||
| observation1_weight_pairs, | ||
| observation2_weight_pairs, | ||
| start_time, | ||
| ); | ||
| let time = start_time.elapsed().unwrap().as_millis(); | ||
| println!("BEST WEIGHT: {:?}", best_weight); | ||
| println!("TOTAL ELAPSED: {time}\n\n"); | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.