From 270c3125b510ccef404083c09d23f85f3b7e3612 Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Mon, 25 Feb 2013 12:45:58 +0100
Subject: [PATCH] Adding new simple example pm file.

sync.pm contains a very simple model that uses the synchronization feature of prism.
---
 examples/dtmc/sync/sync.pm | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)
 create mode 100644 examples/dtmc/sync/sync.pm

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