Some work on cli.

Former-commit-id: c3045f48a8

src/builder/ExplicitPrismModelBuilder.cpp

@@ -54,14 +54,46 @@ namespace storm {
             // Intentionally left empty.
         }
 
+
         template <typename ValueType, typename IndexType>
-        std::unique_ptr<storm::models::AbstractModel<ValueType>> ExplicitPrismModelBuilder<ValueType, IndexType>::translateProgram(storm::prism::Program program, bool commandLabels, bool rewards, std::string const& rewardModelName, std::string const& constantDefinitionString) {
-            // Start by defining the undefined constants in the model.
-            // First, we need to parse the constant definition string.
-            std::map<storm::expressions::Variable, storm::expressions::Expression> constantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString);
+        ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options() : buildCommandLabels(false), buildRewards(false), rewardModelName(), constantDefinitions() {
+            // Intentionally left empty.
+        }
+            
+
+        template <typename ValueType, typename IndexType>
+        ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildRewards(false), rewardModelName(), constantDefinitions() {
+            // FIXME: buildRewards should be something like formula.containsRewardOperator()
+            // FIXME: The necessary labels need to be computed properly.
+        }
+
+        template <typename ValueType, typename IndexType>
+        void ExplicitPrismModelBuilder<ValueType, IndexType>::Options::addConstantDefinitionsFromString(storm::prism::Program const& program, std::string const& constantDefinitionString) {
+            std::map<storm::expressions::Variable, storm::expressions::Expression> newConstantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString);
+            
+            // If there is at least one constant that is defined, and the constant definition map does not yet exist,
+            // we need to create it.
+            if (!constantDefinitions && !newConstantDefinitions.empty()) {
+                constantDefinitions = std::map<storm::expressions::Variable, storm::expressions::Expression>();
+            }
             
-            storm::prism::Program preparedProgram = program.defineUndefinedConstants(constantDefinitions);
+            // Now insert all the entries that need to be defined.
+            for (auto const& entry : newConstantDefinitions) {
+                constantDefinitions.get().insert(entry);
+            }
+        }
+        
+        template <typename ValueType, typename IndexType>
+        std::unique_ptr<storm::models::AbstractModel<ValueType>> ExplicitPrismModelBuilder<ValueType, IndexType>::translateProgram(storm::prism::Program program, Options const& options) {
+            // Start by defining the undefined constants in the model.
+            storm::prism::Program preparedProgram;
+            if (options.constantDefinitions) {
+                 preparedProgram = program.defineUndefinedConstants(options.constantDefinitions.get());
+            } else {
+                preparedProgram = program;
+            }
             
+            // If the program still contains undefined constants, assemble an appropriate error message.
             if (preparedProgram.hasUndefinedConstants()) {
                 std::vector<std::reference_wrapper<storm::prism::Constant const>> undefinedConstants = preparedProgram.getUndefinedConstants();
                 std::stringstream stream;
@@ -85,17 +117,19 @@ namespace storm {
             storm::prism::RewardModel rewardModel = storm::prism::RewardModel();
             
             // Select the appropriate reward model.
-            if (rewards) {
+            if (options.buildRewards) {
                 // If a specific reward model was selected or one with the empty name exists, select it.
-                if (rewardModelName != "" || preparedProgram.hasRewardModel(rewardModelName)) {
-                    rewardModel = preparedProgram.getRewardModel(rewardModelName);
+                if (options.rewardModelName) {
+                    rewardModel = preparedProgram.getRewardModel(options.rewardModelName.get());
+                } else if (preparedProgram.hasRewardModel("")) {
+                    rewardModel = preparedProgram.getRewardModel("");
                 } else if (preparedProgram.hasRewardModel()) {
                     // Otherwise, we select the first one.
                     rewardModel = preparedProgram.getRewardModel(0);
                 }
             }
             
-            ModelComponents modelComponents = buildModelComponents(preparedProgram, rewardModel, commandLabels);
+            ModelComponents modelComponents = buildModelComponents(preparedProgram, rewardModel, options.buildCommandLabels);
             
             std::unique_ptr<storm::models::AbstractModel<ValueType>> result;
             switch (program.getModelType()) {

src/builder/ExplicitPrismModelBuilder.h

@@ -14,6 +14,7 @@
 #include "src/storage/expressions/SimpleValuation.h"
 #include "src/storage/expressions/ExprtkExpressionEvaluator.h"
 #include "src/storage/BitVectorHashMap.h"
+#include "src/logic/Formulas.h"
 #include "src/models/AbstractModel.h"
 #include "src/models/AtomicPropositionsLabeling.h"
 #include "src/storage/SparseMatrix.h"
@@ -119,6 +120,42 @@ namespace storm {
                 boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> choiceLabeling;
             };
             
+            struct Options {
+                /*!
+                 * Creates an object representing the default building options.
+                 */
+                Options();
+                
+                /*! Creates an object representing the suggested building options assuming that the given formula is the
+                 * only one to check.
+                 *
+                 * @param formula The formula based on which to choose the building options.
+                 */
+                Options(storm::logic::Formula const& formula);
+                
+                /*!
+                 * Sets the constants definitions from the given string. The string must be of the form 'X=a,Y=b,Z=c',
+                 * etc. where X,Y,Z are the variable names and a,b,c are the values of the constants.
+                 *
+                 * @param program The program managing the constants that shall be defined. Note that the program itself
+                 * is not modified whatsoever.
+                 * @param constantDefinitionString The string from which to parse the constants' values.
+                 */
+                void addConstantDefinitionsFromString(storm::prism::Program const& program, std::string const& constantDefinitionString);
+                
+                // A flag that indicates whether or not command labels are to be built.
+                bool buildCommandLabels;
+                
+                // A flag that indicates whether or not a reward model is to be built.
+                bool buildRewards;
+                
+                // An optional string, that, if given, indicates which of the reward models is to be built.
+                boost::optional<std::string> rewardModelName;
+                
+                // An optional mapping that, if given, contains defining expressions for undefined constants.
+                boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> constantDefinitions;
+            };
+            
             /*!
              * Convert the program given at construction time to an abstract model. The type of the model is the one
              * specified in the program. The given reward model name selects the rewards that the model will contain.
@@ -129,7 +166,7 @@ namespace storm {
              * @param rewardModel The reward model that is to be built.
              * @return The explicit model that was given by the probabilistic program.
              */
-            static std::unique_ptr<storm::models::AbstractModel<ValueType>> translateProgram(storm::prism::Program program, bool commandLabels = false, bool rewards = true, std::string const& rewardModelName = "", std::string const& constantDefinitionString = "");
+            static std::unique_ptr<storm::models::AbstractModel<ValueType>> translateProgram(storm::prism::Program program, Options const& options = Options());
             
         private:
             static void unpackStateIntoEvaluator(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation, storm::expressions::ExprtkExpressionEvaluator& evaluator);

src/logic/AtomicExpressionFormula.cpp

@@ -26,6 +26,10 @@ namespace storm {
             return expression;
         }
         
+        void AtomicExpressionFormula::gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const {
+            atomicExpressionFormulas.push_back(std::dynamic_pointer_cast<AtomicExpressionFormula const>(this->shared_from_this()));
+        }
+            
         std::ostream& AtomicExpressionFormula::writeToStream(std::ostream& out) const {
             out << expression;
             return out;

src/logic/AtomicExpressionFormula.h

@@ -24,6 +24,8 @@ namespace storm {
             
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
+            virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
+            
         private:
             // The atomic expression represented by this node in the formula tree.
             storm::expressions::Expression expression;

src/logic/AtomicLabelFormula.cpp

@@ -26,6 +26,10 @@ namespace storm {
             return label;
         }
         
+        void AtomicLabelFormula::gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicExpressionFormulas) const {
+            atomicExpressionFormulas.push_back(std::dynamic_pointer_cast<AtomicLabelFormula const>(this->shared_from_this()));
+        }
+        
         std::ostream& AtomicLabelFormula::writeToStream(std::ostream& out) const {
             out << "\"" << label << "\"";
             return out;

src/logic/AtomicLabelFormula.h

@@ -23,6 +23,8 @@ namespace storm {
             
             std::string const& getLabel() const;
             
+            virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
+            
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
         private:

src/logic/BinaryPathFormula.cpp

@@ -33,5 +33,13 @@ namespace storm {
         Formula const& BinaryPathFormula::getRightSubformula() const {
             return *rightSubformula;
         }
+        
+        void BinaryPathFormula::gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const {
+            this->getLeftSubformula().gatherAtomicExpressionFormulas(atomicExpressionFormulas);
+        }
+        
+        void BinaryPathFormula::gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const {
+            this->getLeftSubformula().gatherAtomicLabelFormulas(atomicLabelFormulas);
+        }
     }
 }

src/logic/BinaryPathFormula.h

@@ -25,6 +25,9 @@ namespace storm {
             Formula const& getLeftSubformula() const;
             Formula const& getRightSubformula() const;
             
+            virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
+            virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
+            
         private:
             std::shared_ptr<Formula const> leftSubformula;
             std::shared_ptr<Formula const> rightSubformula;

src/logic/BinaryStateFormula.cpp

@@ -33,5 +33,13 @@ namespace storm {
         Formula const& BinaryStateFormula::getRightSubformula() const {
             return *rightSubformula;
         }
+        
+        void BinaryStateFormula::gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const {
+            this->getLeftSubformula().gatherAtomicExpressionFormulas(atomicExpressionFormulas);
+        }
+        
+        void BinaryStateFormula::gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const {
+            this->getLeftSubformula().gatherAtomicLabelFormulas(atomicLabelFormulas);
+        }
     }
 }

src/logic/BinaryStateFormula.h

@@ -23,6 +23,9 @@ namespace storm {
             Formula const& getLeftSubformula() const;
             Formula const& getRightSubformula() const;
             
+            virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
+            virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
+            
         private:
             std::shared_ptr<Formula const> leftSubformula;
             std::shared_ptr<Formula const> rightSubformula;

src/logic/Formula.cpp

@@ -350,6 +350,18 @@ namespace storm {
             return dynamic_cast<RewardOperatorFormula const&>(*this);
         }
         
+        std::vector<std::shared_ptr<AtomicExpressionFormula const>> Formula::getAtomicExpressionFormulas() const {
+            std::vector<std::shared_ptr<AtomicExpressionFormula const>> result;
+            this->gatherAtomicExpressionFormulas(result);
+            return result;
+        }
+        
+        std::vector<std::shared_ptr<AtomicLabelFormula const>> Formula::getAtomicLabelFormulas() const {
+            std::vector<std::shared_ptr<AtomicLabelFormula const>> result;
+            this->gatherAtomicLabelFormulas(result);
+            return result;
+        }
+        
         std::shared_ptr<Formula const> Formula::asSharedPointer() {
             return this->shared_from_this();
         }
@@ -358,6 +370,14 @@ namespace storm {
             return this->shared_from_this();
         }
         
+        void Formula::gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const {
+            return;
+        }
+        
+        void Formula::gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicExpressionFormulas) const {
+            return;
+        }
+        
         std::ostream& operator<<(std::ostream& out, Formula const& formula) {
             return formula.writeToStream(out);
         }

src/logic/Formula.h

@@ -163,11 +163,17 @@ namespace storm {
             RewardOperatorFormula& asRewardOperatorFormula();
             RewardOperatorFormula const& asRewardOperatorFormula() const;
             
+            std::vector<std::shared_ptr<AtomicExpressionFormula const>> getAtomicExpressionFormulas() const;
+            std::vector<std::shared_ptr<AtomicLabelFormula const>> getAtomicLabelFormulas() const;
+            
             std::shared_ptr<Formula const> asSharedPointer();
             std::shared_ptr<Formula const> asSharedPointer() const;
             
             virtual std::ostream& writeToStream(std::ostream& out) const = 0;
             
+            virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const;
+            virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicExpressionFormulas) const;
+            
         private:
             // Currently empty.
         };

src/logic/ReachabilityRewardFormula.cpp

@@ -14,6 +14,14 @@ namespace storm {
             return *subformula;
         }
         
+        void ReachabilityRewardFormula::gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const {
+            this->getSubformula().gatherAtomicExpressionFormulas(atomicExpressionFormulas);
+        }
+        
+        void ReachabilityRewardFormula::gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const {
+            this->getSubformula().gatherAtomicLabelFormulas(atomicLabelFormulas);
+        }
+        
         std::ostream& ReachabilityRewardFormula::writeToStream(std::ostream& out) const {
             out << "F ";
             this->getSubformula().writeToStream(out);

src/logic/ReachabilityRewardFormula.h

@@ -20,6 +20,9 @@ namespace storm {
             
             Formula const& getSubformula() const;
             
+            virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
+            virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
+            
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
         private:

src/logic/UnaryPathFormula.cpp

@@ -29,5 +29,13 @@ namespace storm {
         Formula const& UnaryPathFormula::getSubformula() const {
             return *subformula;
         }
+        
+        void UnaryPathFormula::gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const {
+            this->getSubformula().gatherAtomicExpressionFormulas(atomicExpressionFormulas);
+        }
+        
+        void UnaryPathFormula::gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const {
+            this->getSubformula().gatherAtomicLabelFormulas(atomicLabelFormulas);
+        }
     }
 }

src/logic/UnaryPathFormula.h

@@ -24,6 +24,9 @@ namespace storm {
             
             Formula const& getSubformula() const;
             
+            virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
+            virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
+            
         private:
             std::shared_ptr<Formula const> subformula;
         };

src/logic/UnaryStateFormula.cpp

@@ -33,5 +33,14 @@ namespace storm {
         Formula const& UnaryStateFormula::getSubformula() const {
             return *subformula;
         }
+        
+        void UnaryStateFormula::gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const {
+            this->getSubformula().gatherAtomicExpressionFormulas(atomicExpressionFormulas);
+        }
+        
+        void UnaryStateFormula::gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const {
+            this->getSubformula().gatherAtomicLabelFormulas(atomicLabelFormulas);
+        }
+
     }
 }

src/logic/UnaryStateFormula.h

@@ -23,6 +23,9 @@ namespace storm {
             
             Formula const& getSubformula() const;
             
+            virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
+            virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
+            
         private:
             std::shared_ptr<Formula const> subformula;
         };

src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp

@@ -30,16 +30,10 @@ namespace storm {
         bool SparseDtmcEliminationModelChecker<ValueType>::canHandle(storm::logic::Formula const& formula) const {
             if (formula.isProbabilityOperatorFormula()) {
                 storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula();
-                // The probability operator must not have a bound.
-                if (!probabilityOperatorFormula.hasBound()) {
-                    return this->canHandle(probabilityOperatorFormula.getSubformula());
-                }
+                return this->canHandle(probabilityOperatorFormula.getSubformula());
             } else if (formula.isRewardOperatorFormula()) {
                 storm::logic::RewardOperatorFormula const& rewardOperatorFormula = formula.asRewardOperatorFormula();
-                // The reward operator must not have a bound.
-                if (!rewardOperatorFormula.hasBound()) {
-                    return this->canHandle(rewardOperatorFormula.getSubformula());
-                }
+                return this->canHandle(rewardOperatorFormula.getSubformula());
             } else if (formula.isUntilFormula() || formula.isEventuallyFormula()) {
                 if (formula.isUntilFormula()) {
                     storm::logic::UntilFormula const& untilFormula = formula.asUntilFormula();
@@ -193,6 +187,8 @@ namespace storm {
         
         template<typename ValueType>
         std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<ValueType>::computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+            std::chrono::high_resolution_clock::time_point totalTimeStart = std::chrono::high_resolution_clock::now();
+            
             // Retrieve the appropriate bitvectors by model checking the subformulas.
             STORM_LOG_THROW(pathFormula.getLeftSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Expected 'eventually' formula.");
             STORM_LOG_THROW(pathFormula.getRightSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Expected 'eventually' formula.");
@@ -218,6 +214,7 @@ namespace storm {
             
             // If the initial state is known to have probability 1 of satisfying the condition, we can apply regular model checking.
             if (model.getInitialStates().isSubsetOf(statesWithProbability1)) {
+                STORM_LOG_INFO("The condition holds with probability 1, so the regular reachability probability is computed.");
                 std::shared_ptr<storm::logic::BooleanLiteralFormula> trueFormula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
                 std::shared_ptr<storm::logic::UntilFormula> untilFormula = std::make_shared<storm::logic::UntilFormula>(trueFormula, pathFormula.getLeftSubformula().asSharedPointer());
                 return this->computeUntilProbabilities(*untilFormula);
@@ -276,8 +273,11 @@ namespace storm {
             STORM_LOG_INFO("Computing conditional probilities." << std::endl);
             STORM_LOG_INFO("Eliminating " << states.size() << " states using the state elimination technique." << std::endl);
             boost::optional<std::vector<ValueType>> missingStateRewards;
+            std::chrono::high_resolution_clock::time_point conversionStart = std::chrono::high_resolution_clock::now();
             FlexibleSparseMatrix flexibleMatrix = getFlexibleSparseMatrix(submatrix);
             FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix(submatrixTransposed, true);
+            std::chrono::high_resolution_clock::time_point conversionEnd = std::chrono::high_resolution_clock::now();
+            std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now();
             for (auto const& state : states) {
                 eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions, missingStateRewards);
             }
@@ -373,6 +373,25 @@ namespace storm {
                     numerator += trans1.getValue() * additiveTerm;
                 }
             }
+            std::chrono::high_resolution_clock::time_point modelCheckingEnd = std::chrono::high_resolution_clock::now();
+            std::chrono::high_resolution_clock::time_point totalTimeEnd = std::chrono::high_resolution_clock::now();
+            
+            if (storm::settings::generalSettings().isShowStatisticsSet()) {
+                std::chrono::high_resolution_clock::duration conversionTime = conversionEnd - conversionStart;
+                std::chrono::milliseconds conversionTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(conversionTime);
+                std::chrono::high_resolution_clock::duration modelCheckingTime = modelCheckingEnd - modelCheckingStart;
+                std::chrono::milliseconds modelCheckingTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(modelCheckingTime);
+                std::chrono::high_resolution_clock::duration totalTime = totalTimeEnd - totalTimeStart;
+                std::chrono::milliseconds totalTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(totalTime);
+                
+                STORM_PRINT_AND_LOG(std::endl);
+                STORM_PRINT_AND_LOG("Time breakdown:" << std::endl);
+                STORM_PRINT_AND_LOG("    * time for conversion: " << conversionTimeInMilliseconds.count() << "ms" << std::endl);
+                STORM_PRINT_AND_LOG("    * time for checking: " << modelCheckingTimeInMilliseconds.count() << "ms" << std::endl);
+                STORM_PRINT_AND_LOG("------------------------------------------" << std::endl);
+                STORM_PRINT_AND_LOG("    * total time: " << totalTimeInMilliseconds.count() << "ms" << std::endl);
+                STORM_PRINT_AND_LOG(std::endl);
+            }
             
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(initialState, numerator / denominator));
         }
@@ -395,11 +414,11 @@ namespace storm {
         template<typename ValueType>
         ValueType SparseDtmcEliminationModelChecker<ValueType>::computeReachabilityValue(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional<std::vector<ValueType>>& stateRewards, boost::optional<std::vector<std::size_t>> const& statePriorities) {
             std::chrono::high_resolution_clock::time_point totalTimeStart = std::chrono::high_resolution_clock::now();
-            std::chrono::high_resolution_clock::time_point conversionStart = std::chrono::high_resolution_clock::now();
             
             // Create a bit vector that represents the subsystem of states we still have to eliminate.
             storm::storage::BitVector subsystem = storm::storage::BitVector(transitionMatrix.getRowCount(), true);
             
+            std::chrono::high_resolution_clock::time_point conversionStart = std::chrono::high_resolution_clock::now();
             // Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily.
             FlexibleSparseMatrix flexibleMatrix = getFlexibleSparseMatrix(transitionMatrix);
             FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix(backwardTransitions, true);

src/storage/prism/Program.cpp

@@ -11,7 +11,7 @@
 
 namespace storm {
     namespace prism {
-        Program::Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, bool fixInitialConstruct, storm::prism::InitialConstruct const& initialConstruct, std::vector<Label> const& labels, std::string const& filename, uint_fast64_t lineNumber, bool checkValidity) : LocatedInformation(filename, lineNumber), manager(manager), modelType(modelType), constants(constants), constantToIndexMap(), globalBooleanVariables(globalBooleanVariables), globalBooleanVariableToIndexMap(), globalIntegerVariables(globalIntegerVariables), globalIntegerVariableToIndexMap(), formulas(formulas), formulaToIndexMap(), modules(modules), moduleToIndexMap(), rewardModels(rewardModels), rewardModelToIndexMap(), initialConstruct(initialConstruct), labels(labels), labelToIndexMap(), actionToIndexMap(actionToIndexMap), actions(), actionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap() {
+        Program::Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, bool fixInitialConstruct, storm::prism::InitialConstruct const& initialConstruct, std::vector<Label> const& labels, std::string const& filename, uint_fast64_t lineNumber, bool checkValidity) : LocatedInformation(filename, lineNumber), manager(manager), modelType(modelType), constants(constants), constantToIndexMap(), globalBooleanVariables(globalBooleanVariables), globalBooleanVariableToIndexMap(), globalIntegerVariables(globalIntegerVariables), globalIntegerVariableToIndexMap(), formulas(formulas), formulaToIndexMap(), modules(modules), moduleToIndexMap(), rewardModels(rewardModels), rewardModelToIndexMap(), initialConstruct(initialConstruct), labels(labels), actionToIndexMap(actionToIndexMap), actions(), actionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap() {
             this->createMappings();
             
             // Create a new initial construct if the corresponding flag was set.
@@ -204,6 +204,31 @@ namespace storm {
             return this->getLabels().size();
         }
         
+        void Program::addLabel(std::string const& name, storm::expressions::Expression const& statePredicateExpression) {
+            auto it = std::find_if(this->labels.begin(), this->labels.end(), [&name] (storm::prism::Label const& label) { return label.getName() == name; });
+            STORM_LOG_THROW(it == this->labels.end(), storm::exceptions::InvalidArgumentException, "Cannot add a label '" << name << "', because a label with that name already exists.");
+            this->labels.emplace_back(name, statePredicateExpression);
+        }
+
+        void Program::removeLabel(std::string const& name) {
+            auto it = std::find_if(this->labels.begin(), this->labels.end(), [&name] (storm::prism::Label const& label) { return label.getName() == name; });
+            STORM_LOG_THROW(it != this->labels.end(), storm::exceptions::InvalidArgumentException, "Canno remove unknown label '" << name << "'.");
+            this->labels.erase(it);
+        }
+        
+        void Program::filterLabels(std::set<std::string> const& labelSet) {
+            std::vector<storm::prism::Label> newLabels;
+            newLabels.reserve(labelSet.size());
+            
+            // Now filter the labels by the criterion whether or not their name appears in the given label set.
+            for (auto it = labels.begin(), ite = labels.end(); it != ite; ++it) {
+                auto setIt = labelSet.find(it->getName());
+                if (setIt != labelSet.end()) {
+                    newLabels.emplace_back(*it);
+                }
+            }
+        }
+        
         Program Program::restrictCommands(boost::container::flat_set<uint_fast64_t> const& indexSet) const {
             std::vector<storm::prism::Module> newModules;
             newModules.reserve(this->getNumberOfModules());
@@ -235,9 +260,6 @@ namespace storm {
             for (uint_fast64_t rewardModelIndex = 0; rewardModelIndex < this->getNumberOfRewardModels(); ++rewardModelIndex) {
                 this->rewardModelToIndexMap[this->getRewardModels()[rewardModelIndex].getName()] = rewardModelIndex;
             }
-            for (uint_fast64_t labelIndex = 0; labelIndex < this->getNumberOfLabels(); ++labelIndex) {
-                this->labelToIndexMap[this->getLabels()[labelIndex].getName()] = labelIndex;
-            }
             
             for (auto const& actionIndexPair : this->getActionNameToIndexMapping()) {
                 this->actions.insert(actionIndexPair.first);

src/storage/prism/Program.h

@@ -310,6 +310,29 @@ namespace storm {
              */
             std::size_t getNumberOfLabels() const;
 
+            /*!
+             * Adds a label with the given name and defining expression to the program.
+             *
+             * @param name The name of the label. This name must not yet exist as a label name in the program.
+             * @param statePredicateExpression The predicate that is described by the label.
+             */
+            void addLabel(std::string const& name, storm::expressions::Expression const& statePredicateExpression);
+            
+            /*!
+             * Removes the label with the given name from the program.
+             *
+             * @param name The name of a label that exists within the program.
+             */
+            void removeLabel(std::string const& name);
+            
+            /*!
+             * Removes all labels that are not contained in the given set from the program. Note: no check is performed
+             * as to whether or not the given label names actually exist.
+             *
+             * @param labelSet The label set that is to be kept.
+             */
+            void filterLabels(std::set<std::string> const& labelSet);
+            
             /*!
              * Creates a new program that drops all commands whose indices are not in the given set.
              *
@@ -409,9 +432,6 @@ namespace storm {
             // The labels that are defined for this model.
             std::vector<Label> labels;
             
-            // A mapping from label names to their corresponding indices.
-            std::map<std::string, uint_fast64_t> labelToIndexMap;
-            
             // A mapping from action names to their indices.
             std::map<std::string, uint_fast64_t> actionToIndexMap;
             

src/utility/cli.h

@@ -252,68 +252,65 @@ namespace storm {
             }
             
             template<typename ValueType>
-            std::shared_ptr<storm::models::AbstractModel<ValueType>> buildModel() {
+            std::shared_ptr<storm::models::AbstractModel<ValueType>> buildExplicitModel(std::string const& transitionsFile, std::string const& labelingFile, boost::optional<std::string> const& stateRewardsFile = boost::optional<std::string>(), boost::optional<std::string> const& transitionRewardsFile = boost::optional<std::string>()) {
+                return storm::parser::AutoParser::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "");
+            }
+            
+            template<typename ValueType>
+            std::shared_ptr<storm::models::AbstractModel<ValueType>> buildSymbolicModel(storm::prism::Program const& program, boost::optional<std::shared_ptr<storm::logic::Formula>> const& formula) {
                 std::shared_ptr<storm::models::AbstractModel<ValueType>> result(nullptr);
                 
                 storm::settings::modules::GeneralSettings settings = storm::settings::generalSettings();
 
-                if (settings.isExplicitSet()) {
-                    std::string const transitionFile = settings.getTransitionFilename();
-                    std::string const labelingFile = settings.getLabelingFilename();
-                    
-                    // Parse (and therefore build) the model.
-                    result = storm::parser::AutoParser::parseModel(transitionFile, labelingFile, settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : "", settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : "");
-                } else if (settings.isSymbolicSet()) {
-                    std::string const programFile = settings.getSymbolicModelFilename();
-                    std::string const constants = settings.getConstantDefinitionString();
-                    
-                    // Start by parsing the symbolic model file.
-                    storm::prism::Program program = storm::parser::PrismParser::parse(programFile);
-                    
-                    // Then, build the model from the symbolic description.
-                    result = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, storm::settings::counterexampleGeneratorSettings().isMinimalCommandSetGenerationSet(), true, settings.isSymbolicRewardModelNameSet() ? settings.getSymbolicRewardModelName() : "", constants);
-                } else {
-                    STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
+                // Get the string that assigns values to the unknown currently undefined constants in the model.
+                std::string constants = settings.getConstantDefinitionString();
+                
+                bool buildRewards = false;
+                if (formula) {
+                    buildRewards = formula.get()->isRewardOperatorFormula() || formula.get()->isRewardPathFormula();
                 }
                 
-                // Print some information about the model.
-                result->printModelInformationToStream(std::cout);
+                // Customize model-building.
+                typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
+                if (formula) {
+                    options = storm::builder::ExplicitPrismModelBuilder<double>::Options(*formula.get());
+                } else {
+                    options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString());
+                }
                 
-                if (settings.isBisimulationSet()) {
-                    STORM_LOG_THROW(result->getType() == storm::models::DTMC, storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only compatible with DTMCs.");
-                    std::shared_ptr<storm::models::Dtmc<double>> dtmc = result->template as<storm::models::Dtmc<double>>();
+                // Then, build the model from the symbolic description.
+                result = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
+                return result;
+            }
+            
+            template<typename ValueType>
+            std::shared_ptr<storm::models::AbstractModel<ValueType>> preprocessModel(std::shared_ptr<storm::models::AbstractModel<ValueType>> model, boost::optional<std::shared_ptr<storm::logic::Formula>> const& formula) {
+                if (storm::settings::generalSettings().isBisimulationSet()) {
+                    STORM_LOG_THROW(model->getType() == storm::models::DTMC, storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs.");
+                    std::shared_ptr<storm::models::Dtmc<double>> dtmc = model->template as<storm::models::Dtmc<double>>();
                     
-                    STORM_PRINT(std::endl << "Performing bisimulation minimization..." << std::endl);
+                    std::cout << "Performing bisimulation minimization... ";
                     storm::storage::DeterministicModelBisimulationDecomposition<double> bisimulationDecomposition(*dtmc, boost::optional<std::set<std::string>>(), true, storm::settings::bisimulationSettings().isWeakBisimulationSet(), true);
-                    
-                    result = bisimulationDecomposition.getQuotient();
-                    
-                    STORM_PRINT_AND_LOG(std::endl << "Model after minimization:" << std::endl);
-                    result->printModelInformationToStream(std::cout);
+                    model = bisimulationDecomposition.getQuotient();
+                    std::cout << "done." << std::endl << std::endl;
                 }
-                
-                return result;
+                return model;
             }
             
-            void generateCounterexample(std::shared_ptr<storm::models::AbstractModel<double>> model, std::shared_ptr<storm::logic::Formula> const& formula) {
+            void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::AbstractModel<double>> model, std::shared_ptr<storm::logic::Formula> const& formula) {
                 if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandSetGenerationSet()) {
                     STORM_LOG_THROW(model->getType() == storm::models::MDP, storm::exceptions::InvalidTypeException, "Minimal command set generation is only available for MDPs.");
                     STORM_LOG_THROW(storm::settings::generalSettings().isSymbolicSet(), storm::exceptions::InvalidSettingsException, "Minimal command set generation is only available for symbolic models.");
                     
                     std::shared_ptr<storm::models::Mdp<double>> mdp = model->as<storm::models::Mdp<double>>();
 
-                    // FIXME: do not re-parse the program.
-                    std::string const programFile = storm::settings::generalSettings().getSymbolicModelFilename();
-                    std::string const constants = storm::settings::generalSettings().getConstantDefinitionString();
-                    storm::prism::Program program = storm::parser::PrismParser::parse(programFile);
-
                     // Determine whether we are required to use the MILP-version or the SAT-version.
                     bool useMILP = storm::settings::counterexampleGeneratorSettings().isUseMilpBasedMinimalCommandSetGenerationSet();
 
                     if (useMILP) {
                         storm::counterexamples::MILPMinimalLabelSetGenerator<double>::computeCounterexample(program, *mdp, formula);
                     } else {
-                        storm::counterexamples::SMTMinimalCommandSetGenerator<double>::computeCounterexample(program, constants, *mdp, formula);
+                        storm::counterexamples::SMTMinimalCommandSetGenerator<double>::computeCounterexample(program, storm::settings::generalSettings().getConstantDefinitionString(), *mdp, formula);
                     }
 
                 } else {
@@ -324,30 +321,59 @@ namespace storm {
             void processOptions() {
                 storm::settings::modules::GeneralSettings settings = storm::settings::generalSettings();
                 
-                // Start by parsing/building the model.
-                std::shared_ptr<storm::models::AbstractModel<double>> model = buildModel<double>();
+                // If we have to build the model from a symbolic representation, we need to parse the representation first.
+                boost::optional<storm::prism::Program> program;
+                if (settings.isSymbolicSet()) {
+                    std::string const& programFile = settings.getSymbolicModelFilename();
+                    program = storm::parser::PrismParser::parse(programFile);
+                }
+                
+                // Then proceed to parsing the property (if given), since the model we are building may depend on the property.
+                boost::optional<std::shared_ptr<storm::logic::Formula>> formula;
+                if (settings.isPropertySet()) {
+                    if (program) {
+                        storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer());
+                        formula = formulaParser.parseFromString(settings.getProperty());
+                    } else {
+                        storm::parser::FormulaParser formulaParser;
+                        formula = formulaParser.parseFromString(settings.getProperty());
+                    }
+                }
+                
+                // Now we are ready to actually build the model.
+                std::shared_ptr<storm::models::AbstractModel<double>> model;
+                if (settings.isExplicitSet()) {
+                    model = buildExplicitModel<double>(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::optional<std::string>(), settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::optional<std::string>());
+                } else if (settings.isSymbolicSet()) {
+                    STORM_LOG_THROW(program, storm::exceptions::InvalidStateException, "Program has not been successfully parsed.");
+                    model = buildSymbolicModel<double>(program.get(), formula);
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
+                }
+                
+                // Now, we can do the preprocessing on the model, if it was requested.
+                model = preprocessModel(model, formula);
+
+                // Print some information about the model.
+                model->printModelInformationToStream(std::cout);
                 
                 // If we were requested to generate a counterexample, we now do so.
                 if (settings.isCounterexampleSet()) {
                     STORM_LOG_THROW(settings.isPropertySet(), storm::exceptions::InvalidSettingsException, "Unable to generate counterexample without a property.");
-                    storm::parser::FormulaParser formulaParser;
-                    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseFromString(settings.getProperty());
-                    generateCounterexample(model, formula);
-                } else if (settings.isPropertySet()) {
-                    storm::parser::FormulaParser formulaParser;
-                    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseFromString(storm::settings::generalSettings().getProperty());
-                    
-                    std::cout << "Model checking property: " << *formula << " ...";
+                    STORM_LOG_THROW(program, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for non-symbolic model.");
+                    generateCounterexample(program.get(), model, formula.get());
+                } else if (formula) {
+                    std::cout << std::endl << "Model checking property: " << *formula.get() << " ...";
                     std::unique_ptr<storm::modelchecker::CheckResult> result;
                     if (model->getType() == storm::models::DTMC) {
                         std::shared_ptr<storm::models::Dtmc<double>> dtmc = model->as<storm::models::Dtmc<double>>();
 //                        storm::modelchecker::SparseDtmcPrctlModelChecker<double> modelchecker(*dtmc);
                         storm::modelchecker::SparseDtmcEliminationModelChecker<double> modelchecker(*dtmc);
-                        result = modelchecker.check(*formula);
+                        result = modelchecker.check(*formula.get());
                     } else if (model->getType() == storm::models::MDP) {
                         std::shared_ptr<storm::models::Mdp<double>> mdp = model->as<storm::models::Mdp<double>>();
                         storm::modelchecker::SparseMdpPrctlModelChecker<double> modelchecker(*mdp);
-                        result = modelchecker.check(*formula);
+                        result = modelchecker.check(*formula.get());
                     }
                     if (result) {
                         std::cout << " done." << std::endl;