car_pedestrian_mdp.prism

@@ -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

car_pedestrian_simulator.py

@@ -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()

msg_delivery_blanko.prism

@@ -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

msg_delivery_in_class.dot

@@ -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" ];
+}

msg_delivery_in_class.prism

@@ -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

robot_1D_in_class.dot

@@ -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" ];
+}

robot_1D_in_class.prism

@@ -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

shootout.prism

@@ -1,5 +0,0 @@
-dtmc
-
-module shootout
-
-endmodule

task_scheduling.prism

@@ -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

task_scheduling_simulator.py

@@ -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()