|
|
@ -0,0 +1,55 @@ |
|
|
|
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 |