Browse Source

Added multi-objective lra test case for MA

tempestpy_adaptions
Tim Quatmann 4 years ago
parent
commit
bd3c42561b
  1. 101
      resources/examples/testfiles/ma/polling.ma
  2. 41
      src/test/storm/modelchecker/multiobjective/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp

101
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<N -> 2*(j+1) : (j'=N);
<> !newJob1 & !newJob2 & !queue1_full & queue2_full & j<N -> inRate1 : (newJob1'=true) + 2*(j+1) : (j'=N);
<> !newJob1 & !newJob2 & queue1_full & !queue2_full & j<N -> inRate2 : (newJob2'=true) + 2*(j+1) : (j'=N);
<> !newJob1 & !newJob2 & !queue1_full & !queue2_full & j<N -> 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

41
src/test/storm/modelchecker/multiobjective/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp

@ -358,6 +358,47 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, simple_lra) {
EXPECT_TRUE(expectSubset(convertPointset<double>(expectedPoints), result->asExplicitParetoCurveCheckResult<double>().getPoints(), eps)) << "Pareto point missing."; EXPECT_TRUE(expectSubset(convertPointset<double>(expectedPoints), result->asExplicitParetoCurveCheckResult<double>().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<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
storm::generator::NextStateGeneratorOptions options(formulas);
auto ma = storm::builder::ExplicitModelBuilder<double>(program, options).build()->as<storm::models::sparse::MarkovAutomaton<double>>();
{
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[0]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
std::vector<std::vector<std::string>> expectedPoints;
expectedPoints.emplace_back(std::vector<std::string>({"62771/102086","89585/102086"}));
expectedPoints.emplace_back(std::vector<std::string>({"77531/89546","64985/89546"}));
double eps = 1e-4;
EXPECT_TRUE(expectSubset(result->asExplicitParetoCurveCheckResult<double>().getPoints(), convertPointset<double>(expectedPoints), eps)) << "Non-Pareto point found.";
EXPECT_TRUE(expectSubset(convertPointset<double>(expectedPoints), result->asExplicitParetoCurveCheckResult<double>().getPoints(), eps)) << "Pareto point missing.";
}
{
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[1]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
std::vector<std::vector<std::string>> expectedPoints;
expectedPoints.emplace_back(std::vector<std::string>({"0.25918177931828","62771/102086"}));
double eps = 1e-4;
EXPECT_TRUE(expectSubset(result->asExplicitParetoCurveCheckResult<double>().getPoints(), convertPointset<double>(expectedPoints), eps)) << "Non-Pareto point found.";
EXPECT_TRUE(expectSubset(convertPointset<double>(expectedPoints), result->asExplicitParetoCurveCheckResult<double>().getPoints(), eps)) << "Pareto point missing.";
}
}

Loading…
Cancel
Save