Disable lemmas in DeliveryDrone_CASE_v2

Enable them again to reduce analysis time in resource-limited machines
ge-high-assurance · Feb 5, 2021 · 5f9610f · 5f9610f
1 parent a20aa59
commit 5f9610f
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/models/DeliveryDrone_CASE_v2/DeliveryDrone.aadl b/models/DeliveryDrone_CASE_v2/DeliveryDrone.aadl
@@ -609,10 +609,10 @@ public
 
 			eq started: bool = (delivery_status <> Agree_Constants::NOT_STARTED_STATUS);
 
-			guarantee "L1: Auxiliary lemma": not Agree_Nodes::InRestrictedArea(probe_delivery_location);
-			guarantee "L2: Auxiliary lemma": probe_delivery_location = most_recent_delivery_location;
+			--guarantee "L1: Auxiliary lemma": not Agree_Nodes::InRestrictedArea(probe_delivery_location);
+			--guarantee "L2: Auxiliary lemma": probe_delivery_location = most_recent_delivery_location;
 
-			guarantee "L3: Auxiliary lemma": probe_fly_cmd => probe_delivery_location=most_recent_delivery_location;
+			--guarantee "L3: Auxiliary lemma": probe_fly_cmd => probe_delivery_location=most_recent_delivery_location;
 
 			guarantee "P7: The drone never initiates packet release to an off-limits location":
 				started => not Agree_Nodes::InRestrictedArea(probe_delivery_location);