From 1bfd864d2e89577ba8d6f7e7148c195086db9bf0 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@web.de>
Date: Sat, 2 Jul 2016 15:40:52 +0200
Subject: [PATCH] new stream instances

Former-commit-id: 7b142e5dc9dfc8ff41c9c3a67e8bed8e217093ca
---
 .../displaypareto/displaypareto.tex           |  9 ++--
 examples/multiobjective/ma/stream/stream10.ma | 50 +++++++++++++++++++
 .../multiobjective/ma/stream/stream100.ma     | 50 +++++++++++++++++++
 .../multiobjective/ma/stream/stream1000.ma    | 50 +++++++++++++++++++
 examples/multiobjective/ma/stream/stream50.ma | 50 +++++++++++++++++++
 .../multiobjective/ma/stream/stream500.ma     | 50 +++++++++++++++++++
 .../multiobjective/ma/stream/stream5000.ma    | 50 +++++++++++++++++++
 7 files changed, 305 insertions(+), 4 deletions(-)
 create mode 100644 examples/multiobjective/ma/stream/stream10.ma
 create mode 100644 examples/multiobjective/ma/stream/stream100.ma
 create mode 100644 examples/multiobjective/ma/stream/stream1000.ma
 create mode 100644 examples/multiobjective/ma/stream/stream50.ma
 create mode 100644 examples/multiobjective/ma/stream/stream500.ma
 create mode 100644 examples/multiobjective/ma/stream/stream5000.ma

diff --git a/examples/multiobjective/displaypareto/displaypareto.tex b/examples/multiobjective/displaypareto/displaypareto.tex
index 17d5909b8..688b91aa9 100644
--- a/examples/multiobjective/displaypareto/displaypareto.tex
+++ b/examples/multiobjective/displaypareto/displaypareto.tex
@@ -4,15 +4,16 @@
 
 %\newcommand{\resultPath}{../mdp/consensus/results_3_3_2/}
 %\newcommand{\resultPath}{../mdp/scheduler/results05/}
-\newcommand{\resultPath}{../mdp/zeroconf-tb/results4_10/}
+%\newcommand{\resultPath}{../mdp/zeroconf-tb/results4_10/}
+\newcommand{\resultPath}{../ma/stream/results1000/}
 
 \begin{document}
 	\centering
 \begin{tikzpicture}[scale=1.75]
 \begin{axis}[enlargelimits=false, axis background/.style={fill=red!50}]
-\addplot[fill=white] table [col sep=comma] {\resultPath overapproximation.csv} -- cycle;
-\addplot[fill=green] table [col sep=comma] {\resultPath underapproximation.csv} -- cycle;
-\addplot[mark=o, mark options={blue, scale=1.5, thick}, only marks] table [col sep=comma] {\resultPath paretopoints.csv};
+\addplot[fill=white, very thin] table [col sep=comma] {\resultPath overapproximation.csv} -- cycle;
+\addplot[fill=green, very thin] table [col sep=comma] {\resultPath underapproximation.csv} -- cycle;
+%\addplot[mark=o, mark options={blue, scale=1.3, thick}, only marks] table [col sep=comma] {\resultPath paretopoints.csv};
 \addplot[mark=false] table [col sep=comma] {\resultPath boundaries.csv};
 \end{axis}
 \end{tikzpicture}
diff --git a/examples/multiobjective/ma/stream/stream10.ma b/examples/multiobjective/ma/stream/stream10.ma
new file mode 100644
index 000000000..c7fc431f9
--- /dev/null
+++ b/examples/multiobjective/ma/stream/stream10.ma
@@ -0,0 +1,50 @@
+
+ma
+
+const int N=10; // num packages
+
+const double inRate = 4;
+const double processingRate = 5;
+
+module streamingclient
+	
+	s : [0..3]; // current state:
+	// 0: decide whether to start	
+	// 1: buffering
+	// 2: running
+	// 3: done
+	
+	n : [0..N]; // number of received packages
+	k : [0..N]; // number of processed packages 	
+	
+	[buffer]  s=0 & n<N -> 1 : (s'=1);
+	[start] s=0 & k<n -> 1 : (s'=2) & (k'=k+1);
+	
+	<> s=1 -> inRate : (n'=n+1) & (s'=0);
+	
+	<> s=2 & n<N & k<n -> inRate : (n'=n+1) + processingRate : (k'=k+1);
+	<> s=2 & n<N & k=n -> inRate : (n'=n+1) + processingRate : (s'=0); 
+	<> s=2 & n=N & k<n -> processingRate : (k'=k+1);
+	<> s=2 & n=N & k=N -> processingRate : (s'=3);
+	
+	<> s=3 -> 1 : true;
+endmodule
+
+// All packages received and buffer empty
+label "done" = (s=3);
+
+rewards "buffering"
+	s=1 : 1;
+endrewards
+
+rewards "initialbuffering"
+	s=1 & k = 0: 1;
+endrewards
+
+rewards "intermediatebuffering"
+	s=1 & k > 0: 1;
+endrewards
+
+rewards "numRestarts"
+	[start] k > 0 : 1;
+endrewards
diff --git a/examples/multiobjective/ma/stream/stream100.ma b/examples/multiobjective/ma/stream/stream100.ma
new file mode 100644
index 000000000..8eee818ba
--- /dev/null
+++ b/examples/multiobjective/ma/stream/stream100.ma
@@ -0,0 +1,50 @@
+
+ma
+
+const int N=100; // num packages
+
+const double inRate = 4;
+const double processingRate = 5;
+
+module streamingclient
+	
+	s : [0..3]; // current state:
+	// 0: decide whether to start	
+	// 1: buffering
+	// 2: running
+	// 3: done
+	
+	n : [0..N]; // number of received packages
+	k : [0..N]; // number of processed packages 	
+	
+	[buffer]  s=0 & n<N -> 1 : (s'=1);
+	[start] s=0 & k<n -> 1 : (s'=2) & (k'=k+1);
+	
+	<> s=1 -> inRate : (n'=n+1) & (s'=0);
+	
+	<> s=2 & n<N & k<n -> inRate : (n'=n+1) + processingRate : (k'=k+1);
+	<> s=2 & n<N & k=n -> inRate : (n'=n+1) + processingRate : (s'=0); 
+	<> s=2 & n=N & k<n -> processingRate : (k'=k+1);
+	<> s=2 & n=N & k=N -> processingRate : (s'=3);
+	
+	<> s=3 -> 1 : true;
+endmodule
+
+// All packages received and buffer empty
+label "done" = (s=3);
+
+rewards "buffering"
+	s=1 : 1;
+endrewards
+
+rewards "initialbuffering"
+	s=1 & k = 0: 1;
+endrewards
+
+rewards "intermediatebuffering"
+	s=1 & k > 0: 1;
+endrewards
+
+rewards "numRestarts"
+	[start] k > 0 : 1;
+endrewards
diff --git a/examples/multiobjective/ma/stream/stream1000.ma b/examples/multiobjective/ma/stream/stream1000.ma
new file mode 100644
index 000000000..1860928f7
--- /dev/null
+++ b/examples/multiobjective/ma/stream/stream1000.ma
@@ -0,0 +1,50 @@
+
+ma
+
+const int N=1000; // num packages
+
+const double inRate = 4;
+const double processingRate = 5;
+
+module streamingclient
+	
+	s : [0..3]; // current state:
+	// 0: decide whether to start	
+	// 1: buffering
+	// 2: running
+	// 3: done
+	
+	n : [0..N]; // number of received packages
+	k : [0..N]; // number of processed packages 	
+	
+	[buffer]  s=0 & n<N -> 1 : (s'=1);
+	[start] s=0 & k<n -> 1 : (s'=2) & (k'=k+1);
+	
+	<> s=1 -> inRate : (n'=n+1) & (s'=0);
+	
+	<> s=2 & n<N & k<n -> inRate : (n'=n+1) + processingRate : (k'=k+1);
+	<> s=2 & n<N & k=n -> inRate : (n'=n+1) + processingRate : (s'=0); 
+	<> s=2 & n=N & k<n -> processingRate : (k'=k+1);
+	<> s=2 & n=N & k=N -> processingRate : (s'=3);
+	
+	<> s=3 -> 1 : true;
+endmodule
+
+// All packages received and buffer empty
+label "done" = (s=3);
+
+rewards "buffering"
+	s=1 : 1;
+endrewards
+
+rewards "initialbuffering"
+	s=1 & k = 0: 1;
+endrewards
+
+rewards "intermediatebuffering"
+	s=1 & k > 0: 1;
+endrewards
+
+rewards "numRestarts"
+	[start] k > 0 : 1;
+endrewards
diff --git a/examples/multiobjective/ma/stream/stream50.ma b/examples/multiobjective/ma/stream/stream50.ma
new file mode 100644
index 000000000..190122cde
--- /dev/null
+++ b/examples/multiobjective/ma/stream/stream50.ma
@@ -0,0 +1,50 @@
+
+ma
+
+const int N=50; // num packages
+
+const double inRate = 4;
+const double processingRate = 5;
+
+module streamingclient
+	
+	s : [0..3]; // current state:
+	// 0: decide whether to start	
+	// 1: buffering
+	// 2: running
+	// 3: done
+	
+	n : [0..N]; // number of received packages
+	k : [0..N]; // number of processed packages 	
+	
+	[buffer]  s=0 & n<N -> 1 : (s'=1);
+	[start] s=0 & k<n -> 1 : (s'=2) & (k'=k+1);
+	
+	<> s=1 -> inRate : (n'=n+1) & (s'=0);
+	
+	<> s=2 & n<N & k<n -> inRate : (n'=n+1) + processingRate : (k'=k+1);
+	<> s=2 & n<N & k=n -> inRate : (n'=n+1) + processingRate : (s'=0); 
+	<> s=2 & n=N & k<n -> processingRate : (k'=k+1);
+	<> s=2 & n=N & k=N -> processingRate : (s'=3);
+	
+	<> s=3 -> 1 : true;
+endmodule
+
+// All packages received and buffer empty
+label "done" = (s=3);
+
+rewards "buffering"
+	s=1 : 1;
+endrewards
+
+rewards "initialbuffering"
+	s=1 & k = 0: 1;
+endrewards
+
+rewards "intermediatebuffering"
+	s=1 & k > 0: 1;
+endrewards
+
+rewards "numRestarts"
+	[start] k > 0 : 1;
+endrewards
diff --git a/examples/multiobjective/ma/stream/stream500.ma b/examples/multiobjective/ma/stream/stream500.ma
new file mode 100644
index 000000000..90933bd63
--- /dev/null
+++ b/examples/multiobjective/ma/stream/stream500.ma
@@ -0,0 +1,50 @@
+
+ma
+
+const int N=500; // num packages
+
+const double inRate = 4;
+const double processingRate = 5;
+
+module streamingclient
+	
+	s : [0..3]; // current state:
+	// 0: decide whether to start	
+	// 1: buffering
+	// 2: running
+	// 3: done
+	
+	n : [0..N]; // number of received packages
+	k : [0..N]; // number of processed packages 	
+	
+	[buffer]  s=0 & n<N -> 1 : (s'=1);
+	[start] s=0 & k<n -> 1 : (s'=2) & (k'=k+1);
+	
+	<> s=1 -> inRate : (n'=n+1) & (s'=0);
+	
+	<> s=2 & n<N & k<n -> inRate : (n'=n+1) + processingRate : (k'=k+1);
+	<> s=2 & n<N & k=n -> inRate : (n'=n+1) + processingRate : (s'=0); 
+	<> s=2 & n=N & k<n -> processingRate : (k'=k+1);
+	<> s=2 & n=N & k=N -> processingRate : (s'=3);
+	
+	<> s=3 -> 1 : true;
+endmodule
+
+// All packages received and buffer empty
+label "done" = (s=3);
+
+rewards "buffering"
+	s=1 : 1;
+endrewards
+
+rewards "initialbuffering"
+	s=1 & k = 0: 1;
+endrewards
+
+rewards "intermediatebuffering"
+	s=1 & k > 0: 1;
+endrewards
+
+rewards "numRestarts"
+	[start] k > 0 : 1;
+endrewards
diff --git a/examples/multiobjective/ma/stream/stream5000.ma b/examples/multiobjective/ma/stream/stream5000.ma
new file mode 100644
index 000000000..32dea35a6
--- /dev/null
+++ b/examples/multiobjective/ma/stream/stream5000.ma
@@ -0,0 +1,50 @@
+
+ma
+
+const int N=5000; // num packages
+
+const double inRate = 4;
+const double processingRate = 5;
+
+module streamingclient
+	
+	s : [0..3]; // current state:
+	// 0: decide whether to start	
+	// 1: buffering
+	// 2: running
+	// 3: done
+	
+	n : [0..N]; // number of received packages
+	k : [0..N]; // number of processed packages 	
+	
+	[buffer]  s=0 & n<N -> 1 : (s'=1);
+	[start] s=0 & k<n -> 1 : (s'=2) & (k'=k+1);
+	
+	<> s=1 -> inRate : (n'=n+1) & (s'=0);
+	
+	<> s=2 & n<N & k<n -> inRate : (n'=n+1) + processingRate : (k'=k+1);
+	<> s=2 & n<N & k=n -> inRate : (n'=n+1) + processingRate : (s'=0); 
+	<> s=2 & n=N & k<n -> processingRate : (k'=k+1);
+	<> s=2 & n=N & k=N -> processingRate : (s'=3);
+	
+	<> s=3 -> 1 : true;
+endmodule
+
+// All packages received and buffer empty
+label "done" = (s=3);
+
+rewards "buffering"
+	s=1 : 1;
+endrewards
+
+rewards "initialbuffering"
+	s=1 & k = 0: 1;
+endrewards
+
+rewards "intermediatebuffering"
+	s=1 & k > 0: 1;
+endrewards
+
+rewards "numRestarts"
+	[start] k > 0 : 1;
+endrewards