// prism find a single ergodic set (BSCC) specified by the following atomic proposition
label "ergodic1" = (a1=1 & a2=3 & a3=2 & a4=6 & a5=7 & a6=4 & a7=5 & a8=8) |
                   (a1=2 & a2=1 & a3=3 & a4=6 & a5=7 & a6=4 & a7=5 & a8=8) |
                   (a1=2 & a2=1 & a3=8 & a4=6 & a5=7 & a6=4 & a7=5 & a8=3) |
                   (a1=3 & a2=2 & a3=1 & a4=6 & a5=7 & a6=4 & a7=5 & a8=8);

// probability reached a ergodic set by round R
const int r; // bound of number of rounds
P=?[ F<=r "ergodic1" ]

// expected number of rounds to reach the ergodic set
R{"rounds"}=? [ F "ergodic1" ]