more tests on pmdps and fixes

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<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1);
+	[] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1);
+	[] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2);
+	// success
+	[] (s=4) & (i<N) -> (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
+
+

src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp

@@ -29,7 +29,7 @@ namespace storm {
     
             template <typename SparseModelType, typename ConstantType>
             bool SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> 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 <typename SparseModelType, typename ConstantType>

src/storm/storage/FlexibleSparseMatrix.cpp

@@ -234,7 +234,7 @@ namespace storm {
                 oldToNewColumnIndexMapping[oldColumnIndex] = newColumnIndex++;
             }
             
-            storm::storage::SparseMatrixBuilder<ValueType> matrixBuilder(rowConstraint.getNumberOfSetBits(), newColumnIndex, numEntries, true, hasTrivialRowGrouping(), numRowGroups);
+            storm::storage::SparseMatrixBuilder<ValueType> matrixBuilder(rowConstraint.getNumberOfSetBits(), newColumnIndex, numEntries, true, !hasTrivialRowGrouping(), numRowGroups);
             uint_fast64_t currRowIndex = 0;
             auto rowGroupIndexIt = getRowGroupIndices().begin();
             for (auto const& oldRowIndex : rowConstraint) {

src/storm/transformer/GoalStateMerger.cpp

@@ -47,8 +47,9 @@ namespace storm {
             std::unordered_map<std::string, typename SparseModelType::RewardModelType> 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<typename SparseModelType::RewardModelType::ValueType>());
+                auto transitionsOfMaybeStates = originalModel.getTransitionMatrix().getRowIndicesOfRowGroups(maybeStates);
+                auto resTotalRewards = storm::utility::vector::filterVector(origTotalRewards, transitionsOfMaybeStates);
+                resTotalRewards.resize(transitionMatrix.getRowCount(), storm::utility::zero<typename SparseModelType::RewardModelType::ValueType>());
                 rewardModels.insert(std::make_pair(rewardModelName, typename SparseModelType::RewardModelType(boost::none, resTotalRewards)));
             }
                 

src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp

@@ -61,7 +61,6 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew) {
     //start testing
     auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
     auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
-    auto exBothHardRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4", modelParameters); //this region has a local maximum!
     auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::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<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
 
     //start testing
-    auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("", modelParameters);
+    auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::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));
 

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<std::shared_ptr<const storm::logic::Formula>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program));
     std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
@@ -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<std::shared_ptr<const storm::logic::Formula>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program));
+    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
+    
+    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
+    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
+    modelParameters.insert(rewParameters.begin(), rewParameters.end());
+    
+    storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
+    parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
+    
+    //start testing
+    auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters);
+    auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters);
+    auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::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<std::shared_ptr<const storm::logic::Formula>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program));
+    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
+    
+    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
+    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
+    modelParameters.insert(rewParameters.begin(), rewParameters.end());
+    
+    storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
+    parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
+    
+   //start testing
+    auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
+    auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
+    auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::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<std::shared_ptr<const storm::logic::Formula>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program));
+    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
+    
+    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
+    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
+    modelParameters.insert(rewParameters.begin(), rewParameters.end());
+    
+    storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
+    parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
+
+    //start testing
+    auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::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<std::shared_ptr<const storm::logic::Formula>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program));
+    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
+    
+    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
+    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
+    modelParameters.insert(rewParameters.begin(), rewParameters.end());
+    
+    storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*model);
+    parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
+    
+    //start testing
+    auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::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<storm::RationalFunction>::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<storm::RationalFunction>::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