From 194cc6b059438dd2bb9493f62de5d16ad1ed4bf7 Mon Sep 17 00:00:00 2001 From: Simon Rask Date: Fri, 17 Nov 2023 14:58:40 +0100 Subject: [PATCH 1/6] Use `Rc` for zones in `StatePair` --- src/model_objects/statepair.rs | 57 ++++++++++++++++++++--------- src/model_objects/statepair_list.rs | 31 +++++++++------- src/system/refine.rs | 41 ++++++--------------- 3 files changed, 68 insertions(+), 61 deletions(-) diff --git a/src/model_objects/statepair.rs b/src/model_objects/statepair.rs index f8e15dbf..9c0bc997 100644 --- a/src/model_objects/statepair.rs +++ b/src/model_objects/statepair.rs @@ -1,14 +1,16 @@ use edbm::zones::OwnedFederation; use crate::transition_systems::{LocationTree, TransitionSystemPtr}; -use std::fmt::{Display, Formatter}; +use std::{ + fmt::{Display, Formatter}, + rc::Rc, +}; #[derive(Clone, Debug)] pub struct StatePair { pub locations1: LocationTree, pub locations2: LocationTree, - /// The sentinel (Option) allows us to take ownership of the internal fed from a mutable reference - zone_sentinel: Option, + zone: Rc, } impl StatePair { @@ -17,12 +19,27 @@ impl StatePair { locations1: LocationTree, locations2: LocationTree, ) -> StatePair { - let zone = OwnedFederation::init(dimensions); + let mut zone = OwnedFederation::init(dimensions); + zone = locations1.apply_invariants(zone); + zone = locations2.apply_invariants(zone); + + StatePair { + locations1, + locations2, + zone: Rc::new(zone), + } + } + + pub fn new( + locations1: LocationTree, + locations2: LocationTree, + zone: Rc, + ) -> Self { StatePair { locations1, locations2, - zone_sentinel: Some(zone), + zone, } } @@ -35,7 +52,10 @@ impl StatePair { } //Used to allow borrowing both states as mutable - pub fn get_mut_states(&mut self, is_states1: bool) -> (&mut LocationTree, &mut LocationTree) { + pub fn get_mut_locations( + &mut self, + is_states1: bool, + ) -> (&mut LocationTree, &mut LocationTree) { if is_states1 { (&mut self.locations1, &mut self.locations2) } else { @@ -52,30 +72,31 @@ impl StatePair { } pub fn clone_zone(&self) -> OwnedFederation { - self.ref_zone().clone() + self.zone.as_ref().clone() } pub fn ref_zone(&self) -> &OwnedFederation { - self.zone_sentinel.as_ref().unwrap() - } - - pub fn take_zone(&mut self) -> OwnedFederation { - self.zone_sentinel.take().unwrap() + self.zone.as_ref() } - pub fn set_zone(&mut self, zone: OwnedFederation) { - self.zone_sentinel = Some(zone); + pub fn get_zone(&self) -> Rc { + Rc::clone(&self.zone) } pub fn extrapolate_max_bounds( - &mut self, + self, sys1: &TransitionSystemPtr, sys2: &TransitionSystemPtr, - ) { + ) -> Self { let mut bounds = sys1.get_local_max_bounds(&self.locations1); bounds.add_bounds(&sys2.get_local_max_bounds(&self.locations2)); - let zone = self.take_zone().extrapolate_max_bounds(&bounds); - self.set_zone(zone); + let zone = self.clone_zone().extrapolate_max_bounds(&bounds); + + StatePair { + locations1: self.locations1, + locations2: self.locations2, + zone: Rc::new(zone), + } } } diff --git a/src/model_objects/statepair_list.rs b/src/model_objects/statepair_list.rs index 99efd558..51c2b2c0 100644 --- a/src/model_objects/statepair_list.rs +++ b/src/model_objects/statepair_list.rs @@ -1,17 +1,20 @@ -use std::collections::{HashMap, VecDeque}; +use std::{ + collections::{HashMap, VecDeque}, + rc::Rc, +}; use edbm::zones::OwnedFederation; use crate::{model_objects::StatePair, transition_systems::LocationID}; pub type PassedStateList = PassedStateListFed; -type PassedStateListFed = HashMap<(LocationID, LocationID), OwnedFederation>; -type PassedStateListVec = HashMap<(LocationID, LocationID), Vec>; +type PassedStateListFed = HashMap<(LocationID, LocationID), Rc>; +type PassedStateListVec = HashMap<(LocationID, LocationID), Vec>>; pub type WaitingStateList = DepthFirstWaitingStateList; pub struct DepthFirstWaitingStateList { queue: VecDeque, - map: HashMap<(LocationID, LocationID), VecDeque>, + map: HashMap<(LocationID, LocationID), VecDeque>>, } pub trait PassedStateListExt { @@ -21,8 +24,8 @@ pub trait PassedStateListExt { } impl PassedStateListExt for PassedStateListVec { - fn put(&mut self, mut pair: StatePair) { - let fed = pair.take_zone(); + fn put(&mut self, pair: StatePair) { + let fed = pair.get_zone(); let (loc1, loc2) = (pair.locations1.id, pair.locations2.id); let key = (loc1, loc2); if let Some(vec) = self.get_mut(&key) { @@ -47,16 +50,16 @@ impl PassedStateListExt for PassedStateListVec { fn zones(&self, key: &(LocationID, LocationID)) -> Vec<&OwnedFederation> { match self.get(key) { - Some(vec) => vec.iter().collect(), + Some(vec) => vec.iter().map(AsRef::as_ref).collect(), None => panic!("No zones for key: {:?}", key), } } } impl PassedStateListExt for DepthFirstWaitingStateList { - fn put(&mut self, mut pair: StatePair) { + fn put(&mut self, pair: StatePair) { self.queue.push_front(pair.clone()); - let fed = pair.take_zone(); + let fed = pair.get_zone(); let (loc1, loc2) = (pair.locations1.id, pair.locations2.id); let key = (loc1, loc2); if let Some(vec) = self.map.get_mut(&key) { @@ -79,7 +82,7 @@ impl PassedStateListExt for DepthFirstWaitingStateList { } fn zones(&self, key: &(LocationID, LocationID)) -> Vec<&OwnedFederation> { match self.map.get(key) { - Some(vec) => vec.iter().collect(), + Some(vec) => vec.iter().map(|e| e.as_ref()).collect(), None => panic!("No zones for key: {:?}", key), } } @@ -115,22 +118,22 @@ impl DepthFirstWaitingStateList { } } impl PassedStateListExt for PassedStateListFed { - fn put(&mut self, mut pair: StatePair) { - let mut fed = pair.take_zone(); + fn put(&mut self, pair: StatePair) { + let mut fed = pair.clone_zone(); let (loc1, loc2) = (pair.locations1.id, pair.locations2.id); let key = (loc1, loc2); if let Some(f) = self.get(&key) { fed = fed.union(f).expensive_reduce(); } - self.insert(key, fed); + self.insert(key, Rc::new(fed)); } fn has(&self, pair: &StatePair) -> bool { let (loc1, loc2, fed) = ( pair.locations1.id.clone(), pair.locations2.id.clone(), - pair.ref_zone(), + pair.get_zone(), ); let key = (loc1, loc2); match self.get(&key) { diff --git a/src/system/refine.rs b/src/system/refine.rs index 606a4703..a9074825 100644 --- a/src/system/refine.rs +++ b/src/system/refine.rs @@ -5,8 +5,9 @@ use crate::model_objects::{ PassedStateList, PassedStateListExt, StatePair, Transition, WaitingStateList, }; use crate::system::query_failures::RefinementFailure; -use crate::transition_systems::{LocationTree, TransitionSystemPtr}; +use crate::transition_systems::TransitionSystemPtr; use std::collections::HashSet; +use std::rc::Rc; use super::query_failures::{ActionFailure, RefinementPrecondition, RefinementResult}; @@ -144,10 +145,10 @@ pub fn check_refinement(sys1: TransitionSystemPtr, sys2: TransitionSystemPtr) -> initial_locations_2.clone(), ); - if !prepare_init_state(&mut initial_pair, initial_locations_1, initial_locations_2) { + if initial_pair.ref_zone().is_empty() { return RefinementFailure::empty_initial(sys1.as_ref(), sys2.as_ref()); } - initial_pair.extrapolate_max_bounds(context.sys1, context.sys2); + initial_pair = initial_pair.extrapolate_max_bounds(context.sys1, context.sys2); debug!("Initial {}", initial_pair); context.waiting_list.put(initial_pair); @@ -336,12 +337,10 @@ fn build_state_pair( context: &mut RefinementContext, is_state1: bool, ) -> BuildResult { - //Creates new state pair - let mut new_sp: StatePair = curr_pair.clone(); //Creates DBM for that state pair - let mut new_sp_zone = new_sp.take_zone(); + let mut new_sp_zone = curr_pair.clone_zone(); + //Apply guards on both sides - let (locations1, locations2) = new_sp.get_mut_states(is_state1); //Applies the left side guards and checks if zone is valid new_sp_zone = transition1.apply_guards(new_sp_zone); @@ -361,16 +360,15 @@ fn build_state_pair( new_sp_zone = new_sp_zone.up(); //Update locations in states - - transition1.move_locations(locations1); - transition2.move_locations(locations2); + let (locations1, locations2) = ( + transition1.target_locations.clone(), + transition2.target_locations.clone(), + ); // Apply invariants on the left side of relation let (left_loc, right_loc) = if is_state1 { - //(locations2, locations1) (locations1, locations2) } else { - //(locations1, locations2) (locations2, locations1) }; @@ -395,9 +393,8 @@ fn build_state_pair( return BuildResult::Failure; } - new_sp.set_zone(new_sp_zone); - - new_sp.extrapolate_max_bounds(context.sys1, context.sys2); + let mut new_sp = StatePair::new(left_loc, right_loc, Rc::new(new_sp_zone)); + new_sp = new_sp.extrapolate_max_bounds(context.sys1, context.sys2); if !context.passed_list.has(&new_sp) && !context.waiting_list.has(&new_sp) { debug!("New state {}", new_sp); @@ -408,20 +405,6 @@ fn build_state_pair( BuildResult::Success } -fn prepare_init_state( - initial_pair: &mut StatePair, - initial_locations_1: LocationTree, - initial_locations_2: LocationTree, -) -> bool { - let mut sp_zone = initial_pair.take_zone(); - sp_zone = initial_locations_1.apply_invariants(sp_zone); - sp_zone = initial_locations_2.apply_invariants(sp_zone); - - initial_pair.set_zone(sp_zone); - - !initial_pair.ref_zone().is_empty() -} - fn check_preconditions( sys1: &TransitionSystemPtr, sys2: &TransitionSystemPtr, From 446f5a7d09e038fef3a131d727edb02b9c805e6e Mon Sep 17 00:00:00 2001 From: Simon Rask Date: Sat, 18 Nov 2023 12:03:33 +0100 Subject: [PATCH 2/6] Use reference counting for `LocationTree` in `StatePair` --- src/data_reader/proto_reader.rs | 5 +- src/model_objects/decision.rs | 8 +- src/model_objects/state.rs | 12 +-- src/model_objects/statepair.rs | 44 +++++----- src/model_objects/statepair_list.rs | 6 +- src/model_objects/transition.rs | 22 +++-- src/system/extract_state.rs | 16 ++-- src/system/local_consistency.rs | 12 +-- src/system/reachability.rs | 9 +- src/system/refine.rs | 4 +- src/system/save_component.rs | 57 +++++++------ src/tests/edge_ids/transition_id_tests.rs | 3 +- src/tests/reachability/partial_state.rs | 86 ++++++++++---------- src/transition_systems/common.rs | 31 +++---- src/transition_systems/compiled_component.rs | 20 +++-- src/transition_systems/composition.rs | 3 +- src/transition_systems/conjunction.rs | 3 +- src/transition_systems/location_tree.rs | 60 +++++++------- src/transition_systems/quotient.rs | 68 +++++++++------- src/transition_systems/transition_system.rs | 28 ++++--- 20 files changed, 273 insertions(+), 224 deletions(-) diff --git a/src/data_reader/proto_reader.rs b/src/data_reader/proto_reader.rs index ec80baf0..1b8eba09 100644 --- a/src/data_reader/proto_reader.rs +++ b/src/data_reader/proto_reader.rs @@ -1,5 +1,6 @@ use std::collections::HashMap; use std::convert::TryInto; +use std::rc::Rc; use edbm::util::constraints::{Conjunction, Constraint, Disjunction, Inequality, RawInequality}; use edbm::zones::OwnedFederation; @@ -81,7 +82,7 @@ pub fn proto_state_to_state(state: ProtoState, system: &TransitionSystemPtr) -> fn proto_location_tree_to_location_tree( location_tree: ProtoLocationTree, system: &TransitionSystemPtr, -) -> LocationTree { +) -> Rc { let target: SpecificLocation = location_tree.into(); system.construct_location_tree(target).unwrap() @@ -216,7 +217,7 @@ mod tests { return; } for action in system.get_actions() { - for t in system.next_transitions(&state.decorated_locations, &action) { + for t in system.next_transitions(Rc::clone(&state.decorated_locations), &action) { let state = t.use_transition_alt(state); if let Some(state) = state { let next_state = convert_to_proto_and_back(&state, system); diff --git a/src/model_objects/decision.rs b/src/model_objects/decision.rs index 10d7fefa..376e1327 100644 --- a/src/model_objects/decision.rs +++ b/src/model_objects/decision.rs @@ -1,3 +1,5 @@ +use std::rc::Rc; + use crate::model_objects::{State, Transition}; use crate::transition_systems::TransitionSystemPtr; @@ -16,7 +18,8 @@ impl Decision { /// # Panics /// Panics if the [`Decision`] leads to no new states or is ambiguous (leads to multiple new states) pub fn resolve(&self, system: &TransitionSystemPtr) -> Vec { - let transitions = system.next_transitions(&self.state.decorated_locations, &self.action); + let transitions = + system.next_transitions(Rc::clone(&self.state.decorated_locations), &self.action); let mut next_states: Vec<_> = transitions .into_iter() .filter_map(|transition| transition.use_transition_alt(&self.state)) @@ -64,7 +67,8 @@ impl Decision { let mut next_decisions = vec![]; for action in system.get_actions() { - let possible_transitions = system.next_transitions(&state.decorated_locations, &action); + let possible_transitions = + system.next_transitions(Rc::clone(&state.decorated_locations), &action); for t in possible_transitions { if let Some(decision) = Decision::from_state_transition(state.clone(), &t, &action) { diff --git a/src/model_objects/state.rs b/src/model_objects/state.rs index 4f842669..5b90de13 100644 --- a/src/model_objects/state.rs +++ b/src/model_objects/state.rs @@ -1,3 +1,5 @@ +use std::rc::Rc; + use crate::transition_systems::{LocationTree, TransitionSystem}; use edbm::util::bounds::Bounds; use edbm::util::constraints::ClockIndex; @@ -8,12 +10,12 @@ use edbm::zones::OwnedFederation; // This should probably be refactored as it causes unnecessary confusion #[derive(Clone, Debug)] pub struct State { - pub decorated_locations: LocationTree, + pub decorated_locations: Rc, zone_sentinel: Option, } impl State { - pub fn new(decorated_locations: LocationTree, zone: OwnedFederation) -> Self { + pub fn new(decorated_locations: Rc, zone: OwnedFederation) -> Self { State { decorated_locations, zone_sentinel: Some(zone), @@ -25,7 +27,7 @@ impl State { } pub fn from_location( - decorated_locations: LocationTree, + decorated_locations: Rc, dimensions: ClockIndex, ) -> Option { let mut fed = OwnedFederation::init(dimensions); @@ -78,7 +80,7 @@ impl State { } pub fn extrapolate_max_bounds(&mut self, system: &dyn TransitionSystem) { - let bounds = system.get_local_max_bounds(&self.decorated_locations); + let bounds = system.get_local_max_bounds(self.decorated_locations.as_ref()); self.update_zone(|zone| zone.extrapolate_max_bounds(&bounds)) } @@ -87,7 +89,7 @@ impl State { system: &dyn TransitionSystem, extra_bounds: &Bounds, ) { - let mut bounds = system.get_local_max_bounds(&self.decorated_locations); + let mut bounds = system.get_local_max_bounds(self.decorated_locations.as_ref()); bounds.add_bounds(extra_bounds); self.update_zone(|zone| zone.extrapolate_max_bounds(&bounds)) } diff --git a/src/model_objects/statepair.rs b/src/model_objects/statepair.rs index 9c0bc997..593524a4 100644 --- a/src/model_objects/statepair.rs +++ b/src/model_objects/statepair.rs @@ -8,16 +8,16 @@ use std::{ #[derive(Clone, Debug)] pub struct StatePair { - pub locations1: LocationTree, - pub locations2: LocationTree, + pub locations1: Rc, + pub locations2: Rc, zone: Rc, } impl StatePair { pub fn from_locations( dimensions: usize, - locations1: LocationTree, - locations2: LocationTree, + locations1: Rc, + locations2: Rc, ) -> StatePair { let mut zone = OwnedFederation::init(dimensions); @@ -32,8 +32,8 @@ impl StatePair { } pub fn new( - locations1: LocationTree, - locations2: LocationTree, + locations1: Rc, + locations2: Rc, zone: Rc, ) -> Self { StatePair { @@ -43,25 +43,25 @@ impl StatePair { } } - pub fn get_locations1(&self) -> &LocationTree { - &self.locations1 + pub fn get_locations1(&self) -> Rc { + self.locations1.clone() } - pub fn get_locations2(&self) -> &LocationTree { - &self.locations2 + pub fn get_locations2(&self) -> Rc { + self.locations2.clone() } //Used to allow borrowing both states as mutable - pub fn get_mut_locations( - &mut self, - is_states1: bool, - ) -> (&mut LocationTree, &mut LocationTree) { - if is_states1 { - (&mut self.locations1, &mut self.locations2) - } else { - (&mut self.locations2, &mut self.locations1) - } - } + // pub fn get_mut_locations( + // &mut self, + // is_states1: bool, + // ) -> (&mut LocationTree, &mut LocationTree) { + // if is_states1 { + // (&mut self.locations1, &mut self.locations2) + // } else { + // (&mut self.locations2, &mut self.locations1) + // } + // } pub fn get_locations(&self, is_states1: bool) -> (&LocationTree, &LocationTree) { if is_states1 { @@ -88,8 +88,8 @@ impl StatePair { sys1: &TransitionSystemPtr, sys2: &TransitionSystemPtr, ) -> Self { - let mut bounds = sys1.get_local_max_bounds(&self.locations1); - bounds.add_bounds(&sys2.get_local_max_bounds(&self.locations2)); + let mut bounds = sys1.get_local_max_bounds(self.locations1.as_ref()); + bounds.add_bounds(&sys2.get_local_max_bounds(self.locations2.as_ref())); let zone = self.clone_zone().extrapolate_max_bounds(&bounds); StatePair { diff --git a/src/model_objects/statepair_list.rs b/src/model_objects/statepair_list.rs index 51c2b2c0..c41fb024 100644 --- a/src/model_objects/statepair_list.rs +++ b/src/model_objects/statepair_list.rs @@ -26,7 +26,7 @@ pub trait PassedStateListExt { impl PassedStateListExt for PassedStateListVec { fn put(&mut self, pair: StatePair) { let fed = pair.get_zone(); - let (loc1, loc2) = (pair.locations1.id, pair.locations2.id); + let (loc1, loc2) = (pair.locations1.id.clone(), pair.locations2.id.clone()); let key = (loc1, loc2); if let Some(vec) = self.get_mut(&key) { vec.push(fed); @@ -60,7 +60,7 @@ impl PassedStateListExt for DepthFirstWaitingStateList { fn put(&mut self, pair: StatePair) { self.queue.push_front(pair.clone()); let fed = pair.get_zone(); - let (loc1, loc2) = (pair.locations1.id, pair.locations2.id); + let (loc1, loc2) = (pair.locations1.id.clone(), pair.locations2.id.clone()); let key = (loc1, loc2); if let Some(vec) = self.map.get_mut(&key) { vec.push_front(fed); @@ -120,7 +120,7 @@ impl DepthFirstWaitingStateList { impl PassedStateListExt for PassedStateListFed { fn put(&mut self, pair: StatePair) { let mut fed = pair.clone_zone(); - let (loc1, loc2) = (pair.locations1.id, pair.locations2.id); + let (loc1, loc2) = (pair.locations1.id.clone(), pair.locations2.id.clone()); let key = (loc1, loc2); if let Some(f) = self.get(&key) { diff --git a/src/model_objects/transition.rs b/src/model_objects/transition.rs index 7b56ce50..b4afe371 100644 --- a/src/model_objects/transition.rs +++ b/src/model_objects/transition.rs @@ -7,6 +7,7 @@ use edbm::util::constraints::ClockIndex; use edbm::zones::OwnedFederation; use std::collections::HashMap; use std::fmt; +use std::rc::Rc; /// Represents a single transition from taking edges in multiple components #[derive(Debug, Clone)] @@ -14,24 +15,22 @@ pub struct Transition { /// The ID of the transition, based on the edges it is created from. pub id: TransitionID, pub guard_zone: OwnedFederation, - pub target_locations: LocationTree, + pub target_locations: Rc, pub updates: Vec, } impl Transition { /// Create a new transition not based on an edge with no identifier - pub fn without_id(target_locations: &LocationTree, dim: ClockIndex) -> Transition { + pub fn without_id(target_locations: Rc, dim: ClockIndex) -> Transition { Transition { id: TransitionID::None, guard_zone: OwnedFederation::universe(dim), - target_locations: target_locations.clone(), + target_locations, updates: vec![], } } pub fn from_component_and_edge(comp: &Component, edge: &Edge, dim: ClockIndex) -> Transition { - //let (comp, edge) = edges; - let target_loc_name = &edge.target_location; let target_loc = comp.get_location_by_name(target_loc_name); let target_locations = LocationTree::simple(target_loc, comp.get_declarations(), dim); @@ -58,7 +57,7 @@ impl Transition { zone = self.apply_guards(zone); if !zone.is_empty() { zone = self.apply_updates(zone).up(); - self.move_locations(&mut state.decorated_locations); + state.decorated_locations = Rc::clone(&self.target_locations); zone = state.decorated_locations.apply_invariants(zone); if !zone.is_empty() { state.set_zone(zone); @@ -86,8 +85,11 @@ impl Transition { let mut out: Vec = vec![]; for l in left { for r in right { - let target_locations = - LocationTree::compose(&l.target_locations, &r.target_locations, comp); + let target_locations = LocationTree::compose( + Rc::clone(&l.target_locations), + Rc::clone(&r.target_locations), + comp, + ); let guard_zone = l.guard_zone.clone().intersection(&r.guard_zone); @@ -148,10 +150,6 @@ impl Transition { zone.intersection(&self.guard_zone) } - pub fn move_locations(&self, locations: &mut LocationTree) { - *locations = self.target_locations.clone(); - } - pub fn combine_edge_guards( edges: &Vec<(&Component, &Edge)>, dim: ClockIndex, diff --git a/src/system/extract_state.rs b/src/system/extract_state.rs index 7b11872a..c8146b4e 100644 --- a/src/system/extract_state.rs +++ b/src/system/extract_state.rs @@ -1,3 +1,5 @@ +use std::rc::Rc; + use edbm::zones::OwnedFederation; use itertools::Itertools; @@ -110,29 +112,29 @@ fn construct_location_tree( locations: &Vec, machine: &SystemRecipe, system: &TransitionSystemPtr, -) -> Result { +) -> Result, String> { match machine { SystemRecipe::Composition(left, right) => { let (left_system, right_system) = system.get_children(); Ok(LocationTree::compose( - &construct_location_tree(locations, left, left_system)?, - &construct_location_tree(locations, right, right_system)?, + construct_location_tree(locations, left, left_system)?, + construct_location_tree(locations, right, right_system)?, CompositionType::Composition, )) } SystemRecipe::Conjunction(left, right) => { let (left_system, right_system) = system.get_children(); Ok(LocationTree::compose( - &construct_location_tree(locations, left, left_system)?, - &construct_location_tree(locations, right, right_system)?, + construct_location_tree(locations, left, left_system)?, + construct_location_tree(locations, right, right_system)?, CompositionType::Conjunction, )) } SystemRecipe::Quotient(left, right, ..) => { let (left_system, right_system) = system.get_children(); Ok(LocationTree::merge_as_quotient( - &construct_location_tree(locations, left, left_system)?, - &construct_location_tree(locations, right, right_system)?, + construct_location_tree(locations, left, left_system)?, + construct_location_tree(locations, right, right_system)?, )) } SystemRecipe::Component(component) => { diff --git a/src/system/local_consistency.rs b/src/system/local_consistency.rs index 1e2b7a27..047ffa94 100644 --- a/src/system/local_consistency.rs +++ b/src/system/local_consistency.rs @@ -1,3 +1,5 @@ +use std::rc::Rc; + use edbm::zones::OwnedFederation; use log::warn; @@ -44,7 +46,7 @@ fn is_deterministic_helper( for action in system.get_actions() { let mut location_fed = OwnedFederation::empty(system.get_dim()); - for transition in &system.next_transitions(&state.decorated_locations, &action) { + for transition in &system.next_transitions(Rc::clone(&state.decorated_locations), &action) { let mut new_state = state.clone(); if transition.use_transition(&mut new_state) { let mut allowed_fed = transition.get_allowed_federation(); @@ -95,7 +97,7 @@ pub fn consistency_least_helper( passed_list.push(state.clone()); for input in system.get_input_actions() { - for transition in &system.next_inputs(&state.decorated_locations, &input) { + for transition in &system.next_inputs(Rc::clone(&state.decorated_locations), &input) { let mut new_state = state.clone(); if transition.use_transition(&mut new_state) { new_state.extrapolate_max_bounds(system); @@ -110,7 +112,7 @@ pub fn consistency_least_helper( } for output in system.get_output_actions() { - for transition in system.next_outputs(&state.decorated_locations, &output) { + for transition in system.next_outputs(Rc::clone(&state.decorated_locations), &output) { let mut new_state = state.clone(); if transition.use_transition(&mut new_state) { new_state.extrapolate_max_bounds(system); @@ -135,7 +137,7 @@ fn consistency_fully_helper( passed_list.push(state.clone()); for input in system.get_input_actions() { - for transition in system.next_inputs(&state.decorated_locations, &input) { + for transition in system.next_inputs(Rc::clone(&state.decorated_locations), &input) { let mut new_state = state.clone(); if transition.use_transition(&mut new_state) { new_state.extrapolate_max_bounds(system); @@ -149,7 +151,7 @@ fn consistency_fully_helper( let mut output_existed = false; for output in system.get_output_actions() { - for transition in system.next_outputs(&state.decorated_locations, &output) { + for transition in system.next_outputs(Rc::clone(&state.decorated_locations), &output) { let mut new_state = state.clone(); if transition.use_transition(&mut new_state) { new_state.extrapolate_max_bounds(system); diff --git a/src/system/reachability.rs b/src/system/reachability.rs index d0e5496c..3cd095cd 100644 --- a/src/system/reachability.rs +++ b/src/system/reachability.rs @@ -134,9 +134,10 @@ fn reachability_search( } for action in &actions { - for transition in - &system.next_transitions(&sub_path.destination_state.decorated_locations, action) - { + for transition in &system.next_transitions( + Rc::clone(&sub_path.destination_state.decorated_locations), + action, + ) { take_transition( &sub_path, transition, @@ -156,7 +157,7 @@ fn reachability_search( fn reached_end_state(cur_state: &State, end_state: &State) -> bool { cur_state .decorated_locations - .compare_partial_locations(&end_state.decorated_locations) + .compare_partial_locations(Rc::clone(&end_state.decorated_locations)) && cur_state.zone_ref().has_intersection(end_state.zone_ref()) } diff --git a/src/system/refine.rs b/src/system/refine.rs index a9074825..0ca3f0ab 100644 --- a/src/system/refine.rs +++ b/src/system/refine.rs @@ -141,8 +141,8 @@ pub fn check_refinement(sys1: TransitionSystemPtr, sys2: TransitionSystemPtr) -> let mut initial_pair = StatePair::from_locations( dimensions, - initial_locations_1.clone(), - initial_locations_2.clone(), + Rc::clone(&initial_locations_1), + Rc::clone(&initial_locations_2), ); if initial_pair.ref_zone().is_empty() { diff --git a/src/system/save_component.rs b/src/system/save_component.rs index ad350f3b..9a9cb1df 100644 --- a/src/system/save_component.rs +++ b/src/system/save_component.rs @@ -2,6 +2,7 @@ use crate::model_objects::expressions::BoolExpression; use crate::model_objects::{Component, Declarations, Location, LocationType, SyncType}; use crate::transition_systems::{LocationTree, TransitionSystemPtr}; use std::collections::HashMap; +use std::rc::Rc; pub enum PruningStrategy { Reachable, @@ -16,7 +17,7 @@ pub fn combine_components( system: &TransitionSystemPtr, reachability: PruningStrategy, ) -> Component { - let mut location_trees = vec![]; + let mut location_trees: Vec> = vec![]; let mut edges = vec![]; let clocks = get_clock_map(system); match reachability { @@ -28,7 +29,7 @@ pub fn combine_components( } }; - let locations = get_locations_from_trees(&location_trees, &clocks); + let locations = get_locations_from_trees(location_trees.as_slice(), &clocks); Component { name: "".to_string(), @@ -43,7 +44,7 @@ pub fn combine_components( } pub fn get_locations_from_trees( - location_trees: &[LocationTree], + location_trees: &[Rc], clock_map: &HashMap, ) -> Vec { location_trees @@ -92,20 +93,20 @@ pub fn get_clock_map(sysrep: &TransitionSystemPtr) -> HashMap, + locations: &mut Vec>, edges: &mut Vec, clock_map: &HashMap, ) { let l = representation.get_all_locations(); locations.extend(l); for location in locations { - collect_edges_from_location(location, representation, edges, clock_map); + collect_edges_from_location(Rc::clone(location), representation, edges, clock_map); } } fn collect_reachable_edges_and_locations( representation: &TransitionSystemPtr, - locations: &mut Vec, + locations: &mut Vec>, edges: &mut Vec, clock_map: &HashMap, ) { @@ -118,17 +119,17 @@ fn collect_reachable_edges_and_locations( locations.push(l.clone()); - collect_reachable_locations(&l, representation, locations); + collect_reachable_locations(l, representation, locations); for loc in locations { - collect_edges_from_location(loc, representation, edges, clock_map); + collect_edges_from_location(Rc::clone(loc), representation, edges, clock_map); } } fn collect_reachable_locations( - location: &LocationTree, + location: Rc, representation: &TransitionSystemPtr, - locations: &mut Vec, + locations: &mut Vec>, ) { for input in [true, false].iter() { for sync in if *input { @@ -136,15 +137,14 @@ fn collect_reachable_locations( } else { representation.get_output_actions() } { - let transitions = representation.next_transitions(location, &sync); + let transitions = representation.next_transitions(Rc::clone(&location), &sync); for transition in transitions { - let mut target_location = location.clone(); - transition.move_locations(&mut target_location); + let target_location = transition.target_locations; if !locations.contains(&target_location) { - locations.push(target_location.clone()); - collect_reachable_locations(&target_location, representation, locations); + locations.push(Rc::clone(&target_location)); + collect_reachable_locations(target_location, representation, locations); } } } @@ -152,17 +152,29 @@ fn collect_reachable_locations( } fn collect_edges_from_location( - location: &LocationTree, + location: Rc, representation: &TransitionSystemPtr, edges: &mut Vec, clock_map: &HashMap, ) { - collect_specific_edges_from_location(location, representation, edges, true, clock_map); - collect_specific_edges_from_location(location, representation, edges, false, clock_map); + collect_specific_edges_from_location( + Rc::clone(&location), + representation, + edges, + true, + clock_map, + ); + collect_specific_edges_from_location( + Rc::clone(&location), + representation, + edges, + false, + clock_map, + ); } fn collect_specific_edges_from_location( - location: &LocationTree, + location: Rc, representation: &TransitionSystemPtr, edges: &mut Vec, input: bool, @@ -173,10 +185,9 @@ fn collect_specific_edges_from_location( } else { representation.get_output_actions() } { - let transitions = representation.next_transitions(location, &sync); + let transitions = representation.next_transitions(Rc::clone(&location), &sync); for transition in transitions { - let mut target_location = location.clone(); - transition.move_locations(&mut target_location); + let target_location_id = transition.target_locations.id.to_string(); let guard = transition.get_renamed_guard_expression(clock_map); if let Some(BoolExpression::Bool(false)) = guard { @@ -186,7 +197,7 @@ fn collect_specific_edges_from_location( let edge = Edge { id: transition.id.to_string(), source_location: location.id.to_string(), - target_location: target_location.id.to_string(), + target_location: target_location_id, sync_type: if input { SyncType::Input } else { diff --git a/src/tests/edge_ids/transition_id_tests.rs b/src/tests/edge_ids/transition_id_tests.rs index 32d0d8ec..ee43af78 100644 --- a/src/tests/edge_ids/transition_id_tests.rs +++ b/src/tests/edge_ids/transition_id_tests.rs @@ -2,6 +2,7 @@ mod reachability_transition_id_test { use std::collections::HashSet; use std::iter::FromIterator; + use std::rc::Rc; use crate::model_objects::expressions::SystemExpression; use crate::tests::reachability::helper_functions::reachability_test_helper_functions; @@ -81,7 +82,7 @@ mod reachability_transition_id_test { ); for loc in system.get_all_locations() { for ac in system.get_actions() { - for tran in system.next_transitions(&loc, &ac) { + for tran in system.next_transitions(Rc::clone(&loc), &ac) { if expected_ids.contains(&tran.id) { expected_ids.remove(&tran.id); } else { diff --git a/src/tests/reachability/partial_state.rs b/src/tests/reachability/partial_state.rs index ace233d8..d37186e3 100644 --- a/src/tests/reachability/partial_state.rs +++ b/src/tests/reachability/partial_state.rs @@ -1,11 +1,13 @@ #[cfg(test)] mod reachability_partial_states_test { + use std::rc::Rc; + use crate::model_objects::{Declarations, Location, LocationType}; use crate::transition_systems::CompositionType; use crate::transition_systems::LocationTree; use test_case::test_case; - fn build_location_tree_helper(id: &str, location_type: LocationType) -> LocationTree { + fn build_location_tree_helper(id: &str, location_type: LocationType) -> Rc { LocationTree::simple( &Location { id: id.to_string(), @@ -26,68 +28,68 @@ mod reachability_partial_states_test { #[test_case(build_location_tree_helper("L5", LocationType::Normal), build_location_tree_helper("L5", LocationType::Normal); "L5 == L5")] - #[test_case(LocationTree::merge_as_quotient(&build_location_tree_helper("L5", LocationType::Normal), &LocationTree::build_any_location_tree()), - LocationTree::merge_as_quotient(&build_location_tree_helper("L5", LocationType::Normal), &build_location_tree_helper("L1", LocationType::Normal)); + #[test_case(LocationTree::merge_as_quotient(build_location_tree_helper("L5", LocationType::Normal), LocationTree::build_any_location_tree()), + LocationTree::merge_as_quotient(build_location_tree_helper("L5", LocationType::Normal), build_location_tree_helper("L1", LocationType::Normal)); "L5//_ == L5//L1")] - #[test_case(LocationTree::compose(&build_location_tree_helper("L5", LocationType::Normal), &LocationTree::build_any_location_tree(), CompositionType::Conjunction), - LocationTree::compose(&LocationTree::build_any_location_tree(), &build_location_tree_helper("L1", LocationType::Normal), CompositionType::Conjunction); - "L5&&_ == _&&L1")] - #[test_case(LocationTree::compose(&build_location_tree_helper("L7", LocationType::Normal), &LocationTree::build_any_location_tree(), CompositionType::Composition), - LocationTree::compose(&build_location_tree_helper("L7", LocationType::Normal), &build_location_tree_helper("L1", LocationType::Normal), CompositionType::Composition); + #[test_case(LocationTree::compose(build_location_tree_helper("L5", LocationType::Normal), LocationTree::build_any_location_tree(), CompositionType::Conjunction), + LocationTree::compose(LocationTree::build_any_location_tree(), build_location_tree_helper("L1", LocationType::Normal), CompositionType::Conjunction); + "L5_ == _L1")] + #[test_case(LocationTree::compose(build_location_tree_helper("L7", LocationType::Normal), LocationTree::build_any_location_tree(), CompositionType::Composition), + LocationTree::compose(build_location_tree_helper("L7", LocationType::Normal), build_location_tree_helper("L1", LocationType::Normal), CompositionType::Composition); "L7||_ == L7||L1")] - #[test_case(LocationTree::compose(&LocationTree::build_any_location_tree(), &LocationTree::build_any_location_tree(), CompositionType::Composition), - LocationTree::compose(&build_location_tree_helper("L2", LocationType::Normal), &build_location_tree_helper("L1", LocationType::Normal), CompositionType::Composition); + #[test_case(LocationTree::compose(LocationTree::build_any_location_tree(), LocationTree::build_any_location_tree(), CompositionType::Composition), + LocationTree::compose(build_location_tree_helper("L2", LocationType::Normal), build_location_tree_helper("L1", LocationType::Normal), CompositionType::Composition); "_||_ == L2||L1")] - #[test_case(LocationTree::compose(&LocationTree::compose(&LocationTree::build_any_location_tree(), &LocationTree::build_any_location_tree(), CompositionType::Composition),&build_location_tree_helper("L2", LocationType::Normal), CompositionType::Composition), - LocationTree::compose(&LocationTree::compose(&build_location_tree_helper("L2", LocationType::Normal), &build_location_tree_helper("L1", LocationType::Normal), CompositionType::Composition),&build_location_tree_helper("L2", LocationType::Normal), CompositionType::Composition); + #[test_case(LocationTree::compose(LocationTree::compose(LocationTree::build_any_location_tree(), LocationTree::build_any_location_tree(), CompositionType::Composition),build_location_tree_helper("L2", LocationType::Normal), CompositionType::Composition), + LocationTree::compose(LocationTree::compose(build_location_tree_helper("L2", LocationType::Normal), build_location_tree_helper("L1", LocationType::Normal), CompositionType::Composition),build_location_tree_helper("L2", LocationType::Normal), CompositionType::Composition); "_||_||L2 == L2||L1||L2")] #[test_case(build_location_tree_helper("L_35", LocationType::Normal), build_location_tree_helper("L_35", LocationType::Normal); "L_35 == L_35")] - fn checks_cmp_locations_returns_true(loc1: LocationTree, loc2: LocationTree) { - assert!(loc1.compare_partial_locations(&loc2)); + fn checks_cmp_locations_returns_true(loc1: Rc, loc2: Rc) { + assert!(loc1.compare_partial_locations(loc2)); } - #[test_case(LocationTree::compose(&build_location_tree_helper("L2", LocationType::Normal), &build_location_tree_helper("L5", LocationType::Normal), CompositionType::Composition), - LocationTree::compose(&build_location_tree_helper("L2", LocationType::Normal), &build_location_tree_helper("L1", LocationType::Normal), CompositionType::Composition); + #[test_case(LocationTree::compose(build_location_tree_helper("L2", LocationType::Normal), build_location_tree_helper("L5", LocationType::Normal), CompositionType::Composition), + LocationTree::compose(build_location_tree_helper("L2", LocationType::Normal), build_location_tree_helper("L1", LocationType::Normal), CompositionType::Composition); "L2||L5 != L2||L1")] - #[test_case(LocationTree::merge_as_quotient(&build_location_tree_helper("L2", LocationType::Normal), &build_location_tree_helper("L6", LocationType::Normal)), - LocationTree::compose(&build_location_tree_helper("L2", LocationType::Normal), &build_location_tree_helper("L1", LocationType::Normal), CompositionType::Composition); + #[test_case(LocationTree::merge_as_quotient(build_location_tree_helper("L2", LocationType::Normal), build_location_tree_helper("L6", LocationType::Normal)), + LocationTree::compose(build_location_tree_helper("L2", LocationType::Normal), build_location_tree_helper("L1", LocationType::Normal), CompositionType::Composition); "L2//L6 != L2||L1")] - #[test_case(LocationTree::merge_as_quotient(&build_location_tree_helper("L7", LocationType::Normal), &build_location_tree_helper("L6", LocationType::Normal)), - LocationTree::compose(&build_location_tree_helper("L2", LocationType::Normal), &build_location_tree_helper("L1", LocationType::Normal), CompositionType::Conjunction); - "L7//L6 != L2&&L1")] - #[test_case(LocationTree::merge_as_quotient(&build_location_tree_helper("L8", LocationType::Normal), &LocationTree::build_any_location_tree()), - LocationTree::compose(&build_location_tree_helper("L2", LocationType::Normal), &build_location_tree_helper("L1", LocationType::Normal), CompositionType::Conjunction); - "L8//_ != L2&&L1")] + #[test_case(LocationTree::merge_as_quotient(build_location_tree_helper("L7", LocationType::Normal), build_location_tree_helper("L6", LocationType::Normal)), + LocationTree::compose(build_location_tree_helper("L2", LocationType::Normal), build_location_tree_helper("L1", LocationType::Normal), CompositionType::Conjunction); + "L7//L6 != L2L1")] + #[test_case(LocationTree::merge_as_quotient(build_location_tree_helper("L8", LocationType::Normal), LocationTree::build_any_location_tree()), + LocationTree::compose(build_location_tree_helper("L2", LocationType::Normal), build_location_tree_helper("L1", LocationType::Normal), CompositionType::Conjunction); + "L8//_ != L2L1")] #[test_case(LocationTree::build_any_location_tree(), - LocationTree::compose(&build_location_tree_helper("L6", LocationType::Normal), &build_location_tree_helper("L1", LocationType::Normal), CompositionType::Conjunction); - "_ != L6&&L1")] + LocationTree::compose(build_location_tree_helper("L6", LocationType::Normal), build_location_tree_helper("L1", LocationType::Normal), CompositionType::Conjunction); + "_ != L6L1")] #[test_case(LocationTree::build_any_location_tree(), - LocationTree::compose(&LocationTree::build_any_location_tree(), &LocationTree::build_any_location_tree(), CompositionType::Conjunction); - "anylocation _ != _&&_")] - #[test_case(LocationTree::compose(&build_location_tree_helper("L2", LocationType::Normal), &build_location_tree_helper("L4", LocationType::Normal), CompositionType::Conjunction), - LocationTree::merge_as_quotient(&build_location_tree_helper("L2", LocationType::Normal), &build_location_tree_helper("L4", LocationType::Normal)); - "L2&&L4 != L2\\L4")] - #[test_case(LocationTree::compose(&LocationTree::compose(&LocationTree::build_any_location_tree(), &LocationTree::build_any_location_tree(), CompositionType::Composition),&build_location_tree_helper("L2", LocationType::Normal), CompositionType::Conjunction), - LocationTree::compose(&LocationTree::compose(&build_location_tree_helper("L2", LocationType::Normal), &build_location_tree_helper("L1", LocationType::Normal), CompositionType::Composition),&build_location_tree_helper("L2", LocationType::Normal), CompositionType::Composition); - "_||_&&L2 == L2||L1||L2")] - #[test_case(LocationTree::compose(&LocationTree::compose(&build_location_tree_helper("L2", LocationType::Normal), &LocationTree::build_any_location_tree(), CompositionType::Composition),&build_location_tree_helper("L2", LocationType::Normal), CompositionType::Conjunction), - LocationTree::compose(&LocationTree::build_any_location_tree(), &LocationTree::build_any_location_tree(), CompositionType::Conjunction); - "L2||_&&L2 == _&&_")] + LocationTree::compose(LocationTree::build_any_location_tree(), LocationTree::build_any_location_tree(), CompositionType::Conjunction); + "anylocation _ != __")] + #[test_case(LocationTree::compose(build_location_tree_helper("L2", LocationType::Normal), build_location_tree_helper("L4", LocationType::Normal), CompositionType::Conjunction), + LocationTree::merge_as_quotient(build_location_tree_helper("L2", LocationType::Normal), build_location_tree_helper("L4", LocationType::Normal)); + "L2L4 != L2\\L4")] + #[test_case(LocationTree::compose(LocationTree::compose(LocationTree::build_any_location_tree(), LocationTree::build_any_location_tree(), CompositionType::Composition),build_location_tree_helper("L2", LocationType::Normal), CompositionType::Conjunction), + LocationTree::compose(LocationTree::compose(build_location_tree_helper("L2", LocationType::Normal), build_location_tree_helper("L1", LocationType::Normal), CompositionType::Composition),build_location_tree_helper("L2", LocationType::Normal), CompositionType::Composition); + "_||_L2 == L2||L1||L2")] + #[test_case(LocationTree::compose(LocationTree::compose(build_location_tree_helper("L2", LocationType::Normal), LocationTree::build_any_location_tree(), CompositionType::Composition),build_location_tree_helper("L2", LocationType::Normal), CompositionType::Conjunction), + LocationTree::compose(LocationTree::build_any_location_tree(), LocationTree::build_any_location_tree(), CompositionType::Conjunction); + "L2||_L2 == __")] #[test_case(build_location_tree_helper("L7", LocationType::Normal), build_location_tree_helper("L5", LocationType::Normal); "L7 != L5")] - #[test_case(LocationTree::merge_as_quotient(&LocationTree::build_any_location_tree(), &LocationTree::build_any_location_tree()), - LocationTree::compose(&build_location_tree_helper("L6", LocationType::Normal), &build_location_tree_helper("L25", LocationType::Normal), CompositionType::Conjunction); - "_//_ != L6&&L25")] + #[test_case(LocationTree::merge_as_quotient(LocationTree::build_any_location_tree(), LocationTree::build_any_location_tree()), + LocationTree::compose(build_location_tree_helper("L6", LocationType::Normal), build_location_tree_helper("L25", LocationType::Normal), CompositionType::Conjunction); + "_//_ != L6L25")] #[test_case(build_location_tree_helper("_L1", LocationType::Normal), build_location_tree_helper("L1", LocationType::Normal); "_L1 != L1")] #[test_case(build_location_tree_helper("__", LocationType::Normal), build_location_tree_helper("L7", LocationType::Normal); "__ != L7")] - fn checks_cmp_locations_returns_false(loc1: LocationTree, loc2: LocationTree) { - assert!(!loc1.compare_partial_locations(&loc2)); + fn checks_cmp_locations_returns_false(loc1: Rc, loc2: Rc) { + assert!(!loc1.compare_partial_locations(loc2)); } } diff --git a/src/transition_systems/common.rs b/src/transition_systems/common.rs index d16d1f19..26ff5f6b 100644 --- a/src/transition_systems/common.rs +++ b/src/transition_systems/common.rs @@ -1,4 +1,4 @@ -use std::collections::HashSet; +use std::{collections::HashSet, rc::Rc}; use dyn_clone::{clone_trait_object, DynClone}; use edbm::{ @@ -17,7 +17,7 @@ use crate::transition_systems::CompositionType; use super::{LocationTree, TransitionSystem, TransitionSystemPtr}; pub(super) trait ComposedTransitionSystem: DynClone { - fn next_transitions(&self, location: &LocationTree, action: &str) -> Vec; + fn next_transitions(&self, location: Rc, action: &str) -> Vec; fn check_local_consistency(&self) -> ConsistencyResult; @@ -41,8 +41,8 @@ impl TransitionSystem for T { let (left, right) = self.get_children(); let loc_l = loc.get_left(); let loc_r = loc.get_right(); - let mut bounds_l = left.get_local_max_bounds(loc_l); - let bounds_r = right.get_local_max_bounds(loc_r); + let mut bounds_l = left.get_local_max_bounds(&loc_l); + let bounds_r = right.get_local_max_bounds(&loc_r); bounds_l.add_bounds(&bounds_r); bounds_l } @@ -50,7 +50,7 @@ impl TransitionSystem for T { fn get_dim(&self) -> ClockIndex { self.get_dim() } - fn next_transitions(&self, location: &LocationTree, action: &str) -> Vec { + fn next_transitions(&self, location: Rc, action: &str) -> Vec { self.next_transitions(location, action) } fn get_input_actions(&self) -> HashSet { @@ -68,24 +68,24 @@ impl TransitionSystem for T { .collect() } - fn get_initial_location(&self) -> Option { + fn get_initial_location(&self) -> Option> { let (left, right) = self.get_children(); let l = left.get_initial_location()?; let r = right.get_initial_location()?; - Some(LocationTree::compose(&l, &r, self.get_composition_type())) + Some(LocationTree::compose(l, r, self.get_composition_type())) } - fn get_all_locations(&self) -> Vec { + fn get_all_locations(&self) -> Vec> { let (left, right) = self.get_children(); - let mut location_trees = vec![]; + let mut location_trees: Vec> = vec![]; let left = left.get_all_locations(); let right = right.get_all_locations(); for loc1 in &left { for loc2 in &right { location_trees.push(LocationTree::compose( - loc1, - loc2, + Rc::clone(loc1), + Rc::clone(loc2), self.get_composition_type(), )); } @@ -134,14 +134,17 @@ impl TransitionSystem for T { self.get_composition_type() } - fn construct_location_tree(&self, target: SpecificLocation) -> Result { + fn construct_location_tree( + &self, + target: SpecificLocation, + ) -> Result, String> { let (left, right) = self.get_children(); let (t_left, t_right) = target.split(); let loc_l = left.construct_location_tree(t_left)?; let loc_r = right.construct_location_tree(t_right)?; Ok(LocationTree::compose( - &loc_l, - &loc_r, + loc_l, + loc_r, self.get_composition_type(), )) } diff --git a/src/transition_systems/compiled_component.rs b/src/transition_systems/compiled_component.rs index eb9881b0..5952e03a 100644 --- a/src/transition_systems/compiled_component.rs +++ b/src/transition_systems/compiled_component.rs @@ -10,6 +10,7 @@ use edbm::util::constraints::ClockIndex; use std::collections::hash_set::HashSet; use std::collections::HashMap; use std::iter::FromIterator; +use std::rc::Rc; use super::transition_system::ComponentInfoTree; use super::{CompositionType, LocationID}; @@ -28,9 +29,9 @@ pub struct ComponentInfo { pub struct CompiledComponent { inputs: HashSet, outputs: HashSet, - locations: HashMap, + locations: HashMap>, location_edges: HashMap>, - initial_location: Option, + initial_location: Option>, comp_info: ComponentInfo, dim: ClockIndex, } @@ -48,7 +49,7 @@ impl CompiledComponent { .map_err(|e| e.to_simple_failure(&component.name))?; } - let locations: HashMap = component + let locations: HashMap> = component .locations .iter() .map(|loc| { @@ -124,7 +125,7 @@ impl TransitionSystem for CompiledComponent { self.dim } - fn next_transitions(&self, locations: &LocationTree, action: &str) -> Vec { + fn next_transitions(&self, locations: Rc, action: &str) -> Vec { assert!(self.actions_contain(action)); let is_input = self.inputs_contain(action); @@ -160,11 +161,11 @@ impl TransitionSystem for CompiledComponent { self.inputs.union(&self.outputs).cloned().collect() } - fn get_initial_location(&self) -> Option { + fn get_initial_location(&self) -> Option> { self.initial_location.clone() } - fn get_all_locations(&self) -> Vec { + fn get_all_locations(&self) -> Vec> { self.locations.values().cloned().collect() } @@ -194,7 +195,7 @@ impl TransitionSystem for CompiledComponent { CompositionType::Simple } - fn get_location(&self, id: &LocationID) -> Option { + fn get_location(&self, id: &LocationID) -> Option> { self.locations.get(id).cloned() } @@ -210,7 +211,10 @@ impl TransitionSystem for CompiledComponent { self.comp_info.name.clone() } - fn construct_location_tree(&self, target: SpecificLocation) -> Result { + fn construct_location_tree( + &self, + target: SpecificLocation, + ) -> Result, String> { match target { SpecificLocation::ComponentLocation { comp, location_id } => { assert_eq!(comp.name, self.comp_info.name); diff --git a/src/transition_systems/composition.rs b/src/transition_systems/composition.rs index 8f580c97..22fceeb6 100644 --- a/src/transition_systems/composition.rs +++ b/src/transition_systems/composition.rs @@ -4,6 +4,7 @@ use crate::model_objects::Transition; use crate::system::query_failures::{ActionFailure, SystemRecipeFailure}; use crate::transition_systems::{LocationTree, TransitionSystem, TransitionSystemPtr}; use std::collections::hash_set::HashSet; +use std::rc::Rc; use super::common::ComposedTransitionSystem; use super::CompositionType; @@ -75,7 +76,7 @@ impl Composition { } impl ComposedTransitionSystem for Composition { - fn next_transitions(&self, location: &LocationTree, action: &str) -> Vec { + fn next_transitions(&self, location: Rc, action: &str) -> Vec { assert!(self.actions_contain(action)); let loc_left = location.get_left(); diff --git a/src/transition_systems/conjunction.rs b/src/transition_systems/conjunction.rs index 2f882b6c..5cfe2d17 100644 --- a/src/transition_systems/conjunction.rs +++ b/src/transition_systems/conjunction.rs @@ -7,6 +7,7 @@ use crate::transition_systems::{ CompositionType, LocationTree, TransitionSystem, TransitionSystemPtr, }; use std::collections::hash_set::HashSet; +use std::rc::Rc; use super::common::ComposedTransitionSystem; @@ -73,7 +74,7 @@ impl Conjunction { } impl ComposedTransitionSystem for Conjunction { - fn next_transitions(&self, location: &LocationTree, action: &str) -> Vec { + fn next_transitions(&self, location: Rc, action: &str) -> Vec { assert!(self.actions_contain(action)); let loc_left = location.get_left(); diff --git a/src/transition_systems/location_tree.rs b/src/transition_systems/location_tree.rs index 13145d18..3822f52b 100644 --- a/src/transition_systems/location_tree.rs +++ b/src/transition_systems/location_tree.rs @@ -1,3 +1,5 @@ +use std::rc::Rc; + use edbm::{util::constraints::ClockIndex, zones::OwnedFederation}; use crate::edge_eval::constraint_applier::apply_constraints_to_state; @@ -19,8 +21,8 @@ pub struct LocationTree { /// The invariant for the `Location` pub invariant: Option, loc_type: LocationType, - left: Option>, - right: Option>, + left: Option>, + right: Option>, } impl PartialEq for LocationTree { @@ -30,29 +32,29 @@ impl PartialEq for LocationTree { } impl LocationTree { - pub fn universal() -> Self { - LocationTree { + pub fn universal() -> Rc { + Rc::new(LocationTree { id: LocationID::Special(crate::system::specifics::SpecialLocation::Universal), invariant: None, loc_type: LocationType::Universal, left: None, right: None, - } + }) } - pub fn error(dim: ClockIndex, quotient_clock_index: ClockIndex) -> Self { + pub fn error(dim: ClockIndex, quotient_clock_index: ClockIndex) -> Rc { let inv = OwnedFederation::universe(dim).constrain_eq(quotient_clock_index, 0); - LocationTree { + Rc::new(LocationTree { id: LocationID::Special(crate::system::specifics::SpecialLocation::Error), invariant: Some(inv), loc_type: LocationType::Inconsistent, left: None, right: None, - } + }) } - pub fn simple(location: &Location, decls: &Declarations, dim: ClockIndex) -> Self { + pub fn simple(location: &Location, decls: &Declarations, dim: ClockIndex) -> Rc { let invariant = if let Some(inv) = &location.invariant { let mut fed = OwnedFederation::universe(dim); fed = apply_constraints_to_state(inv, decls, fed).unwrap(); @@ -60,45 +62,45 @@ impl LocationTree { } else { None }; - LocationTree { + Rc::new(LocationTree { id: LocationID::Simple(location.id.clone()), invariant, loc_type: location.location_type, left: None, right: None, - } + }) } /// This method is used to a build partial [`LocationTree`]. /// A partial [`LocationTree`] means it has a [`LocationID`] that is [`LocationID::AnyLocation`]. /// A partial [`LocationTree`] has `None` in the field `invariant` since a partial [`LocationTree`] /// covers more than one location, and therefore there is no specific `invariant` - pub fn build_any_location_tree() -> Self { - LocationTree { + pub fn build_any_location_tree() -> Rc { + Rc::new(LocationTree { id: LocationID::AnyLocation, invariant: None, loc_type: LocationType::Any, left: None, right: None, - } + }) } //Merge two locations keeping the invariants seperate - pub fn merge_as_quotient(left: &Self, right: &Self) -> Self { + pub fn merge_as_quotient(left: Rc, right: Rc) -> Rc { let id = LocationID::Quotient(Box::new(left.id.clone()), Box::new(right.id.clone())); let loc_type = left.loc_type.combine(right.loc_type); - LocationTree { + Rc::new(LocationTree { id, invariant: None, loc_type, - left: Some(Box::new(left.clone())), - right: Some(Box::new(right.clone())), - } + left: Some(Rc::clone(&left)), + right: Some(Rc::clone(&right)), + }) } //Compose two locations intersecting the invariants - pub fn compose(left: &Self, right: &Self, comp: CompositionType) -> Self { + pub fn compose(left: Rc, right: Rc, comp: CompositionType) -> Rc { let id = match comp { CompositionType::Conjunction => { LocationID::Conjunction(Box::new(left.id.clone()), Box::new(right.id.clone())) @@ -121,13 +123,13 @@ impl LocationTree { let loc_type = left.loc_type.combine(right.loc_type); - LocationTree { + Rc::new(LocationTree { id, invariant, loc_type, - left: Some(Box::new(left.clone())), - right: Some(Box::new(right.clone())), - } + left: Some(Rc::clone(&left)), + right: Some(Rc::clone(&right)), + }) } pub fn get_invariants(&self) -> Option<&OwnedFederation> { @@ -141,12 +143,12 @@ impl LocationTree { fed } - pub fn get_left(&self) -> &LocationTree { - self.left.as_ref().unwrap() + pub fn get_left(&self) -> Rc { + Rc::clone(self.left.as_ref().unwrap()) } - pub fn get_right(&self) -> &LocationTree { - self.right.as_ref().unwrap() + pub fn get_right(&self) -> Rc { + Rc::clone(self.right.as_ref().unwrap()) } pub fn is_initial(&self) -> bool { @@ -162,7 +164,7 @@ impl LocationTree { } /// This function is used when you want to compare [`LocationTree`]s that can contain partial locations. - pub fn compare_partial_locations(&self, other: &LocationTree) -> bool { + pub fn compare_partial_locations(&self, other: Rc) -> bool { match (&self.id, &other.id) { (LocationID::Composition(..), LocationID::Composition(..)) | (LocationID::Conjunction(..), LocationID::Conjunction(..)) diff --git a/src/transition_systems/quotient.rs b/src/transition_systems/quotient.rs index 564e40fc..276ab9db 100644 --- a/src/transition_systems/quotient.rs +++ b/src/transition_systems/quotient.rs @@ -14,6 +14,7 @@ use crate::transition_systems::{ LocationTree, TransitionID, TransitionSystem, TransitionSystemPtr, }; use std::collections::hash_set::HashSet; +use std::rc::Rc; use std::vec; use super::CompositionType; @@ -24,8 +25,8 @@ pub struct Quotient { s: TransitionSystemPtr, inputs: HashSet, outputs: HashSet, - universal_location: LocationTree, - inconsistent_location: LocationTree, + universal_location: Rc, + inconsistent_location: Rc, decls: Declarations, quotient_clock_index: ClockIndex, new_input_name: String, @@ -124,8 +125,8 @@ impl TransitionSystem for Quotient { let (left, right) = self.get_children(); let loc_l = loc.get_left(); let loc_r = loc.get_right(); - let mut bounds_l = left.get_local_max_bounds(loc_l); - let bounds_r = right.get_local_max_bounds(loc_r); + let mut bounds_l = left.get_local_max_bounds(loc_l.as_ref()); + let bounds_r = right.get_local_max_bounds(loc_r.as_ref()); bounds_l.add_bounds(&bounds_r); bounds_l.add_upper(self.quotient_clock_index, 0); bounds_l @@ -136,7 +137,7 @@ impl TransitionSystem for Quotient { self.dim } - fn next_transitions(&self, location: &LocationTree, action: &str) -> Vec { + fn next_transitions(&self, location: Rc, action: &str) -> Vec { assert!(self.actions_contain(action)); let is_input = self.inputs_contain(action); @@ -163,8 +164,12 @@ impl TransitionSystem for Quotient { // As it is not universal or inconsistent it must be a quotient loc let loc_t = location.get_left(); let loc_s = location.get_right(); - let t = self.t.next_transitions_if_available(loc_t, action); - let s = self.s.next_transitions_if_available(loc_s, action); + let t = self + .t + .next_transitions_if_available(Rc::clone(&loc_t), action); + let s = self + .s + .next_transitions_if_available(Rc::clone(&loc_s), action); //Rule 1 if self.s.actions_contain(action) && self.t.actions_contain(action) { @@ -172,12 +177,12 @@ impl TransitionSystem for Quotient { for s_transition in &s { // In the following comments we use ϕ to symbolize the guard of the transition // ϕ_T ∧ Inv(l2_t)[r |-> 0] ∧ Inv(l1_t) ∧ ϕ_S ∧ Inv(l2_s)[r |-> 0] ∧ Inv(l1_s) - let guard_zone = get_allowed_fed(loc_t, t_transition) - .intersection(&get_allowed_fed(loc_s, s_transition)); + let guard_zone = get_allowed_fed(loc_t.as_ref(), t_transition) + .intersection(&get_allowed_fed(loc_s.as_ref(), s_transition)); let target_locations = merge( - &t_transition.target_locations, - &s_transition.target_locations, + Rc::clone(&t_transition.target_locations), + Rc::clone(&s_transition.target_locations), ); //Union of left and right updates @@ -201,9 +206,10 @@ impl TransitionSystem for Quotient { if self.s.actions_contain(action) && !self.t.actions_contain(action) { //Independent S for s_transition in &s { - let guard_zone = get_allowed_fed(loc_s, s_transition); + let guard_zone = get_allowed_fed(&loc_s, s_transition); - let target_locations = merge(loc_t, &s_transition.target_locations); + let target_locations = + merge(Rc::clone(&loc_t), Rc::clone(&s_transition.target_locations)); let updates = s_transition.updates.clone(); transitions.push(Transition { id: TransitionID::Quotient(Vec::new(), vec![s_transition.id.clone()]), @@ -219,7 +225,7 @@ impl TransitionSystem for Quotient { let mut g_s = OwnedFederation::empty(self.dim); for s_transition in &s { - let allowed_fed = get_allowed_fed(loc_s, s_transition); + let allowed_fed = get_allowed_fed(loc_s.as_ref(), s_transition); g_s += allowed_fed; } @@ -251,14 +257,15 @@ impl TransitionSystem for Quotient { //Calculate inverse G_T let mut g_t = OwnedFederation::empty(self.dim); for t_transition in &t { - g_t = g_t.union(&get_allowed_fed(loc_t, t_transition)); + g_t = g_t.union(&get_allowed_fed(loc_t.as_ref(), t_transition)); } let inverse_g_t = g_t.inverse(); for s_transition in &s { // In the following comments we use ϕ to symbolize the guard of the transition // ϕ_S ∧ Inv(l2_s)[r |-> 0] ∧ Inv(l1_s) ∧ ¬G_T - let guard_zone = get_allowed_fed(loc_s, s_transition).intersection(&inverse_g_t); + let guard_zone = + get_allowed_fed(loc_s.as_ref(), s_transition).intersection(&inverse_g_t); let updates = vec![CompiledUpdate { clock_index: self.quotient_clock_index, @@ -279,8 +286,8 @@ impl TransitionSystem for Quotient { //Rule 7 if action == self.new_input_name { - let inverse_t_invariant = get_invariant(loc_t, self.dim).inverse(); - let s_invariant = get_invariant(loc_s, self.dim); + let inverse_t_invariant = get_invariant(loc_t.as_ref(), self.dim).inverse(); + let s_invariant = get_invariant(loc_s.as_ref(), self.dim); let guard_zone = inverse_t_invariant.intersection(&s_invariant); let updates = vec![CompiledUpdate { @@ -298,11 +305,12 @@ impl TransitionSystem for Quotient { //Rule 8 if self.t.actions_contain(action) && !self.s.actions_contain(action) { for t_transition in &t { - let mut guard_zone = get_allowed_fed(loc_t, t_transition); + let mut guard_zone = get_allowed_fed(loc_t.as_ref(), t_transition); guard_zone = loc_s.apply_invariants(guard_zone); - let target_locations = merge(&t_transition.target_locations, loc_s); + let target_locations = + merge(Rc::clone(&t_transition.target_locations), Rc::clone(&loc_s)); let updates = t_transition.updates.clone(); transitions.push(Transition { @@ -328,22 +336,19 @@ impl TransitionSystem for Quotient { fn get_actions(&self) -> HashSet { self.inputs.union(&self.outputs).cloned().collect() } - fn get_initial_location(&self) -> Option { + fn get_initial_location(&self) -> Option> { let (t, s) = self.get_children(); - Some(merge( - &t.get_initial_location()?, - &s.get_initial_location()?, - )) + Some(merge(t.get_initial_location()?, s.get_initial_location()?)) } - fn get_all_locations(&self) -> Vec { + fn get_all_locations(&self) -> Vec> { let mut location_trees = vec![]; let left = self.t.get_all_locations(); let right = self.s.get_all_locations(); for loc_t in &left { for loc_s in &right { - let location = merge(loc_t, loc_s); + let location = merge(Rc::clone(loc_t), Rc::clone(loc_s)); location_trees.push(location); } } @@ -385,12 +390,15 @@ impl TransitionSystem for Quotient { CompositionType::Quotient } - fn construct_location_tree(&self, target: SpecificLocation) -> Result { + fn construct_location_tree( + &self, + target: SpecificLocation, + ) -> Result, String> { match target { SpecificLocation::BranchLocation(left, right, _) => { let left = self.t.construct_location_tree(*left)?; let right = self.s.construct_location_tree(*right)?; - Ok(merge(&left, &right)) + Ok(merge(left, right)) } SpecificLocation::SpecialLocation(SpecialLocation::Universal) => { Ok(self.universal_location.clone()) @@ -403,7 +411,7 @@ impl TransitionSystem for Quotient { } } -fn merge(t: &LocationTree, s: &LocationTree) -> LocationTree { +fn merge(t: Rc, s: Rc) -> Rc { LocationTree::merge_as_quotient(t, s) } diff --git a/src/transition_systems/transition_system.rs b/src/transition_systems/transition_system.rs index 7feb7f65..4e4c2e40 100644 --- a/src/transition_systems/transition_system.rs +++ b/src/transition_systems/transition_system.rs @@ -15,6 +15,7 @@ use std::collections::hash_map::Entry; use std::collections::vec_deque::VecDeque; use std::collections::{hash_set::HashSet, HashMap}; use std::hash::Hash; +use std::rc::Rc; pub type TransitionSystemPtr = Box; pub type Action = String; @@ -63,7 +64,7 @@ pub trait TransitionSystem: DynClone { fn next_transitions_if_available( &self, - location: &LocationTree, + location: Rc, action: &str, ) -> Vec { if self.actions_contain(action) { @@ -73,14 +74,14 @@ pub trait TransitionSystem: DynClone { } } - fn next_transitions(&self, location: &LocationTree, action: &str) -> Vec; + fn next_transitions(&self, location: Rc, action: &str) -> Vec; - fn next_outputs(&self, location: &LocationTree, action: &str) -> Vec { + fn next_outputs(&self, location: Rc, action: &str) -> Vec { debug_assert!(self.get_output_actions().contains(action)); self.next_transitions(location, action) } - fn next_inputs(&self, location: &LocationTree, action: &str) -> Vec { + fn next_inputs(&self, location: Rc, action: &str) -> Vec { debug_assert!(self.get_input_actions().contains(action)); self.next_transitions(location, action) } @@ -103,14 +104,14 @@ pub trait TransitionSystem: DynClone { self.get_actions().contains(action) } - fn get_initial_location(&self) -> Option; + 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_all_locations(&self) -> Vec>; - fn get_location(&self, id: &LocationID) -> Option { + fn get_location(&self, id: &LocationID) -> Option> { self.get_all_locations() .iter() .find(|loc| loc.id == *id) @@ -179,8 +180,12 @@ 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, init_location: LocationTree, graph: &mut ClockAnalysisGraph) { - let mut worklist = VecDeque::from([init_location]); + fn find_edges_and_nodes( + &self, + init_location: Rc, + graph: &mut ClockAnalysisGraph, + ) { + let mut worklist: VecDeque> = VecDeque::from([init_location]); let actions = self.get_actions(); while let Some(location) = worklist.pop_front() { //Constructs a node to represent this location and add it to the graph. @@ -203,7 +208,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 { - for transition in self.next_transitions_if_available(&location, action) { + for transition in self.next_transitions_if_available(Rc::clone(&location), action) { let mut edge = ClockAnalysisEdge { from: location.id.get_unique_string(), to: transition.target_locations.id.get_unique_string(), @@ -238,7 +243,8 @@ pub trait TransitionSystem: DynClone { self.get_analysis_graph().find_clock_redundancies() } - fn construct_location_tree(&self, target: SpecificLocation) -> Result; + fn construct_location_tree(&self, target: SpecificLocation) + -> Result, String>; } /// Returns a [`TransitionSystemPtr`] equivalent to a `composition` of some `components`. From 14a6b0a7ba0c54f495fda8a2c0cd94a919eb1937 Mon Sep 17 00:00:00 2001 From: Simon Rask Date: Sat, 18 Nov 2023 20:14:08 +0100 Subject: [PATCH 3/6] Make the `zone` of a `State` consistent with `StatePair` --- src/data_reader/proto_reader.rs | 2 +- src/model_objects/decision.rs | 2 +- src/model_objects/state.rs | 34 +++++++++++++++---------- src/model_objects/statepair.rs | 12 --------- src/model_objects/transition.rs | 10 +++----- src/system/local_consistency.rs | 4 +-- src/system/reachability.rs | 16 ++++++------ src/system/specifics.rs | 2 +- src/transition_systems/location_tree.rs | 7 ++--- src/transition_systems/quotient.rs | 5 ++-- 10 files changed, 45 insertions(+), 49 deletions(-) diff --git a/src/data_reader/proto_reader.rs b/src/data_reader/proto_reader.rs index 1b8eba09..2b3dc92c 100644 --- a/src/data_reader/proto_reader.rs +++ b/src/data_reader/proto_reader.rs @@ -165,7 +165,7 @@ mod tests { fn assert_state_equals(state1: &State, state2: &State) { assert!( - state1.zone_ref().equals(state2.zone_ref()), + state1.ref_zone().equals(state2.ref_zone()), "Zones are not equal" ); assert_eq!( diff --git a/src/model_objects/decision.rs b/src/model_objects/decision.rs index 376e1327..c097c369 100644 --- a/src/model_objects/decision.rs +++ b/src/model_objects/decision.rs @@ -47,7 +47,7 @@ impl Decision { // Intersect the state zone with the allowed zone state.update_zone(|zone| zone.intersection(&allowed)); // Check if the new state is empty - if !state.zone_ref().is_empty() { + if !state.ref_zone().is_empty() { let next_state = transition.use_transition_alt(&state).expect( "If the allowed zone is non-empty, the transition should lead to a non-empty state", ); diff --git a/src/model_objects/state.rs b/src/model_objects/state.rs index 5b90de13..93841bd1 100644 --- a/src/model_objects/state.rs +++ b/src/model_objects/state.rs @@ -11,14 +11,17 @@ use edbm::zones::OwnedFederation; #[derive(Clone, Debug)] pub struct State { pub decorated_locations: Rc, - zone_sentinel: Option, + zone: Rc, } impl State { - pub fn new(decorated_locations: Rc, zone: OwnedFederation) -> Self { + pub fn new>>( + decorated_locations: Rc, + zone: Z, + ) -> Self { State { decorated_locations, - zone_sentinel: Some(zone), + zone: zone.into(), } } @@ -39,30 +42,35 @@ impl State { Some(State { decorated_locations, - zone_sentinel: Some(fed), + zone: Rc::new(fed), }) } pub fn apply_invariants(&mut self) { - let fed = self.take_zone(); + let fed = self.clone_zone(); let new_fed = self.decorated_locations.apply_invariants(fed); + self.set_zone(new_fed); } - pub fn zone_ref(&self) -> &OwnedFederation { - self.zone_sentinel.as_ref().unwrap() + pub fn clone_zone(&self) -> OwnedFederation { + self.zone.as_ref().clone() + } + + pub fn ref_zone(&self) -> &OwnedFederation { + self.zone.as_ref() } - pub(crate) fn take_zone(&mut self) -> OwnedFederation { - self.zone_sentinel.take().unwrap() + pub fn get_zone(&self) -> Rc { + Rc::clone(&self.zone) } - pub(crate) fn set_zone(&mut self, zone: OwnedFederation) { - self.zone_sentinel = Some(zone); + pub(crate) fn set_zone>>(&mut self, zone: Z) { + self.zone = zone.into(); } pub fn update_zone(&mut self, update: impl FnOnce(OwnedFederation) -> OwnedFederation) { - let fed = self.take_zone(); + let fed = self.clone_zone(); let new_fed = update(fed); self.set_zone(new_fed); } @@ -72,7 +80,7 @@ impl State { return false; } - self.zone_ref().subset_eq(other.zone_ref()) + self.ref_zone().subset_eq(other.ref_zone()) } pub fn get_location(&self) -> &LocationTree { diff --git a/src/model_objects/statepair.rs b/src/model_objects/statepair.rs index 593524a4..8e3cc28d 100644 --- a/src/model_objects/statepair.rs +++ b/src/model_objects/statepair.rs @@ -51,18 +51,6 @@ impl StatePair { self.locations2.clone() } - //Used to allow borrowing both states as mutable - // pub fn get_mut_locations( - // &mut self, - // is_states1: bool, - // ) -> (&mut LocationTree, &mut LocationTree) { - // if is_states1 { - // (&mut self.locations1, &mut self.locations2) - // } else { - // (&mut self.locations2, &mut self.locations1) - // } - // } - pub fn get_locations(&self, is_states1: bool) -> (&LocationTree, &LocationTree) { if is_states1 { (&self.locations1, &self.locations2) diff --git a/src/model_objects/transition.rs b/src/model_objects/transition.rs index b4afe371..d5574f2a 100644 --- a/src/model_objects/transition.rs +++ b/src/model_objects/transition.rs @@ -53,19 +53,17 @@ impl Transition { } pub fn use_transition(&self, state: &mut State) -> bool { - let mut zone = state.take_zone(); + let mut zone = state.clone_zone(); zone = self.apply_guards(zone); if !zone.is_empty() { zone = self.apply_updates(zone).up(); state.decorated_locations = Rc::clone(&self.target_locations); zone = state.decorated_locations.apply_invariants(zone); - if !zone.is_empty() { - state.set_zone(zone); - return true; - } } + let empty = !zone.is_empty(); state.set_zone(zone); - false + + empty } /// Returns the resulting [`State`] when using a transition in the given [`State`] diff --git a/src/system/local_consistency.rs b/src/system/local_consistency.rs index 047ffa94..33781d0d 100644 --- a/src/system/local_consistency.rs +++ b/src/system/local_consistency.rs @@ -107,7 +107,7 @@ pub fn consistency_least_helper( } } - if state.zone_ref().can_delay_indefinitely() { + if state.ref_zone().can_delay_indefinitely() { return Ok(()); } @@ -169,7 +169,7 @@ fn consistency_fully_helper( Ok(()) } else { let last_state = passed_list.last().unwrap(); - match last_state.zone_ref().can_delay_indefinitely() { + match last_state.ref_zone().can_delay_indefinitely() { false => ConsistencyFailure::inconsistent_from(system, &state), true => Ok(()), } diff --git a/src/system/reachability.rs b/src/system/reachability.rs index 3cd095cd..afef26d6 100644 --- a/src/system/reachability.rs +++ b/src/system/reachability.rs @@ -25,13 +25,13 @@ struct SubPath { fn is_trivially_unreachable(start_state: &State, end_state: &State) -> bool { // If any of the zones are empty - if start_state.zone_ref().is_empty() || end_state.zone_ref().is_empty() { + if start_state.ref_zone().is_empty() || end_state.ref_zone().is_empty() { return true; } // 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.decorated_locations.get_invariants() { - if !end_state.zone_ref().has_intersection(invariants) { + if !end_state.ref_zone().has_intersection(invariants) { return true; } } @@ -115,7 +115,7 @@ fn reachability_search( // Push start state to visited state visited_states.insert( start_state.decorated_locations.id.clone(), - vec![start_state.zone_ref().clone()], + vec![start_state.ref_zone().clone()], ); // Push initial state to frontier @@ -125,7 +125,7 @@ fn reachability_search( transition: None, })); - let target_bounds = end_state.zone_ref().get_bounds(); + let target_bounds = end_state.ref_zone().get_bounds(); // Take the first state from the frontier and explore it while let Some(sub_path) = frontier_states.pop_front() { @@ -158,7 +158,7 @@ fn reached_end_state(cur_state: &State, end_state: &State) -> bool { cur_state .decorated_locations .compare_partial_locations(Rc::clone(&end_state.decorated_locations)) - && cur_state.zone_ref().has_intersection(end_state.zone_ref()) + && cur_state.ref_zone().has_intersection(end_state.ref_zone()) } fn take_transition( @@ -178,14 +178,14 @@ fn take_transition( 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) { + if !zone_subset_of_existing_zones(new_state.ref_zone(), existing_zones) { // Remove the smaller zones for this location in visited_states - remove_existing_subsets_of_zone(new_state.zone_ref(), existing_zones); + remove_existing_subsets_of_zone(new_state.ref_zone(), existing_zones); // Add the new zone to the list of zones for this location in visited_states visited_states .get_mut(new_location_id) .unwrap() - .push(new_state.zone_ref().clone()); + .push(new_state.ref_zone().clone()); // Add the new state to the frontier frontier_states.push_back(Rc::new(SubPath { previous_sub_path: Some(Rc::clone(sub_path)), diff --git a/src/system/specifics.rs b/src/system/specifics.rs index 60bf5b35..378348b9 100644 --- a/src/system/specifics.rs +++ b/src/system/specifics.rs @@ -291,7 +291,7 @@ impl SpecificState { let locations = state_specific_location(state, sys); let clock_map = specific_clock_comp_map(sys); - let constraints = state.zone_ref().minimal_constraints(); + let constraints = state.ref_zone().minimal_constraints(); let constraints = SpecificDisjunction::from_disjunction(constraints, &clock_map); Self { locations, diff --git a/src/transition_systems/location_tree.rs b/src/transition_systems/location_tree.rs index 3822f52b..55259804 100644 --- a/src/transition_systems/location_tree.rs +++ b/src/transition_systems/location_tree.rs @@ -136,11 +136,12 @@ impl LocationTree { self.invariant.as_ref() } - pub fn apply_invariants(&self, mut fed: OwnedFederation) -> OwnedFederation { + pub fn apply_invariants(&self, fed: OwnedFederation) -> OwnedFederation { if let Some(inv) = &self.invariant { - fed = fed.intersection(inv); + fed.intersection(inv) + } else { + fed } - fed } pub fn get_left(&self) -> Rc { diff --git a/src/transition_systems/quotient.rs b/src/transition_systems/quotient.rs index 276ab9db..1c51b2c8 100644 --- a/src/transition_systems/quotient.rs +++ b/src/transition_systems/quotient.rs @@ -220,6 +220,7 @@ impl TransitionSystem for Quotient { } } + let universe = OwnedFederation::universe(self.dim); if self.s.get_output_actions().contains(action) { // new Rule 3 (includes rule 4 by de-morgan) let mut g_s = OwnedFederation::empty(self.dim); @@ -230,7 +231,7 @@ impl TransitionSystem for Quotient { } // Rule 5 when Rule 3 applies - let inv_l_s = loc_s.apply_invariants(OwnedFederation::universe(self.dim)); + let inv_l_s = loc_s.apply_invariants(universe); transitions.push(Transition { id: TransitionID::Quotient(Vec::new(), s.iter().map(|t| t.id.clone()).collect()), @@ -240,7 +241,7 @@ impl TransitionSystem for Quotient { }); } else { // Rule 5 when Rule 3 does not apply - let inv_l_s = loc_s.apply_invariants(OwnedFederation::universe(self.dim)); + let inv_l_s = loc_s.apply_invariants(universe); transitions.push(Transition { id: TransitionID::None, From 26e2b9c33fd3944be639bf28fbbbeb111d67d4fa Mon Sep 17 00:00:00 2001 From: Simon Rask Date: Sat, 18 Nov 2023 21:23:21 +0100 Subject: [PATCH 4/6] Fix clippy errors --- src/data_reader/xml_parser.rs | 5 ++++- src/transition_systems/transition_id.rs | 2 +- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/data_reader/xml_parser.rs b/src/data_reader/xml_parser.rs index 219baac0..1734df56 100644 --- a/src/data_reader/xml_parser.rs +++ b/src/data_reader/xml_parser.rs @@ -13,7 +13,10 @@ use std::io::Read; use std::path::Path; pub fn is_xml_project>(project_path: P) -> bool { - project_path.as_ref().ends_with(".xml") + project_path + .as_ref() + .extension() + .is_some_and(|ext| ext == "xml") } ///Used to parse systems described in xml diff --git a/src/transition_systems/transition_id.rs b/src/transition_systems/transition_id.rs index abbcb172..f8738227 100644 --- a/src/transition_systems/transition_id.rs +++ b/src/transition_systems/transition_id.rs @@ -104,8 +104,8 @@ impl TransitionID { paths[component_index].push( transition .iter() - .cloned() .filter(|id| !matches!(id, TransitionID::None)) + .cloned() .collect(), ); } From 5361edf661c349f5754e6e4ec8db9e766bd4e6b8 Mon Sep 17 00:00:00 2001 From: Simon Rask Date: Sat, 18 Nov 2023 21:48:27 +0100 Subject: [PATCH 5/6] Cleanup --- src/model_objects/statepair.rs | 11 +++-------- src/system/refine.rs | 8 ++++---- src/system/save_component.rs | 2 +- src/transition_systems/quotient.rs | 5 ++--- 4 files changed, 10 insertions(+), 16 deletions(-) diff --git a/src/model_objects/statepair.rs b/src/model_objects/statepair.rs index 8e3cc28d..d56ff3aa 100644 --- a/src/model_objects/statepair.rs +++ b/src/model_objects/statepair.rs @@ -72,19 +72,14 @@ impl StatePair { } pub fn extrapolate_max_bounds( - self, + &mut self, sys1: &TransitionSystemPtr, sys2: &TransitionSystemPtr, - ) -> Self { + ) { let mut bounds = sys1.get_local_max_bounds(self.locations1.as_ref()); bounds.add_bounds(&sys2.get_local_max_bounds(self.locations2.as_ref())); - let zone = self.clone_zone().extrapolate_max_bounds(&bounds); - StatePair { - locations1: self.locations1, - locations2: self.locations2, - zone: Rc::new(zone), - } + self.zone = Rc::new(self.clone_zone().extrapolate_max_bounds(&bounds)); } } diff --git a/src/system/refine.rs b/src/system/refine.rs index 0ca3f0ab..c8152631 100644 --- a/src/system/refine.rs +++ b/src/system/refine.rs @@ -148,7 +148,7 @@ pub fn check_refinement(sys1: TransitionSystemPtr, sys2: TransitionSystemPtr) -> if initial_pair.ref_zone().is_empty() { return RefinementFailure::empty_initial(sys1.as_ref(), sys2.as_ref()); } - initial_pair = initial_pair.extrapolate_max_bounds(context.sys1, context.sys2); + initial_pair.extrapolate_max_bounds(context.sys1, context.sys2); debug!("Initial {}", initial_pair); context.waiting_list.put(initial_pair); @@ -361,8 +361,8 @@ fn build_state_pair( //Update locations in states let (locations1, locations2) = ( - transition1.target_locations.clone(), - transition2.target_locations.clone(), + Rc::clone(&transition1.target_locations), + Rc::clone(&transition2.target_locations), ); // Apply invariants on the left side of relation @@ -394,7 +394,7 @@ fn build_state_pair( } let mut new_sp = StatePair::new(left_loc, right_loc, Rc::new(new_sp_zone)); - new_sp = new_sp.extrapolate_max_bounds(context.sys1, context.sys2); + new_sp.extrapolate_max_bounds(context.sys1, context.sys2); if !context.passed_list.has(&new_sp) && !context.waiting_list.has(&new_sp) { debug!("New state {}", new_sp); diff --git a/src/system/save_component.rs b/src/system/save_component.rs index 9a9cb1df..70915755 100644 --- a/src/system/save_component.rs +++ b/src/system/save_component.rs @@ -17,7 +17,7 @@ pub fn combine_components( system: &TransitionSystemPtr, reachability: PruningStrategy, ) -> Component { - let mut location_trees: Vec> = vec![]; + let mut location_trees = vec![]; let mut edges = vec![]; let clocks = get_clock_map(system); match reachability { diff --git a/src/transition_systems/quotient.rs b/src/transition_systems/quotient.rs index 1c51b2c8..276ab9db 100644 --- a/src/transition_systems/quotient.rs +++ b/src/transition_systems/quotient.rs @@ -220,7 +220,6 @@ impl TransitionSystem for Quotient { } } - let universe = OwnedFederation::universe(self.dim); if self.s.get_output_actions().contains(action) { // new Rule 3 (includes rule 4 by de-morgan) let mut g_s = OwnedFederation::empty(self.dim); @@ -231,7 +230,7 @@ impl TransitionSystem for Quotient { } // Rule 5 when Rule 3 applies - let inv_l_s = loc_s.apply_invariants(universe); + let inv_l_s = loc_s.apply_invariants(OwnedFederation::universe(self.dim)); transitions.push(Transition { id: TransitionID::Quotient(Vec::new(), s.iter().map(|t| t.id.clone()).collect()), @@ -241,7 +240,7 @@ impl TransitionSystem for Quotient { }); } else { // Rule 5 when Rule 3 does not apply - let inv_l_s = loc_s.apply_invariants(universe); + let inv_l_s = loc_s.apply_invariants(OwnedFederation::universe(self.dim)); transitions.push(Transition { id: TransitionID::None, From 5c4f6e6840b276331a721d529e9b29b9f6d5de43 Mon Sep 17 00:00:00 2001 From: Simon Rask Date: Tue, 21 Nov 2023 10:22:30 +0100 Subject: [PATCH 6/6] Fix partial state test --- src/tests/reachability/partial_state.rs | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/src/tests/reachability/partial_state.rs b/src/tests/reachability/partial_state.rs index d37186e3..a18496dc 100644 --- a/src/tests/reachability/partial_state.rs +++ b/src/tests/reachability/partial_state.rs @@ -33,7 +33,7 @@ mod reachability_partial_states_test { "L5//_ == L5//L1")] #[test_case(LocationTree::compose(build_location_tree_helper("L5", LocationType::Normal), LocationTree::build_any_location_tree(), CompositionType::Conjunction), LocationTree::compose(LocationTree::build_any_location_tree(), build_location_tree_helper("L1", LocationType::Normal), CompositionType::Conjunction); - "L5_ == _L1")] + "L5&&_ == _&&L1")] #[test_case(LocationTree::compose(build_location_tree_helper("L7", LocationType::Normal), LocationTree::build_any_location_tree(), CompositionType::Composition), LocationTree::compose(build_location_tree_helper("L7", LocationType::Normal), build_location_tree_helper("L1", LocationType::Normal), CompositionType::Composition); "L7||_ == L7||L1")] @@ -58,31 +58,31 @@ mod reachability_partial_states_test { "L2//L6 != L2||L1")] #[test_case(LocationTree::merge_as_quotient(build_location_tree_helper("L7", LocationType::Normal), build_location_tree_helper("L6", LocationType::Normal)), LocationTree::compose(build_location_tree_helper("L2", LocationType::Normal), build_location_tree_helper("L1", LocationType::Normal), CompositionType::Conjunction); - "L7//L6 != L2L1")] + "L7//L6 != L2&&L1")] #[test_case(LocationTree::merge_as_quotient(build_location_tree_helper("L8", LocationType::Normal), LocationTree::build_any_location_tree()), LocationTree::compose(build_location_tree_helper("L2", LocationType::Normal), build_location_tree_helper("L1", LocationType::Normal), CompositionType::Conjunction); - "L8//_ != L2L1")] + "L8//_ != L2&&L1")] #[test_case(LocationTree::build_any_location_tree(), LocationTree::compose(build_location_tree_helper("L6", LocationType::Normal), build_location_tree_helper("L1", LocationType::Normal), CompositionType::Conjunction); - "_ != L6L1")] + "_ != L6&&L1")] #[test_case(LocationTree::build_any_location_tree(), LocationTree::compose(LocationTree::build_any_location_tree(), LocationTree::build_any_location_tree(), CompositionType::Conjunction); - "anylocation _ != __")] + "anylocation _ != _&&_")] #[test_case(LocationTree::compose(build_location_tree_helper("L2", LocationType::Normal), build_location_tree_helper("L4", LocationType::Normal), CompositionType::Conjunction), LocationTree::merge_as_quotient(build_location_tree_helper("L2", LocationType::Normal), build_location_tree_helper("L4", LocationType::Normal)); - "L2L4 != L2\\L4")] + "L2&&L4 != L2\\L4")] #[test_case(LocationTree::compose(LocationTree::compose(LocationTree::build_any_location_tree(), LocationTree::build_any_location_tree(), CompositionType::Composition),build_location_tree_helper("L2", LocationType::Normal), CompositionType::Conjunction), LocationTree::compose(LocationTree::compose(build_location_tree_helper("L2", LocationType::Normal), build_location_tree_helper("L1", LocationType::Normal), CompositionType::Composition),build_location_tree_helper("L2", LocationType::Normal), CompositionType::Composition); - "_||_L2 == L2||L1||L2")] + "_||_&&L2 == L2||L1||L2")] #[test_case(LocationTree::compose(LocationTree::compose(build_location_tree_helper("L2", LocationType::Normal), LocationTree::build_any_location_tree(), CompositionType::Composition),build_location_tree_helper("L2", LocationType::Normal), CompositionType::Conjunction), LocationTree::compose(LocationTree::build_any_location_tree(), LocationTree::build_any_location_tree(), CompositionType::Conjunction); - "L2||_L2 == __")] + "L2||_&&L2 == _&&_")] #[test_case(build_location_tree_helper("L7", LocationType::Normal), build_location_tree_helper("L5", LocationType::Normal); "L7 != L5")] #[test_case(LocationTree::merge_as_quotient(LocationTree::build_any_location_tree(), LocationTree::build_any_location_tree()), LocationTree::compose(build_location_tree_helper("L6", LocationType::Normal), build_location_tree_helper("L25", LocationType::Normal), CompositionType::Conjunction); - "_//_ != L6L25")] + "_//_ != L6&&L25")] #[test_case(build_location_tree_helper("_L1", LocationType::Normal), build_location_tree_helper("L1", LocationType::Normal); "_L1 != L1")]