diff --git a/first_try.prism b/first_try.prism index 339b125..ac112f8 100644 --- a/first_try.prism +++ b/first_try.prism @@ -3,15 +3,33 @@ mdp const int initY = 40; const int initX = 80; -const int maxY = 240; -const int minX = 12; -const int maxX = 147; +const int maxY = 560; +const int minX = 4; +const int maxX = 144; -formula HitTree = (12241 & x<73) & (y>164 & y<170)); //(y=168)); +formula Passed_Gate_2 = ((x>71 & x<104) & (y>257 & y<262)); //(y=261)); +formula Passed_Gate_3 = ((x>81 & x<113) & (y>349 & y<355)); //(y=353)); +formula Passed_Gate_4 = ((x>55 & x<88) & (y>442 & y<448)); //(y=446)); +formula Passed_Gate_5 = ((x>79 & x<110) & (y>534 & y<540)); //(y=538)); + +formula Tree_1 = ((x>=124 & x<=134) & (y>=194 & y<=200)); +formula Tree_2 = ((x>=32 & x<=42) & (y>=291 & y<=297)); +formula Tree_3 = ((x>=28 & x<=38) & (y>=321 & y<=327)); +formula Tree_4 = ((x>=12 & x<=22) & (y>=412 & y<=418)); +formula Tree_5 = ((x>=129 & x<=139) & (y>=472 & y<=480)); +formula Tree_6 = ((x>=140 & x<=144) & (y>=502 & y<=510)); + +formula Hit_Tree = Tree_1 | Tree_2 | Tree_3 | Tree_4 | Tree_5 | Tree_6; +formula Hit_Gate = Gate_1 | Gate_2 | Gate_3 | Gate_4 | Gate_5; -formula PassedGates = (1581 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(PassedGates|HitTree|HitGate)); - [right] !done & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(PassedGates|HitTree|HitGate)); - [noop] !done & move=0 -> (move'=1) & (done'=(PassedGates|HitTree|HitGate)); + passed_gate_1 : bool init false; + passed_gate_2 : bool init false; + passed_gate_3 : bool init false; + passed_gate_4 : bool init false; + passed_gate_5 : bool init false; + + [g1_left] !passed_gate_1 & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_1'=(Passed_Gate_1)); + [g1_right] !passed_gate_1 & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_1'=(Passed_Gate_1)); + [g1_noop] !passed_gate_1 & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_1'=(Passed_Gate_1)); + + [g2_left] !passed_gate_2 & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_2'=(Passed_Gate_2)); + [g2_right] !passed_gate_2 & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_2'=(Passed_Gate_2)); + [g2_noop] !passed_gate_2 & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_2'=(Passed_Gate_2)); + + [g3_left] !passed_gate_3 & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_3'=(Passed_Gate_3)); + [g3_right] !passed_gate_3 & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_3'=(Passed_Gate_3)); + [g3_noop] !passed_gate_3 & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_3'=(Passed_Gate_3)); + + [g4_left] !passed_gate_4 & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_4'=(Passed_Gate_4)); + [g4_right] !passed_gate_4 & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_4'=(Passed_Gate_4)); + [g4_noop] !passed_gate_4 & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_4'=(Passed_Gate_4)); + + [g5_left] !passed_gate_5 & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_5'=(Passed_Gate_5)); + [g5_right] !passed_gate_5 & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_5'=(Passed_Gate_5)); + [g5_noop] !passed_gate_5 & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate))& (passed_gate_5'=(Passed_Gate_5)); + + [left] !done & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate)); + [right] !done & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate)); + [noop] !done & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate)); [left] done & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1); [right] done & move=0 & ski_position<14 -> (ski_position'=ski_position+1) & (move'=1); @@ -45,27 +89,44 @@ module updateX [update_x] move=2 & standstill>=8 -> (move'=0); [update_x] move=2 & standstill<8 & (ski_position=7 | ski_position=8) -> (move'=0); - [update_x] move=2 & standstill<8 & ski_position=6 -> 0.1: (x'=max(minX,x-3)) + 0.7: (x'=max(minX,x-4)) + 0.2: (x'=max(minX,x-5)) & (move'=0); - [update_x] move=2 & standstill<8 & ski_position=9 -> 0.1: (x'=min(maxX,x+3)) + 0.7: (x'=min(maxX,x+4)) + 0.2: (x'=min(maxX,x+5)) & (move'=0); + [update_x] move=2 & standstill<8 & ski_position=6 -> 0.1: (x'=max(minX,x-2)) + 0.7: (x'=max(minX,x-4)) + 0.2: (x'=max(minX,x-6)) & (move'=0); + [update_x] move=2 & standstill<8 & ski_position=9 -> 0.1: (x'=min(maxX,x+2)) + 0.7: (x'=min(maxX,x+4)) + 0.2: (x'=min(maxX,x+6)) & (move'=0); - [update_x] move=2 & standstill<8 & (ski_position=4 | ski_position=5) -> 0.1: (x'=max(minX,x-5)) + 0.7: (x'=max(minX,x-6)) + 0.2: (x'=max(minX,x-7)) & (move'=0); - [update_x] move=2 & standstill<8 & (ski_position=10 | ski_position=11) -> 0.1: (x'=min(maxX,x+5)) + 0.7: (x'=min(maxX,x+6)) + 0.2: (x'=min(maxX,x+7)) & (move'=0); + [update_x] move=2 & standstill<8 & (ski_position=4 | ski_position=5) -> 0.1: (x'=max(minX,x-4)) + 0.7: (x'=max(minX,x-6)) + 0.2: (x'=max(minX,x-8)) & (move'=0); + [update_x] move=2 & standstill<8 & (ski_position=10 | ski_position=11) -> 0.1: (x'=min(maxX,x+4)) + 0.7: (x'=min(maxX,x+6)) + 0.2: (x'=min(maxX,x+8)) & (move'=0); - [update_x] move=2 & standstill<8 & (ski_position=2 | ski_position=3) -> 0.1: (x'=max(minX,x-5)) + 0.7: (x'=max(minX,x-6)) + 0.2: (x'=max(minX,x-7)) & (move'=0); - [update_x] move=2 & standstill<8 & (ski_position=12 | ski_position=13) -> 0.1: (x'=min(maxX,x+5)) + 0.7: (x'=min(maxX,x+6)) + 0.2: (x'=min(maxX,x+7)) & (move'=0); + [update_x] move=2 & standstill<8 & (ski_position=2 | ski_position=3) -> 0.1: (x'=max(minX,x-4)) + 0.7: (x'=max(minX,x-6)) + 0.2: (x'=max(minX,x-8)) & (move'=0); + [update_x] move=2 & standstill<8 & (ski_position=12 | ski_position=13) -> 0.1: (x'=min(maxX,x+4)) + 0.7: (x'=min(maxX,x+6)) + 0.2: (x'=min(maxX,x+8)) & (move'=0); - [update_x] move=2 & standstill<8 & (ski_position=1) -> 0.1: (x'=max(minX,x-0)) + 0.7: (x'=max(minX,x-2)) + 0.2: (x'=max(minX,x-3)) & (move'=0); - [update_x] move=2 & standstill<8 & (ski_position=14) -> 0.1: (x'=min(maxX,x+0)) + 0.7: (x'=min(maxX,x+2)) + 0.2: (x'=min(maxX,x+3)) & (move'=0); + [update_x] move=2 & standstill<8 & (ski_position=1) -> 0.1: (x'=max(minX,x-0)) + 0.7: (x'=max(minX,x-2)) + 0.2: (x'=max(minX,x-4)) & (move'=0); + [update_x] move=2 & standstill<8 & (ski_position=14) -> 0.1: (x'=min(maxX,x+0)) + 0.7: (x'=min(maxX,x+2)) + 0.2: (x'=min(maxX,x+4)) & (move'=0); endmodule rewards - [left] !done & PassedGates : 100; - [right] !done & PassedGates : 100; - [noop] !done & PassedGates : 100; - [left] !done & (HitTree) : -200; - [right] !done & (HitTree) : -200; - [noop] !done & (HitTree) : -200; - [left] !done & (HitGate) : -150; - [right] !done & (HitGate) : -150; - [noop] !done & (HitGate) : -150; + [g1_left] !passed_gate_1 & Passed_Gate_1: 100; + [g1_right] !passed_gate_1 & Passed_Gate_1: 100; + [g1_noop] !passed_gate_1 & Passed_Gate_1: 100; + + [g2_left] !passed_gate_2 & Passed_Gate_2: 100; + [g2_right] !passed_gate_2 & Passed_Gate_2: 100; + [g2_noop] !passed_gate_2 & Passed_Gate_2: 100; + + [g3_left] !passed_gate_3 & Passed_Gate_3: 100; + [g3_right] !passed_gate_3 & Passed_Gate_3: 100; + [g3_noop] !passed_gate_3 & Passed_Gate_3: 100; + + [g4_left] !passed_gate_4 & Passed_Gate_4: 100; + [g4_right] !passed_gate_4 & Passed_Gate_4: 100; + [g4_noop] !passed_gate_4 & Passed_Gate_4: 100; + + [g5_left] !passed_gate_5 & Passed_Gate_5: 100; + [g5_right] !passed_gate_5 & Passed_Gate_5: 100; + [g5_noop] !passed_gate_5 & Passed_Gate_5: 100; + + [left] !done & (Hit_Tree) : -100; + [right] !done & (Hit_Tree) : -100; + [noop] !done & (Hit_Tree) : -100; + [left] !done & (Hit_Gate) : -100; + [right] !done & (Hit_Gate) : -100; + [noop] !done & (Hit_Gate) : -100; endrewards