From 6eeae9ed9b683570942f8178f3bb0f100a3f7341 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 10 Jan 2017 12:18:28 +0100 Subject: [PATCH] fixed pcaa tests --- .../examples/testfiles/ma/jobscheduler.ma | 20 +++++++------- .../examples/testfiles/mdp/multiobj_team3.nm | 4 +++ .../pcaa/SparsePcaaPreprocessor.cpp | 2 +- .../SparseMaPcaaModelCheckerTest.cpp | 26 +++++++++---------- .../SparseMdpPcaaModelCheckerTest.cpp | 12 ++++----- 5 files changed, 34 insertions(+), 30 deletions(-) diff --git a/resources/examples/testfiles/ma/jobscheduler.ma b/resources/examples/testfiles/ma/jobscheduler.ma index d83a199f5..68f60fb55 100644 --- a/resources/examples/testfiles/ma/jobscheduler.ma +++ b/resources/examples/testfiles/ma/jobscheduler.ma @@ -5,34 +5,28 @@ // Please cite Quatmann et al: Multi-objective Model Checking of Markov Automata ma -const int x_j1 = 1; -const int x_j2 = 2; -const int x_j3 = 3; +const double x_j1 = 1.0; +const double x_j2 = 2.0; +const double x_j3 = 3.0; formula is_running = r_j1 + r_j2 + r_j3 > 0; formula num_finished = f_j1 + f_j2 + f_j3; module main - r_j1 : [0..1]; r_j2 : [0..1]; r_j3 : [0..1]; f_j1 : [0..1]; f_j2 : [0..1]; f_j3 : [0..1]; - <> (r_j1 = 1) -> x_j1 : (r_j1' = 0) & (r_j2' = 0) & (r_j3' = 0) & (f_j1' = 1); <> (r_j2 = 1) -> x_j2 : (r_j1' = 0) & (r_j2' = 0) & (r_j3' = 0) & (f_j2' = 1); <> (r_j3 = 1) -> x_j3 : (r_j1' = 0) & (r_j2' = 0) & (r_j3' = 0) & (f_j3' = 1); - [] (!is_running) & (num_finished = 2) & (f_j1 = 0) -> 1: (r_j1' = 1); [] (!is_running) & (num_finished = 2) & (f_j2 = 0) -> 1: (r_j2' = 1); [] (!is_running) & (num_finished = 2) & (f_j3 = 0) -> 1: (r_j3' = 1); - [] (!is_running) & (num_finished <= 1) & (f_j1 = 0) & (f_j2 = 0) -> 1: (r_j1' = 1) & (r_j2' = 1); [] (!is_running) & (num_finished <= 1) & (f_j1 = 0) & (f_j3 = 0) -> 1: (r_j1' = 1) & (r_j3' = 1); [] (!is_running) & (num_finished <= 1) & (f_j2 = 0) & (f_j3 = 0) -> 1: (r_j2' = 1) & (r_j3' = 1); - endmodule - init r_j1 = 0 & r_j2 = 0 & @@ -40,4 +34,10 @@ init f_j1 = 0 & f_j2 = 0 & f_j3 = 0 -endinit \ No newline at end of file +endinit +label "all_jobs_finished" = num_finished=3; +label "half_of_jobs_finished" = num_finished=2; +label "slowest_before_fastest" = f_j1=1 & f_j3=0; +rewards "avg_waiting_time" + true : (3-num_finished)/3; +endrewards diff --git a/resources/examples/testfiles/mdp/multiobj_team3.nm b/resources/examples/testfiles/mdp/multiobj_team3.nm index 3c075c204..58a7108b1 100644 --- a/resources/examples/testfiles/mdp/multiobj_team3.nm +++ b/resources/examples/testfiles/mdp/multiobj_team3.nm @@ -271,6 +271,10 @@ formula agent3_joins_successful_team_of_1 = (task1_completed & m3_t1=1 & team_si formula agent3_joins_successful_team_of_2 = (task1_completed & m3_t1=1 & team_size_t1=2) | (task2_completed & m3_t2=1 & team_size_t2=2); formula agent3_joins_successful_team_of_3 = (task1_completed & m3_t1=1 & team_size_t1=3) | (task2_completed & m3_t2=1 & team_size_t2=3); + +label "task1_compl" = task1_completed; +label "task2_compl" = task2_completed; + // rewards rewards "w_1_total" [] agent1_joins_successful_team : 1; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp index 60ac261fb..125e12a1e 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp @@ -314,7 +314,7 @@ namespace storm { template void SparsePcaaPreprocessor::preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, ReturnType& result, PcaaObjective& currentObjective, boost::optional const& optionalRewardModelName) { STORM_LOG_THROW(result.originalModel.isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidPropertyException, "Cumulative reward formulas are not supported for the given model type."); - STORM_LOG_THROW(!formula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Expected a cumulativeRewardFormula with a discrete time bound but got " << formula << "."); + STORM_LOG_THROW(formula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Expected a cumulativeRewardFormula with a discrete time bound but got " << formula << "."); // FIXME: really convert to value type? currentObjective.upperTimeBound = storm::utility::convertNumber(formula.getBound()); diff --git a/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp b/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp index f1025bd6f..5f92999c1 100644 --- a/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp +++ b/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp @@ -26,7 +26,7 @@ TEST(SparseMaPcaaModelCheckerTest, serverRationalNumbers) { // programm, model, formula storm::prism::Program program = storm::parseProgram(programFile); program.checkValidity(); - std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); + std::vector> formulas = storm::extractFormulasFromProperties(parseFormulasForProgram(formulasAsString, program)); storm::generator::NextStateGeneratorOptions options(formulas); std::shared_ptr> ma = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); @@ -55,7 +55,7 @@ TEST(SparseMaPcaaModelCheckerTest, server) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); - std::vector> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> ma = storm::buildSparseModel(program, formulas)->as>(); std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula()); @@ -74,17 +74,17 @@ TEST(SparseMaPcaaModelCheckerTest, server) { EXPECT_TRUE(expectedAchievableValues->minkowskiSum(bloatingBox)->contains(result->asParetoCurveCheckResult().getUnderApproximation()->convertNumberRepresentation())); EXPECT_TRUE(result->asParetoCurveCheckResult().getOverApproximation()->convertNumberRepresentation()->minkowskiSum(bloatingBox)->contains(expectedAchievableValues)); - + } TEST(SparseMaPcaaModelCheckerTest, jobscheduler_pareto_3Obj) { std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma"; - std::string formulasAsString = "multi(Tmin=? [ F num_finished=3 ], Pmax=? [ F<=0.2 num_finished=2 ], Pmin=? [ F f_j1=1 & f_j3=0 ]) "; + std::string formulasAsString = "multi(Tmin=? [ F \"all_jobs_finished\" ], Pmax=? [ F<=0.2 \"half_of_jobs_finished\" ], Pmin=? [ F \"slowest_before_fastest\" ]) "; storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); - std::vector> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> ma = storm::buildSparseModel(program, formulas)->as>(); std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula()); @@ -112,12 +112,12 @@ TEST(SparseMaPcaaModelCheckerTest, jobscheduler_pareto_3Obj) { TEST(SparseMaPcaaModelCheckerTest, jobscheduler_achievability_3Obj) { std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma"; - std::string formulasAsString = "multi(T<=1.31 [ F num_finished=3 ], P>=0.17 [ F<=0.2 num_finished=2 ], P<=0.31 [ F f_j1=1 & f_j3=0 ]) "; //true - formulasAsString += "; multi(T<=1.29 [ F num_finished=3 ], P>=0.18 [ F<=0.2 num_finished=2 ], P<=0.29 [ F f_j1=1 & f_j3=0 ])"; //false + std::string formulasAsString = "multi(T<=1.31 [ F \"all_jobs_finished\" ], P>=0.17 [ F<=0.2 \"half_of_jobs_finished\" ], P<=0.31 [ F \"slowest_before_fastest\" ]) "; //true + formulasAsString += "; multi(T<=1.29 [ F \"all_jobs_finished\" ], P>=0.18 [ F<=0.2 \"half_of_jobs_finished\" ], P<=0.29 [ F \"slowest_before_fastest\" ])"; //false storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); - std::vector> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> ma = storm::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *ma->getInitialStates().begin(); @@ -133,12 +133,12 @@ TEST(SparseMaPcaaModelCheckerTest, jobscheduler_achievability_3Obj) { TEST(SparseMaPcaaModelCheckerTest, jobscheduler_quantitative_3Obj) { std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma"; - std::string formulasAsString = "multi(Tmin=? [ F num_finished=3 ], P>=0.1797900683 [ F<=0.2 num_finished=2 ], P<=0.3 [ F f_j1=1 & f_j3=0 ]) "; //quantitative - formulasAsString += "; multi(T<=1.26 [ F num_finished=3 ], P>=0.2 [ F<=0.2 num_finished=2 ], Pmin=? [ F f_j1=1 & f_j3=0 ])"; //false + std::string formulasAsString = "multi(Tmin=? [ F \"all_jobs_finished\" ], P>=0.1797900683 [ F<=0.2 \"half_of_jobs_finished\" ], P<=0.3 [ F \"slowest_before_fastest\" ]) "; //quantitative + formulasAsString += "; multi(T<=1.26 [ F \"all_jobs_finished\" ], P>=0.2 [ F<=0.2 \"half_of_jobs_finished\" ], Pmin=? [ F \"slowest_before_fastest\" ])"; //false storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); - std::vector> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> ma = storm::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *ma->getInitialStates().begin(); @@ -155,11 +155,11 @@ TEST(SparseMaPcaaModelCheckerTest, jobscheduler_quantitative_3Obj) { TEST(SparseMaPcaaModelCheckerTest, jobscheduler_pareto_2Obj) { std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma"; - std::string formulasAsString = "multi( Pmax=? [ F<=0.1 num_finished=1], Pmin=? [F<=0.2 num_finished=3]) "; + std::string formulasAsString = "multi( Pmax=? [ F<=0.1 num_finished=1], Pmin=? [F<=0.2 \"all_jobs_finished\"]) "; storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); - std::vector> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> ma = storm::buildSparseModel(program, formulas)->as>(); std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula()); diff --git a/src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp b/src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp index c25872e9c..1116997c9 100644 --- a/src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp +++ b/src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp @@ -22,7 +22,7 @@ TEST(SparseMdpPcaaModelCheckerTest, consensus) { // programm, model, formula storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); - std::vector> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin();; @@ -48,7 +48,7 @@ TEST(SparseMdpPcaaModelCheckerTest, zeroconf) { // programm, model, formula storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); - std::vector> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); @@ -60,12 +60,12 @@ TEST(SparseMdpPcaaModelCheckerTest, zeroconf) { TEST(SparseMdpPcaaModelCheckerTest, team3with3objectives) { std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_team3.nm"; - std::string formulasAsString = "multi(Pmax=? [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ], P>=0.5 [ F task2_completed ])"; // numerical + std::string formulasAsString = "multi(Pmax=? [ F \"task1_compl\" ], R{\"w_1_total\"}>=2.210204082 [ C ], P>=0.5 [ F \"task2_compl\" ])"; // numerical // programm, model, formula storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); - std::vector> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); @@ -82,7 +82,7 @@ TEST(SparseMdpPcaaModelCheckerTest, scheduler) { // programm, model, formula storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); - std::vector> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); @@ -98,7 +98,7 @@ TEST(SparseMdpPcaaModelCheckerTest, dpm) { // programm, model, formula storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); - std::vector> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin();