Skip to content

Commit

Permalink
Merge pull request #36 from TheGreatfpmK/new-master
Browse files Browse the repository at this point in the history 
All in one MDP approach + final CAV24 models
  • Loading branch information
@TheGreatfpmK
TheGreatfpmK authored Jan 9, 2024
2 parents 9d692eb + cf48ac8 commit 3594d1f
Show file tree
Hide file tree
Showing 53 changed files with 400 additions and 1,481 deletions.
0 models/mdp/sketches/avoid/5-2/sketch.props → models/mdp/cav24/avoid-8-2-easy/sketch.props
View file
File renamed without changes.
10 changes: 5 additions & 5 deletions models/mdp/sketches/avoid/5-2/sketch.templ → models/mdp/cav24/avoid-8-2-easy/sketch.templ
View file
Original file line number Diff line number Diff line change
@@ -1,17 +1,17 @@
mdp

const int N=5;
const int N=8;
const int xMIN = 1;
const int yMIN = 1;
const int xMAX = N;
const int yMAX = N;

hole int o1y in {1..5};
hole int o1x_init in {1..5};
hole int o1y in {1..8};
hole int o1x_init in {5..8};
hole int goright1_init in {0,1};

hole int o2y in {1..5};
hole int o2x_init in {1..5};
hole int o2y in {2..8};
hole int o2x_init in {1..4};
hole int goright2_init in {0,1};

const NUM_OBS = 2;
Expand Down
0 models/mdp/sketches/avoid/6-2/sketch.props → models/mdp/cav24/avoid-8-2/sketch.props
View file
File renamed without changes.
10 changes: 5 additions & 5 deletions models/mdp/sketches/avoid/6-2/sketch.templ → models/mdp/cav24/avoid-8-2/sketch.templ
View file
Original file line number Diff line number Diff line change
@@ -1,17 +1,17 @@
mdp

const int N=6;
const int N=8;
const int xMIN = 1;
const int yMIN = 1;
const int xMAX = N;
const int yMAX = N;

hole int o1y in {1..6};
hole int o1x_init in {1..6};
hole int o1y in {1..8};
hole int o1x_init in {5..8};
hole int goright1_init in {0,1};

hole int o2y in {1..6};
hole int o2x_init in {1..6};
hole int o2y in {1..8};
hole int o2x_init in {1..4};
hole int goright2_init in {0,1};

const NUM_OBS = 2;
Expand Down
0 ...ketches/dodge/8-mod2-pull-30/sketch.props → ...p/cav24/dodge-8-mod2-pull-30/sketch.props
View file
File renamed without changes.
0 ...ketches/dodge/8-mod2-pull-30/sketch.templ → ...p/cav24/dodge-8-mod2-pull-30/sketch.templ
View file
File renamed without changes.
0 ...ketches/dodge/8-mod3-pull-30/sketch.props → ...p/cav24/dodge-8-mod3-pull-30/sketch.props
View file
File renamed without changes.
0 ...ketches/dodge/8-mod3-pull-30/sketch.templ → ...p/cav24/dodge-8-mod3-pull-30/sketch.templ
View file
File renamed without changes.
0 ...tches/dpm/switch-big-q10-old/sketch.props → ...mdp/cav24/dpm-switch-big-q10/sketch.props
View file
File renamed without changes.
38 changes: 19 additions & 19 deletions ...tches/dpm/switch-big-q10-old/sketch.templ → ...mdp/cav24/dpm-switch-big-q10/sketch.templ
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,13 +25,13 @@ hole int P4 in {0,1,2};
hole int QMAX in {10};

// observation level thresholds
hole double T1 in {0.0,0.1,0.2,0.3,0.4};
hole double T2 in {0.5};
hole double T3 in {0.6,0.7,0.8,0.9};
hole int T1 in {0..4};
hole int T2 in {5};
hole int T3 in {6..9};

// switching probabilities
hole double WP1 in {0.9,0.8,0.7};
hole double WP2 in {0.7,0.6,0.5};
hole int WP1 in {50..90:5};
hole int WP2 in {50..90:5};

// ----- modules ---------------------------------------------------------------

Expand Down Expand Up @@ -71,8 +71,8 @@ module SP
[tick1] sp <= 2 & pm > sp -> (sp'=sp+3);
// waiting states
[tick1] sp = 3 -> WP1 : (sp'=sp-2) + 1-WP1 : true;
[tick1] sp = 4 -> WP2 : (sp'=sp-2) + 1-WP2 : true;
[tick1] sp = 3 -> WP1*0.01 : (sp'=sp-2) + 1-WP1*0.01 : true;
[tick1] sp = 4 -> WP2*0.01 : (sp'=sp-2) + 1-WP2*0.01 : true;
endmodule
Expand All @@ -86,21 +86,21 @@ module SR
[tick01] bat=1 -> 1: (sr'=0);
[tick02] bat=1 -> 1: (sr'=0);

[tick1] q <= T1*QMAX & P1 = 0 -> 0.9: true + 0.1: (sr'=1);
[tick1] q <= T1*QMAX & P1 = 1 -> 0.7: true + 0.3: (sr'=1);
[tick1] q <= T1*QMAX & P1 = 2 -> 0.5: true + 0.5: (sr'=1);
[tick1] q <= T1*0.1*QMAX & P1 = 0 -> 0.9: true + 0.1: (sr'=1);
[tick1] q <= T1*0.1*QMAX & P1 = 1 -> 0.7: true + 0.3: (sr'=1);
[tick1] q <= T1*0.1*QMAX & P1 = 2 -> 0.5: true + 0.5: (sr'=1);
[tick1] q > T1*QMAX & q <= T2*QMAX & P2 = 0 -> 0.8: true + 0.2: (sr'=1);
[tick1] q > T1*QMAX & q <= T2*QMAX & P2 = 1 -> 0.6: true + 0.4: (sr'=1);
[tick1] q > T1*QMAX & q <= T2*QMAX & P2 = 2 -> 0.4: true + 0.6: (sr'=1);
[tick1] q > T1*0.1*QMAX & q <= T2*0.1*QMAX & P2 = 0 -> 0.8: true + 0.2: (sr'=1);
[tick1] q > T1*0.1*QMAX & q <= T2*0.1*QMAX & P2 = 1 -> 0.6: true + 0.4: (sr'=1);
[tick1] q > T1*0.1*QMAX & q <= T2*0.1*QMAX & P2 = 2 -> 0.4: true + 0.6: (sr'=1);

[tick1] q > T2*QMAX & q <= T3*QMAX & P3 = 0 -> 0.7: true + 0.3: (sr'=1);
[tick1] q > T2*QMAX & q <= T3*QMAX & P3 = 1 -> 0.4: true + 0.6: (sr'=1);
[tick1] q > T2*QMAX & q <= T3*QMAX & P3 = 2 -> 0.2: true + 0.8: (sr'=1);
[tick1] q > T2*0.1*QMAX & q <= T3*0.1*QMAX & P3 = 0 -> 0.7: true + 0.3: (sr'=1);
[tick1] q > T2*0.1*QMAX & q <= T3*0.1*QMAX & P3 = 1 -> 0.4: true + 0.6: (sr'=1);
[tick1] q > T2*0.1*QMAX & q <= T3*0.1*QMAX & P3 = 2 -> 0.2: true + 0.8: (sr'=1);
[tick1] q > T3*QMAX & P4 = 0 -> 0.5: true + 0.5: (sr'=1);
[tick1] q > T3*QMAX & P4 = 1 -> 0.3: true + 0.7: (sr'=1);
[tick1] q > T3*QMAX & P4 = 2 -> 0.1: true + 0.9: (sr'=1);
[tick1] q > T3*0.1*QMAX & P4 = 0 -> 0.5: true + 0.5: (sr'=1);
[tick1] q > T3*0.1*QMAX & P4 = 1 -> 0.3: true + 0.7: (sr'=1);
[tick1] q > T3*0.1*QMAX & P4 = 2 -> 0.1: true + 0.9: (sr'=1);

endmodule

Expand Down
0 .../sketches/dpm/switch-q10-old/sketch.props → models/mdp/cav24/dpm-switch-q10/sketch.props
View file
File renamed without changes.
38 changes: 19 additions & 19 deletions .../sketches/dpm/switch-q10-old/sketch.templ → models/mdp/cav24/dpm-switch-q10/sketch.templ
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,13 +25,13 @@ hole int P4 in {0,1,2};
hole int QMAX in {10};

// observation level thresholds
hole double T1 in {0.0,0.1,0.2,0.3,0.4};
hole double T2 in {0.5};
hole double T3 in {0.6,0.7,0.8,0.9};
hole int T1 in {0..4};
hole int T2 in {5};
hole int T3 in {6..9};

// switching probabilities
hole double WP1 in {0.9,0.8,0.7};
hole double WP2 in {0.7,0.6,0.5};
hole int WP1 in {7..9:1};
hole int WP2 in {5..7:1};

// ----- modules ---------------------------------------------------------------

Expand Down Expand Up @@ -71,8 +71,8 @@ module SP
[tick1] sp <= 2 & pm > sp -> (sp'=sp+3);
// waiting states
[tick1] sp = 3 -> WP1 : (sp'=sp-2) + 1-WP1 : true;
[tick1] sp = 4 -> WP2 : (sp'=sp-2) + 1-WP2 : true;
[tick1] sp = 3 -> WP1*0.1 : (sp'=sp-2) + 1-WP1*0.1 : true;
[tick1] sp = 4 -> WP2*0.1 : (sp'=sp-2) + 1-WP2*0.1 : true;
endmodule
Expand All @@ -86,21 +86,21 @@ module SR
[tick01] bat=1 -> 1: (sr'=0);
[tick02] bat=1 -> 1: (sr'=0);

[tick1] q <= T1*QMAX & P1 = 0 -> 0.9: true + 0.1: (sr'=1);
[tick1] q <= T1*QMAX & P1 = 1 -> 0.7: true + 0.3: (sr'=1);
[tick1] q <= T1*QMAX & P1 = 2 -> 0.5: true + 0.5: (sr'=1);
[tick1] q <= T1*0.1*QMAX & P1 = 0 -> 0.9: true + 0.1: (sr'=1);
[tick1] q <= T1*0.1*QMAX & P1 = 1 -> 0.7: true + 0.3: (sr'=1);
[tick1] q <= T1*0.1*QMAX & P1 = 2 -> 0.5: true + 0.5: (sr'=1);
[tick1] q > T1*QMAX & q <= T2*QMAX & P2 = 0 -> 0.8: true + 0.2: (sr'=1);
[tick1] q > T1*QMAX & q <= T2*QMAX & P2 = 1 -> 0.6: true + 0.4: (sr'=1);
[tick1] q > T1*QMAX & q <= T2*QMAX & P2 = 2 -> 0.4: true + 0.6: (sr'=1);
[tick1] q > T1*0.1*QMAX & q <= T2*0.1*QMAX & P2 = 0 -> 0.8: true + 0.2: (sr'=1);
[tick1] q > T1*0.1*QMAX & q <= T2*0.1*QMAX & P2 = 1 -> 0.6: true + 0.4: (sr'=1);
[tick1] q > T1*0.1*QMAX & q <= T2*0.1*QMAX & P2 = 2 -> 0.4: true + 0.6: (sr'=1);

[tick1] q > T2*QMAX & q <= T3*QMAX & P3 = 0 -> 0.7: true + 0.3: (sr'=1);
[tick1] q > T2*QMAX & q <= T3*QMAX & P3 = 1 -> 0.4: true + 0.6: (sr'=1);
[tick1] q > T2*QMAX & q <= T3*QMAX & P3 = 2 -> 0.2: true + 0.8: (sr'=1);
[tick1] q > T2*0.1*QMAX & q <= T3*0.1*QMAX & P3 = 0 -> 0.7: true + 0.3: (sr'=1);
[tick1] q > T2*0.1*QMAX & q <= T3*0.1*QMAX & P3 = 1 -> 0.4: true + 0.6: (sr'=1);
[tick1] q > T2*0.1*QMAX & q <= T3*0.1*QMAX & P3 = 2 -> 0.2: true + 0.8: (sr'=1);
[tick1] q > T3*QMAX & P4 = 0 -> 0.5: true + 0.5: (sr'=1);
[tick1] q > T3*QMAX & P4 = 1 -> 0.3: true + 0.7: (sr'=1);
[tick1] q > T3*QMAX & P4 = 2 -> 0.1: true + 0.9: (sr'=1);
[tick1] q > T3*0.1*QMAX & P4 = 0 -> 0.5: true + 0.5: (sr'=1);
[tick1] q > T3*0.1*QMAX & P4 = 1 -> 0.3: true + 0.7: (sr'=1);
[tick1] q > T3*0.1*QMAX & P4 = 2 -> 0.1: true + 0.9: (sr'=1);

endmodule

Expand Down
1 change: 1 addition & 0 deletions models/mdp/cav24/obstacles-10-6-skip-easy/sketch.props
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
P>0.9 [F goal]
49 changes: 14 additions & 35 deletions ...sketches/obstacles/10-9-skip/sketch.templ → ...v24/obstacles-10-6-skip-easy/sketch.templ
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,55 +6,40 @@ const int yMIN = 1;
const int xMAX = N;
const int yMAX = N;

hole int o1x in {1..3};
hole int o1y in {1..3};
hole int o1x in {1..2};
hole int o1y in {1..2};

hole int o2x in {1..3};
hole int o2y in {4..6};
hole int o2x in {1..2};
hole int o2y in {3..10};

hole int o3x in {1..3};
hole int o3y in {7..9};
hole int o3x in {3..5};
hole int o3y in {2..3};

hole int o4x in {4..6};
hole int o4y in {1..3};
hole int o4x in {3..5};
hole int o4y in {3..10};

hole int o5x in {4..6};
hole int o5y in {4..6};
hole int o5x in {5..7};
hole int o5y in {3..5};

hole int o6x in {4..6};
hole int o6y in {7..9};

hole int o7x in {7..9};
hole int o7y in {1..3};

hole int o8x in {7..9};
hole int o8y in {4..6};

hole int o9x in {7..9};
hole int o9y in {7..9};
hole int o6x in {5..9};
hole int o6y in {5..10};

formula at1 = (x = o1x & y = o1y);
formula at2 = (x = o2x & y = o2y);
formula at3 = (x = o3x & y = o3y);
formula at4 = (x = o4x & y = o4y);
formula at5 = (x = o5x & y = o5y);
formula at6 = (x = o6x & y = o6y);
formula at7 = (x = o7x & y = o7y);
formula at8 = (x = o8x & y = o8y);
formula at9 = (x = o9x & y = o9y);

formula near1 = o1x_MIN<=x & x<=o1x_MAX & o1y_MIN<=y & y<=o1y_MAX;
formula near2 = o2x_MIN<=x & x<=o2x_MAX & o2y_MIN<=y & y<=o2y_MAX;
formula near3 = o3x_MIN<=x & x<=o3x_MAX & o3y_MIN<=y & y<=o3y_MAX;
formula near4 = o4x_MIN<=x & x<=o4x_MAX & o4y_MIN<=y & y<=o4y_MAX;
formula near5 = o5x_MIN<=x & x<=o5x_MAX & o5y_MIN<=y & y<=o5y_MAX;
formula near6 = o6x_MIN<=x & x<=o6x_MAX & o6y_MIN<=y & y<=o6y_MAX;
formula near7 = o7x_MIN<=x & x<=o7x_MAX & o7y_MIN<=y & y<=o7y_MAX;
formula near8 = o8x_MIN<=x & x<=o8x_MAX & o8y_MIN<=y & y<=o8y_MAX;
formula near9 = o9x_MIN<=x & x<=o9x_MAX & o9y_MIN<=y & y<=o9y_MAX;

const NUM_OBS = 9;
formula crash = visit1 | visit2 | visit3 | visit4 | visit5 | visit6 | visit7 | visit8 | visit9;
const NUM_OBS = 6;
formula crash = visit1 | visit2 | visit3 | visit4 | visit5 | visit6;
formula goal = (x=xMAX & y=yMAX);
formula done = goal | crash;

Expand All @@ -74,9 +59,6 @@ module clk
[detect4] !done & clk=4 -> (clk'=clk_next);
[detect5] !done & clk=5 -> (clk'=clk_next);
[detect6] !done & clk=6 -> (clk'=clk_next);
[detect7] !done & clk=7 -> (clk'=clk_next);
[detect8] !done & clk=8 -> (clk'=clk_next);
[detect9] !done & clk=9 -> (clk'=clk_next);
endmodule


Expand Down Expand Up @@ -108,6 +90,3 @@ module visit3=visit1[visit1=visit3,detect1=detect3,near1=near3,at1=at3] endmodul
module visit4=visit1[visit1=visit4,detect1=detect4,near1=near4,at1=at4] endmodule
module visit5=visit1[visit1=visit5,detect1=detect5,near1=near5,at1=at5] endmodule
module visit6=visit1[visit1=visit6,detect1=detect6,near1=near6,at1=at6] endmodule
module visit7=visit1[visit1=visit7,detect1=detect7,near1=near7,at1=at7] endmodule
module visit8=visit1[visit1=visit8,detect1=detect8,near1=near8,at1=at8] endmodule
module visit9=visit1[visit1=visit9,detect1=detect9,near1=near9,at1=at9] endmodule
0 ...sketches/obstacles/10-9-pull/sketch.props → ...dp/cav24/obstacles-10-9-pull/sketch.props
View file
File renamed without changes.
0 ...sketches/obstacles/10-9-pull/sketch.templ → ...dp/cav24/obstacles-10-9-pull/sketch.templ
View file
File renamed without changes.
1 change: 1 addition & 0 deletions models/mdp/cav24/obstacles-8-6-skip/sketch.props
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
P>0.9 [F goal]
44 changes: 29 additions & 15 deletions ...s/obstacles/6-4-pull-overlap/sketch.templ → ...mdp/cav24/obstacles-8-6-skip/sketch.templ
View file
Original file line number Diff line number Diff line change
@@ -1,35 +1,45 @@
mdp

const int N = 6;
const int N = 8;
const int xMIN = 1;
const int yMIN = 1;
const int xMAX = N;
const int yMAX = N;

hole int o1x in {1..4};
hole int o1y in {1..4};
hole int o1x in {1..2};
hole int o1y in {1..2};

hole int o2x in {1..4};
hole int o2y in {1..4};
hole int o2x in {1..2};
hole int o2y in {3..5};

hole int o3x in {1..4};
hole int o3y in {4..6};
hole int o3x in {3..5};
hole int o3y in {1..2};

hole int o4x in {4..6};
hole int o4y in {1..4};
hole int o4x in {3..5};
hole int o4y in {6..8};

hole int o5x in {6..8};
hole int o5y in {3..5};

hole int o6x in {6..7};
hole int o6y in {6..7};

formula at1 = (x = o1x & y = o1y);
formula at2 = (x = o2x & y = o2y);
formula at3 = (x = o3x & y = o3y);
formula at4 = (x = o4x & y = o4y);
formula at5 = (x = o5x & y = o5y);
formula at6 = (x = o6x & y = o6y);

formula near1 = o1x_MIN<=x & x<=o1x_MAX & o1y_MIN<=y & y<=o1y_MAX;
formula near2 = o2x_MIN<=x & x<=o2x_MAX & o2y_MIN<=y & y<=o2y_MAX;
formula near3 = o3x_MIN<=x & x<=o3x_MAX & o3y_MIN<=y & y<=o3y_MAX;
formula near4 = o4x_MIN<=x & x<=o4x_MAX & o4y_MIN<=y & y<=o4y_MAX;
formula near5 = o5x_MIN<=x & x<=o5x_MAX & o5y_MIN<=y & y<=o5y_MAX;
formula near6 = o6x_MIN<=x & x<=o6x_MAX & o6y_MIN<=y & y<=o6y_MAX;

const NUM_OBS = 4;
formula crash = visit1 | visit2 | visit3 | visit4;
const NUM_OBS = 6;
formula crash = visit1 | visit2 | visit3 | visit4 | visit5 | visit6;
formula goal = (x=xMAX & y=yMAX);
formula done = goal | crash;

Expand All @@ -47,6 +57,8 @@ module clk
[detect2] !done & clk=2 -> (clk'=clk_next);
[detect3] !done & clk=3 -> (clk'=clk_next);
[detect4] !done & clk=4 -> (clk'=clk_next);
[detect5] !done & clk=5 -> (clk'=clk_next);
[detect6] !done & clk=6 -> (clk'=clk_next);
endmodule


Expand All @@ -61,10 +73,10 @@ module agent
x : [xMIN..xMAX] init xMIN;
y : [yMIN..yMAX] init yMIN;

[left] true -> 1-slip : (x'=xleft) + slip : (y'=ydown);
[right] true -> 1-slip : (x'=xright) + slip : (y'=yup);
[down] true -> 1-slip : (y'=ydown) + slip : (x'=xright);
[up] true -> 1-slip : (y'=yup) + slip : (x'=xleft);
[left] true -> 1-slip : (x'=xleft) + slip : (x'=max(x-2,xMIN));
[right] true -> 1-slip : (x'=xright) + slip : (x'=min(x+2,xMAX));
[down] true -> 1-slip : (y'=ydown) + slip : (y'=max(y-2,yMIN));
[up] true -> 1-slip : (y'=yup) + slip : (y'=min(y+2,yMAX));
endmodule

module visit1
Expand All @@ -76,3 +88,5 @@ endmodule
module visit2=visit1[visit1=visit2,detect1=detect2,near1=near2,at1=at2] endmodule
module visit3=visit1[visit1=visit3,detect1=detect3,near1=near3,at1=at3] endmodule
module visit4=visit1[visit1=visit4,detect1=detect4,near1=near4,at1=at4] endmodule
module visit5=visit1[visit1=visit5,detect1=detect5,near1=near5,at1=at5] endmodule
module visit6=visit1[visit1=visit6,detect1=detect6,near1=near6,at1=at6] endmodule
0 models/mdp/sketches/rocks/6-3/sketch.props → models/mdp/cav24/rocks-6-4/sketch.props
View file
File renamed without changes.
0 models/mdp/sketches/rocks/6-4/sketch.templ → models/mdp/cav24/rocks-6-4/sketch.templ
View file
File renamed without changes.
0 ...s/mdp/sketches/rover/100-big/sketch.props → models/mdp/cav24/rover-100-big/sketch.props
View file
File renamed without changes.
Loading

0 comments on commit 3594d1f

Please sign in to comment.