<!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_2.dtd'>
<nta>
<declaration>
// Scale
const int scale = 100;
// Abstraction parameters (defines level of abstraction)
const int S := 10; // sample period, in 1/scale seconds
const int GranA := 100; // granularity of the acceleration expressed in 1/scale meters per second squared
const int NormX := 100; // maximal loss of precision during a second in 1/scale meters (>= (GranA*S/scale)/2)
// Road parameters
const int L := 60000; // length of the road segment, in 1/scale meters
const int R := 1050; // width of the road segment, in 1/scale meters
const int length_vehicle := 500; // length of a vehicle in 1/scale meters
const int width_vehicle := 200; // width of a vehicle in 1/scale meters
const int begin_junction := 20000; // begining of junction lane in 1/scale meters
const int end_junction := 40000; // end of junction lane in 1/scale meters
const int nb_lane := 3; // number of lanes, including junction (>= 2)
const int marks[nb_lane+1] := {0,350,700,R}; // lateral position of markings separating lanes in 1/scale meters
// Vehicles parameters (to change the number of vehicle in the system, change nb_car value, adjust the size of the sets bellow, set the appropriate number of automaton in system definition and add the needed transitions to A0)
const int V_min := 1000; // min value of longitudinal speed, in 1/scale meters per second
const int V_max := 4000; // max value of longitudinal speed, in 1/scale meters per second
const int A_min := -500; // min value of longitudinal acceleration, in 1/scale meters per second squared
const int A_max := 300; // max value of longitudinal acceleration, in 1/scale meters per second squared
const int W := 100; // maximal absolute value of the lateral speed expressed in 1/scale meters per second
const int nb_car := 3; // number of vehicles (>= 2)
const int freq[nb_car] := {10,10,10}; // activation sample of the controler for each vehicle in 1/scale second
const int min_com_delay[nb_car] := {3,3,3}; // min communication delay for each vehicle in 1/scale second, must be smaller than the vehicle's controller sample
const int max_com_delay[nb_car] := {4,4,4}; // max communication delay for each vehicle in 1/scale second, must be smaller than the vehicle's controller sample
const int init_posX[nb_car] := {5000,0,2000}; // initial longitudinal position for each vehicle in 1/scale meters
const int init_posY[nb_car] := {525,525,175}; // initial lateral position for each vehicle in 1/scale meters
const int init_V[nb_car] := {2000,3500,2820}; // initial longitudinal speed for each vehicle in 1/scale meters per second
const int init_A[nb_car] := {3,3,3}; // initial longitudinal acceleration for each vehicle in 1/scale meters per second squared
const int init_clock[nb_car] := {1,4,8}; // initial controller clock value for each vehicle in 1/scale seconds
//Global clocks
clock C1; // in 1/scale seconds
clock C2; // in 1/scale seconds
clock C3; // in 1/scale seconds
clock C4; // in 1/scale seconds
clock C5; // in 1/scale seconds
//Synchronisation channel
broadcast chan k;
// Constants and data types obtained from parameters
const int GranV := GranA*S; // granularity of the longitudinal speed expressed in 1/scale/scale meters per second
const int GranX := NormX*S; // granularity of the longitudinal position expressed in 1/scale/scale meters
const int GranY := W*S; // granularity of the lateral position expressed in 1/scale/scale meters
const int p := 2*NormX*scale/GranV; // used for posX update
const int LengthX := (L*scale)/GranX; // normalized length of the road segment
const int LengthY := (R*scale)/GranY; // normalized width of the road segment
const int min_speed := (V_min*scale)/GranV; // normalized min value of longitudinal speed
const int max_speed := (V_max*scale)/GranV; // normalized max value of longitudinal speed
const int min_acceleration := A_min/GranA; // normalized min value of longitudinal acceleration
const int max_acceleration := A_max/GranA; // normalized max value of longitudinal acceleration
const int C_len := (length_vehicle*scale)/GranX; // normalized length of a vehicle
const int C_wid := (width_vehicle*scale)/GranY; // normalized width of a vehicle
const int marking[nb_lane+1] := {(marks[0]*scale)/GranY,(marks[1]*scale)/GranY,(marks[2]*scale)/GranY,(marks[3]*scale)/GranY}; // normalized lateral position of markings separating lanes
const int J_beg := (begin_junction*scale)/GranX; // used for posX and posY update
const int J_end := (end_junction*scale)/GranX; // used for posX and posY update
const int J_inf := marking[1]-(C_wid/2); // used for posY update
const int J_sup := marking[1]+(C_wid/2); // used for posY update
typedef int[0,LengthX] RangeX; // longitudinal position range
typedef int[1,LengthY] RangeY; // lateral position range
typedef int[min_speed,max_speed] RangeV; // speed range
typedef int[min_acceleration,max_acceleration] RangeA; // acceleration range
typedef int[-1,1] RangeD; // direction range
typedef int[0,nb_car-1] RangeId; // ids range
typedef int[0,nb_lane-1] RangeLane; // lanes range
// Decision related parameters
const int navigation_points := 2; // number of coordinate on a navigation list
const int navigation_list[nb_car][navigation_points][3] := {
{{0,0,2},{LengthX,1,1}},
{{0,0,2},{LengthX,1,1}},
{{J_end,1,2},{LengthX,1,1}}
}; // GPS trajectory for each vehicle in list of {posX,lane(min),lane(max)}, each car MUST have a complete trajectory that goes up to horizon value
const int safety_length := 200; // longitudinal safety distance of a vehicle in 1/scale meters
const int safety_width := 50; // lateral safety distance of a vehicle in 1/scale meters
const int traj_length := 1000; // length of the predicted trajectory in 1/scale seconds
const int delay_step := 100; // delay step in 1/scale seconds
const int max_delay := 500; // maximum delay in 1/scale seconds
// Constants and data types obtained from decision related parameters
const int S_len := (safety_length*scale)/GranX; // normalized safety length of a vehicle
const int S_wid := (safety_width*scale)/GranY; // normalized safety width of a vehicle
const int traj_range := traj_length/S; // range of the predicted trajectory (number of points)
const int LengthDelay := max_delay/delay_step;
typedef int[0,LengthDelay] RangeDelay; // delay range
// Querries memory
int[0,(L*scale)/(S*V_min)] nb_updates;
// Information structure for each vehicle, the parenthesis indicate wich automaton updates the variable
struct{
bool on_the_road; // tells if the vehicle is on or out of the road (environment)
RangeX posX; // longitudinal position of the car (environment)
RangeY posY; // lateral position of the car (environment)
if(car[id].posX > J_end and car[id].posY < J_sup) car[id].on_the_road := false; // car is out of the road if did not change lane before the end of junction lane
else car[id].speed += car[id].acceleration; // adjust speed regarding the variation choosen by the controler
//update lateral position
if(car[id].direction == -1 and car[id].on_the_road){
if((car[id].posX <= J_end and car[id].posX >= J_beg) or car[id].posY >= J_sup or car[id].posY <= J_inf){ // forbiding to go on junction lane before the junction starts
if(car[id].posY > 1) car[id].posY--;
}
}
if(car[id].direction == 1 and car[id].on_the_road){
if((car[id].posX <= J_end and car[id].posX >= J_beg) or car[id].posY >= J_sup or car[id].posY <= J_inf){ // forbiding to get out of junction lane before the junction starts
if(car[id].posY < LengthY) car[id].posY++;
}
}
if(car[id].posX < J_beg and car[id].posY < J_sup and car[id].posY > J_inf) car[id].on_the_road := false; // car is out of the road if beetween junction lane and highway out of the junction zone
}
}
}
void communicate(RangeId id){
// Send goal and data value to other vehicles
for(n : int[0,nb_car-1]){
if(id<n){
data[n].goal[id] := car[id].goal;
data[n].delay[id] := car[id].delay;
}
if(id>n){
data[n].goal[id-1] := car[id].goal;
data[n].delay[id-1] := car[id].delay;
}
}
}
// Give the goal value that id knows about n
RangeLane read_goal(RangeId id, RangeId n){
if(id>n) return data[id].goal[n];
if(id<n) return data[id].goal[n-1];
return car[id].goal;
}
// Give the delay value that id knows about n
RangeDelay read_delay(RangeId id, RangeId n){
if(id>n) return data[id].delay[n];
if(id<n) return data[id].delay[n-1];
return car[id].delay;
}
// Tells which lane matches with a given lateral position
RangeLane y_to_lane(RangeY y){
for(i : int[1,nb_lane]){
if(y<=marking[i]) return i-1;
}
return nb_lane-1; // for compilation needs
}
// Put the new value of the flag in regard to GPS trajectory
if(id != n and prio[n] and possible_collision(long[id], lat[id], long[n], lat[n])) return true;
}
// check obstacles
for(i : int[0,traj_range-1]){
if(long[id][i] > J_end and lat[id][i] < J_sup) return true; // junction lane after end of zone
if(long[id][i] < J_beg and lat[id][i] < J_sup and lat[id][i] > J_inf) return true; // beetween junction lane and highway out of the junction zone
}
return false;
}
void decision(RangeId id){
RangeD temp_dir;
RangeA temp_acc;
bool prio[nb_car]; // list of prioritary vehicles
RangeX long[nb_car][traj_range];
RangeY lat[nb_car][traj_range];
RangeDelay temp_del;
RangeLane temp_goal;
if(car[id].on_the_road){
// Choosing best possible choices in regard of GPS indication
car[id].goal := navigation(id);
temp_acc := max_acceleration;
temp_del := 0;
temp_goal := car[id].goal;
// Computing the list of other vehicles that have priority
for(n : int[0,nb_car-1]){
if(car[n].on_the_road){
if(car[id].posX < car[n].posX or (car[id].posX == car[n].posX and car[id].posY < car[n].posY)) prio[n] := true;