From 8ff768b14fbca5535ae213f745de87543b08d5f4 Mon Sep 17 00:00:00 2001 From: Thomas Lohse <49527735+t-lohse@users.noreply.github.com> Date: Wed, 30 Nov 2022 12:46:12 +0100 Subject: [PATCH] Advanced clock reduction (#147) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * started advanced cases * start_find_redundant_clocks * test setup, needs test examples * test setup, needs test examples * added test component * added get_transition * added test component for composition * added test component, and refactored file system for test components * Added find transition * Refactor * Name refactor * Where implementations * Some impl * Fixed compile error * Changed reduce_clocks prototype * Miss merge * added get_children_mut * Hardcoded clock reduction of clock y * Hardcoded clock reduction of clock y * merge * heights * compile * Test refactor * Warnings * working on clock reduction analyzer * Some debugging * Fixed Simon Deleuran Laursen's mistake * Fixed tests * Reduces * updated tests * Naming * can make graph from cyclic components, and cyclic component added. Updated .gitignore to ignore .ds_store file (generated by macos) * added guard dependencies to edges * Refactor * Test fix-ish * Removes from updates * Added invariant_dependencies to nodes and converted graph.nodes to a Hashmap instead of a Vec * fixed unused clock detection test * made clock reduction better * fixed naming * Fixed another test * Refactor * fixed another test * Fix error * merged advanced-clock-reduction * removed unnecessary mut * merged * Refactor * fixed tests * added processing to json component * added two test cases * added comments to find_equivalent_clock_groups * Fixed clock reduction tests in the simple cases * helper functions * fixed clock reduction * Error handling * fmt * working on test_check_declarations_unused_clock_are_removed * tiny refactor * start testfunc * Intersect * Small fixes * Fix removal * Added clock removal test for unused and duplicated clocks & removed advanced clock reduction samples * Fix warnings * Fixed SystemRecipe.height * Remove print * Fmt * Fixed comments Co-authored-by: Simon Laursen <69715502+Laursen79@users.noreply.github.com> Co-authored-by: Kira Stæhr Pedersen <74182118+KiraStaehr@users.noreply.github.com> Co-authored-by: Alexander Steffensen Co-authored-by: alexsteffensen Co-authored-by: Jens Emil Fink Højriis <5774453+JE-FH@users.noreply.github.com> --- .gitignore | 4 +- Ecdar-ProtoBuf | 2 +- .../RedundantClocks/SystemDeclaration.json | 4 + .../RedundantClocks/Systems/System1.json | 20 ++ src/DataReader/parse_edge.rs | 2 +- src/ModelObjects/component.rs | 320 ++++------------- src/System/extract_system_rep.rs | 152 ++++++-- src/TransitionSystems/common.rs | 102 +++--- src/TransitionSystems/compiled_component.rs | 75 ++-- src/TransitionSystems/composition.rs | 4 + src/TransitionSystems/conjunction.rs | 4 + src/TransitionSystems/location_tuple.rs | 5 +- src/TransitionSystems/quotient.rs | 15 +- src/TransitionSystems/transition_system.rs | 332 +++++++++++++++++- src/lib.rs | 7 + .../ClockReduction/clock_removal_test.rs | 68 +++- src/tests/ClockReduction/helper.rs | 243 +++---------- src/tests/ClockReduction/mod.rs | 1 - .../redundant_clock_detection_test.rs | 62 ++-- src/tests/ClockReduction/replaced_clocks.rs | 59 ---- .../unused_clock_detection_test.rs | 39 +- src/tests/grpc/send_query.rs | 3 +- 22 files changed, 821 insertions(+), 702 deletions(-) create mode 100644 samples/json/ClockReductionTest/RedundantClocks/SystemDeclaration.json create mode 100644 samples/json/ClockReductionTest/RedundantClocks/Systems/System1.json delete mode 100644 src/tests/ClockReduction/replaced_clocks.rs diff --git a/.gitignore b/.gitignore index 07e96df1..5d55d160 100644 --- a/.gitignore +++ b/.gitignore @@ -8,4 +8,6 @@ dbm/buildw/ *.a *.obj Cargo.lock -.DS_Store +*.DS_Store +**/*.DS_Store + diff --git a/Ecdar-ProtoBuf b/Ecdar-ProtoBuf index a6baa73e..c1d41acd 160000 --- a/Ecdar-ProtoBuf +++ b/Ecdar-ProtoBuf @@ -1 +1 @@ -Subproject commit a6baa73e9fa8405d419f3065580674587c3ea971 +Subproject commit c1d41acd0cde29599f0225536bea565d0d9c9589 diff --git a/samples/json/ClockReductionTest/RedundantClocks/SystemDeclaration.json b/samples/json/ClockReductionTest/RedundantClocks/SystemDeclaration.json new file mode 100644 index 00000000..aa4c231a --- /dev/null +++ b/samples/json/ClockReductionTest/RedundantClocks/SystemDeclaration.json @@ -0,0 +1,4 @@ +{ + "name": "System Declarations", + "declarations": "system Component1;\n IO Component1 {foo!, bar?, baz?}" +} \ No newline at end of file diff --git a/samples/json/ClockReductionTest/RedundantClocks/Systems/System1.json b/samples/json/ClockReductionTest/RedundantClocks/Systems/System1.json new file mode 100644 index 00000000..45db5ca0 --- /dev/null +++ b/samples/json/ClockReductionTest/RedundantClocks/Systems/System1.json @@ -0,0 +1,20 @@ +{ + "name": "System1", + "description": "", + "x": 182.0, + "y": 94.0, + "width": 600.0, + "height": 600.0, + "color": "4", + "systemRootX": 267.2, + "componentInstances": [ + { + "id": 1, + "componentName": "Component1", + "x": 162.66666666666666, + "y": 250.0 + } + ], + "operators": [], + "edges": [] +} \ No newline at end of file diff --git a/src/DataReader/parse_edge.rs b/src/DataReader/parse_edge.rs index 05537dec..1a1ee12e 100644 --- a/src/DataReader/parse_edge.rs +++ b/src/DataReader/parse_edge.rs @@ -23,7 +23,7 @@ pub enum EdgeAttribute { Guard(BoolExpression), } -#[derive(Debug, Clone, Deserialize, Serialize, std::cmp::PartialEq, std::cmp::Eq)] +#[derive(Debug, Clone, Deserialize, Serialize, PartialEq, Eq)] pub struct Update { pub variable: String, #[serde(serialize_with = "encode_boolexpr")] diff --git a/src/ModelObjects/component.rs b/src/ModelObjects/component.rs index 0a20d17d..3968037c 100644 --- a/src/ModelObjects/component.rs +++ b/src/ModelObjects/component.rs @@ -20,7 +20,7 @@ use std::collections::{HashMap, HashSet}; use std::fmt; /// The basic struct used to represent components read from either Json or xml -#[derive(Debug, Deserialize, Serialize, Clone)] +#[derive(Debug, Deserialize, Serialize, Clone, Eq, PartialEq)] #[serde(into = "DummyComponent")] pub struct Component { pub name: String, @@ -137,7 +137,7 @@ impl Component { pub fn get_input_actions(&self) -> Vec { let mut actions = vec![]; - for edge in self.input_edges.as_ref().unwrap() { + for edge in self.input_edges.as_ref().unwrap_or(&vec![]) { if *edge.get_sync_type() == SyncType::Input && !contain(&actions, edge.get_sync()) { if edge.get_sync() == "*" { continue; @@ -152,7 +152,7 @@ impl Component { pub fn get_output_actions(&self) -> Vec { let mut actions = vec![]; - for edge in self.output_edges.as_ref().unwrap() { + for edge in self.output_edges.as_ref().unwrap_or(&vec![]) { if *edge.get_sync_type() == SyncType::Output && !contain(&actions, edge.get_sync()) { if edge.get_sync() == "*" { continue; @@ -268,266 +268,80 @@ impl Component { self.create_edge_io_split(); } - /// Function for reducing the clocks found on the component. - /// Unused clocks and "duplicate" clocks (clocks that are never reset) - /// and then remove them. - pub fn reduce_clocks(&mut self, redundant_clocks: Vec) { - for clock in redundant_clocks { - match &clock.reason { - ClockReductionReason::Duplicate(global) => { - self.replace_clock(&clock, global); - info!("Replaced Clock {} with {global}", clock.clock); // Should be changed in the future to be the information logger - } - ClockReductionReason::Unused => { - self.remove_clock(&clock.updates); - info!("Removed Clock {}", clock.clock); - } - } - - let clock_val = *self - .declarations - .clocks - .get(clock.clock.as_str()) - .unwrap_or_else(|| panic!("Clock {} is not in the declarations", clock.clock)); - self.declarations - .clocks - .values_mut() - .filter(|val| **val > clock_val) - .for_each(|val| *val -= 1); - self.declarations.clocks.remove(clock.clock.as_str()); - } - } - - /// Used to find redundant clocks - checks for unused and duplicates clocks. - - /// Returns [`Vec`] with all found redundant clock. - /// If no redundant clocks are found the vector will be empty - pub(crate) fn find_redundant_clocks(&self) -> Vec { - let mut out: Vec = vec![]; - let mut seen_clocks: HashMap; 2]>> = - self.clocks_in_edges_and_locations(&mut out); - let seen_updates: HashMap> = self.clocks_in_updates(&mut out); - - let mut global: Option = None; - for (clock, places) in seen_clocks + /// Removes unused clock + /// # Arguments + /// `index`: The index to be removed + pub(crate) fn remove_clock(&mut self, index: ClockIndex) { + // Removes from declarations, and updates the other + let name = self + .declarations + .get_clock_name_by_index(index) + .expect("Couldn't find clock with index") + .to_owned(); + self.declarations.clocks.remove(&name); + self.declarations + .clocks + .values_mut() + .filter(|val| **val > index) + .for_each(|val| *val -= 1); + + // Yeets from updates + self.edges .iter_mut() - .filter(|(x, _)| !seen_updates.contains_key(x.as_str())) - { - if let Some(global_clock) = &global { - out.push(RedundantClock::duplicate( - clock.to_string(), - places[0].clone(), - places[1].clone(), - global_clock.clone(), - )); - } else { - global = Some(clock.to_string()); - } - } - out - } - - /// This function loop loops over the edges and locations that have guards and invariants, and returns said clocks - fn clocks_in_edges_and_locations( - &self, - seen: &mut Vec, - ) -> HashMap; 2]>> { - let clocks: HashSet = self.declarations.get_clocks().keys().cloned().collect(); - let mut out: HashMap; 2]>> = HashMap::new(); - - // `index` is the index in either `self.edges` or `self.locations` - // `expr` is the guard or invariant itself - // `which` determines if it is an edge or location, used for saving the indices correctly (0 = edge, 1 = location) - for (index, expr, which) in self - .edges - .iter() - .enumerate() - .filter(|(_, x)| x.guard.is_some()) - .map(|(i, e)| (i, e.guard.as_ref().unwrap(), 0)) - .chain( - self.locations + .filter(|e| e.update.is_some()) + .for_each(|e| { + if let Some((i, _)) = e + .update + .as_ref() + .unwrap() .iter() .enumerate() - .filter(|(_, x)| x.invariant.is_some()) - .map(|(i, l)| (i, l.invariant.as_ref().unwrap(), 1)), - ) - { - // Here we find all varnames in the expression so we can save where it is used - for name in expr.get_varnames() { - if clocks.contains(name) { - if let Some(clock_indices) = out.get_mut(name) { - // Either we have seen the clock, and just add the index in the correct vec (edge or location) - // We know that `which` will be valid because we set it in the loop above - clock_indices.get_mut(which).unwrap().push(index); - } else { - // Or we have not seen the clock before, and have to input it in the HashMap - // and then input the index correctly - out.insert(name.to_string(), Box::new([vec![], vec![]])); - out.get_mut(name) - .unwrap() - .get_mut(which) - .unwrap() - .push(index); - } - } - } - } - for contain in clocks.iter().filter(|k| !out.contains_key(*k)) { - seen.push(RedundantClock::unused(contain.clone())); - } - out - } - - /// This function loop loops over the updates in the component. - /// It saves the indices of already seen clocks (unused clocks that should be removed), - /// and returns all other clocks it finds - fn clocks_in_updates( - &self, - seen: &mut [RedundantClock], - ) -> HashMap> { - let mut out: HashMap> = HashMap::new(); - for (i, updates) in self - .edges - .iter() - .enumerate() - .filter(|(_, x)| x.update.is_some()) - .map(|(i, y)| (i, y.update.as_ref().unwrap())) - { - for (j, upd) in updates.iter().enumerate() { - if let Some(c) = seen.iter_mut().find(|x| x.clock == upd.variable) { - c.updates.insert(i, j); - } else { - out.entry(upd.variable.clone()) - .or_insert_with(HashMap::new) - .entry(i) - .or_insert(j); + .find(|(_, u)| u.variable == name) + { + e.update.as_mut().unwrap().remove(i); } - } - } - out - } - - /// Removes unused clock - - /// # Arguments - /// `clock_updates`: Hashmap where the keys are the indices for the `edges`, and the value is the index in `updates` on said edge - pub(crate) fn remove_clock(&mut self, clock_updates: &HashMap) { - for (i, u) in clock_updates { - self.edges[*i] - .update - .as_mut() - .expect("No updates on the edge") - .remove(*u); - } + }); + info!( + "Removed Clock '{name}' has been removed from component {}", + self.name + ); // Should be changed in the future to be the information logger } /// Replaces duplicate clock with a new /// # Arguments - /// `clock`: [`RedundantClock`] representing the clock to be replaced - /// `other_clock`: The name of the clock to replace `clock` - pub(crate) fn replace_clock(&mut self, clock: &RedundantClock, other_clock: &String) { - for e in &clock.edge_indices { - self.edges[*e] - .guard - .as_mut() - .unwrap() - .replace_varname(&clock.clock, other_clock); - } - for l in &clock.location_indices { - self.locations[*l] - .invariant - .as_mut() - .unwrap() - .replace_varname(&clock.clock, other_clock); - } - for (i, u) in &clock.updates { - let mut upd = &mut self.edges[*i].update.as_mut().unwrap()[*u]; - (*upd).variable = other_clock.clone(); - upd.expression.replace_varname(&clock.clock, other_clock); - } - } -} - -///Enum to hold the reason for why a clock is declared redundant. -#[derive(Debug)] -pub enum ClockReductionReason { - ///Which clock is it a duplicate of. - Duplicate(String), - ///If a clock is not used by a guard or invariant it is unused. - Unused, -} - -///Datastructure to hold the found redundant clocks, where they are used and their reason for being redundant. -#[derive(Debug)] -#[allow(dead_code)] -pub struct RedundantClock { - ///Name of the redundant clock. - pub(crate) clock: String, - ///Indices of which edges the clock are being used on. - pub(crate) edge_indices: Vec, - ///Indices of which locations the clock are being used in. - pub(crate) location_indices: Vec, - ///Reason for why the clock is declared redundant. - pub(crate) reason: ClockReductionReason, - /// Which updates clock occurs in. Key is index of edge and Value is the index for the update - pub(crate) updates: HashMap, -} - -impl RedundantClock { - ///Creates a new [`RedundantClock`] - #[allow(unused)] - fn new( - clock: String, - edge_indices: Vec, - location_indices: Vec, - reason: ClockReductionReason, - updates: HashMap, - ) -> RedundantClock { - RedundantClock { - clock, - edge_indices, - location_indices, - reason, - updates, - } - } - - ///Shorthand function to create a duplicated [`RedundantClock`] - fn duplicate( - clock: String, - edge_indices: Vec, - location_indices: Vec, - duplicate: String, - ) -> RedundantClock { - RedundantClock { - clock, - edge_indices, - location_indices, - reason: ClockReductionReason::Duplicate(duplicate), - updates: HashMap::new(), + /// `global_index`: The index of the global clock\n + /// `indices` are the duplicate clocks that should be set to `global_index` + pub(crate) fn replace_clock( + &mut self, + global_index: ClockIndex, + indices: &HashSet, + ) { + for (name, index) in self + .declarations + .clocks + .iter_mut() + .filter(|(_, c)| indices.contains(c)) + { + *index = global_index; + // TODO: Maybe log the global clock name instead of index + info!("Replaced Clock {name} with {global_index}"); // Should be changed in the future to be the information logger } } - ///Shorthand function to create a unused [`RedundantClock`] - fn unused(clock: String) -> RedundantClock { - RedundantClock { - clock, - edge_indices: vec![], - location_indices: vec![], - reason: ClockReductionReason::Unused, - updates: HashMap::new(), + /// Decrements the indices of the clocks to decrement the DBM + pub(crate) fn decrement_dim(&mut self, decr: usize, omit: Vec) { + for index in self + .declarations + .clocks + .values_mut() + .filter(|i| !omit.contains(i)) + { + *index -= decr; } } } - pub fn contain(channels: &[Channel], channel: &str) -> bool { - for c in channels { - if c.name == channel { - return true; - } - } - - false + channels.iter().any(|c| c.name == channel) } /// FullState is a struct used for initial verification of consistency, and determinism as a state that also hols a dbm @@ -657,6 +471,7 @@ pub struct Transition { pub target_locations: LocationTuple, pub updates: Vec, } + impl Transition { /// Create a new transition not based on an edge with no identifier pub fn new(target_locations: &LocationTuple, dim: ClockIndex) -> Transition { @@ -1093,4 +908,13 @@ impl Declarations { pub fn get_clock_index_by_name(&self, name: &str) -> Option<&ClockIndex> { self.get_clocks().get(name) } + + /// Gets the name of a given `ClockIndex`. + /// Returns `None` if it does not exist in the declarations + pub fn get_clock_name_by_index(&self, index: ClockIndex) -> Option<&String> { + self.clocks + .iter() + .find(|(_, v)| **v == index) + .map(|(k, _)| k) + } } diff --git a/src/System/extract_system_rep.rs b/src/System/extract_system_rep.rs index 772dd70a..d57d9be7 100644 --- a/src/System/extract_system_rep.rs +++ b/src/System/extract_system_rep.rs @@ -7,17 +7,20 @@ use crate::System::executable_query::{ ReachabilityExecutor, RefinementExecutor, }; use crate::System::extract_state::get_state; +use std::cmp::max; +use std::collections::HashSet; use crate::TransitionSystems::{ CompiledComponent, Composition, Conjunction, Quotient, TransitionSystemPtr, }; use crate::component::State; +use crate::ProtobufServer::services::query_request::{settings::ReduceClocksLevel, Settings}; use crate::System::pruning; +use crate::TransitionSystems::transition_system::{ClockReductionInstruction, Heights, Intersect}; use edbm::util::constraints::ClockIndex; use log::debug; use simple_error::bail; - use std::error::Error; /// This function fetches the appropriate components based on the structure of the query and makes the enum structure match the query @@ -32,8 +35,10 @@ pub fn create_executable_query<'a>( match query { QueryExpression::Refinement(left_side, right_side) => { let mut quotient_index = None; - let left = get_system_recipe(left_side, component_loader, &mut dim, &mut quotient_index); - let right = get_system_recipe(right_side, component_loader, &mut dim, &mut quotient_index); + + let mut left = get_system_recipe(left_side, component_loader, &mut dim, &mut quotient_index); + let mut right = get_system_recipe(right_side, component_loader, &mut dim, &mut quotient_index); + clock_reduction(&mut left, &mut right, component_loader.get_settings(), &mut dim)?; Ok(Box::new(RefinementExecutor { sys1: left.compile(dim)?, sys2: right.compile(dim)?, @@ -76,14 +81,16 @@ pub fn create_executable_query<'a>( ), dim })), - QueryExpression::Determinism(query_expression) => Ok(Box::new(DeterminismExecutor { - system: get_system_recipe( - query_expression, - component_loader, - &mut dim, - &mut None - ).compile(dim)?, - })), + QueryExpression::Determinism(query_expression) => { + Ok(Box::new(DeterminismExecutor { + system: get_system_recipe( + query_expression, + component_loader, + &mut dim, + &mut None, + ).compile(dim)?, + })) + }, QueryExpression::GetComponent(save_as_expression) => { if let QueryExpression::SaveAs(query_expression, comp_name) = save_as_expression.as_ref() { Ok(Box::new( @@ -120,6 +127,52 @@ pub fn create_executable_query<'a>( } } +fn clock_reduction( + left: &mut Box, + right: &mut Box, + set: &Settings, + dim: &mut usize, +) -> Result<(), String> { + let height = max(left.height(), right.height()); + let heights = match set.reduce_clocks_level.to_owned().ok_or_else(|| "No clock reduction level specified".to_string())? { + ReduceClocksLevel::Level(y) if y >= 0 => Heights::new(height, y as usize), + ReduceClocksLevel::All(true) => Heights::new(height, height), + ReduceClocksLevel::All(false) => return Ok(()), + ReduceClocksLevel::Level(err) => return Err(format!("Clock reduction error: Couldn't parse argument correctly. Got {err}, expected a value above")), + }; + + let clocks = left + .clone() + .compile(*dim)? + .find_redundant_clocks(heights) + .intersect(&right.clone().compile(*dim)?.find_redundant_clocks(heights)); + + debug!("Clocks to be reduced: {clocks:?}"); + *dim -= clocks + .iter() + .fold(0, |acc, c| acc + c.clocks_removed_count()); + debug!("New dimension: {dim}"); + + left.reduce_clocks(clocks.clone()); + right.reduce_clocks(clocks); + Ok(()) +} + +fn clean_component_decls(mut comps: Vec<&mut Component>, omit: HashSet<(ClockIndex, usize)>) { + let mut list: Vec<&(ClockIndex, usize)> = omit.iter().collect(); + list.sort_by(|(c1, _), (c2, _)| c1.cmp(c2)); + + for (clock, size) in list.iter().rev() { + comps.iter_mut().for_each(|c| { + c.declarations + .clocks + .values_mut() + .filter(|cl| **cl > *clock) + .for_each(|cl| *cl -= size) + }); + } +} + #[derive(Clone)] pub enum SystemRecipe { Composition(Box, Box), @@ -149,6 +202,72 @@ impl SystemRecipe { }, } } + + /// Gets the height of the `SystemRecipe` tree + fn height(&self) -> usize { + match self { + SystemRecipe::Composition(l, r) + | SystemRecipe::Conjunction(l, r) + | SystemRecipe::Quotient(l, r, _) => 1 + max(l.height(), r.height()), + SystemRecipe::Component(_) => 1, + } + } + + /// Gets the count `Components`s in the `SystemRecipe` + pub fn count_component(&self) -> usize { + match self { + SystemRecipe::Composition(left, right) + | SystemRecipe::Conjunction(left, right) + | SystemRecipe::Quotient(left, right, _) => { + left.count_component() + right.count_component() + } + SystemRecipe::Component(_) => 1, + } + } + + ///Applies the clock-reduction + pub(crate) fn reduce_clocks(&mut self, clock_instruction: Vec) { + let mut comps = self.get_components(); + let mut omitting = HashSet::new(); + for redundant in clock_instruction { + match redundant { + ClockReductionInstruction::RemoveClock { clock_index } => { + match comps + .iter_mut() + .find(|c| c.declarations.clocks.values().any(|ci| *ci == clock_index)) + { + Some(c) => c.remove_clock(clock_index), + None => continue, + } + omitting.insert((clock_index, 1)); + } + ClockReductionInstruction::ReplaceClocks { + clock_indices, + clock_index, + } => { + comps + .iter_mut() + .for_each(|c| c.replace_clock(clock_index, &clock_indices)); + omitting.insert((clock_index, clock_indices.len())); + } + } + } + clean_component_decls(comps, omitting); + } + + /// Gets all components in `SystemRecipe` + fn get_components(&mut self) -> Vec<&mut Component> { + match self { + SystemRecipe::Composition(left, right) + | SystemRecipe::Conjunction(left, right) + | SystemRecipe::Quotient(left, right, _) => { + let mut o = left.get_components(); + o.extend(right.get_components()); + o + } + SystemRecipe::Component(c) => vec![c], + } + } } pub fn get_system_recipe( @@ -205,7 +324,7 @@ fn validate_reachability_input( state: &QueryExpression, ) -> Result<(), String> { if let QueryExpression::State(loc_names, _) = state { - if loc_names.len() != count_component(machine) { + if loc_names.len() != machine.count_component() { return Err( "The number of automata does not match the number of locations".to_string(), ); @@ -219,12 +338,3 @@ fn validate_reachability_input( Ok(()) } - -fn count_component(system: &SystemRecipe) -> usize { - match system { - SystemRecipe::Composition(left, right) => count_component(left) + count_component(right), - SystemRecipe::Conjunction(left, right) => count_component(left) + count_component(right), - SystemRecipe::Quotient(left, right, _) => count_component(left) + count_component(right), - SystemRecipe::Component(_) => 1, - } -} diff --git a/src/TransitionSystems/common.rs b/src/TransitionSystems/common.rs index a91caf25..c9345835 100644 --- a/src/TransitionSystems/common.rs +++ b/src/TransitionSystems/common.rs @@ -7,15 +7,13 @@ use edbm::{ }; use log::warn; +use crate::TransitionSystems::CompositionType; use crate::{ ModelObjects::component::{Declarations, State, Transition}, System::local_consistency::{ConsistencyResult, DeterminismResult}, }; -use super::{ - transition_system::PrecheckResult, CompositionType, LocationTuple, TransitionSystem, - TransitionSystemPtr, -}; +use super::{LocationTuple, TransitionSystem, TransitionSystemPtr}; pub trait ComposedTransitionSystem: DynClone { fn next_transitions(&self, location: &LocationTuple, action: &str) -> Vec; @@ -24,6 +22,8 @@ pub trait ComposedTransitionSystem: DynClone { fn get_children(&self) -> (&TransitionSystemPtr, &TransitionSystemPtr); + fn get_children_mut(&mut self) -> (&mut TransitionSystemPtr, &mut TransitionSystemPtr); + fn get_composition_type(&self) -> CompositionType; fn get_dim(&self) -> ClockIndex; @@ -36,16 +36,34 @@ pub trait ComposedTransitionSystem: DynClone { clone_trait_object!(ComposedTransitionSystem); impl TransitionSystem for T { + fn get_local_max_bounds(&self, loc: &LocationTuple) -> Bounds { + if loc.is_universal() || loc.is_inconsistent() { + Bounds::new(self.get_dim()) + } else { + let (left, right) = self.get_children(); + let loc_l = loc.get_left(); + let loc_r = loc.get_right(); + let mut bounds_l = left.get_local_max_bounds(loc_l); + let bounds_r = right.get_local_max_bounds(loc_r); + bounds_l.add_bounds(&bounds_r); + bounds_l + } + } + + fn get_dim(&self) -> ClockIndex { + self.get_dim() + } fn next_transitions(&self, location: &LocationTuple, action: &str) -> Vec { self.next_transitions(location, action) } - fn get_input_actions(&self) -> HashSet { self.get_input_actions() } + fn get_output_actions(&self) -> HashSet { self.get_output_actions() } + fn get_actions(&self) -> HashSet { self.get_input_actions() .union(&self.get_output_actions()) @@ -53,20 +71,6 @@ impl TransitionSystem for T { .collect() } - fn get_local_max_bounds(&self, loc: &LocationTuple) -> Bounds { - if loc.is_universal() || loc.is_inconsistent() { - Bounds::new(self.get_dim()) - } else { - let (left, right) = self.get_children(); - let loc_l = loc.get_left(); - let loc_r = loc.get_right(); - let mut bounds_l = left.get_local_max_bounds(loc_l); - let bounds_r = right.get_local_max_bounds(loc_r); - bounds_l.add_bounds(&bounds_r); - bounds_l - } - } - fn get_initial_location(&self) -> Option { let (left, right) = self.get_children(); let l = left.get_initial_location()?; @@ -75,6 +79,24 @@ impl TransitionSystem for T { Some(LocationTuple::compose(&l, &r, self.get_composition_type())) } + fn get_all_locations(&self) -> Vec { + let (left, right) = self.get_children(); + let mut location_tuples = vec![]; + let left = left.get_all_locations(); + let right = right.get_all_locations(); + for loc1 in &left { + for loc2 in &right { + location_tuples.push(LocationTuple::compose( + loc1, + loc2, + self.get_composition_type(), + )); + } + } + location_tuples + } + + /// Returns the declarations of both children. fn get_decls(&self) -> Vec<&Declarations> { let (left, right) = self.get_children(); @@ -83,19 +105,6 @@ impl TransitionSystem for T { comps } - fn precheck_sys_rep(&self) -> PrecheckResult { - if let DeterminismResult::Failure(location, action) = self.is_deterministic() { - warn!("Not deterministic"); - return PrecheckResult::NotDeterministic(location, action); - } - - if let ConsistencyResult::Failure(failure) = self.is_locally_consistent() { - warn!("Not consistent"); - return PrecheckResult::NotConsistent(failure); - } - PrecheckResult::Success - } - fn is_deterministic(&self) -> DeterminismResult { let (left, right) = self.get_children(); if let DeterminismResult::Success = left.is_deterministic() { @@ -109,6 +118,10 @@ impl TransitionSystem for T { } } + fn is_locally_consistent(&self) -> ConsistencyResult { + self.is_locally_consistent() + } + fn get_initial_state(&self) -> Option { let init_loc = self.get_initial_location().unwrap(); let mut zone = OwnedFederation::init(self.get_dim()); @@ -121,31 +134,6 @@ impl TransitionSystem for T { Some(State::create(init_loc, zone)) } - fn get_dim(&self) -> ClockIndex { - self.get_dim() - } - - fn get_all_locations(&self) -> Vec { - let (left, right) = self.get_children(); - let mut location_tuples = vec![]; - let left = left.get_all_locations(); - let right = right.get_all_locations(); - for loc1 in &left { - for loc2 in &right { - location_tuples.push(LocationTuple::compose( - loc1, - loc2, - self.get_composition_type(), - )); - } - } - location_tuples - } - - fn is_locally_consistent(&self) -> ConsistencyResult { - self.is_locally_consistent() - } - fn get_children(&self) -> (&TransitionSystemPtr, &TransitionSystemPtr) { self.get_children() } diff --git a/src/TransitionSystems/compiled_component.rs b/src/TransitionSystems/compiled_component.rs index db8c25f6..4cb58979 100644 --- a/src/TransitionSystems/compiled_component.rs +++ b/src/TransitionSystems/compiled_component.rs @@ -5,11 +5,9 @@ use crate::System::local_consistency::{self, ConsistencyResult, DeterminismResul use crate::TransitionSystems::{LocationTuple, TransitionSystem, TransitionSystemPtr}; use edbm::util::bounds::Bounds; use edbm::util::constraints::ClockIndex; -use log::warn; use std::collections::hash_set::HashSet; use std::collections::HashMap; -use super::transition_system::PrecheckResult; use super::{CompositionType, LocationID}; type Action = String; @@ -115,32 +113,8 @@ impl TransitionSystem for CompiledComponent { } } - fn get_composition_type(&self) -> CompositionType { - panic!("Components do not have a composition type") - } - - fn get_decls(&self) -> Vec<&Declarations> { - vec![&self.comp_info.declarations] - } - - fn get_input_actions(&self) -> HashSet { - self.inputs.clone() - } - - fn get_output_actions(&self) -> HashSet { - self.outputs.clone() - } - - fn get_actions(&self) -> HashSet { - self.inputs.union(&self.outputs).cloned().collect() - } - - fn get_initial_location(&self) -> Option { - self.initial_location.clone() - } - - fn get_all_locations(&self) -> Vec { - self.locations.values().cloned().collect() + fn get_dim(&self) -> ClockIndex { + self.dim } fn next_transitions(&self, locations: &LocationTuple, action: &str) -> Vec { @@ -167,27 +141,28 @@ impl TransitionSystem for CompiledComponent { transitions } - fn get_initial_state(&self) -> Option { - let init_loc = self.get_initial_location().unwrap(); + fn get_input_actions(&self) -> HashSet { + self.inputs.clone() + } - State::from_location(init_loc, self.dim) + fn get_output_actions(&self) -> HashSet { + self.outputs.clone() } - fn get_children(&self) -> (&TransitionSystemPtr, &TransitionSystemPtr) { - unimplemented!() + fn get_actions(&self) -> HashSet { + self.inputs.union(&self.outputs).cloned().collect() } - fn precheck_sys_rep(&self) -> PrecheckResult { - if let DeterminismResult::Failure(location, action) = self.is_deterministic() { - warn!("Not deterministic"); - return PrecheckResult::NotDeterministic(location, action); - } + fn get_initial_location(&self) -> Option { + self.initial_location.clone() + } - if let ConsistencyResult::Failure(failure) = self.is_locally_consistent() { - warn!("Not consistent"); - return PrecheckResult::NotConsistent(failure); - } - PrecheckResult::Success + fn get_all_locations(&self) -> Vec { + self.locations.values().cloned().collect() + } + + fn get_decls(&self) -> Vec<&Declarations> { + vec![&self.comp_info.declarations] } fn is_deterministic(&self) -> DeterminismResult { @@ -198,8 +173,18 @@ impl TransitionSystem for CompiledComponent { local_consistency::is_least_consistent(self) } - fn get_dim(&self) -> ClockIndex { - self.dim + fn get_initial_state(&self) -> Option { + let init_loc = self.get_initial_location().unwrap(); + + State::from_location(init_loc, self.dim) + } + + fn get_children(&self) -> (&TransitionSystemPtr, &TransitionSystemPtr) { + unimplemented!() + } + + fn get_composition_type(&self) -> CompositionType { + panic!("Components do not have a composition type") } fn get_combined_decls(&self) -> Declarations { diff --git a/src/TransitionSystems/composition.rs b/src/TransitionSystems/composition.rs index 88cbe3b7..b42b5a35 100644 --- a/src/TransitionSystems/composition.rs +++ b/src/TransitionSystems/composition.rs @@ -120,6 +120,10 @@ impl ComposedTransitionSystem for Composition { (&self.left, &self.right) } + fn get_children_mut(&mut self) -> (&mut TransitionSystemPtr, &mut TransitionSystemPtr) { + (&mut self.left, &mut self.right) + } + fn get_composition_type(&self) -> CompositionType { CompositionType::Composition } diff --git a/src/TransitionSystems/conjunction.rs b/src/TransitionSystems/conjunction.rs index d5c4faa5..f62d4892 100644 --- a/src/TransitionSystems/conjunction.rs +++ b/src/TransitionSystems/conjunction.rs @@ -82,6 +82,10 @@ impl ComposedTransitionSystem for Conjunction { (&self.left, &self.right) } + fn get_children_mut(&mut self) -> (&mut TransitionSystemPtr, &mut TransitionSystemPtr) { + (&mut self.left, &mut self.right) + } + fn get_composition_type(&self) -> CompositionType { CompositionType::Conjunction } diff --git a/src/TransitionSystems/location_tuple.rs b/src/TransitionSystems/location_tuple.rs index 21aee6fe..9f1c1ed6 100644 --- a/src/TransitionSystems/location_tuple.rs +++ b/src/TransitionSystems/location_tuple.rs @@ -7,7 +7,7 @@ use crate::{ use super::LocationID; -#[derive(Debug, Clone, std::cmp::PartialEq, Eq, Hash, Copy)] +#[derive(Debug, Clone, PartialEq, Eq, Hash, Copy)] pub enum CompositionType { Conjunction, Composition, @@ -17,7 +17,8 @@ pub enum CompositionType { #[derive(Clone, Debug)] pub struct LocationTuple { pub id: LocationID, - invariant: Option, + /// The invariant for the `Location` + pub invariant: Option, pub loc_type: LocationType, left: Option>, right: Option>, diff --git a/src/TransitionSystems/quotient.rs b/src/TransitionSystems/quotient.rs index e61d206b..46e5cfea 100644 --- a/src/TransitionSystems/quotient.rs +++ b/src/TransitionSystems/quotient.rs @@ -1,6 +1,6 @@ use edbm::util::constraints::ClockIndex; use edbm::zones::OwnedFederation; -use log::{debug, warn}; +use log::debug; use crate::EdgeEval::updater::CompiledUpdate; use crate::ModelObjects::component::Declarations; @@ -398,19 +398,6 @@ impl TransitionSystem for Quotient { comps } - fn precheck_sys_rep(&self) -> PrecheckResult { - if let DeterminismResult::Failure(location, action) = self.is_deterministic() { - warn!("Not deterministic"); - return PrecheckResult::NotDeterministic(location, action); - } - - if let ConsistencyResult::Failure(failure) = self.is_locally_consistent() { - warn!("Not consistent"); - return PrecheckResult::NotConsistent(failure); - } - PrecheckResult::Success - } - fn is_deterministic(&self) -> DeterminismResult { if let DeterminismResult::Success = self.T.is_deterministic() { if let DeterminismResult::Success = self.S.is_deterministic() { diff --git a/src/TransitionSystems/transition_system.rs b/src/TransitionSystems/transition_system.rs index 2caee0f5..bd04e5f5 100644 --- a/src/TransitionSystems/transition_system.rs +++ b/src/TransitionSystems/transition_system.rs @@ -1,4 +1,5 @@ use super::{CompositionType, LocationID, LocationTuple}; +use crate::EdgeEval::updater::CompiledUpdate; use crate::{ ModelObjects::component::{Declarations, State, Transition}, System::local_consistency::DeterminismResult, @@ -6,9 +7,14 @@ use crate::{ }; use dyn_clone::{clone_trait_object, DynClone}; use edbm::util::{bounds::Bounds, constraints::ClockIndex}; +use log::warn; +use std::collections::hash_map::Entry; use std::collections::{hash_set::HashSet, HashMap}; pub type TransitionSystemPtr = Box; +pub type Action = String; +pub type EdgeTuple = (Action, Transition); +pub type EdgeIndex = (LocationID, usize); /// Precheck can fail because of either consistency or determinism. pub enum PrecheckResult { @@ -17,6 +23,34 @@ pub enum PrecheckResult { NotConsistent(ConsistencyFailure), } +#[derive(Clone, Copy)] +/// Struct for determining the level for clock reduction +pub struct Heights { + /// The level in the tree + pub(crate) tree: usize, + /// The level to reduce + pub(crate) target: usize, +} + +impl Heights { + pub fn new(tree: usize, target: usize) -> Heights { + Heights { tree, target } + } + + /// Function to "go down" a level in the tree + pub fn level_down(&self) -> Heights { + Heights { + tree: self.tree - 1, + ..*self + } + } + + /// Creates an empty `Heights` (ALl values are `0`) + pub fn empty() -> Heights { + Heights::new(0, 0) + } +} + pub trait TransitionSystem: DynClone { fn get_local_max_bounds(&self, loc: &LocationTuple) -> Bounds; @@ -77,6 +111,18 @@ pub trait TransitionSystem: DynClone { fn get_decls(&self) -> Vec<&Declarations>; + fn precheck_sys_rep(&self) -> PrecheckResult { + if let DeterminismResult::Failure(location, action) = self.is_deterministic() { + warn!("Not deterministic"); + return PrecheckResult::NotDeterministic(location, action); + } + + if let ConsistencyResult::Failure(failure) = self.is_locally_consistent() { + warn!("Not consistent"); + return PrecheckResult::NotConsistent(failure); + } + PrecheckResult::Success + } fn get_combined_decls(&self) -> Declarations { let mut clocks = HashMap::new(); let mut ints = HashMap::new(); @@ -89,8 +135,6 @@ pub trait TransitionSystem: DynClone { Declarations { ints, clocks } } - fn precheck_sys_rep(&self) -> PrecheckResult; - fn is_deterministic(&self) -> DeterminismResult; fn is_locally_consistent(&self) -> ConsistencyResult; @@ -100,6 +144,290 @@ pub trait TransitionSystem: DynClone { fn get_children(&self) -> (&TransitionSystemPtr, &TransitionSystemPtr); fn get_composition_type(&self) -> CompositionType; + + ///Constructs a [CLockAnalysisGraph], + ///where nodes represents locations and Edges represent transitions + fn get_analysis_graph(&self) -> ClockAnalysisGraph { + let mut graph: ClockAnalysisGraph = ClockAnalysisGraph::empty(); + graph.dim = self.get_dim(); + let location = self.get_initial_location().unwrap(); + let actions = self.get_actions(); + + self.find_edges_and_nodes(&location, &actions, &mut graph); + + graph + } + + ///Helper function to recursively traverse all transitions in a transitions system + ///in order to find all transitions and location in the transition system, and + ///saves these as [ClockAnalysisEdge]s and [ClockAnalysisNode]s in the [ClockAnalysisGraph] + fn find_edges_and_nodes( + &self, + location: &LocationTuple, + actions: &HashSet, + graph: &mut ClockAnalysisGraph, + ) { + //Constructs a node to represent this location and add it to the graph. + let mut node: ClockAnalysisNode = ClockAnalysisNode { + invariant_dependencies: HashSet::new(), + id: location.id.to_owned(), + }; + + //Finds clocks used in invariants in this location. + if let Some(invariant) = &location.invariant { + let conjunctions = invariant.minimal_constraints().conjunctions; + for conjunction in conjunctions { + for constraint in conjunction.iter() { + node.invariant_dependencies.insert(constraint.i); + node.invariant_dependencies.insert(constraint.j); + } + } + } + graph.nodes.insert(node.id.clone(), node); + + //Constructs an edge to represent each transition from this graph and add it to the graph. + for action in actions.iter() { + let transitions = self.next_transitions_if_available(location, action); + for transition in transitions { + let mut edge = ClockAnalysisEdge { + from: location.id.to_owned(), + to: transition.target_locations.id.clone(), + guard_dependencies: HashSet::new(), + updates: transition.updates, + edge_type: action.to_string(), + }; + + //Finds clocks used in guards in this transition. + let conjunctions = transition.guard_zone.minimal_constraints().conjunctions; + for conjunction in &conjunctions { + for constraint in conjunction.iter() { + edge.guard_dependencies.insert(constraint.i); + edge.guard_dependencies.insert(constraint.j); + } + } + + graph.edges.push(edge); + + //Calls itself on the transitions target location if the location is not already in + //represented as a node in the graph. + if !graph.nodes.contains_key(&transition.target_locations.id) { + self.find_edges_and_nodes(&transition.target_locations, actions, graph); + } + } + } + } + + fn find_redundant_clocks(&self, height: Heights) -> Vec { + if height.tree > height.target { + let (a, b) = self.get_children(); + let mut out = a.find_redundant_clocks(height.clone().level_down()); + out.extend(b.find_redundant_clocks(height.level_down())); + out + } else { + self.get_analysis_graph().find_clock_redundancies() + } + } +} + +pub(crate) trait Intersect { + fn intersect(&self, other: &[T]) -> Vec; +} + +impl Intersect for Vec { + // Prioritizes replacements over removals + fn intersect(&self, other: &[ClockReductionInstruction]) -> Vec { + self.iter() + .filter(|r| r.is_replace()) + .chain(other.iter().filter(|r| r.is_replace())) + .chain( + self.iter() + .filter(|r| !r.is_replace()) + .filter_map(|c| other.iter().filter(|r| !r.is_replace()).find(|rc| *rc == c)), + ) + .cloned() + .collect() + } +} + +#[derive(Debug, Clone, Eq, PartialEq)] +pub enum ClockReductionInstruction { + RemoveClock { + clock_index: ClockIndex, + }, + ReplaceClocks { + clock_index: ClockIndex, + clock_indices: HashSet, + }, +} + +impl ClockReductionInstruction { + pub(crate) fn clocks_removed_count(&self) -> usize { + match self { + ClockReductionInstruction::RemoveClock { .. } => 1, + ClockReductionInstruction::ReplaceClocks { clock_indices, .. } => clock_indices.len(), + } + } + + fn is_replace(&self) -> bool { + match self { + ClockReductionInstruction::RemoveClock { .. } => false, + ClockReductionInstruction::ReplaceClocks { .. } => true, + } + } +} + +#[derive(Debug)] +pub struct ClockAnalysisNode { + pub invariant_dependencies: HashSet, + pub id: LocationID, +} + +#[derive(Debug)] +pub struct ClockAnalysisEdge { + pub from: LocationID, + pub to: LocationID, + pub guard_dependencies: HashSet, + pub updates: Vec, + pub edge_type: String, +} + +#[derive(Debug)] +pub struct ClockAnalysisGraph { + pub nodes: HashMap, + pub edges: Vec, + pub dim: ClockIndex, +} + +impl ClockAnalysisGraph { + pub fn empty() -> ClockAnalysisGraph { + ClockAnalysisGraph { + nodes: HashMap::new(), + edges: vec![], + dim: 0, + } + } + + pub fn find_clock_redundancies(&self) -> Vec { + //First we find the used clocks + let used_clocks = self.find_used_clocks(); + + //Then we instruct the caller to remove the unused clocks, we start at 1 since the 0 clock is not a real clock + let mut unused_clocks = (1..self.dim).collect::>(); + for used_clock in &used_clocks { + unused_clocks.remove(used_clock); + } + + let mut rv: Vec = Vec::new(); + for unused_clock in &unused_clocks { + rv.push(ClockReductionInstruction::RemoveClock { + clock_index: *unused_clock, + }); + } + + let mut equivalent_clock_groups = self.find_equivalent_clock_groups(&used_clocks); + + for equivalent_clock_group in &mut equivalent_clock_groups { + let lowest_clock = *equivalent_clock_group.iter().min().unwrap(); + equivalent_clock_group.remove(&lowest_clock); + rv.push(ClockReductionInstruction::ReplaceClocks { + clock_index: lowest_clock, + clock_indices: equivalent_clock_group.clone(), + }); + } + + rv + } + + fn find_used_clocks(&self) -> HashSet { + let mut used_clocks = HashSet::new(); + + //First we find the used clocks + for edge in &self.edges { + for guard_dependency in &edge.guard_dependencies { + used_clocks.insert(*guard_dependency); + } + } + + for node in &self.nodes { + for invariant_dependency in &node.1.invariant_dependencies { + used_clocks.insert(*invariant_dependency); + } + } + + //Clock index 0 is not a real clock therefore it is removed + used_clocks.remove(&0); + + used_clocks + } + + fn find_equivalent_clock_groups( + &self, + used_clocks: &HashSet, + ) -> Vec> { + if used_clocks.len() < 2 || self.edges.is_empty() { + return Vec::new(); + } + let mut equivalent_clock_groups: Vec> = Vec::new(); + + //This function works by maintaining the loop invariant that equivalent_clock_groups contains + //groups containing clocks where all clocks contained are equivalent in all edges we have iterated + //through. We also have to make sure that each clock are only present in one group at a time. + //This means that for the first iteration all clocks are equivalent. We do not include + //unused clocks since they are all equivalent and will removed completely in another stage. + equivalent_clock_groups.push(used_clocks.clone()); + + for edge in &self.edges { + //First the clocks which are equivalent in this edge are found. This is defined by every + //clock in their respective group are set to the same value. This is done through a + //HashMap with the value being key and the group of clocks being the value + let mut locally_equivalent_clock_groups: HashMap> = + HashMap::new(); + //Here the clocks are grouped by the value they are set to + for update in edge.updates.iter() { + //This gets the values' clock group or creates a new one and inserts the new one + //in the hashset and returns a mutable reference + let clock_group: &mut HashSet = + match locally_equivalent_clock_groups.entry(update.value) { + Entry::Occupied(o) => o.into_mut(), + Entry::Vacant(v) => v.insert(HashSet::new()), + }; + clock_group.insert(update.clock_index); + } + //Then we maintain the loop invariant by creating a new list of clock groups and + //dividing the old groups when clocks are found to not be equivalent + let mut new_groups: Vec> = Vec::new(); + //We do this by iterating on each globally equivalent clock group and removing the clocks + //that are not updated to the same value + for equivalent_clock_group in &mut equivalent_clock_groups { + //For each of the locally equivalent clock groups we can construct a new clock group + //for the clocks that are in the globally equivalant clock group we are iterating + //over now. + //Then we remove the clocks from the globally equivalent clocks that we use in + //the new group + for locally_equivalent_clock_group in &locally_equivalent_clock_groups { + let mut new_clock_group = HashSet::new(); + for locally_equivalent_clock in locally_equivalent_clock_group.1 { + if equivalent_clock_group.contains(locally_equivalent_clock) { + new_clock_group.insert(*locally_equivalent_clock); + equivalent_clock_group.remove(locally_equivalent_clock); + } + } + //If the new clock group only contains one clock then there is no reason to keep + //Track of it, since it will never be redundant + if new_clock_group.len() > 1 { + new_groups.push(new_clock_group); + } + } + //The same thing is done here + if equivalent_clock_group.len() > 1 { + new_groups.push(equivalent_clock_group.clone()); + } + } + //Then we use the new groups which uphold the loop invariant + equivalent_clock_groups = new_groups; + } + equivalent_clock_groups + } } clone_trait_object!(TransitionSystem); diff --git a/src/lib.rs b/src/lib.rs index 6313514d..f3b7b900 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -22,11 +22,18 @@ pub use ModelObjects::queries; pub use ProtobufServer::start_grpc_server_with_tokio; pub use System::executable_query::QueryResult; +/// The default settings pub const DEFAULT_SETTINGS: ProtobufServer::services::query_request::Settings = ProtobufServer::services::query_request::Settings { reduce_clocks_level: Some(All(true)), }; +/// The default settings for Testing +pub const TEST_SETTINGS: ProtobufServer::services::query_request::Settings = + ProtobufServer::services::query_request::Settings { + reduce_clocks_level: Some(All(false)), + }; + #[macro_use] extern crate pest_derive; extern crate colored; diff --git a/src/tests/ClockReduction/clock_removal_test.rs b/src/tests/ClockReduction/clock_removal_test.rs index 3ed9b8d1..2da51f94 100644 --- a/src/tests/ClockReduction/clock_removal_test.rs +++ b/src/tests/ClockReduction/clock_removal_test.rs @@ -1,28 +1,62 @@ #[cfg(test)] pub mod clock_removal_tests { - use crate::tests::ClockReduction::helper::test::assert_edges_in_component; use crate::DataReader::json_reader::read_json_component; + use crate::TransitionSystems::{CompiledComponent, TransitionSystem}; use std::collections::HashSet; - // Tests that the clocks that are never used in any guards are removed. #[test] - fn test_removal_unused_clocks() { + fn test_check_declarations_unused_clocks_are_removed() { + check_declarations_unused_clocks_are_removed("Component1", "x"); + check_declarations_unused_clocks_are_removed("Component2", "i"); + check_declarations_unused_clocks_are_removed("Component3", "c"); + } + + fn check_declarations_unused_clocks_are_removed(component_name: &str, clock: &str) { let mut component = read_json_component( - "samples/json/ClockReductionTest/UnusedClockWithCycle", + "samples/json/ClockReductionTest/UnusedClock", + component_name, + ); + + let clock_index = component + .declarations + .get_clock_index_by_name(clock) + .unwrap(); + + component.remove_clock(*clock_index); + + let clock_reduced_compiled_component = + CompiledComponent::compile(component.clone(), component.declarations.clocks.len() + 1) + .unwrap(); + + let decls = clock_reduced_compiled_component.get_decls(); + + assert!(!decls[0].clocks.contains_key(clock)); + } + + #[test] + fn test_check_declarations_duplicated_clocks_are_removed() { + let mut component = read_json_component( + "samples/json/ClockReductionTest/RedundantClocks", "Component1", ); - let redundant_clocks = component.find_redundant_clocks(); - - component.reduce_clocks(redundant_clocks); - - assert_edges_in_component( - &component, - &HashSet::from([ - "L0-y->L1".to_string(), - "L1-y->L0".to_string(), - "L0-->L1".to_string(), - "L1-y->L3".to_string(), - ]), - ) + + let clock_1_index = component.declarations.get_clock_index_by_name("x").unwrap(); + let mut duplicate_clocks_index = HashSet::new(); + duplicate_clocks_index + .insert(*component.declarations.get_clock_index_by_name("y").unwrap()); + duplicate_clocks_index + .insert(*component.declarations.get_clock_index_by_name("z").unwrap()); + + component.replace_clock(*clock_1_index, &duplicate_clocks_index); + + let clock_reduced_compiled_component = + CompiledComponent::compile(component.clone(), component.declarations.clocks.len() + 1) + .unwrap(); + + let decls = clock_reduced_compiled_component.get_decls(); + + assert_eq!(*decls[0].clocks.get_key_value("x").unwrap().1, 1); + assert_eq!(*decls[0].clocks.get_key_value("y").unwrap().1, 1); + assert_eq!(*decls[0].clocks.get_key_value("z").unwrap().1, 1); } } diff --git a/src/tests/ClockReduction/helper.rs b/src/tests/ClockReduction/helper.rs index 7fe784f1..f086a046 100644 --- a/src/tests/ClockReduction/helper.rs +++ b/src/tests/ClockReduction/helper.rs @@ -1,204 +1,67 @@ #[cfg(test)] pub mod test { - use crate::component::{ClockReductionReason, Component, RedundantClock}; - use std::collections::{HashMap, HashSet}; - use std::iter::FromIterator; - - /// Asserts that component contains given locations and edges. - pub fn assert_locations_and_edges_in_component( - component: &Component, - expected_locations: &HashSet, - expected_edges: &HashSet, - ) { - assert_locations_in_component(component, expected_locations); - assert_edges_in_component(component, expected_edges); - } - - /// Asserts that component contains given locations. - fn assert_locations_in_component(component: &Component, expected_locations: &HashSet) { - let mut actual_locations: HashSet = HashSet::new(); - - for location in &component.locations { - let mut clocks_in_invariants = HashSet::new(); - if let Some(invariant) = &location.invariant { - invariant.get_varnames().iter().for_each(|clock| { - clocks_in_invariants.insert((*clock).to_string()); - }); - } - - let clock = sort_clocks_and_join(&clocks_in_invariants); - - actual_locations.insert(format!("{}-{}", location.id.clone(), clock)); - } - assert!( - expected_locations.is_subset(&actual_locations) - && expected_locations.len() == actual_locations.len(), - "Expected these locations {:?}, but got {:?}", - expected_locations, - actual_locations - ); - } - - /// Asserts that component contains given locations. - pub(crate) fn assert_edges_in_component( - component: &Component, - expected_edges: &HashSet, - ) { - let mut actual_edges: HashSet = HashSet::new(); + use crate::component; + use crate::component::{Edge, SyncType}; + use crate::DataReader::json_reader::read_json_component; + use crate::TransitionSystems::transition_system::ClockReductionInstruction; + use edbm::util::constraints::ClockIndex; + use std::collections::HashSet; + + /// Reads and processes a component. + pub fn read_json_component_and_process( + project_path: &str, + component_name: &str, + ) -> component::Component { + let mut component = read_json_component(project_path, component_name); + + let input_edges: &mut Vec = component.input_edges.insert(vec![]); + let output_edges: &mut Vec = component.output_edges.insert(vec![]); for edge in &component.edges { - let mut clocks_in_guards_and_updates = HashSet::new(); - if let Some(guard) = &edge.guard { - guard.get_varnames().iter().for_each(|clock| { - clocks_in_guards_and_updates.insert((*clock).to_string()); - }); - } - if let Some(updates) = &edge.update { - for update in updates { - clocks_in_guards_and_updates.insert(update.variable.to_string()); - } - } - - let sorted_clocks = sort_clocks_and_join(&clocks_in_guards_and_updates); - - let edge_id = format!( - "{}-{}->{}", - edge.source_location, sorted_clocks, edge.target_location - ); - - assert!( - !actual_edges.contains(&edge_id), - "Duplicate edge: {}", - edge_id - ); - - actual_edges.insert(edge_id); + match edge.sync_type { + SyncType::Input => input_edges.push(edge.clone()), + SyncType::Output => output_edges.push(edge.clone()), + }; } - assert!( - expected_edges.is_subset(&actual_edges) && expected_edges.len() == actual_edges.len(), - "Expected these edges {:?} but got {:?}", - expected_edges, - actual_edges - ) - } - - fn sort_clocks_and_join(dependent_clocks: &HashSet) -> String { - let mut dependent_clocks_vec = Vec::from_iter(dependent_clocks.iter()); - let mut sorted_clocks = String::new(); - dependent_clocks_vec.sort(); - for clock in dependent_clocks_vec { - sorted_clocks = sorted_clocks + clock; - } - sorted_clocks + component } - /// Assert that a redundant clock is redundant for the correct reason - pub fn assert_clock_reason( - redundant_clocks: &Vec, - expected_amount_to_reduce: u32, - expected_reducible_clocks: HashSet<&str>, - unused_allowed: bool, + /// Assert that a [`vec<&ClockReductionInstruction>`] contains an instruction that `clock` should + /// be removed. + pub(crate) fn assert_unused_clock_in_clock_reduction_instruction_vec( + redundant_clocks: Vec, + clock: ClockIndex, ) { - let mut global_clock: String = String::from(""); - - let mut clocksReduced: HashSet = HashSet::new(); - - for redundancy in redundant_clocks { - match &redundancy.reason { - ClockReductionReason::Duplicate(replaced_by) => { - if global_clock.is_empty() { - global_clock = replaced_by.clone(); - } - assert!( - expected_reducible_clocks.contains(redundancy.clock.as_str()), - "Clock ({}) was marked as duplicate unexpectedly", - redundancy.clock - ); - assert!( - !clocksReduced.contains(&redundancy.clock), - "Clock ({}) was marked as duplicate multiple times", - redundancy.clock - ); - assert_eq!( - &global_clock, replaced_by, - "Multiple clocks were chosen as global clock {} and {}", - global_clock, replaced_by - ); - clocksReduced.insert(redundancy.clock.clone()); - } - ClockReductionReason::Unused => { - assert!(unused_allowed, "Unexpected unused optimization"); - assert!( - expected_reducible_clocks.contains(&redundancy.clock.as_str()), - "Clock ({}) is not set as unused, but is not in expected", - redundancy.clock.as_str() - ); - assert!( - !clocksReduced.contains(&redundancy.clock), - "Clock {} has been removed multiple times", - redundancy.clock - ); - clocksReduced.insert(redundancy.clock.clone()); + assert!(redundant_clocks + .iter() + .any(|instruction| match instruction { + ClockReductionInstruction::RemoveClock { clock_index } => { + println!("Found {}, searching for {}", clock_index, clock); + *clock_index == clock } - } - } - assert_eq!( - clocksReduced.len(), - expected_amount_to_reduce as usize, - "Too many clocks were reduced, expected only {}, got {}", - expected_amount_to_reduce, - clocksReduced.len() - ); + _ => false, + })); } - - /// Asserts that the specific clocks occur in the correct locations and edges - pub fn assert_correct_edges_and_locations( - component: &Component, - expected_locations: HashMap>, - expected_edges: HashMap>, + /// Assert that a [`vec<&ClockReductionInstruction>`] contains an instruction that `clock` is a + /// duplicate of the clocks in `clocks`. + pub(crate) fn assert_duplicate_clock_in_clock_reduction_instruction_vec( + redundant_clocks: Vec, + clock: ClockIndex, + clocks: &HashSet, ) { - let redundant_clocks = component.find_redundant_clocks(); - - for redundancy in redundant_clocks { - let mut found_location_names: HashSet = HashSet::new(); - let clock_expected_locations = - expected_locations.get(redundancy.clock.as_str()).unwrap(); - for index in redundancy.location_indices { - assert!( - !found_location_names.contains(component.locations[index].id.as_str()), - "Duplicate location index found" - ); - found_location_names.insert(component.locations[index].id.clone()); - } - - assert!( - found_location_names.is_subset(clock_expected_locations) - && found_location_names.len() == clock_expected_locations.len(), - "Got unexpected locations for reduction of {}. Expected: {:?}, got: {:?}", - redundancy.clock, - clock_expected_locations, - found_location_names, - ); - - let mut found_edge_names: HashSet = HashSet::new(); - let clock_expected_edges = expected_edges.get(&redundancy.clock).unwrap(); - - for index in redundancy.edge_indices { - let edge = &component.edges[index]; - let edge_id = format!("{}->{}", edge.source_location, edge.target_location); - assert!(!found_edge_names.contains(&edge_id)); - found_edge_names.insert(edge_id); - } - - assert!( - found_edge_names.is_subset(clock_expected_edges) - && found_edge_names.len() == clock_expected_edges.len(), - "Got unexpected edges for reduction of {}. Expected: {:?}, got: {:?}", - redundancy.clock, - clock_expected_edges, - found_edge_names, - ); - } + assert!(redundant_clocks + .iter() + .any(|instruction| match instruction { + ClockReductionInstruction::RemoveClock { .. } => { + false + } + ClockReductionInstruction::ReplaceClocks { + clock_index, + clock_indices, + } => { + *clock_index == clock && clock_indices == clocks + } + })); } } diff --git a/src/tests/ClockReduction/mod.rs b/src/tests/ClockReduction/mod.rs index 7233eec5..8ae60ef5 100644 --- a/src/tests/ClockReduction/mod.rs +++ b/src/tests/ClockReduction/mod.rs @@ -1,5 +1,4 @@ mod clock_removal_test; mod helper; mod redundant_clock_detection_test; -pub mod replaced_clocks; pub mod unused_clock_detection_test; diff --git a/src/tests/ClockReduction/redundant_clock_detection_test.rs b/src/tests/ClockReduction/redundant_clock_detection_test.rs index 13f5e0cc..de68c74b 100644 --- a/src/tests/ClockReduction/redundant_clock_detection_test.rs +++ b/src/tests/ClockReduction/redundant_clock_detection_test.rs @@ -1,45 +1,41 @@ #[cfg(test)] pub mod test { use crate::tests::ClockReduction::helper::test::{ - assert_clock_reason, assert_correct_edges_and_locations, + assert_duplicate_clock_in_clock_reduction_instruction_vec, read_json_component_and_process, }; - use crate::DataReader::json_reader::read_json_component; - use std::collections::{HashMap, HashSet}; + use crate::TransitionSystems::transition_system::Heights; + use crate::TransitionSystems::{CompiledComponent, TransitionSystem}; + use edbm::util::constraints::ClockIndex; + use std::collections::HashSet; const REDUNDANT_CLOCKS_TEST_PROJECT: &str = "samples/json/ClockReductionTest/RedundantClocks"; + const DIM: ClockIndex = 5; // TODO: Dim #[test] fn test_three_synced_clocks() { - let component = read_json_component(REDUNDANT_CLOCKS_TEST_PROJECT, "Component1"); - - let redundant_clocks = component.find_redundant_clocks(); - - assert_clock_reason(&redundant_clocks, 2, HashSet::from(["x", "y", "z"]), false); - } - - #[test] - fn test_three_synced_clocks_correct_location_target() { - let component = read_json_component(REDUNDANT_CLOCKS_TEST_PROJECT, "Component1"); - - let mut expected_locations: HashMap> = HashMap::new(); - - expected_locations.insert("i".to_string(), HashSet::from(["L2".to_string()])); - expected_locations.insert("x".to_string(), HashSet::from(["L1".to_string()])); - expected_locations.insert("y".to_string(), HashSet::from(["L4".to_string()])); - expected_locations.insert("z".to_string(), HashSet::from([])); - - let mut expected_edges: HashMap> = HashMap::new(); - expected_edges.insert( - "i".to_string(), - HashSet::from(["L1->L0".to_string(), "L0->L2".to_string()]), + let expected_clocks = ["x".to_string(), "y".to_string(), "z".to_string()]; + let component = + read_json_component_and_process(REDUNDANT_CLOCKS_TEST_PROJECT, "Component1"); + let compiled_component = CompiledComponent::compile(component.clone(), DIM).unwrap(); + let clock_index_x = component + .declarations + .get_clock_index_by_name(&expected_clocks[0]) + .unwrap(); + let clock_index_y = component + .declarations + .get_clock_index_by_name(&expected_clocks[1]) + .unwrap(); + let clock_index_z = component + .declarations + .get_clock_index_by_name(&expected_clocks[2]) + .unwrap(); + + let instructions = compiled_component.find_redundant_clocks(Heights::empty()); + + assert_duplicate_clock_in_clock_reduction_instruction_vec( + instructions.clone(), + *clock_index_x, + &HashSet::from([*clock_index_y, *clock_index_z]), ); - expected_edges.insert( - "x".to_string(), - HashSet::from(["L2->L1".to_string(), "L0->L2".to_string()]), - ); - expected_edges.insert("y".to_string(), HashSet::from(["L0->L4".to_string()])); - expected_edges.insert("z".to_string(), HashSet::from(["L4->L2".to_string()])); - - assert_correct_edges_and_locations(&component, expected_locations, expected_edges); } } diff --git a/src/tests/ClockReduction/replaced_clocks.rs b/src/tests/ClockReduction/replaced_clocks.rs deleted file mode 100644 index be039739..00000000 --- a/src/tests/ClockReduction/replaced_clocks.rs +++ /dev/null @@ -1,59 +0,0 @@ -#[cfg(test)] -pub mod test { - use crate::tests::ClockReduction::helper::test::assert_locations_and_edges_in_component; - use crate::DataReader::json_reader::read_json_component; - use std::collections::HashSet; - use std::iter::FromIterator; - - /// If clocks are never reset, a global clock should be used. - /// Checks that clocks are replaced with a global clock in these cases and that other clocks - /// are not removed. - #[test] - pub fn test_replace_clocks() { - let mut component = read_json_component( - "samples/json/ClockReductionTest/RedundantClocks", - "Component1", - ); - let clocks = HashSet::from(["x", "y", "z"]); - - let redundant_clocks = component.find_redundant_clocks(); - assert_eq!( - redundant_clocks.len(), - 2, - "Expected only two redundant clocks, but got {}", - redundant_clocks.len() - ); - let duplicate_clocks = HashSet::from([ - redundant_clocks[0].clock.as_str(), - redundant_clocks[1].clock.as_str(), - ]); - - let global_clock = Vec::from_iter(clocks.symmetric_difference(&duplicate_clocks)); - assert_eq!( - global_clock.len(), - 1, - "reduced only one clock, expected two" - ); - - let expected_locations: HashSet = HashSet::from([ - "L2-i".to_string(), - format!("L1-{}", global_clock[0]), - format!("L4-{}", global_clock[0]), - "L3-".to_string(), - "L0-".to_string(), - ]); - - let expected_edges: HashSet = HashSet::from([ - "L1-i->L0".to_string(), - format!("L2-{}->L1", global_clock[0]), - format!("L0-i{}->L2", global_clock[0]), - format!("L0-{}->L4", global_clock[0]), - format!("L4-{}->L2", global_clock[0]), - "L2-->L3".to_string(), - ]); - - component.reduce_clocks(redundant_clocks); - - assert_locations_and_edges_in_component(&component, &expected_locations, &expected_edges); - } -} diff --git a/src/tests/ClockReduction/unused_clock_detection_test.rs b/src/tests/ClockReduction/unused_clock_detection_test.rs index adf48479..37e70fa7 100644 --- a/src/tests/ClockReduction/unused_clock_detection_test.rs +++ b/src/tests/ClockReduction/unused_clock_detection_test.rs @@ -1,31 +1,52 @@ #[cfg(test)] mod unused_clocks_tests { - use crate::component::Component; - use crate::tests::ClockReduction::helper::test::assert_clock_reason; + use crate::tests::ClockReduction::helper::test::assert_unused_clock_in_clock_reduction_instruction_vec; use crate::DataReader::json_reader::read_json_component; - use std::collections::HashSet; + use crate::TransitionSystems::transition_system::Heights; + use crate::TransitionSystems::{CompiledComponent, TransitionSystem}; + /// Loads the sample in `samples/json/ClockReductionTest/UnusedClockWithCycle` which contains + /// unused clocks. It then tests that these clocks are located correctly. fn unused_clocks_with_cycles(component_name: &str, unused_clock: &str) { let component = read_json_component( "samples/json/ClockReductionTest/UnusedClockWithCycle", component_name, ); - unused_clocks_are_found(&component, HashSet::from([unused_clock])); + let compiled_component = + CompiledComponent::compile(component.clone(), component.declarations.clocks.len() + 1) + .unwrap(); + + let clock_index = component + .declarations + .get_clock_index_by_name(unused_clock) + .unwrap(); + + let instructions = compiled_component.find_redundant_clocks(Heights::empty()); + + assert_unused_clock_in_clock_reduction_instruction_vec(instructions, *clock_index) } + /// Loads the sample in `samples/json/ClockReductionTest/UnusedClock` which contains + /// unused clocks. It then tests that these clocks are located correctly. fn unused_clock(component_name: &str, unused_clock: &str) { let component = read_json_component( "samples/json/ClockReductionTest/UnusedClock", component_name, ); - unused_clocks_are_found(&component, HashSet::from([unused_clock])); - } + let compiled_component = + CompiledComponent::compile(component.clone(), component.declarations.clocks.len() + 1) + .unwrap(); + + let clock_index = component + .declarations + .get_clock_index_by_name(unused_clock) + .unwrap(); + + let instructions = compiled_component.find_redundant_clocks(Heights::empty()); - fn unused_clocks_are_found(component: &Component, unused_clocks: HashSet<&str>) { - let redundant_clocks = component.find_redundant_clocks(); - assert_clock_reason(&redundant_clocks, 1, unused_clocks, true) + assert_unused_clock_in_clock_reduction_instruction_vec(instructions, *clock_index) } #[test] diff --git a/src/tests/grpc/send_query.rs b/src/tests/grpc/send_query.rs index ae2dc938..dd247c84 100644 --- a/src/tests/grpc/send_query.rs +++ b/src/tests/grpc/send_query.rs @@ -7,6 +7,7 @@ mod refinements { use crate::ProtobufServer::services::ComponentsInfo; use crate::ProtobufServer::services::QueryRequest; use crate::ProtobufServer::ConcreteEcdarBackend; + use crate::TEST_SETTINGS; use tonic::Request; //static CONJUN: &str = "samples/xml/conjun.xml"; @@ -75,7 +76,7 @@ mod refinements { components_hash: 0, }), ignored_input_outputs: None, - settings: None, + settings: Some(TEST_SETTINGS), }) } }