diff --git a/examples/multi-objective/mdp/simple/simple.nm b/examples/multi-objective/mdp/simple/simple.nm new file mode 100644 index 000000000..50c4fe344 --- /dev/null +++ b/examples/multi-objective/mdp/simple/simple.nm @@ -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; +endrewards + + +label "a" = s=1; +label "b" = s=2; \ No newline at end of file diff --git a/examples/multi-objective/mdp/simple/simple.pctl b/examples/multi-objective/mdp/simple/simple.pctl new file mode 100644 index 000000000..1300542f9 --- /dev/null +++ b/examples/multi-objective/mdp/simple/simple.pctl @@ -0,0 +1,3 @@ +Pmax=? [ F "a" ] ; +Pmax=? [ F "b" ] ; +multi(P>0.4 [ F "a"], P>0.3 [ F "b"] ) \ No newline at end of file