-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathHighwayEnvironment2.mch
146 lines (135 loc) · 5.97 KB
/
HighwayEnvironment2.mch
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
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
MACHINE HighwayEnvironment2
SETS
Vehicles
CONSTANTS
EgoVehicle
PROPERTIES
card(Vehicles) > 1 &
card(Vehicles) = 5 &
EgoVehicle : Vehicles
VARIABLES
Crash /*@desc "TRUE when a crash occurred" */,
PresentVehicles /*@desc "The vehicles that are on screen" */,
VehiclesX /*@desc "x-coordinates of the vehicles" */,
VehiclesY /*@desc "y-coordinates of the vehicles" */,
VehiclesVx /*@desc "horizontal speed of the vehicles" */,
VehiclesVy /*@desc "vertical speed of the vehicles" */,
VehiclesAx /*@desc "horizontal acceleration of the vehicles" */,
VehiclesAy /*@desc "vertical acceleration of the vehicles" */,
Reward
INVARIANT
Crash : BOOL &
PresentVehicles : POW(Vehicles) &
EgoVehicle : PresentVehicles /*@desc "the Ego vehicle is always present" */ &
VehiclesX : Vehicles --> REAL &
VehiclesY : Vehicles --> REAL &
VehiclesVx : Vehicles --> REAL &
VehiclesVy : Vehicles --> REAL &
VehiclesAx : Vehicles --> REAL &
VehiclesAy : Vehicles --> REAL &
Reward : REAL
INITIALISATION
Crash :: BOOL ||
PresentVehicles : (PresentVehicles : POW(Vehicles) & EgoVehicle : PresentVehicles) ||
VehiclesX :: Vehicles --> REAL ||
VehiclesY :: Vehicles --> REAL ||
VehiclesVx :: Vehicles --> REAL ||
VehiclesVy :: Vehicles --> REAL ||
VehiclesAx :: Vehicles --> REAL ||
VehiclesAy :: Vehicles --> REAL ||
Reward :: REAL
OPERATIONS
IDLE =
SELECT
not(#v. (v : PresentVehicles \ {EgoVehicle} & VehiclesX(v) > 0.0 & VehiclesX(v) < 35.0 & VehiclesY(v) < 3.5 & VehiclesY(v) > -3.5 & VehiclesVx(v) < 0.0))
THEN
Crash :: BOOL ||
PresentVehicles : (PresentVehicles : POW(Vehicles) & EgoVehicle : PresentVehicles) ||
VehiclesX :: Vehicles --> REAL ||
VehiclesY :: Vehicles --> REAL ||
VehiclesVx :: Vehicles --> REAL ||
VehiclesVy :: Vehicles --> REAL ||
VehiclesAx :: Vehicles --> REAL ||
VehiclesAy :: Vehicles --> REAL ||
Reward :: REAL
END;
LANE_LEFT =
SELECT
EgoVehicle : dom(VehiclesY) &
VehiclesY(EgoVehicle) > 1.0 &
not(#v. (v : PresentVehicles \ {EgoVehicle} & VehiclesX(v) > -25.0 & VehiclesX(v) <= -15.0 & VehiclesY(v) > -6.0 & VehiclesY(v) < -2.0 & VehiclesVx(v) > 0.0)) &
not(#v. (v : PresentVehicles \ {EgoVehicle} & VehiclesX(v) > -15.0 & VehiclesX(v) <= 15.0 & VehiclesY(v) > -6.0 & VehiclesY(v) < -2.0)) &
not(#v. (v : PresentVehicles \ {EgoVehicle} & VehiclesX(v) > 15.0 & VehiclesX(v) <= 35.0 & VehiclesY(v) > -6.0 & VehiclesY(v) < -2.0 & VehiclesVx(v) < 0.0))
THEN
Crash :: BOOL ||
PresentVehicles : (PresentVehicles : POW(Vehicles) & EgoVehicle : PresentVehicles) ||
VehiclesX :: Vehicles --> REAL ||
VehiclesY :: Vehicles --> REAL ||
VehiclesVx :: Vehicles --> REAL ||
VehiclesVy :: Vehicles --> REAL ||
VehiclesAx :: Vehicles --> REAL ||
VehiclesAy :: Vehicles --> REAL ||
Reward :: REAL
END;
LANE_RIGHT =
SELECT
EgoVehicle : dom(VehiclesY) &
VehiclesY(EgoVehicle) < 7.0 &
not(#v. (v : PresentVehicles \ {EgoVehicle} & VehiclesX(v) > -25.0 & VehiclesX(v) <= -15.0 & VehiclesY(v) < 6.0 & VehiclesY(v) > 2.0 & VehiclesVx(v) > 0.0)) &
not(#v. (v : PresentVehicles \ {EgoVehicle} & VehiclesX(v) > -15.0 & VehiclesX(v) < 15.0 & VehiclesY(v) < 6.0 & VehiclesY(v) > 2.0)) &
not(#v. (v : PresentVehicles \ {EgoVehicle} & VehiclesX(v) > 15.0 & VehiclesX(v) <= 35.0 & VehiclesY(v) < 6.0 & VehiclesY(v) > 2.0 & VehiclesVx(v) < 0.0))
THEN
Crash :: BOOL ||
PresentVehicles : (PresentVehicles : POW(Vehicles) & EgoVehicle : PresentVehicles) ||
VehiclesX :: Vehicles --> REAL ||
VehiclesY :: Vehicles --> REAL ||
VehiclesVx :: Vehicles --> REAL ||
VehiclesVy :: Vehicles --> REAL ||
VehiclesAx :: Vehicles --> REAL ||
VehiclesAy :: Vehicles --> REAL ||
Reward :: REAL
END;
FASTER =
SELECT
EgoVehicle : dom(VehiclesVx) &
not(#v. (v : PresentVehicles \ {EgoVehicle} & VehiclesX(v) > 0.0 & VehiclesX(v) < 45.0 & VehiclesY(v) < 3.5 & VehiclesY(v) > -3.5))
THEN
Crash :: BOOL ||
PresentVehicles : (PresentVehicles : POW(Vehicles) & EgoVehicle : PresentVehicles) ||
VehiclesX :: Vehicles --> REAL ||
VehiclesY :: Vehicles --> REAL ||
VehiclesVx :: Vehicles --> REAL ||
VehiclesVy :: Vehicles --> REAL ||
VehiclesAx :: Vehicles --> REAL ||
VehiclesAy :: Vehicles --> REAL ||
Reward :: REAL
END;
SLOWER =
SELECT
EgoVehicle : dom(VehiclesVx) &
(#v. (v : PresentVehicles \ {EgoVehicle} & VehiclesX(v) > 0.0 & VehiclesX(v) < 15.0 & VehiclesY(v) < 3.5 & VehiclesY(v) > -3.5 & VehiclesVx(v) < 0.0)
=>
(not(
VehiclesY(EgoVehicle) > 1.0 &
not(#v. (v : PresentVehicles \ {EgoVehicle} & VehiclesX(v) > -25.0 & VehiclesX(v) <= -15.0 & VehiclesY(v) > -6.0 & VehiclesY(v) < -2.0 & VehiclesVx(v) > 0.0)) &
not(#v. (v : PresentVehicles \ {EgoVehicle} & VehiclesX(v) > -15.0 & VehiclesX(v) <= 15.0 & VehiclesY(v) > -6.0 & VehiclesY(v) < -2.0)) &
not(#v. (v : PresentVehicles \ {EgoVehicle} & VehiclesX(v) > 15.0 & VehiclesX(v) <= 35.0 & VehiclesY(v) > -6.0 & VehiclesY(v) < -2.0 & VehiclesVx(v) < 0.0))
) &
not(
VehiclesY(EgoVehicle) < 7.0 &
not(#v. (v : PresentVehicles \ {EgoVehicle} & VehiclesX(v) > -25.0 & VehiclesX(v) <= -15.0 & VehiclesY(v) < 6.0 & VehiclesY(v) > 2.0 & VehiclesVx(v) > 0.0)) &
not(#v. (v : PresentVehicles \ {EgoVehicle} & VehiclesX(v) > -15.0 & VehiclesX(v) < 15.0 & VehiclesY(v) < 6.0 & VehiclesY(v) > 2.0)) &
not(#v. (v : PresentVehicles \ {EgoVehicle} & VehiclesX(v) > 15.0 & VehiclesX(v) <= 35.0 & VehiclesY(v) < 6.0 & VehiclesY(v) > 2.0 & VehiclesVx(v) < 0.0))
)))
THEN
Crash :: BOOL ||
PresentVehicles : (PresentVehicles : POW(Vehicles) & EgoVehicle : PresentVehicles) ||
VehiclesX :: Vehicles --> REAL ||
VehiclesY :: Vehicles --> REAL ||
VehiclesVx :: Vehicles --> REAL ||
VehiclesVy :: Vehicles --> REAL ||
VehiclesAx :: Vehicles --> REAL ||
VehiclesAy :: Vehicles --> REAL ||
Reward :: REAL
END
END