fixed some bugs related to simplifaction of PRISM programs

Former-commit-id: 3c81bcac8d

src/generator/JaniNextStateGenerator.cpp

@@ -161,6 +161,9 @@ namespace storm {
                 }
                 
                 // Block the current initial state to search for the next one.
+                if (!blockingExpression.isInitialized()) {
+                    break;
+                }
                 solver->add(blockingExpression);
             }
             

src/generator/PrismNextStateGenerator.cpp

@@ -23,8 +23,9 @@ namespace storm {
         
         template<typename ValueType, typename StateType>
         PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator<ValueType, StateType>(program.getManager(), options), program(program), rewardModels() {
+            STORM_LOG_TRACE("Creating next-state generator for PRISM program: " << program);
             STORM_LOG_THROW(!this->program.specifiesSystemComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions.");
-            
+                        
             // Only after checking validity of the program, we initialize the variable information.
             this->checkValid(program);
             this->variableInformation = VariableInformation(program);
@@ -166,6 +167,9 @@ namespace storm {
                 initialStateIndices.push_back(id);
                 
                 // Block the current initial state to search for the next one.
+                if (!blockingExpression.isInitialized()) {
+                    break;
+                }
                 solver->add(blockingExpression);
             }
             
@@ -314,7 +318,7 @@ namespace storm {
         template<typename ValueType, typename StateType>
         boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> PrismNextStateGenerator<ValueType, StateType>::getActiveCommandsByActionIndex(uint_fast64_t const& actionIndex) {
             boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> result((std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>()));
-            
+                        
             // Iterate over all modules.
             for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
                 storm::prism::Module const& module = program.getModule(i);
@@ -445,7 +449,6 @@ namespace storm {
                         
                         for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
                             storm::prism::Command const& command = *iteratorList[i];
-                            
                             for (uint_fast64_t j = 0; j < command.getNumberOfUpdates(); ++j) {
                                 storm::prism::Update const& update = command.getUpdate(j);
                                 

src/parser/PrismParser.cpp

@@ -65,6 +65,8 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << lineNumber << " of file " << filename << ".");
             }
             
+            STORM_LOG_TRACE("Parsed PRISM input: " << result);
+            
             return result;
         }
         

src/storage/prism/Module.h

@@ -104,7 +104,6 @@ namespace storm {
              */
             std::set<storm::expressions::Variable> getAllExpressionVariables() const;
             
-            
             /*!
              * Retrieves a list of expressions that characterize the legal ranges of all variables declared by this
              * module.

src/storage/prism/Program.cpp

@@ -734,6 +734,12 @@ namespace storm {
                 }
             }
             
+            // As we possibly delete some commands and some actions might be dropped from modules altogether, we need to
+            // maintain a list of actions that we need to remove in other modules. For example, if module A loses all [a]
+            // commands, we need to delete all [a] commands from all other modules as well. If we do not do that, we will
+            // remove the forced synchronization that was there before.
+            std::set<uint_fast64_t> actionIndicesToDelete;
+            
             // Now we can substitute the constants in all expressions appearing in the program.
             std::vector<BooleanVariable> newBooleanVariables;
             newBooleanVariables.reserve(this->getNumberOfGlobalBooleanVariables());
@@ -757,6 +763,9 @@ namespace storm {
             newModules.reserve(this->getNumberOfModules());
             for (auto const& module : this->getModules()) {
                 newModules.emplace_back(module.substitute(constantSubstitution));
+                
+                // Determine the set of action indices that have been deleted entirely.
+                std::set_difference(module.getSynchronizingActionIndices().begin(), module.getSynchronizingActionIndices().end(), newModules.back().getSynchronizingActionIndices().begin(), newModules.back().getSynchronizingActionIndices().end(), std::inserter(actionIndicesToDelete, actionIndicesToDelete.begin()));
             }
             
             std::vector<RewardModel> newRewardModels;
@@ -773,7 +782,37 @@ namespace storm {
                 newLabels.emplace_back(label.substitute(constantSubstitution));
             }
             
-            return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, this->getActionNameToIndexMapping(), newRewardModels, newLabels, newInitialConstruct, this->getOptionalSystemCompositionConstruct());
+            // If we have to delete whole actions, do so now.
+            std::map<std::string, uint_fast64_t> newActionToIndexMap;
+            if (!actionIndicesToDelete.empty()) {
+                boost::container::flat_set<uint_fast64_t> actionsToKeep;
+                std::set_difference(this->getSynchronizingActionIndices().begin(), this->getSynchronizingActionIndices().end(), actionIndicesToDelete.begin(), actionIndicesToDelete.end(), std::inserter(actionsToKeep, actionsToKeep.begin()));
+                
+                // Insert the silent action as this is not contained in the synchronizing action indices.
+                actionsToKeep.insert(0);
+                
+                std::vector<Module> cleanedModules;
+                cleanedModules.reserve(this->getNumberOfModules());
+                for (auto const& module : newModules) {
+                    cleanedModules.emplace_back(module.restrictCommands(actionsToKeep));
+                }
+                newModules = std::move(cleanedModules);
+                
+                std::vector<RewardModel> cleanedRewardModels;
+                cleanedRewardModels.reserve(this->getNumberOfRewardModels());
+                for (auto const& rewardModel : newRewardModels) {
+                    cleanedRewardModels.emplace_back(rewardModel.restrictActionRelatedRewards(actionsToKeep));
+                }
+                newRewardModels = std::move(cleanedRewardModels);
+                
+                for (auto const& entry : this->getActionNameToIndexMapping()) {
+                    if (actionsToKeep.find(entry.second) != actionsToKeep.end()) {
+                        newActionToIndexMap.emplace(entry.first, entry.second);
+                    }
+                }
+            }
+            
+            return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, actionIndicesToDelete.empty() ? this->getActionNameToIndexMapping() : newActionToIndexMap, newRewardModels, newLabels, newInitialConstruct, this->getOptionalSystemCompositionConstruct());
         }
         
         void Program::checkValidity(Program::ValidityCheckLevel lvl) const {
@@ -1153,17 +1192,19 @@ namespace storm {
         }
         
         Program Program::simplify() {
+            // Start by substituting the constants, because this will potentially erase some commands or even actions.
+            Program substitutedProgram = this->substituteConstants();
+            
             std::vector<Module> newModules;
-            std::vector<Constant> newConstants = this->getConstants();
-            for (auto const& module : this->getModules()) {
-                // Remove identity assignments from the updates
+            std::vector<Constant> newConstants = substitutedProgram.getConstants();
+            for (auto const& module : substitutedProgram.getModules()) {
+                // Remove identity assignments from the updates.
                 std::vector<Command> newCommands;
                 for (auto const& command : module.getCommands()) {
                     newCommands.emplace_back(command.removeIdentityAssignmentsFromUpdates());
                 }
                 
-                // Substitute Variables by Global constants if possible.
-                
+                // Substitute variables by global constants if possible.
                 std::map<storm::expressions::Variable, storm::expressions::Expression> booleanVars;
                 std::map<storm::expressions::Variable, storm::expressions::Expression> integerVars;
                 for (auto const& variable : module.getBooleanVariables()) {
@@ -1179,11 +1220,11 @@ namespace storm {
                         // Check all assignments.
                         for (auto const& assignment : update.getAssignments()) {
                             auto bit = booleanVars.find(assignment.getVariable());
-                            if(bit != booleanVars.end()) {
+                            if (bit != booleanVars.end()) {
                                 booleanVars.erase(bit);
                             } else {
                                 auto iit = integerVars.find(assignment.getVariable());
-                                if(iit != integerVars.end()) {
+                                if (iit != integerVars.end()) {
                                     integerVars.erase(iit);
                                 }
                             }
@@ -1192,31 +1233,30 @@ namespace storm {
                 }
                 
                 std::vector<storm::prism::BooleanVariable> newBVars;
-                for(auto const& variable : module.getBooleanVariables()) {
-                    if(booleanVars.count(variable.getExpressionVariable()) == 0) {
+                for (auto const& variable : module.getBooleanVariables()) {
+                    if (booleanVars.find(variable.getExpressionVariable()) == booleanVars.end()) {
                         newBVars.push_back(variable);
                     }
                 }
                 std::vector<storm::prism::IntegerVariable> newIVars;
-                for(auto const& variable : module.getIntegerVariables()) {
-                    if(integerVars.count(variable.getExpressionVariable()) == 0) {
+                for (auto const& variable : module.getIntegerVariables()) {
+                    if (integerVars.find(variable.getExpressionVariable()) == integerVars.end()) {
                         newIVars.push_back(variable);
                     }
                 }
                 
                 newModules.emplace_back(module.getName(), newBVars, newIVars, newCommands);
                 
-                for(auto const& entry : booleanVars) {
+                for (auto const& entry : booleanVars) {
                     newConstants.emplace_back(entry.first, entry.second);
                 }
                 
-                for(auto const& entry : integerVars) {
+                for (auto const& entry : integerVars) {
                     newConstants.emplace_back(entry.first, entry.second);
                 }
             }
             
-            return replaceModulesAndConstantsInProgram(newModules, newConstants).substituteConstants();
-            
+            return substitutedProgram.replaceModulesAndConstantsInProgram(newModules, newConstants);
         }
         
         Program Program::replaceModulesAndConstantsInProgram(std::vector<Module> const& newModules, std::vector<Constant> const& newConstants) {

src/storage/prism/RewardModel.cpp

@@ -81,6 +81,24 @@ namespace storm {
             return true;
         }
         
+        RewardModel RewardModel::restrictActionRelatedRewards(boost::container::flat_set<uint_fast64_t> const& actionIndicesToKeep) const {
+            std::vector<StateActionReward> newStateActionRewards;
+            for (auto const& stateActionReward : this->getStateActionRewards()) {
+                if (actionIndicesToKeep.find(stateActionReward.getActionIndex()) != actionIndicesToKeep.end()) {
+                    newStateActionRewards.emplace_back(stateActionReward);
+                }
+            }
+
+            std::vector<TransitionReward> newTransitionRewards;
+            for (auto const& transitionReward : this->getTransitionRewards()) {
+                if (actionIndicesToKeep.find(transitionReward.getActionIndex()) != actionIndicesToKeep.end()) {
+                    newTransitionRewards.emplace_back(transitionReward);
+                }
+            }
+
+            return RewardModel(this->getName(), this->getStateRewards(), newStateActionRewards, newTransitionRewards, this->getFilename(), this->getLineNumber());
+        }
+        
         std::ostream& operator<<(std::ostream& stream, RewardModel const& rewardModel) {
             stream << "rewards";
             if (rewardModel.getName() != "") {

src/storage/prism/RewardModel.h

@@ -4,6 +4,7 @@
 #include <string>
 #include <vector>
 #include <map>
+#include <boost/container/flat_set.hpp>
 
 #include "src/storage/prism/StateReward.h"
 #include "src/storage/prism/StateActionReward.h"
@@ -108,6 +109,14 @@ namespace storm {
              */
             bool containsVariablesOnlyInRewardValueExpressions(std::set<storm::expressions::Variable> const& undefinedConstantVariables) const;
             
+            /*!
+             * Restricts all action-related rewards of the reward model to the ones with an action index in the provided set.
+             *
+             * @param actionIndicesToKeep The set of action indices to keep.
+             * @return The resulting reward model.
+             */
+            RewardModel restrictActionRelatedRewards(boost::container::flat_set<uint_fast64_t> const& actionIndicesToKeep) const;
+            
             friend std::ostream& operator<<(std::ostream& stream, RewardModel const& rewardModel);
 
         private:

src/utility/storm.cpp

@@ -10,7 +10,7 @@
 namespace storm {
    
      storm::prism::Program parseProgram(std::string const& path) {
-        storm::prism::Program program= storm::parser::PrismParser::parse(path).simplify().simplify();
+        storm::prism::Program program = storm::parser::PrismParser::parse(path).simplify().simplify();
         program.checkValidity();
         return program;
     }