You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
55 lines
2.1 KiB
55 lines
2.1 KiB
mdp
|
|
|
|
const int lanes = 5; // Counting the sidewalks as lanes
|
|
const int streetLength = 20;
|
|
|
|
const int maxVelocity = 3;
|
|
const int minVelocity = 1;
|
|
|
|
const int pedMove = 0;
|
|
|
|
const int car1Move = 1;
|
|
|
|
const int car1LaneInit = 2;
|
|
|
|
const double probCrossStreet = 0.2;
|
|
|
|
global move : [0..1] init 0;
|
|
|
|
formula ped_at_edge = ped_street_pos = 1 | ped_street_pos = streetLength;
|
|
|
|
formula car_at_end = car_street_pos = streetLength;
|
|
|
|
formula crash = (car_street_pos =ped_street_pos&car_lane_pos =ped_lane_pos);
|
|
label "crashed" = crash;
|
|
label "maxedOut" = velocity=maxVelocity;
|
|
|
|
module car
|
|
|
|
car_street_pos : [0..streetLength];
|
|
car_lane_pos : [2..lanes-1] init car1LaneInit;
|
|
velocity : [minVelocity..maxVelocity];
|
|
|
|
[changeLeft] move=car1Move & car_lane_pos>2 -> (car_lane_pos'=car_lane_pos-1) & (car_street_pos'=mod(car_street_pos+velocity,streetLength)) & (move'=pedMove);
|
|
[changeRight] move=car1Move & car_lane_pos<lanes-1 -> (car_lane_pos'=car_lane_pos+1) & (car_street_pos'=mod(car_street_pos+velocity,streetLength)) & (move'=pedMove);
|
|
|
|
[accelerate] move=car1Move -> (car_street_pos'=mod(car_street_pos+velocity,streetLength)) & (velocity'=min(velocity+1,maxVelocity)) & (move'=pedMove);
|
|
[decelerate] move=car1Move -> (car_street_pos'=mod(car_street_pos+velocity,streetLength)) & (velocity'=max(velocity-1,minVelocity)) & (move'=pedMove);
|
|
|
|
endmodule
|
|
|
|
|
|
module pedestrian
|
|
|
|
ped_street_pos : [0..streetLength] init floor(streetLength/2);
|
|
ped_lane_pos : [1..lanes] init 1;
|
|
|
|
[] move=pedMove & ped_lane_pos=1 -> (1/3 * (1 - probCrossStreet)) : (move'=car1Move) +
|
|
(1/3 * (1 - probCrossStreet)) : (move'=car1Move) & (ped_street_pos'=min(ped_street_pos+1,streetLength)) +
|
|
(1/3 * (1 - probCrossStreet)) : (move'=car1Move) & (ped_street_pos'=max(ped_street_pos-1,1) ) +
|
|
probCrossStreet : (move'=car1Move) & (ped_lane_pos'=2);
|
|
|
|
[] move=pedMove & ped_lane_pos>1 & ped_lane_pos<lanes -> (move'=car1Move) & (ped_lane_pos'=ped_lane_pos+1);
|
|
[] move=pedMove & ped_lane_pos=lanes -> true;
|
|
|
|
endmodule
|