diff --git a/examples/dtmc/sync/sync.pm b/examples/dtmc/sync/sync.pm new file mode 100644 index 000000000..8bc7f94ce --- /dev/null +++ b/examples/dtmc/sync/sync.pm @@ -0,0 +1,22 @@ +// A simple model using synchronization +dtmc + +module generator + + s : [0..2] init 0; + + [] s=0 -> 0.2 : (s'=1) + 0.8 : (s'=0); + [yield] s=1 -> 1 : (s'=2); + [] s=2 -> 0.5 : (s'=0) + 0.5 : (s'=2); + +endmodule + +module consumer + + t : [0..2] init 0; + + [] t=0 -> 0.8 : (t'=1) + 0.2 : (t'=0); + [yield] t=1 -> 1 : (t'=2); + [] t=2 -> 0.2 : (t'=0) + 0.8 : (t'=2); + +endmodule