Merge pull request #108 from Ecdar-SW5/add_component_to_locationID

Add component id to locationID

src/ModelObjects/component.rs

@@ -652,7 +652,12 @@ impl Transition {
 
         let target_loc_name = &edge.target_location;
         let target_loc = comp.get_location_by_name(target_loc_name);
-        let target_locations = LocationTuple::simple(target_loc, comp.get_declarations(), dim);
+        let target_locations = LocationTuple::simple(
+            target_loc,
+            Some(comp.get_name().to_owned()),
+            comp.get_declarations(),
+            dim,
+        );
 
         let mut compiled_updates = vec![];
         if let Some(updates) = edge.get_update() {

src/System/extract_state.rs

@@ -106,10 +106,13 @@ fn get_location_id(locations: &mut Iter<&str>, machine: &SystemRecipe) -> Locati
             Box::new(get_location_id(locations, left)),
             Box::new(get_location_id(locations, right)),
         ),
-        SystemRecipe::Component(..) => match locations.next().unwrap().trim() {
+        SystemRecipe::Component(component) => match locations.next().unwrap().trim() {
             // It is ensured .next() will not give a None, since the number of location is same as number of component. This is also being checked in validate_reachability_input function, that is called before get_state
             "_" => LocationID::AnyLocation(),
-            str => LocationID::Simple(str.to_string()),
+            str => LocationID::Simple {
+                location_id: str.to_string(),
+                component_id: Some(component.get_name().to_owned()),
+            },
         },
     }
 }

src/System/pruning.rs

@@ -499,7 +499,12 @@ fn is_immediately_inconsistent(
     comp: &Component,
     dimensions: ClockIndex,
 ) -> bool {
-    let loc = LocationTuple::simple(location, &comp.declarations, dimensions);
+    let loc = LocationTuple::simple(
+        location,
+        Some(comp.get_name().to_owned()),
+        &comp.declarations,
+        dimensions,
+    );
 
     loc.is_inconsistent()
 

src/TransitionSystems/compiled_component.rs

@@ -48,7 +48,12 @@ impl CompiledComponent {
             .get_locations()
             .iter()
             .map(|loc| {
-                let tuple = LocationTuple::simple(loc, component.get_declarations(), dim);
+                let tuple = LocationTuple::simple(
+                    loc,
+                    Some(component.get_name().to_owned()),
+                    component.get_declarations(),
+                    dim,
+                );
                 (tuple.id.clone(), tuple)
             })
             .collect();
@@ -57,7 +62,10 @@ impl CompiledComponent {
             locations.keys().map(|k| (k.clone(), vec![])).collect();
 
         for edge in component.get_edges() {
-            let id = LocationID::Simple(edge.source_location.clone());
+            let id = LocationID::Simple {
+                location_id: edge.source_location.clone(),
+                component_id: Some(component.get_name().to_owned()),
+            };
             let transition = Transition::from(&component, edge, dim);
             location_edges
                 .get_mut(&id)

src/TransitionSystems/location_id.rs

@@ -7,7 +7,11 @@ pub enum LocationID {
     Conjunction(Box<LocationID>, Box<LocationID>),
     Composition(Box<LocationID>, Box<LocationID>),
     Quotient(Box<LocationID>, Box<LocationID>),
-    Simple(String),
+    /// Represents the potentially complete identifier of a location
+    Simple {
+        location_id: String,
+        component_id: Option<String>,
+    },
     /// Used for representing a partial state and it is generated when a location's name is set as `_`
     AnyLocation(),
 }
@@ -37,11 +41,11 @@ impl LocationID {
     /// ```
     /// use reveaal::TransitionSystems::LocationID;
     /// // Make two locations where `a` has LocationID::AnyLocation
-    /// let a = LocationID::Quotient(Box::new(LocationID::Simple("L5".to_string())),
+    /// let a = LocationID::Quotient(Box::new(LocationID::Simple { location_id: "L5".to_string(),  component_id: None } ),
     ///                              Box::new(LocationID::AnyLocation()));
     ///
-    /// let b = LocationID::Quotient(Box::new(LocationID::Simple("L5".to_string())),
-    ///                              Box::new(LocationID::Simple("L1".to_string())));
+    /// let b = LocationID::Quotient(Box::new(LocationID::Simple { location_id: "L5".to_string(),  component_id: None } ),
+    ///                              Box::new(LocationID::Simple { location_id: "L1".to_string(),  component_id: None } ));
     ///
     /// assert!(a.compare_partial_locations(&b));
     /// ```
@@ -62,10 +66,31 @@ impl LocationID {
                 self_left.compare_partial_locations(other_left)
                     && self_right.compare_partial_locations(other_right)
             }
-            (LocationID::AnyLocation(), LocationID::Simple(_))
-            | (LocationID::Simple(_), LocationID::AnyLocation())
-            | (LocationID::AnyLocation(), LocationID::AnyLocation()) => true,
-            (LocationID::Simple(loc1), LocationID::Simple(loc2)) => loc1 == loc2,
+            (
+                LocationID::AnyLocation(),
+                LocationID::Simple {
+                    location_id: _,
+                    component_id: _,
+                },
+            )
+            | (
+                LocationID::Simple {
+                    location_id: _,
+                    component_id: _,
+                },
+                LocationID::AnyLocation(),
+            ) => true,
+            (LocationID::AnyLocation(), LocationID::AnyLocation()) => true,
+            (
+                LocationID::Simple {
+                    location_id: location_id_1,
+                    component_id: component_id_1,
+                },
+                LocationID::Simple {
+                    location_id: location_id_2,
+                    component_id: component_id_2,
+                },
+            ) => location_id_1 == location_id_2 && component_id_1 == component_id_2,
             (_, _) => false,
         }
     }
@@ -78,7 +103,10 @@ impl LocationID {
             | LocationID::Quotient(left, right) => {
                 left.is_partial_location() || right.is_partial_location()
             }
-            LocationID::Simple(_) => false,
+            LocationID::Simple {
+                location_id: _,
+                component_id: _,
+            } => false,
             LocationID::AnyLocation() => true,
         }
     }
@@ -97,7 +125,10 @@ impl From<QueryExpression> for LocationID {
                 LocationID::Quotient(Box::new((*left).into()), Box::new((*right).into()))
             }
             QueryExpression::Parentheses(inner) => (*inner).into(),
-            QueryExpression::VarName(name) => LocationID::Simple(name),
+            QueryExpression::VarName(name) => LocationID::Simple {
+                location_id: name,
+                component_id: None,
+            },
             _ => panic!(
                 "Cannot convert queryexpression with {:?} to LocationID",
                 item
@@ -110,43 +141,64 @@ impl Display for LocationID {
     fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
         match self {
             LocationID::Conjunction(left, right) => {
-                match *(*left) {
+                match **left {
                     LocationID::Conjunction(_, _) => write!(f, "{}", (*left))?,
-                    LocationID::Simple(_) => write!(f, "{}", (*left))?,
+                    LocationID::Simple {
+                        location_id: _,
+                        component_id: _,
+                    } => write!(f, "{}", (*left))?,
                     _ => write!(f, "({})", (*left))?,
                 };
                 write!(f, "&&")?;
-                match *(*right) {
+                match **right {
                     LocationID::Conjunction(_, _) => write!(f, "{}", (*right))?,
-                    LocationID::Simple(_) => write!(f, "{}", (*right))?,
+                    LocationID::Simple {
+                        location_id: _,
+                        component_id: _,
+                    } => write!(f, "{}", (*right))?,
                     _ => write!(f, "({})", (*right))?,
                 };
             }
             LocationID::Composition(left, right) => {
-                match *(*left) {
+                match **left {
                     LocationID::Composition(_, _) => write!(f, "{}", (*left))?,
-                    LocationID::Simple(_) => write!(f, "{}", (*left))?,
+                    LocationID::Simple {
+                        location_id: _,
+                        component_id: _,
+                    } => write!(f, "{}", (*left))?,
                     _ => write!(f, "({})", (*left))?,
                 };
                 write!(f, "||")?;
-                match *(*right) {
+                match **right {
                     LocationID::Composition(_, _) => write!(f, "{}", (*right))?,
-                    LocationID::Simple(_) => write!(f, "{}", (*right))?,
+                    LocationID::Simple {
+                        location_id: _,
+                        component_id: _,
+                    } => write!(f, "{}", (*right))?,
                     _ => write!(f, "({})", (*right))?,
                 };
             }
             LocationID::Quotient(left, right) => {
-                match *(*left) {
-                    LocationID::Simple(_) => write!(f, "{}", (*left))?,
+                match **left {
+                    LocationID::Simple {
+                        location_id: _,
+                        component_id: _,
+                    } => write!(f, "{}", (*left))?,
                     _ => write!(f, "({})", (*left))?,
                 };
                 write!(f, "\\\\")?;
-                match *(*right) {
-                    LocationID::Simple(_) => write!(f, "{}", (*right))?,
+                match **right {
+                    LocationID::Simple {
+                        location_id: _,
+                        component_id: _,
+                    } => write!(f, "{}", (*right))?,
                     _ => write!(f, "({})", (*right))?,
                 };
             }
-            LocationID::Simple(name) => write!(f, "{}", name)?,
+            LocationID::Simple {
+                location_id,
+                component_id: _,
+            } => write!(f, "{}", location_id)?,
             LocationID::AnyLocation() => write!(f, "_")?,
         }
         Ok(())

src/TransitionSystems/location_tuple.rs

@@ -30,7 +30,12 @@ impl PartialEq for LocationTuple {
 }
 
 impl LocationTuple {
-    pub fn simple(location: &Location, decls: &Declarations, dim: ClockIndex) -> Self {
+    pub fn simple(
+        location: &Location,
+        component_id: Option<String>,
+        decls: &Declarations,
+        dim: ClockIndex,
+    ) -> Self {
         let invariant = if let Some(inv) = location.get_invariant() {
             let mut fed = OwnedFederation::universe(dim);
             fed = apply_constraints_to_state(inv, decls, fed).unwrap();
@@ -39,7 +44,10 @@ impl LocationTuple {
             None
         };
         LocationTuple {
-            id: LocationID::Simple(location.get_id().clone()),
+            id: LocationID::Simple {
+                location_id: location.get_id().clone(),
+                component_id,
+            },
             invariant,
             loc_type: location.get_location_type().clone(),
             left: None,

src/TransitionSystems/quotient.rs

@@ -192,9 +192,9 @@ impl TransitionSystem for Quotient {
         let s = self.S.next_transitions_if_available(loc_s, action);
 
         let inconsistent_location =
-            LocationTuple::simple(&self.inconsistent_location, &self.decls, self.dim);
+            LocationTuple::simple(&self.inconsistent_location, None, &self.decls, self.dim);
         let universal_location =
-            LocationTuple::simple(&self.universal_location, &self.decls, self.dim);
+            LocationTuple::simple(&self.universal_location, None, &self.decls, self.dim);
 
         //Rule 1
         if self.S.actions_contain(action) && self.T.actions_contain(action) {
@@ -350,8 +350,9 @@ impl TransitionSystem for Quotient {
         }
 
         let inconsistent =
-            LocationTuple::simple(&self.inconsistent_location, &self.decls, self.dim);
-        let universal = LocationTuple::simple(&self.universal_location, &self.decls, self.dim);
+            LocationTuple::simple(&self.inconsistent_location, None, &self.decls, self.dim);
+        let universal =
+            LocationTuple::simple(&self.universal_location, None, &self.decls, self.dim);
 
         location_tuples.push(inconsistent);
         location_tuples.push(universal);