new stream instances

Former-commit-id: 7b142e5dc9

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}

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

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

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

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

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

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