Skip to content

Commit

Permalink
fixed imports and exceptions
Browse files Browse the repository at this point in the history
fixed bugs for remove_clock_from_federation
refactored declarations in component.rs to declarations.rs
added set_dim() for TransitionSystem
fixed a lot of bugs regarding the remove_clocks
removed stale remove_clock methods from component.rs
  • Loading branch information
Aavild committed Nov 21, 2023
1 parent 646137c commit 6d4251a
Show file tree
Hide file tree
Showing 32 changed files with 286 additions and 361 deletions.
3 changes: 2 additions & 1 deletion src/data_reader/parse_edge.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,8 @@ use crate::transition_systems::compiled_update::CompiledUpdate;

use crate::model_objects::expressions::{ArithExpression, BoolExpression};

use crate::{data_reader::serialization::encode_arithexpr, model_objects::Declarations};
use crate::data_reader::serialization::encode_arithexpr;
use crate::model_objects::declarations::Declarations;
use edbm::util::constraints::ClockIndex;
use pest::pratt_parser::{Assoc, Op, PrattParser};
use pest::Parser;
Expand Down
3 changes: 2 additions & 1 deletion src/data_reader/proto_reader.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,8 @@ use std::convert::TryInto;
use edbm::util::constraints::{Conjunction, Constraint, Disjunction, Inequality, RawInequality};
use edbm::zones::OwnedFederation;

use crate::model_objects::{Component, Decision, Declarations, State};
use crate::model_objects::declarations::Declarations;
use crate::model_objects::{Component, Decision, State};
use crate::protobuf_server::services::{
clock::Clock as ClockEnum, Clock as ProtoClock, ComponentsInfo, Constraint as ProtoConstraint,
Decision as ProtoDecision, Disjunction as ProtoDisjunction, LocationTree as ProtoLocationTree,
Expand Down
3 changes: 2 additions & 1 deletion src/data_reader/serialization.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
use crate::data_reader::parse_edge;
use crate::model_objects::declarations::Declarations;
use crate::model_objects::expressions;
use crate::model_objects::{Component, Declarations, Edge, Location, LocationType, SyncType};
use crate::model_objects::{Component, Edge, Location, LocationType, SyncType};
use crate::simulation::graph_layout::layout_dummy_component;
use edbm::util::constraints::ClockIndex;
use serde::{Deserialize, Deserializer, Serialize, Serializer};
Expand Down
3 changes: 2 additions & 1 deletion src/data_reader/xml_parser.rs
Original file line number Diff line number Diff line change
@@ -1,7 +1,8 @@
use crate::data_reader::parse_edge;
use crate::data_reader::parse_edge::Update;
use crate::model_objects::declarations::Declarations;
use crate::model_objects::{
Component, Declarations, Edge, Location, LocationType, Query, SyncType, SystemDeclarations,
Component, Edge, Location, LocationType, Query, SyncType, SystemDeclarations,
SystemSpecification,
};
use edbm::util::constraints::ClockIndex;
Expand Down
4 changes: 2 additions & 2 deletions src/edge_eval/constraint_applier.rs
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
use crate::model_objects::declarations::Declarations;
use edbm::util::constraints::{ClockIndex, Inequality};
use edbm::zones::OwnedFederation;

use crate::model_objects::expressions::{ArithExpression, BoolExpression, Clock};
use crate::model_objects::Declarations;

pub fn apply_constraints_to_state(
guard: &BoolExpression,
Expand Down Expand Up @@ -271,8 +271,8 @@ fn get_clock_val(
#[cfg(test)]
mod test {
use super::get_indices;
use crate::model_objects::declarations::Declarations;
use crate::model_objects::expressions::ArithExpression;
use crate::model_objects::Declarations;
use std::collections::HashMap;

#[test]
Expand Down
116 changes: 1 addition & 115 deletions src/model_objects/component.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,12 +3,10 @@ use crate::data_reader::serialization::{decode_declarations, DummyComponent};
use edbm::util::bounds::Bounds;
use edbm::util::constraints::ClockIndex;

use crate::model_objects::expressions::BoolExpression;
use crate::model_objects::declarations::{DeclarationProvider, Declarations};
use crate::model_objects::{Edge, Location, SyncType};
use itertools::Itertools;
use log::info;
use serde::{Deserialize, Serialize};
use std::collections::{HashMap, HashSet};
use std::iter::FromIterator;

/// The basic struct used to represent components read from either Json or xml
Expand Down Expand Up @@ -106,116 +104,4 @@ impl Component {
edge.id = format!("E{}", index);
}
}

/// Removes unused clock
/// # Arguments
/// `index`: The index to be removed
pub(crate) fn remove_clock(&mut self, index: ClockIndex) {
// Removes from declarations, and updates the other
let name = self
.declarations
.get_clock_name_by_index(index)
.expect("Couldn't find clock with index")
.to_owned();
self.declarations.clocks.remove(&name);

// Removes from from updates and guards
self.edges
.iter_mut()
.filter(|e| e.update.is_some() || e.guard.is_some())
.for_each(|e| {
// The guard is overwritten to `false`. This can be done since we assume
// that all edges with guards involving the given clock is not reachable
// in some composite system.
if let Some(guard) = e.guard.as_mut().filter(|g| g.has_varname(&name)) {
*guard = BoolExpression::Bool(false);
}
if let Some(inv) = e.update.as_mut() {
inv.retain(|u| u.variable != name);
}
});

// Removes from from location invariants
// The invariants containing the clock are overwritten to `false`.
// This can be done since we assume that all locations with invariants involving
// the given clock is not reachable in some composite system.
self.locations
.iter_mut()
.filter_map(|l| l.invariant.as_mut())
.filter(|i| i.has_varname(&name))
.for_each(|i| *i = BoolExpression::Bool(false));

info!(
"Removed Clock '{name}' (index {index}) has been removed from component {}",
self.name
); // Should be changed in the future to be the information logger
}

/// Replaces duplicate clock with a new
/// # Arguments
/// `global_index`: The index of the global clock\n
/// `indices` are the duplicate clocks that should be set to `global_index`
pub(crate) fn replace_clock(
&mut self,
global_index: ClockIndex,
indices: &HashSet<ClockIndex>,
) {
for (name, index) in self
.declarations
.clocks
.iter_mut()
.filter(|(_, c)| indices.contains(c))
{
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
}
}
}

pub trait DeclarationProvider {
fn get_declarations(&self) -> &Declarations;
}

/// The declaration struct is used to hold the indices for each clock, and is meant to be the owner of int variables once implemented
#[derive(Debug, Deserialize, Clone, PartialEq, Eq, Serialize)]
pub struct Declarations {
pub ints: HashMap<String, i32>,
pub clocks: HashMap<String, ClockIndex>,
}

impl Declarations {
pub fn empty() -> Declarations {
Declarations {
ints: HashMap::new(),
clocks: HashMap::new(),
}
}

pub fn get_clock_count(&self) -> usize {
self.clocks.len()
}

pub fn set_clock_indices(&mut self, start_index: ClockIndex) {
for (_, v) in self.clocks.iter_mut() {
*v += start_index
}
}

pub fn get_clock_index_by_name(&self, name: &str) -> Option<&ClockIndex> {
self.clocks.get(name)
}

/// Gets the name of a given `ClockIndex`.
/// Returns `None` if it does not exist in the declarations
pub fn get_clock_name_by_index(&self, index: ClockIndex) -> Option<&String> {
self.clocks
.iter()
.find(|(_, v)| **v == index)
.map(|(k, _)| k)
}
}
61 changes: 61 additions & 0 deletions src/model_objects/declarations.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,61 @@
use edbm::util::constraints::ClockIndex;
use serde::{Deserialize, Serialize};
use std::collections::HashMap;

/// The declaration struct is used to hold the indices for each clock, and is meant to be the owner of int variables once implemented
#[derive(Debug, Deserialize, Clone, PartialEq, Eq, Serialize)]
pub struct Declarations {
pub ints: HashMap<String, i32>,
pub clocks: HashMap<String, ClockIndex>,
}

pub trait DeclarationProvider {
fn get_declarations(&self) -> &Declarations;
}

impl Declarations {
pub fn empty() -> Declarations {
Declarations {
ints: HashMap::new(),
clocks: HashMap::new(),
}
}

pub fn get_clock_count(&self) -> usize {
self.clocks.len()
}

pub fn set_clock_indices(&mut self, start_index: ClockIndex) {
for (_, v) in self.clocks.iter_mut() {
*v += start_index
}
}

pub fn get_clock_index_by_name(&self, name: &str) -> Option<&ClockIndex> {
self.clocks.get(name)
}

/// Gets the name of a given `ClockIndex`.
/// Returns `None` if it does not exist in the declarations
pub fn get_clock_name_by_index(&self, index: ClockIndex) -> Option<&String> {
self.clocks
.iter()
.find(|(_, v)| **v == index)
.map(|(k, _)| k)
}
pub fn remove_clocks(&mut self, clocks_to_be_removed: &Vec<ClockIndex>) {

Check failure on line 46 in src/model_objects/declarations.rs

View workflow job for this annotation

GitHub Actions / Clippy lint and check

writing `&Vec` instead of `&[_]` involves a new object where a slice will do

error: writing `&Vec` instead of `&[_]` involves a new object where a slice will do --> src/model_objects/declarations.rs:46:59 | 46 | pub fn remove_clocks(&mut self, clocks_to_be_removed: &Vec<ClockIndex>) { | ^^^^^^^^^^^^^^^^ help: change this to: `&[ClockIndex]` | = help: for further information visit https://rust-lang.github.io/rust-clippy/master/index.html#ptr_arg = note: `-D clippy::ptr-arg` implied by `-D warnings` = help: to override `-D warnings` add `#[allow(clippy::ptr_arg)]`
let mut clock_count = *self.clocks.values().next().unwrap_or(&(1usize));
let mut new_clocks: HashMap<String, ClockIndex> = HashMap::new();

for (name, _) in self
.clocks
.iter()
.filter(|(_, c)| !clocks_to_be_removed.contains(c))
{
new_clocks.insert(name.clone(), clock_count);
clock_count += 1;
}

self.clocks = new_clocks;
}
}
2 changes: 1 addition & 1 deletion src/model_objects/edge.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ use crate::data_reader::serialization::{
decode_guard, decode_sync, decode_sync_type, decode_update, DummyEdge,
};
use crate::edge_eval::constraint_applier::apply_constraints_to_state;
use crate::model_objects::declarations::Declarations;
use crate::model_objects::expressions::BoolExpression;
use crate::model_objects::Declarations;
use edbm::zones::OwnedFederation;
use serde::{Deserialize, Serialize};
use std::fmt;
Expand Down
1 change: 1 addition & 0 deletions src/model_objects/mod.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
mod component;
mod decision;
pub mod declarations;
mod edge;
pub mod expressions;
mod location;
Expand Down
3 changes: 2 additions & 1 deletion src/model_objects/transition.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
use crate::data_reader::parse_edge;
use crate::model_objects::declarations::DeclarationProvider;
use crate::model_objects::expressions::BoolExpression;
use crate::model_objects::{Component, DeclarationProvider, Edge, State};
use crate::model_objects::{Component, Edge, State};
use crate::transition_systems::compiled_update::CompiledUpdate;
use crate::transition_systems::{CompositionType, LocationTree, TransitionID};
use edbm::util::constraints::ClockIndex;
Expand Down
3 changes: 2 additions & 1 deletion src/system/extract_state.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,9 @@ use itertools::Itertools;

use crate::edge_eval::constraint_applier::apply_constraints_to_state;
use crate::extract_system_rep::SystemRecipe;
use crate::model_objects::declarations::Declarations;
use crate::model_objects::expressions::{BoolExpression, ComponentVariable, StateExpression};
use crate::model_objects::{Declarations, State};
use crate::model_objects::State;
use crate::transition_systems::{CompositionType, LocationID, LocationTree, TransitionSystemPtr};

/// This function takes a [`StateExpression`], the system recipe, and the transitionsystem -
Expand Down
Loading

0 comments on commit 6d4251a

Please sign in to comment.