From a5d2dc573144c54e70931b28d6cf8b2fc5461791 Mon Sep 17 00:00:00 2001 From: Roman Andriushchenko Date: Thu, 12 Sep 2024 12:01:20 +0200 Subject: [PATCH] add POMDP sketches --- .../sketches/obstacles-10-2/sketch.props | 1 + .../sketches/obstacles-10-2/sketch.templ | 85 ++++++++++++++ .../pomdp/sketches/obstacles-8-3/sketch.props | 1 + .../pomdp/sketches/obstacles-8-3/sketch.templ | 102 ++++++++++++++++ .../pomdp/sketches/obstacles-8-6/sketch.props | 1 + .../pomdp/sketches/obstacles-8-6/sketch.templ | 109 ++++++++++++++++++ .../sketches/obstacles-prob/sketch.props | 1 - .../sketches/obstacles-prob/sketch.templ | 83 ------------- .../obstacles-single-pomdp/sketch.props | 1 - .../obstacles-single-pomdp/sketch.templ | 96 --------------- .../sketches/obstacles-uniform/sketch.props | 1 - .../sketches/obstacles-uniform/sketch.templ | 107 ----------------- models/pomdp/sketches/obstacles/sketch.props | 1 - models/pomdp/sketches/obstacles/sketch.templ | 96 --------------- paynt/parser/jani.py | 47 ++++---- paynt/parser/sketch.py | 43 +++---- .../translation/componentTranslations.cpp | 6 +- 17 files changed, 344 insertions(+), 437 deletions(-) create mode 100755 models/pomdp/sketches/obstacles-10-2/sketch.props create mode 100755 models/pomdp/sketches/obstacles-10-2/sketch.templ create mode 100755 models/pomdp/sketches/obstacles-8-3/sketch.props create mode 100755 models/pomdp/sketches/obstacles-8-3/sketch.templ create mode 100755 models/pomdp/sketches/obstacles-8-6/sketch.props create mode 100755 models/pomdp/sketches/obstacles-8-6/sketch.templ delete mode 100755 models/pomdp/sketches/obstacles-prob/sketch.props delete mode 100755 models/pomdp/sketches/obstacles-prob/sketch.templ delete mode 100755 models/pomdp/sketches/obstacles-single-pomdp/sketch.props delete mode 100755 models/pomdp/sketches/obstacles-single-pomdp/sketch.templ delete mode 100755 models/pomdp/sketches/obstacles-uniform/sketch.props delete mode 100755 models/pomdp/sketches/obstacles-uniform/sketch.templ delete mode 100755 models/pomdp/sketches/obstacles/sketch.props delete mode 100755 models/pomdp/sketches/obstacles/sketch.templ diff --git a/models/pomdp/sketches/obstacles-10-2/sketch.props b/models/pomdp/sketches/obstacles-10-2/sketch.props new file mode 100755 index 000000000..0ed744cee --- /dev/null +++ b/models/pomdp/sketches/obstacles-10-2/sketch.props @@ -0,0 +1 @@ +R{"penalty"}min=? [ F goal ]; diff --git a/models/pomdp/sketches/obstacles-10-2/sketch.templ b/models/pomdp/sketches/obstacles-10-2/sketch.templ new file mode 100755 index 000000000..84f25ab6e --- /dev/null +++ b/models/pomdp/sketches/obstacles-10-2/sketch.templ @@ -0,0 +1,85 @@ +pomdp + +const int N = 10; +const int gMIN = 1; +const int gMAX = N; + +observable "clk" = clk; +observable "goal" = goal; +observable "x_small" = x<(gMAX/2); +observable "y_small" = y<(gMAX/2); + +hole int o1x in {3..5}; +hole int o1y in {3..5}; + +hole int o2x in {6..8}; +hole int o2y in {6..8}; + +formula at1 = (x = o1x & y = o1y); +formula at2 = (x = o2x & y = o2y); + +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 goal = (x=gMAX & y=gMAX); + +const NUM_OBS = 2; +formula clk_next = mod(clk+1,NUM_OBS+1); +module clk + clk : [-1..NUM_OBS] init -1; + + [place] clk=-1 -> (clk'=clk_next); + + [up] !goal & clk=0 -> (clk'=clk_next); + [do] !goal & clk=0 -> (clk'=clk_next); + [le] !goal & clk=0 -> (clk'=clk_next); + [ri] !goal & clk=0 -> (clk'=clk_next); + + [detect1] !goal & clk=1 -> (clk'=clk_next); + [detect2] !goal & clk=2 -> (clk'=clk_next); +endmodule + + +const double slip = 0.1; + +formula yup = min(y+1,gMAX); +formula ydo = max(y-1,gMIN); +formula xle = max(x-1,gMIN); +formula xri = min(x+1,gMAX); + +module agent + x : [gMIN..gMAX] init gMIN; + y : [gMIN..gMAX] init gMIN; + + [place] true -> 1/4: (x'=o1x-1) & (y'=o1y) + 1/4: (x'=1) & (y'=1) + 1/4: (x'=2) & (y'=1) + 1/4: (x'=1) & (y'=3); + + [up] true -> 1-slip : (y'=yup) + slip : (y'=min(y+2,gMAX)); + [do] true -> 1-slip : (y'=ydo) + slip : (y'=max(y-2,gMIN)); + [le] true -> 1-slip : (x'=xle) + slip : (x'=max(x-2,gMIN)); + [ri] true -> 1-slip : (x'=xri) + slip : (x'=min(x+2,gMAX)); +endmodule + +module visit1 + visit1 : bool init false; + [detect1] !near1 -> true; + [detect1] near1 -> (visit1'=at1); + + [up] true -> (visit1'=false); + [do] true -> (visit1'=false); + [le] true -> (visit1'=false); + [ri] true -> (visit1'=false); +endmodule + +module visit2=visit1[visit1=visit2,detect1=detect2,near1=near2,at1=at2] endmodule + +formula step_penalty = 1; +formula crash_penalty = 100; +formula num_crashes = (visit1?1:0)+(visit2?1:0); +formula penalty = step_penalty + num_crashes*crash_penalty; + +rewards "penalty" + [up] true : penalty; + [do] true : penalty; + [le] true : penalty; + [ri] true : penalty; +endrewards diff --git a/models/pomdp/sketches/obstacles-8-3/sketch.props b/models/pomdp/sketches/obstacles-8-3/sketch.props new file mode 100755 index 000000000..0ed744cee --- /dev/null +++ b/models/pomdp/sketches/obstacles-8-3/sketch.props @@ -0,0 +1 @@ +R{"penalty"}min=? [ F goal ]; diff --git a/models/pomdp/sketches/obstacles-8-3/sketch.templ b/models/pomdp/sketches/obstacles-8-3/sketch.templ new file mode 100755 index 000000000..e5d1fb362 --- /dev/null +++ b/models/pomdp/sketches/obstacles-8-3/sketch.templ @@ -0,0 +1,102 @@ +pomdp + +const int N = 8; +const int gMIN = 1; +const int gMAX = N; + +observable "clk" = clk; +observable "goal" = goal; +observable "x_small" = x<(gMAX/2); +observable "y_small" = y<(gMAX/2); + +hole int o1x in {1..2}; +hole int o1y in {1..2}; + +hole int o2x in {1..2}; +hole int o2y in {3..5}; + +hole int o3x in {3..5}; +hole int o3y in {1..2}; + +hole int o4x in {3..5}; +hole int o4y in {6..8}; + +hole int o5x in {6..8}; +hole int o5y in {3..5}; + +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 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 goal = (x=gMAX & y=gMAX); + +const NUM_OBS = 5; +formula clk_next = mod(clk+1,NUM_OBS+1); +module clk + clk : [-1..NUM_OBS] init 0; + + [up] !goal & clk=0 -> (clk'=clk_next); + [do] !goal & clk=0 -> (clk'=clk_next); + [le] !goal & clk=0 -> (clk'=clk_next); + [ri] !goal & clk=0 -> (clk'=clk_next); + + [detect1] !goal & clk=1 -> (clk'=clk_next); + [detect2] !goal & clk=2 -> (clk'=clk_next); + [detect3] !goal & clk=3 -> (clk'=clk_next); + [detect4] !goal & clk=4 -> (clk'=clk_next); + [detect5] !goal & clk=5 -> (clk'=clk_next); +endmodule + + +const double slip = 0.1; + +formula yup = min(y+1,gMAX); +formula ydo = max(y-1,gMIN); +formula xle = max(x-1,gMIN); +formula xri = min(x+1,gMAX); + +module agent + x : [gMIN..gMAX] init gMIN; + y : [gMIN..gMAX] init gMIN; + + [up] true -> 1-slip : (y'=yup) + slip : (y'=min(y+2,gMAX)); + [do] true -> 1-slip : (y'=ydo) + slip : (y'=max(y-2,gMIN)); + [le] true -> 1-slip : (x'=xle) + slip : (x'=max(x-2,gMIN)); + [ri] true -> 1-slip : (x'=xri) + slip : (x'=min(x+2,gMAX)); +endmodule + +module visit1 + visit1 : bool init false; + [detect1] !near1 -> true; + [detect1] near1 -> (visit1'=at1); + + [up] true -> (visit1'=false); + [do] true -> (visit1'=false); + [le] true -> (visit1'=false); + [ri] true -> (visit1'=false); +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 + +formula step_penalty = 1; +formula crash_penalty = 100; +formula num_crashes = (visit1?1:0)+(visit2?1:0)+(visit3?1:0)+(visit4?1:0)+(visit5?1:0); +formula penalty = step_penalty + num_crashes*crash_penalty; + +rewards "penalty" + [up] true : penalty; + [do] true : penalty; + [le] true : penalty; + [ri] true : penalty; +endrewards diff --git a/models/pomdp/sketches/obstacles-8-6/sketch.props b/models/pomdp/sketches/obstacles-8-6/sketch.props new file mode 100755 index 000000000..0ed744cee --- /dev/null +++ b/models/pomdp/sketches/obstacles-8-6/sketch.props @@ -0,0 +1 @@ +R{"penalty"}min=? [ F goal ]; diff --git a/models/pomdp/sketches/obstacles-8-6/sketch.templ b/models/pomdp/sketches/obstacles-8-6/sketch.templ new file mode 100755 index 000000000..3ff6583b4 --- /dev/null +++ b/models/pomdp/sketches/obstacles-8-6/sketch.templ @@ -0,0 +1,109 @@ +pomdp + +const int N = 8; +const int gMIN = 1; +const int gMAX = N; + +observable "clk" = clk; +observable "goal" = goal; +observable "x_small" = x<(gMAX/2); +observable "y_small" = y<(gMAX/2); + +hole int o1x in {1..2}; +hole int o1y in {1..2}; + +hole int o2x in {1..2}; +hole int o2y in {3..5}; + +hole int o3x in {3..5}; +hole int o3y in {1..2}; + +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; + +formula goal = (x=gMAX & y=gMAX); + +const NUM_OBS = 6; +formula clk_next = mod(clk+1,NUM_OBS+1); +module clk + clk : [-1..NUM_OBS] init 0; + + [up] !goal & clk=0 -> (clk'=clk_next); + [do] !goal & clk=0 -> (clk'=clk_next); + [le] !goal & clk=0 -> (clk'=clk_next); + [ri] !goal & clk=0 -> (clk'=clk_next); + + [detect1] !goal & clk=1 -> (clk'=clk_next); + [detect2] !goal & clk=2 -> (clk'=clk_next); + [detect3] !goal & clk=3 -> (clk'=clk_next); + [detect4] !goal & clk=4 -> (clk'=clk_next); + [detect5] !goal & clk=5 -> (clk'=clk_next); + [detect6] !goal & clk=6 -> (clk'=clk_next); +endmodule + + +const double slip = 0.1; + +formula yup = min(y+1,gMAX); +formula ydo = max(y-1,gMIN); +formula xle = max(x-1,gMIN); +formula xri = min(x+1,gMAX); + +module agent + x : [gMIN..gMAX] init gMIN; + y : [gMIN..gMAX] init gMIN; + + [up] true -> 1-slip : (y'=yup) + slip : (y'=min(y+2,gMAX)); + [do] true -> 1-slip : (y'=ydo) + slip : (y'=max(y-2,gMIN)); + [le] true -> 1-slip : (x'=xle) + slip : (x'=max(x-2,gMIN)); + [ri] true -> 1-slip : (x'=xri) + slip : (x'=min(x+2,gMAX)); +endmodule + +module visit1 + visit1 : bool init false; + [detect1] !near1 -> true; + [detect1] near1 -> (visit1'=at1); + + [up] true -> (visit1'=false); + [do] true -> (visit1'=false); + [le] true -> (visit1'=false); + [ri] true -> (visit1'=false); +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 + +formula step_penalty = 1; +formula crash_penalty = 100; +formula num_crashes = (visit1?1:0)+(visit2?1:0)+(visit3?1:0)+(visit4?1:0)+(visit5?1:0)+(visit6?1:0); +formula penalty = step_penalty + num_crashes*crash_penalty; + +rewards "penalty" + [up] true : penalty; + [do] true : penalty; + [le] true : penalty; + [ri] true : penalty; +endrewards diff --git a/models/pomdp/sketches/obstacles-prob/sketch.props b/models/pomdp/sketches/obstacles-prob/sketch.props deleted file mode 100755 index 48a404765..000000000 --- a/models/pomdp/sketches/obstacles-prob/sketch.props +++ /dev/null @@ -1 +0,0 @@ -Pmax=? [ F goal ]; \ No newline at end of file diff --git a/models/pomdp/sketches/obstacles-prob/sketch.templ b/models/pomdp/sketches/obstacles-prob/sketch.templ deleted file mode 100755 index b6fe9694a..000000000 --- a/models/pomdp/sketches/obstacles-prob/sketch.templ +++ /dev/null @@ -1,83 +0,0 @@ -pomdp - -// grid dimensions -const int N = 10; -const int xMIN = 0; -const int yMIN = 0; -const int xMAX = N-1; -const int yMAX = N-1; - -// obstacle coordinates -hole int o1x in {3,4,5}; -hole int o1y in {3,4,5}; - -hole int o2x in {6,7,8}; -hole int o2y in {6,7,8}; - -formula near1 = 3<=x & x<=5 & 3<=y & y<=5; -formula near2 = 6<=x & x<=8 & 6<=y & y<=8; -//formula near3 = 1<=x & x<=3 & 3<=y & y<=4; -//formula near4 = 3<=x & x<=4 & 1<=y & y<=3; - -formula at1 = (x = o1x & y = o1y); -formula at2 = (x = o2x & y = o2y); -//formula at3 = (x = o3x & y = o3y); -//formula at4 = (x = o4x & y = o4y); - -const NUM_OBS = 2; -formula crash = crash1 | crash2; -formula goal = (x=xMAX & y=yMAX); -formula done = goal | crash; - - -// observations -observable "clk" = clk; -observable "goal" = goal; -observable "crash" = crash; -observable "x_small" = x (clk'=clk_next); - - [east] !done & clk=0 -> (clk'=clk_next); - [west] !done & clk=0 -> (clk'=clk_next); - [north] !done & clk=0 -> (clk'=clk_next); - [south] !done & clk=0 -> (clk'=clk_next); - - [detect1] !done & clk=1 -> (clk'=clk_next); - [detect2] !done & clk=2 -> (clk'=clk_next); - [detect3] !done & clk=3 -> (clk'=clk_next); - [detect4] !done & clk=4 -> (clk'=clk_next); -endmodule - - -// probability of slipping 2 cells ahead -const double slip = 0.1; - -// moving around the grid -module agent - x : [xMIN..xMAX]; - y : [yMIN..yMAX]; - - [place] true -> 1/4: (x'=o1x-1) & (y'=o1y) + 1/4: (x'=1) & (y'=1) + 1/4: (x'=2) & (y'=1) + 1/4: (x'=1) & (y'=3); - - [west] true -> (1-slip): (x'=max(x-1,xMIN)) + slip: (x'=max(x-2,xMIN)); - [east] true -> (1-slip): (x'=min(x+1,xMAX)) + slip: (x'=min(x+2,xMAX)); - [south] true -> (1-slip): (y'=min(y+1,yMAX)) + slip: (y'=min(y+2,yMAX)); - [north] true -> (1-slip): (y'=max(y-1,yMIN)) + slip: (y'=max(y-2,yMIN)); -endmodule - -// crash detection -module crash1 - crash1 : bool init false; - [detect1] near1 -> (crash1'=at1); - [detect1] !near1 -> true; -endmodule - -module crash2=crash1[crash1=crash2,detect1=detect2,near1=near2,at1=at2] endmodule -//module crash3=crash1[crash1=crash3,detect1=detect3,near1=near3,at1=at3] endmodule -//module crash4=crash1[crash1=crash4,detect1=detect4,near1=near4,at1=at4] endmodule diff --git a/models/pomdp/sketches/obstacles-single-pomdp/sketch.props b/models/pomdp/sketches/obstacles-single-pomdp/sketch.props deleted file mode 100755 index 5489c2ec4..000000000 --- a/models/pomdp/sketches/obstacles-single-pomdp/sketch.props +++ /dev/null @@ -1 +0,0 @@ -R{"penalty"}min=? [ F goal ]; \ No newline at end of file diff --git a/models/pomdp/sketches/obstacles-single-pomdp/sketch.templ b/models/pomdp/sketches/obstacles-single-pomdp/sketch.templ deleted file mode 100755 index ab637feaf..000000000 --- a/models/pomdp/sketches/obstacles-single-pomdp/sketch.templ +++ /dev/null @@ -1,96 +0,0 @@ -pomdp - -// grid dimensions -const int N = 10; -const int xMIN = 0; -const int yMIN = 0; -const int xMAX = N-1; -const int yMAX = N-1; - -formula goal = (x=xMAX & y=yMAX); - -observable "clk" = clk; -observable "goal" = goal; -observable "x_small" = x<(xMAX/2); -observable "y_small" = y<(yMAX/2); - -// obstacle coordinates -hole int o1x in {3}; -hole int o1y in {5}; - -hole int o2x in {6}; -hole int o2y in {8}; - -formula near1 = 3<=x & x<=5 & 3<=y & y<=5; -formula near2 = 6<=x & x<=8 & 6<=y & y<=8; -//formula near3 = 1<=x & x<=3 & 3<=y & y<=4; -//formula near4 = 3<=x & x<=4 & 1<=y & y<=3; - -formula at1 = (x = o1x & y = o1y); -formula at2 = (x = o2x & y = o2y); -//formula at3 = (x = o3x & y = o3y); -//formula at4 = (x = o4x & y = o4y); - -const NUM_OBS = 2; - -formula clk_next = mod(clk+1,NUM_OBS+1); -module clk - clk : [-1..NUM_OBS] init -1; - - [place] clk=-1 -> (clk'=clk_next); - - [up] !goal & clk=0 -> (clk'=clk_next); - [down] !goal & clk=0 -> (clk'=clk_next); - [left] !goal & clk=0 -> (clk'=clk_next); - [right] !goal & clk=0 -> (clk'=clk_next); - - [detect1] !goal & clk=1 -> (clk'=clk_next); - [detect2] !goal & clk=2 -> (clk'=clk_next); - [detect3] !goal & clk=3 -> (clk'=clk_next); - [detect4] !goal & clk=4 -> (clk'=clk_next); -endmodule - - -// probability of slipping 2 cells ahead -const double slip = 0.1; - -// moving around the grid -module agent - x : [xMIN..xMAX]; - y : [yMIN..yMAX]; - - [place] true -> 1/4: (x'=o1x-1) & (y'=o1y) + 1/4: (x'=1) & (y'=1) + 1/4: (x'=2) & (y'=1) + 1/4: (x'=1) & (y'=3); - - [up] true -> (1-slip): (y'=max(y-1,yMIN)) + slip: (y'=max(y-2,yMIN)); - [down] true -> (1-slip): (y'=min(y+1,yMAX)) + slip: (y'=min(y+2,yMAX)); - [left] true -> (1-slip): (x'=max(x-1,xMIN)) + slip: (x'=max(x-2,xMIN)); - [right] true -> (1-slip): (x'=min(x+1,xMAX)) + slip: (x'=min(x+2,xMAX)); -endmodule - -// crash detection -module crash1 - crash1 : bool init false; - [detect1] near1 -> (crash1'=at1); - [detect1] !near1 -> true; - - [up] true -> (crash1'=false); - [down] true -> (crash1'=false); - [left] true -> (crash1'=false); - [right] true -> (crash1'=false); -endmodule - -module crash2=crash1[crash1=crash2,detect1=detect2,near1=near2,at1=at2] endmodule -//module crash3=crash1[crash1=crash3,detect1=detect3,near1=near3,at1=at3] endmodule -//module crash4=crash1[crash1=crash4,detect1=detect4,near1=near4,at1=at4] endmodule - -formula step_penalty = 1; -formula crash_penalty = 100; -formula num_crashes = (crash1?1:0)+(crash2?1:0); -formula penalty = step_penalty + num_crashes*crash_penalty; - -rewards "penalty" - [up] true : penalty; - [down] true : penalty; - [left] true : penalty; - [right] true : penalty; -endrewards diff --git a/models/pomdp/sketches/obstacles-uniform/sketch.props b/models/pomdp/sketches/obstacles-uniform/sketch.props deleted file mode 100755 index 5489c2ec4..000000000 --- a/models/pomdp/sketches/obstacles-uniform/sketch.props +++ /dev/null @@ -1 +0,0 @@ -R{"penalty"}min=? [ F goal ]; \ No newline at end of file diff --git a/models/pomdp/sketches/obstacles-uniform/sketch.templ b/models/pomdp/sketches/obstacles-uniform/sketch.templ deleted file mode 100755 index 8408ba84b..000000000 --- a/models/pomdp/sketches/obstacles-uniform/sketch.templ +++ /dev/null @@ -1,107 +0,0 @@ -pomdp - -// grid dimensions -const int N = 10; -const int xMIN = 0; -const int yMIN = 0; -const int xMAX = N-1; -const int yMAX = N-1; - -formula goal = (x=xMAX & y=yMAX); - -observable "clk" = clk; -observable "goal" = goal; -observable "x_small" = x<(xMAX/2); -observable "y_small" = y<(yMAX/2); - -module hole_clk - hole_clk : [0..4] init 0; - [hole_init] hole_clk<4 -> (hole_clk'=hole_clk+1); - [place] hole_clk=4 -> true; -endmodule - -module hole_init - o1x : [3..5]; - o1y : [3..5]; - o2x : [6..8]; - o2y : [6..8]; - - [hole_init] hole_clk=0 -> 1/3:(o1x'=3)+1/3:(o1x'=4)+1/3:(o1x'=5); - [hole_init] hole_clk=1 -> 1/3:(o1y'=3)+1/3:(o1y'=4)+1/3:(o1y'=5); - [hole_init] hole_clk=2 -> 1/3:(o2x'=6)+1/3:(o2x'=7)+1/3:(o2x'=8); - [hole_init] hole_clk=3 -> 1/3:(o2y'=6)+1/3:(o2y'=7)+1/3:(o2y'=8); -endmodule - -formula near1 = 3<=x & x<=5 & 3<=y & y<=5; -formula near2 = 6<=x & x<=8 & 6<=y & y<=8; -//formula near3 = 1<=x & x<=3 & 3<=y & y<=4; -//formula near4 = 3<=x & x<=4 & 1<=y & y<=3; - -formula at1 = (x = o1x & y = o1y); -formula at2 = (x = o2x & y = o2y); -//formula at3 = (x = o3x & y = o3y); -//formula at4 = (x = o4x & y = o4y); - -const NUM_OBS = 2; - -formula clk_next = mod(clk+1,NUM_OBS+1); -module clk - clk : [-1..NUM_OBS] init -1; - - [place] clk=-1 -> (clk'=clk_next); - - [up] !goal & clk=0 -> (clk'=clk_next); - [down] !goal & clk=0 -> (clk'=clk_next); - [left] !goal & clk=0 -> (clk'=clk_next); - [right] !goal & clk=0 -> (clk'=clk_next); - - [detect1] !goal & clk=1 -> (clk'=clk_next); - [detect2] !goal & clk=2 -> (clk'=clk_next); - [detect3] !goal & clk=3 -> (clk'=clk_next); - [detect4] !goal & clk=4 -> (clk'=clk_next); -endmodule - - -// probability of slipping 2 cells ahead -const double slip = 0.1; - -// moving around the grid -module agent - x : [xMIN..xMAX]; - y : [yMIN..yMAX]; - - [place] true -> 1/4: (x'=o1x-1) & (y'=o1y) + 1/4: (x'=1) & (y'=1) + 1/4: (x'=2) & (y'=1) + 1/4: (x'=1) & (y'=3); - - [up] true -> (1-slip): (y'=max(y-1,yMIN)) + slip: (y'=max(y-2,yMIN)); - [down] true -> (1-slip): (y'=min(y+1,yMAX)) + slip: (y'=min(y+2,yMAX)); - [left] true -> (1-slip): (x'=max(x-1,xMIN)) + slip: (x'=max(x-2,xMIN)); - [right] true -> (1-slip): (x'=min(x+1,xMAX)) + slip: (x'=min(x+2,xMAX)); -endmodule - -// crash detection -module crash1 - crash1 : bool init false; - [detect1] near1 -> (crash1'=at1); - [detect1] !near1 -> true; - - [up] true -> (crash1'=false); - [down] true -> (crash1'=false); - [left] true -> (crash1'=false); - [right] true -> (crash1'=false); -endmodule - -module crash2=crash1[crash1=crash2,detect1=detect2,near1=near2,at1=at2] endmodule -//module crash3=crash1[crash1=crash3,detect1=detect3,near1=near3,at1=at3] endmodule -//module crash4=crash1[crash1=crash4,detect1=detect4,near1=near4,at1=at4] endmodule - -formula step_penalty = 1; -formula crash_penalty = 100; -formula num_crashes = (crash1?1:0)+(crash2?1:0); -formula penalty = step_penalty + num_crashes*crash_penalty; - -rewards "penalty" - [up] true : penalty; - [down] true : penalty; - [left] true : penalty; - [right] true : penalty; -endrewards diff --git a/models/pomdp/sketches/obstacles/sketch.props b/models/pomdp/sketches/obstacles/sketch.props deleted file mode 100755 index 5489c2ec4..000000000 --- a/models/pomdp/sketches/obstacles/sketch.props +++ /dev/null @@ -1 +0,0 @@ -R{"penalty"}min=? [ F goal ]; \ No newline at end of file diff --git a/models/pomdp/sketches/obstacles/sketch.templ b/models/pomdp/sketches/obstacles/sketch.templ deleted file mode 100755 index c84214662..000000000 --- a/models/pomdp/sketches/obstacles/sketch.templ +++ /dev/null @@ -1,96 +0,0 @@ -pomdp - -// grid dimensions -const int N = 10; -const int xMIN = 0; -const int yMIN = 0; -const int xMAX = N-1; -const int yMAX = N-1; - -formula goal = (x=xMAX & y=yMAX); - -observable "clk" = clk; -observable "goal" = goal; -observable "x_small" = x<(xMAX/2); -observable "y_small" = y<(yMAX/2); - -// obstacle coordinates -hole int o1x in {3,4,5}; -hole int o1y in {3,4,5}; - -hole int o2x in {6,7,8}; -hole int o2y in {6,7,8}; - -formula near1 = 3<=x & x<=5 & 3<=y & y<=5; -formula near2 = 6<=x & x<=8 & 6<=y & y<=8; -//formula near3 = 1<=x & x<=3 & 3<=y & y<=4; -//formula near4 = 3<=x & x<=4 & 1<=y & y<=3; - -formula at1 = (x = o1x & y = o1y); -formula at2 = (x = o2x & y = o2y); -//formula at3 = (x = o3x & y = o3y); -//formula at4 = (x = o4x & y = o4y); - -const NUM_OBS = 2; - -formula clk_next = mod(clk+1,NUM_OBS+1); -module clk - clk : [-1..NUM_OBS] init -1; - - [place] clk=-1 -> (clk'=clk_next); - - [up] !goal & clk=0 -> (clk'=clk_next); - [down] !goal & clk=0 -> (clk'=clk_next); - [left] !goal & clk=0 -> (clk'=clk_next); - [right] !goal & clk=0 -> (clk'=clk_next); - - [detect1] !goal & clk=1 -> (clk'=clk_next); - [detect2] !goal & clk=2 -> (clk'=clk_next); - [detect3] !goal & clk=3 -> (clk'=clk_next); - [detect4] !goal & clk=4 -> (clk'=clk_next); -endmodule - - -// probability of slipping 2 cells ahead -const double slip = 0.1; - -// moving around the grid -module agent - x : [xMIN..xMAX]; - y : [yMIN..yMAX]; - - [place] true -> 1/4: (x'=o1x-1) & (y'=o1y) + 1/4: (x'=1) & (y'=1) + 1/4: (x'=2) & (y'=1) + 1/4: (x'=1) & (y'=3); - - [up] true -> (1-slip): (y'=max(y-1,yMIN)) + slip: (y'=max(y-2,yMIN)); - [down] true -> (1-slip): (y'=min(y+1,yMAX)) + slip: (y'=min(y+2,yMAX)); - [left] true -> (1-slip): (x'=max(x-1,xMIN)) + slip: (x'=max(x-2,xMIN)); - [right] true -> (1-slip): (x'=min(x+1,xMAX)) + slip: (x'=min(x+2,xMAX)); -endmodule - -// crash detection -module crash1 - crash1 : bool init false; - [detect1] near1 -> (crash1'=at1); - [detect1] !near1 -> true; - - [up] true -> (crash1'=false); - [down] true -> (crash1'=false); - [left] true -> (crash1'=false); - [right] true -> (crash1'=false); -endmodule - -module crash2=crash1[crash1=crash2,detect1=detect2,near1=near2,at1=at2] endmodule -//module crash3=crash1[crash1=crash3,detect1=detect3,near1=near3,at1=at3] endmodule -//module crash4=crash1[crash1=crash4,detect1=detect4,near1=near4,at1=at4] endmodule - -formula step_penalty = 1; -formula crash_penalty = 100; -formula num_crashes = (crash1?1:0)+(crash2?1:0); -formula penalty = step_penalty + num_crashes*crash_penalty; - -rewards "penalty" - [up] true : penalty; - [down] true : penalty; - [left] true : penalty; - [right] true : penalty; -endrewards diff --git a/paynt/parser/jani.py b/paynt/parser/jani.py index 73e64b6a7..eb52b69a4 100644 --- a/paynt/parser/jani.py +++ b/paynt/parser/jani.py @@ -60,13 +60,12 @@ def __init__(self, prism, hole_expressions, specification, family): # unfold holes in the program self.hole_expressions = hole_expressions self.jani_unfolded = None - self.combination_coloring = None self.unfold_jani(jani, family) logger.debug("constructing the quotient...") # construct the explicit quotient quotient_mdp = paynt.models.model_builder.ModelBuilder.from_jani(self.jani_unfolded, self.specification) - + # associate each action of a quotient MDP with hole options # reconstruct choice labels from choice origins logger.debug("associating choices of the quotient with hole assignments...") @@ -104,16 +103,15 @@ def unfold_jani(self, jani, family): for hole in range(family.num_holes): assert family.hole_name(hole) == open_constants[hole].name - self.combination_coloring = CombinationColoring() - + combination_coloring = CombinationColoring() jani_program = stormpy.JaniModel(jani) new_automata = dict() - for aut_index, automaton in enumerate(jani_program.automata): + for aut_index,automaton in enumerate(jani_program.automata): if not self.automaton_has_holes(automaton, set(expression_variables)): continue - new_aut = self.construct_automaton(automaton, family, expression_variables) + new_aut = self.construct_automaton(automaton, family, expression_variables, combination_coloring) new_automata[aut_index] = new_aut - for aut_index, aut in new_automata.items(): + for aut_index,aut in new_automata.items(): jani_program.replace_automaton(aut_index, aut) for hole in range(family.num_holes): jani_program.remove_constant(family.hole_name(hole)) @@ -130,7 +128,7 @@ def unfold_jani(self, jani, family): if edge.color == 0: continue - options = self.combination_coloring.reverse_coloring[edge.color] + options = combination_coloring.reverse_coloring[edge.color] options = [(hole_index,option) for hole_index,option in enumerate(options) if option is not None] edge_to_hole_options[global_index] = options @@ -138,30 +136,35 @@ def unfold_jani(self, jani, family): self.edge_to_hole_options = edge_to_hole_options - def automaton_has_holes(self, automaton, expression_variables): - for edge_index, e in enumerate(automaton.edges): - if e.guard.contains_variable(expression_variables): + def edge_has_holes(self, edge, expression_variables): + if edge.guard.contains_variable(expression_variables): + return True + for dest in edge.destinations: + if dest.probability.contains_variable(expression_variables): return True - for dest in e.destinations: - if dest.probability.contains_variable(expression_variables): + for assignment in dest.assignments: + if assignment.expression.contains_variable(expression_variables): return True - for assignment in dest.assignments: - if assignment.expression.contains_variable(expression_variables): - return True return False - def construct_automaton(self, automaton, family, expression_variables): + def automaton_has_holes(self, automaton, expression_variables): + for edge in automaton.edges: + if self.edge_has_holes(edge,expression_variables): + return True + return False + + def construct_automaton(self, automaton, family, expression_variables, combination_coloring): new_aut = stormpy.storage.JaniAutomaton(automaton.name, automaton.location_variable) [new_aut.add_location(loc) for loc in automaton.locations] [new_aut.add_initial_location(idx) for idx in automaton.initial_location_indices] [new_aut.variables.add_variable(var) for var in automaton.variables] for edge in automaton.edges: - new_edges = self.construct_edges(edge, family, expression_variables) + new_edges = self.construct_edges(edge, family, expression_variables, combination_coloring) for new_edge in new_edges: new_aut.add_edge(new_edge) return new_aut - def construct_edges(self, edge, family, expression_variables): + def construct_edges(self, edge, family, expression_variables, combination_coloring): # relevant holes in guard variables = edge.template_edge.guard.get_variables() @@ -199,7 +202,7 @@ def construct_edges(self, edge, family, expression_variables): if combination[hole] is not None } new_edge = self.construct_edge(edge,substitution) - new_edge.color = self.combination_coloring.get_or_make_color(combination) + new_edge.color = combination_coloring.get_or_make_color(combination) new_edges.append(new_edge) return new_edges @@ -216,8 +219,8 @@ def construct_edge(self, edge, substitution = None): for templ_edge_dest in edge.template_edge.destinations: assignments = templ_edge_dest.assignments.clone() if substitution is not None: - assignments.substitute(substitution, substitute_transcendental_numbers=True) - # assignments.substitute(substitution) # legacy version + # assignments.substitute(substitution, substitute_transcendental_numbers=True) + assignments.substitute(substitution) # legacy version templ_edge.add_destination(stormpy.storage.JaniTemplateEdgeDestination(assignments)) new_edge = stormpy.storage.JaniEdge( diff --git a/paynt/parser/sketch.py b/paynt/parser/sketch.py index e188780e7..d01736cd8 100644 --- a/paynt/parser/sketch.py +++ b/paynt/parser/sketch.py @@ -146,7 +146,24 @@ def load_sketch(cls, sketch_path, properties_path, logger.info("export OK, aborting...") exit(0) - return Sketch.build_quotient_container(prism, jani_unfolder, explicit_quotient, family, coloring, specification, obs_evaluator, decpomdp_manager) + if jani_unfolder is not None: + if prism.model_type == stormpy.storage.PrismModelType.DTMC: + quotient_container = paynt.quotient.quotient.Quotient(explicit_quotient, family, coloring, specification) + elif prism.model_type == stormpy.storage.PrismModelType.MDP: + quotient_container = paynt.quotient.mdp_family.MdpFamilyQuotient(explicit_quotient, family, coloring, specification) + elif prism.model_type == stormpy.storage.PrismModelType.POMDP: + quotient_container = paynt.quotient.pomdp_family.PomdpFamilyQuotient(explicit_quotient, family, coloring, specification, obs_evaluator) + else: + assert explicit_quotient.is_nondeterministic_model, "expected nondeterministic model" + if decpomdp_manager is not None and decpomdp_manager.num_agents > 1: + quotient_container = paynt.quotient.decpomdp.DecPomdpQuotient(decpomdp_manager, specification) + elif explicit_quotient.labeling.contains_label(paynt.quotient.posg.PosgQuotient.PLAYER_1_STATE_LABEL): + quotient_container = paynt.quotient.posg.PosgQuotient(explicit_quotient, specification) + elif not explicit_quotient.is_partially_observable: + quotient_container = paynt.quotient.mdp.MdpQuotient(explicit_quotient, specification) + else: + quotient_container = paynt.quotient.pomdp.PomdpQuotient(explicit_quotient, specification, decpomdp_manager) + return quotient_container @classmethod @@ -217,27 +234,3 @@ def export(cls, export, sketch_path, jani_unfolder, explicit_quotient): output_path = substitute_suffix(sketch_path, '.', 'pomdp') property_path = substitute_suffix(sketch_path, '/', 'props.pomdp') paynt.parser.pomdp_parser.PomdpParser.write_model_in_pomdp_solve_format(explicit_quotient, output_path, property_path) - - - @classmethod - def build_quotient_container(cls, prism, jani_unfolder, explicit_quotient, family, coloring, specification, obs_evaluator, decpomdp_manager): - if jani_unfolder is not None: - if prism.model_type == stormpy.storage.PrismModelType.DTMC: - quotient_container = paynt.quotient.quotient.Quotient(explicit_quotient, family, coloring, specification) - elif prism.model_type == stormpy.storage.PrismModelType.MDP: - quotient_container = paynt.quotient.mdp_family.MdpFamilyQuotient(explicit_quotient, family, coloring, specification) - elif prism.model_type == stormpy.storage.PrismModelType.POMDP: - quotient_container = paynt.quotient.pomdp_family.PomdpFamilyQuotient(explicit_quotient, family, coloring, specification, obs_evaluator) - else: - assert explicit_quotient.is_nondeterministic_model, "expected nondeterministic model" - if decpomdp_manager is not None and decpomdp_manager.num_agents > 1: - quotient_container = paynt.quotient.decpomdp.DecPomdpQuotient(decpomdp_manager, specification) - elif explicit_quotient.labeling.contains_label(paynt.quotient.posg.PosgQuotient.PLAYER_1_STATE_LABEL): - quotient_container = paynt.quotient.posg.PosgQuotient(explicit_quotient, specification) - elif not explicit_quotient.is_partially_observable: - quotient_container = paynt.quotient.mdp.MdpQuotient(explicit_quotient, specification) - else: - quotient_container = paynt.quotient.pomdp.PomdpQuotient(explicit_quotient, specification, decpomdp_manager) - return quotient_container - - diff --git a/payntbind/src/synthesis/translation/componentTranslations.cpp b/payntbind/src/synthesis/translation/componentTranslations.cpp index 92bd03a11..1d9deb817 100644 --- a/payntbind/src/synthesis/translation/componentTranslations.cpp +++ b/payntbind/src/synthesis/translation/componentTranslations.cpp @@ -103,10 +103,8 @@ storm::models::sparse::StandardRewardModel translateRewardModel( storm::storage::BitVector const& translated_choice_mask ) { std::optional> state_rewards; - STORM_LOG_THROW(!reward_model.hasStateRewards(), storm::exceptions::NotSupportedException, - "state rewards are currently not supported."); - STORM_LOG_THROW(!reward_model.hasTransitionRewards(), storm::exceptions::NotSupportedException, - "transition rewards are currently not supported."); + STORM_LOG_THROW(!reward_model.hasStateRewards() and !reward_model.hasTransitionRewards() and reward_model.hasStateActionRewards(), + storm::exceptions::NotSupportedException, "expected state-action rewards"); uint64_t num_choices = reward_model.getStateActionRewardVector().size(); std::vector action_rewards(translated_to_original_choice.size());