Skip to content

Commit

Permalink
- local analysis for slices (simulation before the local component) -…
Browse files Browse the repository at this point in the history
… 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
  • Loading branch information
erwanM974 committed Sep 28, 2022
1 parent 281abe7 commit 230b285
Show file tree
Hide file tree
Showing 43 changed files with 1,950 additions and 970 deletions.
88 changes: 71 additions & 17 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

5 changes: 3 additions & 2 deletions Cargo.toml
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
[package]
name = "hibou_label"
version = "0.7.7"
version = "0.7.8"
authors = ["Erwan Mahe"]
edition = "2018"

Expand All @@ -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
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
1 change: 1 addition & 0 deletions src/core/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -21,4 +21,5 @@ pub mod semantics;
pub mod error;

pub mod trace;
//pub mod multitrace;

29 changes: 29 additions & 0 deletions src/core/multitrace.rs
Original file line number Diff line number Diff line change
@@ -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<usize>,
pub trace : Vec<HashSet<TraceAction>>
}

pub type MultiTrace = Vec<MultiTraceCanal>;
58 changes: 23 additions & 35 deletions src/core/semantics/frontier.rs
Original file line number Diff line number Diff line change
Expand Up @@ -128,26 +128,26 @@ fn global_frontier_rec(interaction : &Interaction, loop_depth : u32) -> Vec<Fron
return frontier_on_reception(rc_act, loop_depth);
},
Interaction::Strict(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) );
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);
}
}
return front;
},
Interaction::CoReg(ref cr, 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)) {
let mut reqs_lf_ids = frt_elt2.target_lf_ids.clone();
for cr_lf_id in cr {
reqs_lf_ids.remove(cr_lf_id);
Expand All @@ -159,17 +159,17 @@ fn global_frontier_rec(interaction : &Interaction, loop_depth : u32) -> Vec<Fron
return front;
},
Interaction::Alt(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::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");
Expand All @@ -179,30 +179,18 @@ fn global_frontier_rec(interaction : &Interaction, loop_depth : u32) -> Vec<Fron



fn push_frontier_left(frontier : Vec<FrontierElement>) -> Vec<FrontierElement> {
let mut new_frontier : Vec<FrontierElement> = 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<FrontierElement>) -> Vec<FrontierElement> {
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<FrontierElement>) -> Vec<FrontierElement> {
let mut new_frontier : Vec<FrontierElement> = 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<FrontierElement>) -> Vec<FrontierElement> {
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();
}
Loading

0 comments on commit 230b285

Please sign in to comment.