upd system

src/data_reader/component_loader.rs

@@ -29,16 +29,6 @@ pub struct ModelCache {
     cache: Arc<Mutex<LruCache<i32, ComponentTuple>>>,
 }
 
-impl Default for ModelCache {
-    fn default() -> Self {
-        Self {
-            cache: Arc::new(Mutex::new(LruCache::<i32, ComponentTuple>::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::<i32, ComponentTuple>::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);

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<Component> = proto_components
-                .iter()
-                .flat_map(parse_components_if_some)
-                .flatten()
-                .collect::<Vec<Component>>();
-            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<Component> = proto_components
+                    .iter()
+                    .flat_map(parse_components_if_some)
+                    .flatten()
+                    .collect::<Vec<Component>>();
+                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<Component> = proto_components
-        .iter()
-        .flat_map(parse_components_if_some)
-        .flatten()
-        .collect::<Vec<Component>>();
-    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<Component> = proto_components
+            .iter()
+            .flat_map(parse_components_if_some)
+            .flatten()
+            .collect::<Vec<Component>>();
+        let components = construct_components(parsed_components);
+        self.insert_model(user_id, components_hash, Arc::new(components))
+    }
 }
 
-fn constrtuct_componentsmap(
+fn construct_components(
     components: Vec<Component>,
 ) -> crate::data_reader::component_loader::ComponentsMap {
     let mut comp_hashmap = HashMap::<String, Component>::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)
 }

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<Query, Status> {
-    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(

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);

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<Update>, 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

src/system/query_failures.rs

@@ -305,8 +305,8 @@ impl ActionFailure {
     }
 
     /// Creates a new [Result]<T, [ActionFailure]> that failed because the actions in `inputs` are not a disjoint from the actions in `outputs`.
-    pub fn not_disjoint_io(
-        name: impl Into<String>,
+    pub fn not_disjoint_io<T: Into<String>>(
+        name: T,
         inputs: HashSet<String>,
         outputs: HashSet<String>,
     ) -> Result<(), Box<ActionFailure>> {

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;
     }
 

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,