<!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>//INSTRUCTION : Change the values of the parameters bellow
// 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
//INSTRUCTION : Define here as constants any complementary parameters you need for your decision protocol
// Constants and data types obtained from decision related parameters
//INSTRUCTION : For each decision related variable and variable to be communicate, duplicate the following line and replace VAR with the variable and [min_rangeVAR,max_rangeVAR] by the range you need for this variable.
typedef int[min_rangeVAR,max_rangeVAR] RangeVAR;
// 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
}
}
}
// Send comm variables value to other vehicles
void communicate(RangeId id){
for(n : int[0,nb_car-1]){
if(id<n){
//INSTRUCTION : For each comm variable, duplicate the following line and replace VAR with the variable.
comm[n].VAR[id] := car[id].VAR;
}
if(id>n){
//INSTRUCTION : For each comm variable, duplicate the following line and replace VAR with the variable.
comm[n].VAR[id-1] := car[id].VAR;
}
}
}
//INSTRUCTION : For each comm variable, duplicate the following function and replace VAR with the variable.
// Give the VAR value that id knows about n
RangeLane read_VAR(RangeId id, RangeId n){
if(id>n) return comm[id].VAR[n];
if(id<n) return comm[id].VAR[n-1];
return car[id].VAR;
}
// 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
}
//INSTRUCTION : Define here all the subfunctions to be used in decision main function. Must not modifiy any variable in the data sctruture.
void decision(RangeId id){
RangeD temp_dir;
RangeA temp_acc;
//INSTRUCTION : Define here variables to be used in decision main function.
if(car[id].on_the_road){
//INSTRUCTION : Define here decision main function. Must not modifiy any variable in the data sctruture.
//Applying decision
//INSTRUCTION : Define here new values for decision related variables in car[id].
car[id].direction := temp_dir;
car[id].acceleration := temp_acc;
}
}
// Time to collision between two vehicles in 1/scale seconds, dont go above 100s