//Junction with stop sign

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_53"->50;
ego_init_state = (ego_init_position);
ego_target_position = "lane_50"->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_61 to lane_33
npc1_init_position =  "lane_61"->30;
npc1_init_state = (npc1_init_position, ,5.8);
npc1_waypoint = (("lane_707"->1, , 3), ("lane_33"->5, ,7));
npc1_dest_state = ("lane_33"->50);
npc1 = Vehicle(npc1_init_state, Waypoint(npc1_waypoint) , npc1_dest_state);

//npc2: move from lane_60 to lane_32
npc2_init_position =  "lane_60"->20;
npc2_init_state = (npc2_init_position, ,5);
npc2_waypoint = (("lane_708"->1, , 3), ("lane_32"->5, ,7));
npc2_dest_state = ("lane_32"->50);
npc2 = Vehicle(npc2_init_state, Waypoint(npc2_waypoint) , npc2_dest_state);

//npc3: move from lane_60 to lane_51
npc3_init_position =  "lane_60"->30;
npc3_init_state = (npc3_init_position, ,5.5);
npc3_waypoint = (("lane_696"->1, , 3), ("lane_51"->5, ,7));
npc3_dest_state = ("lane_51"->50);
npc3 = Vehicle(npc3_init_state, Waypoint(npc3_waypoint) , npc3_dest_state);

//npc4: move from lane_34 to lane_51
npc4_init_position =  "lane_34"->150;
npc4_init_state = (npc4_init_position, ,5.5);
npc4_waypoint = (("lane_697"->1, , 3), ("lane_51"->5, ,7));
npc4_dest_state = ("lane_51"->50);
npc4 = Vehicle(npc4_init_state, Waypoint(npc4_waypoint) , npc4_dest_state);

//npc5: move from lane_35 to lane_63
npc5_init_position =  "lane_35"->170;
npc5_init_state = (npc5_init_position, ,5.5);
npc5_waypoint = (("lane_704"->1, , 3), ("lane_63"->5, ,7));
npc5_dest_state = ("lane_63"->50);
npc5 = Vehicle(npc5_init_state, Waypoint(npc5_waypoint) , npc5_dest_state);

//npc6: move from lane_34 to lane_50
npc6_init_position =  "lane_34"->170;
npc6_init_state = (npc6_init_position, ,5.5);
npc6_waypoint = (("lane_710"->1, , 3), ("lane_50"->5, ,7));
npc6_dest_state = ("lane_50"->150);
npc6 = Vehicle(npc6_init_state, Waypoint(npc6_waypoint) , npc6_dest_state);

//npc7: move from lane_34 to lane_62
npc7_init_position =  "lane_34"->160;
npc7_init_state = (npc7_init_position, ,5.4);
npc7_dest_state = ("lane_62"->50);
npc7 = Vehicle(npc7_init_state,, npc7_dest_state);

npc = {npc1, npc2, npc3, npc4, npc5, npc6, npc7};

scenario0 = CreateScenario{load(map_name);
			        ego_vehicle;
			        npc;
			        {}; // 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];
npc6_truth = trace[truth][npc6];
npc7_truth = trace[truth][npc7];

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);
dis6 = dis(ego_state, npc6_truth);
dis7 = dis(ego_state, npc7_truth);


// assertion 0
statement1 = dis1>=0.5 & dis2>=0.5 & dis3>=0.5 & dis4>=0.5 & dis5>=0.5 & dis6>=0.5 & dis7>=0.5;
statement2 = dis(ego_state, ego_target_position)<=2.0;

trace |= (G statement1) & (F statement2);