diff --git a/prism-examples/pomdps/simple/guess-multi.prism b/prism-examples/pomdps/simple/guess-multi.prism new file mode 100644 index 00000000..a8f50124 --- /dev/null +++ b/prism-examples/pomdps/simple/guess-multi.prism @@ -0,0 +1,37 @@ +// Simple POMDP guessing a hidden variable (multiple attempts) + +pomdp + +// Number of guesses allowed (N=1,2,3,4) +const int N; + +observables s, g endobservables + +module M + + s : [0..2]; // state + h : [0..3]; // hidden var + g : [0..N] init N; // num guesses left + + // Assign hidden variable randomly + [toss] s=0 -> 0.1:(s'=1)&(h'=1) + 0.3:(s'=1)&(h'=2) + 0.6:(s'=1)&(h'=3); + // Guess the value of the hidden variable + [guess1] s=1&g>0 -> (s'=(h=1)?2:s) & (g'=g-1); + [guess2] s=1&g>0 -> (s'=(h=2)?2:s) & (g'=g-1); + [guess3] s=1&g>0 -> (s'=(h=3)?2:s) & (g'=g-1); + // No more guesses left + [timeup] s=1&g=0 -> (s'=3); + // Done + [loop] s=2 -> true; + +endmodule + +label "correct" = s=2; + +// Number of guesses made +rewards "guesses" + [guess1] true : 1; + [guess2] true : 1; + [guess3] true : 1; +endrewards + diff --git a/prism-examples/pomdps/simple/guess-multi.props b/prism-examples/pomdps/simple/guess-multi.props new file mode 100644 index 00000000..9e35a6dd --- /dev/null +++ b/prism-examples/pomdps/simple/guess-multi.props @@ -0,0 +1,7 @@ +// Maximum probability of guessing the value correctly +// (should be 1 for N>=3) +Pmax=? [ F "correct" ]; + +// Minimum expected number of guesses before guessing the value correctly +// (will be infinite for N<3) +R{"guesses"}min=? [ F "correct" ]; diff --git a/prism-examples/pomdps/simple/guess.prism b/prism-examples/pomdps/simple/guess.prism new file mode 100644 index 00000000..8a1c8499 --- /dev/null +++ b/prism-examples/pomdps/simple/guess.prism @@ -0,0 +1,23 @@ +// Simple POMDP guessing a hidden variable + +pomdp + +observables s endobservables + +module M + + s : [0..2]; // state + h : [0..3]; // hidden var + + // Assign hidden variable randomly + [toss] s=0 -> 0.1:(s'=1)&(h'=1) + 0.3:(s'=1)&(h'=2) + 0.6:(s'=1)&(h'=3); + // Guess the value of the hidden variable + [guess1] s=1 -> (s'=(h=1)?2:3); + [guess2] s=1 -> (s'=(h=2)?2:3); + [guess3] s=1 -> (s'=(h=3)?2:3); + // Done + [loop] s=2 -> true; + +endmodule + +label "correct" = s=2; diff --git a/prism-examples/pomdps/simple/guess.props b/prism-examples/pomdps/simple/guess.props new file mode 100644 index 00000000..19500169 --- /dev/null +++ b/prism-examples/pomdps/simple/guess.props @@ -0,0 +1,3 @@ +// Maximum probability of guessing the value correctly +// (equals the probability of the most likely value) +Pmax=? [ F "correct" ];