No commits in common. 'bc6d574ed6f8df9efb7ef6f28aff25ee326e2bd5' and '1cdea8875e3485a33214e17bdb781cd73b978413' have entirely different histories.
bc6d574ed6
...
1cdea8875e
12 changed files with 84 additions and 330 deletions
-
59car_pedestrian_mdp.prism
-
64car_pedestrian_simulator.py
-
13msg_delivery_blanko.prism
-
11msg_delivery_in_class.dot
-
BINmsg_delivery_in_class.dot.pdf
-
14msg_delivery_in_class.prism
-
30robot_1D_in_class.dot
-
BINrobot_1D_in_class.dot.pdf
-
29robot_1D_in_class.prism
-
5shootout.prism
-
118task_scheduling.prism
-
71task_scheduling_simulator.py
@ -1,59 +0,0 @@ |
|||||
mdp |
|
||||
|
|
||||
const int lanes = 5; // Counting the sidewalks as lanes |
|
||||
const int streetLength = 20; |
|
||||
|
|
||||
const int maxVelocity = 3; |
|
||||
const int minVelocity = 1; |
|
||||
|
|
||||
const int carLaneInit = 2; |
|
||||
const double probFalling = 2/9; |
|
||||
|
|
||||
global move : [0..1] init 0; // 0: car 1: pedestrian |
|
||||
|
|
||||
formula ped_at_edge = ped_street_pos = 1 | ped_street_pos = streetLength; |
|
||||
|
|
||||
formula car_at_end = car_street_pos = streetLength; |
|
||||
|
|
||||
// check ped within [car_pos-velocity..car_pos], same lane |
|
||||
formula crash_straight = (car_lane_pos=ped_lane_pos & ped_street_pos>=car_street_pos-velocity & ped_street_pos<=car_street_pos); |
|
||||
// check ped street pos within [car_street_pos-velocity..car_street_pos], ped lane pos within [car_lane_pos-1..car_lane_pos] |
|
||||
formula crash_left = (switched_left & ped_lane_pos>=car_lane_pos-1 & ped_lane_pos<=car_lane_pos & ped_street_pos>=car_street_pos-velocity & ped_street_pos<=car_street_pos); |
|
||||
// check ped street pos within [car_street_pos-velocity..car_street_pos], ped lane pos within [car_lane_pos+1..car_lane_pos] |
|
||||
formula crash_right = (switched_right & ped_lane_pos>=car_lane_pos+1 & ped_lane_pos<=car_lane_pos & ped_street_pos>=car_street_pos-velocity & ped_street_pos<=car_street_pos); |
|
||||
|
|
||||
label "crashed" = crash_straight | crash_left | crash_right; |
|
||||
label "maxedOut" = velocity=maxVelocity; |
|
||||
label "pedCrossed" = ped_lane_pos=lanes; |
|
||||
|
|
||||
module car |
|
||||
|
|
||||
switched_right : bool init false; |
|
||||
switched_left : bool init false; |
|
||||
|
|
||||
car_street_pos : [0..streetLength] init 0; |
|
||||
car_lane_pos : [2..lanes-1] init carLaneInit; |
|
||||
velocity : [minVelocity..maxVelocity] init minVelocity; |
|
||||
|
|
||||
// TODO |
|
||||
|
|
||||
endmodule |
|
||||
|
|
||||
|
|
||||
module pedestrian |
|
||||
|
|
||||
ped_street_pos : [0..streetLength] init floor(streetLength/4); |
|
||||
ped_lane_pos : [1..lanes] init 1; |
|
||||
fell_down : [0..2] init 0; // 1-2: getting up |
|
||||
|
|
||||
[move] move=1 & fell_down=0 -> ((1-probFalling)/4): (ped_lane_pos'=min(lanes,ped_lane_pos+1)) & (move'=0) + |
|
||||
((1-probFalling)/4): (ped_lane_pos'=max(1,ped_lane_pos-1)) & (move'=0) + |
|
||||
((1-probFalling)/4): (ped_street_pos'=min(lanes,ped_street_pos+1)) & (move'=0) + |
|
||||
((1-probFalling)/4): (ped_street_pos'=max(1,ped_street_pos-1)) & (move'=0) + |
|
||||
(probFalling/4): (ped_lane_pos'=min(lanes,ped_lane_pos+1)) & (fell_down'=2) & (move'=0) + |
|
||||
(probFalling/4): (ped_lane_pos'=max(1,ped_lane_pos-1)) & (fell_down'=2) & (move'=0) + |
|
||||
(probFalling/4): (ped_street_pos'=min(lanes,ped_street_pos+1)) & (fell_down'=2) & (move'=0) + |
|
||||
(probFalling/4): (ped_street_pos'=max(1,ped_street_pos-1)) & (fell_down'=2) & (move'=0); |
|
||||
[getUp] move=1 & fell_down>0 -> 1: (fell_down'=fell_down-1) & (move'=0); |
|
||||
|
|
||||
endmodule |
|
||||
@ -1,64 +0,0 @@ |
|||||
import stormpy |
|
||||
import stormpy.simulator |
|
||||
|
|
||||
newline = "\n" |
|
||||
|
|
||||
def printFrame(streetLength, lanes, carPos, pedPos): |
|
||||
sidewalk = "#" * (streetLength+1) |
|
||||
frame = list(sidewalk + (lanes-2)*("_"*(streetLength+1)) + sidewalk) |
|
||||
|
|
||||
frame[(int(carPos[0])-1)*(streetLength+1)+int(carPos[1])+1] = "C" |
|
||||
frame[(int(pedPos[0])-1)*(streetLength+1)+int(pedPos[1])+1] = "P" |
|
||||
for i in range(lanes): |
|
||||
frame[i*(streetLength+1)] = newline |
|
||||
return "".join(frame) |
|
||||
|
|
||||
def mdp(): |
|
||||
options = stormpy.BuilderOptions([]) |
|
||||
options.set_build_state_valuations(True) |
|
||||
options.set_build_choice_labels(True) |
|
||||
options.set_build_all_labels() |
|
||||
prism_program = stormpy.parse_prism_program("/media/car_pedestrian_mdp.prism") |
|
||||
|
|
||||
streetLength = int(str(prism_program.get_constant("streetLength").definition)) |
|
||||
lanes = int(str(prism_program.get_constant("lanes").definition)) |
|
||||
formula_str = "Pmax=? [G !\"crashed\" ];" |
|
||||
#formula_str = "Pmax=? [F \"crashed\" ];" |
|
||||
|
|
||||
print(stormpy.build_model(prism_program)) |
|
||||
formulas = stormpy.parse_properties_for_prism_program(formula_str, prism_program) |
|
||||
model = stormpy.build_sparse_model_with_options(prism_program, options) |
|
||||
initial_state = model.initial_states[0] |
|
||||
assert initial_state == 0 |
|
||||
result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) |
|
||||
assert result.has_scheduler |
|
||||
scheduler = result.scheduler |
|
||||
assert scheduler.memoryless |
|
||||
assert scheduler.deterministic |
|
||||
|
|
||||
dtmc = model.apply_scheduler(scheduler) |
|
||||
print(dtmc) |
|
||||
simulator = stormpy.simulator.create_simulator(dtmc, seed=42) |
|
||||
simulator.set_observation_mode(stormpy.simulator.SimulatorObservationMode.PROGRAM_LEVEL) |
|
||||
|
|
||||
i=0 |
|
||||
while True: |
|
||||
observation, reward, labels = simulator.step() |
|
||||
print(observation, labels) |
|
||||
frame = printFrame(int(streetLength), int(lanes), (observation["car_lane_pos"], observation["car_street_pos"]), (observation["ped_lane_pos"], observation["ped_street_pos"])) |
|
||||
print(frame) |
|
||||
if simulator.is_done() or "pedCrossed" in labels: |
|
||||
print("Pedestrian arrived on the other side!") |
|
||||
break |
|
||||
input("") |
|
||||
with open(f"/media/frame{i:03}.txt", "w") as text_file: |
|
||||
text_file.write(frame) |
|
||||
i+=1 |
|
||||
if "crashed" in labels: |
|
||||
print("Pedestrian did not arrive on the other side!") |
|
||||
break |
|
||||
|
|
||||
|
|
||||
|
|
||||
if __name__ == '__main__': |
|
||||
mdp() |
|
||||
@ -1,13 +0,0 @@ |
|||||
dtmc |
|
||||
|
|
||||
module msg_delivery |
|
||||
|
|
||||
state : [0..3] init 0; |
|
||||
// s = 0 -> start, s=1 -> try, s=2 -> lost, s=3 -> delivered |
|
||||
|
|
||||
[] state = 0 -> (state'=1); |
|
||||
[] state = 1 -> 1/10 : (state'=2) + 9/10 : (state'=3); |
|
||||
[] state = 2 -> (state'=1); |
|
||||
[] state = 3 -> (state'=0); |
|
||||
|
|
||||
endmodule |
|
||||
@ -0,0 +1,11 @@ |
|||||
|
digraph model { |
||||
|
0 [ label = "0[s=0]: {init}" ]; |
||||
|
1 [ label = "1[s=1]: {}" ]; |
||||
|
2 [ label = "2[s=3]: {delivered}" ]; |
||||
|
3 [ label = "3[s=2]: {}" ]; |
||||
|
0 -> 1 [ label= "1" ]; |
||||
|
1 -> 2 [ label= "0.9" ]; |
||||
|
1 -> 3 [ label= "0.1" ]; |
||||
|
2 -> 2 [ label= "1" ]; |
||||
|
3 -> 1 [ label= "1" ]; |
||||
|
} |
||||
@ -0,0 +1,14 @@ |
|||||
|
dtmc |
||||
|
|
||||
|
const double deliverySuccess = 0.9; |
||||
|
|
||||
|
label "delivered" = s=3; |
||||
|
|
||||
|
module msg_delivery |
||||
|
s : [0..3] init 0; |
||||
|
|
||||
|
[] s=0 -> (s'=1); |
||||
|
[] s=1 -> deliverySuccess : (s'=3) + 1-deliverySuccess: (s'=2); |
||||
|
[] s=2 -> (s'=1); |
||||
|
[] s=3 -> (s'=0); |
||||
|
endmodule |
||||
@ -0,0 +1,30 @@ |
|||||
|
digraph model { |
||||
|
0 [ label = "0[position=0]: {init, lava}" ]; |
||||
|
1 [ label = "1[position=1]: {cliff, init}" ]; |
||||
|
2 [ label = "2[position=2]: {cliff, init}" ]; |
||||
|
3 [ label = "3[position=3]: {init}" ]; |
||||
|
4 [ label = "4[position=4]: {init}" ]; |
||||
|
5 [ label = "5[position=5]: {init}" ]; |
||||
|
6 [ label = "6[position=6]: {init}" ]; |
||||
|
7 [ label = "7[position=7]: {cliff, init}" ]; |
||||
|
8 [ label = "8[position=8]: {init}" ]; |
||||
|
9 [ label = "9[position=9]: {init}" ]; |
||||
|
10 [ label = "10[position=10]: {goal, init}" ]; |
||||
|
0 -> 0 [ label= "1" ]; |
||||
|
1 -> 0 [ label= "1" ]; |
||||
|
2 -> 1 [ label= "1" ]; |
||||
|
3 -> 2 [ label= "0.5" ]; |
||||
|
3 -> 4 [ label= "0.5" ]; |
||||
|
4 -> 3 [ label= "0.5" ]; |
||||
|
4 -> 5 [ label= "0.5" ]; |
||||
|
5 -> 4 [ label= "0.5" ]; |
||||
|
5 -> 6 [ label= "0.5" ]; |
||||
|
6 -> 5 [ label= "0.5" ]; |
||||
|
6 -> 7 [ label= "0.5" ]; |
||||
|
7 -> 8 [ label= "1" ]; |
||||
|
8 -> 7 [ label= "0.5" ]; |
||||
|
8 -> 9 [ label= "0.5" ]; |
||||
|
9 -> 8 [ label= "0.5" ]; |
||||
|
9 -> 10 [ label= "0.5" ]; |
||||
|
10 -> 10 [ label= "1" ]; |
||||
|
} |
||||
@ -0,0 +1,29 @@ |
|||||
|
dtmc |
||||
|
|
||||
|
formula isOnSlippery = !isOnGoal & !isOnLava & !isOnLeftCliff & !isOnRightCliff; |
||||
|
formula isOnRightCliff = position=7; |
||||
|
formula isOnLeftCliff = position=1 | position=2; |
||||
|
formula isOnLava = position=0; |
||||
|
formula isOnGoal = position=10; |
||||
|
|
||||
|
label "goal" = isOnGoal; |
||||
|
label "lava" = isOnLava; |
||||
|
label "cliff" = isOnRightCliff | isOnLeftCliff; |
||||
|
|
||||
|
// labels? |
||||
|
const double slipToRight = 0.5; |
||||
|
|
||||
|
init |
||||
|
true |
||||
|
endinit |
||||
|
|
||||
|
module robot_1D |
||||
|
position : [0..10]; |
||||
|
|
||||
|
// commands? |
||||
|
[] isOnSlippery -> slipToRight: (position'=position+1) + 1-slipToRight: (position'=position-1); |
||||
|
[] isOnRightCliff -> (position'=position+1); |
||||
|
[] isOnLeftCliff -> (position'=position-1); |
||||
|
[] isOnGoal | isOnLava -> true; |
||||
|
|
||||
|
endmodule |
||||
@ -1,5 +0,0 @@ |
|||||
dtmc |
|
||||
|
|
||||
module shootout |
|
||||
|
|
||||
endmodule |
|
||||
@ -1,118 +0,0 @@ |
|||||
mdp |
|
||||
|
|
||||
const int MULT_DUR_1 = 8; |
|
||||
const int ADD_DUR_1 = 4; |
|
||||
const double P1_SUCCESS = 1.0; |
|
||||
const int MULT_DUR_2 = 3; |
|
||||
const int ADD_DUR_2 = 3; |
|
||||
const double P2_SUCCESS = 0.8; |
|
||||
|
|
||||
// target state (all tasks complete) |
|
||||
label "tasks_complete" = (task6=3); |
|
||||
label "no_P1_mult" = (mult_tick_1=0); |
|
||||
label "no_P2_mult" = (mult_tick_2=0); |
|
||||
|
|
||||
// reward structure: elapsed time |
|
||||
rewards "time" |
|
||||
task6!=3 : 1; |
|
||||
endrewards |
|
||||
|
|
||||
// reward structures: energy consumption |
|
||||
rewards "energy" |
|
||||
p1=0 : 10/1000; // processor 1 idle |
|
||||
p1>0 : 100/1000; // processor 1 working |
|
||||
p2=0 : 10/1000; // processor 2 idle |
|
||||
p2>0 : 100/1000; // processor 2 working |
|
||||
endrewards |
|
||||
|
|
||||
module scheduler |
|
||||
|
|
||||
//┌t1─┐ ┌t3─────┐ ┌t5───────┐ |
|
||||
//│A+B│-->│Cx(A+B)│-->│DxCx(A+B)│--. ┌t6─────────────────────┐ |
|
||||
//└───┘\ └───────┘ └─────────┘ \___\│DxCx(A+B)+((A+B)+(CxD))│ |
|
||||
//┌t2─┐ \ ┌t4─────────┐ / /└───────────────────────┘ |
|
||||
//│CxD│-->│(A+B)+(CxD)│------------° |
|
||||
//└───┘ └───────────┘ |
|
||||
|
|
||||
task1 : [0..3]; // A+B, add |
|
||||
task2 : [0..3]; // CxD, mult |
|
||||
task3 : [0..3]; // Cx(A+B), mult |
|
||||
task4 : [0..3]; // (A+B)+(CxD), add |
|
||||
task5 : [0..3]; // DxCx(A+B), mult |
|
||||
task6 : [0..3]; // (DxCx(A+B)) + ((A+B)+(CxD)), add |
|
||||
|
|
||||
p1_idle : bool init true; |
|
||||
p2_idle : bool init true; |
|
||||
|
|
||||
// task status: |
|
||||
// 0 - not started |
|
||||
// 1 - running on processor 1 |
|
||||
// 2 - running on processor 2 |
|
||||
// 3 - task complete |
|
||||
|
|
||||
// start task 1 |
|
||||
[t1p1] task1=0 & p1_idle-> (task1'=1) & (p1_idle'=false); |
|
||||
[t1p2] task1=0 & p2_idle-> (task1'=2) & (p2_idle'=false); |
|
||||
|
|
||||
// start task 2 |
|
||||
[t2p1] task2=0 & p1_idle-> (task2'=1) & (p1_idle'=false); |
|
||||
[t2p2] task2=0 & p2_idle-> (task2'=2) & (p2_idle'=false); |
|
||||
|
|
||||
// start task 3 (must wait for task 1 to complete) |
|
||||
[t3p1] task3=0 & task1=3 & p1_idle-> (task3'=1) & (p1_idle'=false); |
|
||||
[t3p2] task3=0 & task1=3 & p2_idle-> (task3'=2) & (p2_idle'=false); |
|
||||
|
|
||||
// start task 4 (must wait for tasks 1 and 2 to complete) |
|
||||
[t4p1] task4=0 & task1=3 & task2=3 & p1_idle-> (task4'=1) & (p1_idle'=false); |
|
||||
[t4p2] task4=0 & task1=3 & task2=3 & p2_idle-> (task4'=2) & (p2_idle'=false); |
|
||||
|
|
||||
// start task 5 (must wait for task 3 to complete) |
|
||||
[t5p1] task5=0 & task3=3 & p1_idle-> (task5'=1) & (p1_idle'=false); |
|
||||
[t5p2] task5=0 & task3=3 & p2_idle-> (task5'=2) & (p2_idle'=false); |
|
||||
|
|
||||
// start task 6 (must wait for tasks 4 and 5 to complete) |
|
||||
[t6p1] task6=0 & task4=3 & task5=3 & p1_idle -> (task6'=1) & (p1_idle'=false); |
|
||||
[t6p2] task6=0 & task4=3 & task5=3 & p2_idle -> (task6'=2) & (p2_idle'=false); |
|
||||
|
|
||||
// a task finishes on processor 1 |
|
||||
[p1_done] task1=1 & p1=3 -> (task1'=3) & (p1_idle'=true); |
|
||||
[p1_done] task2=1 & p1=3 -> (task2'=3) & (p1_idle'=true); |
|
||||
[p1_done] task3=1 & p1=3 -> (task3'=3) & (p1_idle'=true); |
|
||||
[p1_done] task4=1 & p1=3 -> (task4'=3) & (p1_idle'=true); |
|
||||
[p1_done] task5=1 & p1=3 -> (task5'=3) & (p1_idle'=true); |
|
||||
[p1_done] task6=1 & p1=3 -> (task6'=3) & (p1_idle'=true); |
|
||||
|
|
||||
// a task finishes on processor 2 |
|
||||
[p2_done] task1=2 & p2=3 -> (task1'=3) & (p2_idle'=true); |
|
||||
[p2_done] task2=2 & p2=3 -> (task2'=3) & (p2_idle'=true); |
|
||||
[p2_done] task3=2 & p2=3 -> (task3'=3) & (p2_idle'=true); |
|
||||
[p2_done] task4=2 & p2=3 -> (task4'=3) & (p2_idle'=true); |
|
||||
[p2_done] task5=2 & p2=3 -> (task5'=3) & (p2_idle'=true); |
|
||||
[p2_done] task6=2 & p2=3 -> (task6'=3) & (p2_idle'=true); |
|
||||
|
|
||||
[] task6=3 -> 1 : true; |
|
||||
[] task6=3 -> 1 : true; |
|
||||
|
|
||||
endmodule |
|
||||
|
|
||||
// processor 1 |
|
||||
module P1 |
|
||||
p1 : [0..3]; // 0 inactive, 1 - adding, 2 - multiplying, 3 - done |
|
||||
mult_tick_1 : ; |
|
||||
add_tick_1 : ; |
|
||||
|
|
||||
[p1_done] p1=3 -> 1: (p1'=0) & (mult_tick_1'=0) & (add_tick_1'=0); // finished task |
|
||||
|
|
||||
endmodule |
|
||||
|
|
||||
// processor 2 |
|
||||
// Note: You may also use module renaming to define processor 2 |
|
||||
module P2 |
|
||||
p2 : [0..3]; // 0 inactive, 1 - adding, 2 - multiplying, 3 - done |
|
||||
mult_tick_2 : ; |
|
||||
add_tick_2 : ; |
|
||||
|
|
||||
|
|
||||
[p2_done] p2=3 -> 1: (p2'=0) & (mult_tick_2'=0) & (add_tick_2'=0); // finished task |
|
||||
|
|
||||
endmodule |
|
||||
@ -1,71 +0,0 @@ |
|||||
import stormpy |
|
||||
import stormpy.simulator |
|
||||
|
|
||||
|
|
||||
def mdp(): |
|
||||
options = stormpy.BuilderOptions([]) |
|
||||
options.set_build_state_valuations(True) |
|
||||
options.set_build_choice_labels(True) |
|
||||
options.set_build_all_labels() |
|
||||
options.set_build_all_reward_models() |
|
||||
|
|
||||
program = stormpy.parse_prism_program("/media/task_graph_scheduling.prism") |
|
||||
formula_str = "R{\"time\"}min=? [ F \"tasks_complete\" ];" |
|
||||
formulas = stormpy.parse_properties_for_prism_program(formula_str, program) |
|
||||
model = stormpy.build_sparse_model_with_options(program, options) |
|
||||
print(model) |
|
||||
|
|
||||
initial_state = model.initial_states[0] |
|
||||
assert initial_state == 0 |
|
||||
result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) |
|
||||
assert result.has_scheduler |
|
||||
scheduler = result.scheduler |
|
||||
assert scheduler.memoryless |
|
||||
assert scheduler.deterministic |
|
||||
|
|
||||
dtmc = model.apply_scheduler(scheduler) |
|
||||
print(dtmc) |
|
||||
simulator = stormpy.simulator.create_simulator(dtmc, seed=42) |
|
||||
simulator.set_observation_mode(stormpy.simulator.SimulatorObservationMode.PROGRAM_LEVEL) |
|
||||
|
|
||||
step_counter = 0 |
|
||||
busy1_counter = 0 |
|
||||
busy2_counter = 0 |
|
||||
print(""" |
|
||||
┌t1─┐ ┌t3─────┐ ┌t5───────┐ |
|
||||
│A+B│-->│Cx(A+B)│-->│DxCx(A+B)│--. ┌t6─────────────────────┐ |
|
||||
└───┘\ └───────┘ └─────────┘ \___\│DxCx(A+B)+((A+B)+(CxD))│ |
|
||||
┌t2─┐ \ ┌t4─────────┐ / /└───────────────────────┘ |
|
||||
│CxD│-->│(A+B)+(CxD)│------------° |
|
||||
└───┘ └───────────┘ |
|
||||
""") |
|
||||
print(" " * 32 + "[+,x,x,+,x,+]") |
|
||||
while True: |
|
||||
if simulator.is_done(): |
|
||||
print(f"Tasks complete! Ratio: (approx.): {busy1_counter/(busy1_counter+busy2_counter):1.4f}/{busy2_counter/(busy1_counter+busy2_counter):1.4f}, Steps needed (approx.): {step_counter}") |
|
||||
break |
|
||||
observation, reward, labels = simulator.step() |
|
||||
#input("") |
|
||||
busy1 = str(observation["p1_idle"]) != ("true") |
|
||||
busy2 = str(observation["p2_idle"]) != ("true") |
|
||||
if busy1: busy1_counter += 1 |
|
||||
if busy2: busy2_counter += 1 |
|
||||
tasks = [str(observation[f"task{i}"]) for i in range(1,7)] |
|
||||
print(f"Step {step_counter:3}: P1/2:{'busy' if busy1 else 'idle'}/{'busy' if busy2 else 'idle'} tasks: [{','.join(tasks)}], {str(observation['add_tick_1'])},{str(observation['mult_tick_1'])},{str(observation['add_tick_2'])},{str(observation['mult_tick_2'])},labels: {labels if len(labels) != 0 else ''}, ") |
|
||||
step_counter += 1 |
|
||||
try: |
|
||||
with open("/media/induced_scheduling_dtmc.dot", "w") as text_file: |
|
||||
text_file.write(dtmc.to_dot()) |
|
||||
except Exception as e: |
|
||||
print(e) |
|
||||
print("Could not write to file.") |
|
||||
input("Hit enter to evaluate: 'P=? [ F<={i} \"tasks_complete\" ]' on the DTMC:") |
|
||||
print(dtmc) |
|
||||
|
|
||||
for i in range(30,61): |
|
||||
formula_str = f"P=? [ F<={i} \"tasks_complete\" ]" |
|
||||
formulas = stormpy.parse_properties_for_prism_program(formula_str, program) |
|
||||
result = stormpy.model_checking(dtmc, formulas[0]) |
|
||||
print(f"Probability to finish within {i} timesteps : {result.at(dtmc.initial_states[0]):>1.12f}") |
|
||||
if __name__ == '__main__': |
|
||||
mdp() |
|
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue