From bd3c42561b477abcd78fdfc7c07ec925428aa7f4 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 29 Sep 2020 14:02:59 +0200 Subject: [PATCH] Added multi-objective lra test case for MA --- resources/examples/testfiles/ma/polling.ma | 101 ++++++++++++++++++ ...seMaPcaaMultiObjectiveModelCheckerTest.cpp | 41 +++++++ 2 files changed, 142 insertions(+) create mode 100755 resources/examples/testfiles/ma/polling.ma diff --git a/resources/examples/testfiles/ma/polling.ma b/resources/examples/testfiles/ma/polling.ma new file mode 100755 index 000000000..a33e53261 --- /dev/null +++ b/resources/examples/testfiles/ma/polling.ma @@ -0,0 +1,101 @@ +// Translation of the MAPA Specification of a polling system into PRISM code +// http://wwwhome.cs.utwente.nl/~timmer/scoop/papers/qest13/index.html + +ma + +const int N; // number of job types (should be at most 6) +const int Q; // Maximum queue size in each station + +// Formulae to control the LIFO queue of the stations. +// The queue is represented by some integer whose base N representation has at most Q digits, each representing one of the job types 0, 1, ..., N-1. +// In addition, we store the current size of the queue which is needed to distinguish an empty queue from a queue holding job of type 0 +formula queue1_empty = q1Size=0; +formula queue1_full = q1Size=Q; +formula queue1_pop = floor(q1/N); +formula queue1_head = q1 - (queue1_pop * N); // i.e. q1 modulo N +formula queue1_push = q1*N; +formula queue2_empty = q2Size=0; +formula queue2_full = q2Size=Q; +formula queue2_pop = floor(q2/N); +formula queue2_head = q2 - (queue2_pop * N); // i.e. q2 modulo N +formula queue2_push = q2*N; + +const int queue_maxValue = (N^Q)-1; + +const double inRate1 = 3; // = (2 * #station) + 1; +const double inRate2 = 5; // = (2 * #station) + 1; + +module pollingsys + // The queues for the stations + q1 : [0..queue_maxValue]; + q1Size : [0..Q]; + q2 : [0..queue_maxValue]; + q2Size : [0..Q]; + + // Store the job that is currently processed by the server. j=N means that no job is processed. + j : [0..N] init N; + + // Flag indicating whether a new job arrived + newJob1 : bool init false; + newJob2 : bool init false; + + //<> !newJob1 & !newJob2 & !queue1_full & queue2_full & j=N -> inRate1 : (newJob1'=true); + //<> !newJob1 & !newJob2 & queue1_full & !queue2_full & j=N -> inRate2 : (newJob2'=true); + <> !newJob1 & !newJob2 & !queue1_full & !queue2_full & j=N -> inRate1 : (newJob1'=true) + inRate2 : (newJob2'=true); + <> !newJob1 & !newJob2 & queue1_full & queue2_full & j 2*(j+1) : (j'=N); + <> !newJob1 & !newJob2 & !queue1_full & queue2_full & j inRate1 : (newJob1'=true) + 2*(j+1) : (j'=N); + <> !newJob1 & !newJob2 & queue1_full & !queue2_full & j inRate2 : (newJob2'=true) + 2*(j+1) : (j'=N); + <> !newJob1 & !newJob2 & !queue1_full & !queue2_full & j inRate1 : (newJob1'=true) + inRate2 : (newJob2'=true) + 2*(j+1) : (j'=N); + + [] newJob1 & N>=1 -> 1 : (q1Size'=q1Size+1) & (q1'=queue1_push+0) & (newJob1'=false); + [] newJob1 & N>=2 -> 1 : (q1Size'=q1Size+1) & (q1'=queue1_push+1) & (newJob1'=false); + [] newJob1 & N>=3 -> 1 : (q1Size'=q1Size+1) & (q1'=queue1_push+2) & (newJob1'=false); + [] newJob1 & N>=4 -> 1 : (q1Size'=q1Size+1) & (q1'=queue1_push+3) & (newJob1'=false); + [] newJob1 & N>=5 -> 1 : (q1Size'=q1Size+1) & (q1'=queue1_push+4) & (newJob1'=false); + [] newJob1 & N>=6 -> 1 : (q1Size'=q1Size+1) & (q1'=queue1_push+5) & (newJob1'=false); + + [] newJob2 & N>=1 -> 1 : (q2Size'=q2Size+1) & (q2'=queue2_push+0) & (newJob2'=false); + [] newJob2 & N>=2 -> 1 : (q2Size'=q2Size+1) & (q2'=queue2_push+1) & (newJob2'=false); + [] newJob2 & N>=3 -> 1 : (q2Size'=q2Size+1) & (q2'=queue2_push+2) & (newJob2'=false); + [] newJob2 & N>=4 -> 1 : (q2Size'=q2Size+1) & (q2'=queue2_push+3) & (newJob2'=false); + [] newJob2 & N>=5 -> 1 : (q2Size'=q2Size+1) & (q2'=queue2_push+4) & (newJob2'=false); + [] newJob2 & N>=6 -> 1 : (q2Size'=q2Size+1) & (q2'=queue2_push+5) & (newJob2'=false); + + [copy1] !newJob1 & !newJob2 & !queue1_empty & j=N -> 0.9 : (j'=queue1_head) & (q1Size'=q1Size-1) & (q1'=queue1_pop) + 0.1 : (j'=queue1_head); + [copy2] !newJob1 & !newJob2 & !queue2_empty & j=N -> 0.9 : (j'=queue2_head) & (q2Size'=q2Size-1) & (q2'=queue2_pop) + 0.1 : (j'=queue2_head); + +endmodule + + + +label "q1full" = q1Size=Q; +label "q2full" = q2Size=Q; +label "allqueuesfull" = q1Size=Q & q2Size=Q; + + +// Rewards adapted from Guck et al.: Modelling and Analysis of Markov Reward Automata + +rewards "processedjobs1" + [copy1] true : 0.1; +endrewards + +rewards "processedjobs2" + [copy2] true : 0.1; +endrewards + +rewards "processedjobs" + [copy1] true : 0.1; + [copy2] true : 0.1; +endrewards + +rewards "queuesize1" + true : 0.01 * (q1Size); +endrewards + +rewards "queuesize2" + true : 0.01 * (q2Size); +endrewards + +rewards "queuesize" + true : 0.01 * (q1Size + q2Size); +endrewards diff --git a/src/test/storm/modelchecker/multiobjective/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/multiobjective/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp index 80bbd3752..285b45461 100755 --- a/src/test/storm/modelchecker/multiobjective/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/multiobjective/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp @@ -358,6 +358,47 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, simple_lra) { EXPECT_TRUE(expectSubset(convertPointset(expectedPoints), result->asExplicitParetoCurveCheckResult().getPoints(), eps)) << "Pareto point missing."; } } + +TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, polling) { + if (!storm::test::z3AtLeastVersion(4,8,5)) { + GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3."; + } + storm::Environment env; + env.modelchecker().multi().setMethod(storm::modelchecker::multiobjective::MultiObjectiveMethod::Pcaa); + + std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/polling.ma"; + std::string constantsDefStr = "N=1,Q=1"; + std::string formulasAsString = "multi(LRAmin=? [\"q1full\"], LRAmin=? [\"q2full\"]);\n"; // pareto + formulasAsString += "multi(Pmin=? [F<0.1 \"q1full\"], LRAmin=? [\"q1full\"]);\n" ; // pareto + + // programm, model, formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsDefStr); + program.checkValidity(); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + storm::generator::NextStateGeneratorOptions options(formulas); + auto ma = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); + + { + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[0]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); + std::vector> expectedPoints; + expectedPoints.emplace_back(std::vector({"62771/102086","89585/102086"})); + expectedPoints.emplace_back(std::vector({"77531/89546","64985/89546"})); + double eps = 1e-4; + EXPECT_TRUE(expectSubset(result->asExplicitParetoCurveCheckResult().getPoints(), convertPointset(expectedPoints), eps)) << "Non-Pareto point found."; + EXPECT_TRUE(expectSubset(convertPointset(expectedPoints), result->asExplicitParetoCurveCheckResult().getPoints(), eps)) << "Pareto point missing."; + } + { + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[1]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); + std::vector> expectedPoints; + expectedPoints.emplace_back(std::vector({"0.25918177931828","62771/102086"})); + double eps = 1e-4; + EXPECT_TRUE(expectSubset(result->asExplicitParetoCurveCheckResult().getPoints(), convertPointset(expectedPoints), eps)) << "Non-Pareto point found."; + EXPECT_TRUE(expectSubset(convertPointset(expectedPoints), result->asExplicitParetoCurveCheckResult().getPoints(), eps)) << "Pareto point missing."; + } +}