// intersection with two double direction roads
map_name = "san_francisco";
time = 12:00;
weather = {rain:0.5, snow: 0.1, wetness: heavy};
evn = Environment(time, weather);

car_model = "gt_sensors";
ego_init_position ="lane_540"->50; 
ego_init_state = (ego_init_position);
ego_target_position = "lane_572"->50; 
ego_target_state = (ego_target_position);
vehicle_type = (car_model);
ego_vehicle = AV(ego_init_state, ego_target_state, vehicle_type);

//npc1: move from lane_574 to lane_569
npc1_init_position =  "lane_574"->100;
npc1_init_state = (npc1_init_position, ,6);
npc1_dest_state = ("lane_569"->30);
npc1_model = "Sedan";
npc1_type = (npc1_model);
npc1 = Vehicle(npc1_init_state,  , npc1_dest_state, npc1_type);

//npc2: move from lane_564 to lane_568
npc2_init_position =  "lane_564"->10;
npc2_init_state = (npc2_init_position, ,6);
npc2_dest_state = ("lane_568"->50);
npc2 = Vehicle(npc2_init_state,  , npc2_dest_state);

//npc3: move from lane_565 to lane_569
npc3_init_position =  "lane_565"->10;
npc3_init_state = (npc3_init_position, ,6);
npc3_dest_state = ("lane_569"->50);
npc3 = Vehicle(npc3_init_state,  , npc3_dest_state);

//npc4: move from lane_570 to lane_566
npc4_init_position =  "lane_570"->10;
npc4_init_state = (npc4_init_position, ,6);
npc4_dest_state = ("lane_566"->50);
npc4 = Vehicle(npc4_init_state,  , npc4_dest_state);

//npc5: move from lane_571 to lane_567
npc5_init_position =  "lane_571"->77;
npc5_init_state = (npc5_init_position, ,6);
npc5_dest_state = ("lane_567"->30);
npc5 = Vehicle(npc5_init_state,  , npc5_dest_state); 

scenario0 = CreateScenario{load(map_name);
			        ego_vehicle;
			        {npc1, npc2, npc3, npc4, npc5}; 
			        {}; // no pedestrians;
			        {}; // no obstacles;
			        evn;
};


Trace trace = EXE(scenario0);
ego_state = trace[ego];
npc1_truth = trace[truth][npc1];
npc2_truth = trace[truth][npc2];
npc3_truth = trace[truth][npc3];
npc4_truth = trace[truth][npc4];
npc5_truth = trace[truth][npc5];

dis1 = dis(ego_state, npc1_truth);
dis2 = dis(ego_state, npc2_truth);
dis3 = dis(ego_state, npc3_truth);
dis4 = dis(ego_state, npc4_truth);
dis5 = dis(ego_state, npc5_truth);

// assertion 0
trace |= (G (dis1>=0.5 & dis2>=0.5 & dis3>=0.5 & dis4>=0.5 & dis5>=0.5)) & (F (dis(ego_state, ego_target_position)<=2.0));