From e1104a01f5266629ddd5c9e7a39257afc0482d3e Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Thu, 27 Apr 2023 13:16:56 +0200 Subject: [PATCH 01/19] Initial fix and exploration --- src/ModelObjects/component.rs | 28 ++-- src/ModelObjects/representations.rs | 53 ++++--- src/TransitionSystems/compiled_component.rs | 2 + src/TransitionSystems/transition_system.rs | 162 ++++++++++++++------ 4 files changed, 163 insertions(+), 82 deletions(-) diff --git a/src/ModelObjects/component.rs b/src/ModelObjects/component.rs index 27bc26db..79a085bb 100644 --- a/src/ModelObjects/component.rs +++ b/src/ModelObjects/component.rs @@ -10,7 +10,7 @@ use crate::EdgeEval::updater::CompiledUpdate; use edbm::util::bounds::Bounds; use edbm::util::constraints::ClockIndex; -use crate::ModelObjects::representations::BoolExpression; +use crate::ModelObjects::representations::{BoolExpression, New}; use crate::TransitionSystems::{CompositionType, TransitionSystem}; use crate::TransitionSystems::{LocationTree, TransitionID}; use edbm::zones::OwnedFederation; @@ -191,17 +191,25 @@ impl Component { // Removes from from updates 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) + if let Some(guard) = e + .guard.as_mut() { - e.update.as_mut().unwrap().remove(i); + // Remove + match guard.remove_expr_with_name(&name) { + New::Changed(g) => *guard = g, + New::Unchanged => {} + New::Removed => e.guard = None, + } + } + if let Some(upd) = e.update.as_mut() { + if let Some((i, _)) = upd.iter() + .enumerate() + .find(|(_, u)| u.variable == name) + { + e.update.as_mut().unwrap().remove(i); + }; } }); info!( diff --git a/src/ModelObjects/representations.rs b/src/ModelObjects/representations.rs index 1cfe50ca..d2028422 100644 --- a/src/ModelObjects/representations.rs +++ b/src/ModelObjects/representations.rs @@ -6,7 +6,6 @@ use serde::Deserialize; use std::collections::HashMap; use std::fmt::{Display, Formatter}; use std::ops; -//use serde::de::Unexpected::Option; /// This file contains the nested enums used to represent systems on each side of refinement as well as all guards, updates etc /// note that the enum contains a box (pointer) to an object as they can only hold pointers to data on the heap @@ -443,32 +442,32 @@ impl BoolExpression { } } - /// Replaces all occurrences of `ArithExpression::VarName(old)` with `new` - - /// # Arguments - /// `old`: The `varname` to be replaced - - /// `new`: The new varname - pub fn replace_varname(&mut self, old: &String, new: &String) { + pub fn remove_expr_with_name(&self, name: &str) -> New { match self { - BoolExpression::Parentheses(p) => p.replace_varname(old, new), - BoolExpression::AndOp(e1, e2) | BoolExpression::OrOp(e1, e2) => { - e1.replace_varname(old, new); - e2.replace_varname(old, new); - } - BoolExpression::LessEQ(e1, e2) - | BoolExpression::GreatEQ(e1, e2) - | BoolExpression::LessT(e1, e2) - | BoolExpression::GreatT(e1, e2) - | BoolExpression::EQ(e1, e2) => { - e1.replace_varname(old, new); - e2.replace_varname(old, new); - } - BoolExpression::Bool(_) => (), - BoolExpression::Arithmetic(a) => a.replace_varname(old, new), + BoolExpression::Parentheses(p) => p.remove_expr_with_name(name), + BoolExpression::AndOp(l, r) | + BoolExpression::OrOp(l, r) => { + if l.get_varnames().contains(&name) { + New::Changed(*r.to_owned()) + } else if r.get_varnames().contains(&name) { + New::Changed(*l.to_owned()) + } else { New::Unchanged } + } + BoolExpression::LessEQ(l, r) | + BoolExpression::GreatEQ(l, r) | + BoolExpression::LessT(l, r) | + BoolExpression::GreatT(l, r) | + BoolExpression::EQ(l, r) => { + if l.get_varnames().contains(&name) || r.get_varnames().contains(&name) { + New::Removed + } else { New::Unchanged } + } + BoolExpression::Bool(_) => New::Unchanged, + BoolExpression::Arithmetic(a) => if a.get_varnames().contains(&name) { + New::Removed + } else { New::Unchanged }, } } - pub fn BLessEQ(left: ArithExpression, right: ArithExpression) -> BoolExpression { BoolExpression::LessEQ(Box::new(left), Box::new(right)) } @@ -489,6 +488,12 @@ impl BoolExpression { } } +pub enum New { + Changed(T), + Unchanged, + Removed +} + fn var_from_naming( naming: &HashMap, index: ClockIndex, diff --git a/src/TransitionSystems/compiled_component.rs b/src/TransitionSystems/compiled_component.rs index 7c201d9f..47de54fa 100644 --- a/src/TransitionSystems/compiled_component.rs +++ b/src/TransitionSystems/compiled_component.rs @@ -62,6 +62,8 @@ impl CompiledComponent { let mut location_edges: HashMap> = locations.keys().map(|k| (k.clone(), vec![])).collect(); + log::debug!("decl for {:?}: {:?}", component.name, component.declarations); + log::debug!("Edges: {:?}", component.get_edges()); for edge in component.get_edges() { let id = LocationID::Simple(edge.source_location.clone()); let transition = Transition::from(&component, edge, dim); diff --git a/src/TransitionSystems/transition_system.rs b/src/TransitionSystems/transition_system.rs index f0abebfa..df4b409a 100644 --- a/src/TransitionSystems/transition_system.rs +++ b/src/TransitionSystems/transition_system.rs @@ -16,6 +16,7 @@ use dyn_clone::{clone_trait_object, DynClone}; use edbm::util::{bounds::Bounds, constraints::ClockIndex}; use pest::Parser; use std::collections::hash_map::Entry; +use std::collections::vec_deque::VecDeque; use std::collections::{hash_set::HashSet, HashMap}; use std::hash::Hash; @@ -178,15 +179,20 @@ 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); + + log::debug!( + "All transitions:\n{}", + self.get_all_locations() + .into_iter() + .map(|l| l.id.get_unique_string()) + .collect::>() + .join("\n") + ); graph } @@ -194,52 +200,112 @@ 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(), - }; + 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() { + // for location in init_location { + log::debug!("loc: {:?}", location.id.get_unique_string()); + //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 { + let transitions = self.next_transitions_if_available(&location, action); + //log::debug!("Trans: {transitions:?}"); + 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 { + for constraint in conjunction.iter() { + edge.guard_dependencies.insert(constraint.i); + edge.guard_dependencies.insert(constraint.j); + } + } + + graph.edges.push(edge); - //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); + if !graph + .nodes + .contains_key(&transition.target_locations.id.get_unique_string()) + { + worklist.push_back(transition.target_locations); + //self.find_edges_and_nodes(&transition.target_locations, actions, graph); + } } } } - 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_all(&self, graph: &mut ClockAnalysisGraph) { + let actions = self.get_actions(); + for location in self.get_all_locations() { + log::debug!("loc: {:?}", location.id.get_unique_string()); + //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 { + let transitions = self.next_transitions_if_available(&location, action); + //log::debug!("Trans: {transitions:?}"); + 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 { + 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); + } } } } @@ -326,15 +392,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(); From 8622a2d2618f62631640e916e5f5f1d81e31ad8b Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Sat, 6 May 2023 11:42:39 +0200 Subject: [PATCH 02/19] Finalized fix --- src/ModelObjects/component.rs | 40 +++++++----- src/ModelObjects/representations.rs | 67 +++++--------------- src/TransitionSystems/compiled_component.rs | 6 +- src/TransitionSystems/transition_system.rs | 69 ++------------------- src/lib.rs | 2 +- 5 files changed, 50 insertions(+), 134 deletions(-) diff --git a/src/ModelObjects/component.rs b/src/ModelObjects/component.rs index bf76ff2d..95c72274 100644 --- a/src/ModelObjects/component.rs +++ b/src/ModelObjects/component.rs @@ -10,7 +10,7 @@ use crate::EdgeEval::updater::CompiledUpdate; use edbm::util::bounds::Bounds; use edbm::util::constraints::ClockIndex; -use crate::ModelObjects::representations::{BoolExpression, New}; +use crate::ModelObjects::representations::BoolExpression; use crate::TransitionSystems::{CompositionType, TransitionSystem}; use crate::TransitionSystems::{LocationTree, TransitionID}; use edbm::zones::OwnedFederation; @@ -187,30 +187,42 @@ 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() || e.guard.is_some()) .for_each(|e| { - if let Some(guard) = e - .guard.as_mut() - { - // Remove - match guard.remove_expr_with_name(&name) { - New::Changed(g) => *guard = g, - New::Unchanged => {} - New::Removed => e.guard = None, + if let Some(guard) = e.guard.as_mut() { + // 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 guard.has_varname(&name) { + *guard = BoolExpression::Bool(false); } } + if let Some(upd) = e.update.as_mut() { - if let Some((i, _)) = upd.iter() - .enumerate() - .find(|(_, u)| u.variable == name) - { + if let Some((i, _)) = upd.iter().enumerate().find(|(_, u)| u.variable == name) { e.update.as_mut().unwrap().remove(i); }; } }); + + // Removes from from location invariants + self.locations + .iter_mut() + .filter(|l| l.invariant.is_some()) + .for_each(|l| { + if let Some(invariant) = l.invariant.as_mut() { + // The invariant is 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. + if invariant.has_varname(&name) { + *invariant = BoolExpression::Bool(false); + } + } + }); + info!( "Removed Clock '{name}' (index {index}) has been removed from component {}", self.name diff --git a/src/ModelObjects/representations.rs b/src/ModelObjects/representations.rs index af0c8405..8041337a 100644 --- a/src/ModelObjects/representations.rs +++ b/src/ModelObjects/representations.rs @@ -418,56 +418,22 @@ 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::Parentheses(p) => p.get_varnames(), - BoolExpression::AndOp(p1, p2) | BoolExpression::OrOp(p1, p2) => p1 - .get_varnames() - .iter() - .chain(p2.get_varnames().iter()) - .copied() - .collect(), + BoolExpression::Parentheses(p) => p.has_varname(name), + 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::Arithmetic(a) => a.get_varnames(), + | BoolExpression::EQ(a1, a2) => a1.has_varname(name) || a2.has_varname(name), + BoolExpression::Bool(_) => false, + BoolExpression::Arithmetic(a) => a.has_varname(name), } } - pub fn remove_expr_with_name(&self, name: &str) -> New { - match self { - BoolExpression::Parentheses(p) => p.remove_expr_with_name(name), - BoolExpression::AndOp(l, r) | - BoolExpression::OrOp(l, r) => { - if l.get_varnames().contains(&name) { - New::Changed(*r.to_owned()) - } else if r.get_varnames().contains(&name) { - New::Changed(*l.to_owned()) - } else { New::Unchanged } - } - BoolExpression::LessEQ(l, r) | - BoolExpression::GreatEQ(l, r) | - BoolExpression::LessT(l, r) | - BoolExpression::GreatT(l, r) | - BoolExpression::EQ(l, r) => { - if l.get_varnames().contains(&name) || r.get_varnames().contains(&name) { - New::Removed - } else { New::Unchanged } - } - BoolExpression::Bool(_) => New::Unchanged, - BoolExpression::Arithmetic(a) => if a.get_varnames().contains(&name) { - New::Removed - } else { New::Unchanged }, - } - } pub fn BLessEQ(left: ArithExpression, right: ArithExpression) -> BoolExpression { BoolExpression::LessEQ(Box::new(left), Box::new(right)) } @@ -491,7 +457,7 @@ impl BoolExpression { pub enum New { Changed(T), Unchanged, - Removed + Removed, } fn var_from_naming( @@ -1022,21 +988,16 @@ 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::Parentheses(p) => p.get_varnames(), + ArithExpression::Parentheses(p) => p.has_varname(name), 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/TransitionSystems/compiled_component.rs b/src/TransitionSystems/compiled_component.rs index ada141c4..e469f4ed 100644 --- a/src/TransitionSystems/compiled_component.rs +++ b/src/TransitionSystems/compiled_component.rs @@ -62,7 +62,11 @@ impl CompiledComponent { let mut location_edges: HashMap> = locations.keys().map(|k| (k.clone(), vec![])).collect(); - log::debug!("decl for {:?}: {:?}", component.name, component.declarations); + log::debug!( + "decl for {:?}: {:?}", + component.name, + component.declarations + ); log::debug!("Edges: {:?}", component.get_edges()); for edge in component.get_edges() { let id = LocationID::Simple(edge.source_location.clone()); diff --git a/src/TransitionSystems/transition_system.rs b/src/TransitionSystems/transition_system.rs index df4b409a..db626ce4 100644 --- a/src/TransitionSystems/transition_system.rs +++ b/src/TransitionSystems/transition_system.rs @@ -109,6 +109,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 { @@ -185,15 +188,6 @@ pub trait TransitionSystem: DynClone { let mut graph: ClockAnalysisGraph = ClockAnalysisGraph::from_dim(self.get_dim()); self.find_edges_and_nodes(self.get_initial_location().unwrap(), &mut graph); - log::debug!( - "All transitions:\n{}", - self.get_all_locations() - .into_iter() - .map(|l| l.id.get_unique_string()) - .collect::>() - .join("\n") - ); - graph } @@ -204,8 +198,6 @@ pub trait TransitionSystem: DynClone { let mut worklist = VecDeque::from([init_location]); let actions = self.get_actions(); while let Some(location) = worklist.pop_front() { - // for location in init_location { - log::debug!("loc: {:?}", location.id.get_unique_string()); //Constructs a node to represent this location and add it to the graph. let mut node: ClockAnalysisNode = ClockAnalysisNode { invariant_dependencies: HashSet::new(), @@ -226,9 +218,7 @@ pub trait TransitionSystem: DynClone { //Constructs an edge to represent each transition from this graph and add it to the graph. for action in &actions { - let transitions = self.next_transitions_if_available(&location, action); - //log::debug!("Trans: {transitions:?}"); - for transition in transitions { + 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(), @@ -253,58 +243,7 @@ pub trait TransitionSystem: DynClone { .contains_key(&transition.target_locations.id.get_unique_string()) { worklist.push_back(transition.target_locations); - //self.find_edges_and_nodes(&transition.target_locations, actions, graph); - } - } - } - } - } - - fn find_edges_and_nodes_all(&self, graph: &mut ClockAnalysisGraph) { - let actions = self.get_actions(); - for location in self.get_all_locations() { - log::debug!("loc: {:?}", location.id.get_unique_string()); - //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 { - let transitions = self.next_transitions_if_available(&location, action); - //log::debug!("Trans: {transitions:?}"); - 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 { - for constraint in conjunction.iter() { - edge.guard_dependencies.insert(constraint.i); - edge.guard_dependencies.insert(constraint.j); - } } - - graph.edges.push(edge); } } } diff --git a/src/lib.rs b/src/lib.rs index e8a6c57c..33b0f41a 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -23,7 +23,7 @@ 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, }; #[macro_use] From 9824297d03cb7ea7cde331dc74f991140456d8f2 Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Thu, 18 May 2023 09:36:14 +0200 Subject: [PATCH 03/19] Minor optimizations --- src/ModelObjects/component.rs | 42 +++++++++++------------------ src/ModelObjects/representations.rs | 6 ----- 2 files changed, 16 insertions(+), 32 deletions(-) diff --git a/src/ModelObjects/component.rs b/src/ModelObjects/component.rs index 95c72274..18cfb083 100644 --- a/src/ModelObjects/component.rs +++ b/src/ModelObjects/component.rs @@ -18,6 +18,7 @@ use log::info; use serde::{Deserialize, Serialize}; 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, Eq, PartialEq)] #[serde(into = "DummyComponent")] @@ -192,36 +193,25 @@ impl Component { .iter_mut() .filter(|e| e.update.is_some() || e.guard.is_some()) .for_each(|e| { - if let Some(guard) = e.guard.as_mut() { - // 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 guard.has_varname(&name) { - *guard = BoolExpression::Bool(false); - } - } - - if let Some(upd) = e.update.as_mut() { - if let Some((i, _)) = upd.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); } + e.update.as_mut().unwrap().retain(|u| u.variable != name); }); // Removes from from location invariants - self.locations - .iter_mut() - .filter(|l| l.invariant.is_some()) - .for_each(|l| { - if let Some(invariant) = l.invariant.as_mut() { - // The invariant is 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. - if invariant.has_varname(&name) { - *invariant = BoolExpression::Bool(false); - } - } - }); + // 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.retain(|l| { + l.invariant + .as_ref() + .filter(|i| i.has_varname(&name)) + .is_none() + }); info!( "Removed Clock '{name}' (index {index}) has been removed from component {}", diff --git a/src/ModelObjects/representations.rs b/src/ModelObjects/representations.rs index 8041337a..61193cdf 100644 --- a/src/ModelObjects/representations.rs +++ b/src/ModelObjects/representations.rs @@ -454,12 +454,6 @@ impl BoolExpression { } } -pub enum New { - Changed(T), - Unchanged, - Removed, -} - fn var_from_naming( naming: &HashMap, index: ClockIndex, From a730b85cb94e6a5eee3a0dd3193708438b234182 Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Thu, 18 May 2023 09:54:07 +0200 Subject: [PATCH 04/19] Invariant update --- src/ModelObjects/component.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/ModelObjects/component.rs b/src/ModelObjects/component.rs index 18cfb083..eafb9e72 100644 --- a/src/ModelObjects/component.rs +++ b/src/ModelObjects/component.rs @@ -199,7 +199,9 @@ impl Component { if let Some(guard) = e.guard.as_mut().filter(|g| g.has_varname(&name)) { *guard = BoolExpression::Bool(false); } - e.update.as_mut().unwrap().retain(|u| u.variable != name); + if let Some(inv) = e.update.as_mut() { + inv.retain(|u| u.variable != name); + } }); // Removes from from location invariants From 2621e4f236c1b3878e807a58cbe055b17289f408 Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Thu, 18 May 2023 10:29:36 +0200 Subject: [PATCH 05/19] Removed and refactored some unused and unnecessary functions --- src/EdgeEval/constraint_applyer.rs | 6 +- src/ModelObjects/component.rs | 167 ++++--------------------- src/ModelObjects/representations.rs | 6 + src/System/input_enabler.rs | 26 ++-- src/System/pruning.rs | 79 ++++++------ src/TransitionSystems/location_tree.rs | 6 +- 6 files changed, 85 insertions(+), 205 deletions(-) diff --git a/src/EdgeEval/constraint_applyer.rs b/src/EdgeEval/constraint_applyer.rs index e615828e..e17a1073 100644 --- a/src/EdgeEval/constraint_applyer.rs +++ b/src/EdgeEval/constraint_applyer.rs @@ -158,9 +158,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()) @@ -174,7 +174,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::Parentheses(x) => get_const(x, decls), ArithExpression::Difference(l, r) => get_const(l, decls) - get_const(r, decls), ArithExpression::Addition(l, r) => get_const(l, decls) + get_const(r, decls), diff --git a/src/ModelObjects/component.rs b/src/ModelObjects/component.rs index eafb9e72..aa77d8ca 100644 --- a/src/ModelObjects/component.rs +++ b/src/ModelObjects/component.rs @@ -14,10 +14,12 @@ use crate::ModelObjects::representations::BoolExpression; use crate::TransitionSystems::{CompositionType, TransitionSystem}; use crate::TransitionSystems::{LocationTree, TransitionID}; use edbm::zones::OwnedFederation; +use itertools::Itertools; use log::info; 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)] @@ -53,9 +55,6 @@ impl Component { 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 @@ -76,59 +75,26 @@ impl Component { 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 @@ -138,7 +104,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; @@ -147,7 +113,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; @@ -163,11 +129,6 @@ 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 @@ -247,10 +208,6 @@ impl Component { } } -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 @@ -368,21 +325,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, @@ -418,7 +360,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() @@ -614,7 +556,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!( @@ -626,7 +567,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(()) @@ -639,7 +580,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); } @@ -649,47 +590,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 { @@ -711,49 +617,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/representations.rs b/src/ModelObjects/representations.rs index 61193cdf..0d44d0df 100644 --- a/src/ModelObjects/representations.rs +++ b/src/ModelObjects/representations.rs @@ -454,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/System/input_enabler.rs b/src/System/input_enabler.rs index 1f8df17d..6fe51cf9 100644 --- a/src/System/input_enabler.rs +++ b/src/System/input_enabler.rs @@ -11,11 +11,11 @@ pub fn make_input_enabled(component: &mut component::Component, inputs: &[String let input_edges = component .get_edges() .iter() - .filter(|edge| *edge.get_sync_type() == component::SyncType::Input); + .filter(|edge| edge.sync_type == component::SyncType::Input); for location in component.get_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(), diff --git a/src/System/pruning.rs b/src/System/pruning.rs index 47db8b18..53b4b176 100644 --- a/src/System/pruning.rs +++ b/src/System/pruning.rs @@ -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); @@ -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); } @@ -313,11 +313,11 @@ fn predt_of_all_outputs( .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/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, } From 373bee0dbe5a1cf1df7d1456453a650f94474058 Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Thu, 18 May 2023 10:43:36 +0200 Subject: [PATCH 06/19] Removed additional --- src/DataReader/component_loader.rs | 18 +++++++-------- src/DataReader/json_writer.rs | 2 +- src/DataReader/proto_reader.rs | 3 +-- src/ModelObjects/component.rs | 23 +------------------ src/ModelObjects/system_declarations.rs | 4 ++-- .../ecdar_requests/send_query.rs | 4 ++-- src/System/extract_state.rs | 3 +-- src/System/extract_system_rep.rs | 2 +- src/System/input_enabler.rs | 6 ++--- src/System/local_consistency.rs | 5 ++-- src/System/pruning.rs | 8 +++---- src/System/reachability.rs | 10 ++++---- src/TransitionSystems/compiled_component.rs | 6 ++--- src/tests/reachability/parse_partial_state.rs | 2 +- src/tests/sample.rs | 12 +++++----- 15 files changed, 42 insertions(+), 66 deletions(-) diff --git a/src/DataReader/component_loader.rs b/src/DataReader/component_loader.rs index 1d259a79..4ff13a39 100644 --- a/src/DataReader/component_loader.rs +++ b/src/DataReader/component_loader.rs @@ -114,7 +114,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); @@ -150,10 +150,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)) } @@ -213,7 +213,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); @@ -223,7 +223,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 { @@ -268,7 +268,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); } @@ -293,7 +293,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); @@ -333,12 +333,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 ef7d5597..035621b8 100644 --- a/src/DataReader/proto_reader.rs +++ b/src/DataReader/proto_reader.rs @@ -187,8 +187,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/ModelObjects/component.rs b/src/ModelObjects/component.rs index aa77d8ca..9571c137 100644 --- a/src/ModelObjects/component.rs +++ b/src/ModelObjects/component.rs @@ -48,14 +48,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_location_by_name(&self, name: &str) -> &Location { let loc_vec = self .locations @@ -69,15 +61,6 @@ 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_edges(&mut self, edges: &mut Vec) { - self.edges.append(edges); - } pub fn get_input_actions(&self) -> Vec { self.get_specific_actions(SyncType::Input) @@ -132,7 +115,7 @@ impl Component { /// 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); } } @@ -278,10 +261,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); let zone = self.take_zone().extrapolate_max_bounds(&bounds); 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/send_query.rs b/src/ProtobufServer/ecdar_requests/send_query.rs index d07f1b6c..f0b442fc 100644 --- a/src/ProtobufServer/ecdar_requests/send_query.rs +++ b/src/ProtobufServer/ecdar_requests/send_query.rs @@ -131,11 +131,11 @@ fn parse_xml_components(xml: &str) -> Vec { 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/System/extract_state.rs b/src/System/extract_state.rs index 5740fac3..a00cd6ad 100644 --- a/src/System/extract_state.rs +++ b/src/System/extract_state.rs @@ -95,8 +95,7 @@ fn build_location_tree( .get_location(&LocationID::Simple(str.to_string())) .ok_or(format!( "Location {} does not exist in the component {}", - str, - component.get_name() + str, component.name )), }, } diff --git a/src/System/extract_system_rep.rs b/src/System/extract_system_rep.rs index 35c9ad51..865b43a8 100644 --- a/src/System/extract_system_rep.rs +++ b/src/System/extract_system_rep.rs @@ -74,7 +74,7 @@ pub fn create_executable_query<'a>( let start_state: State = if let Some(state) = start.as_ref() { validate_reachability_input(&machine, state)?; 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 6fe51cf9..e7345287 100644 --- a/src/System/input_enabler.rs +++ b/src/System/input_enabler.rs @@ -9,10 +9,10 @@ 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.sync_type == component::SyncType::Input); - for location in component.get_locations() { + for location in &component.locations { let mut location_inv_zone = OwnedFederation::universe(dimension); if let Some(invariant) = &location.invariant { @@ -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 53b4b176..39919d1a 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); @@ -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) @@ -309,7 +309,7 @@ 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) { diff --git a/src/System/reachability.rs b/src/System/reachability.rs index fa349cdc..34a8f8bb 100644 --- a/src/System/reachability.rs +++ b/src/System/reachability.rs @@ -30,7 +30,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; } @@ -114,7 +114,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()], ); @@ -152,8 +152,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()) } @@ -169,7 +169,7 @@ fn take_transition( if transition.use_transition(&mut new_state) { // TODO: bounds here are not always correct, they should take the added bounds from the target state into account new_state.extrapolate_max_bounds(system.as_ref()); // Ensures the bounds cant grow infinitely, avoiding infinite loops - 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 e469f4ed..bec86aaa 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); @@ -67,8 +67,8 @@ impl CompiledComponent { component.name, component.declarations ); - log::debug!("Edges: {:?}", component.get_edges()); - for edge in component.get_edges() { + 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/tests/reachability/parse_partial_state.rs b/src/tests/reachability/parse_partial_state.rs index 1e07ba35..e634872c 100644 --- a/src/tests/reachability/parse_partial_state.rs +++ b/src/tests/reachability/parse_partial_state.rs @@ -33,7 +33,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] From 72834a610311037e1b4d624521da98ae43c290f9 Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Thu, 18 May 2023 14:15:28 +0200 Subject: [PATCH 07/19] Initial impl --- Cargo.toml | 1 + src/ModelObjects/component.rs | 12 +++- .../ecdar_requests/send_query.rs | 2 +- src/logging.rs | 62 ++++++++++++++++++- src/main.rs | 19 +++++- 5 files changed, 88 insertions(+), 8 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index 9ca41880..11421209 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -45,6 +45,7 @@ lru = "0.8.1" itertools = "0.10.5" regex = "1" rayon = "1.6.1" +once_cell = "1.17.1" # Enable optimizations for EDBM in debug mode, but not for our code: [profile.dev.package.edbm] diff --git a/src/ModelObjects/component.rs b/src/ModelObjects/component.rs index 9571c137..4173123c 100644 --- a/src/ModelObjects/component.rs +++ b/src/ModelObjects/component.rs @@ -10,6 +10,7 @@ use crate::EdgeEval::updater::CompiledUpdate; use edbm::util::bounds::Bounds; use edbm::util::constraints::ClockIndex; +use crate::msg; use crate::ModelObjects::representations::BoolExpression; use crate::TransitionSystems::{CompositionType, TransitionSystem}; use crate::TransitionSystems::{LocationTree, TransitionID}; @@ -163,6 +164,9 @@ impl Component { "Removed Clock '{name}' (index {index}) has been removed from component {}", self.name ); // Should be changed in the future to be the information logger + + msg!("Clock Reduction", msg: "Removed Clock '{name}' (index {index}) has been removed from component {}", + self.name) } /// Replaces duplicate clock with a new @@ -183,10 +187,16 @@ 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 {}", self.name - ); // Should be changed in the future to be the information logger + ); + + msg!("Clock Reduction", + msg: "Replaced Clock '{name}' (index {old}) with {global_index} in component {}", + self.name + ); } } } diff --git a/src/ProtobufServer/ecdar_requests/send_query.rs b/src/ProtobufServer/ecdar_requests/send_query.rs index f0b442fc..b175bd77 100644 --- a/src/ProtobufServer/ecdar_requests/send_query.rs +++ b/src/ProtobufServer/ecdar_requests/send_query.rs @@ -69,7 +69,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().unwrap_or_default(), result: Some(result.into()), }) } diff --git a/src/logging.rs b/src/logging.rs index c3eb6739..0fd8084b 100644 --- a/src/logging.rs +++ b/src/logging.rs @@ -2,7 +2,14 @@ use crate::ProtobufServer::services::query_response::Information; use chrono::Local; use colored::{ColoredString, Colorize}; use log::SetLoggerError; +use once_cell::sync::Lazy; +use std::collections::hash_map::Entry; +use std::collections::HashMap; use std::io::Write; +use std::sync::Mutex; +use std::thread; +use std::thread::ThreadId; +//use std::time::Duration; #[cfg(feature = "logging")] /// Sets up the logging @@ -32,8 +39,57 @@ pub fn setup_logger() -> Result<(), SetLoggerError> { .try_init() } -// TODO: Implement a logging for informations to both the CLI and gRPC +#[macro_export] +macro_rules! msg { //TODO: Check for server or not; if server, save in table, otherwise use info (for now) --- thread::current().id() + ($severity:expr, subject: $subject:expr, msg: $msg:expr) => ($crate::logging::__set_info__($severity, $subject, $msg)); + + + ($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)); + ($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())); +} + +#[doc(hidden)] +static __MESSAGES__: Lazy>>> = Lazy::new(Mutex::default); + /// Gets messages saved for other clients (through gRPC) -pub fn get_messages() -> Vec { - unimplemented!() +#[doc(hidden)] +pub fn __set_info__(severity: i32, subject: &str, message: String) { + let msg = Information { + serverity: severity, + subject: subject.to_string(), + message, + }; + + match __MESSAGES__.lock().unwrap().entry(thread::current().id()) { + Entry::Occupied(mut o) => o.get_mut().push(msg), + Entry::Vacant(v) => { + v.insert(vec![msg]); + } + }; +} + +//static mut TEMP: i32 = 10; + +pub fn get_messages() -> Option> { + //println!("{:?}", thread::current().name()); + /* + unsafe { + println!("{}", TEMP); + } + thread::spawn(|| unsafe { + TEMP = 20; + println!("{}", TEMP); + }); + thread::sleep(Duration::from_millis(1000)); + unsafe { + println!("{}", TEMP); + } + */ + + __MESSAGES__.lock().unwrap().remove(&thread::current().id()) } diff --git a/src/main.rs b/src/main.rs index af0c90d4..6b341a79 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,12 +1,12 @@ #![allow(non_snake_case)] use clap::{load_yaml, App}; -use reveaal::logging::setup_logger; +use reveaal::logging::{get_messages, setup_logger}; 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, msg, parse_queries, start_grpc_server_with_tokio, xml_parser, + ComponentLoader, JsonProjectLoader, ProjectLoader, Query, XmlProjectLoader, }; use std::env; @@ -15,6 +15,17 @@ 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") { let thread_count: usize = match matches.value_of("thread_number") { Some(num_of_threads) => num_of_threads @@ -32,6 +43,8 @@ fn main() -> Result<(), Box> { } else { start_using_cli(&matches); } + println!("{:?}", get_messages().unwrap()); + println!("{:?}", get_messages().unwrap()); Ok(()) } From 4ae4686138f47eb1ffd50b76ab7dccb1acbde543 Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Thu, 18 May 2023 14:43:04 +0200 Subject: [PATCH 08/19] added server check --- src/ModelObjects/component.rs | 2 +- src/lib.rs | 12 ++++++++++++ src/logging.rs | 34 ++++++++++++++++++++++++++-------- src/main.rs | 8 +++++--- 4 files changed, 44 insertions(+), 12 deletions(-) diff --git a/src/ModelObjects/component.rs b/src/ModelObjects/component.rs index 4173123c..ce233d5b 100644 --- a/src/ModelObjects/component.rs +++ b/src/ModelObjects/component.rs @@ -166,7 +166,7 @@ impl Component { ); // Should be changed in the future to be the information logger msg!("Clock Reduction", msg: "Removed Clock '{name}' (index {index}) has been removed from component {}", - self.name) + self.name); } /// Replaces duplicate clock with a new diff --git a/src/lib.rs b/src/lib.rs index 33b0f41a..d64ac23f 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -26,6 +26,18 @@ pub const DEFAULT_SETTINGS: Settings = Settings { disable_clock_reduction: true, }; +static mut IS_SERVER: Option = None; + +pub fn set_server(is_server: bool) { + unsafe { + IS_SERVER = Some(is_server); + } +} + +fn is_server() -> bool { + unsafe { IS_SERVER.expect("Server or CLI never specified") } +} + #[macro_use] extern crate pest_derive; extern crate colored; diff --git a/src/logging.rs b/src/logging.rs index 0fd8084b..45bfc953 100644 --- a/src/logging.rs +++ b/src/logging.rs @@ -40,8 +40,20 @@ pub fn setup_logger() -> Result<(), SetLoggerError> { } #[macro_export] -macro_rules! msg { //TODO: Check for server or not; if server, save in table, otherwise use info (for now) --- thread::current().id() - ($severity:expr, subject: $subject:expr, msg: $msg:expr) => ($crate::logging::__set_info__($severity, $subject, $msg)); +macro_rules! msg { //TODO: Maybe format the information when not server + ($severity:expr, subject: $subject:expr, msg: $msg:expr) => ({ + if $crate::is_server() { + $crate::logging::__set_info__($crate::logging::__as_information__($severity, $subject, $msg)); + } else { + //println!("{:?}", $crate::logging::__as_information__($severity, $subject, $msg)); + let lvl = match $severity { + 0 => log::Level::Info, + 1 => log::Level::Warn, + _ => unreachable!(), + }; + log::log!(lvl, "{:?}", $crate::logging::__as_information__($severity, $subject, $msg)); + } + }); ($severity:expr, subject: $subject:expr, msg: $($msg:tt)+) => (msg!($severity, subject: $subject, msg: format_args!($($msg)+).to_string())); @@ -56,25 +68,31 @@ macro_rules! msg { //TODO: Check for server or not; if server, save in table, ot #[doc(hidden)] static __MESSAGES__: Lazy>>> = Lazy::new(Mutex::default); -/// Gets messages saved for other clients (through gRPC) #[doc(hidden)] -pub fn __set_info__(severity: i32, subject: &str, message: String) { - let msg = Information { +pub fn __as_information__(severity: i32, subject: &str, message: String) -> Information { + Information { serverity: 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(msg), + Entry::Occupied(mut o) => o.get_mut().push(info), Entry::Vacant(v) => { - v.insert(vec![msg]); + v.insert(vec![info]); } }; } //static mut TEMP: i32 = 10; +/// 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() -> Option> { //println!("{:?}", thread::current().name()); /* diff --git a/src/main.rs b/src/main.rs index 6b341a79..dfb19860 100644 --- a/src/main.rs +++ b/src/main.rs @@ -5,7 +5,7 @@ use reveaal::System::query_failures::QueryResult; use reveaal::ProtobufServer::services::query_request::Settings; use reveaal::{ - extract_system_rep, msg, parse_queries, start_grpc_server_with_tokio, xml_parser, + extract_system_rep, msg, parse_queries, set_server, start_grpc_server_with_tokio, xml_parser, ComponentLoader, JsonProjectLoader, ProjectLoader, Query, XmlProjectLoader, }; use std::env; @@ -27,6 +27,7 @@ fn main() -> Result<(), Box> { */ 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() @@ -41,10 +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()); + //println!("{:?}", get_messages().unwrap()); + //println!("{:?}", get_messages().unwrap()); Ok(()) } From f79038cfb8f18c3bdf3b44f39d828def63a51e12 Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Thu, 18 May 2023 15:07:49 +0200 Subject: [PATCH 09/19] added server check and impl Display --- src/ModelObjects/component.rs | 15 +++-- .../ecdar_requests/send_query.rs | 2 +- src/logging.rs | 66 ++++++++++++------- src/main.rs | 4 +- 4 files changed, 56 insertions(+), 31 deletions(-) diff --git a/src/ModelObjects/component.rs b/src/ModelObjects/component.rs index ce233d5b..18b1fc1a 100644 --- a/src/ModelObjects/component.rs +++ b/src/ModelObjects/component.rs @@ -160,10 +160,12 @@ impl Component { .is_none() }); + /* info!( "Removed Clock '{name}' (index {index}) has been removed from component {}", self.name - ); // Should be changed in the future to be the information logger + ); + */ msg!("Clock Reduction", msg: "Removed Clock '{name}' (index {index}) has been removed from component {}", self.name); @@ -187,11 +189,12 @@ 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 {}", - self.name - ); + /* + info!( + "Replaced Clock '{name}' (index {old}) with {global_index} in component {}", + self.name + ); + */ msg!("Clock Reduction", msg: "Replaced Clock '{name}' (index {old}) with {global_index} in component {}", diff --git a/src/ProtobufServer/ecdar_requests/send_query.rs b/src/ProtobufServer/ecdar_requests/send_query.rs index b175bd77..fce56b62 100644 --- a/src/ProtobufServer/ecdar_requests/send_query.rs +++ b/src/ProtobufServer/ecdar_requests/send_query.rs @@ -69,7 +69,7 @@ impl ConcreteEcdarBackend { let result = query.execute(); Ok(QueryResponse { query_id: query_request.query_id, - info: crate::logging::get_messages().unwrap_or_default(), + info: crate::logging::get_messages(), result: Some(result.into()), }) } diff --git a/src/logging.rs b/src/logging.rs index 45bfc953..be05d6ff 100644 --- a/src/logging.rs +++ b/src/logging.rs @@ -5,25 +5,26 @@ use log::SetLoggerError; use once_cell::sync::Lazy; use std::collections::hash_map::Entry; use std::collections::HashMap; +use std::fmt::{Display, Formatter}; use std::io::Write; use std::sync::Mutex; use std::thread; use std::thread::ThreadId; -//use std::time::Duration; #[cfg(feature = "logging")] -/// Sets up the logging -pub fn setup_logger() -> Result<(), SetLoggerError> { - fn colored_level(level: log::Level) -> ColoredString { - match level { - log::Level::Error => level.to_string().red(), - log::Level::Warn => level.to_string().yellow(), - log::Level::Info => level.to_string().cyan(), - log::Level::Debug => level.to_string().blue(), - log::Level::Trace => level.to_string().magenta(), - } +fn colored_level(level: log::Level) -> ColoredString { + match level { + log::Level::Error => level.to_string().red(), + log::Level::Warn => level.to_string().yellow(), + log::Level::Info => level.to_string().cyan(), + log::Level::Debug => level.to_string().blue(), + log::Level::Trace => level.to_string().magenta(), } +} +#[cfg(feature = "logging")] +/// Sets up the logging +pub fn setup_logger() -> Result<(), SetLoggerError> { env_logger::Builder::from_env(env_logger::Env::default()) .format(|buf, record| { writeln!( @@ -45,13 +46,9 @@ macro_rules! msg { //TODO: Maybe format the information when not server if $crate::is_server() { $crate::logging::__set_info__($crate::logging::__as_information__($severity, $subject, $msg)); } else { - //println!("{:?}", $crate::logging::__as_information__($severity, $subject, $msg)); - let lvl = match $severity { - 0 => log::Level::Info, - 1 => log::Level::Warn, - _ => unreachable!(), - }; - log::log!(lvl, "{:?}", $crate::logging::__as_information__($severity, $subject, $msg)); + //let lvl = $crate::logging::__severity__($severity); + //log::log!(lvl, "{}", $crate::logging::__as_information__($severity, $subject, $msg)); + println!("{}", $crate::logging::__as_information__($severity, $subject, $msg)); } }); @@ -65,6 +62,28 @@ macro_rules! msg { //TODO: Maybe format the information when not server ($($msg:tt)+) => (msg!(0, subject: "general", msg: format_args!($($msg)+).to_string())); } +#[doc(hidden)] +pub fn __severity__(severity: i32) -> log::Level { + match severity { + 0 => log::Level::Info, + 1 => log::Level::Warn, + _ => unreachable!(), + } +} + +impl Display for Information { + fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { + write!( + f, + "[{} {}: {}] - {}", + Local::now().format("%H:%M:%S").to_string().cyan(), + colored_level(__severity__(self.serverity)), + self.subject, + self.message + ) + } +} + #[doc(hidden)] static __MESSAGES__: Lazy>>> = Lazy::new(Mutex::default); @@ -89,11 +108,10 @@ pub fn __set_info__(info: Information) { //static mut TEMP: i32 = 10; -/// Function to get information messages -/// +/// 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() -> Option> { +pub fn get_messages() -> Vec { //println!("{:?}", thread::current().name()); /* unsafe { @@ -109,5 +127,9 @@ pub fn get_messages() -> Option> { } */ - __MESSAGES__.lock().unwrap().remove(&thread::current().id()) + __MESSAGES__ + .lock() + .unwrap() + .remove(&thread::current().id()) + .unwrap_or_default() } diff --git a/src/main.rs b/src/main.rs index dfb19860..136ec069 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,11 +1,11 @@ #![allow(non_snake_case)] use clap::{load_yaml, App}; -use reveaal::logging::{get_messages, setup_logger}; +use reveaal::logging::setup_logger; use reveaal::System::query_failures::QueryResult; use reveaal::ProtobufServer::services::query_request::Settings; use reveaal::{ - extract_system_rep, msg, parse_queries, set_server, start_grpc_server_with_tokio, xml_parser, + extract_system_rep, parse_queries, set_server, start_grpc_server_with_tokio, xml_parser, ComponentLoader, JsonProjectLoader, ProjectLoader, Query, XmlProjectLoader, }; use std::env; From acebea05a9436ad13dc655570d1bc1cbe4cb1413 Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Thu, 18 May 2023 15:08:05 +0200 Subject: [PATCH 10/19] added server check and impl Display --- src/ModelObjects/component.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/src/ModelObjects/component.rs b/src/ModelObjects/component.rs index 18b1fc1a..92a82261 100644 --- a/src/ModelObjects/component.rs +++ b/src/ModelObjects/component.rs @@ -16,7 +16,6 @@ use crate::TransitionSystems::{CompositionType, TransitionSystem}; use crate::TransitionSystems::{LocationTree, TransitionID}; use edbm::zones::OwnedFederation; use itertools::Itertools; -use log::info; use serde::{Deserialize, Serialize}; use std::collections::{HashMap, HashSet}; use std::fmt; From 95fda460bca86835cfec61c0079eb4b2ff02016d Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Thu, 18 May 2023 15:24:53 +0200 Subject: [PATCH 11/19] Fixed test error --- src/lib.rs | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/lib.rs b/src/lib.rs index d64ac23f..af1dc294 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -34,10 +34,16 @@ pub fn set_server(is_server: bool) { } } +#[cfg(not(test))] fn is_server() -> bool { unsafe { IS_SERVER.expect("Server or CLI never specified") } } +#[cfg(test)] +fn is_server() -> bool { + false +} + #[macro_use] extern crate pest_derive; extern crate colored; From 511e3717a3dfee2c7f1073c499fcecd284ee308f Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Mon, 22 May 2023 09:42:24 +0200 Subject: [PATCH 12/19] Updated and added test --- .gitmodules | 2 +- Ecdar-ProtoBuf | 2 +- src/lib.rs | 2 +- src/logging.rs | 90 ++++++++++++++++++++++++++++---------------------- 4 files changed, 53 insertions(+), 43 deletions(-) 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/src/lib.rs b/src/lib.rs index af1dc294..ed099b29 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -41,7 +41,7 @@ fn is_server() -> bool { #[cfg(test)] fn is_server() -> bool { - false + true } #[macro_use] diff --git a/src/logging.rs b/src/logging.rs index be05d6ff..92be1e33 100644 --- a/src/logging.rs +++ b/src/logging.rs @@ -1,4 +1,4 @@ -use crate::ProtobufServer::services::query_response::Information; +use crate::ProtobufServer::services::query_response::{information, Information}; use chrono::Local; use colored::{ColoredString, Colorize}; use log::SetLoggerError; @@ -11,20 +11,18 @@ use std::sync::Mutex; use std::thread; use std::thread::ThreadId; -#[cfg(feature = "logging")] -fn colored_level(level: log::Level) -> ColoredString { - match level { - log::Level::Error => level.to_string().red(), - log::Level::Warn => level.to_string().yellow(), - log::Level::Info => level.to_string().cyan(), - log::Level::Debug => level.to_string().blue(), - log::Level::Trace => level.to_string().magenta(), - } -} - #[cfg(feature = "logging")] /// Sets up the logging pub fn setup_logger() -> Result<(), SetLoggerError> { + fn colored_level(level: log::Level) -> ColoredString { + match level { + log::Level::Error => level.to_string().red(), + log::Level::Warn => level.to_string().yellow(), + log::Level::Info => level.to_string().cyan(), + log::Level::Debug => level.to_string().blue(), + log::Level::Trace => level.to_string().magenta(), + } + } env_logger::Builder::from_env(env_logger::Env::default()) .format(|buf, record| { writeln!( @@ -62,22 +60,18 @@ macro_rules! msg { //TODO: Maybe format the information when not server ($($msg:tt)+) => (msg!(0, subject: "general", msg: format_args!($($msg)+).to_string())); } -#[doc(hidden)] -pub fn __severity__(severity: i32) -> log::Level { - match severity { - 0 => log::Level::Info, - 1 => log::Level::Warn, - _ => unreachable!(), - } -} - 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(), - colored_level(__severity__(self.serverity)), + lvl, self.subject, self.message ) @@ -90,7 +84,7 @@ static __MESSAGES__: Lazy>>> = Lazy::ne #[doc(hidden)] pub fn __as_information__(severity: i32, subject: &str, message: String) -> Information { Information { - serverity: severity, + severity, subject: subject.to_string(), message, } @@ -106,30 +100,46 @@ pub fn __set_info__(info: Information) { }; } -//static mut TEMP: i32 = 10; - /// 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 { - //println!("{:?}", thread::current().name()); - /* - unsafe { - println!("{}", TEMP); - } - thread::spawn(|| unsafe { - TEMP = 20; - println!("{}", TEMP); - }); - thread::sleep(Duration::from_millis(1000)); - unsafe { - println!("{}", TEMP); - } - */ - __MESSAGES__ .lock() .unwrap() .remove(&thread::current().id()) .unwrap_or_default() } + +#[cfg(test)] +mod tests { + use crate::logging::get_messages; + use std::thread; + use std::time::Duration; + + #[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()) + ); + } +} From b374069d62b9d633a127bccfa2a2c3aad9a4a016 Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Mon, 22 May 2023 09:48:18 +0200 Subject: [PATCH 13/19] refactor of module --- src/logging.rs | 166 ++++++++++++++++++++++++++----------------------- 1 file changed, 87 insertions(+), 79 deletions(-) diff --git a/src/logging.rs b/src/logging.rs index 92be1e33..64221995 100644 --- a/src/logging.rs +++ b/src/logging.rs @@ -1,15 +1,8 @@ -use crate::ProtobufServer::services::query_response::{information, Information}; use chrono::Local; use colored::{ColoredString, Colorize}; use log::SetLoggerError; -use once_cell::sync::Lazy; -use std::collections::hash_map::Entry; -use std::collections::HashMap; -use std::fmt::{Display, Formatter}; use std::io::Write; -use std::sync::Mutex; use std::thread; -use std::thread::ThreadId; #[cfg(feature = "logging")] /// Sets up the logging @@ -39,14 +32,14 @@ pub fn setup_logger() -> Result<(), SetLoggerError> { } #[macro_export] -macro_rules! msg { //TODO: Maybe format the information when not server +macro_rules! msg { ($severity:expr, subject: $subject:expr, msg: $msg:expr) => ({ if $crate::is_server() { - $crate::logging::__set_info__($crate::logging::__as_information__($severity, $subject, $msg)); + $crate::logging::message::__set_info__($crate::logging::message::__as_information__($severity, $subject, $msg)); } else { //let lvl = $crate::logging::__severity__($severity); //log::log!(lvl, "{}", $crate::logging::__as_information__($severity, $subject, $msg)); - println!("{}", $crate::logging::__as_information__($severity, $subject, $msg)); + println!("{}", $crate::logging::message::__as_information__($severity, $subject, $msg)); } }); @@ -60,86 +53,101 @@ macro_rules! msg { //TODO: Maybe format the information when not server ($($msg:tt)+) => (msg!(0, subject: "general", msg: format_args!($($msg)+).to_string())); } -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 - ) - } -} - -#[doc(hidden)] -static __MESSAGES__: Lazy>>> = Lazy::new(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]); - } - }; -} - /// 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 { - __MESSAGES__ +pub fn get_messages() -> Vec { + message::__MESSAGES__ .lock() .unwrap() .remove(&thread::current().id()) .unwrap_or_default() } -#[cfg(test)] -mod tests { - use crate::logging::get_messages; +#[doc(hidden)] +pub mod message { + use crate::ProtobufServer::services::query_response::{information, Information}; + use chrono::Local; + use colored::Colorize; + use once_cell::sync::Lazy; + use std::collections::hash_map::Entry; + use std::collections::HashMap; + use std::fmt::{Display, Formatter}; + use std::sync::Mutex; use std::thread; - use std::time::Duration; + 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 + ) + } + } + + #[doc(hidden)] + pub static __MESSAGES__: Lazy>>> = + Lazy::new(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 std::thread; + use std::time::Duration; - #[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()) - ); - }); + #[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()) + ); } - 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()) - ); } } From 37c8f125a6e5241276eb8a3e2dc8388e9d634ea0 Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Mon, 22 May 2023 10:16:38 +0200 Subject: [PATCH 14/19] Added into --- src/ModelObjects/component.rs | 5 +++-- src/logging.rs | 4 ++-- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/ModelObjects/component.rs b/src/ModelObjects/component.rs index 92a82261..3f75357c 100644 --- a/src/ModelObjects/component.rs +++ b/src/ModelObjects/component.rs @@ -12,6 +12,7 @@ use edbm::util::constraints::ClockIndex; use crate::msg; use crate::ModelObjects::representations::BoolExpression; +use crate::ProtobufServer::services::query_response::information; use crate::TransitionSystems::{CompositionType, TransitionSystem}; use crate::TransitionSystems::{LocationTree, TransitionID}; use edbm::zones::OwnedFederation; @@ -166,7 +167,7 @@ impl Component { ); */ - msg!("Clock Reduction", msg: "Removed Clock '{name}' (index {index}) has been removed from component {}", + msg!(information::Severity::Info, subject: "Clock Reduction", msg: "Removed Clock '{name}' (index {index}) has been removed from component {}", self.name); } @@ -195,7 +196,7 @@ impl Component { ); */ - msg!("Clock Reduction", + msg!(information::Severity::Info, subject: "Clock Reduction", msg: "Replaced Clock '{name}' (index {old}) with {global_index} in component {}", self.name ); diff --git a/src/logging.rs b/src/logging.rs index 64221995..0ab6afaf 100644 --- a/src/logging.rs +++ b/src/logging.rs @@ -35,11 +35,11 @@ pub fn setup_logger() -> Result<(), SetLoggerError> { 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, $subject, $msg)); + $crate::logging::message::__set_info__($crate::logging::message::__as_information__($severity.into(), $subject, $msg)); } else { //let lvl = $crate::logging::__severity__($severity); //log::log!(lvl, "{}", $crate::logging::__as_information__($severity, $subject, $msg)); - println!("{}", $crate::logging::message::__as_information__($severity, $subject, $msg)); + println!("{}", $crate::logging::message::__as_information__($severity.into(), $subject, $msg)); } }); From 225a06044b199d3e0039e3ac014dfb7cf76eba22 Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Mon, 22 May 2023 10:39:22 +0200 Subject: [PATCH 15/19] Removed commented code --- src/ModelObjects/component.rs | 14 -------------- 1 file changed, 14 deletions(-) diff --git a/src/ModelObjects/component.rs b/src/ModelObjects/component.rs index 3f75357c..d7d57a4b 100644 --- a/src/ModelObjects/component.rs +++ b/src/ModelObjects/component.rs @@ -160,13 +160,6 @@ impl Component { .is_none() }); - /* - info!( - "Removed Clock '{name}' (index {index}) has been removed from component {}", - self.name - ); - */ - msg!(information::Severity::Info, subject: "Clock Reduction", msg: "Removed Clock '{name}' (index {index}) has been removed from component {}", self.name); } @@ -189,13 +182,6 @@ 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 {}", - self.name - ); - */ - msg!(information::Severity::Info, subject: "Clock Reduction", msg: "Replaced Clock '{name}' (index {old}) with {global_index} in component {}", self.name From a611bca7f9751e03d7d11d418197b0aaa0b39cc5 Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Mon, 22 May 2023 12:47:58 +0200 Subject: [PATCH 16/19] Changed to use lazy_static --- Cargo.toml | 2 +- src/lib.rs | 1 + src/logging.rs | 8 +++----- 3 files changed, 5 insertions(+), 6 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index 11421209..c55d98bc 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -45,7 +45,7 @@ lru = "0.8.1" itertools = "0.10.5" regex = "1" rayon = "1.6.1" -once_cell = "1.17.1" +lazy_static = "1.4.0" # Enable optimizations for EDBM in debug mode, but not for our code: [profile.dev.package.edbm] diff --git a/src/lib.rs b/src/lib.rs index ed099b29..32a9505f 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -48,6 +48,7 @@ fn is_server() -> bool { extern crate pest_derive; extern crate colored; extern crate core; +extern crate lazy_static; extern crate serde; extern crate serde_xml_rs; extern crate simple_error; diff --git a/src/logging.rs b/src/logging.rs index 0ab6afaf..699f012b 100644 --- a/src/logging.rs +++ b/src/logging.rs @@ -69,7 +69,6 @@ pub mod message { use crate::ProtobufServer::services::query_response::{information, Information}; use chrono::Local; use colored::Colorize; - use once_cell::sync::Lazy; use std::collections::hash_map::Entry; use std::collections::HashMap; use std::fmt::{Display, Formatter}; @@ -95,10 +94,9 @@ pub mod message { } } - #[doc(hidden)] - pub static __MESSAGES__: Lazy>>> = - Lazy::new(Mutex::default); - + lazy_static! { + pub static ref __MESSAGES__: Mutex>> = Mutex::default(); + } #[doc(hidden)] pub fn __as_information__(severity: i32, subject: &str, message: String) -> Information { Information { From a7a7cd804bd7f68ebdd26baf9222a8b93c557588 Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Mon, 22 May 2023 12:48:30 +0200 Subject: [PATCH 17/19] Changed to use lazy_static --- src/lib.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/lib.rs b/src/lib.rs index 32a9505f..82ecf592 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -48,8 +48,9 @@ fn is_server() -> bool { extern crate pest_derive; extern crate colored; extern crate core; -extern crate lazy_static; extern crate serde; extern crate serde_xml_rs; extern crate simple_error; extern crate xml; +#[macro_use] +extern crate lazy_static; From 7b8891181941072aed693851994bf404a7d0eb14 Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Thu, 25 May 2023 14:08:34 +0200 Subject: [PATCH 18/19] refactored removal of invariants --- .gitmodules | 2 +- Ecdar-ProtoBuf | 2 +- samples/xml/ConsTests.xml | 2 +- src/ModelObjects/component.rs | 11 +++++------ 4 files changed, 8 insertions(+), 9 deletions(-) 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/ModelObjects/component.rs b/src/ModelObjects/component.rs index 77e5f120..676a25c2 100644 --- a/src/ModelObjects/component.rs +++ b/src/ModelObjects/component.rs @@ -208,12 +208,11 @@ impl Component { // 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.retain(|l| { - l.invariant - .as_ref() - .filter(|i| i.has_varname(&name)) - .is_none() - }); + self.locations + .iter_mut() + .filter_map(|l| l.invariant.as_mut()) + .filter(|i| i.has_varname(&name)) + .for_each(|i| *i = BoolExpression::Bool(false)); info!( "Removed Clock '{name}' (index {index}) has been removed from component {}", From f5d1eb6c63064ecb4339f3602d0dd2a9c36e23fd Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Fri, 26 May 2023 10:32:44 +0200 Subject: [PATCH 19/19] Added macro tests --- src/logging.rs | 36 +++++++++++++++++++++++++++++++----- 1 file changed, 31 insertions(+), 5 deletions(-) diff --git a/src/logging.rs b/src/logging.rs index 699f012b..85ba7657 100644 --- a/src/logging.rs +++ b/src/logging.rs @@ -35,22 +35,22 @@ pub fn setup_logger() -> Result<(), SetLoggerError> { 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)); + $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)); + 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)); + ($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())); + ($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. @@ -119,9 +119,35 @@ pub mod message { #[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());