From 52dedca2a085e1b8e4b7b3e4dc3b27696e89b28c Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 24 Dec 2015 09:31:37 +0100
Subject: [PATCH] added tiny example for long-run properties

Former-commit-id: 245d0c96c90ae8aff32ed9c40154643b5aca39c8
---
 examples/pdtmc/tiny/tiny.pm | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 examples/pdtmc/tiny/tiny.pm

diff --git a/examples/pdtmc/tiny/tiny.pm b/examples/pdtmc/tiny/tiny.pm
new file mode 100644
index 000000000..fca4f4de3
--- /dev/null
+++ b/examples/pdtmc/tiny/tiny.pm
@@ -0,0 +1,11 @@
+dtmc
+
+module tiny
+  s : [0 .. 2] init 0;
+
+  [] s = 0 -> 1/2 : (s'=1) + 1/2 : (s'=2);
+  [] s = 1 -> 1 : (s'=2);
+  [] s = 2 -> 1/2 : (s'=2) + 1/2 : (s'=1);
+
+endmodule
+