Former-commit-id: 1af510712a
1af510712a
@ -0,0 +1,26 @@
// sum of two dice as the asynchronous parallel composition of
// two copies of Knuth's model of a fair die using only fair coins
mdp
module simple
// local state
s : [0..2] init 0;
[A] s=0 -> 0.2 : (s'=1) + 0.8 : (s'=0);
[B] s=0 -> 1 : (s'=2);
[] s>0 -> 1 : (s'=s);
endmodule
rewards "actA"
[A] true : 1;
endrewards
rewards "actB"
[B] true : 2;
label "a" = s=1;
label "b" = s=2;
@ -0,0 +1,3 @@
Pmax=? [ F "a" ] ;
Pmax=? [ F "b" ] ;
multi(P>0.4 [ F "a"], P>0.3 [ F "b"] )