Refactored preprocess for symbolic input

src/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -36,7 +36,6 @@
 #include "storm/storage/jani/ParallelComposition.h"
 #include "storm/storage/jani/visitor/CompositionInformationVisitor.h"
 #include "storm/utility/macros.h"
-#include "storm/utility/prism.h"
 #include "storm/utility/vector.h"
 
 namespace storm::gbar {

src/storm-parsers/api/properties.cpp

@@ -10,7 +10,7 @@
 #include "storm/storage/jani/Model.h"
 #include "storm/storage/jani/Property.h"
 #include "storm/storage/prism/Program.h"
-#include "storm/utility/cli.h"
+#include "storm/utility/string.h"
 
 namespace storm {
 namespace api {
@@ -19,7 +19,7 @@ boost::optional<std::set<std::string>> parsePropertyFilter(std::string const& pr
     if (propertyFilter == "all") {
         return boost::none;
     }
-    std::vector<std::string> propertyNames = storm::utility::cli::parseCommaSeparatedStrings(propertyFilter);
+    std::vector<std::string> propertyNames = storm::utility::string::parseCommaSeparatedStrings(propertyFilter);
     std::set<std::string> propertyNameSet(propertyNames.begin(), propertyNames.end());
     return propertyNameSet;
 }

src/storm/builder/DdPrismModelBuilder.cpp

@@ -19,7 +19,6 @@
 #include "storm/storage/prism/Compositions.h"
 #include "storm/storage/prism/Program.h"
 #include "storm/utility/dd.h"
-#include "storm/utility/prism.h"
 
 namespace storm {
 namespace builder {

src/storm/builder/ExplicitModelBuilder.h

@@ -21,8 +21,6 @@
 #include "storm/storage/sparse/ModelComponents.h"
 #include "storm/storage/sparse/StateStorage.h"
 
-#include "storm/utility/prism.h"
-
 #include "storm/builder/ExplorationOrder.h"
 
 #include "storm/generator/CompressedState.h"
@@ -33,7 +31,6 @@ namespace storm {
 
 namespace builder {
 
-using namespace storm::utility::prism;
 using namespace storm::generator;
 
 // Forward-declare classes.

src/storm/modelchecker/exploration/SparseExplorationModelChecker.cpp

@@ -29,7 +29,6 @@
 #include "storm/utility/constants.h"
 #include "storm/utility/graph.h"
 #include "storm/utility/macros.h"
-#include "storm/utility/prism.h"
 
 #include "storm/exceptions/InvalidOperationException.h"
 #include "storm/exceptions/InvalidPropertyException.h"

src/storm/storage/SymbolicModelDescription.cpp

@@ -1,14 +1,15 @@
 #include "storm/storage/SymbolicModelDescription.h"
 
-#include "storm/utility/cli.h"
-#include "storm/utility/prism.h"
+#include <boost/algorithm/string.hpp>
 
+#include "storm/adapters/RationalNumberAdapter.h"
+#include "storm/exceptions/InvalidOperationException.h"
+#include "storm/exceptions/InvalidTypeException.h"
+#include "storm/exceptions/WrongFormatException.h"
 #include "storm/storage/jani/Automaton.h"
 #include "storm/storage/jani/Model.h"
 #include "storm/storage/jani/Property.h"
-
-#include "storm/exceptions/InvalidOperationException.h"
-#include "storm/exceptions/InvalidTypeException.h"
+#include "storm/utility/constants.h"
 #include "storm/utility/macros.h"
 
 namespace storm {
@@ -159,30 +160,25 @@ std::pair<SymbolicModelDescription, std::vector<storm::jani::Property>> Symbolic
 }
 
 SymbolicModelDescription SymbolicModelDescription::preprocess(std::string const& constantDefinitionString) const {
-    std::map<storm::expressions::Variable, storm::expressions::Expression> substitution = parseConstantDefinitions(constantDefinitionString);
-    return preprocess(substitution);
+    return this->preprocess(this->parseConstantDefinitions(constantDefinitionString));
 }
 
 SymbolicModelDescription SymbolicModelDescription::preprocess(
     std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) const {
     if (this->isJaniModel()) {
-        storm::jani::Model preparedModel = this->asJaniModel().defineUndefinedConstants(constantDefinitions).substituteConstants();
-        // We intentionally do not eliminate function expressions in jani models at this point because that would also remove the function
-        // declarations from the model. However, those might still be needed to, e.g., process properties that refer to functions.
-        return SymbolicModelDescription(preparedModel);
+        return SymbolicModelDescription(this->asJaniModel().preprocess(constantDefinitions));
     } else if (this->isPrismProgram()) {
-        return SymbolicModelDescription(
-            this->asPrismProgram().defineUndefinedConstants(constantDefinitions).substituteConstantsFormulas().substituteNonStandardPredicates());
+        return SymbolicModelDescription(this->asPrismProgram().preprocess(constantDefinitions));
     }
     return *this;
 }
 
 std::map<storm::expressions::Variable, storm::expressions::Expression> SymbolicModelDescription::parseConstantDefinitions(
     std::string const& constantDefinitionString) const {
     if (this->isJaniModel()) {
-        return storm::utility::cli::parseConstantDefinitionString(this->asJaniModel().getManager(), constantDefinitionString);
+        return parseConstantDefinitionString(this->asJaniModel().getManager(), constantDefinitionString);
     } else {
-        return storm::utility::cli::parseConstantDefinitionString(this->asPrismProgram().getManager(), constantDefinitionString);
+        return parseConstantDefinitionString(this->asPrismProgram().getManager(), constantDefinitionString);
     }
 }
 
@@ -244,5 +240,67 @@ std::ostream& operator<<(std::ostream& out, SymbolicModelDescription::ModelType
     }
     return out;
 }
+
+std::map<storm::expressions::Variable, storm::expressions::Expression> parseConstantDefinitionString(storm::expressions::ExpressionManager const& manager,
+                                                                                                     std::string const& constantDefinitionString) {
+    std::map<storm::expressions::Variable, storm::expressions::Expression> constantDefinitions;
+    std::set<storm::expressions::Variable> definedConstants;
+
+    if (!constantDefinitionString.empty()) {
+        std::vector<std::string> definitions;
+        boost::split(definitions, constantDefinitionString, boost::is_any_of(","));
+        for (auto& definition : definitions) {
+            boost::trim(definition);
+
+            std::size_t positionOfAssignmentOperator = definition.find('=');
+            STORM_LOG_THROW(positionOfAssignmentOperator != std::string::npos, storm::exceptions::WrongFormatException,
+                            "Illegal constant definition string: syntax error.");
+
+            std::string constantName = definition.substr(0, positionOfAssignmentOperator);
+            boost::trim(constantName);
+            std::string value = definition.substr(positionOfAssignmentOperator + 1);
+            boost::trim(value);
+
+            if (manager.hasVariable(constantName)) {
+                auto const& variable = manager.getVariable(constantName);
+                STORM_LOG_THROW(definedConstants.find(variable) == definedConstants.end(), storm::exceptions::WrongFormatException,
+                                "Illegally trying to define constant '" << constantName << "' twice.");
+                definedConstants.insert(variable);
+
+                if (manager.hasVariable(value)) {
+                    auto const& valueVariable = manager.getVariable(value);
+                    STORM_LOG_THROW(
+                        variable.getType() == valueVariable.getType(), storm::exceptions::WrongFormatException,
+                        "Illegally trying to define constant '" << constantName << "' by constant '" << valueVariable.getName() << " of different type.");
+                    constantDefinitions[variable] = valueVariable.getExpression();
+                } else if (variable.hasBooleanType()) {
+                    if (value == "true") {
+                        constantDefinitions[variable] = manager.boolean(true);
+                    } else if (value == "false") {
+                        constantDefinitions[variable] = manager.boolean(false);
+                    } else {
+                        throw storm::exceptions::WrongFormatException() << "Illegal value for boolean constant: " << value << ".";
+                    }
+                } else if (variable.hasIntegerType()) {
+                    int_fast64_t integerValue = std::stoll(value);
+                    constantDefinitions[variable] = manager.integer(integerValue);
+                } else if (variable.hasRationalType()) {
+                    try {
+                        storm::RationalNumber rationalValue = storm::utility::convertNumber<storm::RationalNumber>(value);
+                        constantDefinitions[variable] = manager.rational(rationalValue);
+                    } catch (std::exception& e) {
+                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
+                                        "Illegal constant definition string '" << constantName << "=" << value << "': " << e.what());
+                    }
+                }
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
+                                "Illegal constant definition string: unknown undefined constant '" << constantName << "'.");
+            }
+        }
+    }
+
+    return constantDefinitions;
+}
 }  // namespace storage
 }  // namespace storm

src/storm/storage/SymbolicModelDescription.h

@@ -1,7 +1,10 @@
 #pragma once
 
 #include <boost/variant.hpp>
+#include <map>
 
+#include "storm/storage/expressions/Expression.h"
+#include "storm/storage/expressions/ExpressionManager.h"
 #include "storm/storage/jani/Model.h"
 #include "storm/storage/prism/Program.h"
 
@@ -64,5 +67,13 @@ class SymbolicModelDescription {
 std::ostream& operator<<(std::ostream& out, SymbolicModelDescription const& model);
 
 std::ostream& operator<<(std::ostream& out, SymbolicModelDescription::ModelType const& type);
+
+/*!
+ * Parses a comma-separated string of constant definitions (e.g. "k=5,epsilon=0.01")
+ * into a map from variables to their corresponding expressions.
+ * @throws WrongFormatException if the string is malformed or references unknown constants.
+ */
+std::map<storm::expressions::Variable, storm::expressions::Expression> parseConstantDefinitionString(storm::expressions::ExpressionManager const& manager,
+                                                                                                     std::string const& constantDefinitionString);
 }  // namespace storage
 }  // namespace storm

src/storm/storage/jani/Model.cpp

@@ -2,11 +2,18 @@
 
 #include <algorithm>
 
+#include "storm/exceptions/InvalidArgumentException.h"
+#include "storm/exceptions/InvalidOperationException.h"
+#include "storm/exceptions/InvalidTypeException.h"
+#include "storm/exceptions/NotImplementedException.h"
+#include "storm/exceptions/WrongFormatException.h"
+#include "storm/solver/SmtSolver.h"
+#include "storm/storage/SymbolicModelDescription.h"
 #include "storm/storage/expressions/ExpressionManager.h"
-
-#include "Compositions.h"
+#include "storm/storage/expressions/LinearityCheckVisitor.h"
 #include "storm/storage/jani/Automaton.h"
 #include "storm/storage/jani/AutomatonComposition.h"
+#include "storm/storage/jani/Compositions.h"
 #include "storm/storage/jani/Edge.h"
 #include "storm/storage/jani/EdgeDestination.h"
 #include "storm/storage/jani/Location.h"
@@ -20,21 +27,10 @@
 #include "storm/storage/jani/visitor/CompositionInformationVisitor.h"
 #include "storm/storage/jani/visitor/JSONExporter.h"
 #include "storm/storage/jani/visitor/JaniExpressionSubstitutionVisitor.h"
-
-#include "storm/storage/expressions/LinearityCheckVisitor.h"
-
 #include "storm/utility/combinatorics.h"
-
-#include "storm/exceptions/InvalidArgumentException.h"
-#include "storm/exceptions/InvalidOperationException.h"
-#include "storm/exceptions/InvalidTypeException.h"
-#include "storm/exceptions/NotImplementedException.h"
-#include "storm/exceptions/WrongFormatException.h"
 #include "storm/utility/macros.h"
 #include "storm/utility/vector.h"
 
-#include "storm/solver/SmtSolver.h"
-
 namespace storm {
 namespace jani {
 
@@ -1156,6 +1152,16 @@ Model Model::substituteConstantsFunctionsTranscendentals() const {
     return result;
 }
 
+Model Model::preprocess(std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) const {
+    // We intentionally do not eliminate function expressions in jani models at this point because that would also remove the function
+    // declarations from the model. However, those might still be needed to, e.g., process properties that refer to functions.
+    return this->defineUndefinedConstants(constantDefinitions).substituteConstants();
+}
+
+Model Model::preprocess(std::string const& constantDefinitionString) const {
+    return this->preprocess(storm::storage::parseConstantDefinitionString(this->getManager(), constantDefinitionString));
+}
+
 std::map<storm::expressions::Variable, storm::expressions::Expression> Model::getConstantsSubstitution() const {
     std::map<storm::expressions::Variable, storm::expressions::Expression> result;
 

src/storm/storage/jani/Model.h

@@ -3,6 +3,7 @@
 #include <memory>
 
 #include "Composition.h"
+#include "storm/storage/BoostTypes.h"
 #include "storm/storage/jani/Action.h"
 #include "storm/storage/jani/Automaton.h"
 #include "storm/storage/jani/Constant.h"
@@ -13,8 +14,6 @@
 #include "storm/storage/jani/ModelType.h"
 #include "storm/storage/jani/TemplateEdge.h"
 #include "storm/storage/jani/VariableSet.h"
-
-#include "storm/storage/BoostTypes.h"
 #include "storm/utility/solver.h"
 
 namespace storm {
@@ -429,6 +428,23 @@ class Model {
      */
     Model substituteConstants() const;
 
+    /*!
+     * Preprocesses the model by defining the given constant definitions and substituting constants.
+     *
+     * @param constantDefinitions A mapping from undefined constant to the expressions they are supposed to be replaced with.
+     * @return The preprocessed model.
+     */
+    Model preprocess(std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) const;
+
+    /*!
+     * Preprocesses the model by parsing the given constant definition string, defining the constants,
+     * and substituting constants.
+     *
+     * @param constantDefinitionString A string of constant definitions, e.g., "p=0.5, n=10".
+     * @return The preprocessed model.
+     */
+    Model preprocess(std::string const& constantDefinitionString = "") const;
+
     /*!
      * Retrieves a mapping from expression variables associated with defined constants of the model to their
      * (the constants') defining expression.

src/storm/storage/prism/Program.cpp

@@ -4,27 +4,24 @@
 #include <boost/algorithm/string/join.hpp>
 #include <sstream>
 
-#include "storm/storage/jani/Model.h"
-#include "storm/storage/jani/Property.h"
-
 #include "storm/exceptions/InternalException.h"
 #include "storm/exceptions/InvalidArgumentException.h"
 #include "storm/exceptions/InvalidOperationException.h"
 #include "storm/exceptions/InvalidTypeException.h"
 #include "storm/exceptions/OutOfRangeException.h"
 #include "storm/exceptions/WrongFormatException.h"
 #include "storm/solver/SmtSolver.h"
+#include "storm/storage/SymbolicModelDescription.h"
 #include "storm/storage/expressions/ExpressionManager.h"
+#include "storm/storage/jani/Model.h"
+#include "storm/storage/jani/Property.h"
 #include "storm/storage/jani/visitor/JaniExpressionSubstitutionVisitor.h"
-#include "storm/utility/macros.h"
-#include "storm/utility/solver.h"
-#include "storm/utility/vector.h"
-
 #include "storm/storage/prism/CompositionVisitor.h"
 #include "storm/storage/prism/Compositions.h"
 #include "storm/storage/prism/ToJaniConverter.h"
-
 #include "storm/utility/macros.h"
+#include "storm/utility/solver.h"
+#include "storm/utility/vector.h"
 
 namespace storm {
 namespace prism {
@@ -1162,6 +1159,14 @@ Program Program::substituteConstantsFormulas(bool substituteConstants, bool subs
                    this->getOptionalSystemCompositionConstruct(), prismCompatibility);
 }
 
+Program Program::preprocess(std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) const {
+    return this->defineUndefinedConstants(constantDefinitions).substituteConstantsFormulas().substituteNonStandardPredicates();
+}
+
+Program Program::preprocess(std::string const& constantDefinitionString) const {
+    return this->preprocess(storm::storage::parseConstantDefinitionString(this->getManager(), constantDefinitionString));
+}
+
 Program Program::labelUnlabelledCommands(std::map<uint64_t, std::string> const& nameSuggestions) const {
     for (auto const& entry : nameSuggestions) {
         STORM_LOG_THROW(!hasAction(entry.second), storm::exceptions::InvalidArgumentException, "Cannot suggest names already in the program.");

src/storm/storage/prism/Program.h

@@ -1,5 +1,4 @@
-#ifndef STORM_STORAGE_PRISM_PROGRAM_H_
-#define STORM_STORAGE_PRISM_PROGRAM_H_
+#pragma once
 
 #include <boost/optional.hpp>
 #include <map>
@@ -693,6 +692,24 @@ class Program : public LocatedInformation {
      */
     Program substituteConstantsFormulas(bool substituteConstants = true, bool substituteFormulas = true) const;
 
+    /*!
+     * Preprocesses the program by defining the given constant definitions, substituting constants and formulas,
+     * and substituting non-standard predicates.
+     *
+     * @param constantDefinitions A mapping from undefined constant to the expressions they are supposed to be replaced with.
+     * @return The preprocessed program.
+     */
+    Program preprocess(std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) const;
+
+    /*!
+     * Preprocesses the program by parsing the given constant definition string, defining the constants,
+     * substituting constants and formulas, and substituting non-standard predicates.
+     *
+     * @param constantDefinitionString A string of constant definitions, e.g., "p=0.5, n=10".
+     * @return The preprocessed program.
+     */
+    Program preprocess(std::string const& constantDefinitionString = "") const;
+
     /*!
      * Replace the initialization in variables by an init-expression. This should not change the semantics of the program and can be a preprocessing step.
      *
@@ -903,5 +920,3 @@ std::ostream& operator<<(std::ostream& out, Program::ModelType const& type);
 
 }  // namespace prism
 }  // namespace storm
-
-#endif /* STORM_STORAGE_PRISM_PROGRAM_H_ */