drone_model.use

model DroneDeliveryModel

-- enumeration for states
enum Drone_State {Created, Parked, Delivering, Charging, Unloading, Returning}
-- Parked = drone init or drone in a warehouse
-- Delivering = drone is moving to a receptacle to deliver a cmd
-- Charging = drone is charging his battery
-- Unloading = drone is at destination receptacle and is delivering cmd
-- Returning = drone has delivered a cmd and is now returning to warehouse

enum Point_State {Created, Free, Occupied}
enum Command_State {Created, Assigned, Delivered}

class Drone
	attributes
		capacity : Integer init = 0
		energy : Integer init = 3
		state : Drone_State init = Drone_State::Parked
		destination_point : Point -- needed by shift()
			derive : 
			if self.capacity > 0 then self.receptacle
			else self.warehouse endif

		--state : Drone_State init = Drone_State::Parked 

	operations

		distancePoint(p:Point) : Integer = (self.position_drone.x - p.x).abs + (self.position_drone.y - p.y).abs;

		recharge ()
			begin
				self.energy := self.energy + 1;
			end
		shift() -- find the right position to move to
			begin
				declare point_dest : Point, distance_toDest : Integer, newX : Integer, newY : Integer;
				distance_toDest := self.distancePoint(self.destination_point);

				-- TODO improve the algo (occupation !!)
				point_dest := self.position_drone.neighbours()->select(p | p.distance(self.destination_point) < distance_toDest and (p.state = Point_State::Free or (p.oclIsTypeOf(Receptacle) and p.oclAsType(Receptacle).oclInState(Free)) or (p.oclIsTypeOf(Warehouse))))->asSequence->first();


			   -- shift  = point_dest.x - self.position_drone.x ...
			   self.move(point_dest);
			end
		move (point : Point) -- ?? deplacement vers un Point ou comme pour l'instant, ie deplacer d'un x et d'un y
			begin
				point.setOccupied(); -- verify if it's not the WH ?
				self.position_drone.setFree();
				delete (self.position_drone, self) from Position; 
				insert (point, self) into Position;
				
				self.energy := self.energy -1;
				
			end
		deliver()
			begin
				declare recep : Set(Receptacle); -- current receptacle
				recep := Receptacle.allInstances().select( rec | rec.distanceDrone(self) = 0);
				for r in recep do
					r.capacity := r.capacity + self.capacity;
					r.cmd.deliver();
					delete(r, r.cmd) from Destination;
				end;

				self.capacity := 0;
				self.energy := self.energy - 1;

				delete (self.receptacle, self) from Delivery;
			end
		allocate(recep : Receptacle, cmd: Command)
			begin
				insert(recep, cmd) into Destination;
				insert(recep, self) into Delivery;

				--set charge
				self.capacity := self.receptacle.cmd.weight;
			end
		finish() 
			begin
				
			end
		statemachines
			psm DroneStateMachine
				states
					Created:initial
					Parked
					Delivering
					Charging
					Unloading
					Returning
				transitions
					Created -> Parked { create }
					Parked -> Delivering { allocate() }
					Delivering -> Delivering { shift() }
					Delivering -> Charging { recharge() }
					Delivering -> Unloading { deliver() }
					Unloading -> Returning { shift() }
					Returning -> Charging { recharge() }
					Charging -> Charging { recharge() }
					Charging -> Unloading { deliver() }
					Charging -> Returning {[self.destination_point.oclIsTypeOf(Warehouse)] shift()}
					Charging -> Delivering {[self.destination_point.oclIsTypeOf(Receptacle)] shift()}
					Unloading -> Charging { recharge() }
					Returning -> Parked { finish() }
		end


end

class Point 
	attributes 
		x : Integer
		y : Integer
		state : Point_State init = Point_State::Free
	operations
		-- Manhattan distance between two points 
		distance(dest : Point ) : Integer =
			(self.x - dest.x).abs + (self.y - dest.y).abs

		neighbours() : Set(Point) =
            Point.allInstances()->select(p | self.distance(p) = 1)
		-- Set point's states
        setFree()
			begin
				self.state := Point_State::Free;
			end
        setOccupied()
	    	begin
	    		self.state := Point_State::Occupied;
			end

		-- check if there is a receptacle or a warehouse in the current point
		
end

class Warehouse < Point end


class Receptacle < Point
    attributes
        capacity : Integer init = 0

    operations 
    	-- All neighbours 
        neighboursRecept() : Set(Receptacle) =
            Receptacle.allInstances()->select (r| distance(r) < 3)

		-- Get distance from given drone
		distanceDrone(d : Drone) : Integer =
            (self.x-d.position_drone.x).abs + (self.y-d.position_drone.y).abs

        distancePoint(p : Point) : Integer = 
        	(self.x- p.x).abs + (self.y- p.y).abs

        statemachines
	        psm ReceptacleStateMachine
	        states
	        	Created:initial
	            Free
	            Occupied
	            --Full
	         transitions
	         	Created -> Free { create }
	            Free -> Occupied {[Drone.allInstances()->one(d | distanceDrone(d) = 0)] setOccupied()}
	            Occupied -> Free {[Drone.allInstances()->forAll(d | distanceDrone(d) <> 0)] setFree()}
    	end
		
end

class Command
	attributes
		state : Command_State init = Command_State::Created
		weight : Integer -- temp (must be a Product attribute)

	operations
	 	assign()
		 	begin
		 		self.state := Command_State::Assigned
		 	end
	 	deliver()
		 	begin
		 		self.state := Command_State::Delivered
		 	end

		statemachines
	        psm CommandStateMachine
	        states
	        	Created:initial
	            Assigned
	            Delivered
	         transitions
	            Created -> Assigned {assign()}
	            Assigned -> Delivered {deliver()}
    	end
end


class Grid
  attributes
  	Time : Integer init = 0 -- time
  	Length : Integer -- Length of a side of the square grid
    RNB  : Integer -- Number of Receptacles 
    RCAP : Integer -- Capacity of a receptacle
    DNB  : Integer -- number of Drones
    DCAP : Integer -- Capacity of a drone
    NELEMNTS: Integer -- Number of elements to generate (need ??)

    operations
    	tick() -- TODO : when can we consider that all objects have finished their operations and we can send the following tick ??
    		begin
    			declare drones_torecharge : Set(Drone), drones_todeliver :  Set(Drone),drones_tomove :  Set(Drone), tmp : Boolean;

    			drones_torecharge := Drone.allInstances().select(d | d.energy <= 1 and (d.position_drone.oclIsTypeOf(Receptacle) or d.position_drone.oclIsTypeOf(Warehouse))); 

    			drones_todeliver := Drone.allInstances().select(d | d.capacity > 0  and d.receptacle.distancePoint(d.position_drone) = 0);-- exclude drones_torecharge 
    			drones_tomove := Drone.allInstances(); -- exclude the 2 prec collections

    			self.Time := self.Time + 1; -- set time
    			-- recharge drones which need to be 

    			for dc in drones_torecharge do
					dc.recharge();
					tmp := drones_todeliver->excluding(dc)->isEmpty() and drones_tomove->excluding(dc)->isEmpty();
				end;

				-- deliver command for drones which have to
    			for dd in drones_todeliver do
					dd.deliver();
					tmp := drones_tomove->excluding(dd)->isEmpty();
				end;

				-- move drones which must be
    			for dm in drones_tomove do
					dm.shift();
				end;

    		end
end

association Owner between 
	Warehouse[1] role warehouse;
	Grid[1] role grid;
end

association Location between 
	Receptacle[*] role receptacles;
	Grid[1] role grid;
end

association Destination between 
	Receptacle[1] role receptacle;
	Command[1] role cmd;
end

association Position between 
	Point[1] role position_drone;
	Drone[*] role drone_position;
end

association Delivery between 
	Receptacle[1] role receptacle;
	Drone[1] role deliver;
end

association Crew between 
	Warehouse[1] role warehouse;
	Drone[*] role drones;

end


-- ####### CONSTRAINTS  ##########
constraints


-- ********** PRE AND POST CONDITIONS ************

context Drone::move(point : Point)
	pre droneIsCharged : self.energy > 0
	pre moveToNeighbour : ((point.x - self.position_drone.x) + (point.y - self.position_drone.y)).abs = 1
	pre destinationIsFree : point.oclIsTypeOf(Warehouse) or not Drone.allInstances->exists(drone | drone.position_drone.x = point.x and drone.position_drone.y = point.y) 
	post locationHasChanged : (self.position_drone <> self.position_drone@pre)

context Drone::deliver()
	pre isRightReceptacle : self.receptacle.x =self.position_drone.x and self.receptacle.y = self.position_drone.y
	pre droneIsAtTheLocation : 
		Receptacle.allInstances-> one(r | r.distanceDrone(self) =0) and not Warehouse.allInstances-> exists(w | w.distance(self.position_drone) =0)
	pre droneContainsCmd : self.capacity <> 0
	post droneHasDeliveredCmd : self.capacity = 0
	post droneDoesNotMove : Receptacle.allInstances-> one(r | r.distanceDrone(self) =0) and 
		not Warehouse.allInstances-> exists (w | w.distance(self.position_drone) =0)

context Drone::recharge()
	pre droneIsNotFull: self.energy < 3
	pre locationAllowCharging: Receptacle.allInstances->exists (r | r.distanceDrone(self) =0)
	post droneDoesnotMove: Receptacle.allInstances->exists (r | r.distanceDrone(self) =0)

context Drone::allocate(recep : Receptacle, cmd: Command)
	pre droneIsAtWarehouse : self.position_drone.oclIsTypeOf(Warehouse)
	pre droneIsEmpty : self.capacity = 0
	pre cmdHasProduct : cmd.weight > 0
	post droneIsFilled : self.capacity = cmd.weight
	post droneDoesnotMove : self.position_drone.oclIsTypeOf(Warehouse)



-- ************ INVARIANTS ***********

-- ** The Battery level is always between 3 and 0
context Drone inv batteryLevel : self.energy >= 0 and self.energy <= 3 

-- ** Every Point is Unique
context point:Point inv everyPointIsUniqueAndBelongToGrid : 
	Point.allInstances().select(p|p = point)->size() = 1 
	 

-- ** There is no 2 or more drones at the same receptacle
context point:Point inv atMostOneDronePerPoint:
	if not point.oclIsTypeOf(Warehouse) then
		Drone.allInstances().select(d|d.position_drone = point)->size() <= 1 
	else
		Drone.allInstances().select(d|d.position_drone = point)->size() >= 0
	endif


-- ** Every drone in a simple point (not receptacle or warehouse) must have charge
context Drone inv droneHasChargeIfSimplePosition :
	Drone.allInstances().select(d| not d.position_drone.oclIsTypeOf(Warehouse) and d.position_drone.oclIsTypeOf(Receptacle) and d.energy < 1)->size() = 0

-- A command should be deliver to a Receptacle point
context Command inv commandForReceptaclePosition :
	Command.allInstances().select(c| not c.receptacle.oclIsTypeOf(Receptacle))->size() = 0

-- ** Only One Warehouse in the grid
context Warehouse inv onlyOneWarehouse : Warehouse.allInstances->size() = 1

-- ** At least 1 Receptacle as warehouse's neighbour 
context Warehouse inv atLeastOneNeighbourReceptacle : 
	self.neighbours()->select(p | p.oclIsTypeOf(Receptacle))->size() >= 1

-- ** DNB
context Grid inv DNB : 
	self.DNB = self.warehouse.drones->size()

-- ** DCAP
context Grid inv DCAP : 
	Drone.allInstances().select(d| d.capacity > self.DCAP)->size() = 0 

-- ** RNB
context Grid inv RNB : 
	 self.RNB = self.receptacles->size() 

-- ** RCAP
context Grid inv RCAP : 
	Receptacle.allInstances().select(r| r.capacity > self.RCAP)->size() = 0