From 12e00e8c00bfd46776ecee566de938fcf77e6d15 Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Mon, 12 Feb 2024 15:29:52 +0100 Subject: [PATCH] upd system --- src/data_reader/component_loader.rs | 20 +++--- .../ecdar_requests/request_util.rs | 66 ++++++++++--------- .../ecdar_requests/send_query.rs | 14 ++-- src/system/input_enabler.rs | 15 ++--- src/system/pruning.rs | 56 +++++----------- src/system/query_failures.rs | 4 +- src/system/refine.rs | 2 +- src/system/specifics.rs | 4 +- 8 files changed, 78 insertions(+), 103 deletions(-) diff --git a/src/data_reader/component_loader.rs b/src/data_reader/component_loader.rs index 0bb4ed18..65ed71ab 100644 --- a/src/data_reader/component_loader.rs +++ b/src/data_reader/component_loader.rs @@ -29,16 +29,6 @@ pub struct ModelCache { cache: Arc>>, } -impl Default for ModelCache { - fn default() -> Self { - Self { - cache: Arc::new(Mutex::new(LruCache::::new( - NonZeroUsize::new(100).unwrap(), - ))), - } - } -} - impl ModelCache { /// A Method that creates a new cache with a given size limit. /// @@ -108,6 +98,16 @@ impl ModelCache { } } +impl Default for ModelCache { + fn default() -> Self { + Self { + cache: Arc::new(Mutex::new(LruCache::::new( + NonZeroUsize::new(100).unwrap(), + ))), + } + } +} + pub trait ComponentLoader { fn get_component(&mut self, component_name: &str) -> Result<&Component, SyntaxResult>; fn save_component(&mut self, component: Component); diff --git a/src/protobuf_server/ecdar_requests/request_util.rs b/src/protobuf_server/ecdar_requests/request_util.rs index 61f4147a..11e644ea 100644 --- a/src/protobuf_server/ecdar_requests/request_util.rs +++ b/src/protobuf_server/ecdar_requests/request_util.rs @@ -12,42 +12,44 @@ use crate::{ }, }; -pub fn get_or_insert_model( - model_cache: &mut ModelCache, - user_id: i32, - components_hash: u32, - proto_components: &[ProtoComponent], -) -> ComponentContainer { - match model_cache.get_model(user_id, components_hash) { - Some(model) => model, - None => { - let parsed_components: Vec = proto_components - .iter() - .flat_map(parse_components_if_some) - .flatten() - .collect::>(); - let components = constrtuct_componentsmap(parsed_components); - model_cache.insert_model(user_id, components_hash, Arc::new(components)) +impl ModelCache { + pub fn get_or_insert_model( + &mut self, + user_id: i32, + components_hash: u32, + proto_components: &[ProtoComponent], + ) -> ComponentContainer { + match self.get_model(user_id, components_hash) { + Some(model) => model, + None => { + let parsed_components: Vec = proto_components + .iter() + .flat_map(parse_components_if_some) + .flatten() + .collect::>(); + let components = construct_components(parsed_components); + self.insert_model(user_id, components_hash, Arc::new(components)) + } } } -} -pub fn insert_model( - model_cache: &mut ModelCache, - user_id: i32, - components_hash: u32, - proto_components: &[ProtoComponent], -) -> ComponentContainer { - let parsed_components: Vec = proto_components - .iter() - .flat_map(parse_components_if_some) - .flatten() - .collect::>(); - let components = constrtuct_componentsmap(parsed_components); - model_cache.insert_model(user_id, components_hash, Arc::new(components)) + pub fn insert_proto_model( + &mut self, + user_id: i32, + components_hash: u32, + proto_components: &[ProtoComponent], + ) -> ComponentContainer { + let parsed_components: Vec = proto_components + .iter() + .flat_map(parse_components_if_some) + .flatten() + .collect::>(); + let components = construct_components(parsed_components); + self.insert_model(user_id, components_hash, Arc::new(components)) + } } -fn constrtuct_componentsmap( +fn construct_components( components: Vec, ) -> crate::data_reader::component_loader::ComponentsMap { let mut comp_hashmap = HashMap::::new(); @@ -76,7 +78,7 @@ pub fn simulation_info_to_transition_system( let user_id = simulation_info.user_id; let mut component_container = - get_or_insert_model(model_cache, user_id, info.components_hash, &info.components); + model_cache.get_or_insert_model(user_id, info.components_hash, &info.components); component_loader_to_transition_system(&mut component_container, &composition) } diff --git a/src/protobuf_server/ecdar_requests/send_query.rs b/src/protobuf_server/ecdar_requests/send_query.rs index 58f4dca1..6ac026e0 100644 --- a/src/protobuf_server/ecdar_requests/send_query.rs +++ b/src/protobuf_server/ecdar_requests/send_query.rs @@ -1,9 +1,7 @@ use crate::data_reader::component_loader::{ComponentContainer, ModelCache}; use crate::data_reader::json_writer::component_to_json; -use crate::data_reader::parse_queries; -use crate::extract_system_rep::ExecutableQueryError; +use crate::extract_system_rep::{create_executable_query, ExecutableQueryError}; use crate::model_objects::Query; -use crate::protobuf_server::ecdar_requests::request_util::insert_model; use crate::protobuf_server::services::component::Rep; use crate::protobuf_server::services::query_response::{ Error as InnerError, Result as ProtobufResult, Success, @@ -17,8 +15,7 @@ use crate::system::query_failures::{ SyntaxFailure, SystemRecipeFailure, }; -use crate::system::extract_system_rep; - +use crate::parse_queries::parse_to_query; use log::trace; use tonic::Status; @@ -45,8 +42,7 @@ impl ConcreteEcdarBackend { } // Model not in cache but included in request else if !proto_components.is_empty() { - let model = insert_model( - &mut model_cache, + let model = model_cache.insert_proto_model( query_request.user_id, components_info.components_hash, proto_components, @@ -74,7 +70,7 @@ fn send_query( model.set_settings(query_request.settings.unwrap_or(crate::DEFAULT_SETTINGS)); - match extract_system_rep::create_executable_query(&query, &mut model) { + match create_executable_query(&query, &mut model) { Ok(query) => { let result = query.execute(); Ok(QueryResponse { @@ -98,7 +94,7 @@ fn send_query( } fn parse_query(query_request: &QueryRequest) -> Result { - let mut queries = parse_queries::parse_to_query(&query_request.query); + let mut queries = parse_to_query(&query_request.query); if queries.len() != 1 { Err(Status::invalid_argument( diff --git a/src/system/input_enabler.rs b/src/system/input_enabler.rs index f5e74071..80bc8684 100644 --- a/src/system/input_enabler.rs +++ b/src/system/input_enabler.rs @@ -1,6 +1,6 @@ use edbm::zones::OwnedFederation; -use crate::edge_eval::constraint_applier; +use crate::edge_eval::constraint_applier::apply_constraints_to_state; use crate::model_objects::expressions::BoolExpression; use crate::model_objects::DeclarationProvider; use crate::model_objects::{Component, Edge, SyncType}; @@ -16,7 +16,7 @@ pub fn make_input_enabled(component: &mut Component, inputs: &[String]) { let mut location_inv_zone = OwnedFederation::universe(dimension); if let Some(invariant) = &location.invariant { - location_inv_zone = constraint_applier::apply_constraints_to_state( + location_inv_zone = apply_constraints_to_state( invariant, component.get_declarations(), location_inv_zone, @@ -42,7 +42,7 @@ pub fn make_input_enabled(component: &mut Component, inputs: &[String]) { .get_location_by_name(edge.target_location.as_str()) .invariant { - guard_zone = constraint_applier::apply_constraints_to_state( + guard_zone = apply_constraints_to_state( target_invariant, component.get_declarations(), guard_zone, @@ -59,12 +59,9 @@ pub fn make_input_enabled(component: &mut Component, inputs: &[String]) { } if let Some(guard) = &edge.guard { - guard_zone = constraint_applier::apply_constraints_to_state( - guard, - component.get_declarations(), - guard_zone, - ) - .unwrap(); + guard_zone = + apply_constraints_to_state(guard, component.get_declarations(), guard_zone) + .unwrap(); } zones_federation += guard_zone.intersection(&location_inv_zone); diff --git a/src/system/pruning.rs b/src/system/pruning.rs index d80bda1d..48e7c30a 100644 --- a/src/system/pruning.rs +++ b/src/system/pruning.rs @@ -2,6 +2,7 @@ use edbm::util::constraints::ClockIndex; use edbm::zones::OwnedFederation; use log::{debug, trace}; +use crate::data_reader::parse_edge::Update; use crate::edge_eval::constraint_applier::apply_constraints_to_state; use crate::model_objects::expressions::BoolExpression; use crate::model_objects::DeclarationProvider; @@ -223,6 +224,20 @@ fn handle_input(edge: &Edge, context: &mut PruneContext) { remove_transition_if_unsat(edge, context); } +fn handle_updates(updates: &Vec, edge_fed: &mut OwnedFederation, decls: &Declarations) { + // TODO: this is different from J-ecdar + for update in updates { + *edge_fed = update.compiled(decls).apply_as_guard(edge_fed.clone()); + } + + // apply updates as free + if !edge_fed.is_empty() { + for update in updates { + *edge_fed = update.compiled(decls).apply_as_free(edge_fed.clone()); + } + } +} + fn remove_transition_if_unsat(edge: &Edge, context: &mut PruneContext) { let mut edge_fed = OwnedFederation::universe(context.dim); // apply target invariant @@ -238,16 +253,7 @@ fn remove_transition_if_unsat(edge: &Edge, context: &mut PruneContext) { 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); - } - - // apply updates as free - if !edge_fed.is_empty() { - for update in updates { - edge_fed = update.compiled(context.decl()).apply_as_free(edge_fed); - } - } + handle_updates(updates, &mut edge_fed, context.decl()); } // Apply guards @@ -395,22 +401,7 @@ fn handle_output(edge: &Edge, context: &mut PruneContext) { // Partially inconsistent target let mut incons_after_reset = target_incons.clone(); if let Some(updates) = &edge.update { - // TODO: this is different from J-ecdar - // apply updates as guard - for update in updates { - incons_after_reset = update - .compiled(context.decl()) - .apply_as_guard(incons_after_reset); - } - - // apply updates as free - if !incons_after_reset.is_empty() { - for update in updates { - incons_after_reset = update - .compiled(context.decl()) - .apply_as_free(incons_after_reset); - } - } + handle_updates(updates, &mut incons_after_reset, context.decl()); } let mut guard_fed = OwnedFederation::universe(context.dim); // Apply guards @@ -456,18 +447,7 @@ fn handle_output(edge: &Edge, context: &mut PruneContext) { } if let Some(updates) = &other_edge.update { - // TODO: this is different from J-ecdar - // apply updates as guard - for update in updates { - good_part = update.compiled(context.decl()).apply_as_guard(good_part); - } - - // apply updates as free - if !good_part.is_empty() { - for update in updates { - good_part = update.compiled(context.decl()).apply_as_free(good_part); - } - } + handle_updates(updates, &mut good_part, context.decl()); } // Apply guards diff --git a/src/system/query_failures.rs b/src/system/query_failures.rs index 03f28db7..c5c7cb0f 100644 --- a/src/system/query_failures.rs +++ b/src/system/query_failures.rs @@ -305,8 +305,8 @@ impl ActionFailure { } /// Creates a new [Result] that failed because the actions in `inputs` are not a disjoint from the actions in `outputs`. - pub fn not_disjoint_io( - name: impl Into, + pub fn not_disjoint_io>( + name: T, inputs: HashSet, outputs: HashSet, ) -> Result<(), Box> { diff --git a/src/system/refine.rs b/src/system/refine.rs index c8152631..5e70aaf5 100644 --- a/src/system/refine.rs +++ b/src/system/refine.rs @@ -389,7 +389,7 @@ fn build_state_pair( let t_invariant = new_sp_zone.clone().down(); // Check if the invariant of T (right) cuts delay solutions from S (left) and if so, report failure - if !(s_invariant.subset_eq(&t_invariant)) { + if !s_invariant.subset_eq(&t_invariant) { return BuildResult::Failure; } diff --git a/src/system/specifics.rs b/src/system/specifics.rs index 378348b9..1d95638c 100644 --- a/src/system/specifics.rs +++ b/src/system/specifics.rs @@ -217,7 +217,7 @@ pub struct SpecificState { pub constraints: SpecificDisjunction, } -/// Intermediate representation of a [LocationID](crate::transition_systems::location_id::LocationID) in a system. +/// Intermediate representation of a [LocationID](LocationID) in a system. /// It is a binary tree with either [component](SpecificComp) locations or [special](SpecialLocation) locations at the leaves. #[derive(Clone, Debug, PartialEq, Eq, Hash)] pub enum SpecificLocation { @@ -269,7 +269,7 @@ impl fmt::Display for SpecificLocation { } } -/// Intermediate representation of a [special](crate::transition_systems::location_id::LocationID::Special) location. E.g. `Error` or `Universal` from a quotient. +/// Intermediate representation of a [special](LocationID::Special) location. E.g. `Error` or `Universal` from a quotient. #[derive(Clone, Debug, PartialEq, Eq, Hash)] pub enum SpecialLocation { Universal,