Added kanban model for LRA test

resources/examples/testfiles/ctmc/kanban.prism

@@ -0,0 +1,111 @@
+// kanban manufacturing example [CT96]
+// dxp/gxn 3/2/00
+
+ctmc
+
+// number of tokens 
+const int t = 1; 
+
+// rates
+const double in1      = 1.0;
+const double out4     = 0.9;
+const double synch123 = 0.4;
+const double synch234 = 0.5;
+const double back     = 0.3;
+const double redo1    = 0.36;
+const double redo2    = 0.42;
+const double redo3    = 0.39;
+const double redo4    = 0.33;
+const double ok1      = 0.84;
+const double ok2      = 0.98;
+const double ok3      = 0.91;
+const double ok4      = 0.77;
+
+module k1
+
+	w1 : [0..t];
+	x1 : [0..t];
+	y1 : [0..t];
+	z1 : [0..t];
+	
+	[in]   (w1<t) & (x1<t) -> in1 	 : (w1'=w1+1) & (x1'=x1+1);
+	[]   (x1>0) & (y1<t) -> redo1	 : (x1'=x1-1) & (y1'=y1+1);
+	[]   (x1>0) & (z1<t) -> ok1 	 : (x1'=x1-1) & (z1'=z1+1);
+	[]   (y1>0) & (x1<t) -> back	 : (y1'=y1-1) & (x1'=x1+1);
+	[s1] (z1>0) & (w1>0) -> synch123 : (z1'=z1-1) & (w1'=w1-1);
+
+endmodule
+
+module k2
+
+	w2 : [0..t];
+	x2 : [0..t];
+	y2 : [0..t];
+	z2 : [0..t];
+	
+	[s1] (w2<t) & (x2<t) -> 1	 : (w2'=w2+1) & (x2'=x2+1);
+	[]   (x2>0) & (y2<t) -> redo2 : (x2'=x2-1) & (y2'=y2+1);
+	[]   (x2>0) & (z2<t) -> ok2   : (x2'=x2-1) & (z2'=z2+1);
+	[]   (y2>0) & (x2<t) -> back  : (y2'=y2-1) & (x2'=x2+1);
+	[s2] (z2>0) & (w2>0) -> 1	 : (z2'=z2-1) & (w2'=w2-1);
+
+endmodule
+
+module k3
+
+	w3 : [0..t];
+	x3 : [0..t];
+	y3 : [0..t];
+	z3 : [0..t];
+	
+	[s1] (w3<t) & (x3<t) -> 1	 : (w3'=w3+1) & (x3'=x3+1);
+	[]   (x3>0) & (y3<t) -> redo3 : (x3'=x3-1) & (y3'=y3+1);
+	[]   (x3>0) & (z3<t) -> ok3   : (x3'=x3-1) & (z3'=z3+1);
+	[]   (y3>0) & (x3<t) -> back  : (y3'=y3-1) & (x3'=x3+1);
+	[s2] (z3>0) & (w3>0) -> 1	 : (z3'=z3-1) & (w3'=w3-1);
+
+
+endmodule
+
+module k4
+
+	w4 : [0..t];
+	x4 : [0..t];
+	y4 : [0..t];
+	z4 : [0..t];
+	
+	[s2] (w4<t) & (x4<t) -> synch234 : (w4'=w4+1) & (x4'=x4+1);
+	[]   (x4>0) & (y4<t) -> redo4	: (x4'=x4-1) & (y4'=y4+1);
+	[]   (x4>0) & (z4<t) -> ok4  	: (x4'=x4-1) & (z4'=z4+1);
+	[]   (y4>0) & (x4<t) -> back 	: (y4'=y4-1) & (x4'=x4+1);
+	[]   (z4>0) & (w4>0) -> out4 	: (z4'=z4-1) & (w4'=w4-1);
+
+endmodule
+
+// reward structures
+
+// tokens in cell1
+rewards "tokens_cell1"
+	true : x1+y1+z1;
+endrewards
+
+// tokens in cell2
+rewards "tokens_cell2"
+	true : x2+y2+z2;
+endrewards
+
+// tokens in cell3
+rewards "tokens_cell3"
+	true : x3+y3+z3;
+endrewards
+
+// tokens in cell4
+rewards "tokens_cell4"
+	true : x4+y4+z4;
+endrewards
+
+// throughput of the system
+rewards "throughput"
+	[in] true : 1;
+endrewards
+

src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp

@@ -396,4 +396,21 @@ namespace {
         EXPECT_NEAR(this->parseNumber("11/15"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
     }
     
+    
+    TYPED_TEST(LraCtmcCslModelCheckerTest, kanban) {
+        std::string formulasString = "R{\"throughput\"}=? [ LRA ]";
+        
+        auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/kanban.prism", formulasString);
+        auto model = std::move(modelFormulas.first);
+        auto tasks = this->getTasks(modelFormulas.second);
+        EXPECT_EQ(160ul, model->getNumberOfStates());
+        EXPECT_EQ(616ul, model->getNumberOfTransitions());
+        ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc);
+        auto checker = this->createModelChecker(model);
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+        
+        result = checker->check(this->env(), tasks[0]);
+        EXPECT_NEAR(this->parseNumber("113237255213395163953677015242972426399989689654967642609491830216061334090202313396984106738516704120069048184391587092670711590526535239899047608853509681914074220789038015289373871985431257486278/1223067474012215838745994023624181143448435715858923491568712969277184634645504346456117443333632535902774869182827010789201972713368729205674432492059242349591780604188152950845769793378621446766887"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+    }
+    
 }