CollisionAvoidanceSystem/AirTrafficController.pd at master · varuna-v/CollisionAvoidanceSystem · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
//*******************************************************
//* File:    C:/Users/User/Desktop/Third Year Project/CollisionAvoidanceSystem/AirTrafficController.pd
//* Author:  Varuna
//* Created: 14:39:29 on Sunday January 25th 2015 UTC
//*******************************************************

class AirTrafficController ^=
abstract

	var aircrafts : seq of Aircraft;
	var minX : real; //meters
	var maxX : real; //meters
	var minY : real; //meters
	var maxY : real; //meters

	invariant forall a::aircrafts :- minX <= a.position.x <= maxX & minY <= a.position.y <= maxY;
	invariant forall i::0..<#aircrafts :-(forall j::(i+1)..<#aircrafts :- aircrafts[i] ~= aircrafts[j]);

confined

	function getPairs : set of AircraftPair
		^= (let s ^= (for i::0..<#aircrafts yield (for j::(i+1)..<#aircrafts yield AircraftPair{aircrafts[i], aircrafts[j]}).ran).ran;
			flatten(s))
		assert #result = ((#aircrafts)*(#aircrafts-1)/2);

	function conflicts : map of (AircraftPair -> ConflictStatus)
		^= (let pairs ^= getPairs;
			map of (AircraftPair -> ConflictStatus){(for p::pairs yield pair of (AircraftPair, ConflictStatus){p, p.getConflictStatus})})
		assert forall a::result.pairs :- a.x.craft1 in aircrafts & a.x.craft2 in aircrafts & a.y = a.x.getConflictStatus &
		 #result = ((#aircrafts)*(#aircrafts-1)/2);

	function willAllAircraftsBeInBoundaryAfterFlying(flyForTime : real) : bool
		^= forall a::aircrafts :- willAircraftBeInBoundryAfterFlying(a, flyForTime);

	function willAircraftBeInBoundryAfterFlying(aircraft : Aircraft, flyForTime : real) : bool
		^= (let endPosition ^= aircraft.positionAfterFlying(flyForTime);
			((minX <= endPosition.x <= maxX) & (minY <= endPosition.y <= maxY)));

	schema !dropIfLeavesBoundaryAfterFlying(flyForTime : real)
		pre forall a::aircrafts :- minX <= a.position.x <= maxX & minY <= a.position.y <= maxY
		post aircrafts != (those a::aircrafts :- willAircraftBeInBoundryAfterFlying(a, flyForTime))
		assert (forall a::aircrafts' :- minX <= a.position.x <= maxX & minY <= a.position.y <= maxY) &
			   (forall i::0..<#aircrafts' :-(forall j::(i+1)..<#aircrafts' :- aircrafts'[i] ~= aircrafts'[j]));

	function getPairsThatArePFC : set of AircraftPair
		^= (let pairs ^= getPairs;
			those p::pairs :- p.getConflictStatus = ConflictStatus PotentialFutureConflict);
interface

	function aircrafts;

	function numberOfAirCrafts : nat
		^= #aircrafts;

	function getAircraftPairsOrderedByTimeToConflict : seq of AircraftPair
		^= getPairsThatArePFC.opermndec;

	function getConflictStatus(aircraft : Aircraft, incconflicts : map of (AircraftPair -> ConflictStatus)) : ConflictStatus
		^= (let lst ^= (for those c::incconflicts.pairs :- c.x.craft1 = aircraft | c.x.craft2 = aircraft yield c.y);
			([ConflictStatus Conflicted in lst] : ConflictStatus Conflicted,
			 [ConflictStatus PotentialFutureConflict in lst] : ConflictStatus PotentialFutureConflict,
			 [] : ConflictStatus NoConflict));

	schema !changeCraftHeight(identification : string, targetHeight : real)
		pre exists c::aircrafts :- c.identification = identification
		post (let craft ^= that c::aircrafts :- c.identification = identification;
			  aircrafts != (those c::aircrafts :- c.identification ~= identification).append(craft.getCraftTargettingHeight(targetHeight)));

	schema !fly(forTime : real)
		post self!dropIfLeavesBoundaryAfterFlying(forTime) then
			 aircrafts != (for craft::aircrafts yield craft.getCraftAfterFlying(forTime)) then
			 (let locConflicts ^= conflicts;
			  aircrafts != (for craft::aircrafts yield craft.getCraftWithConflictStatus(getConflictStatus(craft, locConflicts))))
		assert (forall a::aircrafts' :- minX <= a.position.x <= maxX & minY <= a.position.y <= maxY) &
			   (forall i::0..<#aircrafts' :-(forall j::(i+1)..<#aircrafts' :- aircrafts'[i] ~= aircrafts'[j]));

	schema !addAircraft(aircraft : Aircraft)
		post aircrafts != aircrafts.append(aircraft) then
			 !fly(0.0);

	build{!aircrafts : seq of Aircraft, !minX : real, ! maxX : real, !minY : real, !maxY : real}
		pre minX < maxX & minY < maxY
			& (forall i::0..<#aircrafts :-(forall j::(i+1)..<#aircrafts :- aircrafts[i] ~= aircrafts[j]))
			& (forall a::aircrafts :- minX <= a.position.x <= maxX & minY <= a.position.y <= maxY)
		post !fly(0.0);

end;


//----------- Print for debugging -----------
//	function printConflicts : string
//		^= "Number of aircrafts in system: " ++ numberOfAirCrafts.toString ++ "<br>" ++ getConflictsString(conflicts.pairs);

//	function getConflictsString(cons : set of pair of(AircraftPair, ConflictStatus)) : string
//		decrease #cons
//		^= ([#cons = 0] : "",
//			[] : (let c ^= any k::cons :- k=k;
//				  "Pair <br>" ++ c.x.toString ++ "<br> Status: " ++ c.y.toString ++ "<br>" ++ getConflictsString(cons.remove(c))));