tempest/examples/ctmc/tiny/tiny.sm

ctmc

module one
  s : [0 .. 3] init 1;
  
  [] s<3 -> 3/2 : (s'=s+1);
  [] s>0 -> 3 : (s'=s-1);
endmodule

label "empty" = s=0;
label "full" = s=3;