From 230b285ea61fedebd2aa7a527e8635882fa90fb5 Mon Sep 17 00:00:00 2001 From: erwanM Date: Wed, 28 Sep 2022 19:52:21 +0200 Subject: [PATCH] - local analysis for slices (simulation before the local component) - specified Inconclusive verdicts in specific cases (hide with coloc, simu with loopP or loopW and colocs, Fail when filtered) - local analysis with only front - made the stopping criterion on simulation configurable (loop num, act num etc) and graphical display - refactored generic process queue in generic process manager so as to implement HCS (high coverage search) in addition of BFS and DFS - refactored priorities so as to add a random option to randomly reorder child steps of the same parent node - for slice generation added a random version in addition to the exhaustive one - for the trace generation logger added an option to generate traces only in terminal nodes (in addition to always or whenever the interaction expresses the empty trace) - refactored coverage and global verdicts, added WeakFail for Failed slice analysis under simulation criteria, replaced Dead verdict for local analysis with a boolean on Out and OutSim --- Cargo.lock | 88 ++++- Cargo.toml | 5 +- src/core/mod.rs | 1 + src/core/multitrace.rs | 29 ++ src/core/semantics/frontier.rs | 58 ++- src/core/syntax/interaction.rs | 91 ++++- src/core/syntax/util/check_interaction.rs | 127 ++++++- src/from_hfiles/proc_options/hibou_options.rs | 356 ------------------ src/from_hfiles/proc_options/loggers.rs | 3 + src/from_hfiles/proc_options/opt_analyze.rs | 138 +++++-- src/from_hfiles/proc_options/opt_explore.rs | 40 +- src/from_hfiles/traces/htf_file.rs | 4 +- src/loggers/graphic/glog_ana.rs | 14 +- src/loggers/graphic/glog_explo.rs | 10 +- src/loggers/graphic/graphic_logger.rs | 6 +- src/loggers/graphic/verdict.rs | 14 +- src/loggers/tracegen/conf.rs | 2 + src/loggers/tracegen/tlog_explo.rs | 20 +- src/main.rs | 2 + src/process/abstract_proc/common.rs | 12 +- src/process/abstract_proc/generic.rs | 129 +------ src/process/abstract_proc/manager.rs | 194 ++++++++++ src/process/abstract_proc/mod.rs | 2 + src/process/abstract_proc/queue.rs | 234 ++++++++++++ src/process/ana_proc/anakind.rs | 187 ++++++++- src/process/ana_proc/interface/logger.rs | 8 +- src/process/ana_proc/local_analysis.rs | 39 +- src/process/ana_proc/manager.rs | 134 +++---- src/process/ana_proc/matches.rs | 292 +++++++------- src/process/ana_proc/multitrace.rs | 80 +++- src/process/ana_proc/verdicts.rs | 121 ++++-- src/process/explo_proc/interface/logger.rs | 7 +- .../explo_proc/interface/priorities.rs | 6 + src/process/explo_proc/manager.rs | 85 +++-- .../custom_draw/seqdiag/ext_multi_trace.rs | 23 +- .../custom_draw/seqdiag/interaction.rs | 6 +- src/sd_syntax.pest | 48 ++- src/slice/exhaustive.rs | 48 +++ src/slice/generate.rs | 80 ++++ src/slice/mod.rs | 60 +-- src/slice/random.rs | 66 ++++ src/ui/hibou_cli.rs | 26 +- src/ui/hibou_cli.yml | 25 +- 43 files changed, 1950 insertions(+), 970 deletions(-) create mode 100644 src/core/multitrace.rs delete mode 100644 src/from_hfiles/proc_options/hibou_options.rs create mode 100644 src/process/abstract_proc/manager.rs create mode 100644 src/process/abstract_proc/queue.rs create mode 100644 src/slice/exhaustive.rs create mode 100644 src/slice/generate.rs create mode 100644 src/slice/random.rs diff --git a/Cargo.lock b/Cargo.lock index 43eaffb..3d0119b 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -88,6 +88,12 @@ version = "0.1.10" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "4785bdd1c96b2a846b2bd7cc02e86b6b3dbf14e7e53446c4f54c92a361040822" +[[package]] +name = "cfg-if" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" + [[package]] name = "clap" version = "3.0.10" @@ -125,7 +131,7 @@ version = "1.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ba125de2af0df55319f41944744ad91c71113bf74a4646efff39afe1f6842db1" dependencies = [ - "cfg-if", + "cfg-if 0.1.10", ] [[package]] @@ -134,7 +140,7 @@ version = "0.4.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "09ee0cc8804d5393478d743b035099520087a5186f3b93fa58cec08fa62407b6" dependencies = [ - "cfg-if", + "cfg-if 0.1.10", "crossbeam-utils", ] @@ -156,7 +162,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "058ed274caafc1f60c4997b5fc07bf7dc7cca454af7c6e81edffe5f33f70dace" dependencies = [ "autocfg", - "cfg-if", + "cfg-if 0.1.10", "crossbeam-utils", "lazy_static", "maybe-uninit", @@ -171,7 +177,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c3c7c73a2d1e9fc0886a08b93e98eb643461230d5f1925e4036204d5f2e261a8" dependencies = [ "autocfg", - "cfg-if", + "cfg-if 0.1.10", "lazy_static", ] @@ -227,9 +233,20 @@ version = "0.1.14" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7abc8dd8451921606d809ba32e95b6111925cd2906060d2dcc29c070220503eb" dependencies = [ - "cfg-if", + "cfg-if 0.1.10", + "libc", + "wasi 0.9.0+wasi-snapshot-preview1", +] + +[[package]] +name = "getrandom" +version = "0.2.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4eb1a864a501629691edf6c15a593b7a51eebaa1e8468e9ddc623de7c9b58ec6" +dependencies = [ + "cfg-if 1.0.0", "libc", - "wasi", + "wasi 0.11.0+wasi-snapshot-preview1", ] [[package]] @@ -268,7 +285,7 @@ dependencies = [ [[package]] name = "hibou_label" -version = "0.7.7" +version = "0.7.8" dependencies = [ "clap", "image", @@ -277,6 +294,7 @@ dependencies = [ "maplit", "pest", "pest_derive", + "rand 0.8.5", "rusttype", "strum", "strum_macros", @@ -311,7 +329,7 @@ dependencies = [ "image", "itertools 0.9.0", "num 0.3.1", - "rand", + "rand 0.7.3", "rand_distr", "rayon", "rulinalg", @@ -363,9 +381,9 @@ checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646" [[package]] name = "libc" -version = "0.2.76" +version = "0.2.133" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "755456fae044e6fa1ebbbd1b3e902ae19e73097ed4ed87bb79934a867c007bc3" +checksum = "c0f80d65747a3e43d1596c7c5492d95d5edddaabd45a7fcdb02b95f644164966" [[package]] name = "linked-hash-map" @@ -634,13 +652,24 @@ version = "0.7.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "6a6b1679d49b24bbfe0c803429aa1874472f50d9b363131f0e89fc356b544d03" dependencies = [ - "getrandom", + "getrandom 0.1.14", "libc", - "rand_chacha", - "rand_core", + "rand_chacha 0.2.2", + "rand_core 0.5.1", "rand_hc", ] +[[package]] +name = "rand" +version = "0.8.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "34af8d1a0e25924bc5b7c43c079c942339d8f0a8b57c39049bef581b46327404" +dependencies = [ + "libc", + "rand_chacha 0.3.1", + "rand_core 0.6.4", +] + [[package]] name = "rand_chacha" version = "0.2.2" @@ -648,7 +677,17 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f4c8ed856279c9737206bf725bf36935d8666ead7aa69b52be55af369d193402" dependencies = [ "ppv-lite86", - "rand_core", + "rand_core 0.5.1", +] + +[[package]] +name = "rand_chacha" +version = "0.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e6c10a63a0fa32252be49d21e7709d4d4baf8d231c2dbce1eaa8141b9b127d88" +dependencies = [ + "ppv-lite86", + "rand_core 0.6.4", ] [[package]] @@ -657,7 +696,16 @@ version = "0.5.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "90bde5296fc891b0cef12a6d03ddccc162ce7b2aff54160af9338f8d40df6d19" dependencies = [ - "getrandom", + "getrandom 0.1.14", +] + +[[package]] +name = "rand_core" +version = "0.6.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ec0be4795e2f6a28069bec0b5ff3e2ac9bafc99e6a9a7dc3547996c5c816922c" +dependencies = [ + "getrandom 0.2.7", ] [[package]] @@ -666,7 +714,7 @@ version = "0.2.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "96977acbdd3a6576fb1d27391900035bf3863d4a16422973a409b488cf29ffb2" dependencies = [ - "rand", + "rand 0.7.3", ] [[package]] @@ -675,7 +723,7 @@ version = "0.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ca3129af7b92a17112d59ad498c6f81eaf463253766b90396d39ea7a39d6613c" dependencies = [ - "rand_core", + "rand_core 0.5.1", ] [[package]] @@ -857,6 +905,12 @@ version = "0.9.0+wasi-snapshot-preview1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "cccddf32554fecc6acb585f82a32a72e28b48f8c4c1883ddfeeeaa96f7d8e519" +[[package]] +name = "wasi" +version = "0.11.0+wasi-snapshot-preview1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" + [[package]] name = "weezl" version = "0.1.5" diff --git a/Cargo.toml b/Cargo.toml index a8c92a6..89092d1 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "hibou_label" -version = "0.7.7" +version = "0.7.8" authors = ["Erwan Mahe"] edition = "2018" @@ -19,4 +19,5 @@ pest = "2.1.3" # for pest parser pest_derive = "2.1.0" # ... clap = {version="3.0.6",features=["yaml"]} # for the command line interface maplit = "1.0.2" # for !hashset macro etc -itertools = "0.10.2" # for .sorted() etc \ No newline at end of file +itertools = "0.10.2" # for .sorted() etc +rand = "0.8.4" # random number generation e.g. for traversal heuristics for interaction semantics exploration and/or multitrace analysis \ No newline at end of file diff --git a/src/core/mod.rs b/src/core/mod.rs index 150ee8b..f29485d 100644 --- a/src/core/mod.rs +++ b/src/core/mod.rs @@ -21,4 +21,5 @@ pub mod semantics; pub mod error; pub mod trace; +//pub mod multitrace; diff --git a/src/core/multitrace.rs b/src/core/multitrace.rs new file mode 100644 index 0000000..5d53d03 --- /dev/null +++ b/src/core/multitrace.rs @@ -0,0 +1,29 @@ +/* +Copyright 2020 Erwan Mahe (github.com/erwanM974) + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +*/ + +// TODO: use this to refactor the current implementation of multitraces: +// TODO: decouple the multi-trace content's with the various flags and stuff for the analysis +// TODO: also in the graphical representation do not draw the multi-trace in the same drawing but rather draw two different and compose with Graphviz, it's cleaner I guess + +use std::collections::HashSet; +use crate::core::trace::TraceAction; + +pub struct MultiTraceCanal { + pub co_localization : HashSet, + pub trace : Vec> +} + +pub type MultiTrace = Vec; \ No newline at end of file diff --git a/src/core/semantics/frontier.rs b/src/core/semantics/frontier.rs index 331ed0d..f02a6de 100644 --- a/src/core/semantics/frontier.rs +++ b/src/core/semantics/frontier.rs @@ -128,16 +128,16 @@ fn global_frontier_rec(interaction : &Interaction, loop_depth : u32) -> Vec { - let mut front = push_frontier_left( global_frontier_rec(i1,loop_depth) ); + let mut front = push_frontier_left( &mut global_frontier_rec(i1,loop_depth) ); if i1.express_empty() { - front.append( &mut push_frontier_right( global_frontier_rec(i2,loop_depth)) ); + front.append( &mut push_frontier_right( &mut global_frontier_rec(i2,loop_depth)) ); } return front; }, Interaction::Seq(ref i1, ref i2) => { - let mut front = push_frontier_left( global_frontier_rec(i1,loop_depth) ); + let mut front = push_frontier_left( &mut global_frontier_rec(i1,loop_depth) ); // *** - for frt_elt2 in push_frontier_right( global_frontier_rec(i2,loop_depth)) { + for frt_elt2 in push_frontier_right( &mut global_frontier_rec(i2,loop_depth)) { if i1.avoids_all_of(&frt_elt2.target_lf_ids) { front.push(frt_elt2); } @@ -145,9 +145,9 @@ fn global_frontier_rec(interaction : &Interaction, loop_depth : u32) -> Vec { - let mut front = push_frontier_left( global_frontier_rec(i1,loop_depth) ); + let mut front = push_frontier_left( &mut global_frontier_rec(i1,loop_depth) ); // *** - for frt_elt2 in push_frontier_right( global_frontier_rec(i2,loop_depth)) { + for frt_elt2 in push_frontier_right( &mut global_frontier_rec(i2,loop_depth)) { let mut reqs_lf_ids = frt_elt2.target_lf_ids.clone(); for cr_lf_id in cr { reqs_lf_ids.remove(cr_lf_id); @@ -159,17 +159,17 @@ fn global_frontier_rec(interaction : &Interaction, loop_depth : u32) -> Vec { - let mut front = push_frontier_left( global_frontier_rec(i1,loop_depth) ); - front.append( &mut push_frontier_right( global_frontier_rec(i2,loop_depth)) ); + let mut front = push_frontier_left( &mut global_frontier_rec(i1,loop_depth) ); + front.append( &mut push_frontier_right( &mut global_frontier_rec(i2,loop_depth)) ); return front; }, Interaction::Par(ref i1, ref i2) => { - let mut front = push_frontier_left( global_frontier_rec(i1,loop_depth) ); - front.append( &mut push_frontier_right( global_frontier_rec(i2,loop_depth)) ); + let mut front = push_frontier_left( &mut global_frontier_rec(i1,loop_depth) ); + front.append( &mut push_frontier_right( &mut global_frontier_rec(i2,loop_depth)) ); return front; }, Interaction::Loop(_, ref i1) => { - return push_frontier_left( global_frontier_rec(i1,loop_depth+1) ); + return push_frontier_left( &mut global_frontier_rec(i1,loop_depth+1) ); }, _ => { panic!("non-conform interaction"); @@ -179,30 +179,18 @@ fn global_frontier_rec(interaction : &Interaction, loop_depth : u32) -> Vec) -> Vec { - let mut new_frontier : Vec = Vec::new(); - // *** - for frt_elt in frontier { - new_frontier.push( FrontierElement::new(Position::Left( Box::new(frt_elt.position ) ), - frt_elt.target_lf_ids, - frt_elt.target_actions, - frt_elt.act_kind, - frt_elt.loop_depth ) ); - } - // *** - return new_frontier; +fn push_frontier_left(frontier : &mut Vec) -> Vec { + return frontier.drain(..).map(|frt_elt| FrontierElement::new(Position::Left( Box::new(frt_elt.position ) ), + frt_elt.target_lf_ids, + frt_elt.target_actions, + frt_elt.act_kind, + frt_elt.loop_depth ) ).collect(); } -fn push_frontier_right(frontier : Vec) -> Vec { - let mut new_frontier : Vec = Vec::new(); - // *** - for frt_elt in frontier { - new_frontier.push( FrontierElement::new(Position::Right( Box::new(frt_elt.position ) ), - frt_elt.target_lf_ids, - frt_elt.target_actions, - frt_elt.act_kind, - frt_elt.loop_depth ) ); - } - // *** - return new_frontier; +fn push_frontier_right(frontier : &mut Vec) -> Vec { + return frontier.drain(..).map(|frt_elt| FrontierElement::new(Position::Right( Box::new(frt_elt.position ) ), + frt_elt.target_lf_ids, + frt_elt.target_actions, + frt_elt.act_kind, + frt_elt.loop_depth) ).collect(); } \ No newline at end of file diff --git a/src/core/syntax/interaction.rs b/src/core/syntax/interaction.rs index 477a097..f775144 100644 --- a/src/core/syntax/interaction.rs +++ b/src/core/syntax/interaction.rs @@ -14,6 +14,7 @@ See the License for the specific language governing permissions and limitations under the License. */ +use std::cmp::max; use std::collections::HashSet; use std::hash::{Hash, Hasher}; @@ -59,6 +60,69 @@ impl Interaction { } } + pub fn max_number_of_atomic_actions_outside_loops(&self) -> u32 { + match self { + &Interaction::Empty => { + return 0; + }, + &Interaction::Emission(ref em_act) => { + match &em_act.synchronicity { + CommunicationSynchronicity::Synchronous => { + return 1; + }, + CommunicationSynchronicity::Asynchronous => { + let mut num_act = 1; + for target in &em_act.targets { + match target { + EmissionTargetRef::Lifeline(_) => { + num_act += 1; + }, + _ => {} + } + } + return num_act; + } + } + }, + &Interaction::Reception(ref rc_act) => { + if rc_act.recipients.len() == 0 { + return 0; + } else { + match &rc_act.synchronicity { + CommunicationSynchronicity::Synchronous => { + return 1; + }, + CommunicationSynchronicity::Asynchronous => { + return rc_act.recipients.len() as u32; + } + } + } + }, + &Interaction::Strict(ref i1, ref i2) => { + return i1.max_number_of_atomic_actions_outside_loops() + i2.max_number_of_atomic_actions_outside_loops(); + }, + &Interaction::Seq(ref i1, ref i2) => { + return i1.max_number_of_atomic_actions_outside_loops() + i2.max_number_of_atomic_actions_outside_loops(); + }, + &Interaction::CoReg(_, ref i1, ref i2) => { + return i1.max_number_of_atomic_actions_outside_loops() + i2.max_number_of_atomic_actions_outside_loops(); + }, + &Interaction::Par(ref i1, ref i2) => { + return i1.max_number_of_atomic_actions_outside_loops() + i2.max_number_of_atomic_actions_outside_loops(); + }, + &Interaction::Alt(ref i1, ref i2) => { + let num1 = i1.max_number_of_atomic_actions_outside_loops(); + let num2 = i2.max_number_of_atomic_actions_outside_loops(); + return max(num1,num2); + }, + &Interaction::Loop(_, _) => { + return 0; + }, + _ => { + panic!("non-conform interaction"); + } + } + } pub fn express_empty(&self) -> bool { match self { @@ -357,7 +421,32 @@ impl Interaction { } } - + pub fn total_loop_num(&self) -> u32 { + match self { + &Interaction::Empty => { + return 0; + }, &Interaction::Emission(_) => { + return 0; + }, &Interaction::Reception(_) => { + return 0; + }, &Interaction::Strict(ref i1, ref i2) => { + return i1.total_loop_num() + i2.total_loop_num(); + }, &Interaction::Seq(ref i1, ref i2) => { + return i1.total_loop_num() + i2.total_loop_num(); + }, &Interaction::CoReg(_, ref i1, ref i2) => { + return i1.total_loop_num() + i2.total_loop_num(); + }, &Interaction::Par(ref i1, ref i2) => { + return i1.total_loop_num() + i2.total_loop_num(); + }, &Interaction::Alt(ref i1, ref i2) => { + return i1.total_loop_num() + i2.total_loop_num(); + }, &Interaction::Loop(_, ref i1) => { + return 1 + i1.total_loop_num(); + }, + _ => { + panic!("non-conform interaction"); + } + } + } pub fn hide(&self, lfs_to_remove : &HashSet) -> Interaction { diff --git a/src/core/syntax/util/check_interaction.rs b/src/core/syntax/util/check_interaction.rs index 17af508..ece8d51 100644 --- a/src/core/syntax/util/check_interaction.rs +++ b/src/core/syntax/util/check_interaction.rs @@ -15,11 +15,136 @@ limitations under the License. */ -use crate::core::syntax::interaction::Interaction; +use crate::core::syntax::interaction::*; use crate::core::syntax::action::*; + +pub struct InteractionCharacteristics { + pub has_gates : bool, + pub has_ands : bool, + pub has_coregions : bool, + pub has_loopP : bool, + pub has_loopW : bool, + pub has_loopS : bool +} + +impl InteractionCharacteristics { + + pub fn new(has_gates : bool, + has_ands : bool, + has_coregions : bool, + has_loopP : bool, + has_loopW : bool, + has_loopS : bool) -> InteractionCharacteristics { + return InteractionCharacteristics{has_gates,has_ands,has_coregions,has_loopP,has_loopW,has_loopS}; + } + + pub fn new_empty() -> InteractionCharacteristics { + return InteractionCharacteristics::new(false, + false, + false, + false, + false, + false); + } + + pub fn has_loop(&self) -> bool { + return (self.has_loopS || self.has_loopW || self.has_loopP); + } + + pub fn merge(&self, other : &InteractionCharacteristics) -> InteractionCharacteristics { + return InteractionCharacteristics::new( + self.has_gates || other.has_gates, + self.has_ands || other.has_ands, + self.has_coregions || other.has_coregions, + self.has_loopP || other.has_loopP, + self.has_loopW || other.has_loopW, + self.has_loopS || other.has_loopS, + ) + } +} + + impl Interaction { + pub fn get_characteristics(&self) -> InteractionCharacteristics { + match self { + Interaction::Empty => { + return InteractionCharacteristics::new_empty(); + }, + Interaction::Emission(ref em_act) => { + let mut has_gates : bool = false; + for tar_ref in &em_act.targets { + match tar_ref { + EmissionTargetRef::Gate(_) => { + has_gates = true; + }, + _ => {} + } + } + // *** + let mut charac = InteractionCharacteristics::new_empty(); + charac.has_gates = has_gates; + return charac; + }, + Interaction::Reception(ref rc_act) => { + let has_gates : bool; + match rc_act.origin_gt_id { + None => { + has_gates = false; + }, + Some(_) => { + has_gates = true; + } + } + // *** + let mut charac = InteractionCharacteristics::new_empty(); + charac.has_gates = has_gates; + return charac; + }, + Interaction::Strict(ref i1, ref i2) => { + return i1.get_characteristics().merge( &i2.get_characteristics() ); + }, + Interaction::Seq(ref i1, ref i2) => { + return i1.get_characteristics().merge( &i2.get_characteristics() ); + }, + Interaction::Par(ref i1, ref i2) => { + return i1.get_characteristics().merge( &i2.get_characteristics() ); + }, + Interaction::Alt(ref i1, ref i2) => { + return i1.get_characteristics().merge( &i2.get_characteristics() ); + }, + Interaction::Loop(ref sk, ref i1) => { + let mut charac = i1.get_characteristics(); + match sk { + LoopKind::SStrictSeq => { + charac.has_loopS = true; + }, + LoopKind::HHeadFirstWS => { + // *** + }, + LoopKind::WWeakSeq => { + charac.has_loopW = true; + }, + LoopKind::PInterleaving => { + charac.has_loopP = true; + } + } + return charac; + }, + Interaction::CoReg(ref cr, ref i1, ref i2) => { + let mut charac = i1.get_characteristics().merge( &i2.get_characteristics() ); + charac.has_coregions = true; + return charac; + }, + Interaction::And(ref i1, ref i2) => { + let mut charac = i1.get_characteristics().merge( &i2.get_characteristics() ); + charac.has_ands = true; + return charac; + } + } + } + pub fn has_gates(&self) -> bool { match self { Interaction::Empty => { diff --git a/src/from_hfiles/proc_options/hibou_options.rs b/src/from_hfiles/proc_options/hibou_options.rs deleted file mode 100644 index 20bb8e0..0000000 --- a/src/from_hfiles/proc_options/hibou_options.rs +++ /dev/null @@ -1,356 +0,0 @@ -/* -Copyright 2020 Erwan Mahe (github.com/erwanM974) - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - http://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. -*/ -use std::fs; -use std::collections::{HashSet,HashMap}; -use std::collections::btree_map::BTreeMap; -use std::path::Path; - -use pest::iterators::Pair; - -use crate::pest::Parser; - -use crate::core::syntax::interaction::Interaction; -use crate::core::syntax::action::*; -use crate::core::general_context::GeneralContext; - - -use crate::from_hfiles::error::HibouParsingError; - -use crate::from_hfiles::parser::*; -use crate::rendering::process::graphic_logger::{GraphicProcessLoggerOutputKind,GraphicProcessLoggerLayout,GraphicProcessLogger}; -use crate::process::hibou_process::*; -use crate::from_hfiles::hsf_file::ProcessKind; - -use crate::process::priorities::ProcessPriorities; -use crate::process::verdicts::GlobalVerdict; -use crate::process::anakind::{AnalysisKind,UseLocalAnalysis}; - -pub struct HibouOptions { - pub loggers : Vec>, - pub strategy : HibouSearchStrategy, - pub pre_filters : Vec, - pub ana_kind : Option, - pub local_analysis : Option, - pub goal : Option, - pub frontier_priorities : ProcessPriorities -} - - - -impl HibouOptions { - pub fn new(loggers : Vec>, - strategy : HibouSearchStrategy, - pre_filters : Vec, - ana_kind : Option, - local_analysis : Option, - goal:Option, - frontier_priorities : ProcessPriorities) -> HibouOptions { - return HibouOptions{loggers,strategy,pre_filters,ana_kind,local_analysis,goal,frontier_priorities}; - } - - pub fn default_explore() -> HibouOptions { - return HibouOptions{loggers:Vec::new(), - strategy:HibouSearchStrategy::BFS, - pre_filters:vec![HibouPreFilter::MaxLoopInstanciation(1)], - ana_kind:None, - goal:None, - local_analysis:None, - frontier_priorities:ProcessPriorities::new(0,0,0, None, -2, -2)}; - } - - pub fn default_analyze() -> HibouOptions { - return HibouOptions{loggers:Vec::new(), - strategy:HibouSearchStrategy::DFS, - pre_filters:Vec::new(), - ana_kind:Some(AnalysisKind::Prefix), - local_analysis:Some(UseLocalAnalysis::Yes), - goal:Some(GlobalVerdict::WeakPass), - frontier_priorities:ProcessPriorities::new(0,0,0, None, -2, -2)}; - } - - /* to be used recursively in global analyses when checking that its component local analysis are ok - important to keep "local_analysis:UseLocalAnalysis::No" so we don't infinitely recurse!! */ - pub fn local_analyze() -> HibouOptions { - return HibouOptions{loggers:Vec::new(), - strategy:HibouSearchStrategy::DFS, // of course DFS is better here - pre_filters:Vec::new(), - ana_kind:Some(AnalysisKind::Prefix), // because only one canal, no need for hide or simulate - local_analysis:Some(UseLocalAnalysis::No), // No so we don't infinitely recurse - goal:Some(GlobalVerdict::WeakPass), // it suffices to have a prefix - frontier_priorities:ProcessPriorities::new(0,0,0, None, -2, -2)}; // whatever works - } - -} - -#[derive(Clone, PartialEq, Eq, Hash, Debug)] -enum LoggerKinds { - graphic -} - -fn parse_priorities(priority_pair : Pair, - pp : &mut ProcessPriorities, - frontier_pp : bool) -> Result<(),HibouParsingError> { - let mut priority_contents = priority_pair.into_inner(); - let priority_kind_pair = priority_contents.next().unwrap(); - // *** - let priority_level_pair = priority_contents.next().unwrap(); - let priority_level_str : String = priority_level_pair.as_str().chars().filter(|c| !c.is_whitespace()).collect(); - let priority_level : i32 = priority_level_str.parse::().unwrap(); - // *** - match priority_kind_pair.as_rule() { - Rule::OPTION_PRIORITY_emission => { - pp.emission = priority_level; - }, - Rule::OPTION_PRIORITY_reception => { - pp.reception = priority_level; - }, - Rule::OPTION_PRIORITY_loop => { - pp.in_loop = priority_level; - }, - Rule::OPTION_PRIORITY_hide => { - pp.hide = priority_level; - }, - Rule::OPTION_PRIORITY_simu => { - pp.simulate = priority_level; - }, - Rule::OPTION_PRIORITY_step => { - if frontier_pp { - return Err( HibouParsingError::ProcessPriorityError("cannot specify \"step\" in frontier priorities".to_string()) ); - } else { - pp.step = Some( priority_level ); - } - } - _ => { - panic!("what rule then ? : {:?}", priority_kind_pair.as_rule() ); - } - } - return Ok(()); -} - -pub fn parse_hibou_options(option_pair : Pair, file_name : &str, process_kind : &ProcessKind) -> Result { - let mut loggers : Vec> = Vec::new(); - let mut strategy : HibouSearchStrategy = HibouSearchStrategy::BFS; - let mut frontier_priorities = ProcessPriorities::new(0,0,0, None, -2, -2); - let mut pre_filters : Vec = Vec::new(); - let mut ana_kind_opt : Option = Some(AnalysisKind::Prefix); - let mut local_analysis : Option = Some(UseLocalAnalysis::Yes); - let mut goal : Option = Some(GlobalVerdict::WeakPass); - // *** - let mut got_loggers : bool = false; - let mut got_strategy : bool = false; - let mut got_frontier_priorities : bool = false; - let mut got_pre_filters : bool = false; - let mut got_ana_kind : bool = false; - let mut got_locana : bool = false; - let mut got_goal : bool = false; - // *** - let mut declared_loggers : HashSet = HashSet::new(); - // *** - for option_decl_pair in option_pair.into_inner() { - match option_decl_pair.as_rule() { - Rule::OPTION_LOCANA_yes => { - if got_locana { - return Err( HibouParsingError::HsfSetupError("several 'local_analysis=X' declared in the same '@X_option' section".to_string())); - } - got_locana = true; - // *** - local_analysis = Some(UseLocalAnalysis::Yes); - }, - Rule::OPTION_LOCANA_no => { - if got_locana { - return Err( HibouParsingError::HsfSetupError("several 'local_analysis=X' declared in the same '@X_option' section".to_string())); - } - got_locana = true; - // *** - local_analysis = Some(UseLocalAnalysis::No); - }, - Rule::OPTION_LOGGER_DECL => { - if got_loggers { - return Err( HibouParsingError::HsfSetupError("several 'loggers=[X]' declared in the same '@X_option' section".to_string())); - } - got_loggers = true; - // *** - for logger_kind_pair in option_decl_pair.into_inner() { - match logger_kind_pair.as_rule() { - Rule::OPTION_GRAPHIC_LOGGER => { - if declared_loggers.contains(&LoggerKinds::graphic) { - return Err( HibouParsingError::HsfSetupError("several 'graphic' loggers declared in the same '@X_option' section".to_string())); - } - declared_loggers.insert( LoggerKinds::graphic ); - let graphic_logger_opts_pair = logger_kind_pair.into_inner().next(); - match graphic_logger_opts_pair { - None => { - loggers.push(Box::new(GraphicProcessLogger::new(file_name.to_string(), - GraphicProcessLoggerOutputKind::png, - GraphicProcessLoggerLayout::vertical ) ) ); - }, - Some(graphic_logger_opts) => { - let mut output_kind = GraphicProcessLoggerOutputKind::png; - let mut layout_kind = GraphicProcessLoggerLayout::vertical; - for opt_pair in graphic_logger_opts.into_inner() { - match opt_pair.as_rule() { - Rule::GRAPHIC_LOGGER_png => { - output_kind = GraphicProcessLoggerOutputKind::png; - }, - Rule::GRAPHIC_LOGGER_svg => { - output_kind = GraphicProcessLoggerOutputKind::svg; - }, - Rule::GRAPHIC_LOGGER_vertical => { - layout_kind = GraphicProcessLoggerLayout::vertical; - }, - Rule::GRAPHIC_LOGGER_horizontal => { - layout_kind = GraphicProcessLoggerLayout::horizontal; - }, - _ => { - panic!("what rule then ? : {:?}", opt_pair.as_rule() ); - } - } - } - loggers.push(Box::new(GraphicProcessLogger::new(file_name.to_string(),output_kind,layout_kind ) ) ); - } - } - }, - _ => { - panic!("what rule then ? : {:?}", logger_kind_pair.as_rule() ); - } - } - } - }, - Rule::OPTION_STRATEGY_DECL => { - if got_strategy { - return Err( HibouParsingError::HsfSetupError("several 'strategy=X' declared in the same '@X_option' section".to_string())); - } - got_strategy = true; - // *** - let strategy_pair = option_decl_pair.into_inner().next().unwrap(); - match strategy_pair.as_rule() { - Rule::OPTION_STRATEGY_BFS => { - strategy = HibouSearchStrategy::BFS; - }, - Rule::OPTION_STRATEGY_DFS => { - strategy = HibouSearchStrategy::DFS; - }, - _ => { - panic!("what rule then ? : {:?}", strategy_pair.as_rule() ); - } - } - }, - Rule::OPTION_FRONTIER_PRIORITIES_DECL => { - if got_frontier_priorities { - return Err( HibouParsingError::HsfSetupError("several 'frontier_priorities=X' declared in the same '@X_option' section".to_string())); - } - got_frontier_priorities = true; - // *** - for priority_pair in option_decl_pair.into_inner() { - parse_priorities(priority_pair,&mut frontier_priorities,true); - } - }, - Rule::OPTION_PREFILTERS_DECL => { - if got_pre_filters { - return Err( HibouParsingError::HsfSetupError("several 'pre_filters=[X]' declared in the same '@X_option' section".to_string())); - } - got_pre_filters = true; - // *** - for pre_filter_pair in option_decl_pair.into_inner() { - match pre_filter_pair.as_rule() { - Rule::OPTION_PREFILTER_MAX_DEPTH => { - let content = pre_filter_pair.into_inner().next().unwrap(); - let content_str : String = content.as_str().chars().filter(|c| !c.is_whitespace()).collect(); - let my_val : u32 = content_str.parse::().unwrap(); - pre_filters.push(HibouPreFilter::MaxProcessDepth(my_val)); - }, - Rule::OPTION_PREFILTER_MAX_LOOP_DEPTH => { - let content = pre_filter_pair.into_inner().next().unwrap(); - let content_str : String = content.as_str().chars().filter(|c| !c.is_whitespace()).collect(); - let my_val : u32 = content_str.parse::().unwrap(); - pre_filters.push(HibouPreFilter::MaxLoopInstanciation(my_val)); - }, - Rule::OPTION_PREFILTER_MAX_NODE_NUMBER => { - let content = pre_filter_pair.into_inner().next().unwrap(); - let content_str : String = content.as_str().chars().filter(|c| !c.is_whitespace()).collect(); - let my_val : u32 = content_str.parse::().unwrap(); - pre_filters.push(HibouPreFilter::MaxNodeNumber(my_val)); - }, - _ => { - panic!("what rule then ? : {:?}", pre_filter_pair.as_rule() ); - } - } - } - }, - Rule::OPTION_ANALYSIS_KIND_DECL => { - if got_ana_kind { - return Err( HibouParsingError::HsfSetupError("several 'ana_kind=X' declared in the same '@X_option' section".to_string())); - } - got_ana_kind = true; - // *** - let ana_kind_pair = option_decl_pair.into_inner().next().unwrap(); - match ana_kind_pair.as_rule() { - Rule::OPTION_ANA_KIND_accept => { - ana_kind_opt = Some( AnalysisKind::Accept ); - }, - Rule::OPTION_ANA_KIND_prefix => { - ana_kind_opt = Some( AnalysisKind::Prefix ); - }, - Rule::OPTION_ANA_KIND_hide => { - ana_kind_opt = Some( AnalysisKind::Hide ); - }, - Rule::OPTION_ANA_KIND_simulate_prefix => { - ana_kind_opt = Some( AnalysisKind::Simulate(false) ); - }, - Rule::OPTION_ANA_KIND_simulate_slice => { - ana_kind_opt = Some( AnalysisKind::Simulate(true) ); - }, - _ => { - panic!("what rule then ? : {:?}", ana_kind_pair.as_rule() ); - } - } - }, - Rule::OPTION_GOAL_DECL => { - if got_goal { - return Err( HibouParsingError::HsfSetupError("several 'goal=X' declared in the same '@X_option' section".to_string())); - } - got_goal = true; - // *** - let goal_pair = option_decl_pair.into_inner().next().unwrap(); - match goal_pair.as_rule() { - Rule::OPTION_GOAL_pass => { - goal = Some( GlobalVerdict::Pass ); - }, - Rule::OPTION_GOAL_weakpass => { - goal = Some( GlobalVerdict::WeakPass ); - }, - Rule::OPTION_GOAL_none => { - goal = None; - }, - _ => { - panic!("what rule then ? : {:?}", goal_pair.as_rule() ); - } - } - }, - _ => { - panic!("what rule then ? : {:?}", option_decl_pair.as_rule() ); - } - } - } - match process_kind { - ProcessKind::Analyze => { - return Ok( HibouOptions::new(loggers,strategy,pre_filters,ana_kind_opt, local_analysis, goal,frontier_priorities) ); - }, - _ => { - return Ok( HibouOptions::new(loggers,strategy,pre_filters,None, None, None,frontier_priorities) ); - } - } -} \ No newline at end of file diff --git a/src/from_hfiles/proc_options/loggers.rs b/src/from_hfiles/proc_options/loggers.rs index 64cb9b3..fe2a9f1 100644 --- a/src/from_hfiles/proc_options/loggers.rs +++ b/src/from_hfiles/proc_options/loggers.rs @@ -96,6 +96,9 @@ pub fn parse_tracegen_logger(gen_ctx : &GeneralContext, let mut co_localizations = gen_ctx.get_trivial_partition(); for opt_pair in tracegen_logger_opts.into_inner() { match opt_pair.as_rule() { + Rule::TRACEGEN_LOGGER_terminal => { + generation = TracegenProcessLoggerGeneration::terminal; + }, Rule::TRACEGEN_LOGGER_exact => { generation = TracegenProcessLoggerGeneration::exact; }, diff --git a/src/from_hfiles/proc_options/opt_analyze.rs b/src/from_hfiles/proc_options/opt_analyze.rs index d1f91c1..c711d0d 100644 --- a/src/from_hfiles/proc_options/opt_analyze.rs +++ b/src/from_hfiles/proc_options/opt_analyze.rs @@ -37,7 +37,8 @@ use crate::loggers::graphic::graphic_logger::GraphicProcessLogger; use crate::from_hfiles::proc_options::loggers::parse_graphic_logger; use crate::process::abstract_proc::common::HibouSearchStrategy; -use crate::process::ana_proc::anakind::{AnalysisKind, UseLocalAnalysis}; +use crate::process::abstract_proc::manager::GenericProcessPriorities; +use crate::process::ana_proc::anakind::{AnalysisKind, SimulationActionCriterion, SimulationConfiguration, SimulationLoopCriterion, UseLocalAnalysis}; use crate::process::ana_proc::interface::conf::AnalysisConfig; use crate::process::ana_proc::interface::filter::AnalysisFilter; use crate::process::ana_proc::interface::logger::AnalysisLogger; @@ -50,7 +51,7 @@ pub struct HibouAnalyzeOptions { pub loggers : Vec>, pub strategy : HibouSearchStrategy, pub filters : Vec, - pub priorities : AnalysisPriorities, + pub priorities : GenericProcessPriorities, pub ana_kind : AnalysisKind, pub local_analysis : UseLocalAnalysis, pub goal : Option @@ -60,7 +61,7 @@ impl HibouAnalyzeOptions { pub fn new(loggers : Vec>, strategy : HibouSearchStrategy, filters : Vec, - priorities : AnalysisPriorities, + priorities : GenericProcessPriorities, ana_kind : AnalysisKind, local_analysis : UseLocalAnalysis, goal : Option) -> HibouAnalyzeOptions { @@ -72,16 +73,16 @@ impl HibouAnalyzeOptions { loggers:Vec::new(), strategy:HibouSearchStrategy::DFS, filters:Vec::new(), - priorities:AnalysisPriorities::default(), + priorities:GenericProcessPriorities::Specific(AnalysisPriorities::default()), ana_kind:AnalysisKind::Prefix, - local_analysis:UseLocalAnalysis::Yes, + local_analysis:UseLocalAnalysis::Yes(false), goal:Some(GlobalVerdict::WeakPass) }; } /* to be used recursively in global analyses when checking that its component local analysis are ok important to keep "local_analysis:UseLocalAnalysis::No" so we don't infinitely recurse!! */ - pub fn local_analyze() -> HibouAnalyzeOptions { + /*pub fn local_analyze() -> HibouAnalyzeOptions { return HibouAnalyzeOptions{ loggers:Vec::new(), strategy:HibouSearchStrategy::DFS, // of course DFS is better here @@ -91,7 +92,7 @@ impl HibouAnalyzeOptions { local_analysis:UseLocalAnalysis::No, // No so we don't infinitely recurse goal:Some(GlobalVerdict::WeakPass), // it suffices to have a prefix }; - } + }*/ } @@ -126,7 +127,7 @@ fn parse_filters(filters_decl_pair : Pair) -> Result,H return Ok(filters); } -fn parse_priorities(priorities_decl_pair : Pair) -> Result { +fn parse_specific_priorities(priorities_decl_pair : Pair) -> Result { let mut emission : i32 = 0; let mut reception : i32 = 0; let mut multi_rdv : i32 = 0; @@ -176,9 +177,9 @@ pub fn parse_analyze_options(option_pair : Pair, let mut loggers : Vec> = Vec::new(); let mut strategy : HibouSearchStrategy = HibouSearchStrategy::BFS; let mut filters : Vec = Vec::new(); - let mut priorities = AnalysisPriorities::default(); + let mut priorities : GenericProcessPriorities = GenericProcessPriorities::Specific(AnalysisPriorities::default()); let mut ana_kind = AnalysisKind::Prefix; - let mut local_analysis = UseLocalAnalysis::Yes; + let mut local_analysis = UseLocalAnalysis::Yes(false); let mut goal = Some(GlobalVerdict::WeakPass); // *** for option_decl_pair in option_pair.into_inner() { @@ -207,6 +208,9 @@ pub fn parse_analyze_options(option_pair : Pair, Rule::OPTION_STRATEGY_DFS => { strategy = HibouSearchStrategy::DFS; }, + Rule::OPTION_STRATEGY_HCS => { + strategy = HibouSearchStrategy::HCS; + }, _ => { panic!("what rule then ? : {:?}", strategy_pair.as_rule() ); } @@ -222,13 +226,24 @@ pub fn parse_analyze_options(option_pair : Pair, } } }, - Rule::OPTION_FRONTIER_PRIORITIES_DECL => { - match parse_priorities(option_decl_pair) { - Ok( got_priorities) => { - priorities = got_priorities; + Rule::OPTION_PRIORITIES_DECL => { + let inner : Pair = option_decl_pair.into_inner().next().unwrap(); + match inner.as_rule() { + Rule::OPTION_PRIORITY_SPECIFIC => { + match parse_specific_priorities(inner) { + Ok( got_priorities) => { + priorities = GenericProcessPriorities::Specific(got_priorities); + }, + Err(e) => { + return Err(e); + } + } }, - Err(e) => { - return Err(e); + Rule::OPTION_PRIORITY_RANDOM => { + priorities = GenericProcessPriorities::Random; + }, + _ => { + panic!("what rule then ? : {:?}", inner.as_rule() ); } } }, @@ -244,11 +259,26 @@ pub fn parse_analyze_options(option_pair : Pair, Rule::OPTION_ANA_KIND_hide => { ana_kind = AnalysisKind::Hide; }, - Rule::OPTION_ANA_KIND_simulate_prefix => { - ana_kind = AnalysisKind::Simulate(false); - }, - Rule::OPTION_ANA_KIND_simulate_slice => { - ana_kind = AnalysisKind::Simulate(true); + Rule::OPTION_ANA_KIND_simulate => { + let mut inner = ana_kind_pair.into_inner(); + match inner.next() { + None => { + ana_kind = AnalysisKind::Simulate( + SimulationConfiguration{sim_before:false, + loop_crit:SimulationLoopCriterion::MaxDepth, + act_crit:SimulationActionCriterion::None}); + }, + Some( sim_config_decl_pair) => { + match parse_simulation_config(sim_config_decl_pair) { + Ok( config) => { + ana_kind = AnalysisKind::Simulate(config); + }, + Err(e) => { + return Err(e); + } + } + } + } }, _ => { panic!("what rule then ? : {:?}", ana_kind_pair.as_rule() ); @@ -256,7 +286,10 @@ pub fn parse_analyze_options(option_pair : Pair, } }, Rule::OPTION_LOCANA_yes => { - local_analysis = UseLocalAnalysis::Yes; + local_analysis = UseLocalAnalysis::Yes(false); + }, + Rule::OPTION_LOCANA_onlyfront => { + local_analysis = UseLocalAnalysis::Yes(true); }, Rule::OPTION_LOCANA_no => { local_analysis = UseLocalAnalysis::No; @@ -286,4 +319,65 @@ pub fn parse_analyze_options(option_pair : Pair, // *** let hoptions = HibouAnalyzeOptions{loggers,strategy,filters,priorities,ana_kind,local_analysis,goal}; return Ok(hoptions); +} + + +fn parse_simulation_config(simu_config_decl_pair : Pair) -> Result { + let mut sim_before = false; + let mut loop_crit = SimulationLoopCriterion::MaxDepth; + let mut act_crit = SimulationActionCriterion::None; + // *** + for config_opt_pair in simu_config_decl_pair.into_inner() { + match config_opt_pair.as_rule() { + Rule::OPTION_ANA_SIMULATE_CONFIG_simbefore => { + sim_before = true; + }, + Rule::OPTION_ANA_SIMULATE_CONFIG_act => { + let inner : Pair = config_opt_pair.into_inner().next().unwrap(); + match inner.as_rule() { + Rule::OPTION_ANA_SIMULATE_CONFIG_crit_num => { + let content : Pair = inner.into_inner().next().unwrap(); + let content_str : String = content.as_str().chars().filter(|c| !c.is_whitespace()).collect(); + let my_val : u32 = content_str.parse::().unwrap(); + act_crit = SimulationActionCriterion::SpecificNum(my_val); + }, + Rule::OPTION_ANA_SIMULATE_CONFIG_crit_none => { + act_crit = SimulationActionCriterion::None; + }, + _ => { + panic!("what rule then ? : {:?}", inner.as_rule() ); + } + } + }, + Rule::OPTION_ANA_SIMULATE_CONFIG_loop => { + let inner : Pair = config_opt_pair.into_inner().next().unwrap(); + match inner.as_rule() { + Rule::OPTION_ANA_SIMULATE_CONFIG_crit_num => { + let content : Pair = inner.into_inner().next().unwrap(); + let content_str : String = content.as_str().chars().filter(|c| !c.is_whitespace()).collect(); + let my_val : u32 = content_str.parse::().unwrap(); + loop_crit = SimulationLoopCriterion::SpecificNum(my_val); + }, + Rule::OPTION_ANA_SIMULATE_CONFIG_crit_maxnum => { + loop_crit = SimulationLoopCriterion::MaxNum; + }, + Rule::OPTION_ANA_SIMULATE_CONFIG_crit_maxdepth => { + loop_crit = SimulationLoopCriterion::MaxDepth; + }, + Rule::OPTION_ANA_SIMULATE_CONFIG_crit_none => { + loop_crit = SimulationLoopCriterion::None; + }, + _ => { + panic!("what rule then ? : {:?}", inner.as_rule() ); + } + } + }, + _ => { + panic!("what rule then ? : {:?}", config_opt_pair.as_rule() ); + } + } + } + // *** + let config = SimulationConfiguration{sim_before,loop_crit,act_crit}; + return Ok(config); } \ No newline at end of file diff --git a/src/from_hfiles/proc_options/opt_explore.rs b/src/from_hfiles/proc_options/opt_explore.rs index 5a028a9..d1f0c86 100644 --- a/src/from_hfiles/proc_options/opt_explore.rs +++ b/src/from_hfiles/proc_options/opt_explore.rs @@ -37,6 +37,7 @@ use crate::loggers::graphic::graphic_logger::GraphicProcessLogger; use crate::from_hfiles::proc_options::loggers::{parse_graphic_logger, parse_tracegen_logger}; use crate::process::abstract_proc::common::HibouSearchStrategy; +use crate::process::abstract_proc::manager::GenericProcessPriorities; use crate::process::explo_proc::interface::conf::ExplorationConfig; use crate::process::explo_proc::interface::filter::ExplorationFilter; @@ -48,7 +49,7 @@ pub struct HibouExploreOptions { pub loggers : Vec>, pub strategy : HibouSearchStrategy, pub filters : Vec, - pub priorities : ExplorationPriorities + pub priorities : GenericProcessPriorities } @@ -57,7 +58,7 @@ impl HibouExploreOptions { pub fn new(loggers : Vec>, strategy : HibouSearchStrategy, filters : Vec, - priorities : ExplorationPriorities) -> HibouExploreOptions { + priorities : GenericProcessPriorities) -> HibouExploreOptions { return HibouExploreOptions{loggers,strategy,filters,priorities}; } @@ -65,7 +66,7 @@ impl HibouExploreOptions { return HibouExploreOptions::new(Vec::new(), HibouSearchStrategy::BFS, vec![ExplorationFilter::MaxLoopInstanciation(1)], - ExplorationPriorities::default()); + GenericProcessPriorities::Specific(ExplorationPriorities::default())); } } @@ -103,7 +104,10 @@ fn parse_filters(filters_decl_pair : Pair) -> Result) -> Result { + + + +fn parse_specific_priorities(priorities_decl_pair : Pair) -> Result { let mut emission : i32 = 0; let mut reception : i32 = 0; let mut multi_rdv : i32 = 0; @@ -146,7 +150,7 @@ pub fn parse_explore_options(gen_ctx: &GeneralContext, let mut loggers : Vec> = Vec::new(); let mut strategy : HibouSearchStrategy = HibouSearchStrategy::BFS; let mut filters : Vec = Vec::new(); - let mut priorities = ExplorationPriorities::default(); + let mut priorities : GenericProcessPriorities = GenericProcessPriorities::Specific(ExplorationPriorities::default()); // *** for option_decl_pair in option_pair.into_inner() { match option_decl_pair.as_rule() { @@ -184,6 +188,9 @@ pub fn parse_explore_options(gen_ctx: &GeneralContext, Rule::OPTION_STRATEGY_DFS => { strategy = HibouSearchStrategy::DFS; }, + Rule::OPTION_STRATEGY_HCS => { + strategy = HibouSearchStrategy::HCS; + }, _ => { panic!("what rule then ? : {:?}", strategy_pair.as_rule() ); } @@ -199,13 +206,24 @@ pub fn parse_explore_options(gen_ctx: &GeneralContext, } } }, - Rule::OPTION_FRONTIER_PRIORITIES_DECL => { - match parse_priorities(option_decl_pair) { - Ok( got_priorities) => { - priorities = got_priorities; + Rule::OPTION_PRIORITIES_DECL => { + let inner : Pair = option_decl_pair.into_inner().next().unwrap(); + match inner.as_rule() { + Rule::OPTION_PRIORITY_SPECIFIC => { + match parse_specific_priorities(inner) { + Ok( got_priorities) => { + priorities = GenericProcessPriorities::Specific(got_priorities); + }, + Err(e) => { + return Err(e); + } + } }, - Err(e) => { - return Err(e); + Rule::OPTION_PRIORITY_RANDOM => { + priorities = GenericProcessPriorities::Random; + }, + _ => { + panic!("what rule then ? : {:?}", inner.as_rule() ); } } }, diff --git a/src/from_hfiles/traces/htf_file.rs b/src/from_hfiles/traces/htf_file.rs index 61874e8..225de71 100644 --- a/src/from_hfiles/traces/htf_file.rs +++ b/src/from_hfiles/traces/htf_file.rs @@ -88,7 +88,7 @@ pub fn multitrace_from_text(multitrace_str : &String, gen_ctx.set_partition(vec![lifelines]); let unique_canal = AnalysableMultiTraceCanal::new(got_trace,false,false,0,0,0); let mut canals : Vec = vec![unique_canal]; - return Ok( AnalysableMultiTrace::new(canals,0) ); + return Ok( AnalysableMultiTrace::new(canals,0,0) ); } } }, @@ -117,7 +117,7 @@ pub fn multitrace_from_text(multitrace_str : &String, } } complete_canals_up_to_defined_lifelines(&mut canals,gen_ctx); - return Ok( AnalysableMultiTrace::new(canals,0) ); + return Ok( AnalysableMultiTrace::new(canals,0,0) ); }, _ => { panic!("what rule then ? : {:?}", first_pair.as_rule() ); diff --git a/src/loggers/graphic/glog_ana.rs b/src/loggers/graphic/glog_ana.rs index 3bceaba..c6693be 100644 --- a/src/loggers/graphic/glog_ana.rs +++ b/src/loggers/graphic/glog_ana.rs @@ -36,9 +36,11 @@ impl AnalysisLogger for GraphicProcessLogger { gen_ctx: &GeneralContext, interaction: &Interaction, remaining_multi_trace: &AnalysableMultiTrace, - is_simulation : bool) { + is_simulation : bool, + sim_crit_loop : bool, + sim_crit_act : bool) { self.initiate(); - self.write_interaction(gen_ctx,1, interaction, &Some(remaining_multi_trace), is_simulation); + self.write_interaction(gen_ctx,1, interaction, &Some(remaining_multi_trace), is_simulation, sim_crit_loop, sim_crit_act); } fn log_term(&mut self, @@ -56,7 +58,9 @@ impl AnalysisLogger for GraphicProcessLogger { sim_map: &HashMap, new_interaction: &Interaction, remaining_multi_trace: &AnalysableMultiTrace, - is_simulation : bool) { + is_simulation : bool, + sim_crit_loop : bool, + sim_crit_act : bool) { // *** self.write_firing(gen_ctx,new_state_id,action_position,executed_actions,consu_set,sim_map); // *** Transition To Firing @@ -66,7 +70,7 @@ impl AnalysisLogger for GraphicProcessLogger { self.write_edge(format!("i{:}", parent_state_id), format!("f{:}", new_state_id), tran_gv_options); } // *** Resulting Interaction Node - self.write_interaction(gen_ctx, new_state_id, new_interaction, &Some(remaining_multi_trace),is_simulation); + self.write_interaction(gen_ctx, new_state_id, new_interaction, &Some(remaining_multi_trace),is_simulation,sim_crit_loop,sim_crit_act); // *** Transition To Interaction Node { let mut tran_gv_options : GraphvizEdgeStyle = Vec::new(); @@ -94,7 +98,7 @@ impl AnalysisLogger for GraphicProcessLogger { self.write_edge(parent_interaction_node_name, format!("h{:}", new_state_id), tran_gv_options); } // *** Resulting Interaction Node - self.write_interaction(gen_ctx, new_state_id, hidden_interaction, &Some(remaining_multi_trace), false ); + self.write_interaction(gen_ctx, new_state_id, hidden_interaction, &Some(remaining_multi_trace), false,false,false ); // *** Transition To Interaction Node { let mut tran_gv_options : GraphvizEdgeStyle = Vec::new(); diff --git a/src/loggers/graphic/glog_explo.rs b/src/loggers/graphic/glog_explo.rs index f0fb6d8..3b13a23 100644 --- a/src/loggers/graphic/glog_explo.rs +++ b/src/loggers/graphic/glog_explo.rs @@ -28,7 +28,7 @@ impl ExplorationLogger for GraphicProcessLogger { fn log_init(&mut self, interaction: &Interaction, gen_ctx: &GeneralContext) { self.initiate(); - self.write_interaction(gen_ctx,1, interaction, &None, false); + self.write_interaction(gen_ctx,1, interaction, &None, false, false, false); } fn log_term(&mut self, options_as_str: &Vec) { @@ -51,7 +51,7 @@ impl ExplorationLogger for GraphicProcessLogger { self.write_edge(format!("i{:}", parent_state_id), format!("f{:}", new_state_id), tran_gv_options); } // *** Resulting Interaction Node - self.write_interaction(gen_ctx, new_state_id, new_interaction, &None, false); + self.write_interaction(gen_ctx, new_state_id, new_interaction, &None, false, false, false); // *** Transition To Interaction Node { let mut tran_gv_options : GraphvizEdgeStyle = Vec::new(); @@ -64,7 +64,11 @@ impl ExplorationLogger for GraphicProcessLogger { self.write_filtered(parent_state_id,new_state_id,elim_kind); } - fn log_notified_lastchild_explored(&mut self, parent_id: u32) { + fn log_notified_lastchild_explored(&mut self, gen_ctx : &GeneralContext, parent_id: u32) { + // *** + } + + fn log_notified_terminal_node_explored(&mut self, gen_ctx : &GeneralContext, parent_id: u32) { // *** } } \ No newline at end of file diff --git a/src/loggers/graphic/graphic_logger.rs b/src/loggers/graphic/graphic_logger.rs index 0d1e909..a653509 100644 --- a/src/loggers/graphic/graphic_logger.rs +++ b/src/loggers/graphic/graphic_logger.rs @@ -158,10 +158,12 @@ impl GraphicProcessLogger { new_state_id : u32, new_interaction : &Interaction, remaining_multi_trace : &Option<&AnalysableMultiTrace>, - is_simulation : bool) { + is_simulation : bool, + sim_crit_loop : bool, + sim_crit_act : bool) { // *** let int_img_path : String = format!("./temp/{:}_i{}.png", self.log_name ,new_state_id); - draw_interaction(&int_img_path, new_interaction, gen_ctx, remaining_multi_trace, is_simulation); + draw_interaction(&int_img_path, new_interaction, gen_ctx, remaining_multi_trace, is_simulation, sim_crit_loop, sim_crit_act); // *** let mut node_gv_options : GraphvizNodeStyle = Vec::new(); node_gv_options.push( GraphvizNodeStyleItem::Image( int_img_path ) ); diff --git a/src/loggers/graphic/verdict.rs b/src/loggers/graphic/verdict.rs index d643e96..775a44f 100644 --- a/src/loggers/graphic/verdict.rs +++ b/src/loggers/graphic/verdict.rs @@ -34,20 +34,14 @@ impl CoverageVerdict { CoverageVerdict::Slice => { return GraphvizColor::darkorchid3; // 154 50 205 }, - CoverageVerdict::Inconc => { + CoverageVerdict::Inconc(_) => { return GraphvizColor::deeppink3; // 205 16 118 }, - CoverageVerdict::LackObs => { - return GraphvizColor::orangered3; // 205 55 0 - }, - CoverageVerdict::Dead => { - return GraphvizColor::firebrick; // 178 34 34 - }, - CoverageVerdict::Out => { + CoverageVerdict::Out(_) => { return GraphvizColor::red3; // 205 0 0 }, - CoverageVerdict::UnCov => { - return GraphvizColor::red3; + CoverageVerdict::OutSim(_) => { + return GraphvizColor::crimson; } } } diff --git a/src/loggers/tracegen/conf.rs b/src/loggers/tracegen/conf.rs index 5a05dd1..b36c682 100644 --- a/src/loggers/tracegen/conf.rs +++ b/src/loggers/tracegen/conf.rs @@ -20,6 +20,8 @@ pub enum TracegenProcessLoggerGeneration { // i.e. at each new node verify express empty and if it is the case generate prefixes, // generate a trace file for each global prefixes // i.e. at each new node generate + terminal // generate a trace file only when reaching a terminal node i.e. a node that has no child + // this can be due to e.g. a stopping criterion etc. /* multipref, // generate a trace file for all multiprefixes // works as "exact" but then, reload traces and generate prefixes diff --git a/src/loggers/tracegen/tlog_explo.rs b/src/loggers/tracegen/tlog_explo.rs index 0320590..896051d 100644 --- a/src/loggers/tracegen/tlog_explo.rs +++ b/src/loggers/tracegen/tlog_explo.rs @@ -55,6 +55,9 @@ impl ExplorationLogger for TraceGenProcessLogger { }, TracegenProcessLoggerGeneration::prefixes => { generate_trace_file = true; + }, + TracegenProcessLoggerGeneration::terminal => { + generate_trace_file = false; } } // *** @@ -67,7 +70,22 @@ impl ExplorationLogger for TraceGenProcessLogger { // *** } - fn log_notified_lastchild_explored(&mut self, parent_id: u32) { + fn log_notified_lastchild_explored(&mut self, + gen_ctx: &GeneralContext, + parent_id: u32) { self.trace_map.remove(&parent_id); } + + fn log_notified_terminal_node_explored(&mut self, + gen_ctx: &GeneralContext, + parent_id: u32) { + match self.generation { + TracegenProcessLoggerGeneration::terminal => { + self.generate_trace_file(gen_ctx,parent_id); + }, + _ => { + // nothing + } + } + } } \ No newline at end of file diff --git a/src/main.rs b/src/main.rs index 056f59c..2fc4d22 100644 --- a/src/main.rs +++ b/src/main.rs @@ -36,6 +36,8 @@ extern crate clap; #[macro_use] extern crate maplit; +extern crate rand; + // ********** pub mod core; diff --git a/src/process/abstract_proc/common.rs b/src/process/abstract_proc/common.rs index 395edc2..19027ec 100644 --- a/src/process/abstract_proc/common.rs +++ b/src/process/abstract_proc/common.rs @@ -42,18 +42,22 @@ impl std::string::ToString for FilterEliminationKind { pub enum HibouSearchStrategy { - BFS, - DFS + BFS, // breadth first search + DFS, // depth first search + HCS // high coverage search } impl std::string::ToString for HibouSearchStrategy { fn to_string(&self) -> String { match self { HibouSearchStrategy::BFS => { - return "BreadthFS".to_string(); + return "BreadthFirstSearch".to_string(); }, HibouSearchStrategy::DFS => { - return "DepthFS".to_string(); + return "DepthFirstSearch".to_string(); + }, + HibouSearchStrategy::HCS => { + return "HighCoverageSearch".to_string(); } } } diff --git a/src/process/abstract_proc/generic.rs b/src/process/abstract_proc/generic.rs index e498548..647e5fe 100644 --- a/src/process/abstract_proc/generic.rs +++ b/src/process/abstract_proc/generic.rs @@ -15,15 +15,13 @@ limitations under the License. */ -use std::cmp::Reverse; + use std::collections::{HashMap, HashSet}; use std::ops::DerefMut; use crate::core::general_context::GeneralContext; use crate::process::abstract_proc::common::{FilterEliminationKind, HibouSearchStrategy}; - - pub trait AbstractConfiguration : Sized { type NodeKind : AbstractNodeKind; type StepKind : AbstractStepKind; @@ -40,9 +38,6 @@ pub trait AbstractPriorities : Sized { } - - - pub trait AbstractStepKind : Sized { fn get_priority(&self, process_priorities : &Config::Priorities) -> i32; @@ -78,125 +73,3 @@ impl GenericStep { return GenericStep{parent_id,id_as_child,kind}; } } - -pub struct GenericProcessManager { - pub gen_ctx : GeneralContext, - strategy : HibouSearchStrategy, - filters : Vec, - priorities : Config::Priorities, - memorized_states : HashMap>, - process_queue : Vec>, - pub loggers: Vec -} - -impl GenericProcessManager { - - pub fn new(gen_ctx : GeneralContext, - strategy : HibouSearchStrategy, - filters : Vec, - priorities : Config::Priorities, - /*memorized_states : HashMap>, - process_queue : Vec>,*/ - loggers : Vec) -> GenericProcessManager { - return GenericProcessManager{gen_ctx,strategy,filters,priorities,memorized_states:hashmap!{},process_queue:vec![],loggers}; - } - - pub fn pick_memorized_state(&mut self, id:u32) -> GenericNode { - return self.memorized_states.remove(&id).unwrap(); - } - - pub fn remember_state(&mut self, id:u32, state : GenericNode) { - assert!(!self.memorized_states.contains_key(&id)); - self.memorized_states.insert( id, state ); - } - - pub fn extract_from_queue(&mut self) -> Option> { - if self.process_queue.len() > 0 { - return Some( self.process_queue.remove(0) ); - } else { - return None; - } - } - - pub fn apply_filters(&self, depth : u32, node_counter : u32, criterion : &Config::FilterCriterion) -> Option { - for filter in &self.filters { - match filter.apply_filter(depth,node_counter,criterion) { - None => {}, - Some( elim_kind) => { - return Some(elim_kind); - } - } - } - return None; - } - - pub fn enqueue_new_steps(&mut self, - parent_id : u32, - to_enqueue : Vec>, - node_depth : u32) { - let mut to_enqueue_reorganized : Vec> = Vec::new(); - { - let mut to_enqueue_reorganize_by_priorities : HashMap>> = HashMap::new(); - for child in to_enqueue { - let priority = child.kind.get_priority(&self.priorities); - // *** - match to_enqueue_reorganize_by_priorities.get_mut(&priority) { - None => { - to_enqueue_reorganize_by_priorities.insert(priority,vec![ child ]); - }, - Some( queue ) => { - queue.push(child ); - } - } - } - // *** - let mut keys : Vec = to_enqueue_reorganize_by_priorities.keys().cloned().collect(); - keys.sort_by_key(|k| Reverse(*k)); - for k in keys { - match to_enqueue_reorganize_by_priorities.get_mut(&k) { - None => {}, - Some( queue ) => { - for child in queue.drain(..) { - to_enqueue_reorganized.push( child ); - } - } - } - } - } - // *** - match &self.strategy { - &HibouSearchStrategy::DFS => { - to_enqueue_reorganized.append(&mut self.process_queue); - self.process_queue = to_enqueue_reorganized; - }, - &HibouSearchStrategy::BFS => { - self.process_queue.append( &mut to_enqueue_reorganized ); - } - } - } - - pub fn get_basic_options_as_strings(&self) -> Vec { - let mut options_str : Vec = Vec::new(); - options_str.push( format!("strategy={}", &self.strategy.to_string()) ); - options_str.push( format!("priorities=[{}]", &self.priorities.print_as_string()) ); - { - let mut rem_filter = self.filters.len(); - let mut filters_str = "filters=[".to_string(); - for filter in &self.filters { - filters_str.push_str( &filter.to_string() ); - rem_filter = rem_filter - 1; - if rem_filter > 0 { - filters_str.push_str( "," ); - } - } - filters_str.push_str( "]" ); - options_str.push( filters_str ); - } - return options_str; - } -} - - - - - diff --git a/src/process/abstract_proc/manager.rs b/src/process/abstract_proc/manager.rs new file mode 100644 index 0000000..66074ee --- /dev/null +++ b/src/process/abstract_proc/manager.rs @@ -0,0 +1,194 @@ +/* +Copyright 2020 Erwan Mahe (github.com/erwanM974) + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +*/ + +use rand::thread_rng; +use std::cmp::Reverse; +use std::collections::HashMap; +use rand::seq::SliceRandom; +use crate::core::general_context::GeneralContext; +use crate::process::abstract_proc::common::{FilterEliminationKind, HibouSearchStrategy}; +use crate::process::abstract_proc::generic::*; +use crate::process::abstract_proc::queue::*; + + +pub enum GenericProcessPriorities { + Random, + Specific(Config::Priorities) +} + +impl GenericProcessPriorities { + pub fn print_as_string(&self) -> String { + match self { + GenericProcessPriorities::Random => { + return "random".to_string(); + }, + GenericProcessPriorities::Specific(spec_prio) => { + return spec_prio.print_as_string(); + } + } + } +} + +pub struct GenericProcessManager { + pub gen_ctx : GeneralContext, + strategy : HibouSearchStrategy, + filters : Vec, + priorities : GenericProcessPriorities, + memorized_states : HashMap>, + process_queue : Box< dyn GenericProcessQueue >, + pub loggers: Vec +} + +impl GenericProcessManager { + + pub fn new(gen_ctx : GeneralContext, + strategy : HibouSearchStrategy, + filters : Vec, + priorities : GenericProcessPriorities, + loggers : Vec) -> GenericProcessManager { + let process_queue : Box< dyn GenericProcessQueue >; + match &strategy { + HibouSearchStrategy::BFS => { + process_queue = Box::new(BFS_ProcessQueue::::new() ); + }, + HibouSearchStrategy::DFS => { + process_queue = Box::new(DFS_ProcessQueue::::new() ); + }, + HibouSearchStrategy::HCS => { + process_queue = Box::new(HCS_ProcessQueue::::new() ); + } + } + return GenericProcessManager{gen_ctx, + strategy, + filters, + priorities, + memorized_states:hashmap!{}, + process_queue, + loggers}; + } + + pub fn pick_memorized_state(&mut self, id:u32) -> GenericNode { + return self.memorized_states.remove(&id).unwrap(); + } + + pub fn remember_state(&mut self, id:u32, state : GenericNode) { + assert!(!self.memorized_states.contains_key(&id)); + self.memorized_states.insert( id, state ); + } + + pub fn extract_from_queue(&mut self) -> Option> { + match self.process_queue.extract_from_queue() { + None => { + return None; + }, + Some( (step,_) ) => { + return Some(step); + } + } + } + + pub fn apply_filters(&self, + depth : u32, + node_counter : u32, + criterion : &Config::FilterCriterion) -> Option { + for filter in &self.filters { + match filter.apply_filter(depth,node_counter,criterion) { + None => {}, + Some( elim_kind) => { + return Some(elim_kind); + } + } + } + return None; + } + + fn reorganize_by_priority(priorities : &Config::Priorities, to_enqueue : Vec>) -> Vec> { + let mut to_enqueue_reorganized : Vec> = Vec::new(); + { + let mut to_enqueue_reorganize_by_priorities : HashMap>> = HashMap::new(); + for child in to_enqueue { + let priority = child.kind.get_priority(priorities); + // *** + match to_enqueue_reorganize_by_priorities.get_mut(&priority) { + None => { + to_enqueue_reorganize_by_priorities.insert(priority,vec![ child ]); + }, + Some( queue ) => { + queue.push(child ); + } + } + } + // *** + let mut keys : Vec = to_enqueue_reorganize_by_priorities.keys().cloned().collect(); + keys.sort(); + for k in keys { + match to_enqueue_reorganize_by_priorities.get_mut(&k) { + None => {}, + Some( queue ) => { + to_enqueue_reorganized.append( queue ); + } + } + } + } + return to_enqueue_reorganized; + } + + pub fn queue_set_last_reached_has_no_child(&mut self) { + self.process_queue.set_last_reached_has_no_child(); + } + + pub fn enqueue_new_steps(&mut self, + parent_id : u32, + to_enqueue : Vec>, + node_depth : u32) { + match &self.priorities { + GenericProcessPriorities::Random => { + let mut new_steps = to_enqueue; + new_steps.shuffle(&mut thread_rng()); + self.process_queue.enqueue_new_steps(parent_id,new_steps); + }, + GenericProcessPriorities::Specific(priorities) => { + let to_enqueue_reorganized = GenericProcessManager::reorganize_by_priority(priorities,to_enqueue); + self.process_queue.enqueue_new_steps(parent_id,to_enqueue_reorganized); + } + } + } + + pub fn get_basic_options_as_strings(&self) -> Vec { + let mut options_str : Vec = Vec::new(); + options_str.push( format!("strategy={}", &self.strategy.to_string()) ); + options_str.push( format!("priorities={}", &self.priorities.print_as_string()) ); + { + let mut rem_filter = self.filters.len(); + let mut filters_str = "filters=[".to_string(); + for filter in &self.filters { + filters_str.push_str( &filter.to_string() ); + rem_filter = rem_filter - 1; + if rem_filter > 0 { + filters_str.push_str( "," ); + } + } + filters_str.push_str( "]" ); + options_str.push( filters_str ); + } + return options_str; + } +} + + + + + diff --git a/src/process/abstract_proc/mod.rs b/src/process/abstract_proc/mod.rs index 9877fcd..e19029f 100644 --- a/src/process/abstract_proc/mod.rs +++ b/src/process/abstract_proc/mod.rs @@ -16,3 +16,5 @@ limitations under the License. pub mod generic; pub mod common; +pub mod queue; +pub mod manager; diff --git a/src/process/abstract_proc/queue.rs b/src/process/abstract_proc/queue.rs new file mode 100644 index 0000000..3f19baf --- /dev/null +++ b/src/process/abstract_proc/queue.rs @@ -0,0 +1,234 @@ +/* +Copyright 2020 Erwan Mahe (github.com/erwanM974) + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +*/ + + + + +use std::cmp::Reverse; +use std::collections::{HashMap, HashSet, VecDeque}; +use std::ops::DerefMut; +use crate::core::general_context::GeneralContext; +use crate::process::abstract_proc::common::{FilterEliminationKind, HibouSearchStrategy}; +use crate::process::abstract_proc::generic::*; + + +pub trait GenericProcessQueue { + + fn new() -> Self where Self : Sized; + + /** returns a next step to execute + and if the parent state from which this step is fired + has no other child left + then return its ID + so that we may then forget it / erase from memory + **/ + fn extract_from_queue(&mut self) -> Option<(GenericStep,Option)>; + + fn enqueue_new_steps(&mut self, + parent_id : u32, + to_enqueue : Vec>); + + fn set_last_reached_has_no_child(&mut self); + +} + + +pub struct BFS_ProcessQueue { + queue : VecDeque< (u32,Vec>) > +} + +impl GenericProcessQueue for BFS_ProcessQueue { + + fn new() -> BFS_ProcessQueue { + return BFS_ProcessQueue{queue:VecDeque::new()}; + } + + fn extract_from_queue(&mut self) -> Option<(GenericStep,Option)> { + match self.queue.pop_front() { + None => { + return None; + }, + Some( (parent_id,mut rem) ) => { + match rem.pop() { + None => { + panic!("should never have an empty vector here"); + }, + Some( got_step ) => { + if rem.len() > 0 { + self.queue.push_front((parent_id,rem) ); + return Some( (got_step,None) ); + } else { + return Some( (got_step,Some(parent_id)) ); + } + } + } + } + } + } + + fn enqueue_new_steps(&mut self, + parent_id : u32, + to_enqueue : Vec>) { + if to_enqueue.len() > 0 { + self.queue.push_back( (parent_id,to_enqueue) ); + } + } + + fn set_last_reached_has_no_child(&mut self) {} + +} + + + + +pub struct DFS_ProcessQueue { + queue : Vec< (u32,Vec>) > +} + +impl GenericProcessQueue for DFS_ProcessQueue { + + fn new() -> DFS_ProcessQueue { + return DFS_ProcessQueue{queue:Vec::new()}; + } + + fn extract_from_queue(&mut self) -> Option<(GenericStep,Option)> { + match self.queue.pop() { + None => { + return None; + }, + Some( (parent_id,mut rem) ) => { + match rem.pop() { + None => { + panic!("should never have an empty vector here"); + }, + Some( got_step ) => { + if rem.len() > 0 { + self.queue.push((parent_id,rem) ); + return Some( (got_step,None) ); + } else { + return Some( (got_step,Some(parent_id)) ); + } + } + } + } + } + } + + fn enqueue_new_steps(&mut self, + parent_id : u32, + to_enqueue : Vec>) { + if to_enqueue.len() > 0 { + self.queue.push( (parent_id,to_enqueue) ); + } + } + + fn set_last_reached_has_no_child(&mut self) {} +} + + + + + + +pub struct HCS_ProcessQueue { + queue : VecDeque< (u32,Vec>) >, + last_reached_has_no_child : bool +} + + +impl HCS_ProcessQueue { + + fn extract_DFS(&mut self) -> Option<(GenericStep,Option)> { + match self.queue.pop_back() { + None => { + return None; + }, + Some( (parent_id,mut rem) ) => { + match rem.pop() { + None => { + panic!("should never have an empty vector here"); + }, + Some( got_step ) => { + if rem.len() > 0 { + self.queue.push_back((parent_id,rem) ); + return Some( (got_step,None) ); + } else { + return Some( (got_step,Some(parent_id)) ); + } + } + } + } + } + } + + fn extract_BFS(&mut self) -> Option<(GenericStep,Option)> { + match self.queue.pop_front() { + None => { + return None; + }, + Some( (parent_id,mut rem) ) => { + match rem.pop() { + None => { + panic!("should never have an empty vector here"); + }, + Some( got_step ) => { + if rem.len() > 0 { + self.queue.push_front((parent_id,rem) ); + return Some( (got_step,None) ); + } else { + return Some( (got_step,Some(parent_id)) ); + } + } + } + } + } + } + +} + +impl GenericProcessQueue for HCS_ProcessQueue { + + fn new() -> HCS_ProcessQueue { + return HCS_ProcessQueue{queue:VecDeque::new(), + last_reached_has_no_child:true}; + } + + fn extract_from_queue(&mut self) -> Option<(GenericStep,Option)> { + match self.last_reached_has_no_child { + true => { + self.last_reached_has_no_child = false; + return self.extract_BFS(); + }, + false => { + return self.extract_DFS(); + } + } + } + + fn enqueue_new_steps(&mut self, + parent_id : u32, + to_enqueue : Vec>) { + if to_enqueue.len() > 0 { + self.queue.push_back( (parent_id,to_enqueue) ); + } + } + + fn set_last_reached_has_no_child(&mut self) { + self.last_reached_has_no_child = true; + } + +} + diff --git a/src/process/ana_proc/anakind.rs b/src/process/ana_proc/anakind.rs index 2f0a538..f037ef9 100644 --- a/src/process/ana_proc/anakind.rs +++ b/src/process/ana_proc/anakind.rs @@ -14,12 +14,174 @@ See the License for the specific language governing permissions and limitations under the License. */ +use crate::core::syntax::interaction::Interaction; + +#[derive(Clone, PartialEq, Debug)] +pub enum SimulationLoopCriterion { + MaxNum, + MaxDepth, + SpecificNum(u32), + None +} + +impl std::string::ToString for SimulationLoopCriterion { + fn to_string(&self) -> String { + match self { + SimulationLoopCriterion::MaxNum => { + return "maximum loop number".to_string(); + }, + SimulationLoopCriterion::MaxDepth => { + return "maximum loop depth".to_string(); + }, + SimulationLoopCriterion::SpecificNum(sn) => { + return format!("loop num : {:}", sn); + }, + SimulationLoopCriterion::None => { + return String::new(); + } + } + } +} + +#[derive(Clone, PartialEq, Debug)] +pub enum SimulationActionCriterion { + SpecificNum(u32), + None +} + +impl std::string::ToString for SimulationActionCriterion { + fn to_string(&self) -> String { + match self { + SimulationActionCriterion::SpecificNum(sn) => { + return format!("action num : {:}", sn); + }, + SimulationActionCriterion::None => { + return String::new(); + } + } + } +} + +#[derive(Clone, PartialEq, Debug)] +pub struct SimulationConfiguration { + pub sim_before : bool, + pub loop_crit : SimulationLoopCriterion, + pub act_crit : SimulationActionCriterion +} + +impl std::string::ToString for SimulationConfiguration { + fn to_string(&self) -> String { + return format!("sim_before : {:} | {:} | {:}", self.sim_before, self.loop_crit.to_string(), self.act_crit.to_string()); + } +} + +impl SimulationConfiguration { + + pub fn get_reset_rem_loop(&self, + interaction : &Interaction) -> u32 { + match self.loop_crit { + SimulationLoopCriterion::MaxDepth => { + return interaction.max_nested_loop_depth(); + }, + SimulationLoopCriterion::MaxNum => { + return interaction.total_loop_num(); + }, + SimulationLoopCriterion::SpecificNum( sn ) => { + return sn; + }, + SimulationLoopCriterion::None => { + return 0; + } + } + } + pub fn get_reset_rem_act(&self, + interaction : &Interaction) -> u32 { + match self.act_crit { + SimulationActionCriterion::SpecificNum( sn ) => { + return sn; + }, + SimulationActionCriterion::None => { + return 0; + } + } + } +} + #[derive(Clone, PartialEq, Debug)] pub enum AnalysisKind { Accept, Prefix, Hide, - Simulate(bool) + Simulate(SimulationConfiguration) +} + +impl AnalysisKind { + + pub fn get_sim_crits(&self) -> (bool,bool,bool) { + let has_simulation : bool; + let sim_crit_loop : bool; + let sim_crit_act : bool; + match self { + AnalysisKind::Simulate(config) => { + has_simulation = true; + match &config.loop_crit { + SimulationLoopCriterion::None => { + sim_crit_loop = false; + }, + _ => { + sim_crit_loop = true; + } + } + match &config.act_crit { + SimulationActionCriterion::None => { + sim_crit_act = false; + }, + _ => { + sim_crit_act = true; + } + } + }, + _ => { + has_simulation = false; + sim_crit_loop = false; + sim_crit_act = false; + } + } + return (has_simulation,sim_crit_loop,sim_crit_act); + } + + pub fn get_sim_config(&self) -> Option<&SimulationConfiguration> { + match self { + AnalysisKind::Simulate(config) => { + return Some(config); + }, + _ => { + return None; + } + } + } + + pub fn has_simulation(&self) -> bool { + match self { + AnalysisKind::Simulate(_) => { + return true; + }, + _ => { + return false; + } + } + } + + pub fn sim_before(&self) -> bool { + match self { + AnalysisKind::Simulate(config) => { + return config.sim_before; + }, + _ => { + return false; + } + } + } } @@ -35,12 +197,8 @@ impl std::string::ToString for AnalysisKind { AnalysisKind::Hide => { return "hide".to_string(); }, - AnalysisKind::Simulate(sim_before) => { - if *sim_before { - return "simulate multi-slices".to_string(); - } else { - return "simulate multi-prefixes".to_string(); - } + AnalysisKind::Simulate(sim_config) => { + return format!("simulate[{:}]", sim_config.to_string()); } } } @@ -51,8 +209,7 @@ impl std::string::ToString for AnalysisKind { #[derive(Clone, PartialEq, Debug)] pub enum UseLocalAnalysis { No, - OnlyFront, - Yes + Yes(bool) } @@ -62,11 +219,13 @@ impl std::string::ToString for UseLocalAnalysis { UseLocalAnalysis::No => { return "No".to_string(); }, - UseLocalAnalysis::OnlyFront => { - return "OnlyFront".to_string(); - }, - UseLocalAnalysis::Yes => { - return "Yes".to_string(); + UseLocalAnalysis::Yes(only_front) => { + if *only_front { + return "Only front".to_string(); + } + else { + return "Yes".to_string(); + } } } } diff --git a/src/process/ana_proc/interface/logger.rs b/src/process/ana_proc/interface/logger.rs index d813285..55a55bf 100644 --- a/src/process/ana_proc/interface/logger.rs +++ b/src/process/ana_proc/interface/logger.rs @@ -32,7 +32,9 @@ pub trait AnalysisLogger { gen_ctx : &GeneralContext, interaction : &Interaction, remaining_multi_trace : &AnalysableMultiTrace, - is_simulation : bool); + is_simulation : bool, + sim_crit_loop : bool, + sim_crit_act : bool); fn log_term(&mut self, options_as_str : &Vec); @@ -47,7 +49,9 @@ pub trait AnalysisLogger { sim_map : &HashMap, new_interaction : &Interaction, remaining_multi_trace : &AnalysableMultiTrace, - is_simulation : bool); + is_simulation : bool, + sim_crit_loop : bool, + sim_crit_act : bool); fn log_hide(&mut self, gen_ctx : &GeneralContext, diff --git a/src/process/ana_proc/local_analysis.rs b/src/process/ana_proc/local_analysis.rs index eaefa23..04d37a9 100644 --- a/src/process/ana_proc/local_analysis.rs +++ b/src/process/ana_proc/local_analysis.rs @@ -18,7 +18,9 @@ limitations under the License. use crate::core::general_context::GeneralContext; use crate::core::syntax::interaction::Interaction; use crate::process::abstract_proc::common::HibouSearchStrategy; +use crate::process::abstract_proc::manager::GenericProcessPriorities; use crate::process::ana_proc::anakind::{AnalysisKind, UseLocalAnalysis}; +use crate::process::ana_proc::interface::filter::AnalysisFilter; use crate::process::ana_proc::manager::AnalysisProcessManager; use crate::process::ana_proc::interface::priorities::AnalysisPriorities; use crate::process::ana_proc::multitrace::{AnalysableMultiTraceCanal,AnalysableMultiTrace}; @@ -30,10 +32,12 @@ pub fn is_dead_local_analysis(gen_ctx : &GeneralContext, interaction : &Interaction, multi_trace : &mut AnalysableMultiTrace) -> bool { match use_locana { - UseLocalAnalysis::No => {return false;}, - UseLocalAnalysis::Yes => { + UseLocalAnalysis::No => { + // nothing + }, + UseLocalAnalysis::Yes(only_front) => { for (canal_id,canal) in multi_trace.canals.iter_mut().enumerate() { - match perform_local_analysis(gen_ctx,parent_analysis_kind,interaction,canal_id,canal) { + match perform_local_analysis(gen_ctx,parent_analysis_kind,interaction,canal_id,canal,*only_front) { GlobalVerdict::Fail => { return true; }, @@ -42,12 +46,10 @@ pub fn is_dead_local_analysis(gen_ctx : &GeneralContext, } } } - return false; - }, - UseLocalAnalysis::OnlyFront => { - panic!("TODO implement"); + // nothing } } + return false; } @@ -55,7 +57,8 @@ fn perform_local_analysis(gen_ctx : &GeneralContext, parent_analysis_kind : &AnalysisKind, interaction : &Interaction, canal_id : usize, - canal : &AnalysableMultiTraceCanal) -> GlobalVerdict { + canal : &AnalysableMultiTraceCanal, + only_front : bool) -> GlobalVerdict { if canal.flag_dirty4local && canal.trace.len() > 0 { // *** let local_interaction : Interaction; @@ -77,14 +80,14 @@ fn perform_local_analysis(gen_ctx : &GeneralContext, 0, 0, 0) ); - local_mu = AnalysableMultiTrace::new(canals,0); + local_mu = AnalysableMultiTrace::new(canals,0,0); } // *** let local_analysis_kind : AnalysisKind; match parent_analysis_kind { - AnalysisKind::Simulate( sim_before ) => { - if *sim_before { - local_analysis_kind = AnalysisKind::Simulate(true); + AnalysisKind::Simulate( sim_config ) => { + if sim_config.sim_before { + local_analysis_kind = AnalysisKind::Simulate(sim_config.clone()); } else { local_analysis_kind = AnalysisKind::Prefix; } @@ -97,16 +100,22 @@ fn perform_local_analysis(gen_ctx : &GeneralContext, let mut new_gen_ctx= gen_ctx.clone(); new_gen_ctx.co_localizations = vec![ gen_ctx.co_localizations.get(canal_id).unwrap().clone() ]; // *** + let mut locana_filters : Vec = vec![]; + if only_front { + locana_filters.push( AnalysisFilter::MaxProcessDepth(1) ); + } + // *** let mut local_analysis_manager = AnalysisProcessManager::new(new_gen_ctx, HibouSearchStrategy::DFS, - vec![], - AnalysisPriorities::default(), + locana_filters, + GenericProcessPriorities::Specific(AnalysisPriorities::default()), vec![], local_analysis_kind, UseLocalAnalysis::No, Some(GlobalVerdict::WeakPass) ); - let (local_verdict,_) = local_analysis_manager.analyze(local_interaction,local_mu); + let local_int_characs = local_interaction.get_characteristics(); + let (local_verdict,_) = local_analysis_manager.analyze(local_interaction,local_int_characs,local_mu); return local_verdict; } else { return GlobalVerdict::Pass; diff --git a/src/process/ana_proc/manager.rs b/src/process/ana_proc/manager.rs index 0eea9e5..b8c7aa6 100644 --- a/src/process/ana_proc/manager.rs +++ b/src/process/ana_proc/manager.rs @@ -25,36 +25,38 @@ use crate::core::semantics::execute::execute_interaction; use crate::core::semantics::frontier::global_frontier; use crate::core::syntax::interaction::Interaction; use crate::core::syntax::position::Position; +use crate::core::syntax::util::check_interaction::InteractionCharacteristics; use crate::core::trace::{TraceAction}; use crate::process::ana_proc::multitrace::{AnalysableMultiTraceCanal, AnalysableMultiTrace, WasMultiTraceConsumedWithSimulation}; -use crate::process::abstract_proc::generic::{GenericNode, GenericProcessManager, GenericStep}; +use crate::process::abstract_proc::generic::*; +use crate::process::abstract_proc::manager::*; use crate::process::abstract_proc::common::{FilterEliminationKind, HibouSearchStrategy}; -use crate::process::ana_proc::anakind::{AnalysisKind, UseLocalAnalysis}; +use crate::process::ana_proc::anakind::{AnalysisKind, SimulationActionCriterion, SimulationLoopCriterion, UseLocalAnalysis}; use crate::process::ana_proc::interface::conf::AnalysisConfig; use crate::process::ana_proc::interface::filter::{AnalysisFilter, AnalysisFilterCriterion}; use crate::process::ana_proc::interface::logger::AnalysisLogger; use crate::process::ana_proc::local_analysis::is_dead_local_analysis; -use crate::process::ana_proc::matches::{add_action_matches_in_analysis, add_simulation_matches_in_analysis}; +use crate::process::ana_proc::matches::*; use crate::process::ana_proc::interface::step::{AnalysisStepKind, SimulationStepKind}; use crate::process::ana_proc::interface::node::AnalysisNodeKind; use crate::process::ana_proc::interface::priorities::AnalysisPriorities; -use crate::process::ana_proc::verdicts::{CoverageVerdict, GlobalVerdict, update_global_verdict_from_new_coverage_verdict}; +use crate::process::ana_proc::verdicts::{CoverageVerdict, GlobalVerdict, InconcReason, update_global_verdict_from_new_coverage_verdict}; use crate::rendering::textual::monochrome::multi_trace::multi_trace_as_text; pub struct AnalysisProcessManager { - manager: GenericProcessManager, - ana_kind : AnalysisKind, - use_locana : UseLocalAnalysis, - goal : Option, - is_simulation : bool + pub(crate) manager: GenericProcessManager, + pub(crate) ana_kind : AnalysisKind, + pub(crate) use_locana : UseLocalAnalysis, + pub(crate) goal : Option, + pub(crate) has_filtered_nodes : bool } impl AnalysisProcessManager { pub fn new(gen_ctx : GeneralContext, strategy : HibouSearchStrategy, filters : Vec, - priorities : AnalysisPriorities, + priorities : GenericProcessPriorities, loggers : Vec>, ana_kind : AnalysisKind, use_locana : UseLocalAnalysis, @@ -66,26 +68,21 @@ impl AnalysisProcessManager { priorities, loggers ); - let is_simulation : bool; - match &ana_kind { - &AnalysisKind::Simulate(_) => { - is_simulation = true; - }, - _ => { - is_simulation = false; - } - } - return AnalysisProcessManager{manager,ana_kind,use_locana,goal,is_simulation}; + return AnalysisProcessManager{manager,ana_kind,use_locana,goal,has_filtered_nodes:false}; } pub fn analyze(&mut self, interaction : Interaction, + int_characs : InteractionCharacteristics, got_multi_trace : AnalysableMultiTrace) -> (GlobalVerdict,u32) { // *** let mut multi_trace = got_multi_trace; match &self.ana_kind { - AnalysisKind::Simulate(_) => { - multi_trace.remaining_loop_instantiations_in_simulation = interaction.max_nested_loop_depth(); + AnalysisKind::Simulate( sim_config ) => { + let rem_loop_in_sim = sim_config.get_reset_rem_loop(&interaction); + let rem_act_in_sim = sim_config.get_reset_rem_act(&interaction); + multi_trace.rem_loop_in_sim = rem_loop_in_sim; + multi_trace.rem_act_in_sim = rem_act_in_sim; }, _ => {} } @@ -99,7 +96,7 @@ impl AnalysisProcessManager { // *** let pursue_analysis : bool; match self.enqueue_next_node_in_analysis(next_state_id, - interaction, + interaction,&int_characs, multi_trace, 0, 0) { @@ -142,6 +139,7 @@ impl AnalysisProcessManager { node_counter = node_counter + 1; match self.enqueue_next_node_in_analysis(new_state_id, new_interaction, + &int_characs, new_multi_trace, new_depth, new_loop_depth) { @@ -169,6 +167,10 @@ impl AnalysisProcessManager { } } // *** + if global_verdict == GlobalVerdict::Fail && self.has_filtered_nodes { + global_verdict = GlobalVerdict::Inconc(InconcReason::FilteredNodes); + } + // *** self.term_loggers(&global_verdict); // *** return (global_verdict,node_counter); @@ -177,6 +179,7 @@ impl AnalysisProcessManager { fn enqueue_next_node_in_analysis(&mut self, parent_id : u32, interaction : Interaction, + initial_int_characs : &InteractionCharacteristics, mut multi_trace : AnalysableMultiTrace, depth : u32, loop_depth : u32) -> Option { @@ -187,7 +190,12 @@ impl AnalysisProcessManager { if multi_trace.length() > 0 { // *** if is_dead_local_analysis(&self.manager.gen_ctx, &self.ana_kind,&self.use_locana,&interaction,&mut multi_trace) { - let verdict = CoverageVerdict::Dead; + let verdict : CoverageVerdict; + if self.ana_kind.has_simulation() { + verdict = CoverageVerdict::OutSim(true); + } else { + verdict = CoverageVerdict::Out(true); + } self.verdict_loggers(&verdict,parent_id); return Some( verdict ); } @@ -197,10 +205,10 @@ impl AnalysisProcessManager { // *** match &self.ana_kind { &AnalysisKind::Accept => { - add_action_matches_in_analysis(&self.manager.gen_ctx,parent_id,&interaction,&head_actions,&mut id_as_child, &mut to_enqueue); + self.add_action_matches_in_analysis(parent_id,&interaction,&head_actions,&mut id_as_child, &mut to_enqueue); }, &AnalysisKind::Prefix => { - add_action_matches_in_analysis(&self.manager.gen_ctx,parent_id,&interaction,&head_actions,&mut id_as_child, &mut to_enqueue); + self.add_action_matches_in_analysis(parent_id,&interaction,&head_actions,&mut id_as_child, &mut to_enqueue); }, &AnalysisKind::Hide => { let mut to_hide : HashSet = HashSet::new(); @@ -216,11 +224,11 @@ impl AnalysisProcessManager { let generic_step = GenericStep{parent_id,id_as_child:id_as_child,kind:AnalysisStepKind::Hide( to_hide )}; to_enqueue.push( generic_step ); } else { - add_action_matches_in_analysis(&self.manager.gen_ctx,parent_id,&interaction,&head_actions,&mut id_as_child, &mut to_enqueue); + self.add_action_matches_in_analysis(parent_id,&interaction,&head_actions,&mut id_as_child, &mut to_enqueue); } }, - &AnalysisKind::Simulate(sim_before) => { - add_simulation_matches_in_analysis(&self.manager.gen_ctx, parent_id,&interaction,&multi_trace,sim_before,&mut id_as_child, &mut to_enqueue); + &AnalysisKind::Simulate(_) => { + self.add_simulation_matches_in_analysis(parent_id, &interaction, &multi_trace,&mut id_as_child, &mut to_enqueue); } } } @@ -232,7 +240,12 @@ impl AnalysisProcessManager { self.manager.enqueue_new_steps( parent_id, to_enqueue, depth ); return None; } else { - let verdict = self.get_coverage_verdict(&interaction,&multi_trace); + // here enqueue the empty to_enqueue so that the queue for the HCS search strategy + // knows that the last node had no child and hence + // selects the highest parent in the next step instead of continuing on as in DFS + self.manager.enqueue_new_steps( parent_id, to_enqueue, depth ); + // *** + let verdict = self.get_coverage_verdict(initial_int_characs,&interaction,&multi_trace); self.verdict_loggers(&verdict,parent_id); return Some( verdict ); } @@ -281,19 +294,14 @@ impl AnalysisProcessManager { &frt_elt.position, &frt_elt.target_lf_ids, true); - let rem_sim_depth : u32; - if consu_set.len() > 0 { - rem_sim_depth = exe_result.interaction.max_nested_loop_depth(); - } else { - let new_max_ld = exe_result.interaction.max_nested_loop_depth(); - let removed = parent_state.kind.multi_trace.remaining_loop_instantiations_in_simulation - target_loop_depth; - rem_sim_depth = new_max_ld.min(removed); - } - let new_multi_trace = parent_state.kind.multi_trace.update_on_simulation(&self.manager.gen_ctx, + let new_multi_trace = parent_state.kind.multi_trace.update_on_simulation(self.ana_kind.get_sim_config().unwrap(), + consu_set, sim_map, + &self.manager.gen_ctx, &frt_elt.target_lf_ids, &exe_result.affected_lifelines, - rem_sim_depth); + target_loop_depth, + &exe_result.interaction); // *** self.execution_loggers(&frt_elt.position, &frt_elt.target_actions, @@ -318,8 +326,9 @@ impl AnalysisProcessManager { } pub fn get_coverage_verdict(&self, - interaction:&Interaction, - multi_trace:&AnalysableMultiTrace) -> CoverageVerdict { + initial_int_characs : &InteractionCharacteristics, + interaction : &Interaction, + multi_trace : &AnalysableMultiTrace) -> CoverageVerdict { if multi_trace.length() == 0 { if interaction.express_empty() { match self.ana_kind { @@ -334,7 +343,7 @@ impl AnalysisProcessManager { if self.manager.gen_ctx.are_colocalizations_singletons() { return CoverageVerdict::MultiPref; } else { - return CoverageVerdict::Inconc; + return CoverageVerdict::Inconc(InconcReason::HideWithColocs); } } else { return CoverageVerdict::Cov; @@ -354,10 +363,10 @@ impl AnalysisProcessManager { } } } - } else { + } else { /* multi-trace empty but interaction does not express empty */ match self.ana_kind { AnalysisKind::Accept => { - return CoverageVerdict::UnCov; + return CoverageVerdict::Out(false); }, AnalysisKind::Prefix => { return CoverageVerdict::TooShort; @@ -367,7 +376,7 @@ impl AnalysisProcessManager { if self.manager.gen_ctx.are_colocalizations_singletons() { return CoverageVerdict::MultiPref; } else { - return CoverageVerdict::Inconc; + return CoverageVerdict::Inconc(InconcReason::HideWithColocs); } } else { return CoverageVerdict::TooShort; @@ -388,31 +397,32 @@ impl AnalysisProcessManager { } } } - } else { + } else { /* multi-trace not emptied */ match self.ana_kind { AnalysisKind::Accept => { - return CoverageVerdict::UnCov; + return CoverageVerdict::Out(false); }, AnalysisKind::Prefix => { if multi_trace.is_any_component_empty() { - return CoverageVerdict::LackObs; + return CoverageVerdict::Inconc(InconcReason::LackObs); } else { - return CoverageVerdict::Out; + return CoverageVerdict::Out(false); } }, AnalysisKind::Hide => { - return CoverageVerdict::Out; + return CoverageVerdict::Out(false); }, AnalysisKind::Simulate(_) => { - return CoverageVerdict::Out; - }, + return CoverageVerdict::OutSim(false); + } } } } fn init_loggers(&mut self, interaction : &Interaction,remaining_multi_trace : &AnalysableMultiTrace) { + let (is_simulation,sim_crit_loop,sim_crit_act) = self.ana_kind.get_sim_crits(); for logger in self.manager.loggers.iter_mut() { - (*logger).log_init( &self.manager.gen_ctx, interaction,remaining_multi_trace,self.is_simulation); + (*logger).log_init( &self.manager.gen_ctx, interaction,remaining_multi_trace,is_simulation,sim_crit_loop,sim_crit_act); } } @@ -429,17 +439,7 @@ impl AnalysisProcessManager { let mut options_as_strs = (&self).manager.get_basic_options_as_strings(); options_as_strs.insert(0, "process=analysis".to_string()); options_as_strs.push( format!("analysis kind={}", self.ana_kind.to_string()) ); - match self.use_locana { - UseLocalAnalysis::No => { - options_as_strs.push("local_analysis=false".to_string()); - }, - UseLocalAnalysis::Yes => { - options_as_strs.push("local_analysis=true".to_string()); - }, - _ => { - panic!("TODO: implement") - } - } + options_as_strs.push( format!("local analysis={}", self.use_locana.to_string()) ); match self.goal.as_ref() { None => { options_as_strs.push( "goal=None".to_string() ); @@ -459,6 +459,7 @@ impl AnalysisProcessManager { parent_state_id : u32, new_state_id : u32, elim_kind : &FilterEliminationKind) { + self.has_filtered_nodes = true; for logger in self.manager.loggers.iter_mut() { logger.log_filtered(parent_state_id, new_state_id, @@ -475,6 +476,7 @@ impl AnalysisProcessManager { parent_state_id : u32, new_state_id :u32, remaining_multi_trace : &AnalysableMultiTrace) { + let (is_simulation,sim_crit_loop,sim_crit_act) = self.ana_kind.get_sim_crits(); for logger in self.manager.loggers.iter_mut() { logger.log_execution(&self.manager.gen_ctx, parent_state_id, @@ -485,7 +487,7 @@ impl AnalysisProcessManager { sim_map, new_interaction, remaining_multi_trace, - self.is_simulation); + is_simulation,sim_crit_loop,sim_crit_act); } } diff --git a/src/process/ana_proc/matches.rs b/src/process/ana_proc/matches.rs index bff9720..234dc0a 100644 --- a/src/process/ana_proc/matches.rs +++ b/src/process/ana_proc/matches.rs @@ -20,165 +20,179 @@ use std::convert::TryFrom; use std::iter::FromIterator; use crate::core::general_context::GeneralContext; -use crate::core::semantics::frontier::global_frontier; +use crate::core::semantics::frontier::{FrontierElement, global_frontier}; use crate::core::syntax::interaction::Interaction; use crate::core::trace::TraceAction; use crate::process::abstract_proc::generic::GenericStep; use crate::process::ana_proc::interface::conf::AnalysisConfig; use crate::process::ana_proc::interface::step::{AnalysisStepKind, SimulationStepKind}; +use crate::process::ana_proc::manager::AnalysisProcessManager; use crate::process::ana_proc::multitrace::AnalysableMultiTrace; use crate::util::powerset::powerset; +use crate::process::ana_proc::anakind::{AnalysisKind, SimulationActionCriterion, SimulationLoopCriterion, UseLocalAnalysis}; +impl AnalysisProcessManager { - -pub fn add_action_matches_in_analysis(gen_ctx : &GeneralContext, - parent_id : u32, - interaction : &Interaction, - head_actions : &HashSet<&TraceAction>, - id_as_child : &mut u32, - to_enqueue : &mut Vec>) { - // *** - for frt_elt in global_frontier(&interaction,&Some(head_actions)) { - *id_as_child = *id_as_child +1; - let mut canal_ids_of_targets : HashSet = hashset!{}; // ids of the canals of the actions part of the frontier element - for lf_id in &frt_elt.target_lf_ids { - canal_ids_of_targets.insert( gen_ctx.get_lf_coloc_id(*lf_id).unwrap() ); + pub fn is_ok_to_simulate(&self, + frt_elt : &FrontierElement, + interaction : &Interaction, + multi_trace : &AnalysableMultiTrace) -> bool { + match &self.ana_kind { + AnalysisKind::Simulate(ref config) => { + let mut ok_to_simulate = true; + match config.act_crit { + SimulationActionCriterion::None => { + // nothing + }, + _ => { + if multi_trace.rem_act_in_sim <= 0 { + ok_to_simulate = false; + } + } + } + match config.loop_crit { + SimulationLoopCriterion::None => { + // nothing + }, + _ => { + let loop_depth = interaction.get_loop_depth_at_pos(&frt_elt.position); + if loop_depth > multi_trace.rem_loop_in_sim { + ok_to_simulate = false; + } + } + } + return ok_to_simulate; + }, + _ => { + panic!(); + } } - let generic_step = GenericStep{parent_id, - id_as_child:*id_as_child, - kind:AnalysisStepKind::Simulate(frt_elt,canal_ids_of_targets,hashmap!{})}; - to_enqueue.push( generic_step ); } -} - - - - -pub fn add_simulation_matches_in_analysis(gen_ctx : &GeneralContext, - parent_id : u32, - interaction : &Interaction, - multi_trace : &AnalysableMultiTrace, - sim_before:bool, - next_child_id : &mut u32, - to_enqueue : &mut Vec>) { - // *** - for frt_elt in global_frontier(&interaction,&None) { - let mut canal_ids_of_targets : HashSet = hashset!{}; // ids of the canals of the actions part of the frontier element - for lf_id in &frt_elt.target_lf_ids { - canal_ids_of_targets.insert( gen_ctx.get_lf_coloc_id(*lf_id).unwrap() ); - } + pub fn add_simulation_matches_in_analysis(&self, + parent_id : u32, + interaction : &Interaction, + multi_trace : &AnalysableMultiTrace, + next_child_id : &mut u32, + to_enqueue : &mut Vec>) { // *** - let mut match_on_canal : Vec = vec!{}; // ids of the canals on which there is a match - let mut ok_canals : HashSet = hashset!{}; // canals in which we already do something match or simu - let mut act_left_to_match : HashSet<&TraceAction> = frt_elt.target_actions.iter().collect(); - for (canal_id, canal) in multi_trace.canals.iter().enumerate() { - match canal.trace.get(0) { - None => {}, - Some( got_multiact ) => { - let mut intersect_with_front_elt = false; - let mut entirely_included_in_front_elt = true; - for got_act in got_multiact { - if act_left_to_match.contains(got_act) { - intersect_with_front_elt = true; - } else { - entirely_included_in_front_elt = false; - } - } - // *** - if intersect_with_front_elt && entirely_included_in_front_elt { - match_on_canal.push(canal_id ); - ok_canals.insert(canal_id); + for frt_elt in global_frontier(&interaction,&None) { + let mut canal_ids_of_targets : HashSet = hashset!{}; // ids of the canals of the actions part of the frontier element + for lf_id in &frt_elt.target_lf_ids { + canal_ids_of_targets.insert( self.manager.gen_ctx.get_lf_coloc_id(*lf_id).unwrap() ); + } + // *** + let mut match_on_canal : Vec = vec!{}; // ids of the canals on which there is a match + let mut ok_canals : HashSet = hashset!{}; // canals in which we already do something match or simu + let mut act_left_to_match : HashSet<&TraceAction> = frt_elt.target_actions.iter().collect(); + for (canal_id, canal) in multi_trace.canals.iter().enumerate() { + match canal.trace.get(0) { + None => {}, + Some( got_multiact ) => { + let mut intersect_with_front_elt = false; + let mut entirely_included_in_front_elt = true; for got_act in got_multiact { - act_left_to_match.remove(got_act); + if act_left_to_match.contains(got_act) { + intersect_with_front_elt = true; + } else { + entirely_included_in_front_elt = false; + } + } + // *** + if intersect_with_front_elt && entirely_included_in_front_elt { + match_on_canal.push(canal_id ); + ok_canals.insert(canal_id); + for got_act in got_multiact { + act_left_to_match.remove(got_act); + } } } } } - } - if multi_trace.length() > 0 { - let mut to_simulate : HashMap = hashmap!{}; // id of the canal on which the simulation step is done, which kind of simulation step - let mut ok_to_simulate = true; - if act_left_to_match.len() > 0 && interaction.get_loop_depth_at_pos(&frt_elt.position) > multi_trace.remaining_loop_instantiations_in_simulation { - ok_to_simulate = false; - } - for tract in act_left_to_match { - if !ok_to_simulate { - break; + if multi_trace.length() > 0 { + let mut to_simulate : HashMap = hashmap!{}; // id of the canal on which the simulation step is done, which kind of simulation step + let mut ok_to_simulate = true; + if act_left_to_match.len() > 0 { + ok_to_simulate = self.is_ok_to_simulate(&frt_elt,interaction,multi_trace); } - let tract_coloc_id = gen_ctx.get_lf_coloc_id(tract.lf_id).unwrap(); - if ok_canals.contains(&tract_coloc_id) { - println!("analysis line 101 : an action left to simulate on a coloc on which we already do some match-execution"); - } else { - let mut gotit = false; - for (canal_id, canal) in multi_trace.canals.iter().enumerate() { - let canal_lifelines = gen_ctx.co_localizations.get(canal_id).unwrap(); - if canal_lifelines.contains(&tract.lf_id) { - if canal.trace.len() == 0 { - to_simulate.insert( canal_id, SimulationStepKind::AfterEnd); - gotit = true; - break; - } else { - if sim_before && (canal.consumed == 0) { - to_simulate.insert(canal_id,SimulationStepKind::BeforeStart); + for tract in act_left_to_match { + if !ok_to_simulate { + break; + } + let tract_coloc_id = self.manager.gen_ctx.get_lf_coloc_id(tract.lf_id).unwrap(); + if ok_canals.contains(&tract_coloc_id) { + println!("analysis line 101 : an action left to simulate on a coloc on which we already do some match-execution"); + } else { + let mut gotit = false; + for (canal_id, canal) in multi_trace.canals.iter().enumerate() { + let canal_lifelines = self.manager.gen_ctx.co_localizations.get(canal_id).unwrap(); + if canal_lifelines.contains(&tract.lf_id) { + if canal.trace.len() == 0 { + to_simulate.insert( canal_id, SimulationStepKind::AfterEnd); gotit = true; break; + } else { + if self.ana_kind.sim_before() && (canal.consumed == 0) { + to_simulate.insert(canal_id,SimulationStepKind::BeforeStart); + gotit = true; + break; + } } } } - } - if !gotit { - ok_to_simulate = false; + if !gotit { + ok_to_simulate = false; + } } } - } - if ok_to_simulate { - { - *next_child_id = *next_child_id +1; - let consu_set : HashSet; + if ok_to_simulate { { - let simu_set : HashSet = HashSet::from_iter(to_simulate.keys().cloned()); - consu_set = HashSet::from_iter( canal_ids_of_targets.difference( &simu_set ).cloned() ); + *next_child_id = *next_child_id +1; + let consu_set : HashSet; + { + let simu_set : HashSet = HashSet::from_iter(to_simulate.keys().cloned()); + consu_set = HashSet::from_iter( canal_ids_of_targets.difference( &simu_set ).cloned() ); + } + let generic_step = GenericStep{parent_id, + id_as_child:*next_child_id, + kind:AnalysisStepKind::Simulate(frt_elt.clone(),consu_set, + to_simulate.clone())}; + to_enqueue.push( generic_step ); } - let generic_step = GenericStep{parent_id, - id_as_child:*next_child_id, - kind:AnalysisStepKind::Simulate(frt_elt.clone(),consu_set, - to_simulate.clone())}; - to_enqueue.push( generic_step ); - } - if match_on_canal.len() > 0 && interaction.get_loop_depth_at_pos(&frt_elt.position) <= multi_trace.remaining_loop_instantiations_in_simulation { - for combinations in powerset(&match_on_canal) { - if combinations.len() > 0 { - let mut ok_to_simulate = true; - let mut to_simulate_more = to_simulate.clone(); - for canal_id in combinations { - if !ok_to_simulate{ - break; - } - let canal = multi_trace.canals.get(canal_id).unwrap(); - if canal.trace.len() == 0 { - to_simulate_more.insert( canal_id, SimulationStepKind::AfterEnd); - } else { - if sim_before && (canal.consumed == 0) { - to_simulate_more.insert(canal_id,SimulationStepKind::BeforeStart); + if match_on_canal.len() > 0 && self.is_ok_to_simulate(&frt_elt,interaction,multi_trace) { + for combinations in powerset(&match_on_canal) { + if combinations.len() > 0 { + let mut ok_to_simulate = true; + let mut to_simulate_more = to_simulate.clone(); + for canal_id in combinations { + if !ok_to_simulate{ + break; + } + let canal = multi_trace.canals.get(canal_id).unwrap(); + if canal.trace.len() == 0 { + to_simulate_more.insert( canal_id, SimulationStepKind::AfterEnd); } else { - ok_to_simulate = false; + if self.ana_kind.sim_before() && (canal.consumed == 0) { + to_simulate_more.insert(canal_id,SimulationStepKind::BeforeStart); + } else { + ok_to_simulate = false; + } } } - } - if ok_to_simulate { - { - *next_child_id = *next_child_id +1; - let consu_set : HashSet; + if ok_to_simulate { { - let simu_set : HashSet = HashSet::from_iter(to_simulate_more.keys().cloned()); - consu_set = HashSet::from_iter( canal_ids_of_targets.difference( &simu_set ).cloned() ); + *next_child_id = *next_child_id +1; + let consu_set : HashSet; + { + let simu_set : HashSet = HashSet::from_iter(to_simulate_more.keys().cloned()); + consu_set = HashSet::from_iter( canal_ids_of_targets.difference( &simu_set ).cloned() ); + } + let generic_step = GenericStep{parent_id, + id_as_child:*next_child_id, + kind:AnalysisStepKind::Simulate(frt_elt.clone(),consu_set, + to_simulate_more.clone())}; + to_enqueue.push( generic_step ); } - let generic_step = GenericStep{parent_id, - id_as_child:*next_child_id, - kind:AnalysisStepKind::Simulate(frt_elt.clone(),consu_set, - to_simulate_more.clone())}; - to_enqueue.push( generic_step ); } } } @@ -187,5 +201,31 @@ pub fn add_simulation_matches_in_analysis(gen_ctx : &GeneralContext, } } } + + + pub fn add_action_matches_in_analysis(&self, + parent_id : u32, + interaction : &Interaction, + head_actions : &HashSet<&TraceAction>, + id_as_child : &mut u32, + to_enqueue : &mut Vec>) { + // *** + for frt_elt in global_frontier(&interaction,&Some(head_actions)) { + *id_as_child = *id_as_child +1; + let mut canal_ids_of_targets : HashSet = hashset!{}; // ids of the canals of the actions part of the frontier element + for lf_id in &frt_elt.target_lf_ids { + canal_ids_of_targets.insert( self.manager.gen_ctx.get_lf_coloc_id(*lf_id).unwrap() ); + } + let generic_step = GenericStep{parent_id, + id_as_child:*id_as_child, + kind:AnalysisStepKind::Simulate(frt_elt,canal_ids_of_targets,hashmap!{})}; + to_enqueue.push( generic_step ); + } + } + } + + + + diff --git a/src/process/ana_proc/multitrace.rs b/src/process/ana_proc/multitrace.rs index 829d0c8..5c274b2 100644 --- a/src/process/ana_proc/multitrace.rs +++ b/src/process/ana_proc/multitrace.rs @@ -20,6 +20,7 @@ use std::collections::{HashMap, HashSet}; use crate::core::general_context::GeneralContext; use crate::core::syntax::interaction::Interaction; use crate::core::trace::TraceAction; +use crate::process::ana_proc::anakind::{SimulationActionCriterion, SimulationConfiguration, SimulationLoopCriterion}; use crate::process::ana_proc::interface::step::SimulationStepKind; @@ -47,7 +48,8 @@ impl AnalysableMultiTraceCanal { #[derive(Clone, PartialEq, Debug)] pub struct AnalysableMultiTrace { pub canals : Vec, - pub remaining_loop_instantiations_in_simulation : u32 + pub rem_loop_in_sim : u32, + pub rem_act_in_sim : u32 } pub enum WasMultiTraceConsumedWithSimulation { @@ -58,8 +60,10 @@ pub enum WasMultiTraceConsumedWithSimulation { impl AnalysableMultiTrace { - pub fn new(canals:Vec,remaining_loop_instantiations_in_simulation : u32) -> AnalysableMultiTrace { - return AnalysableMultiTrace{canals,remaining_loop_instantiations_in_simulation}; + pub fn new(canals:Vec, + rem_loop_in_sim : u32, + rem_act_in_sim : u32) -> AnalysableMultiTrace { + return AnalysableMultiTrace{canals,rem_loop_in_sim,rem_act_in_sim}; } pub fn head_actions(&self) -> HashSet<&TraceAction> { @@ -117,11 +121,11 @@ impl AnalysableMultiTrace { } pub fn update_on_execution(&self, + sim_config : &SimulationConfiguration, gen_ctx : &GeneralContext, target_lf_ids : &HashSet, affected_lfs : &HashSet, new_interaction : &Interaction) -> AnalysableMultiTrace { - let remaining_loop_instantiations_in_simulation = new_interaction.max_nested_loop_depth(); let mut new_canals : Vec = Vec::new(); // *** for coloc_id in 0..self.canals.len() { @@ -140,9 +144,14 @@ impl AnalysableMultiTrace { new_canals.push( updated_canal ); } // *** - return AnalysableMultiTrace::new(new_canals,remaining_loop_instantiations_in_simulation); + let rem_loop_in_sim= sim_config.get_reset_rem_loop(new_interaction); + let rem_act_in_sim = sim_config.get_reset_rem_act(new_interaction); + // *** + return AnalysableMultiTrace::new(new_canals,rem_loop_in_sim,rem_act_in_sim); } + + pub fn update_on_hide(&self, gen_ctx : &GeneralContext, lfs_to_hide : &HashSet) -> AnalysableMultiTrace { let mut new_canals : Vec = Vec::new(); // *** @@ -155,15 +164,18 @@ impl AnalysableMultiTrace { new_canals.push( updated_canal ); } // *** - return AnalysableMultiTrace::new(new_canals,0); + return AnalysableMultiTrace::new(new_canals,0,0); } pub fn update_on_simulation(&self, - gen_ctx : &GeneralContext, + sim_config : &SimulationConfiguration, + consu_set : &HashSet, sim_map : &HashMap, // id of canal on which simulation step is done, kind of simulation step + gen_ctx : &GeneralContext, target_lf_ids : &HashSet, affected_lfs : &HashSet, - rem_sim_depth : u32) -> AnalysableMultiTrace { + loop_depth : u32, + new_interaction : &Interaction) -> AnalysableMultiTrace { // *** let mut new_canals : Vec = Vec::new(); // *** @@ -197,7 +209,57 @@ impl AnalysableMultiTrace { new_canals.push( updated_canal ); } // *** - return AnalysableMultiTrace::new(new_canals,rem_sim_depth); + let rem_loop_in_sim : u32; + match sim_config.loop_crit { + SimulationLoopCriterion::MaxDepth => { + if consu_set.len() > 0 { + rem_loop_in_sim = new_interaction.max_nested_loop_depth(); + } else { + let on_crit = new_interaction.max_nested_loop_depth(); + let removed = self.rem_loop_in_sim - loop_depth; + rem_loop_in_sim = on_crit.min(removed); + } + }, + SimulationLoopCriterion::MaxNum => { + if consu_set.len() > 0 { + rem_loop_in_sim = new_interaction.total_loop_num(); + } else { + let on_crit = new_interaction.total_loop_num(); + let removed = self.rem_loop_in_sim - loop_depth; + rem_loop_in_sim = on_crit.min(removed); + } + }, + SimulationLoopCriterion::SpecificNum( sn ) => { + if consu_set.len() > 0 { + rem_loop_in_sim = sn; + } else { + let on_crit = sn; + let removed = self.rem_loop_in_sim - loop_depth; + rem_loop_in_sim = on_crit.min(removed); + } + }, + SimulationLoopCriterion::None => { + rem_loop_in_sim = 0; + } + } + // *** + let rem_act_in_sim : u32; + match sim_config.act_crit { + SimulationActionCriterion::SpecificNum( sn ) => { + if consu_set.len() > 0 { + rem_act_in_sim = sn; + } else { + let on_crit = sn; + let removed = self.rem_act_in_sim - 1; + rem_act_in_sim = on_crit.min(removed); + } + }, + SimulationActionCriterion::None => { + rem_act_in_sim = 0; + } + } + // *** + return AnalysableMultiTrace::new(new_canals,rem_loop_in_sim,rem_act_in_sim); } } diff --git a/src/process/ana_proc/verdicts.rs b/src/process/ana_proc/verdicts.rs index 78690f6..6f95848 100644 --- a/src/process/ana_proc/verdicts.rs +++ b/src/process/ana_proc/verdicts.rs @@ -14,6 +14,48 @@ See the License for the specific language governing permissions and limitations under the License. */ +#[derive(PartialEq, Eq, PartialOrd, Ord, Debug)] +pub enum InconcReason { + LackObs, + HideWithColocs, + FilteredNodes +} + +impl InconcReason { + + pub fn get_explanation_string(&self) -> String { + match self { + InconcReason::LackObs => { + return "due to a lack of observation in the multi-trace (events not at the end globally may be missing) -> rather use hiding or simulation".to_string(); + }, + InconcReason::HideWithColocs => { + return "due to having non-singleton co-localizations on the multi-trace while using the hiding-based algorithm. WeakPasses may be false positives because using hide may remove strict orderings between events occurring on distinct lifelines".to_string(); + }, + InconcReason::FilteredNodes => { + return "due to having set a filter which forcefully limited exploration of the graph : Fails may be false negative".to_string(); + } + } + } + +} + +impl std::string::ToString for InconcReason { + + fn to_string(&self) -> String { + match self { + InconcReason::LackObs => { + return "LackObs".to_string(); + }, + InconcReason::HideWithColocs => { + return "HideWithColocs".to_string(); + }, + InconcReason::FilteredNodes => { + return "FilteredNodes".to_string(); + } + } + } + +} pub enum CoverageVerdict{ @@ -21,11 +63,9 @@ pub enum CoverageVerdict{ TooShort, MultiPref, Slice, - Inconc, - LackObs, - Dead, - UnCov, - Out + Inconc(InconcReason), + Out(bool), // bool for if it's known via local analysis + OutSim(bool) // bool for if it's known via local analysis } impl std::string::ToString for CoverageVerdict { @@ -44,20 +84,22 @@ impl std::string::ToString for CoverageVerdict { CoverageVerdict::Slice => { return "Slice".to_string(); }, - CoverageVerdict::Inconc => { - return "Inconc".to_string(); + CoverageVerdict::Inconc(reason) => { + return format!("Inconc {:}", reason.to_string()); }, - CoverageVerdict::LackObs => { - return "LackObs".to_string(); - }, - CoverageVerdict::UnCov => { - return "UnCov".to_string(); - }, - CoverageVerdict::Dead => { - return "Dead".to_string(); + CoverageVerdict::Out(ref loc) => { + if *loc { + return "Out-l".to_string(); + } else { + return "Out".to_string(); + } }, - CoverageVerdict::Out => { - return "Out".to_string(); + CoverageVerdict::OutSim(ref loc) => { + if *loc { + return "OutSim-l".to_string(); + } else { + return "OutSim".to_string(); + } } } } @@ -67,7 +109,8 @@ impl std::string::ToString for CoverageVerdict { #[derive(PartialEq, Eq, PartialOrd, Ord, Debug)] pub enum GlobalVerdict { Fail, - Inconc, + WeakFail, + Inconc(InconcReason), WeakPass, Pass } @@ -81,8 +124,11 @@ impl std::string::ToString for GlobalVerdict { GlobalVerdict::WeakPass => { return "WeakPass".to_string(); }, - GlobalVerdict::Inconc => { - return "Inconc".to_string(); + GlobalVerdict::Inconc(reason) => { + return format!("Inconc {:}", reason.to_string()); + }, + GlobalVerdict::WeakFail => { + return "WeakFail".to_string(); }, GlobalVerdict::Fail => { return "Fail".to_string(); @@ -106,7 +152,7 @@ pub fn update_global_verdict_from_new_coverage_verdict(glo:GlobalVerdict,cov:Cov } } }, - GlobalVerdict::Inconc => { + GlobalVerdict::Inconc(glo_reason) => { match cov { CoverageVerdict::Cov => { return GlobalVerdict::Pass; @@ -122,7 +168,30 @@ pub fn update_global_verdict_from_new_coverage_verdict(glo:GlobalVerdict,cov:Cov return GlobalVerdict::WeakPass; }, _ => { - return GlobalVerdict::Inconc; + return GlobalVerdict::Inconc(glo_reason); + } + } + }, + GlobalVerdict::WeakFail => { + match cov { + CoverageVerdict::Cov => { + return GlobalVerdict::Pass; + }, + // *** + CoverageVerdict::TooShort => { + return GlobalVerdict::WeakPass; + }, + CoverageVerdict::MultiPref => { + return GlobalVerdict::WeakPass; + }, + CoverageVerdict::Slice => { + return GlobalVerdict::WeakPass; + }, + CoverageVerdict::Inconc(reason) => { + return GlobalVerdict::Inconc(reason); + }, + _ => { + return GlobalVerdict::WeakFail; } } }, @@ -142,11 +211,11 @@ pub fn update_global_verdict_from_new_coverage_verdict(glo:GlobalVerdict,cov:Cov return GlobalVerdict::WeakPass; }, // *** - CoverageVerdict::Inconc => { - return GlobalVerdict::Inconc; + CoverageVerdict::Inconc(reason) => { + return GlobalVerdict::Inconc(reason); }, - CoverageVerdict::LackObs => { - return GlobalVerdict::Inconc; + CoverageVerdict::OutSim(_) => { + return GlobalVerdict::WeakFail; }, _ => { return GlobalVerdict::Fail; diff --git a/src/process/explo_proc/interface/logger.rs b/src/process/explo_proc/interface/logger.rs index 0e9cf72..9da8c73 100644 --- a/src/process/explo_proc/interface/logger.rs +++ b/src/process/explo_proc/interface/logger.rs @@ -47,7 +47,12 @@ pub trait ExplorationLogger { elim_kind : &FilterEliminationKind); fn log_notified_lastchild_explored(&mut self, - parent_id : u32); + gen_ctx: &GeneralContext, + parent_id : u32); + + fn log_notified_terminal_node_explored(&mut self, + gen_ctx: &GeneralContext, + parent_id : u32); } diff --git a/src/process/explo_proc/interface/priorities.rs b/src/process/explo_proc/interface/priorities.rs index 8d5d85a..8b08bfd 100644 --- a/src/process/explo_proc/interface/priorities.rs +++ b/src/process/explo_proc/interface/priorities.rs @@ -18,6 +18,9 @@ limitations under the License. use crate::process::abstract_proc::generic::AbstractPriorities; + + + pub struct ExplorationPriorities { pub emission : i32, pub reception : i32, @@ -25,6 +28,9 @@ pub struct ExplorationPriorities { pub in_loop : i32 } + + + impl ExplorationPriorities { pub fn new(emission : i32, diff --git a/src/process/explo_proc/manager.rs b/src/process/explo_proc/manager.rs index 2a08c6f..a55bb6b 100644 --- a/src/process/explo_proc/manager.rs +++ b/src/process/explo_proc/manager.rs @@ -24,20 +24,41 @@ use crate::core::semantics::frontier::global_frontier; use crate::core::syntax::interaction::Interaction; use crate::core::syntax::position::Position; use crate::core::trace::TraceAction; -use crate::process::abstract_proc::common::FilterEliminationKind; -use crate::process::abstract_proc::generic::{GenericNode, GenericProcessManager, GenericStep}; +use crate::process::abstract_proc::common::{FilterEliminationKind, HibouSearchStrategy}; +use crate::process::abstract_proc::generic::*; +use crate::process::abstract_proc::manager::*; use crate::process::explo_proc::interface::conf::ExplorationConfig; -use crate::process::explo_proc::interface::filter::ExplorationFilterCriterion; +use crate::process::explo_proc::interface::filter::{ExplorationFilter, ExplorationFilterCriterion}; +use crate::process::explo_proc::interface::logger::ExplorationLogger; use crate::process::explo_proc::interface::node::ExplorationNodeKind; use crate::process::explo_proc::interface::step::ExplorationStepKind; -pub type ExplorationProcessManager = GenericProcessManager; +pub struct ExplorationProcessManager { + pub(crate) manager: GenericProcessManager, + pub(crate) node_has_child_interaction : HashSet +} impl ExplorationProcessManager { - pub fn explore(&mut self,interaction : Interaction) -> u32 { + pub fn new(gen_ctx : GeneralContext, + strategy : HibouSearchStrategy, + filters : Vec, + priorities : GenericProcessPriorities, + loggers : Vec>) -> ExplorationProcessManager { + let manager = GenericProcessManager::new( + gen_ctx, + strategy, + filters, + priorities, + loggers + ); + return ExplorationProcessManager{manager,node_has_child_interaction:HashSet::new()}; + } + + pub fn explore(&mut self, + interaction : Interaction) -> u32 { self.init_loggers(&interaction); // *** let mut next_state_id : u32 = 1; @@ -47,11 +68,11 @@ impl ExplorationProcessManager { node_counter = node_counter +1; // *** // *** - while let Some(next_to_process) = self.extract_from_queue() { + while let Some(next_to_process) = self.manager.extract_from_queue() { let new_state_id = next_state_id; next_state_id = next_state_id + 1; // *** - let mut parent_state = self.pick_memorized_state(next_to_process.parent_id); + let mut parent_state = self.manager.pick_memorized_state(next_to_process.parent_id); // *** match self.process_step(&parent_state, &next_to_process, @@ -59,6 +80,7 @@ impl ExplorationProcessManager { node_counter) { None => {}, Some( (new_interaction,new_depth,new_loop_depth) ) => { + self.node_has_child_interaction.insert(next_to_process.parent_id); node_counter = node_counter + 1; self.enqueue_next_node_in_exploration(new_state_id, new_interaction, @@ -69,8 +91,12 @@ impl ExplorationProcessManager { // *** parent_state.remaining_ids_to_process.remove(&next_to_process.id_as_child); if parent_state.remaining_ids_to_process.len() > 0 { - self.remember_state(next_to_process.parent_id,parent_state); + self.manager.remember_state(next_to_process.parent_id,parent_state); } else { + let parent_has_child_interaction = self.node_has_child_interaction.remove(&next_to_process.parent_id); + if !parent_has_child_interaction { + self.notify_terminal_node_explored(next_to_process.parent_id); + } self.notify_lastchild_explored_loggers(next_to_process.parent_id); } // *** @@ -87,20 +113,26 @@ impl ExplorationProcessManager { depth : u32, loop_depth : u32) { // *** + let mut glob_front = global_frontier(&interaction,&None); + // reverse so that when one pops from right to left the actions appear from the top to the bottom + glob_front.reverse(); + // *** let mut id_as_child : u32 = 0; // *** let mut to_enqueue : Vec> = Vec::new(); - for front_pos in global_frontier(&interaction,&None) { + for front_pos in glob_front { + id_as_child = id_as_child + 1; let generic_step = GenericStep{parent_id,id_as_child,kind:ExplorationStepKind::Execute(front_pos)}; - id_as_child = id_as_child +1; to_enqueue.push( generic_step ); } // *** if id_as_child > 0 { let remaining_ids_to_process : HashSet = HashSet::from_iter((1..(id_as_child+1)).collect::>().iter().cloned() ); let generic_node = GenericNode{kind:ExplorationNodeKind{interaction,loop_depth},remaining_ids_to_process,depth}; - self.remember_state( parent_id, generic_node ); - self.enqueue_new_steps( parent_id, to_enqueue, depth ); + self.manager.remember_state( parent_id, generic_node ); + self.manager.enqueue_new_steps( parent_id, to_enqueue, depth ); + } else { + self.notify_terminal_node_explored(parent_id); } } @@ -114,7 +146,7 @@ impl ExplorationProcessManager { let new_depth = parent_state.depth + 1; let new_loop_depth = parent_state.kind.loop_depth + (parent_state.kind.interaction).get_loop_depth_at_pos(&frt_elt.position); // *** - match self.apply_filters(new_depth,node_counter,&ExplorationFilterCriterion{loop_depth:new_loop_depth}) { + match self.manager.apply_filters(new_depth,node_counter,&ExplorationFilterCriterion{loop_depth:new_loop_depth}) { None => { // *** let exe_result = execute_interaction(&parent_state.kind.interaction, @@ -142,22 +174,31 @@ impl ExplorationProcessManager { } fn init_loggers(&mut self, interaction : &Interaction) { - for logger in self.loggers.iter_mut() { - (*logger).log_init(interaction, &self.gen_ctx); + for logger in self.manager.loggers.iter_mut() { + (*logger).log_init(interaction, &self.manager.gen_ctx); } } fn term_loggers(&mut self) { - let mut options_as_strs = (&self).get_basic_options_as_strings(); + let mut options_as_strs = (&self).manager.get_basic_options_as_strings(); options_as_strs.insert(0, "process=exploration".to_string()); - for logger in self.loggers.iter_mut() { + for logger in self.manager.loggers.iter_mut() { (*logger).log_term(&options_as_strs); } } fn notify_lastchild_explored_loggers(&mut self, parent_id : u32) { - for logger in self.loggers.iter_mut() { - (*logger).log_notified_lastchild_explored(parent_id); + for logger in self.manager.loggers.iter_mut() { + (*logger).log_notified_lastchild_explored(&self.manager.gen_ctx,parent_id); + } + } + + fn notify_terminal_node_explored(&mut self, parent_id : u32) { + // for the HCS queue to know the node id'ed by parent_id is terminal + self.manager.queue_set_last_reached_has_no_child(); + // *** + for logger in self.manager.loggers.iter_mut() { + (*logger).log_notified_terminal_node_explored(&self.manager.gen_ctx,parent_id); } } @@ -165,7 +206,7 @@ impl ExplorationProcessManager { parent_state_id : u32, new_state_id : u32, elim_kind : &FilterEliminationKind) { - for logger in self.loggers.iter_mut() { + for logger in self.manager.loggers.iter_mut() { logger.log_filtered(parent_state_id, new_state_id, elim_kind); @@ -178,8 +219,8 @@ impl ExplorationProcessManager { new_interaction : &Interaction, parent_state_id : u32, new_state_id :u32) { - for logger in self.loggers.iter_mut() { - logger.log_explore(&self.gen_ctx, + for logger in self.manager.loggers.iter_mut() { + logger.log_explore(&self.manager.gen_ctx, parent_state_id, new_state_id, action_position, diff --git a/src/rendering/custom_draw/seqdiag/ext_multi_trace.rs b/src/rendering/custom_draw/seqdiag/ext_multi_trace.rs index f9b2a51..171a286 100644 --- a/src/rendering/custom_draw/seqdiag/ext_multi_trace.rs +++ b/src/rendering/custom_draw/seqdiag/ext_multi_trace.rs @@ -93,7 +93,9 @@ fn extract_texts_on_canal_visible(gen_ctx : &GeneralContext, pub fn extract_texts_on_multi_trace(gen_ctx : &GeneralContext, multi_trace : &AnalysableMultiTrace, - is_simulation : bool) -> Vec> { + is_simulation : bool, + sim_crit_loop : bool, + sim_crit_act : bool) -> Vec> { let mut all_texts : Vec> = Vec::new(); for i in 0..gen_ctx.co_localizations.len() { let lifelines = gen_ctx.co_localizations.get(i).unwrap(); @@ -106,8 +108,23 @@ pub fn extract_texts_on_multi_trace(gen_ctx : &GeneralContext, } } if is_simulation { - all_texts.push( vec![ TextToPrint{text:" ".to_string(), color:Rgb(HCP_Black)} ] ); - all_texts.push( vec![ TextToPrint{text:format!("⌕{:}", multi_trace.remaining_loop_instantiations_in_simulation), color:Rgb(HC_Grammar_Symbol)} ] ); + let mut simu_vec: Vec = vec![]; + // *** + simu_vec.push( TextToPrint{text:" ⌕ ".to_string(), color:Rgb(HC_Grammar_Symbol)} ); + if (!sim_crit_loop) && (!sim_crit_act) { + simu_vec.push( TextToPrint{text:"*".to_string(), color:Rgb(HC_Grammar_Symbol)} ); + } else { + if sim_crit_loop { + simu_vec.push( TextToPrint{text:format!("L{:} ",multi_trace.rem_loop_in_sim), + color:Rgb(HC_Grammar_Symbol)} ); + } + if sim_crit_act { + simu_vec.push( TextToPrint{text:format!("A{:}",multi_trace.rem_act_in_sim), + color:Rgb(HC_Grammar_Symbol)} ); + } + } + // *** + all_texts.push(simu_vec); } // return all_texts; diff --git a/src/rendering/custom_draw/seqdiag/interaction.rs b/src/rendering/custom_draw/seqdiag/interaction.rs index 243765e..7b43747 100644 --- a/src/rendering/custom_draw/seqdiag/interaction.rs +++ b/src/rendering/custom_draw/seqdiag/interaction.rs @@ -46,7 +46,9 @@ pub fn draw_interaction(path_str : &String, interaction : &Interaction, gen_ctx : &GeneralContext, remaining_multi_trace : &Option<&AnalysableMultiTrace>, - is_simulation : bool) { + is_simulation : bool, + sim_crit_loop : bool, + sim_crit_act : bool) { let path = Path::new( path_str ); // *** let mut lf_x_widths : HashMap = HashMap::new(); @@ -77,7 +79,7 @@ pub fn draw_interaction(path_str : &String, multi_trace_txttoprint = None; } Some( multi_trace ) => { - let mt_ttp = extract_texts_on_multi_trace( gen_ctx, multi_trace, is_simulation); + let mt_ttp = extract_texts_on_multi_trace( gen_ctx, multi_trace, is_simulation, sim_crit_loop, sim_crit_act); let mut max_char_count = 0; for ttp in &mt_ttp { max_char_count = max_char_count.max(TextToPrint::char_count(ttp) ); diff --git a/src/sd_syntax.pest b/src/sd_syntax.pest index f77d2f8..75063f4 100644 --- a/src/sd_syntax.pest +++ b/src/sd_syntax.pest @@ -80,13 +80,14 @@ GRAPHIC_LOGGER_opt = _{ GRAPHIC_LOGGER_png | GRAPHIC_LOGGER_svg | GRAPHIC_LOGGER GRAPHIC_LOGGER_opts = { "[" ~ GRAPHIC_LOGGER_opt ~ ("," ~ GRAPHIC_LOGGER_opt)* ~ "]" } OPTION_GRAPHIC_LOGGER = { "graphic" ~ GRAPHIC_LOGGER_opts? } // *** +TRACEGEN_LOGGER_terminal = { "terminal" } TRACEGEN_LOGGER_exact = { "exact" } TRACEGEN_LOGGER_prefix = { "prefix" } TRACEGEN_LOGGER_partition_discrete = { "discrete" } TRACEGEN_LOGGER_partition_trivial = { "trivial" } TRACEGEN_LOGGER_partition_specific = { "{" ~ HIBOU_LABEL_LIST ~ ("," ~ HIBOU_LABEL_LIST)* ~ "}" } TRACEGEN_LOGGER_partition = _{ "partition" ~ "=" ~ (TRACEGEN_LOGGER_partition_discrete | TRACEGEN_LOGGER_partition_trivial | TRACEGEN_LOGGER_partition_specific) } -TRACEGEN_LOGGER_opt = _{ TRACEGEN_LOGGER_exact | TRACEGEN_LOGGER_prefix | TRACEGEN_LOGGER_partition } +TRACEGEN_LOGGER_opt = _{ TRACEGEN_LOGGER_exact | TRACEGEN_LOGGER_prefix | TRACEGEN_LOGGER_terminal | TRACEGEN_LOGGER_partition } TRACEGEN_LOGGER_opts = { "[" ~ TRACEGEN_LOGGER_opt ~ ("," ~ TRACEGEN_LOGGER_opt)* ~ "]" } OPTION_TRACEGEN_LOGGER = { "tracegen" ~ TRACEGEN_LOGGER_opts? } // *** @@ -110,11 +111,15 @@ OPTION_PRIORITY_KIND = _{ OPTION_PRIORITY_emission | OPTION_PRIORITY_hide | OPTION_PRIORITY_simu } OPTION_PRIORITY_LEVEL = { ARITH_INTEGER | ("-" ~ ARITH_INTEGER ) } -OPTION_PRIORITY = { OPTION_PRIORITY_KIND ~ "=" ~ OPTION_PRIORITY_LEVEL } -// *********************************************** -OPTION_STRATEGY_BFS = { "BreadthFS" } -OPTION_STRATEGY_DFS = { "DepthFS" } -OPTION_STRATEGY_KIND = _{ OPTION_STRATEGY_BFS | OPTION_STRATEGY_DFS } +OPTION_PRIORITY_SPECIFIC_elt = { OPTION_PRIORITY_KIND ~ "=" ~ OPTION_PRIORITY_LEVEL } +OPTION_PRIORITY_SPECIFIC = { "[" ~ OPTION_PRIORITY_SPECIFIC_elt ~ ("," ~ OPTION_PRIORITY_SPECIFIC_elt)* ~ "]" } +OPTION_PRIORITY_RANDOM = { "random" | "rand" } +OPTION_PRIORITY = _{ OPTION_PRIORITY_SPECIFIC | OPTION_PRIORITY_RANDOM } +// *********************************************** +OPTION_STRATEGY_BFS = { "BreadthFS" | "Breadth First Search" | "BFS" } +OPTION_STRATEGY_DFS = { "DepthFS" | "Depth First Search" | "DFS" } +OPTION_STRATEGY_HCS = { "HighCoverageS" | "High Coverage Search" | "HCS" } +OPTION_STRATEGY_KIND = _{ OPTION_STRATEGY_BFS | OPTION_STRATEGY_DFS | OPTION_STRATEGY_HCS } OPTION_STRATEGY_DECL = { "strategy" ~ "=" ~ OPTION_STRATEGY_KIND } // *********************************************** OPTION_FILTER_MAX_DEPTH = { "max_depth" ~ "=" ~ ARITH_INTEGER } @@ -123,12 +128,12 @@ OPTION_FILTER_MAX_NODE_NUMBER = { "max_node_number" ~ "=" ~ ARITH_INTEGER } OPTION_FILTER = _{ OPTION_FILTER_MAX_DEPTH | OPTION_FILTER_MAX_LOOP_DEPTH | OPTION_FILTER_MAX_NODE_NUMBER } OPTION_FILTERS_DECL = { "filters" ~ "=" ~ "[" ~ OPTION_FILTER ~ ("," ~ OPTION_FILTER)* ~ "]" } // *********************************************** -OPTION_FRONTIER_PRIORITIES_DECL = { "priorities" ~ "=" ~ "[" ~ OPTION_PRIORITY ~ ("," ~ OPTION_PRIORITY)* ~ "]" } +OPTION_PRIORITIES_DECL = { "priorities" ~ "=" ~ OPTION_PRIORITY } // *********************************************** GENERAL_OPTION_DECL = _{ OPTION_LOGGER_DECL | OPTION_STRATEGY_DECL | OPTION_FILTERS_DECL - | OPTION_FRONTIER_PRIORITIES_DECL } + | OPTION_PRIORITIES_DECL } // *********************************************** EXPLORE_OPTION_DECL = _{ GENERAL_OPTION_DECL } EXPLORE_OPTION_SECTION = { "@explore_option" ~ "{" ~ @@ -138,13 +143,31 @@ EXPLORE_OPTION_SECTION = { "@explore_option" ~ "{" ~ OPTION_ANA_KIND_accept = { "accept" } OPTION_ANA_KIND_prefix = { "prefix" } OPTION_ANA_KIND_hide = { "hide" } -OPTION_ANA_KIND_simulate_prefix = { "simulate" ~ "[" ~ "multi-prefix" ~ "]" } -OPTION_ANA_KIND_simulate_slice = { "simulate" ~ "[" ~ "multi-slice" ~ "]" } +// *** +OPTION_ANA_SIMULATE_CONFIG_crit_num = { "num" ~ "=" ~ ARITH_INTEGER } +OPTION_ANA_SIMULATE_CONFIG_crit_maxnum = { "maxnum" | "max"~"num" } +OPTION_ANA_SIMULATE_CONFIG_crit_maxdepth = { "maxdepth" | "max"~"depth" } +OPTION_ANA_SIMULATE_CONFIG_crit_none = { "none" | "None" | "NONE" } +// *** +OPTION_ANA_SIMULATE_CONFIG_loop = { "loop" ~ ( OPTION_ANA_SIMULATE_CONFIG_crit_num + | OPTION_ANA_SIMULATE_CONFIG_crit_maxnum + | OPTION_ANA_SIMULATE_CONFIG_crit_maxdepth + | OPTION_ANA_SIMULATE_CONFIG_crit_none ) } +OPTION_ANA_SIMULATE_CONFIG_act = { "act" ~ ( OPTION_ANA_SIMULATE_CONFIG_crit_num + | OPTION_ANA_SIMULATE_CONFIG_crit_none) } +// *** +OPTION_ANA_SIMULATE_CONFIG_simbefore = { "slice" | "before" | "preamble" } +OPTION_ANA_SIMULATE_CONFIG_opt = _{ OPTION_ANA_SIMULATE_CONFIG_simbefore + | OPTION_ANA_SIMULATE_CONFIG_act + | OPTION_ANA_SIMULATE_CONFIG_loop } +// *** +OPTION_ANA_SIMULATE_CONFIG_decl = { "[" ~ OPTION_ANA_SIMULATE_CONFIG_opt ~ ("," ~ OPTION_ANA_SIMULATE_CONFIG_opt)* ~ "]" } +// *** +OPTION_ANA_KIND_simulate = { "simulate" ~ OPTION_ANA_SIMULATE_CONFIG_decl? } OPTION_ANALYSIS_KIND = _{ OPTION_ANA_KIND_accept | OPTION_ANA_KIND_prefix | OPTION_ANA_KIND_hide - | OPTION_ANA_KIND_simulate_prefix - | OPTION_ANA_KIND_simulate_slice } + | OPTION_ANA_KIND_simulate } OPTION_ANALYSIS_KIND_DECL = { "analysis_kind" ~ "=" ~ OPTION_ANALYSIS_KIND } // *********************************************** OPTION_GOAL_pass = { "Pass" } @@ -154,6 +177,7 @@ OPTION_GOAL_KIND = _{ OPTION_GOAL_pass | OPTION_GOAL_weakpass | OPTION_GOAL_none OPTION_GOAL_DECL = { "goal" ~ "=" ~ OPTION_GOAL_KIND } // *********************************************** OPTION_LOCANA_yes = { "local_analysis" ~ "=" ~ "true" } +OPTION_LOCANA_onlyfront = { "local_analysis" ~ "=" ~ ("front" | "onlyfront" | "only" ~"front") } OPTION_LOCANA_no = { "local_analysis" ~ "=" ~ "false" } OPTION_LOCANA = _{ OPTION_LOCANA_yes | OPTION_LOCANA_no } // *********************************************** diff --git a/src/slice/exhaustive.rs b/src/slice/exhaustive.rs new file mode 100644 index 0000000..53b40f8 --- /dev/null +++ b/src/slice/exhaustive.rs @@ -0,0 +1,48 @@ +/* +Copyright 2020 Erwan Mahe (github.com/erwanM974) + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +*/ + +use std::collections::HashSet; +use std::fs; +use crate::core::general_context::GeneralContext; +use crate::core::trace::TraceAction; +use crate::process::ana_proc::multitrace::{AnalysableMultiTrace, AnalysableMultiTraceCanal}; +use crate::to_hfiles::multitrace_to_htf::write_multi_trace_into_file; +use crate::util::slicer::Slicer; + + + +pub fn get_all_slices_rec<'a>(gen_ctx : &GeneralContext, + dir_name : &str, + id : &mut u32, + ok_canals : &Vec< Vec> >, + rem_canals : &mut (impl Iterator + Clone)) { + match rem_canals.next() { + None => { + let file_path = format!("{:}/s{:}", dir_name, id); + *id = *id + 1; + write_multi_trace_into_file(&file_path, gen_ctx, Some(&gen_ctx.co_localizations),ok_canals); + }, + Some( rem_canal ) => { + let mut slicer = Slicer::new(&rem_canal.trace); + while let Some(got_slice) = slicer.next() { + let mut new_trace = got_slice.iter().cloned().collect::>>(); + let mut new_ok_canals = ok_canals.clone(); + new_ok_canals.push(new_trace); + get_all_slices_rec(gen_ctx,dir_name,id,&new_ok_canals,&mut rem_canals.clone()); + } + } + } +} \ No newline at end of file diff --git a/src/slice/generate.rs b/src/slice/generate.rs new file mode 100644 index 0000000..2771315 --- /dev/null +++ b/src/slice/generate.rs @@ -0,0 +1,80 @@ +/* +Copyright 2020 Erwan Mahe (github.com/erwanM974) + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +*/ + +use std::fs; +use crate::core::general_context::GeneralContext; +use crate::process::ana_proc::multitrace::{AnalysableMultiTrace, AnalysableMultiTraceCanal}; +use crate::slice::exhaustive::get_all_slices_rec; +use crate::slice::random::get_random_slices; + + +pub enum SliceGenerationConfiguration { + Exhaustive, // all the slices + Random(u32) // a number 'x' of random slices +} + + +pub fn generate_slices(gen_ctx : &GeneralContext, + mu_name : &str, + multi_trace : &AnalysableMultiTrace, + parent_folder : Option<&str>, + conf : SliceGenerationConfiguration) { + let dir_name : String; + match parent_folder { + None => { + dir_name = format!("./{:}_slices", mu_name); + }, + Some( parent ) => { + dir_name = format!("{:}/{:}_slices", parent, mu_name); + } + } + // empties directory if exists + match fs::remove_dir_all(&dir_name) { + Ok(_) => { + // do nothing + }, + Err(e) => { + // do nothing + } + } + // creates directory + fs::create_dir_all(&dir_name).unwrap(); + // *** + match conf { + SliceGenerationConfiguration::Exhaustive => { + get_all_slices_rec(gen_ctx,&dir_name, &mut 1, &vec![], &mut multi_trace.canals.iter()); + }, + SliceGenerationConfiguration::Random( mut num_slices ) => { + if num_slices >= get_total_num_slices(&multi_trace) { + get_all_slices_rec(gen_ctx,&dir_name, &mut 1, &vec![], &mut multi_trace.canals.iter()); + } else { + get_random_slices(gen_ctx,&dir_name,&mut num_slices,&multi_trace); + } + } + } +} + +fn get_total_num_slices(multi_trace : &AnalysableMultiTrace) -> u32 { + let mut prod : u32 = 1; + for canal in &multi_trace.canals { + let canal_len = canal.trace.len(); + if canal_len > 0 { + let num_slices_of_canal : u32 = (1..canal_len as u32).sum(); + prod = prod * num_slices_of_canal; + } + } + return prod; +} diff --git a/src/slice/mod.rs b/src/slice/mod.rs index c8e876f..4c2319f 100644 --- a/src/slice/mod.rs +++ b/src/slice/mod.rs @@ -15,61 +15,7 @@ limitations under the License. */ -use std::collections::HashSet; -use std::fs; -use crate::core::general_context::GeneralContext; -use crate::core::trace::TraceAction; -use crate::process::ana_proc::multitrace::{AnalysableMultiTrace, AnalysableMultiTraceCanal}; -use crate::to_hfiles::multitrace_to_htf::write_multi_trace_into_file; -use crate::util::slicer::Slicer; +mod exhaustive; +mod random; +pub mod generate; -pub fn generate_slices(gen_ctx : &GeneralContext, - mu_name : &str, - multi_trace : &AnalysableMultiTrace, - parent_folder : Option<&str>) { - let dir_name : String; - match parent_folder { - None => { - dir_name = format!("./{:}_slices", mu_name); - }, - Some( parent ) => { - dir_name = format!("{:}/{:}_slices", parent, mu_name); - } - } - // empties directory if exists - match fs::remove_dir_all(&dir_name) { - Ok(_) => { - // do nothing - }, - Err(e) => { - // do nothing - } - } - // creates directory - fs::create_dir_all(&dir_name).unwrap(); - // *** - get_slices_rec(gen_ctx,&dir_name, &mut 1, &vec![], &mut multi_trace.canals.iter()); -} - -fn get_slices_rec<'a>(gen_ctx : &GeneralContext, - dir_name : &str, - id : &mut u32, - ok_canals : &Vec< Vec> >, - rem_canals : &mut (impl Iterator + Clone)) { - match rem_canals.next() { - None => { - let file_path = format!("{:}/s{:}", dir_name, id); - *id = *id + 1; - write_multi_trace_into_file(&file_path, gen_ctx, Some(&gen_ctx.co_localizations),ok_canals); - }, - Some( rem_canal ) => { - let mut slicer = Slicer::new(&rem_canal.trace); - while let Some(got_slice) = slicer.next() { - let mut new_trace = got_slice.iter().cloned().collect::>>(); - let mut new_ok_canals = ok_canals.clone(); - new_ok_canals.push(new_trace); - get_slices_rec(gen_ctx,dir_name,id,&new_ok_canals,&mut rem_canals.clone()); - } - } - } -} \ No newline at end of file diff --git a/src/slice/random.rs b/src/slice/random.rs new file mode 100644 index 0000000..b73b4f6 --- /dev/null +++ b/src/slice/random.rs @@ -0,0 +1,66 @@ +/* +Copyright 2020 Erwan Mahe (github.com/erwanM974) + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +*/ + + + +use std::cmp::{min,max}; +use rand::Rng; +use rand::distributions::{Distribution, Uniform}; + +use std::collections::HashSet; +use std::fs; +use crate::core::general_context::GeneralContext; +use crate::core::trace::TraceAction; +use crate::process::ana_proc::multitrace::{AnalysableMultiTrace, AnalysableMultiTraceCanal}; +use crate::to_hfiles::multitrace_to_htf::write_multi_trace_into_file; +use crate::util::slicer::Slicer; + + + + +pub fn get_random_slices(gen_ctx : &GeneralContext, + dir_name : &str, + num_slices : &mut u32, + multi_trace : &AnalysableMultiTrace) { + let mut slices : HashSet< Vec<(usize,usize)> > = hashset!{}; + let mut rng = rand::thread_rng(); + while *num_slices > 0 { + let mut new_canals_ids : Vec<(usize,usize)> = vec![]; + let mut new_canals : Vec>> = vec![]; + // *** + for canal in &multi_trace.canals { + let rng_indices = Uniform::from(0..canal.trace.len()); + let id1 = rng_indices.sample(&mut rng); + let id2 = rng_indices.sample(&mut rng); + let min_id = min(id1,id2); + let max_id = max(id1,id2); + let new_trace : Vec> = canal.trace[min_id..max_id].iter().cloned().collect(); + new_canals.push(new_trace); + new_canals_ids.push( (min_id,max_id) ); + } + // *** + let file_path = format!("{:}/s{:}", dir_name, num_slices); + *num_slices = *num_slices - 1; + // *** + if !slices.contains( &new_canals_ids ) { + write_multi_trace_into_file(&file_path, + gen_ctx, + Some(&gen_ctx.co_localizations), + &new_canals); + slices.insert(new_canals_ids); + } + } +} \ No newline at end of file diff --git a/src/ui/hibou_cli.rs b/src/ui/hibou_cli.rs index 4c5d488..6efa814 100644 --- a/src/ui/hibou_cli.rs +++ b/src/ui/hibou_cli.rs @@ -42,7 +42,7 @@ use crate::from_hfiles::traces::htf_file::parse_htf_file; use crate::plantuml::sequence::to_plant_uml_sd; use crate::plantuml::automata_product::to_plant_uml_ap; use crate::rendering::custom_draw::term::term_repr_out::to_term_repr; -use crate::slice::generate_slices; +use crate::slice::generate::*; //use crate::canonize::process::canon_process_interaction_term; //use crate::merge_gates::process::merge_process_interaction_term; @@ -60,7 +60,7 @@ fn get_ascii_left() -> Vec<&'static str> { my_vec.push(r#"-"-"- Oracle "#); my_vec.push(r#" \_/ Utility "#); my_vec.push(r#" "#); - my_vec.push(r#" V-label-0.7.7 "#); + my_vec.push(r#" V-label-0.7.8 "#); return my_vec; } @@ -117,7 +117,7 @@ pub fn hibou_cli() -> i32 { ret_print.push( format!("from file '{}'",hsf_file_path) ); ret_print.push( format!("on file : {}",spec_output_file) ); ret_print.push( "".to_string()); - draw_interaction(&spec_output_file, &my_int,&gen_ctx,&None, false); + draw_interaction(&spec_output_file, &my_int,&gen_ctx,&None, false,false,false); } } } else if let Some(matches) = matches.subcommand_matches("puml_sd") { @@ -288,6 +288,14 @@ pub fn hibou_cli() -> i32 { return -1; }, Ok( (mut gen_ctx,my_int,hoptions) ) => { + let int_characs = my_int.get_characteristics(); + // *** + if int_characs.has_ands { + ret_print.push( "Interaction term has 'And's -> Analysis Not Implemented".to_string() ); + print_retval(ret_print); + return -1; + } + // *** let htf_file_path = matches.value_of("htf").unwrap(); match parse_htf_file(htf_file_path,&mut gen_ctx,false) { Err(e) => { @@ -312,7 +320,7 @@ pub fn hibou_cli() -> i32 { hoptions.analyze_options.local_analysis, hoptions.analyze_options.goal); let now = Instant::now(); - let (verdict,node_count) = manager.analyze(my_int,multi_trace); + let (verdict,node_count) = manager.analyze(my_int,int_characs,multi_trace); let elapsed_time = now.elapsed(); ret_print.push( format!("verdict : '{}'", verdict.to_string() ) ); ret_print.push( format!("node count : {:?}", node_count ) ); @@ -347,7 +355,15 @@ pub fn hibou_cli() -> i32 { } } // *** - generate_slices(&gen_ctx,mu_name,&multi_trace,parent_folder); + if matches.is_present("random") { + let extracted = matches.value_of("random").unwrap(); + let content_str : String = extracted.chars().filter(|c| !c.is_whitespace()).collect(); + let my_val : u32 = content_str.parse::().unwrap(); + generate_slices(&gen_ctx,mu_name,&multi_trace,parent_folder,SliceGenerationConfiguration::Random(my_val)); + } else { + generate_slices(&gen_ctx,mu_name,&multi_trace,parent_folder,SliceGenerationConfiguration::Exhaustive); + } + } } } else { diff --git a/src/ui/hibou_cli.yml b/src/ui/hibou_cli.yml index 462b7f4..5e19f07 100644 --- a/src/ui/hibou_cli.yml +++ b/src/ui/hibou_cli.yml @@ -16,13 +16,13 @@ name: hibou_label -version: "0.7.7" +version: "0.7.8" author: Erwan Mahe about: Holistic Interaction Behavioral Oracle Utility - hibou provides utilities for manipulating interaction models (sequence diagrams/sequence charts) subcommands: - draw: about: utility to draw as a sequence diagram an interaction encoded in a hibou specification file (.hsf) - version: "0.7.7" + version: "0.7.8" author: Erwan Mahe args: - hsf: @@ -36,7 +36,7 @@ subcommands: help: target file for drawing (default is 'the name of the hsf'.png) - explore: about: utility to explore the semantics of an interaction encoded in a hibou specification file (.hsf) - version: "0.7.7" + version: "0.7.8" author: Erwan Mahe args: - hsf: @@ -45,7 +45,7 @@ subcommands: help: input hibou specification file - analyze: about: utility to analyze an input (multi-)trace encoded in a hibou trace file (.htf) w.r.t. an interaction encoded in a hibou specification file (.hsf) - version: "0.7.7" + version: "0.7.8" author: Erwan Mahe args: - hsf: @@ -58,7 +58,7 @@ subcommands: help: input hibou trace file - slice: about: utility to generate slices of a (multi-)trace encoded in a hibou trace file (.htf) - version: "0.7.7" + version: "0.7.8" author: Erwan Mahe args: - htf: @@ -70,9 +70,14 @@ subcommands: short: p takes_value: true help: parent file in which to generate slices + - random: + required: false + short: r + takes_value: true + help: random selection of a number of slices instead of exhaustive generation - puml_sd: about: utility to translate an interaction encoded in a hibou specification file (.hsf) into a .puml informal sequence diagram spec (.puml) - version: "0.7.7" + version: "0.7.8" author: Erwan Mahe args: - hsf: @@ -81,7 +86,7 @@ subcommands: help: input hibou specification file - puml_ap: about: utility to translate an interaction encoded in a hibou specification file (.hsf) into a .puml informal automata product spec (.puml) - version: "0.7.7" + version: "0.7.8" author: Erwan Mahe args: - hsf: @@ -90,7 +95,7 @@ subcommands: help: input hibou specification file - term_repr: about: utility to translate an interaction encoded in a hibou specification file (.hsf) into a .puml informal automata product spec (.puml) - version: "0.7.7" + version: "0.7.8" author: Erwan Mahe args: - hsf: @@ -99,7 +104,7 @@ subcommands: help: input hibou specification file - canonize: about: utility to compute the normal form of an interaction encoded in a hibou specification file (.hsf) and to draw possible sequences of transformations leading to that normal form - version: "0.7.7" + version: "0.7.8" author: Erwan Mahe args: - hsf: @@ -113,7 +118,7 @@ subcommands: help: computes all possible sequences of transformations (by default only one is) - merge: about: utility to merge interaction with gates - version: "0.7.7" + version: "0.7.8" author: Erwan Mahe args: - hsf: