Skip to content

Commit

Permalink
Merge pull request #21 from ECDAR-AAU-SW-P5/reference-counting-locati…
Browse files Browse the repository at this point in the history
…ontree-statepair-4

Reference counting locationtree statepair group4
  • Loading branch information
SimonRask authored Dec 8, 2023
2 parents 6cb4f1a + 5c4f6e6 commit 89a24f6
Show file tree
Hide file tree
Showing 23 changed files with 350 additions and 301 deletions.
7 changes: 4 additions & 3 deletions src/data_reader/proto_reader.rs
Original file line number Diff line number Diff line change
@@ -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;
Expand Down Expand Up @@ -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<LocationTree> {
let target: SpecificLocation = location_tree.into();

system.construct_location_tree(target).unwrap()
Expand Down Expand Up @@ -164,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!(
Expand Down Expand Up @@ -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);
Expand Down
5 changes: 4 additions & 1 deletion src/data_reader/xml_parser.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,10 @@ use std::io::Read;
use std::path::Path;

pub fn is_xml_project<P: AsRef<Path>>(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
Expand Down
10 changes: 7 additions & 3 deletions src/model_objects/decision.rs
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
use std::rc::Rc;

use crate::model_objects::{State, Transition};
use crate::transition_systems::TransitionSystemPtr;

Expand All @@ -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<Decision> {
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))
Expand Down Expand Up @@ -44,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",
);
Expand All @@ -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)
{
Expand Down
44 changes: 27 additions & 17 deletions src/model_objects/state.rs
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
use std::rc::Rc;

use crate::transition_systems::{LocationTree, TransitionSystem};
use edbm::util::bounds::Bounds;
use edbm::util::constraints::ClockIndex;
Expand All @@ -8,15 +10,18 @@ use edbm::zones::OwnedFederation;
// This should probably be refactored as it causes unnecessary confusion
#[derive(Clone, Debug)]
pub struct State {
pub decorated_locations: LocationTree,
zone_sentinel: Option<OwnedFederation>,
pub decorated_locations: Rc<LocationTree>,
zone: Rc<OwnedFederation>,
}

impl State {
pub fn new(decorated_locations: LocationTree, zone: OwnedFederation) -> Self {
pub fn new<Z: Into<Rc<OwnedFederation>>>(
decorated_locations: Rc<LocationTree>,
zone: Z,
) -> Self {
State {
decorated_locations,
zone_sentinel: Some(zone),
zone: zone.into(),
}
}

Expand All @@ -25,7 +30,7 @@ impl State {
}

pub fn from_location(
decorated_locations: LocationTree,
decorated_locations: Rc<LocationTree>,
dimensions: ClockIndex,
) -> Option<Self> {
let mut fed = OwnedFederation::init(dimensions);
Expand All @@ -37,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<OwnedFederation> {
Rc::clone(&self.zone)
}

pub(crate) fn set_zone(&mut self, zone: OwnedFederation) {
self.zone_sentinel = Some(zone);
pub(crate) fn set_zone<Z: Into<Rc<OwnedFederation>>>(&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);
}
Expand All @@ -70,15 +80,15 @@ 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 {
&self.decorated_locations
}

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

Expand All @@ -87,7 +97,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))
}
Expand Down
68 changes: 36 additions & 32 deletions src/model_objects/statepair.rs
Original file line number Diff line number Diff line change
@@ -1,46 +1,54 @@
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<OwnedFederation>,
pub locations1: Rc<LocationTree>,
pub locations2: Rc<LocationTree>,
zone: Rc<OwnedFederation>,
}

impl StatePair {
pub fn from_locations(
dimensions: usize,
locations1: LocationTree,
locations2: LocationTree,
locations1: Rc<LocationTree>,
locations2: Rc<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_sentinel: Some(zone),
zone: Rc::new(zone),
}
}

pub fn get_locations1(&self) -> &LocationTree {
&self.locations1
pub fn new(
locations1: Rc<LocationTree>,
locations2: Rc<LocationTree>,
zone: Rc<OwnedFederation>,
) -> Self {
StatePair {
locations1,
locations2,
zone,
}
}

pub fn get_locations2(&self) -> &LocationTree {
&self.locations2
pub fn get_locations1(&self) -> Rc<LocationTree> {
self.locations1.clone()
}

//Used to allow borrowing both states as mutable
pub fn get_mut_states(&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_locations2(&self) -> Rc<LocationTree> {
self.locations2.clone()
}

pub fn get_locations(&self, is_states1: bool) -> (&LocationTree, &LocationTree) {
Expand All @@ -52,30 +60,26 @@ 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()
self.zone.as_ref()
}

pub fn take_zone(&mut self) -> OwnedFederation {
self.zone_sentinel.take().unwrap()
}

pub fn set_zone(&mut self, zone: OwnedFederation) {
self.zone_sentinel = Some(zone);
pub fn get_zone(&self) -> Rc<OwnedFederation> {
Rc::clone(&self.zone)
}

pub fn extrapolate_max_bounds(
&mut self,
sys1: &TransitionSystemPtr,
sys2: &TransitionSystemPtr,
) {
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 mut bounds = sys1.get_local_max_bounds(self.locations1.as_ref());
bounds.add_bounds(&sys2.get_local_max_bounds(self.locations2.as_ref()));

self.zone = Rc::new(self.clone_zone().extrapolate_max_bounds(&bounds));
}
}

Expand Down
Loading

0 comments on commit 89a24f6

Please sign in to comment.