diff --git a/resources/examples/testfiles/ctmc/kanban.prism b/resources/examples/testfiles/ctmc/kanban.prism new file mode 100644 index 000000000..8f5191efb --- /dev/null +++ b/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 in1 : (w1'=w1+1) & (x1'=x1+1); + [] (x1>0) & (y1 redo1 : (x1'=x1-1) & (y1'=y1+1); + [] (x1>0) & (z1 ok1 : (x1'=x1-1) & (z1'=z1+1); + [] (y1>0) & (x1 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 1 : (w2'=w2+1) & (x2'=x2+1); + [] (x2>0) & (y2 redo2 : (x2'=x2-1) & (y2'=y2+1); + [] (x2>0) & (z2 ok2 : (x2'=x2-1) & (z2'=z2+1); + [] (y2>0) & (x2 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 1 : (w3'=w3+1) & (x3'=x3+1); + [] (x3>0) & (y3 redo3 : (x3'=x3-1) & (y3'=y3+1); + [] (x3>0) & (z3 ok3 : (x3'=x3-1) & (z3'=z3+1); + [] (y3>0) & (x3 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 synch234 : (w4'=w4+1) & (x4'=x4+1); + [] (x4>0) & (y4 redo4 : (x4'=x4-1) & (y4'=y4+1); + [] (x4>0) & (z4 ok4 : (x4'=x4-1) & (z4'=z4+1); + [] (y4>0) & (x4 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 + diff --git a/src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp index b8d3b1fc7..f142a764c 100755 --- a/src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp +++ b/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 result; + + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("113237255213395163953677015242972426399989689654967642609491830216061334090202313396984106738516704120069048184391587092670711590526535239899047608853509681914074220789038015289373871985431257486278/1223067474012215838745994023624181143448435715858923491568712969277184634645504346456117443333632535902774869182827010789201972713368729205674432492059242349591780604188152950845769793378621446766887"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + } + }