sp
/
Skiing
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

mdp update

add_velocity_into_framework
sp 6 months ago
parent
6fce864656
commit
3d05a4aeda
1 changed files with 118 additions and 14 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 132
      velocity_safety_no_formulas.prism

132
velocity_safety_no_formulas.prism
View File

@ -4,18 +4,25 @@ const int initY = 40;
const int initX = 80; const int initX = 80;
//const int maxY = 580; //const int maxY = 580;
const int maxY = 300;
//const int maxY = 430;
const int maxY = 200;
const int minX = 10; const int minX = 10;
const int maxX = 152; const int maxX = 152;
const int maxVel = 8; const int maxVel = 8;
formula Gate_1 = (((42<x & x<50) | (74<x & x<82)) & 164<y & y<172);
formula Gate_1 = (((42<x & x<50) | (74<x & x<82)) & 164<y & y<172);
formula Gate_2 = (((72<x & x<80) | (104<x & x<112)) & 256<y & y<264); formula Gate_2 = (((72<x & x<80) | (104<x & x<112)) & 256<y & y<264);
formula Gate_3 = (((80<x & x<88) | (112<x & x<120)) & 349<y & y<357); formula Gate_3 = (((80<x & x<88) | (112<x & x<120)) & 349<y & y<357);
formula Gate_4 = (((54<x & x<62) | (88<x & x<96)) & 442<y & y<450);
formula Gate_4 = (((54<x & x<62) | (88<x & x<96)) & 442<y & y<450);
formula Gate_5 = (((80<x & x<88) | (112<x & x<120)) & 530<y & y<538); formula Gate_5 = (((80<x & x<88) | (112<x & x<120)) & 530<y & y<538);
formula S_Gate_1 = (((32<x & x<60) | (64<x & x<92)) & 124<y & y<172);
formula S_Gate_2 = (((62<x & x<90) | (94<x & x<132)) & 216<y & y<264);
formula S_Gate_3 = (((70<x & x<98) | (102<x & x<130)) & 309<y & y<357);
formula S_Gate_4 = (((44<x & x<72) | (78<x & x<106)) & 402<y & y<450);
formula S_Gate_5 = (((70<x & x<98) | (102<x & x<130)) & 490<y & y<538);
formula Tree_1 = ((x>=124 & x<=142) & (y>=190 & y<=200)); formula Tree_1 = ((x>=124 & x<=142) & (y>=190 & y<=200));
formula Tree_2 = ((x>=32 & x<=49) & (y>=284 & y<=295)); formula Tree_2 = ((x>=32 & x<=49) & (y>=284 & y<=295));
@ -24,26 +31,114 @@ formula Tree_4 = ((x>=12 & x<=30) & (y>=408 & y<=418));
formula Tree_5 = ((x>=129 & x<=146) & (y>=468 & y<=480)); formula Tree_5 = ((x>=129 & x<=146) & (y>=468 & y<=480));
formula Tree_6 = ((x>=140 & x<=152) & (y>=496 & y<=510)); formula Tree_6 = ((x>=140 & x<=152) & (y>=496 & y<=510));
formula S_Tree_1 = ((x>=114 & x<=152) & (y>=150 & y<=200));
formula S_Tree_2 = ((x>=22 & x<=59) & (y>=244 & y<=295));
formula S_Tree_3 = ((x>=20 & x<=59) & (y>=277 & y<=327));
formula S_Tree_4 = ((x>=2 & x<=40) & (y>=368 & y<=418));
formula S_Tree_5 = ((x>=119 & x<=156) & (y>=438 & y<=480));
formula S_Tree_6 = ((x>=130 & x<=162) & (y>=456 & y<=510));
formula Hit_Tree = Tree_1 | Tree_2 | Tree_3 | Tree_4 | Tree_5 | Tree_6; 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 Hit_Gate = Gate_1 | Gate_2 | Gate_3 | Gate_4 | Gate_5;
formula S_Hit_Tree = S_Tree_1 | S_Tree_2 | S_Tree_3 | S_Tree_4 | S_Tree_5 | S_Tree_6;
formula S_Hit_Gate = S_Gate_1 | S_Gate_2 | S_Gate_3 | S_Gate_4 | S_Gate_5;
label "Hit_Tree" = Hit_Tree; label "Hit_Tree" = Hit_Tree;
label "Hit_Gate" = Hit_Gate; label "Hit_Gate" = Hit_Gate;
label "S_Hit_Tree" = S_Hit_Tree;
label "S_Hit_Gate" = S_Hit_Gate;
global move : [0..3]; global move : [0..3];
module skier
ski_position : [1..8] init 4;
done : bool init false;
[left] !done & !Safe & !Unsafe & !Hit_Gate & !Hit_Tree & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1);
[right] !done & !Safe & !Unsafe & !Hit_Gate & !Hit_Tree & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1);
[noop] !done & !Safe & !Unsafe & !Hit_Gate & !Hit_Tree & move=0 -> (move'=1);
module skier
ski_position : [1..8] init 4;
reward_given: bool init false;
//done: bool init false;
[left] !reward_given & !Safe_1 & !Unsafe_1 & !Hit_Gate & !Hit_Tree & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1);
[right] !reward_given & !Safe_1 & !Unsafe_1 & !Hit_Gate & !Hit_Tree & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1);
[noop] !reward_given & !Safe_1 & !Unsafe_1 & !Hit_Gate & !Hit_Tree & move=0 -> (move'=1);
//[left] !reward_given & (Safe_1 | Unsafe_1 | Hit_Tree | Hit_Gate) & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (reward_given'=true);
//[right] !reward_given & (Safe_1 | Unsafe_1 | Hit_Tree | Hit_Gate) & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1) & (reward_given'=true);
//[noop] !reward_given & (Safe_1 | Unsafe_1 | Hit_Tree | Hit_Gate) & move=0 -> (move'=1) & (reward_given'=true);
[left] !reward_given & !Safe_2 & !Unsafe_2 & !Hit_Gate & !Hit_Tree & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1);
[right] !reward_given & !Safe_2 & !Unsafe_2 & !Hit_Gate & !Hit_Tree & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1);
[noop] !reward_given & !Safe_2 & !Unsafe_2 & !Hit_Gate & !Hit_Tree & move=0 -> (move'=1);
//[left] !reward_given & (Safe_2 | Unsafe_2 | Hit_Tree | Hit_Gate) & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (reward_given'=true);
//[right] !reward_given & (Safe_2 | Unsafe_2 | Hit_Tree | Hit_Gate) & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1) & (reward_given'=true);
//[noop] !reward_given & (Safe_2 | Unsafe_2 | Hit_Tree | Hit_Gate) & move=0 -> (move'=1) & (reward_given'=true);
[left] !reward_given & !Safe_3 & !Unsafe_3 & !Hit_Gate & !Hit_Tree & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1);
[right] !reward_given & !Safe_3 & !Unsafe_3 & !Hit_Gate & !Hit_Tree & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1);
[noop] !reward_given & !Safe_3 & !Unsafe_3 & !Hit_Gate & !Hit_Tree & move=0 -> (move'=1);
//[left] !reward_given & (Safe_3 | Unsafe_3 | Hit_Tree | Hit_Gate) & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (reward_given'=true);
//[right] !reward_given & (Safe_3 | Unsafe_3 | Hit_Tree | Hit_Gate) & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1) & (reward_given'=true);
//[noop] !reward_given & (Safe_3 | Unsafe_3 | Hit_Tree | Hit_Gate) & move=0 -> (move'=1) & (reward_given'=true);
[left] !reward_given & !Safe_4 & !Unsafe_4 & !Hit_Gate & !Hit_Tree & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1);
[right] !reward_given & !Safe_4 & !Unsafe_4 & !Hit_Gate & !Hit_Tree & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1);
[noop] !reward_given & !Safe_4 & !Unsafe_4 & !Hit_Gate & !Hit_Tree & move=0 -> (move'=1);
//[left] !reward_given & (Safe_4 | Unsafe_4 | Hit_Tree | Hit_Gate) & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (reward_given'=true);
//[right] !reward_given & (Safe_4 | Unsafe_4 | Hit_Tree | Hit_Gate) & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1) & (reward_given'=true);
//[noop] !reward_given & (Safe_4 | Unsafe_4 | Hit_Tree | Hit_Gate) & move=0 -> (move'=1) & (reward_given'=true);
[left] !reward_given & !Safe_5 & !Unsafe_5 & !Hit_Gate & !Hit_Tree & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1);
[right] !reward_given & !Safe_5 & !Unsafe_5 & !Hit_Gate & !Hit_Tree & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1);
[noop] !reward_given & !Safe_5 & !Unsafe_5 & !Hit_Gate & !Hit_Tree & move=0 -> (move'=1);
//[left] !reward_given & (Safe_5 | Unsafe_5 | Hit_Tree | Hit_Gate) & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (reward_given'=true);
//[right] !reward_given & (Safe_5 | Unsafe_5 | Hit_Tree | Hit_Gate) & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1) & (reward_given'=true);
//[noop] !reward_given & (Safe_5 | Unsafe_5 | Hit_Tree | Hit_Gate) & move=0 -> (move'=1) & (reward_given'=true);
[left] !reward_given & !Safe_6 & !Unsafe_6 & !Hit_Gate & !Hit_Tree & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1);
[right] !reward_given & !Safe_6 & !Unsafe_6 & !Hit_Gate & !Hit_Tree & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1);
[noop] !reward_given & !Safe_6 & !Unsafe_6 & !Hit_Gate & !Hit_Tree & move=0 -> (move'=1);
//[left] !reward_given & (Safe_6 | Unsafe_6 | Hit_Tree | Hit_Gate) & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (reward_given'=true);
//[right] !reward_given & (Safe_6 | Unsafe_6 | Hit_Tree | Hit_Gate) & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1) & (reward_given'=true);
//[noop] !reward_given & (Safe_6 | Unsafe_6 | Hit_Tree | Hit_Gate) & move=0 -> (move'=1) & (reward_given'=true);
[left] !reward_given & !Safe_7 & !Unsafe_7 & !Hit_Gate & !Hit_Tree & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1);
[right] !reward_given & !Safe_7 & !Unsafe_7 & !Hit_Gate & !Hit_Tree & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1);
[noop] !reward_given & !Safe_7 & !Unsafe_7 & !Hit_Gate & !Hit_Tree & move=0 -> (move'=1);
//[left] !reward_given & (Safe_7 | Unsafe_7 | Hit_Tree | Hit_Gate) & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (reward_given'=true);
//[right] !reward_given & (Safe_7 | Unsafe_7 | Hit_Tree | Hit_Gate) & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1) & (reward_given'=true);
//[noop] !reward_given & (Safe_7 | Unsafe_7 | Hit_Tree | Hit_Gate) & move=0 -> (move'=1) & (reward_given'=true);
[left] !reward_given & !Safe_8 & !Unsafe_8 & !Hit_Gate & !Hit_Tree & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1);
[right] !reward_given & !Safe_8 & !Unsafe_8 & !Hit_Gate & !Hit_Tree & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1);
[noop] !reward_given & !Safe_8 & !Unsafe_8 & !Hit_Gate & !Hit_Tree & move=0 -> (move'=1);
//[left] !reward_given & (Safe_8 | Unsafe_8 | Hit_Tree | Hit_Gate) & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (reward_given'=true);
//[right] !reward_given & (Safe_8 | Unsafe_8 | Hit_Tree | Hit_Gate) & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1) & (reward_given'=true);
//[noop] !reward_given & (Safe_8 | Unsafe_8 | Hit_Tree | Hit_Gate) & move=0 -> (move'=1) & (reward_given'=true);
//[left] reward_given & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=true);
//[right] reward_given & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1) & (done'=true);
//[noop] reward_given & move=0 -> (move'=1) & (done'=true);
[done] !reward_given & (Hit_Tree | Hit_Gate) & move=0 -> (reward_given'=true);
[done] !reward_given & Unsafe_1 & move=0 -> (reward_given'=true);
[done] !reward_given & Unsafe_2 & move=0 -> (reward_given'=true);
[done] !reward_given & Unsafe_3 & move=0 -> (reward_given'=true);
[done] !reward_given & Unsafe_4 & move=0 -> (reward_given'=true);
[done] !reward_given & Unsafe_5 & move=0 -> (reward_given'=true);
[done] !reward_given & Unsafe_6 & move=0 -> (reward_given'=true);
[done] !reward_given & Unsafe_7 & move=0 -> (reward_given'=true);
[done] !reward_given & Unsafe_8 & move=0 -> (reward_given'=true);
[done] !reward_given & Safe_1 & move=0 -> (reward_given'=true);
[done] !reward_given & Safe_2 & move=0 -> (reward_given'=true);
[done] !reward_given & Safe_3 & move=0 -> (reward_given'=true);
[done] !reward_given & Safe_4 & move=0 -> (reward_given'=true);
[done] !reward_given & Safe_5 & move=0 -> (reward_given'=true);
[done] !reward_given & Safe_6 & move=0 -> (reward_given'=true);
[done] !reward_given & Safe_7 & move=0 -> (reward_given'=true);
[done] !reward_given & Safe_8 & move=0 -> (reward_given'=true);
[done] move=0 & (Safe | Unsafe | Hit_Tree | Hit_Gate) -> (done'=true);
endmodule endmodule
module updateY module updateY
@ -77,9 +172,18 @@ module updateX
[update_x] move=3 & standstill<8 & (ski_position=8) -> 0.2: (x'=min(maxX,x+2)) & (move'=0) + 0.8: (x'=min(maxX,x+3)) & (move'=0); [update_x] move=3 & standstill<8 & (ski_position=8) -> 0.2: (x'=min(maxX,x+2)) & (move'=0) + 0.8: (x'=min(maxX,x+3)) & (move'=0);
endmodule endmodule
//rewards
// [left] !done & !reward_given & Hit_Tree : -100;
// [left] !done & !reward_given & Hit_Gate : -100;
// [left] !done & !reward_given & (Unsafe_1 | Unsafe_2 | Unsafe_3 | Unsafe_4 | Unsafe_5 | Unsafe_6 | Unsafe_7 | Unsafe_8) : -100;
// [right] !done & !reward_given & Hit_Tree : -100;
// [right] !done & !reward_given & Hit_Gate : -100;
// [right] !done & !reward_given & (Unsafe_1 | Unsafe_2 | Unsafe_3 | Unsafe_4 | Unsafe_5 | Unsafe_6 | Unsafe_7 | Unsafe_8) : -100;
// [noop] !done & !reward_given & Hit_Tree : -100;
// [noop] !done & !reward_given & Hit_Gate : -100;
// [noop] !done & !reward_given & (Unsafe_1 | Unsafe_2 | Unsafe_3 | Unsafe_4 | Unsafe_5 | Unsafe_6 | Unsafe_7 | Unsafe_8) : -100;
//endrewards
rewards rewards
[done] !done & Hit_Tree : -100;
[done] !done & Hit_Gate : -100;
[done] !done & Unsafe : -100;
[done] !reward_given & (Hit_Gate | Hit_Tree | (Unsafe_1 | Unsafe_2 | Unsafe_3 | Unsafe_4 | Unsafe_5 | Unsafe_6 | Unsafe_7 | Unsafe_8)) : -100;
endrewards endrewards
Write Preview
Loading…
Cancel
Save