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.
42 lines
1.6 KiB
42 lines
1.6 KiB
dtmc
|
|
|
|
const int lanes = 4; // Counting the sidewalk as a lane
|
|
const int street_length = 20;
|
|
|
|
const double prob_cross_street = 0.1;
|
|
|
|
global move : [0..1] init 0;
|
|
|
|
formula ped_at_edge = ped_street_pos = 1 | ped_street_pos = street_length;
|
|
|
|
formula car_at_end = car_street_pos = street_length;
|
|
|
|
formula crash = car_street_pos = ped_street_pos & ped_lane_pos = car_lane_pos;
|
|
label "crashed" = crash;
|
|
|
|
module car
|
|
|
|
car_street_pos : [0..street_length];
|
|
car_lane_pos : [2..lanes-1];
|
|
|
|
[] move=0 -> 1/3 : (car_lane_pos'=min(car_lane_pos+1, lanes-1)) & (car_street_pos'=mod(car_street_pos+1,street_length)) & (move'=1) +
|
|
1/3 : (car_lane_pos'=max(2, car_lane_pos-1)) & (car_street_pos'=mod(car_street_pos+1,street_length)) & (move'=1) +
|
|
1/3 : (car_street_pos'=mod(car_street_pos+1,street_length)) & (move'=1);
|
|
|
|
|
|
endmodule
|
|
|
|
module pedestrian
|
|
|
|
ped_street_pos : [0..street_length] init floor(street_length/2);
|
|
ped_lane_pos : [1..lanes] init 1;
|
|
|
|
[] move=1 & ped_lane_pos=1 -> (1/3 * (1 - prob_cross_street)) : (move'=0) +
|
|
(1/3 * (1 - prob_cross_street)) : (move'=0) & (ped_street_pos'=min(ped_street_pos+1,street_length)) +
|
|
(1/3 * (1 - prob_cross_street)) : (move'=0) & (ped_street_pos'=max(ped_street_pos-1,1) ) +
|
|
prob_cross_street : (move'=0) & (ped_lane_pos'=2);
|
|
|
|
[] move=1 & ped_lane_pos>1 & ped_lane_pos<lanes -> (move'=0) & (ped_lane_pos'=ped_lane_pos+1);
|
|
|
|
|
|
endmodule
|