From 24bc53549cddb4fcc2e2ba3c7940830db8005d2a Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 13 Mar 2017 18:49:30 +0100 Subject: [PATCH] more tests on pmdps and fixes --- resources/examples/testfiles/pmdp/brp16_2.nm | 148 ++++++++++++++++++ .../testfiles/pmdp/{coin2_2.pm => coin2_2.nm} | 0 .../SparseMdpParameterLiftingModelChecker.cpp | 2 +- src/storm/storage/FlexibleSparseMatrix.cpp | 2 +- src/storm/transformer/GoalStateMerger.cpp | 5 +- .../SparseDtmcParameterLiftingTest.cpp | 3 +- .../SparseMdpParameterLiftingTest.cpp | 126 ++++++++++++++- 7 files changed, 277 insertions(+), 9 deletions(-) create mode 100644 resources/examples/testfiles/pmdp/brp16_2.nm rename resources/examples/testfiles/pmdp/{coin2_2.pm => coin2_2.nm} (100%) diff --git a/resources/examples/testfiles/pmdp/brp16_2.nm b/resources/examples/testfiles/pmdp/brp16_2.nm new file mode 100644 index 000000000..33ac0c7c4 --- /dev/null +++ b/resources/examples/testfiles/pmdp/brp16_2.nm @@ -0,0 +1,148 @@ +// bounded retransmission protocol [D'AJJL01] +// gxn/dxp 23/05/2001 +// Modified by Ernst Moritz Hahn (emh@cs.uni-sb.de) + +mdp +//dtmc + +// number of chunks +const int N = 16; +// maximum number of retransmissions +const int MAX = 2; + +// reliability of channels +const double pL; +const double pK; + +// timeouts +const double TOMsg; +const double TOAck; + +module sender + + s : [0..6]; + // 0 idle + // 1 next_frame + // 2 wait_ack + // 3 retransmit + // 4 success + // 5 error + // 6 wait sync + srep : [0..3]; + // 0 bottom + // 1 not ok (nok) + // 2 do not know (dk) + // 3 ok (ok) + nrtr : [0..MAX]; + i : [0..N]; + bs : bool; + s_ab : bool; + fs : bool; + ls : bool; + + // idle + [NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0); + // next_frame + [aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0); + // wait_ack + [aB] (s=2) -> (s'=4) & (s_ab'=!s_ab); + [TO_Msg] (s=2) -> (s'=3); + [TO_Ack] (s=2) -> (s'=3); + // retransmit + [aF] (s=3) & (nrtr (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); + [] (s=3) & (nrtr=MAX) & (i (s'=5) & (srep'=1); + [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); + // success + [] (s=4) & (i (s'=1) & (i'=i+1); + [] (s=4) & (i=N) -> (s'=0) & (srep'=3); + // error + [SyncWait] (s=5) -> (s'=6); + // wait sync + [SyncWait] (s=6) -> (s'=0) & (s_ab'=false); + +endmodule + +module receiver + + r : [0..5]; + // 0 new_file + // 1 fst_safe + // 2 frame_received + // 3 frame_reported + // 4 idle + // 5 resync + rrep : [0..4]; + // 0 bottom + // 1 fst + // 2 inc + // 3 ok + // 4 nok + fr : bool; + lr : bool; + br : bool; + r_ab : bool; + recv : bool; + + + // new_file + [SyncWait] (r=0) -> (r'=0); + [aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); + // fst_safe_frame + [] (r=1) -> (r'=2) & (r_ab'=br); + // frame_received + [] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1); + [] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2); + [] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3); + [aA] (r=2) & !(r_ab=br) -> (r'=4); + // frame_reported + [aA] (r=3) -> (r'=4) & (r_ab'=!r_ab); + // idle + [aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); + [SyncWait] (r=4) & (ls=true) -> (r'=5); + [SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4); + // resync + [SyncWait] (r=5) -> (r'=0) & (rrep'=0); + +endmodule + +module checker + + T : bool init false; + + [NewFile] (T=false) -> (T'=false); + [NewFile] (T=false) -> (T'=true); + +endmodule + +module channelK + + k : [0..2]; + + // idle + [aF] (k=0) -> pK : (k'=1) + 1-pK : (k'=2); + // sending + [aG] (k=1) -> (k'=0); + // lost + [TO_Msg] (k=2) -> (k'=0); + +endmodule + +module channelL + + l : [0..2]; + + // idle + [aA] (l=0) -> pL : (l'=1) + 1-pL : (l'=2); + // sending + [aB] (l=1) -> (l'=0); + // lost + [TO_Ack] (l=2) -> (l'=0); + +endmodule + +rewards + [TO_Msg] true : TOMsg; + [TO_Ack] true : TOAck; +endrewards + + diff --git a/resources/examples/testfiles/pmdp/coin2_2.pm b/resources/examples/testfiles/pmdp/coin2_2.nm similarity index 100% rename from resources/examples/testfiles/pmdp/coin2_2.pm rename to resources/examples/testfiles/pmdp/coin2_2.nm diff --git a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp index 4410adf55..e8bcb9256 100644 --- a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp @@ -29,7 +29,7 @@ namespace storm { template bool SparseMdpParameterLiftingModelChecker::canHandle(CheckTask const& checkTask) const { - return checkTask.getFormula().isInFragment(storm::logic::reachability().setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true)); + return checkTask.getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true)); } template diff --git a/src/storm/storage/FlexibleSparseMatrix.cpp b/src/storm/storage/FlexibleSparseMatrix.cpp index 1b3534eee..ef8ccf72d 100644 --- a/src/storm/storage/FlexibleSparseMatrix.cpp +++ b/src/storm/storage/FlexibleSparseMatrix.cpp @@ -234,7 +234,7 @@ namespace storm { oldToNewColumnIndexMapping[oldColumnIndex] = newColumnIndex++; } - storm::storage::SparseMatrixBuilder matrixBuilder(rowConstraint.getNumberOfSetBits(), newColumnIndex, numEntries, true, hasTrivialRowGrouping(), numRowGroups); + storm::storage::SparseMatrixBuilder matrixBuilder(rowConstraint.getNumberOfSetBits(), newColumnIndex, numEntries, true, !hasTrivialRowGrouping(), numRowGroups); uint_fast64_t currRowIndex = 0; auto rowGroupIndexIt = getRowGroupIndices().begin(); for (auto const& oldRowIndex : rowConstraint) { diff --git a/src/storm/transformer/GoalStateMerger.cpp b/src/storm/transformer/GoalStateMerger.cpp index 5238404b9..f7ccc7f19 100644 --- a/src/storm/transformer/GoalStateMerger.cpp +++ b/src/storm/transformer/GoalStateMerger.cpp @@ -47,8 +47,9 @@ namespace storm { std::unordered_map rewardModels; for (auto rewardModelName : selectedRewardModels) { auto origTotalRewards = originalModel.getRewardModel(rewardModelName).getTotalRewardVector(originalModel.getTransitionMatrix()); - auto resTotalRewards = storm::utility::vector::filterVector(origTotalRewards, maybeStates); - resTotalRewards.resize(resNumStates, storm::utility::zero()); + auto transitionsOfMaybeStates = originalModel.getTransitionMatrix().getRowIndicesOfRowGroups(maybeStates); + auto resTotalRewards = storm::utility::vector::filterVector(origTotalRewards, transitionsOfMaybeStates); + resTotalRewards.resize(transitionMatrix.getRowCount(), storm::utility::zero()); rewardModels.insert(std::make_pair(rewardModelName, typename SparseModelType::RewardModelType(boost::none, resTotalRewards))); } diff --git a/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp b/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp index a892fa4b8..a7adb5d22 100644 --- a/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp +++ b/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp @@ -61,7 +61,6 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew) { //start testing auto allSatRegion=storm::storage::ParameterRegion::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters); auto exBothRegion=storm::storage::ParameterRegion::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters); - auto exBothHardRegion=storm::storage::ParameterRegion::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4", modelParameters); //this region has a local maximum! auto allVioRegion=storm::storage::ParameterRegion::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters); EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, parameterLiftingContext.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true)); @@ -91,7 +90,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Infty) { parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask(*formulas[0], true)); //start testing - auto allSatRegion=storm::storage::ParameterRegion::parseRegion("", modelParameters); + auto allSatRegion=storm::storage::ParameterRegion::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters); EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, parameterLiftingContext.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true)); diff --git a/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp b/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp index 3e12c1074..cda3867bd 100644 --- a/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp +++ b/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp @@ -41,11 +41,9 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob) { TEST(SparseMdpParameterLiftingTest, coin_Prob) { - std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/coin2_2.pm"; + std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/coin2_2.nm"; std::string formulaAsString = "P>0.25 [F \"finished\"&\"all_coins_equal_1\" ]"; - carl::VariablePool::getInstance().clear(); - storm::prism::Program program = storm::parseProgram(programFile); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); @@ -69,4 +67,126 @@ TEST(SparseMdpParameterLiftingTest, coin_Prob) { carl::VariablePool::getInstance().clear(); } +TEST(SparseMdpParameterLiftingTest, brp_Prop) { + + std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm"; + std::string formulaAsString = "P<=0.84 [ F (s=5 & T) ]"; + std::string constantsAsString = "TOMsg=0.0,TOAck=0.0"; + + storm::prism::Program program = storm::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + storm::modelchecker::parametric::ParameterLifting, double> parameterLiftingContext(*model); + parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask(*formulas[0], true)); + + //start testing + auto allSatRegion=storm::storage::ParameterRegion::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters); + auto exBothRegion=storm::storage::ParameterRegion::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters); + auto allVioRegion=storm::storage::ParameterRegion::parseRegion("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters); + + EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, parameterLiftingContext.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, parameterLiftingContext.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, parameterLiftingContext.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true)); + + carl::VariablePool::getInstance().clear(); +} + +TEST(SparseMdpParameterLiftingTest, brp_Rew) { + + std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm"; + std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]"; + std::string constantsAsString = "pL=0.9,TOAck=0.5"; + + + storm::prism::Program program = storm::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + storm::modelchecker::parametric::ParameterLifting, double> parameterLiftingContext(*model); + parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask(*formulas[0], true)); + + //start testing + auto allSatRegion=storm::storage::ParameterRegion::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters); + auto exBothRegion=storm::storage::ParameterRegion::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters); + auto allVioRegion=storm::storage::ParameterRegion::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters); + + EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, parameterLiftingContext.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, parameterLiftingContext.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, parameterLiftingContext.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true)); + + carl::VariablePool::getInstance().clear(); +} + + +TEST(SparseMdpParameterLiftingTest, Brp_Rew_Infty) { + + std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm"; + std::string formulaAsString = "R>2.5 [F (s=0&srep=3) ]"; + std::string constantsAsString = ""; + carl::VariablePool::getInstance().clear(); + storm::prism::Program program = storm::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + storm::modelchecker::parametric::ParameterLifting, double> parameterLiftingContext(*model); + parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask(*formulas[0], true)); + + //start testing + auto allSatRegion=storm::storage::ParameterRegion::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters); + + EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, parameterLiftingContext.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true)); + + carl::VariablePool::getInstance().clear(); +} + +TEST(SparseMdpParameterLiftingTest, Brp_Rew_4Par) { + + std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm"; + std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]"; + std::string constantsAsString = ""; //!! this model will have 4 parameters + carl::VariablePool::getInstance().clear(); + storm::prism::Program program = storm::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + storm::modelchecker::parametric::ParameterLifting, double> parameterLiftingContext(*model); + parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask(*formulas[0], true)); + + //start testing + auto allSatRegion=storm::storage::ParameterRegion::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters); + auto exBothRegion=storm::storage::ParameterRegion::parseRegion("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9", modelParameters); + auto allVioRegion=storm::storage::ParameterRegion::parseRegion("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2", modelParameters); + + EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, parameterLiftingContext.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, parameterLiftingContext.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, parameterLiftingContext.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true)); + + carl::VariablePool::getInstance().clear(); +} + + + + + #endif