<!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>
<?xml version="1.0" encoding="utf-8"?>
<!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>//Global clocks
clock C1; // in 1/scale seconds
clock C2; // in 1/scale seconds
clock C3; // in 1/scale seconds
clock x_A; // in 1/scale seconds
clock x_B; // in 1/scale seconds
clock x_C; // in 1/scale seconds
//Synchronisation channel
broadcast chan k;
...
...
@@ -60,7 +60,7 @@ const int J_sup := marking[1]+(C_wid/2); // used for posY update
const int nb_car := 3; // number of vehicles (>= 2)
typedef int[0,nb_car-1] RangeId; // ids range
const int freq[nb_car] := {10,10,10}; // activation sample of the controler for each vehicle in 1/scale second
const int ctr_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] := {0,3000,4000}; // initial longitudinal position for each vehicle in 1/scale meters