Fixed the issue with parsing universal locations into the reachabilit…

…y query (#142)

This commit solves parsing of universal and inconsistent locations.
The previous commits in main can make the internal representation for any single location from a query.
However, when combining components, it only support locations that are not universal or inconsistent.

We have add a extra field `add` in the enum type `LocationType` to represent any location in for the particular component.

We have refactored `get_state` function and spilled some of it content into some sub functions.

The method `compare_partial_locations` in `LocationID` is removed and moved to `LocationTuple` with extra addition code to handle comparing of universal or inconsistent locations

The method `get_location` in `TransitionSystem` returns the `LocationTuple` for the given `LocationID` input argument

The method 'get_combined_decls' combines the individual declaration of components into one declaration. This method is used for `apply_constraints_to_state` in extract_state.rs

src/DataReader/serialization.rs

@@ -354,6 +354,7 @@ where
         LocationType::Initial => serializer.serialize_str("INITIAL"),
         LocationType::Universal => serializer.serialize_str("UNIVERSAL"),
         LocationType::Inconsistent => serializer.serialize_str("INCONSISTENT"),
+        LocationType::Any => unreachable!(),
     }
 }
 

src/ModelObjects/component.rs

@@ -605,6 +605,7 @@ pub enum LocationType {
     Initial,
     Universal,
     Inconsistent,
+    Any,
 }
 
 #[derive(Debug, Deserialize, Serialize, Clone, PartialEq, Eq)]

src/System/extract_state.rs

@@ -1,13 +1,10 @@
-use std::collections::HashMap;
-
 use edbm::zones::OwnedFederation;
 
-use crate::component::Declarations;
 use crate::extract_system_rep::SystemRecipe;
 use crate::EdgeEval::constraint_applyer::apply_constraints_to_state;
 use crate::ModelObjects::component::State;
-use crate::ModelObjects::representations::QueryExpression;
-use crate::TransitionSystems::{LocationID, LocationTuple, TransitionSystemPtr};
+use crate::ModelObjects::representations::{BoolExpression, QueryExpression};
+use crate::TransitionSystems::{CompositionType, LocationID, LocationTuple, TransitionSystemPtr};
 use std::slice::Iter;
 
 /// This function takes a [`QueryExpression`], the system recipe, and the transitionsystem -
@@ -21,104 +18,88 @@ pub fn get_state(
     machine: &SystemRecipe,
     system: &TransitionSystemPtr,
 ) -> Result<State, String> {
-    match state_query {
-        QueryExpression::State(loc, clock) => {
-            let mut locations: Vec<&str> = Vec::new();
-
-            for location in loc {
-                match location.as_ref() {
-                    QueryExpression::LocName(name) => locations.push(name),
-                    _ => panic!(),
-                };
-            }
-
-            let locationtuple = build_location_tuple(&locations, machine, system)?;
+    if let QueryExpression::State(loc, clock) = state_query {
+        let mut locations: Vec<&str> = Vec::new();
 
-            let zone = if let Some(clock_constraints) = clock {
-                let mut clocks = HashMap::new();
-                for decl in system.get_decls() {
-                    clocks.extend(decl.clocks.clone());
-                }
-
-                let declarations = Declarations {
-                    ints: HashMap::new(),
-                    clocks,
-                };
-
-                match apply_constraints_to_state(
-                    clock_constraints,
-                    &declarations,
-                    OwnedFederation::universe(system.get_dim()),
-                ) {
-                    Ok(zone) => zone,
-                    Err(wrong_clock) => {
-                        return Err(format!(
-                            "Clock {} does not exist in the transition system",
-                            wrong_clock
-                        ))
-                    }
-                }
-            } else {
-                OwnedFederation::universe(system.get_dim())
+        for location in loc {
+            match location.as_ref() {
+                QueryExpression::LocName(name) => locations.push(name),
+                _ => unreachable!(),
             };
-
-            Ok(State::create(locationtuple, zone))
         }
-        _ => panic!("Expected QueryExpression::State, but got {:?}", state_query),
+
+        Ok(State::create(
+            build_location_tuple(&mut locations.iter(), machine, system)?,
+            create_zone_given_constraints(clock.as_deref(), system)?,
+        ))
+    } else {
+        Err(format!(
+            "The following information \"{}\" could not be used to create a State",
+            state_query.pretty_string()
+        ))
     }
 }
 
+fn create_zone_given_constraints(
+    constraints: Option<&BoolExpression>,
+    system: &TransitionSystemPtr,
+) -> Result<OwnedFederation, String> {
+    constraints
+        .map_or_else(
+            || Ok(OwnedFederation::universe(system.get_dim())),
+            |clock| {
+                apply_constraints_to_state(
+                    clock,
+                    &system.get_combined_decls(),
+                    OwnedFederation::universe(system.get_dim()),
+                )
+            },
+        )
+        .map_err(|clock| format!("Clock {} does not exist in the transition system", clock))
+}
+
 fn build_location_tuple(
-    locations: &[&str],
+    locations: &mut Iter<&str>,
     machine: &SystemRecipe,
     system: &TransitionSystemPtr,
 ) -> Result<LocationTuple, String> {
-    let location_id = get_location_id(&mut locations.iter(), machine);
-
-    system
-        .get_all_locations()
-        .iter()
-        .find(|loc| loc.id.compare_partial_locations(&location_id))
-        .ok_or_else(|| {
-            format!(
-                "{} is not a location in the transition system ",
-                location_id
-            )
-        })
-        .map(|location_tuple| {
-            if !location_id.is_partial_location() {
-                location_tuple.clone()
-            } else {
-                LocationTuple::create_partial_location(location_id)
-            }
-        })
-}
-
-fn get_location_id(locations: &mut Iter<&str>, machine: &SystemRecipe) -> LocationID {
     match machine {
-        SystemRecipe::Composition(left, right) => LocationID::Composition(
-            box_location_id(locations, left),
-            box_location_id(locations, right),
-        ),
-        SystemRecipe::Conjunction(left, right) => LocationID::Conjunction(
-            box_location_id(locations, left),
-            box_location_id(locations, right),
-        ),
-        SystemRecipe::Quotient(left, right, ..) => LocationID::Quotient(
-            box_location_id(locations, left),
-            box_location_id(locations, right),
-        ),
+        SystemRecipe::Composition(left, right) => {
+            let (left_system, right_system) = system.get_children();
+            Ok(LocationTuple::compose(
+                &build_location_tuple(locations, left, left_system)?,
+                &build_location_tuple(locations, right, right_system)?,
+                CompositionType::Composition,
+            ))
+        }
+        SystemRecipe::Conjunction(left, right) => {
+            let (left_system, right_system) = system.get_children();
+            Ok(LocationTuple::compose(
+                &build_location_tuple(locations, left, left_system)?,
+                &build_location_tuple(locations, right, right_system)?,
+                CompositionType::Conjunction,
+            ))
+        }
+        SystemRecipe::Quotient(left, right, ..) => {
+            let (left_system, right_system) = system.get_children();
+            Ok(LocationTuple::merge_as_quotient(
+                &build_location_tuple(locations, left, left_system)?,
+                &build_location_tuple(locations, right, right_system)?,
+            ))
+        }
         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 {
-                location_id: str.to_string(),
-                component_id: Some(component.get_name().to_owned()),
-            },
+            "_" => Ok(LocationTuple::build_any_location_tuple()),
+            str => system
+                .get_location(&LocationID::Simple {
+                    location_id: str.to_string(),
+                    component_id: Some(component.get_name().clone()),
+                })
+                .ok_or(format!(
+                    "Location {} does not exist in the component {}",
+                    str,
+                    component.get_name()
+                )),
         },
     }
 }
-
-fn box_location_id(left: &mut Iter<&str>, right: &SystemRecipe) -> Box<LocationID> {
-    Box::new(get_location_id(left, right))
-}

src/System/extract_system_rep.rs

@@ -46,7 +46,7 @@ pub fn create_executable_query<'a>(
 
                 let start_state: State = if let Some(state) = start.as_ref() {
                     validate_reachability_input(&machine, state)?;
-                    let state = get_state(state, &machine, &transition_system)?;
+                    let state = get_state(state, &machine, &transition_system).map_err(|err| format!("Invalid Start state: {}",err))?;
                     if state.get_location().id.is_partial_location() {
                         return Err("Start state is a partial state, which it must not be".into())
                     }
@@ -59,7 +59,7 @@ pub fn create_executable_query<'a>(
                     }
                 };
 
-                let end_state: State = get_state(end, &machine, &transition_system)?;
+                let end_state: State = get_state(end, &machine, &transition_system).map_err(|err| format!("Invalid End state: {}",err))?;
 
                 Ok(Box::new(ReachabilityExecutor {
                     transition_system,

src/System/reachability.rs

@@ -1,5 +1,6 @@
 use edbm::zones::OwnedFederation;
 
+use crate::component::LocationType;
 use crate::ModelObjects::component::{State, Transition};
 use crate::TransitionSystems::{LocationID, TransitionSystem};
 use std::collections::HashMap;
@@ -17,14 +18,26 @@ struct SubPath {
     transition: Option<Transition>,
 }
 
-fn is_trivially_unreachable(end_state: &State, _system: &dyn TransitionSystem) -> bool {
+fn is_trivially_unreachable(start_state: &State, end_state: &State) -> bool {
     if let Some(invariants) = end_state.get_location().get_invariants() {
         if !end_state.zone_ref().has_intersection(invariants) {
             return true;
         }
     }
+
+    if matches!(
+        start_state.decorated_locations.loc_type,
+        LocationType::Universal | LocationType::Inconsistent
+    ) && !start_state
+        .decorated_locations
+        .compare_partial_locations(&end_state.decorated_locations)
+    {
+        return true;
+    }
+
     false
 }
+
 ///# Find path
 ///
 /// Returns a path from a start state to an end state in a transition system.
@@ -61,7 +74,7 @@ pub fn find_path(
     end_state: State,
     system: &dyn TransitionSystem,
 ) -> Result<Path, String> {
-    if is_trivially_unreachable(&end_state, system) {
+    if is_trivially_unreachable(&start_state, &end_state) {
         return Ok(Path {
             path: None,
             was_reachable: false,
@@ -127,8 +140,7 @@ fn search_algorithm(start_state: &State, end_state: &State, system: &dyn Transit
 fn reached_end_state(cur_state: &State, end_state: &State) -> bool {
     cur_state
         .get_location()
-        .id
-        .compare_partial_locations(&end_state.get_location().id)
+        .compare_partial_locations(end_state.get_location())
         && cur_state.zone_ref().has_intersection(end_state.zone_ref())
 }
 
@@ -144,12 +156,15 @@ fn take_transition(
         new_state.extrapolate_max_bounds(system); // Ensures the bounds cant grow infinitely, avoiding infinite loops in an edge case TODO: does not take end state zone into account, leading to a very rare edge case
         let new_location_id = &new_state.get_location().id;
         let existing_zones = visited_states.entry(new_location_id.clone()).or_default();
+
         if !zone_subset_of_existing_zones(new_state.zone_ref(), existing_zones) {
             remove_existing_subsets_of_zone(new_state.zone_ref(), existing_zones);
+
             visited_states
                 .get_mut(new_location_id)
                 .unwrap()
                 .push(new_state.zone_ref().clone());
+
             frontier_states.push(Rc::new(SubPath {
                 previous_sub_path: Some(Rc::clone(sub_path)),
                 destination_state: new_state,
@@ -180,10 +195,9 @@ fn remove_existing_subsets_of_zone(
     existing_zones.retain(|existing_zone| !existing_zone.subset_eq(new_zone));
 }
 /// Makes the path from the last subpath
-fn make_path(sub_path: Rc<SubPath>) -> Path {
+fn make_path(mut sub_path: Rc<SubPath>) -> Path {
     let mut path: Vec<Transition> = Vec::new();
 
-    let mut sub_path = sub_path;
     while sub_path.previous_sub_path.is_some() {
         path.push(sub_path.transition.clone().unwrap());
         sub_path = Rc::clone(sub_path.previous_sub_path.as_ref().unwrap());

src/TransitionSystems/compiled_component.rs

@@ -201,4 +201,12 @@ impl TransitionSystem for CompiledComponent {
     fn get_dim(&self) -> ClockIndex {
         self.dim
     }
+
+    fn get_combined_decls(&self) -> Declarations {
+        self.comp_info.declarations.clone()
+    }
+
+    fn get_location(&self, id: &LocationID) -> Option<LocationTuple> {
+        self.locations.get(id).cloned()
+    }
 }

src/TransitionSystems/location_id.rs

@@ -36,65 +36,6 @@ impl LocationID {
         }
     }
 
-    /// This function is used when you want to compare a [`LocationID`] containing a partial location [`LocationID::AnyLocation`] with another [`LocationID`].
-    /// [`LocationID::AnyLocation`] should always be true when compared to [`LocationID::Simple`]
-    /// ```
-    /// use reveaal::TransitionSystems::LocationID;
-    /// // Make two locations where `a` has LocationID::AnyLocation
-    /// 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 { 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));
-    /// ```
-    pub fn compare_partial_locations(&self, other: &Self) -> bool {
-        match (self, other) {
-            (
-                LocationID::Composition(self_left, self_right),
-                LocationID::Composition(other_left, other_right),
-            )
-            | (
-                LocationID::Conjunction(self_left, self_right),
-                LocationID::Conjunction(other_left, other_right),
-            )
-            | (
-                LocationID::Quotient(self_left, self_right),
-                LocationID::Quotient(other_left, other_right),
-            ) => {
-                self_left.compare_partial_locations(other_left)
-                    && self_right.compare_partial_locations(other_right)
-            }
-            (
-                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,
-        }
-    }
-
     /// It check whether the [`LocationID`] is a partial location by search through [`LocationID`] structure and see if there is any [`LocationID::AnyLocation`]
     pub fn is_partial_location(&self) -> bool {
         match self {
@@ -103,10 +44,7 @@ impl LocationID {
             | LocationID::Quotient(left, right) => {
                 left.is_partial_location() || right.is_partial_location()
             }
-            LocationID::Simple {
-                location_id: _,
-                component_id: _,
-            } => false,
+            LocationID::Simple { .. } => false,
             LocationID::AnyLocation() => true,
         }
     }