fixes and improvements for the new goal state merger

src/storm/transformer/GoalStateMerger.cpp

@@ -30,7 +30,7 @@ namespace storm {
   
             auto result = initialize(maybeStates, targetStates, sinkStates);
             
-            auto transitionMatrix = buildTransitionMatrix(maybeStates, targetStates, sinkStates, result.first, result.second);
+            auto transitionMatrix = buildTransitionMatrix(maybeStates, result.first, result.second);
             auto labeling = buildStateLabeling(maybeStates, targetStates, sinkStates, result.first);
             auto rewardModels = buildRewardModels(maybeStates, result.first, selectedRewardModels);
             
@@ -169,7 +169,7 @@ namespace storm {
             uint_fast64_t stateCount = maybeStates.getNumberOfSetBits() + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0);
             storm::models::sparse::StateLabeling labeling(stateCount);
             
-            for (auto const& label : originalModel.getLabels()) {
+            for (auto const& label : originalModel.getStateLabeling().getLabels()) {
                 storm::storage::BitVector const& oldStatesWithLabel = originalModel.getStates(label);
                 storm::storage::BitVector newStatesWithLabel = oldStatesWithLabel % maybeStates;
                 newStatesWithLabel.resize(stateCount, false);
@@ -199,19 +199,19 @@ namespace storm {
                 auto origRewardModel = originalModel.getRewardModel(rewardModelName);
                 
                 boost::optional<std::vector<RewardValueType>> stateRewards;
-                if (origRewardModel.hasStateRewards) {
+                if (origRewardModel.hasStateRewards()) {
                     stateRewards = storm::utility::vector::filterVector(origRewardModel.getStateRewardVector(), maybeStates);
                     stateRewards->resize(stateCount, storm::utility::zero<RewardValueType>());
                 }
                 
                 boost::optional<std::vector<RewardValueType>> stateActionRewards;
-                if (origRewardModel.hasStateActionRewards) {
+                if (origRewardModel.hasStateActionRewards()) {
                     stateActionRewards = storm::utility::vector::filterVector(origRewardModel.getStateActionRewardVector(), resultData.keptChoices);
                     stateActionRewards->resize(choiceCount, storm::utility::zero<RewardValueType>());
                 }
                 
                 boost::optional<storm::storage::SparseMatrix<RewardValueType>> transitionRewards;
-                if (origRewardModel.hasTransitionRewards) {
+                if (origRewardModel.hasTransitionRewards()) {
                     storm::storage::SparseMatrixBuilder<RewardValueType> builder(choiceCount, stateCount, 0, true);
                     for (auto const& row : resultData.keptChoices) {
                         boost::optional<typename SparseModelType::ValueType> targetValue, sinkValue;
@@ -256,6 +256,20 @@ namespace storm {
             return std::make_shared<storm::models::sparse::MarkovAutomaton<double>> (std::move(transitionMatrix), std::move(labeling), std::move(markovianStates), std::move(exitRates), true, std::move(rewardModels));
         }
         
+        template <>
+        std::shared_ptr<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>> GoalStateMerger<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>::buildOutputModel(storm::storage::BitVector const& maybeStates, ReturnType const& resultData, storm::storage::SparseMatrix<storm::RationalNumber>&& transitionMatrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map<std::string, typename storm::models::sparse::MarkovAutomaton<storm::RationalNumber>::RewardModelType>&& rewardModels) const {
+            
+            uint_fast64_t stateCount = maybeStates.getNumberOfSetBits() + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0);
+
+            storm::storage::BitVector markovianStates = originalModel.getMarkovianStates() % maybeStates;
+            markovianStates.resize(stateCount, true);
+            
+            std::vector<storm::RationalNumber> exitRates = storm::utility::vector::filterVector(originalModel.getExitRates(), maybeStates);
+            exitRates.resize(stateCount, storm::utility::one<storm::RationalNumber>());
+            
+            return std::make_shared<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>> (std::move(transitionMatrix), std::move(labeling), std::move(markovianStates), std::move(exitRates), true, std::move(rewardModels));
+        }
+        
         template <typename SparseModelType>
         std::shared_ptr<SparseModelType> GoalStateMerger<SparseModelType>::buildOutputModel(storm::storage::BitVector const& maybeStates, GoalStateMerger::ReturnType const& resultData, storm::storage::SparseMatrix<typename SparseModelType::ValueType>&& transitionMatrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map<std::string, typename SparseModelType::RewardModelType>&& rewardModels) const {
             
@@ -267,6 +281,7 @@ namespace storm {
         template class GoalStateMerger<storm::models::sparse::MarkovAutomaton<double>>;
         template class GoalStateMerger<storm::models::sparse::Dtmc<storm::RationalNumber>>;
         template class GoalStateMerger<storm::models::sparse::Mdp<storm::RationalNumber>>;
+        template class GoalStateMerger<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>;
         template class GoalStateMerger<storm::models::sparse::Dtmc<storm::RationalFunction>>;
         template class GoalStateMerger<storm::models::sparse::Mdp<storm::RationalFunction>>;
 

src/storm/transformer/GoalStateMerger.h

@@ -41,6 +41,7 @@ namespace storm {
              *  * Only the selected reward models will be kept. The target and sink states will not get any reward.
              *  * Choices that lead from a maybeState to a ~(target | sink) state will be removed. An exception is thrown if this leads to deadlocks.
              *  * It is assumed that maybeStates, targetStates, and sinkStates are pairwise disjoint. Otherwise an exception is thrown.
+             *  * The order of the maybeStates will not be affected (i.e. s_1 < s_2 in the input model implies s'_1 < s'_2 in the output model).
              */
              ReturnType mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, std::vector<std::string> const& selectedRewardModels = std::vector<std::string>()) const;
             

src/storm/transformer/SparseParametricDtmcSimplifier.cpp

@@ -38,7 +38,7 @@ namespace storm {
             
             // obtain the resulting subsystem
             storm::transformer::GoalStateMerger<SparseModelType> goalStateMerger(this->originalModel);
-            storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult =  goalStateMerger.mergeTargetAndSinkStates(maybeStates, statesWithProbability01.second, statesWithProbability01.first);
+            typename storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult =  goalStateMerger.mergeTargetAndSinkStates(maybeStates, statesWithProbability01.second, statesWithProbability01.first);
             this->simplifiedModel = mergerResult.model;
             statesWithProbability01.second = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false);
             if (mergerResult.targetState) {
@@ -90,7 +90,7 @@ namespace storm {
             
             // obtain the resulting subsystem
             storm::transformer::GoalStateMerger<SparseModelType> goalStateMerger(this->originalModel);
-            storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult =  goalStateMerger.mergeTargetAndSinkStates(maybeStates, prob0States, psiStates);
+            typename storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult =  goalStateMerger.mergeTargetAndSinkStates(maybeStates, prob0States, psiStates);
             this->simplifiedModel = mergerResult.model;
             psiStates = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false);
             if (mergerResult.targetState) {
@@ -132,7 +132,7 @@ namespace storm {
             // obtain the resulting subsystem
             std::vector<std::string> rewardModelNameAsVector(1, formula.hasRewardModelName() ? formula.getRewardModelName() : this->originalModel.getRewardModels().begin()->first);
             storm::transformer::GoalStateMerger<SparseModelType> goalStateMerger(this->originalModel);
-            storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult =  goalStateMerger.mergeTargetAndSinkStates(maybeStates, targetStates, infinityStates, rewardModelNameAsVector);
+            typename storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult =  goalStateMerger.mergeTargetAndSinkStates(maybeStates, targetStates, infinityStates, rewardModelNameAsVector);
             this->simplifiedModel = mergerResult.model;
             targetStates = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false);
             if (mergerResult.targetState) {
@@ -142,7 +142,7 @@ namespace storm {
             while (this->simplifiedModel->hasLabel(targetLabel)) {
                 targetLabel = "_" + targetLabel;
             }
-            this->simplifiedModel->getStateLabeling().addLabel(targetLabel, std::move(psiStates));
+            this->simplifiedModel->getStateLabeling().addLabel(targetLabel, std::move(targetStates));
             
             // obtain the simplified formula for the simplified model
             auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula const> (targetLabel);
@@ -175,7 +175,7 @@ namespace storm {
             // obtain the resulting subsystem
             std::vector<std::string> rewardModelNameAsVector(1, formula.hasRewardModelName() ? formula.getRewardModelName() : this->originalModel.getRewardModels().begin()->first);
             storm::transformer::GoalStateMerger<SparseModelType> goalStateMerger(this->originalModel);
-            storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult =  goalStateMerger.mergeTargetAndSinkStates(maybeStates, noStates, zeroRewardStates, rewardModelNameAsVector);
+            typename storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult =  goalStateMerger.mergeTargetAndSinkStates(maybeStates, noStates, zeroRewardStates, rewardModelNameAsVector);
             this->simplifiedModel = mergerResult.model;
             
             // obtain the simplified formula for the simplified model

src/storm/transformer/SparseParametricMdpSimplifier.cpp

@@ -45,7 +45,7 @@ namespace storm {
             
             // obtain the resulting subsystem
             storm::transformer::GoalStateMerger<SparseModelType> goalStateMerger(this->originalModel);
-            storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult =  goalStateMerger.mergeTargetAndSinkStates(maybeStates, statesWithProbability01.second, statesWithProbability01.first);
+            typename storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult =  goalStateMerger.mergeTargetAndSinkStates(maybeStates, statesWithProbability01.second, statesWithProbability01.first);
             this->simplifiedModel = mergerResult.model;
             statesWithProbability01.second = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false);
             if (mergerResult.targetState) {
@@ -105,7 +105,7 @@ namespace storm {
             
             // obtain the resulting subsystem
             storm::transformer::GoalStateMerger<SparseModelType> goalStateMerger(this->originalModel);
-            storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult =  goalStateMerger.mergeTargetAndSinkStates(maybeStates, prob0States, psiStates);
+            typename storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult =  goalStateMerger.mergeTargetAndSinkStates(maybeStates, prob0States, psiStates);
             this->simplifiedModel = mergerResult.model;
             psiStates = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false);
             if (mergerResult.targetState) {
@@ -154,7 +154,7 @@ namespace storm {
             // obtain the resulting subsystem
             std::vector<std::string> rewardModelNameAsVector(1, formula.hasRewardModelName() ? formula.getRewardModelName() : this->originalModel.getRewardModels().begin()->first);
             storm::transformer::GoalStateMerger<SparseModelType> goalStateMerger(this->originalModel);
-            storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult =  goalStateMerger.mergeTargetAndSinkStates(maybeStates, targetStates, infinityStates, rewardModelNameAsVector);
+            typename storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult =  goalStateMerger.mergeTargetAndSinkStates(maybeStates, targetStates, infinityStates, rewardModelNameAsVector);
             this->simplifiedModel = mergerResult.model;
             targetStates = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false);
             if (mergerResult.targetState) {
@@ -164,7 +164,7 @@ namespace storm {
             while (this->simplifiedModel->hasLabel(targetLabel)) {
                 targetLabel = "_" + targetLabel;
             }
-            this->simplifiedModel->getStateLabeling().addLabel(targetLabel, std::move(psiStates));
+            this->simplifiedModel->getStateLabeling().addLabel(targetLabel, std::move(targetStates));
             
             // obtain the simplified formula for the simplified model
             auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula const> (targetLabel);
@@ -204,7 +204,7 @@ namespace storm {
             // obtain the resulting subsystem
             std::vector<std::string> rewardModelNameAsVector(1, formula.hasRewardModelName() ? formula.getRewardModelName() : this->originalModel.getRewardModels().begin()->first);
             storm::transformer::GoalStateMerger<SparseModelType> goalStateMerger(this->originalModel);
-            storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult =  goalStateMerger.mergeTargetAndSinkStates(maybeStates, noStates, zeroRewardStates, rewardModelNameAsVector);
+            typename storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult =  goalStateMerger.mergeTargetAndSinkStates(maybeStates, noStates, zeroRewardStates, rewardModelNameAsVector);
             this->simplifiedModel = mergerResult.model;
             
             // obtain the simplified formula for the simplified model