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.
40 lines
836 B
40 lines
836 B
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];
|
|
|
|
|
|
endmodule
|
|
|
|
|
|
module pedestrian
|
|
|
|
ped_street_pos : [0..streetLength] init floor(streetLength/2);
|
|
ped_lane_pos : [1..lanes] init 1;
|
|
|
|
|
|
endmodule
|