Copy of DeliveryDrone model to reproduce CRV results described in Wiki

models/DeliveryDrone_CRV/.project

@@ -0,0 +1,17 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<projectDescription>
+	<name>DeliveryDrone_CRV</name>
+	<comment></comment>
+	<projects>
+	</projects>
+	<buildSpec>
+		<buildCommand>
+			<name>org.eclipse.xtext.ui.shared.xtextBuilder</name>
+			<arguments>
+			</arguments>
+		</buildCommand>
+	</buildSpec>
+	<natures>
+		<nature>org.eclipse.xtext.ui.shared.xtextNature</nature>
+	</natures>
+</projectDescription>

models/DeliveryDrone_CRV/Agree_Constants.aadl

@@ -0,0 +1,23 @@
+package Agree_Constants
+public
+	with Data_Types;
+
+	annex agree {**
+
+		const ITEM_VALUE_THRESHOLD: real = 100.0;
+
+		const WAITING_CONFIRMATION_THRESHOLD: int = 10;
+
+		const MAXIMUM_NUMBER_OF_RETRIES: int = 3;
+
+		-- enums
+		const RELEASE_PACKAGE_CMD: Data_Types::PackageDeliveryCommand = enum(Data_Types::PackageDeliveryCommand, RELEASE_PACKAGE);
+		const ABORT_DELIVERY_CMD: Data_Types::PackageDeliveryCommand = enum(Data_Types::PackageDeliveryCommand, ABORT_DELIVERY);
+		const NO_OPERATION_CMD: Data_Types::PackageDeliveryCommand = enum(Data_Types::PackageDeliveryCommand, NO_OPERATION);
+		const NOT_STARTED_STATUS: Data_Types::DeliveryStatus = enum(Data_Types::DeliveryStatus, NOT_STARTED);
+		const FAILED_STATUS: Data_Types::DeliveryStatus = enum(Data_Types::DeliveryStatus, FAILED);
+		const COMPLETED_STATUS: Data_Types::DeliveryStatus = enum(Data_Types::DeliveryStatus, COMPLETED);
+
+
+	**};
+end Agree_Constants;

models/DeliveryDrone_CRV/Agree_Nodes.aadl

@@ -0,0 +1,51 @@
+package Agree_Nodes
+public
+	with Data_Types;
+
+	annex agree {**
+
+		-- HasHappened(X) is true iff X has been true at least once so far
+		node HasHappened(X : bool) returns (Y : bool);
+		let
+  			Y = X or (false -> pre (Y)) ;
+		tel;
+
+		-- Initially(X) is true iff X was true at the initial step
+		node InitiallyX(X: bool) returns (Y: bool);
+		let
+  			Y = X -> true;
+		tel;
+
+		-- FirstLocation(X) is the constant stream consisting of the first value of X
+		node FirstLocation( X : Data_Types::Position.impl ) returns ( Y : Data_Types::Position.impl );
+		let
+  			Y = X -> pre (Y);
+		tel;
+
+		node close_locations(p1: Data_Types::Position.impl, p2: Data_Types::Position.impl) returns (are_close: bool);
+		let
+  			are_close = p1 = p2;
+		tel;
+
+		node Duration(p: bool) returns (r: int) ;
+		let   
+			r = (if p then 1 else 0) -> (if p then pre(r) + 1 else 0) ;
+		tel;
+
+		node Sofar(X : bool ) returns ( Y : bool );
+		let
+ 			Y = X -> (X and (pre(Y)));
+		tel;
+
+		node Since(X: bool, Y : bool ) returns ( Z : bool );
+		let
+  			Z =  X or (Y and (false -> pre(Z)));
+		tel;
+
+		node ToInt(b: bool) returns (i: int);
+		let
+			i = if b then 1 else 0;
+		tel;
+
+	**};
+end Agree_Nodes;

models/DeliveryDrone_CRV/Data_Types.aadl

@@ -0,0 +1,83 @@
+package Data_Types
+public
+	with Data_Model, Base_Types;
+
+	data Position
+	end Position;
+
+	data implementation Position.impl
+		subcomponents
+			x: data Base_Types::Float; 
+			y: data Base_Types::Float;
+  	end Position.impl;
+
+  	data DeliveryOrder
+  	end DeliveryOrder;
+
+  	data implementation DeliveryOrder.impl
+  		subcomponents
+  			target_position: data Position.impl;
+  			target_picture: data Base_Types::Integer;
+  			item_value: data Base_Types::Float;
+  	end DeliveryOrder.impl;
+
+  	data DeliveryStatus
+  		properties
+	    	Data_Model::Data_Representation => Enum;
+	    	Data_Model::Enumerators => ("NOT_STARTED", "IN_PROGRESS", "COMPLETED", "FAILED");
+	end DeliveryStatus;
+
+  	data Constellation
+  		properties
+	    	Data_Model::Data_Representation => Enum;
+	    	Data_Model::Enumerators => ("Satellite0", "Satellite1");
+	end Constellation;
+
+  	data InputBus
+  	end InputBus;
+
+  	data implementation InputBus.impl
+  		subcomponents
+  			connected: data Base_Types::Boolean;
+  			update_order: data Base_Types::Boolean; -- not used in new delivery planner?
+  			order: data DeliveryOrder.impl; 
+  			-- added
+  			on_off: data Base_Types::Boolean; --Check if it makes sense to come from bus?
+  			abort_cmd: data Base_Types::Boolean; --Check if it makes sense to come from bus?
+  			constellation: data Constellation;
+  			launch_pos: data Position.impl;
+  			init_criteria_satisfied: data Base_Types::Boolean;
+  			mission_store_release_sequence: data Base_Types::Boolean;
+  	end InputBus.impl;
+
+  	data RadioResponse
+  	end RadioResponse;
+
+  	data implementation RadioResponse.impl
+  		subcomponents
+  			data_available: data Base_Types::Boolean;
+  			target_confirmed: data Base_Types::Boolean;
+  	end RadioResponse.impl;
+
+  	data ProbeSafeLanding
+  	end ProbeSafeLanding;
+
+  	data implementation ProbeSafeLanding.impl
+  		subcomponents
+  			is_target_clear: data Base_Types::Boolean;
+  			has_valid_marker: data Base_Types::Boolean;
+  	end ProbeSafeLanding.impl;
+
+	data DeliveryPlannerState
+  		properties
+	    	Data_Model::Data_Representation => Enum;
+	    	Data_Model::Enumerators => ("OFF", "INIT", "READY", "LAUNCH", "ABORT", "FLYING_TO_DEST", "MAKING_DELIVERY", "RETURN_TO_TRUCK");
+	end DeliveryPlannerState; 
+
+	data PackageDeliveryCommand
+  		properties
+	    	Data_Model::Data_Representation => Enum;
+	    	Data_Model::Enumerators => ("NO_OPERATION", "RELEASE_PACKAGE", "ABORT_DELIVERY");
+	end PackageDeliveryCommand;
+
+end Data_Types;