diff --git a/.gitmodules b/.gitmodules index 0f1d640e..fa9c441f 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,4 +1,4 @@ [submodule "Ecdar-ProtoBuf"] path = Ecdar-ProtoBuf url = https://github.com/Ecdar/Ecdar-ProtoBuf.git - branch = futureproof2 + branch = futureproof1 diff --git a/Ecdar-ProtoBuf b/Ecdar-ProtoBuf index ae8364e6..9b9ce8fd 160000 --- a/Ecdar-ProtoBuf +++ b/Ecdar-ProtoBuf @@ -1 +1 @@ -Subproject commit ae8364e6c8942a5cfde24adec779ca87d4431e4a +Subproject commit 9b9ce8fd52c14916d110667147e6421255b0c54d diff --git a/samples/xml/ConsTests.xml b/samples/xml/ConsTests.xml index 0c95941f..9fa66467 100644 --- a/samples/xml/ConsTests.xml +++ b/samples/xml/ConsTests.xml @@ -28,4 +28,4 @@ IO G21 { i?, o! } IO G22 { o! } IO G23 { o! } IO G24 { i?, o! } -IO G25 { i?, o! } \ No newline at end of file +IO G25 { i?, o! } diff --git a/src/DataReader/component_loader.rs b/src/DataReader/component_loader.rs index 544d185b..8d98fde8 100644 --- a/src/DataReader/component_loader.rs +++ b/src/DataReader/component_loader.rs @@ -125,7 +125,7 @@ pub struct ComponentContainer { impl ComponentLoader for ComponentContainer { fn get_component(&mut self, component_name: &str) -> &Component { if let Some(component) = self.loaded_components.get(component_name) { - assert_eq!(component_name, component.get_name()); + assert_eq!(component_name, component.name); component } else { panic!("The component '{}' could not be retrieved", component_name); @@ -161,10 +161,10 @@ impl ComponentContainer { pub fn from_components(components: Vec) -> ComponentContainer { let mut comp_hashmap = HashMap::::new(); for mut component in components { - log::trace!("Adding comp {} to container", component.get_name()); + log::trace!("Adding comp {} to container", component.name); let inputs: Vec<_> = component.get_input_actions(); input_enabler::make_input_enabled(&mut component, &inputs); - comp_hashmap.insert(component.get_name().to_string(), component); + comp_hashmap.insert(component.name.to_string(), component); } ComponentContainer::new(Arc::new(comp_hashmap)) } @@ -224,7 +224,7 @@ impl ComponentLoader for JsonProjectLoader { } if let Some(component) = self.loaded_components.get(component_name) { - assert_eq!(component_name, component.get_name()); + assert_eq!(component_name, component.name); component } else { panic!("The component '{}' could not be retrieved", component_name); @@ -234,7 +234,7 @@ impl ComponentLoader for JsonProjectLoader { fn save_component(&mut self, component: Component) { component_to_json_file(&self.project_path, &component); self.loaded_components - .insert(component.get_name().clone(), component); + .insert(component.name.clone(), component); } fn get_settings(&self) -> &Settings { @@ -279,7 +279,7 @@ impl JsonProjectLoader { let opt_inputs = self .get_declarations() - .get_component_inputs(component.get_name()); + .get_component_inputs(&component.name); if let Some(inputs) = opt_inputs { input_enabler::make_input_enabled(&mut component, inputs); } @@ -304,7 +304,7 @@ pub struct XmlProjectLoader { impl ComponentLoader for XmlProjectLoader { fn get_component(&mut self, component_name: &str) -> &Component { if let Some(component) = self.loaded_components.get(component_name) { - assert_eq!(component_name, component.get_name()); + assert_eq!(component_name, component.name); component } else { panic!("The component '{}' could not be retrieved", component_name); @@ -344,12 +344,12 @@ impl XmlProjectLoader { let mut map = HashMap::::new(); for mut component in comps { - let opt_inputs = system_declarations.get_component_inputs(component.get_name()); + let opt_inputs = system_declarations.get_component_inputs(&component.name); if let Some(opt_inputs) = opt_inputs { input_enabler::make_input_enabled(&mut component, opt_inputs); } - let name = String::from(component.get_name()); + let name = String::from(&component.name); map.insert(name, component); } diff --git a/src/DataReader/json_writer.rs b/src/DataReader/json_writer.rs index b5c4c83e..054274bb 100644 --- a/src/DataReader/json_writer.rs +++ b/src/DataReader/json_writer.rs @@ -6,7 +6,7 @@ pub fn component_to_json_file(project_path: &str, component: &Component) { "{0}{1}Components{1}{2}.json", project_path, std::path::MAIN_SEPARATOR, - component.get_name() + component.name ); let file = File::create(path).expect("Couldnt open file"); diff --git a/src/DataReader/proto_reader.rs b/src/DataReader/proto_reader.rs index 2f8956f6..879655ea 100644 --- a/src/DataReader/proto_reader.rs +++ b/src/DataReader/proto_reader.rs @@ -169,8 +169,7 @@ mod tests { "Zones are not equal" ); assert_eq!( - *state1.get_location(), - *state2.get_location(), + state1.decorated_locations, state2.decorated_locations, "Location trees are not equal" ); } diff --git a/src/EdgeEval/constraint_applyer.rs b/src/EdgeEval/constraint_applyer.rs index 4df295e9..007f6b86 100644 --- a/src/EdgeEval/constraint_applyer.rs +++ b/src/EdgeEval/constraint_applyer.rs @@ -155,9 +155,9 @@ fn replace_vars(expr: &ArithExpression, decls: &Declarations) -> Result Ok(ArithExpression::Clock(*x)), ArithExpression::VarName(name) => { - if let Some(x) = decls.get_clocks().get(name.as_str()).copied() { + if let Some(x) = decls.clocks.get(name.as_str()).copied() { Ok(ArithExpression::Clock(x)) - } else if let Some(x) = decls.get_ints().get(name.as_str()).copied() { + } else if let Some(x) = decls.ints.get(name.as_str()).copied() { Ok(ArithExpression::Int(x)) } else { Err(name.to_string()) @@ -171,7 +171,7 @@ fn get_const(expr: &ArithExpression, decls: &Declarations) -> i32 { match expr { ArithExpression::Int(x) => *x, ArithExpression::Clock(_) => 0, - ArithExpression::VarName(name) => decls.get_ints().get(name).copied().unwrap_or(0), + ArithExpression::VarName(name) => decls.ints.get(name).copied().unwrap_or(0), ArithExpression::Difference(l, r) => get_const(l, decls) - get_const(r, decls), ArithExpression::Addition(l, r) => get_const(l, decls) + get_const(r, decls), ArithExpression::Multiplication(l, r) => get_const(l, decls) * get_const(r, decls), diff --git a/src/ModelObjects/Expressions/arith_expression.rs b/src/ModelObjects/Expressions/arith_expression.rs index 3ffdd519..242849c7 100644 --- a/src/ModelObjects/Expressions/arith_expression.rs +++ b/src/ModelObjects/Expressions/arith_expression.rs @@ -392,20 +392,15 @@ impl ArithExpression { } /// Finds the clock names used in the expression - pub fn get_varnames(&self) -> Vec<&str> { + pub fn has_varname(&self, name: &String) -> bool { match self { ArithExpression::Difference(a1, a2) | ArithExpression::Addition(a1, a2) | ArithExpression::Multiplication(a1, a2) | ArithExpression::Division(a1, a2) - | ArithExpression::Modulo(a1, a2) => a1 - .get_varnames() - .iter() - .chain(a2.get_varnames().iter()) - .copied() - .collect(), - ArithExpression::Clock(_) | ArithExpression::Int(_) => vec![], - ArithExpression::VarName(name) => vec![name.as_str()], + | ArithExpression::Modulo(a1, a2) => a1.has_varname(name) || a2.has_varname(name), + ArithExpression::Clock(_) | ArithExpression::Int(_) => false, + ArithExpression::VarName(n) => name == n, } } diff --git a/src/ModelObjects/Expressions/bool_expression.rs b/src/ModelObjects/Expressions/bool_expression.rs index 9ad328ef..d02e9ea4 100644 --- a/src/ModelObjects/Expressions/bool_expression.rs +++ b/src/ModelObjects/Expressions/bool_expression.rs @@ -396,25 +396,17 @@ impl BoolExpression { } /// Finds the clock names used in the expression - pub fn get_varnames(&self) -> Vec<&str> { + pub fn has_varname(&self, name: &String) -> bool { match self { - BoolExpression::AndOp(p1, p2) | BoolExpression::OrOp(p1, p2) => p1 - .get_varnames() - .iter() - .chain(p2.get_varnames().iter()) - .copied() - .collect(), + BoolExpression::AndOp(p1, p2) | BoolExpression::OrOp(p1, p2) => { + p1.has_varname(name) || p2.has_varname(name) + } BoolExpression::LessEQ(a1, a2) | BoolExpression::GreatEQ(a1, a2) | BoolExpression::LessT(a1, a2) | BoolExpression::GreatT(a1, a2) - | BoolExpression::EQ(a1, a2) => a1 - .get_varnames() - .iter() - .chain(a2.get_varnames().iter()) - .copied() - .collect(), - BoolExpression::Bool(_) => vec![], + | BoolExpression::EQ(a1, a2) => a1.has_varname(name) || a2.has_varname(name), + BoolExpression::Bool(_) => false, } } @@ -462,6 +454,12 @@ impl BoolExpression { } } +impl Default for BoolExpression { + fn default() -> Self { + BoolExpression::Bool(true) + } +} + fn var_from_naming( naming: &HashMap, index: ClockIndex, diff --git a/src/ModelObjects/component.rs b/src/ModelObjects/component.rs index 35f7a80e..c5c3ea55 100644 --- a/src/ModelObjects/component.rs +++ b/src/ModelObjects/component.rs @@ -10,14 +10,18 @@ use crate::EdgeEval::updater::CompiledUpdate; use edbm::util::bounds::Bounds; use edbm::util::constraints::ClockIndex; +use crate::msg; use crate::ModelObjects::Expressions::BoolExpression; +use crate::ProtobufServer::services::query_response::information; use crate::TransitionSystems::{CompositionType, TransitionSystem}; use crate::TransitionSystems::{LocationTree, TransitionID}; use edbm::zones::OwnedFederation; -use log::info; +use itertools::Itertools; use serde::{Deserialize, Serialize}; use std::collections::{HashMap, HashSet}; use std::fmt; +use std::iter::FromIterator; + /// The basic struct used to represent components read from either Json or xml #[derive(Debug, Deserialize, Serialize, Clone, Eq, PartialEq)] #[serde(into = "DummyComponent")] @@ -50,17 +54,6 @@ impl Component { *indices += self.declarations.get_clock_count(); } - ///Start of basic methods for manipulating fields - pub fn get_name(&self) -> &String { - &self.name - } - pub fn get_locations(&self) -> &Vec { - &self.locations - } - pub fn get_mut_locations(&mut self) -> &mut Vec { - &mut self.locations - } - pub fn get_location_by_name(&self, name: &str) -> &Location { let loc_vec = self .locations @@ -74,65 +67,23 @@ impl Component { panic!("Unable to retrieve location based on id: {}", name) } } - pub fn get_edges(&self) -> &Vec { - &self.edges - } - pub fn get_mut_edges(&mut self) -> &mut Vec { - &mut self.edges - } - pub fn add_edge(&mut self, edge: Edge) { - self.edges.push(edge); - } - pub fn add_edges(&mut self, edges: &mut Vec) { - self.edges.append(edges); - } - pub fn get_mut_declaration(&mut self) -> &mut Declarations { - &mut self.declarations - } - - pub fn get_initial_location(&self) -> Option<&Location> { - let vec: Vec<&Location> = self - .get_locations() - .iter() - .filter(|location| location.get_location_type() == LocationType::Initial) - .collect(); - - vec.first().copied() - } - - pub fn get_actions(&self) -> Vec { - let mut actions = vec![]; - for edge in self.get_edges() { - actions.push(edge.get_sync().clone()); - } - - actions - } pub fn get_input_actions(&self) -> Vec { - let mut actions = vec![]; - for edge in &self.edges { - if *edge.get_sync_type() == SyncType::Input && !contain(&actions, edge.get_sync()) { - if edge.get_sync() == "*" { - continue; - }; - actions.push(edge.get_sync().clone()); - } - } - actions + self.get_specific_actions(SyncType::Input) } pub fn get_output_actions(&self) -> Vec { - let mut actions = vec![]; - for edge in &self.edges { - if *edge.get_sync_type() == SyncType::Output && !contain(&actions, edge.get_sync()) { - if edge.get_sync() == "*" { - continue; - }; - actions.push(edge.get_sync().clone()); - } - } - actions + self.get_specific_actions(SyncType::Output) + } + + fn get_specific_actions(&self, sync_type: SyncType) -> Vec { + Vec::from_iter( + self.edges + .iter() + .filter(|e| e.sync_type == sync_type && e.sync != "*") + .map(|e| e.sync.clone()) + .unique(), + ) } // End of basic methods @@ -142,7 +93,7 @@ impl Component { for (clock_name, clock_id) in &self.declarations.clocks { let mut max_bound = 0; for edge in &self.edges { - if let Some(guard) = edge.get_guard() { + if let Some(guard) = &edge.guard { let new_bound = guard.get_max_constant(*clock_id, clock_name); if max_bound < new_bound { max_bound = new_bound; @@ -151,7 +102,7 @@ impl Component { } for location in &self.locations { - if let Some(inv) = location.get_invariant() { + if let Some(inv) = &location.invariant { let new_bound = inv.get_max_constant(*clock_id, clock_name); if max_bound < new_bound { max_bound = new_bound; @@ -167,15 +118,10 @@ impl Component { max_bounds } - /// Find [`Edge`] in the component given the edges `id`. - pub fn find_edge_from_id(&self, id: &str) -> Option<&Edge> { - self.get_edges().iter().find(|e| e.id.contains(id)) - } - /// Redoes the components Edge IDs by giving them new unique IDs based on their index. pub fn remake_edge_ids(&mut self) { // Give all edges a name - for (index, edge) in self.get_mut_edges().iter_mut().enumerate() { + for (index, edge) in self.edges.iter_mut().enumerate() { edge.id = format!("E{}", index); } } @@ -192,26 +138,34 @@ impl Component { .to_owned(); self.declarations.clocks.remove(&name); - // Removes from from updates + // Removes from from updates and guards self.edges .iter_mut() - .filter(|e| e.update.is_some()) + .filter(|e| e.update.is_some() || e.guard.is_some()) .for_each(|e| { - if let Some((i, _)) = e - .update - .as_ref() - .unwrap() - .iter() - .enumerate() - .find(|(_, u)| u.variable == name) - { - e.update.as_mut().unwrap().remove(i); + // The guard is overwritten to `false`. This can be done since we assume + // that all edges with guards involving the given clock is not reachable + // in some composite system. + if let Some(guard) = e.guard.as_mut().filter(|g| g.has_varname(&name)) { + *guard = BoolExpression::Bool(false); + } + if let Some(inv) = e.update.as_mut() { + inv.retain(|u| u.variable != name); } }); - info!( - "Removed Clock '{name}' (index {index}) has been removed from component {}", - self.name - ); // Should be changed in the future to be the information logger + + // Removes from from location invariants + // The invariants containing the clock are overwritten to `false`. + // This can be done since we assume that all locations with invariants involving + // the given clock is not reachable in some composite system. + self.locations + .iter_mut() + .filter_map(|l| l.invariant.as_mut()) + .filter(|i| i.has_varname(&name)) + .for_each(|i| *i = BoolExpression::Bool(false)); + + msg!(information::Severity::Info, subject: "Clock Reduction", msg: "Removed Clock '{name}' (index {index}) has been removed from component {}", + self.name); } /// Replaces duplicate clock with a new @@ -232,18 +186,14 @@ impl Component { let old = *index; *index = global_index; // TODO: Maybe log the global clock name instead of index - info!( - "Replaced Clock '{name}' (index {old}) with {global_index} in component {}", + msg!(information::Severity::Info, subject: "Clock Reduction", + msg: "Replaced Clock '{name}' (index {old}) with {global_index} in component {}", self.name - ); // Should be changed in the future to be the information logger + ); } } } -fn contain(channels: &[String], channel: &str) -> bool { - channels.iter().any(|c| c == channel) -} - /// FullState is a struct used for initial verification of consistency, and determinism as a state that also hols a dbm /// This is done as the type used in refinement state pair assumes to sides of an operation /// this should probably be refactored as it causes unnecessary confusion @@ -314,10 +264,6 @@ impl State { self.zone_ref().subset_eq(other.zone_ref()) } - pub fn get_location(&self) -> &LocationTree { - &self.decorated_locations - } - pub fn extrapolate_max_bounds(&mut self, system: &dyn TransitionSystem) { let bounds = system.get_local_max_bounds(&self.decorated_locations); self.update_zone(|zone| zone.extrapolate_max_bounds(&bounds)) @@ -370,21 +316,6 @@ pub struct Location { pub urgency: String, } -impl Location { - pub fn get_id(&self) -> &String { - &self.id - } - pub fn get_invariant(&self) -> &Option { - &self.invariant - } - pub fn get_location_type(&self) -> LocationType { - self.location_type - } - pub fn get_urgency(&self) -> &String { - &self.urgency - } -} - #[derive(Debug, Deserialize, Serialize, Clone, Copy, PartialEq, Eq)] pub enum SyncType { Input, @@ -420,7 +351,7 @@ impl Transition { let target_locations = LocationTree::simple(target_loc, comp.get_declarations(), dim); let mut compiled_updates = vec![]; - if let Some(updates) = edge.get_update() { + if let Some(updates) = &edge.update { compiled_updates.extend( updates .iter() @@ -616,7 +547,6 @@ pub struct Edge { pub sync: String, } -const TRUE: BoolExpression = BoolExpression::Bool(true); impl fmt::Display for Edge { fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { f.write_fmt(format_args!( @@ -628,7 +558,7 @@ impl fmt::Display for Edge { SyncType::Output => "!", }, self.target_location, - self.guard.as_ref().unwrap_or(&TRUE), + self.guard.as_ref().unwrap_or(&BoolExpression::default()), self.update ))?; Ok(()) @@ -641,7 +571,7 @@ impl Edge { decl: &Declarations, //Will eventually be mutable mut fed: OwnedFederation, ) -> OwnedFederation { - if let Some(updates) = self.get_update() { + if let Some(updates) = &self.update { for update in updates { fed = update.compiled(decl).apply(fed); } @@ -651,47 +581,12 @@ impl Edge { } pub fn apply_guard(&self, decl: &Declarations, mut fed: OwnedFederation) -> OwnedFederation { - if let Some(guards) = self.get_guard() { + if let Some(guards) = &self.guard { fed = apply_constraints_to_state(guards, decl, fed).expect("Failed to apply guard"); }; fed } - - pub fn get_source_location(&self) -> &String { - &self.source_location - } - - pub fn get_target_location(&self) -> &String { - &self.target_location - } - - pub fn get_sync_type(&self) -> &SyncType { - &self.sync_type - } - - pub fn get_guard(&self) -> &Option { - &self.guard - } - - pub fn get_update(&self) -> &Option> { - &self.update - } - - pub fn get_sync(&self) -> &String { - &self.sync - } - - pub fn get_update_clocks(&self) -> Vec<&str> { - let mut clock_vec = vec![]; - if let Some(updates) = self.get_update() { - for u in updates { - clock_vec.push(u.get_variable_name()) - } - } - - clock_vec - } } pub trait DeclarationProvider { @@ -713,49 +608,18 @@ impl Declarations { } } - pub fn get_ints(&self) -> &HashMap { - &self.ints - } - - pub fn get_mut_ints(&mut self) -> &mut HashMap { - &mut self.ints - } - - pub fn get_clocks(&self) -> &HashMap { - &self.clocks - } - pub fn get_clock_count(&self) -> usize { self.clocks.len() } - pub fn get_max_clock_index(&self) -> ClockIndex { - *self.clocks.values().max().unwrap_or(&0) - } - pub fn set_clock_indices(&mut self, start_index: ClockIndex) { for (_, v) in self.clocks.iter_mut() { *v += start_index } } - pub fn update_clock_indices(&mut self, start_index: ClockIndex, old_offset: ClockIndex) { - for (_, v) in self.clocks.iter_mut() { - *v -= old_offset; - *v += start_index; - } - } - - pub fn reset_clock_indices(&mut self) { - let mut i = 1; - for (_, v) in self.clocks.iter_mut() { - *v = i; - i += 1; - } - } - pub fn get_clock_index_by_name(&self, name: &str) -> Option<&ClockIndex> { - self.get_clocks().get(name) + self.clocks.get(name) } /// Gets the name of a given `ClockIndex`. diff --git a/src/ModelObjects/system_declarations.rs b/src/ModelObjects/system_declarations.rs index d94bee51..a8d65532 100644 --- a/src/ModelObjects/system_declarations.rs +++ b/src/ModelObjects/system_declarations.rs @@ -25,10 +25,10 @@ impl SystemDeclarations { pub fn add_component(&mut self, comp: &Component) { self.declarations .input_actions - .insert(comp.get_name().clone(), comp.get_input_actions()); + .insert(comp.name.clone(), comp.get_input_actions()); self.declarations .output_actions - .insert(comp.get_name().clone(), comp.get_output_actions()); + .insert(comp.name.clone(), comp.get_output_actions()); } } diff --git a/src/ProtobufServer/ecdar_requests/request_util.rs b/src/ProtobufServer/ecdar_requests/request_util.rs index 530f9b95..eef614a7 100644 --- a/src/ProtobufServer/ecdar_requests/request_util.rs +++ b/src/ProtobufServer/ecdar_requests/request_util.rs @@ -35,11 +35,11 @@ pub fn get_or_insert_model( fn create_components(components: Vec) -> HashMap { let mut comp_hashmap = HashMap::::new(); for mut component in components { - trace!("Adding comp {} to container", component.get_name()); + trace!("Adding comp {} to container", component.name); let inputs: Vec<_> = component.get_input_actions(); input_enabler::make_input_enabled(&mut component, &inputs); - comp_hashmap.insert(component.get_name().to_string(), component); + comp_hashmap.insert(component.name.to_string(), component); } comp_hashmap } diff --git a/src/ProtobufServer/ecdar_requests/send_query.rs b/src/ProtobufServer/ecdar_requests/send_query.rs index 1f739d4f..1eef28cc 100644 --- a/src/ProtobufServer/ecdar_requests/send_query.rs +++ b/src/ProtobufServer/ecdar_requests/send_query.rs @@ -53,7 +53,7 @@ impl ConcreteEcdarBackend { let result = query.execute(); Ok(QueryResponse { query_id: query_request.query_id, - info: vec![], // TODO: Should be logs + info: crate::logging::get_messages(), result: Some(result.into()), }) } diff --git a/src/System/extract_system_rep.rs b/src/System/extract_system_rep.rs index 1a7c6d03..6cabe8c0 100644 --- a/src/System/extract_system_rep.rs +++ b/src/System/extract_system_rep.rs @@ -81,7 +81,7 @@ pub fn create_executable_query<'a>( let start_state: State = if let Some(state) = from.as_ref() { let state = get_state(state, &machine, &transition_system) .map_err(|err| format!("Invalid Start state: {}", err))?; - if state.get_location().id.is_partial_location() { + if state.decorated_locations.id.is_partial_location() { return Err("Start state is a partial state, which it must not be".into()); } state diff --git a/src/System/input_enabler.rs b/src/System/input_enabler.rs index 89420025..d5205c86 100644 --- a/src/System/input_enabler.rs +++ b/src/System/input_enabler.rs @@ -9,13 +9,13 @@ pub fn make_input_enabled(component: &mut component::Component, inputs: &[String let dimension = component.declarations.get_clock_count() + 1; let mut new_edges: Vec = vec![]; let input_edges = component - .get_edges() + .edges .iter() - .filter(|edge| *edge.get_sync_type() == component::SyncType::Input); - for location in component.get_locations() { + .filter(|edge| edge.sync_type == component::SyncType::Input); + for location in &component.locations { let mut location_inv_zone = OwnedFederation::universe(dimension); - if let Some(invariant) = location.get_invariant() { + if let Some(invariant) = &location.invariant { location_inv_zone = constraint_applyer::apply_constraints_to_state( invariant, component.get_declarations(), @@ -28,19 +28,19 @@ pub fn make_input_enabled(component: &mut component::Component, inputs: &[String let full_federation = location_inv_zone.clone(); let location_edges = input_edges .clone() - .filter(|edge| edge.get_source_location() == location.get_id()); + .filter(|edge| edge.source_location == location.id); for input in inputs { let specific_edges = location_edges .clone() - .filter(|edge| *edge.get_sync() == *input || *edge.get_sync() == "*"); + .filter(|edge| edge.sync == *input || edge.sync == "*"); let mut zones_federation = OwnedFederation::empty(dimension); for edge in specific_edges { let mut guard_zone = OwnedFederation::universe(dimension); - if let Some(target_invariant) = component - .get_location_by_name(edge.get_target_location()) - .get_invariant() + if let Some(target_invariant) = &component + .get_location_by_name(edge.target_location.as_str()) + .invariant { guard_zone = constraint_applyer::apply_constraints_to_state( target_invariant, @@ -50,7 +50,7 @@ pub fn make_input_enabled(component: &mut component::Component, inputs: &[String .unwrap(); } - if let Some(updates) = edge.get_update() { + if let Some(updates) = &edge.update { for update in updates { let cu = update.compiled(component.get_declarations()); guard_zone = cu.apply_as_guard(guard_zone); @@ -58,7 +58,7 @@ pub fn make_input_enabled(component: &mut component::Component, inputs: &[String } } - if let Some(guard) = edge.get_guard() { + if let Some(guard) = &edge.guard { guard_zone = constraint_applyer::apply_constraints_to_state( guard, component.get_declarations(), @@ -77,13 +77,13 @@ pub fn make_input_enabled(component: &mut component::Component, inputs: &[String } new_edges.push(component::Edge { - id: format!("input_{}_{}", location.get_id(), input), - source_location: location.get_id().to_string(), - target_location: location.get_id().to_string(), + id: format!("input_{}_{}", location.id, input), + source_location: location.id.to_string(), + target_location: location.id.to_string(), sync_type: component::SyncType::Input, guard: BoolExpression::from_disjunction( &result_federation.minimal_constraints(), - component.get_declarations().get_clocks(), + &component.get_declarations().clocks, ), update: None, sync: input.to_string(), @@ -91,5 +91,5 @@ pub fn make_input_enabled(component: &mut component::Component, inputs: &[String } } - component.add_edges(&mut new_edges); + component.edges.append(&mut new_edges); } diff --git a/src/System/local_consistency.rs b/src/System/local_consistency.rs index bbbfba8f..62410d14 100644 --- a/src/System/local_consistency.rs +++ b/src/System/local_consistency.rs @@ -52,8 +52,7 @@ fn is_deterministic_helper( if allowed_fed.has_intersection(&location_fed) { warn!( "Not deterministic from location {} failing action {}", - state.get_location().id, - action + state.decorated_locations.id, action ); return DeterminismFailure::from(system, action, &state); } @@ -121,7 +120,7 @@ pub fn consistency_least_helper( } } } - warn!("No saving outputs from {}", state.get_location().id); + warn!("No saving outputs from {}", state.decorated_locations.id); ConsistencyFailure::inconsistent_from(system, &state) } diff --git a/src/System/pruning.rs b/src/System/pruning.rs index 75131c58..46a5ea52 100644 --- a/src/System/pruning.rs +++ b/src/System/pruning.rs @@ -24,7 +24,7 @@ pub fn prune_system(ts: TransitionSystemPtr, dim: ClockIndex) -> TransitionSyste let comp = combine_components(&ts, PruningStrategy::NoPruning); let mut input_map: HashMap> = HashMap::new(); - input_map.insert(comp.get_name().clone(), inputs.iter().cloned().collect()); + input_map.insert(comp.name.clone(), inputs.iter().cloned().collect()); let result = prune(&comp, dim, inputs, outputs); @@ -121,7 +121,7 @@ pub fn prune( .iter() .filter(|e| e.target_location == target_loc) { - if *edge.get_sync_type() == SyncType::Input { + if edge.sync_type == SyncType::Input { handle_input(edge, &mut context); } handle_output(edge, &mut context); @@ -142,8 +142,8 @@ pub fn prune( debug!( "Pruned component from {} edges to {} edges", - comp.get_edges().len(), - new_comp.get_edges().len() + comp.edges.len(), + new_comp.edges.len() ); CompiledComponent::compile_with_actions(new_comp, inputs, outputs, dim, 0) @@ -160,7 +160,7 @@ fn add_inconsistent_parts_to_invariants( if let Some(incons) = incons_parts.get(&location.id) { // get invariant let mut invariant_fed = OwnedFederation::universe(dim); - if let Some(inv) = location.get_invariant() { + if let Some(inv) = &location.invariant { invariant_fed = apply_constraints_to_state(inv, &decls, invariant_fed).unwrap(); } // Remove inconsistent part @@ -175,16 +175,16 @@ fn add_inconsistent_parts_to_invariants( } fn handle_input(edge: &Edge, context: &mut PruneContext) { - let target_loc = context.get_loc(edge.get_target_location()).clone(); - let mut inconsistent_part = context.get_incons(target_loc.get_id()).clone(); + let target_loc = context.get_loc(&edge.target_location).clone(); + let mut inconsistent_part = context.get_incons(&target_loc.id).clone(); // apply target invariant - if let Some(inv) = target_loc.get_invariant() { + if let Some(inv) = &target_loc.invariant { inconsistent_part = apply_constraints_to_state(inv, context.decl(), inconsistent_part).unwrap(); } // apply updates as guard - if let Some(updates) = edge.get_update() { + if let Some(updates) = &edge.update { for update in updates { inconsistent_part = update .compiled(context.decl()) @@ -212,14 +212,14 @@ fn handle_input(edge: &Edge, context: &mut PruneContext) { inconsistent_part = inconsistent_part.down(); // apply source invariant - let source_loc = context.get_loc(edge.get_source_location()); - if let Some(inv) = source_loc.get_invariant() { + let source_loc = context.get_loc(&edge.source_location); + if let Some(inv) = &source_loc.invariant { inconsistent_part = apply_constraints_to_state(inv, context.decl(), inconsistent_part).unwrap(); } } - process_source_location(edge.get_source_location(), inconsistent_part, context); + process_source_location(&edge.source_location, inconsistent_part, context); } remove_transition_if_unsat(edge, context); @@ -228,17 +228,17 @@ fn handle_input(edge: &Edge, context: &mut PruneContext) { fn remove_transition_if_unsat(edge: &Edge, context: &mut PruneContext) { let mut edge_fed = OwnedFederation::universe(context.dim); // apply target invariant - let target_loc = context.get_loc(edge.get_target_location()); - if let Some(inv) = target_loc.get_invariant() { + let target_loc = context.get_loc(&edge.target_location); + if let Some(inv) = &target_loc.invariant { edge_fed = apply_constraints_to_state(inv, context.decl(), edge_fed).unwrap(); } // Subtract target inconsistent part - if let Some(incons) = context.try_get_incons(edge.get_target_location()) { + if let Some(incons) = context.try_get_incons(&edge.target_location) { edge_fed = edge_fed.subtraction(incons); } - if let Some(updates) = edge.get_update() { + if let Some(updates) = &edge.update { // apply updates as guard for update in updates { edge_fed = update.compiled(context.decl()).apply_as_guard(edge_fed); @@ -253,18 +253,18 @@ fn remove_transition_if_unsat(edge: &Edge, context: &mut PruneContext) { } // Apply guards - if let Some(guard) = edge.get_guard() { + if let Some(guard) = &edge.guard { edge_fed = apply_constraints_to_state(guard, context.decl(), edge_fed).unwrap(); } // Apply source invariant - let source_loc = context.get_loc(edge.get_source_location()); - if let Some(inv) = source_loc.get_invariant() { + let source_loc = context.get_loc(&edge.source_location); + if let Some(inv) = &source_loc.invariant { edge_fed = apply_constraints_to_state(inv, context.decl(), edge_fed).unwrap(); } // Subtract source inconsistent part - if let Some(incons) = context.try_get_incons(edge.get_source_location()) { + if let Some(incons) = context.try_get_incons(&edge.source_location) { edge_fed = edge_fed.subtraction(incons); } @@ -309,15 +309,15 @@ fn predt_of_all_outputs( let mut incons_fed = inconsistent_part; for other_edge in context .comp - .get_edges() + .edges .iter() .filter(|e| e.source_location == source_loc.id && e.sync_type == SyncType::Output) { - let target_loc = context.get_loc(other_edge.get_target_location()); + let target_loc = context.get_loc(&other_edge.target_location); let mut saving_fed = OwnedFederation::universe(context.dim); // apply target invariant - if let Some(inv) = target_loc.get_invariant() { + if let Some(inv) = &target_loc.invariant { saving_fed = apply_constraints_to_state(inv, context.decl(), saving_fed).unwrap(); } @@ -327,13 +327,12 @@ fn predt_of_all_outputs( .iter() .any(|id| *id == target_loc.id) { - saving_fed = - saving_fed.subtraction(context.get_incons(other_edge.get_target_location())) + saving_fed = saving_fed.subtraction(context.get_incons(&other_edge.target_location)) } // apply updates via free if !saving_fed.is_empty() { - if let Some(updates) = other_edge.get_update() { + if let Some(updates) = &other_edge.update { for update in updates { saving_fed = update.compiled(context.decl()).apply_as_free(saving_fed); } @@ -341,12 +340,12 @@ fn predt_of_all_outputs( } // apply edge guard - if let Some(guard) = other_edge.get_guard() { + if let Some(guard) = &other_edge.guard { saving_fed = apply_constraints_to_state(guard, context.decl(), saving_fed).unwrap(); } // apply source invariant - if let Some(inv) = source_loc.get_invariant() { + if let Some(inv) = &source_loc.invariant { saving_fed = apply_constraints_to_state(inv, context.decl(), saving_fed).unwrap(); } @@ -365,7 +364,7 @@ fn back_exploration_on_transition( context: &mut PruneContext, ) -> OwnedFederation { // apply updates via free - if let Some(updates) = edge.get_update() { + if let Some(updates) = &edge.update { for update in updates { inconsistent_part = update .compiled(context.decl()) @@ -374,14 +373,14 @@ fn back_exploration_on_transition( } // apply edge guard - if let Some(guard) = edge.get_guard() { + if let Some(guard) = &edge.guard { inconsistent_part = apply_constraints_to_state(guard, context.decl(), inconsistent_part).unwrap(); } // apply source invariant - let source = context.get_loc(edge.get_source_location()); - if let Some(inv) = source.get_invariant() { + let source = context.get_loc(&edge.source_location); + if let Some(inv) = &source.invariant { inconsistent_part = apply_constraints_to_state(inv, context.decl(), inconsistent_part).unwrap(); } @@ -390,14 +389,14 @@ fn back_exploration_on_transition( } fn handle_output(edge: &Edge, context: &mut PruneContext) { - let target_incons = context.get_incons(edge.get_target_location()); + let target_incons = context.get_incons(&edge.target_location); if target_incons.is_universe() { // Fully inconsistent target context.remove_edge(edge); } else { // Partially inconsistent target let mut incons_after_reset = target_incons.clone(); - if let Some(updates) = edge.get_update() { + if let Some(updates) = &edge.update { // TODO: this is different from J-ecdar // apply updates as guard for update in updates { @@ -417,7 +416,7 @@ fn handle_output(edge: &Edge, context: &mut PruneContext) { } let mut guard_fed = OwnedFederation::universe(context.dim); // Apply guards - if let Some(guard) = edge.get_guard() { + if let Some(guard) = &edge.guard { guard_fed = apply_constraints_to_state(guard, context.decl(), guard_fed).unwrap(); } guard_fed = guard_fed.subtraction(&incons_after_reset); @@ -431,8 +430,8 @@ fn handle_output(edge: &Edge, context: &mut PruneContext) { // get source invariant let mut source_invariant = OwnedFederation::universe(context.dim); - let source_loc = context.get_loc(edge.get_source_location()); - if let Some(inv) = source_loc.get_invariant() { + let source_loc = context.get_loc(&edge.source_location); + if let Some(inv) = &source_loc.invariant { source_invariant = apply_constraints_to_state(inv, context.decl(), source_invariant).unwrap(); } @@ -442,23 +441,23 @@ fn handle_output(edge: &Edge, context: &mut PruneContext) { } else { let mut fed_that_saves_us = OwnedFederation::empty(context.dim); for other_edge in context.comp.edges.iter().filter(|e| { - e.source_location == edge.source_location && *e.get_sync_type() == SyncType::Output + e.source_location == edge.source_location && e.sync_type == SyncType::Output }) { // calculate and backtrack the part that is NOT inconsistent // get target invariant let mut good_part = OwnedFederation::universe(context.dim); - let target_loc = context.get_loc(other_edge.get_target_location()); - if let Some(inv) = target_loc.get_invariant() { + let target_loc = context.get_loc(&other_edge.target_location); + if let Some(inv) = &target_loc.invariant { good_part = apply_constraints_to_state(inv, context.decl(), good_part).unwrap(); } // If target is inconsistent we must avoid that part - if let Some(incons) = context.try_get_incons(other_edge.get_target_location()) { + if let Some(incons) = context.try_get_incons(&other_edge.target_location) { good_part = good_part.subtraction(incons); } - if let Some(updates) = other_edge.get_update() { + if let Some(updates) = &other_edge.update { // TODO: this is different from J-ecdar // apply updates as guard for update in updates { @@ -474,7 +473,7 @@ fn handle_output(edge: &Edge, context: &mut PruneContext) { } // Apply guards - if let Some(guard) = other_edge.get_guard() { + if let Some(guard) = &other_edge.guard { good_part = apply_constraints_to_state(guard, context.decl(), good_part).unwrap(); } // We are allowed to delay into outputs @@ -484,7 +483,7 @@ fn handle_output(edge: &Edge, context: &mut PruneContext) { } let new_incon_part = source_invariant.subtraction(&fed_that_saves_us); - process_source_location(edge.get_source_location(), new_incon_part, context) + process_source_location(&edge.source_location, new_incon_part, context) } } diff --git a/src/System/reachability.rs b/src/System/reachability.rs index b25c158e..eac0bc56 100644 --- a/src/System/reachability.rs +++ b/src/System/reachability.rs @@ -31,7 +31,7 @@ fn is_trivially_unreachable(start_state: &State, end_state: &State) -> bool { } // If the end location has invariants and these do not have an intersection (overlap) with the zone of the end state of the query - if let Some(invariants) = end_state.get_location().get_invariants() { + if let Some(invariants) = end_state.decorated_locations.get_invariants() { if !end_state.zone_ref().has_intersection(invariants) { return true; } @@ -115,7 +115,7 @@ fn reachability_search( // Push start state to visited state visited_states.insert( - start_state.get_location().id.clone(), + start_state.decorated_locations.id.clone(), vec![start_state.zone_ref().clone()], ); @@ -156,8 +156,8 @@ fn reachability_search( fn reached_end_state(cur_state: &State, end_state: &State) -> bool { cur_state - .get_location() - .compare_partial_locations(end_state.get_location()) + .decorated_locations + .compare_partial_locations(&end_state.decorated_locations) && cur_state.zone_ref().has_intersection(end_state.zone_ref()) } @@ -175,7 +175,7 @@ fn take_transition( // Extrapolation ensures the bounds cant grow indefinitely, avoiding infinite loops // We must take the added bounds from the target state into account to ensure correctness new_state.extrapolate_max_bounds_with_extra_bounds(system.as_ref(), target_bounds); - let new_location_id = &new_state.get_location().id; + let new_location_id = &new_state.decorated_locations.id; let existing_zones = visited_states.entry(new_location_id.clone()).or_default(); // If this location has not already been reached (explored) with a larger zone if !zone_subset_of_existing_zones(new_state.zone_ref(), existing_zones) { diff --git a/src/TransitionSystems/compiled_component.rs b/src/TransitionSystems/compiled_component.rs index 193e5a2c..e26aab44 100644 --- a/src/TransitionSystems/compiled_component.rs +++ b/src/TransitionSystems/compiled_component.rs @@ -51,7 +51,7 @@ impl CompiledComponent { } let locations: HashMap = component - .get_locations() + .locations .iter() .map(|loc| { let loc = LocationTree::simple(loc, component.get_declarations(), dim); @@ -62,7 +62,13 @@ impl CompiledComponent { let mut location_edges: HashMap> = locations.keys().map(|k| (k.clone(), vec![])).collect(); - for edge in component.get_edges() { + log::debug!( + "decl for {:?}: {:?}", + component.name, + component.declarations + ); + log::debug!("Edges: {:?}", component.edges); + for edge in &component.edges { let id = LocationID::Simple(edge.source_location.clone()); let transition = Transition::from(&component, edge, dim); location_edges diff --git a/src/TransitionSystems/location_tree.rs b/src/TransitionSystems/location_tree.rs index bfdfb678..89bae7e5 100644 --- a/src/TransitionSystems/location_tree.rs +++ b/src/TransitionSystems/location_tree.rs @@ -55,7 +55,7 @@ impl LocationTree { } pub fn simple(location: &Location, decls: &Declarations, dim: ClockIndex) -> Self { - let invariant = if let Some(inv) = location.get_invariant() { + let invariant = if let Some(inv) = &location.invariant { let mut fed = OwnedFederation::universe(dim); fed = apply_constraints_to_state(inv, decls, fed).unwrap(); Some(fed) @@ -63,9 +63,9 @@ impl LocationTree { None }; LocationTree { - id: LocationID::Simple(location.get_id().clone()), + id: LocationID::Simple(location.id.clone()), invariant, - loc_type: location.get_location_type(), + loc_type: location.location_type, left: None, right: None, } diff --git a/src/TransitionSystems/transition_system.rs b/src/TransitionSystems/transition_system.rs index de0b8bd2..6a104102 100644 --- a/src/TransitionSystems/transition_system.rs +++ b/src/TransitionSystems/transition_system.rs @@ -14,6 +14,7 @@ use crate::{ use dyn_clone::{clone_trait_object, DynClone}; use edbm::util::{bounds::Bounds, constraints::ClockIndex}; use std::collections::hash_map::Entry; +use std::collections::vec_deque::VecDeque; use std::collections::{hash_set::HashSet, HashMap}; use std::hash::Hash; @@ -106,6 +107,9 @@ pub trait TransitionSystem: DynClone { fn get_initial_location(&self) -> Option; + /// Function to get all locations from a [`TransitionSystem`] + /// #### Warning + /// This function utilizes a lot of memory. Use with caution fn get_all_locations(&self) -> Vec; fn get_location(&self, id: &LocationID) -> Option { @@ -165,15 +169,11 @@ pub trait TransitionSystem: DynClone { .collect() } - ///Constructs a [CLockAnalysisGraph], + ///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 actions = self.get_actions(); - for location in self.get_all_locations() { - self.find_edges_and_nodes(&location, &actions, &mut graph); - } + let mut graph: ClockAnalysisGraph = ClockAnalysisGraph::from_dim(self.get_dim()); + self.find_edges_and_nodes(self.get_initial_location().unwrap(), &mut graph); graph } @@ -181,52 +181,57 @@ pub trait TransitionSystem: DynClone { ///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: &LocationTree, - 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.get_unique_string(), - }; - - //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.get_unique_string(), - to: transition.target_locations.id.get_unique_string(), - 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 { + fn find_edges_and_nodes(&self, init_location: LocationTree, graph: &mut ClockAnalysisGraph) { + let mut worklist = VecDeque::from([init_location]); + let actions = self.get_actions(); + while let Some(location) = worklist.pop_front() { + //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.get_unique_string(), + }; + + //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() { - edge.guard_dependencies.insert(constraint.i); - edge.guard_dependencies.insert(constraint.j); + 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 { + for transition in self.next_transitions_if_available(&location, action) { + let mut edge = ClockAnalysisEdge { + from: location.id.get_unique_string(), + to: transition.target_locations.id.get_unique_string(), + 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); + graph.edges.push(edge); + + if !graph + .nodes + .contains_key(&transition.target_locations.id.get_unique_string()) + { + worklist.push_back(transition.target_locations); + } + } } } } @@ -309,15 +314,15 @@ pub struct ClockAnalysisGraph { } impl ClockAnalysisGraph { - pub fn empty() -> ClockAnalysisGraph { + pub fn from_dim(dim: usize) -> ClockAnalysisGraph { ClockAnalysisGraph { nodes: HashMap::new(), edges: vec![], - dim: 0, + dim, } } - pub fn find_clock_redundancies(&self) -> Vec { + pub fn find_clock_redundancies(self) -> Vec { //First we find the used clocks let used_clocks = self.find_used_clocks(); diff --git a/src/lib.rs b/src/lib.rs index 29c09e25..82ecf592 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -23,9 +23,27 @@ pub use ProtobufServer::start_grpc_server_with_tokio; /// The default settings pub const DEFAULT_SETTINGS: Settings = Settings { - disable_clock_reduction: false, + disable_clock_reduction: true, }; +static mut IS_SERVER: Option = None; + +pub fn set_server(is_server: bool) { + unsafe { + IS_SERVER = Some(is_server); + } +} + +#[cfg(not(test))] +fn is_server() -> bool { + unsafe { IS_SERVER.expect("Server or CLI never specified") } +} + +#[cfg(test)] +fn is_server() -> bool { + true +} + #[macro_use] extern crate pest_derive; extern crate colored; diff --git a/src/logging.rs b/src/logging.rs index c3eb6739..85ba7657 100644 --- a/src/logging.rs +++ b/src/logging.rs @@ -1,8 +1,8 @@ -use crate::ProtobufServer::services::query_response::Information; use chrono::Local; use colored::{ColoredString, Colorize}; use log::SetLoggerError; use std::io::Write; +use std::thread; #[cfg(feature = "logging")] /// Sets up the logging @@ -16,7 +16,6 @@ pub fn setup_logger() -> Result<(), SetLoggerError> { log::Level::Trace => level.to_string().magenta(), } } - env_logger::Builder::from_env(env_logger::Env::default()) .format(|buf, record| { writeln!( @@ -32,8 +31,147 @@ pub fn setup_logger() -> Result<(), SetLoggerError> { .try_init() } -// TODO: Implement a logging for informations to both the CLI and gRPC -/// Gets messages saved for other clients (through gRPC) -pub fn get_messages() -> Vec { - unimplemented!() +#[macro_export] +macro_rules! msg { + ($severity:expr, subject: $subject:expr, msg: $msg:expr) => ({ + if $crate::is_server() { + $crate::logging::message::__set_info__($crate::logging::message::__as_information__($severity.into(), $subject, $msg.to_string())); + } else { + //let lvl = $crate::logging::__severity__($severity); + //log::log!(lvl, "{}", $crate::logging::__as_information__($severity, $subject, $msg)); + println!("{}", $crate::logging::message::__as_information__($severity.into(), $subject, $msg.to_string())); + } + }); + + + ($severity:expr, subject: $subject:expr, msg: $($msg:tt)+) => (msg!($severity, subject: $subject, msg: format_args!($($msg)+).to_string())); + + ($subject:expr, msg: $msg:expr) => (msg!(0, subject: $subject, msg: $msg.to_string())); + ($subject:expr, msg: $($msg:tt)+) => (msg!(0, subject: $subject, msg: format_args!($($msg)+).to_string())); + + ($msg:expr) => (msg!(0, subject: "General", msg: $msg.to_string())); + ($($msg:tt)+) => (msg!(0, subject: "General", msg: format_args!($($msg)+).to_string())); +} + +/// Function to get information messages. +/// ### Info +/// Will always return `None` when Reveaal is run through the CLI, only use as server. +pub fn get_messages() -> Vec { + message::__MESSAGES__ + .lock() + .unwrap() + .remove(&thread::current().id()) + .unwrap_or_default() +} + +#[doc(hidden)] +pub mod message { + use crate::ProtobufServer::services::query_response::{information, Information}; + use chrono::Local; + use colored::Colorize; + use std::collections::hash_map::Entry; + use std::collections::HashMap; + use std::fmt::{Display, Formatter}; + use std::sync::Mutex; + use std::thread; + use std::thread::ThreadId; + + impl Display for Information { + fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { + let lvl = match information::Severity::from_i32(self.severity) { + Some(s @ information::Severity::Warning) => s.as_str_name().yellow(), + Some(s @ information::Severity::Info) => s.as_str_name().cyan(), + None => panic!("Couldn't parse severity"), + }; + write!( + f, + "[{} {}: {}] - {}", + Local::now().format("%H:%M:%S").to_string().cyan(), + lvl, + self.subject, + self.message + ) + } + } + + lazy_static! { + pub static ref __MESSAGES__: Mutex>> = Mutex::default(); + } + #[doc(hidden)] + pub fn __as_information__(severity: i32, subject: &str, message: String) -> Information { + Information { + severity, + subject: subject.to_string(), + message, + } + } + + #[doc(hidden)] + pub fn __set_info__(info: Information) { + match __MESSAGES__.lock().unwrap().entry(thread::current().id()) { + Entry::Occupied(mut o) => o.get_mut().push(info), + Entry::Vacant(v) => { + v.insert(vec![info]); + } + }; + } + + #[cfg(test)] + mod tests { + use crate::logging::get_messages; + use crate::logging::message::__as_information__; + use std::thread; + use std::time::Duration; + + #[test] + fn msg_macro_formats_test() { + msg!("{}", "test"); + msg!("test"); + + msg!("Testing", msg: "{}", "test"); + msg!("Testing", msg: "test"); + + msg!(1, subject: "Testing", msg: "{}", "test"); + msg!(1, subject: "Testing", msg: "test"); + let msgs = get_messages(); + assert_eq!(msgs.len(), 6); + assert_eq!( + msgs, + vec![ + __as_information__(0, "General", "test".to_string()), + __as_information__(0, "General", "test".to_string()), + __as_information__(0, "Testing", "test".to_string()), + __as_information__(0, "Testing", "test".to_string()), + __as_information__(1, "Testing", "test".to_string()), + __as_information__(1, "Testing", "test".to_string()) + ] + ); + } + + #[test] + fn multithreading_msg_test() { + msg!("{:?}", thread::current().id()); + for _ in 1..=10 { + thread::spawn(|| { + msg!("{:?}", thread::current().id()); + thread::sleep(Duration::from_millis(100)); + let msgs = get_messages(); + assert_eq!(msgs.len(), 1); + assert_eq!(get_messages().len(), 0); + assert_eq!( + msgs.first().unwrap().message, + format!("{:?}", thread::current().id()) + ); + }); + } + thread::sleep(Duration::from_millis(200)); + let msgs = get_messages(); + assert_eq!(msgs.len(), 1); + assert_eq!(get_messages().len(), 0); + assert_eq!( + msgs.first().unwrap().message, + format!("{:?}", thread::current().id()) + ); + } + } } diff --git a/src/main.rs b/src/main.rs index 2c8b5949..d318696d 100644 --- a/src/main.rs +++ b/src/main.rs @@ -5,8 +5,8 @@ use reveaal::System::query_failures::QueryResult; use reveaal::ProtobufServer::services::query_request::Settings; use reveaal::{ - extract_system_rep, parse_queries, start_grpc_server_with_tokio, xml_parser, ComponentLoader, - JsonProjectLoader, ProjectLoader, Query, XmlProjectLoader, + extract_system_rep, parse_queries, set_server, start_grpc_server_with_tokio, xml_parser, + ComponentLoader, JsonProjectLoader, ProjectLoader, Query, XmlProjectLoader, }; use std::env; @@ -15,7 +15,19 @@ fn main() -> Result<(), Box> { let yaml = load_yaml!("cli.yml"); let matches = App::from(yaml).get_matches(); setup_logger().unwrap(); + /* + msg!(1, subject: "testing", msg: "gamer".to_string()); + msg!("gamer"); + msg!("testing", msg: "gamer".to_string()); + msg!(1, subject: "testing", msg: "gamer{}", 3); + println!("{:?}", get_messages().unwrap()); + println!("{:?}", get_messages().unwrap()); + println!("{:?}", get_messages().unwrap()); + println!("{:?}", get_messages().unwrap()); + */ + if let Some(ip_endpoint) = matches.value_of("endpoint") { + set_server(true); let thread_count: usize = match matches.value_of("thread_number") { Some(num_of_threads) => num_of_threads .parse() @@ -30,8 +42,11 @@ fn main() -> Result<(), Box> { start_grpc_server_with_tokio(ip_endpoint, cache_count, thread_count)?; } else { + set_server(false); start_using_cli(&matches); } + //println!("{:?}", get_messages().unwrap()); + //println!("{:?}", get_messages().unwrap()); Ok(()) } diff --git a/src/tests/reachability/parse_partial_state.rs b/src/tests/reachability/parse_partial_state.rs index 7b9f13bc..2f22d4e0 100644 --- a/src/tests/reachability/parse_partial_state.rs +++ b/src/tests/reachability/parse_partial_state.rs @@ -31,7 +31,7 @@ mod reachability_parse_partial_state { if let Ok(end_state) = result { assert_eq!( - end_state.get_location().id.is_partial_location(), + end_state.decorated_locations.id.is_partial_location(), expect_partial ); } else { diff --git a/src/tests/sample.rs b/src/tests/sample.rs index 2ca358f2..060e7716 100644 --- a/src/tests/sample.rs +++ b/src/tests/sample.rs @@ -12,8 +12,8 @@ mod samples { ); let t1 = project_loader.get_component("Test1"); - assert_eq!(t1.get_name(), "Test1"); - assert_eq!(t1.get_locations().len(), 2); + assert_eq!(t1.name, "Test1"); + assert_eq!(t1.locations.len(), 2); } #[test] @@ -24,8 +24,8 @@ mod samples { ); let t2 = project_loader.get_component("Test2"); - assert_eq!(t2.get_name(), "Test2"); - assert_eq!(t2.get_locations().len(), 2); + assert_eq!(t2.name, "Test2"); + assert_eq!(t2.locations.len(), 2); } #[test] @@ -36,8 +36,8 @@ mod samples { ); let t3 = project_loader.get_component("Test3"); - assert_eq!(t3.get_name(), "Test3"); - assert_eq!(t3.get_locations().len(), 3); + assert_eq!(t3.name, "Test3"); + assert_eq!(t3.locations.len(), 3); } #[test]