diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 042eaea43..244e24057 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -204,7 +204,7 @@ if(USE_CARL) LOG_INSTALL ON ) - add_dependencies(resources xercesc) + add_dependencies(resources carl) include_directories(${STORM_3RDPARTY_BINARY_DIR}/carl/include) list(APPEND STORM_LINK_LIBRARIES ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl${DYNAMIC_EXT}) set(STORM_HAVE_CARL ON) diff --git a/src/adapters/AddExpressionAdapter.cpp b/src/adapters/AddExpressionAdapter.cpp index e50620db8..2f0dc7190 100644 --- a/src/adapters/AddExpressionAdapter.cpp +++ b/src/adapters/AddExpressionAdapter.cpp @@ -194,8 +194,8 @@ namespace storm { } template - boost::any AddExpressionAdapter::visit(storm::expressions::DoubleLiteralExpression const& expression) { - return ddManager->getConstant(static_cast(expression.getValue())); + boost::any AddExpressionAdapter::visit(storm::expressions::RationalLiteralExpression const& expression) { + return ddManager->getConstant(static_cast(expression.getValueAsDouble())); } // Explicitly instantiate the symbolic expression adapter diff --git a/src/adapters/AddExpressionAdapter.h b/src/adapters/AddExpressionAdapter.h index 89d825d96..dfb13a315 100644 --- a/src/adapters/AddExpressionAdapter.h +++ b/src/adapters/AddExpressionAdapter.h @@ -31,7 +31,7 @@ namespace storm { virtual boost::any visit(storm::expressions::UnaryNumericalFunctionExpression const& expression) override; virtual boost::any visit(storm::expressions::BooleanLiteralExpression const& expression) override; virtual boost::any visit(storm::expressions::IntegerLiteralExpression const& expression) override; - virtual boost::any visit(storm::expressions::DoubleLiteralExpression const& expression) override; + virtual boost::any visit(storm::expressions::RationalLiteralExpression const& expression) override; private: // The manager responsible for the DDs built by this adapter. diff --git a/src/adapters/MathsatExpressionAdapter.h b/src/adapters/MathsatExpressionAdapter.h index 9fec0cf15..77b39cc68 100644 --- a/src/adapters/MathsatExpressionAdapter.h +++ b/src/adapters/MathsatExpressionAdapter.h @@ -171,8 +171,8 @@ namespace storm { return expression.getValue() ? msat_make_true(env) : msat_make_false(env); } - virtual boost::any visit(expressions::DoubleLiteralExpression const& expression) override { - return msat_make_number(env, std::to_string(expression.getValue()).c_str()); + virtual boost::any visit(expressions::RationalLiteralExpression const& expression) override { + return msat_make_number(env, std::to_string(expression.getValueAsDouble()).c_str()); } virtual boost::any visit(expressions::IntegerLiteralExpression const& expression) override { diff --git a/src/adapters/Z3ExpressionAdapter.cpp b/src/adapters/Z3ExpressionAdapter.cpp index 60b4e8e1c..a80355422 100644 --- a/src/adapters/Z3ExpressionAdapter.cpp +++ b/src/adapters/Z3ExpressionAdapter.cpp @@ -177,6 +177,8 @@ namespace storm { return ite(leftResult <= rightResult, leftResult, rightResult); case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Max: return ite(leftResult >= rightResult, leftResult, rightResult); + case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Power: + return pw(leftResult,rightResult); default: STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Cannot evaluate expression: unknown numerical binary operator '" << static_cast(expression.getOperatorType()) << "' in expression " << expression << "."); } @@ -208,7 +210,7 @@ namespace storm { return context.bool_val(expression.getValue()); } - boost::any Z3ExpressionAdapter::visit(storm::expressions::DoubleLiteralExpression const& expression) { + boost::any Z3ExpressionAdapter::visit(storm::expressions::RationalLiteralExpression const& expression) { std::stringstream fractionStream; fractionStream << expression.getValue(); return context.real_val(fractionStream.str().c_str()); diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h index 4fc60c8a5..2735f5713 100644 --- a/src/adapters/Z3ExpressionAdapter.h +++ b/src/adapters/Z3ExpressionAdapter.h @@ -63,7 +63,7 @@ namespace storm { virtual boost::any visit(storm::expressions::BooleanLiteralExpression const& expression) override; - virtual boost::any visit(storm::expressions::DoubleLiteralExpression const& expression) override; + virtual boost::any visit(storm::expressions::RationalLiteralExpression const& expression) override; virtual boost::any visit(storm::expressions::IntegerLiteralExpression const& expression) override; diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index a397b0de0..6c495e15c 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -1415,7 +1415,7 @@ namespace storm { template storm::dd::Bdd DdPrismModelBuilder::createInitialStatesDecisionDiagram(GenerationInformation& generationInfo) { - storm::dd::Bdd initialStates = generationInfo.rowExpressionAdapter->translateExpression(generationInfo.program.getInitialConstruct().getInitialStatesExpression()).toBdd(); + storm::dd::Bdd initialStates = generationInfo.rowExpressionAdapter->translateExpression(generationInfo.program.getInitialStatesExpression()).toBdd(); for (auto const& metaVariable : generationInfo.rowMetaVariables) { initialStates &= generationInfo.manager->getRange(metaVariable); diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index 44ebb71ec..64665a8fc 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -628,7 +628,7 @@ namespace storm { } // Construct an expression that exactly characterizes the initial state. - storm::expressions::Expression initialStateExpression = program.getInitialConstruct().getInitialStatesExpression(); + storm::expressions::Expression initialStateExpression = program.getInitialStatesExpression(); // Store the found implications in a container similar to the preceding label sets. std::map, std::set>> backwardImplications; diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index cfb08fb79..0b2fad41a 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/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); } diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp index c0026a98d..6e1aeafdb 100644 --- a/src/generator/PrismNextStateGenerator.cpp +++ b/src/generator/PrismNextStateGenerator.cpp @@ -23,8 +23,9 @@ namespace storm { template PrismNextStateGenerator::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator(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); @@ -136,7 +137,7 @@ namespace storm { for (auto const& expression : rangeExpressions) { solver->add(expression); } - solver->add(program.getInitialConstruct().getInitialStatesExpression()); + solver->add(program.getInitialStatesExpression()); // Proceed ss long as the solver can still enumerate initial states. std::vector initialStateIndices; @@ -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 boost::optional>>> PrismNextStateGenerator::getActiveCommandsByActionIndex(uint_fast64_t const& actionIndex) { boost::optional>>> result((std::vector>>())); - + // 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); diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp index 616dcf828..660906acb 100644 --- a/src/modelchecker/AbstractModelChecker.cpp +++ b/src/modelchecker/AbstractModelChecker.cpp @@ -17,6 +17,7 @@ #include "src/models/symbolic/Mdp.h" #include "src/models/sparse/MarkovAutomaton.h" #include "src/models/sparse/StandardRewardModel.h" +#include "src/models/symbolic/StandardRewardModel.h" #include "src/storage/dd/Add.h" #include "src/storage/dd/Bdd.h" diff --git a/src/parser/ExpressionParser.cpp b/src/parser/ExpressionParser.cpp index 20982bd20..3054f2fe0 100644 --- a/src/parser/ExpressionParser.cpp +++ b/src/parser/ExpressionParser.cpp @@ -3,6 +3,34 @@ #include "src/exceptions/InvalidTypeException.h" #include "src/exceptions/WrongFormatException.h" +#include "src/utility/constants.h" + +namespace boost { + namespace spirit { + namespace traits { + template<> + bool scale(int exp, storm::RationalNumber& r, storm::RationalNumber acc) { + if (exp >= 0) { + r = acc * storm::utility::pow(storm::RationalNumber(10), static_cast(exp)); + } else { + r = acc / storm::utility::pow(storm::RationalNumber(10), static_cast(-exp)); + } + return true; + } + + template<> + bool is_equal_to_one(storm::RationalNumber const& value) { + return storm::utility::isOne(value); + } + + template<> + storm::RationalNumber negate(bool neg, storm::RationalNumber const& number) { + return neg ? storm::RationalNumber(-number) : number; + } + } + } +} + namespace storm { namespace parser { ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols const& invalidIdentifiers_, bool enableErrorHandling, bool allowBacktracking) : ExpressionParser::base_type(expression), orOperator_(), andOperator_(), equalityOperator_(), relationalOperator_(), plusOperator_(), multiplicationOperator_(), infixPowerOperator_(), unaryOperator_(), floorCeilOperator_(), minMaxOperator_(), prefixPowerOperator_(), trueFalse_(manager), manager(manager.getSharedPointer()), createExpressions(false), acceptDoubleLiterals(true), identifiers_(nullptr), invalidIdentifiers_(invalidIdentifiers_) { @@ -33,7 +61,7 @@ namespace storm { identifierExpression = identifier[qi::_val = phoenix::bind(&ExpressionParser::getIdentifierExpression, phoenix::ref(*this), qi::_1, allowBacktracking, qi::_pass)]; identifierExpression.name("identifier expression"); - literalExpression = trueFalse_[qi::_val = qi::_1] | strict_double[qi::_val = phoenix::bind(&ExpressionParser::createDoubleLiteralExpression, phoenix::ref(*this), qi::_1, qi::_pass)] | qi::int_[qi::_val = phoenix::bind(&ExpressionParser::createIntegerLiteralExpression, phoenix::ref(*this), qi::_1, qi::_pass)]; + literalExpression = trueFalse_[qi::_val = qi::_1] | rationalLiteral_[qi::_val = phoenix::bind(&ExpressionParser::createRationalLiteralExpression, phoenix::ref(*this), qi::_1, qi::_pass)] | qi::int_[qi::_val = phoenix::bind(&ExpressionParser::createIntegerLiteralExpression, phoenix::ref(*this), qi::_1, qi::_pass)]; literalExpression.name("literal expression"); atomicExpression = floorCeilExpression | prefixPowerExpression | minMaxExpression | (qi::lit("(") >> expression >> qi::lit(")")) | literalExpression | identifierExpression; @@ -295,7 +323,7 @@ namespace storm { return manager->boolean(false); } - storm::expressions::Expression ExpressionParser::createDoubleLiteralExpression(double value, bool& pass) const { + storm::expressions::Expression ExpressionParser::createRationalLiteralExpression(storm::RationalNumber const& value, bool& pass) const { // If we are not supposed to accept double expressions, we reject it by setting pass to false. if (!this->acceptDoubleLiterals) { pass = false; diff --git a/src/parser/ExpressionParser.h b/src/parser/ExpressionParser.h index 66d851707..077be8db2 100644 --- a/src/parser/ExpressionParser.h +++ b/src/parser/ExpressionParser.h @@ -8,8 +8,20 @@ #include "src/storage/expressions/Expression.h" #include "src/storage/expressions/ExpressionManager.h" +#include "src/adapters/CarlAdapter.h" + namespace storm { namespace parser { + template + struct RationalPolicies : boost::spirit::qi::strict_real_policies { + static const bool expect_dot = true; + + template + static bool parse_nan(It&, It const&, Attr&) { return false; } + template + static bool parse_inf(It&, It const&, Attr&) { return false; } + }; + class ExpressionParser : public qi::grammar { public: /*! @@ -236,7 +248,7 @@ namespace storm { qi::rule identifier; // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser). - boost::spirit::qi::real_parser> strict_double; + boost::spirit::qi::real_parser> rationalLiteral_; // Helper functions to create expressions. storm::expressions::Expression createIteExpression(storm::expressions::Expression e1, storm::expressions::Expression e2, storm::expressions::Expression e3, bool& pass) const; @@ -248,7 +260,7 @@ namespace storm { storm::expressions::Expression createMultExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const; storm::expressions::Expression createPowerExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const; storm::expressions::Expression createUnaryExpression(boost::optional const& operatorType, storm::expressions::Expression const& e1, bool& pass) const; - storm::expressions::Expression createDoubleLiteralExpression(double value, bool& pass) const; + storm::expressions::Expression createRationalLiteralExpression(storm::RationalNumber const& value, bool& pass) const; storm::expressions::Expression createIntegerLiteralExpression(int value, bool& pass) const; storm::expressions::Expression createMinimumMaximumExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const; storm::expressions::Expression createFloorCeilExpression(storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e1, bool& pass) const; diff --git a/src/parser/JaniParser.h b/src/parser/JaniParser.h index 82165b5ef..80b4ca0d7 100644 --- a/src/parser/JaniParser.h +++ b/src/parser/JaniParser.h @@ -42,7 +42,8 @@ namespace storm { storm::jani::Property parseProperty(json const& propertyStructure); storm::jani::Automaton parseAutomaton(json const& automatonStructure, storm::jani::Model const& parentModel); std::shared_ptr parseVariable(json const& variableStructure, std::string const& scopeDescription, bool prefWithScope = false); - storm::expressions::Expression parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map> const& localVars = {}); + storm::expressions::Expression parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map> const& localVars = std::unordered_map>()); + private: std::shared_ptr parseConstant(json const& constantStructure, std::string const& scopeDescription = "global"); diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index 7d54f18c6..d3e5191e2 100644 --- a/src/parser/PrismParser.cpp +++ b/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; } @@ -103,10 +105,10 @@ namespace storm { formulaDefinition = (qi::lit("formula") > identifier > qi::lit("=") > expressionParser > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createFormula, phoenix::ref(*this), qi::_1, qi::_2)]; formulaDefinition.name("formula definition"); - booleanVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("bool")) > ((qi::lit("init") > expressionParser) | qi::attr(manager->boolean(false))) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createBooleanVariable, phoenix::ref(*this), qi::_1, qi::_2)]; + booleanVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("bool")) > -((qi::lit("init") > expressionParser[qi::_a = qi::_1]) | qi::attr(manager->boolean(false))) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createBooleanVariable, phoenix::ref(*this), qi::_1, qi::_a)]; booleanVariableDefinition.name("boolean variable definition"); - integerVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("[")[phoenix::bind(&PrismParser::allowDoubleLiterals, phoenix::ref(*this), false)]) > expressionParser[qi::_a = qi::_1] > qi::lit("..") > expressionParser > qi::lit("]")[phoenix::bind(&PrismParser::allowDoubleLiterals, phoenix::ref(*this), true)] > -(qi::lit("init") > expressionParser[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createIntegerVariable, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_a)]; + integerVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("[")[phoenix::bind(&PrismParser::allowDoubleLiterals, phoenix::ref(*this), false)]) > expressionParser > qi::lit("..") > expressionParser > qi::lit("]")[phoenix::bind(&PrismParser::allowDoubleLiterals, phoenix::ref(*this), true)] > -(qi::lit("init") > expressionParser[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createIntegerVariable, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_a)]; integerVariableDefinition.name("integer variable definition"); variableDefinition = (booleanVariableDefinition[phoenix::push_back(qi::_r1, qi::_1)] | integerVariableDefinition[phoenix::push_back(qi::_r2, qi::_1)]); @@ -208,7 +210,7 @@ namespace storm { moduleDefinitionList %= +(moduleRenaming(qi::_r1) | moduleDefinition(qi::_r1))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::modules, qi::_r1), qi::_1)]; moduleDefinitionList.name("module list"); - start = (qi::eps + start = (qi::eps[phoenix::bind(&PrismParser::removeInitialConstruct, phoenix::ref(*this), qi::_a)] > modelTypeDefinition[phoenix::bind(&GlobalProgramInformation::modelType, qi::_a) = qi::_1] > *(definedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_a), qi::_1)] | undefinedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_a), qi::_1)] @@ -276,7 +278,7 @@ namespace storm { return true; } - bool PrismParser::addInitialStatesConstruct(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation) { + bool PrismParser::addInitialStatesConstruct(storm::expressions::Expression const& initialStatesExpression, GlobalProgramInformation& globalProgramInformation) { STORM_LOG_THROW(!globalProgramInformation.hasInitialConstruct, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Program must not define two initial constructs."); if (globalProgramInformation.hasInitialConstruct) { return false; @@ -585,7 +587,7 @@ namespace storm { auto const& renamingPair = renaming.find(variable.getName()); STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Boolean variable '" << variable.getName() << " was not renamed."); - booleanVariables.push_back(storm::prism::BooleanVariable(manager->getVariable(renamingPair->second), variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1))); + booleanVariables.push_back(storm::prism::BooleanVariable(manager->getVariable(renamingPair->second), variable.hasInitialValue() ? variable.getInitialValueExpression().substitute(expressionRenaming) : variable.getInitialValueExpression(), this->getFilename(), get_line(qi::_1))); } // Rename the integer variables. @@ -594,7 +596,7 @@ namespace storm { auto const& renamingPair = renaming.find(variable.getName()); STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Integer variable '" << variable.getName() << " was not renamed."); - integerVariables.push_back(storm::prism::IntegerVariable(manager->getVariable(renamingPair->second), variable.getLowerBoundExpression().substitute(expressionRenaming), variable.getUpperBoundExpression().substitute(expressionRenaming), variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1))); + integerVariables.push_back(storm::prism::IntegerVariable(manager->getVariable(renamingPair->second), variable.getLowerBoundExpression().substitute(expressionRenaming), variable.getUpperBoundExpression().substitute(expressionRenaming), variable.hasInitialValue() ? variable.getInitialValueExpression().substitute(expressionRenaming) : variable.getInitialValueExpression(), this->getFilename(), get_line(qi::_1))); } // Rename commands. @@ -640,7 +642,11 @@ namespace storm { } storm::prism::Program PrismParser::createProgram(GlobalProgramInformation const& globalProgramInformation) const { - return storm::prism::Program(manager, globalProgramInformation.modelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.actionIndices, globalProgramInformation.rewardModels, globalProgramInformation.labels, secondRun && !globalProgramInformation.hasInitialConstruct ? boost::none : boost::optional(storm::prism::InitialConstruct(manager->boolean(false))), globalProgramInformation.systemCompositionConstruct, this->getFilename(), 1, this->secondRun); + return storm::prism::Program(manager, globalProgramInformation.modelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.actionIndices, globalProgramInformation.rewardModels, globalProgramInformation.labels, secondRun && !globalProgramInformation.hasInitialConstruct ? boost::none : boost::make_optional(globalProgramInformation.initialConstruct), globalProgramInformation.systemCompositionConstruct, this->getFilename(), 1, this->secondRun); + } + + void PrismParser::removeInitialConstruct(GlobalProgramInformation& globalProgramInformation) const { + globalProgramInformation.hasInitialConstruct = false; } } // namespace parser } // namespace storm diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index 84a5b601e..2a83e3193 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -188,7 +188,7 @@ namespace storm { // Rules for variable definitions. qi::rule&, std::vector&), Skipper> variableDefinition; - qi::rule booleanVariableDefinition; + qi::rule, Skipper> booleanVariableDefinition; qi::rule, Skipper> integerVariableDefinition; // Rules for command definitions. @@ -241,7 +241,7 @@ namespace storm { // Helper methods used in the grammar. bool isValidIdentifier(std::string const& identifier); - bool addInitialStatesConstruct(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation); + bool addInitialStatesConstruct(storm::expressions::Expression const& initialStatesExpression, GlobalProgramInformation& globalProgramInformation); bool addSystemCompositionConstruct(std::shared_ptr const& composition, GlobalProgramInformation& globalProgramInformation); @@ -274,6 +274,8 @@ namespace storm { storm::prism::Module createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map const& renaming, GlobalProgramInformation& globalProgramInformation) const; storm::prism::Program createProgram(GlobalProgramInformation const& globalProgramInformation) const; + void removeInitialConstruct(GlobalProgramInformation& globalProgramInformation) const; + // An error handler function. phoenix::function handler; }; diff --git a/src/settings/modules/CoreSettings.cpp b/src/settings/modules/CoreSettings.cpp index b42a301c8..5a6dfc9c0 100644 --- a/src/settings/modules/CoreSettings.cpp +++ b/src/settings/modules/CoreSettings.cpp @@ -30,7 +30,6 @@ namespace storm { const std::string CoreSettings::engineOptionShortName = "e"; const std::string CoreSettings::ddLibraryOptionName = "ddlib"; const std::string CoreSettings::cudaOptionName = "cuda"; - const std::string CoreSettings::minMaxEquationSolvingTechniqueOptionName = "ndmethod"; CoreSettings::CoreSettings() : ModuleSettings(moduleName), engine(CoreSettings::Engine::Sparse) { this->addOption(storm::settings::OptionBuilder(moduleName, counterexampleOptionName, false, "Generates a counterexample for the given PRCTL formulas if not satisfied by the model") @@ -57,10 +56,6 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an SMT solver. Available are: z3 and mathsat.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(smtSolvers)).setDefaultValueString("z3").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, statisticsOptionName, false, "Sets whether to display statistics if available.").setShortName(statisticsOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, cudaOptionName, false, "Sets whether to use CUDA to speed up computation time.").build()); - - std::vector minMaxSolvingTechniques = {"vi", "value-iteration", "pi", "policy-iteration"}; - this->addOption(storm::settings::OptionBuilder(moduleName, minMaxEquationSolvingTechniqueOptionName, false, "Sets which min/max linear equation solving technique is preferred.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a min/max linear equation solving technique. Available are: value-iteration (vi) and policy-iteration (pi).").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(minMaxSolvingTechniques)).setDefaultValueString("vi").build()).build()); } bool CoreSettings::isCounterexampleSet() const { diff --git a/src/settings/modules/CoreSettings.h b/src/settings/modules/CoreSettings.h index 9b7189e2c..f6c8fbdf2 100644 --- a/src/settings/modules/CoreSettings.h +++ b/src/settings/modules/CoreSettings.h @@ -151,7 +151,6 @@ namespace storm { static const std::string engineOptionShortName; static const std::string ddLibraryOptionName; static const std::string cudaOptionName; - static const std::string minMaxEquationSolvingTechniqueOptionName; }; } // namespace modules diff --git a/src/storage/expressions/BinaryNumericalFunctionExpression.cpp b/src/storage/expressions/BinaryNumericalFunctionExpression.cpp index 95a326de1..7c4367952 100644 --- a/src/storage/expressions/BinaryNumericalFunctionExpression.cpp +++ b/src/storage/expressions/BinaryNumericalFunctionExpression.cpp @@ -3,7 +3,7 @@ #include "src/storage/expressions/BinaryNumericalFunctionExpression.h" #include "src/storage/expressions/IntegerLiteralExpression.h" -#include "src/storage/expressions/DoubleLiteralExpression.h" +#include "src/storage/expressions/RationalLiteralExpression.h" #include "src/storage/expressions/ExpressionVisitor.h" #include "src/utility/macros.h" #include "src/exceptions/InvalidTypeException.h" @@ -102,7 +102,7 @@ namespace storm { case OperatorType::Power: newValue = static_cast(std::pow(firstOperandEvaluation, secondOperandEvaluation)); break; case OperatorType::Divide: STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Unable to simplify division."); break; } - return std::shared_ptr(new DoubleLiteralExpression(this->getManager(), newValue)); + return std::shared_ptr(new RationalLiteralExpression(this->getManager(), newValue)); } } diff --git a/src/storage/expressions/DoubleLiteralExpression.cpp b/src/storage/expressions/DoubleLiteralExpression.cpp deleted file mode 100644 index cab9fc31b..000000000 --- a/src/storage/expressions/DoubleLiteralExpression.cpp +++ /dev/null @@ -1,39 +0,0 @@ -#include "src/storage/expressions/DoubleLiteralExpression.h" -#include "src/storage/expressions/ExpressionManager.h" -#include "src/storage/expressions/ExpressionVisitor.h" - -namespace storm { - namespace expressions { - DoubleLiteralExpression::DoubleLiteralExpression(ExpressionManager const& manager, double value) : BaseExpression(manager, manager.getRationalType()), value(value) { - // Intentionally left empty. - } - - double DoubleLiteralExpression::evaluateAsDouble(Valuation const* valuation) const { - return this->getValue(); - } - - bool DoubleLiteralExpression::isLiteral() const { - return true; - } - - void DoubleLiteralExpression::gatherVariables(std::set& variables) const { - return; - } - - std::shared_ptr DoubleLiteralExpression::simplify() const { - return this->shared_from_this(); - } - - boost::any DoubleLiteralExpression::accept(ExpressionVisitor& visitor) const { - return visitor.visit(*this); - } - - double DoubleLiteralExpression::getValue() const { - return this->value; - } - - void DoubleLiteralExpression::printToStream(std::ostream& stream) const { - stream << this->getValue(); - } - } -} \ No newline at end of file diff --git a/src/storage/expressions/DoubleLiteralExpression.h b/src/storage/expressions/DoubleLiteralExpression.h deleted file mode 100644 index 676291a77..000000000 --- a/src/storage/expressions/DoubleLiteralExpression.h +++ /dev/null @@ -1,53 +0,0 @@ -#ifndef STORM_STORAGE_EXPRESSIONS_DOUBLELITERALEXPRESSION_H_ -#define STORM_STORAGE_EXPRESSIONS_DOUBLELITERALEXPRESSION_H_ - -#include "src/storage/expressions/BaseExpression.h" -#include "src/utility/OsDetection.h" - -namespace storm { - namespace expressions { - class DoubleLiteralExpression : public BaseExpression { - public: - /*! - * Creates an double literal expression with the given value. - * - * @param manager The manager responsible for this expression. - * @param value The value of the double literal. - */ - DoubleLiteralExpression(ExpressionManager const& manager, double value); - - // Instantiate constructors and assignments with their default implementations. - DoubleLiteralExpression(DoubleLiteralExpression const& other) = default; - DoubleLiteralExpression& operator=(DoubleLiteralExpression const& other) = delete; -#ifndef WINDOWS - DoubleLiteralExpression(DoubleLiteralExpression&&) = default; - DoubleLiteralExpression& operator=(DoubleLiteralExpression&&) = delete; -#endif - virtual ~DoubleLiteralExpression() = default; - - // Override base class methods. - virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override; - virtual bool isLiteral() const override; - virtual void gatherVariables(std::set& variables) const override; - virtual std::shared_ptr simplify() const override; - virtual boost::any accept(ExpressionVisitor& visitor) const override; - - /*! - * Retrieves the value of the double literal. - * - * @return The value of the double literal. - */ - double getValue() const; - - protected: - // Override base class method. - virtual void printToStream(std::ostream& stream) const override; - - private: - // The value of the double literal. - double value; - }; - } -} - -#endif /* STORM_STORAGE_EXPRESSIONS_DOUBLELITERALEXPRESSION_H_ */ \ No newline at end of file diff --git a/src/storage/expressions/ExpressionManager.cpp b/src/storage/expressions/ExpressionManager.cpp index d1add4402..ed51f76ee 100644 --- a/src/storage/expressions/ExpressionManager.cpp +++ b/src/storage/expressions/ExpressionManager.cpp @@ -65,7 +65,11 @@ namespace storm { } Expression ExpressionManager::rational(double value) const { - return Expression(std::shared_ptr(new DoubleLiteralExpression(*this, value))); + return Expression(std::shared_ptr(new RationalLiteralExpression(*this, value))); + } + + Expression ExpressionManager::rational(storm::RationalNumber const& value) const { + return Expression(std::shared_ptr(new RationalLiteralExpression(*this, value))); } bool ExpressionManager::operator==(ExpressionManager const& other) const { diff --git a/src/storage/expressions/ExpressionManager.h b/src/storage/expressions/ExpressionManager.h index 6fee92fd6..f3ec7e76b 100644 --- a/src/storage/expressions/ExpressionManager.h +++ b/src/storage/expressions/ExpressionManager.h @@ -10,6 +10,7 @@ #include "src/storage/expressions/Variable.h" #include "src/storage/expressions/Expression.h" +#include "src/adapters/CarlAdapter.h" #include "src/utility/OsDetection.h" namespace storm { @@ -104,6 +105,14 @@ namespace storm { * @return The resulting expression. */ Expression rational(double value) const; + + /*! + * Creates an expression that characterizes the given rational literal. + * + * @param value The value of the rational literal. + * @return The resulting expression. + */ + Expression rational(storm::RationalNumber const& value) const; /*! * Compares the two expression managers for equality, which holds iff they are the very same object. diff --git a/src/storage/expressions/ExpressionVisitor.h b/src/storage/expressions/ExpressionVisitor.h index 5fdb486c2..1abafc2a6 100644 --- a/src/storage/expressions/ExpressionVisitor.h +++ b/src/storage/expressions/ExpressionVisitor.h @@ -15,7 +15,7 @@ namespace storm { class UnaryNumericalFunctionExpression; class BooleanLiteralExpression; class IntegerLiteralExpression; - class DoubleLiteralExpression; + class RationalLiteralExpression; class ExpressionVisitor { public: @@ -28,7 +28,7 @@ namespace storm { virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) = 0; virtual boost::any visit(BooleanLiteralExpression const& expression) = 0; virtual boost::any visit(IntegerLiteralExpression const& expression) = 0; - virtual boost::any visit(DoubleLiteralExpression const& expression) = 0; + virtual boost::any visit(RationalLiteralExpression const& expression) = 0; }; } } diff --git a/src/storage/expressions/Expressions.h b/src/storage/expressions/Expressions.h index d670c29e3..655cc4aab 100644 --- a/src/storage/expressions/Expressions.h +++ b/src/storage/expressions/Expressions.h @@ -4,7 +4,7 @@ #include "src/storage/expressions/BinaryRelationExpression.h" #include "src/storage/expressions/BooleanLiteralExpression.h" #include "src/storage/expressions/IntegerLiteralExpression.h" -#include "src/storage/expressions/DoubleLiteralExpression.h" +#include "src/storage/expressions/RationalLiteralExpression.h" #include "src/storage/expressions/UnaryBooleanFunctionExpression.h" #include "src/storage/expressions/UnaryNumericalFunctionExpression.h" #include "src/storage/expressions/VariableExpression.h" diff --git a/src/storage/expressions/LinearCoefficientVisitor.cpp b/src/storage/expressions/LinearCoefficientVisitor.cpp index 8d7f39278..dc9a909f9 100644 --- a/src/storage/expressions/LinearCoefficientVisitor.cpp +++ b/src/storage/expressions/LinearCoefficientVisitor.cpp @@ -151,8 +151,8 @@ namespace storm { return VariableCoefficients(static_cast(expression.getValue())); } - boost::any LinearCoefficientVisitor::visit(DoubleLiteralExpression const& expression) { - return VariableCoefficients(expression.getValue()); + boost::any LinearCoefficientVisitor::visit(RationalLiteralExpression const& expression) { + return VariableCoefficients(expression.getValueAsDouble()); } } } \ No newline at end of file diff --git a/src/storage/expressions/LinearCoefficientVisitor.h b/src/storage/expressions/LinearCoefficientVisitor.h index b48c53d09..dea1bfc2e 100644 --- a/src/storage/expressions/LinearCoefficientVisitor.h +++ b/src/storage/expressions/LinearCoefficientVisitor.h @@ -75,7 +75,7 @@ namespace storm { virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) override; virtual boost::any visit(BooleanLiteralExpression const& expression) override; virtual boost::any visit(IntegerLiteralExpression const& expression) override; - virtual boost::any visit(DoubleLiteralExpression const& expression) override; + virtual boost::any visit(RationalLiteralExpression const& expression) override; }; } } diff --git a/src/storage/expressions/LinearityCheckVisitor.cpp b/src/storage/expressions/LinearityCheckVisitor.cpp index 35e1e5c76..7a33a501a 100644 --- a/src/storage/expressions/LinearityCheckVisitor.cpp +++ b/src/storage/expressions/LinearityCheckVisitor.cpp @@ -85,7 +85,7 @@ namespace storm { return LinearityStatus::LinearWithoutVariables; } - boost::any LinearityCheckVisitor::visit(DoubleLiteralExpression const& expression) { + boost::any LinearityCheckVisitor::visit(RationalLiteralExpression const& expression) { return LinearityStatus::LinearWithoutVariables; } } diff --git a/src/storage/expressions/LinearityCheckVisitor.h b/src/storage/expressions/LinearityCheckVisitor.h index 2df8f8084..6bb35b7e8 100644 --- a/src/storage/expressions/LinearityCheckVisitor.h +++ b/src/storage/expressions/LinearityCheckVisitor.h @@ -29,7 +29,7 @@ namespace storm { virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) override; virtual boost::any visit(BooleanLiteralExpression const& expression) override; virtual boost::any visit(IntegerLiteralExpression const& expression) override; - virtual boost::any visit(DoubleLiteralExpression const& expression) override; + virtual boost::any visit(RationalLiteralExpression const& expression) override; private: enum class LinearityStatus { NonLinear, LinearContainsVariables, LinearWithoutVariables }; diff --git a/src/storage/expressions/RationalLiteralExpression.cpp b/src/storage/expressions/RationalLiteralExpression.cpp new file mode 100644 index 000000000..3fa226a8a --- /dev/null +++ b/src/storage/expressions/RationalLiteralExpression.cpp @@ -0,0 +1,53 @@ +#include "src/storage/expressions/RationalLiteralExpression.h" +#include "src/storage/expressions/ExpressionManager.h" +#include "src/storage/expressions/ExpressionVisitor.h" + +#include "src/utility/constants.h" + +namespace storm { + namespace expressions { + RationalLiteralExpression::RationalLiteralExpression(ExpressionManager const& manager, double value) : BaseExpression(manager, manager.getRationalType()), value(storm::utility::convertNumber(value)) { + // Intentionally left empty. + } + + RationalLiteralExpression::RationalLiteralExpression(ExpressionManager const& manager, std::string const& valueAsString) : BaseExpression(manager, manager.getRationalType()), value(storm::utility::convertNumber(valueAsString)) { + // Intentionally left empty. + } + + RationalLiteralExpression::RationalLiteralExpression(ExpressionManager const& manager, storm::RationalNumber const& value) : BaseExpression(manager, manager.getRationalType()), value(value) { + // Intentionally left empty. + } + + double RationalLiteralExpression::evaluateAsDouble(Valuation const* valuation) const { + return this->getValueAsDouble(); + } + + bool RationalLiteralExpression::isLiteral() const { + return true; + } + + void RationalLiteralExpression::gatherVariables(std::set& variables) const { + return; + } + + std::shared_ptr RationalLiteralExpression::simplify() const { + return this->shared_from_this(); + } + + boost::any RationalLiteralExpression::accept(ExpressionVisitor& visitor) const { + return visitor.visit(*this); + } + + double RationalLiteralExpression::getValueAsDouble() const { + return storm::utility::convertNumber(this->value); + } + + storm::RationalNumber RationalLiteralExpression::getValue() const { + return this->value; + } + + void RationalLiteralExpression::printToStream(std::ostream& stream) const { + stream << this->getValue(); + } + } +} \ No newline at end of file diff --git a/src/storage/expressions/RationalLiteralExpression.h b/src/storage/expressions/RationalLiteralExpression.h new file mode 100644 index 000000000..4eff900b2 --- /dev/null +++ b/src/storage/expressions/RationalLiteralExpression.h @@ -0,0 +1,78 @@ +#ifndef STORM_STORAGE_EXPRESSIONS_RationalLiteralExpression_H_ +#define STORM_STORAGE_EXPRESSIONS_RationalLiteralExpression_H_ + +#include "src/storage/expressions/BaseExpression.h" +#include "src/utility/OsDetection.h" + +#include "src/adapters/CarlAdapter.h" + +namespace storm { + namespace expressions { + class RationalLiteralExpression : public BaseExpression { + public: + /*! + * Creates an double literal expression with the given value. + * + * @param manager The manager responsible for this expression. + * @param value The value of the double literal. + */ + RationalLiteralExpression(ExpressionManager const& manager, double value); + + /*! + * Creates an double literal expression with the value given as a string. + * + * @param manager The manager responsible for this expression. + * @param value The string representation of the value of the literal. + */ + RationalLiteralExpression(ExpressionManager const& manager, std::string const& valueAsString); + + /*! + * Creates an double literal expression with the rational value. + * + * @param manager The manager responsible for this expression. + * @param value The rational number that is the value of this literal expression. + */ + RationalLiteralExpression(ExpressionManager const& manager, storm::RationalNumber const& value); + + // Instantiate constructors and assignments with their default implementations. + RationalLiteralExpression(RationalLiteralExpression const& other) = default; + RationalLiteralExpression& operator=(RationalLiteralExpression const& other) = delete; +#ifndef WINDOWS + RationalLiteralExpression(RationalLiteralExpression&&) = default; + RationalLiteralExpression& operator=(RationalLiteralExpression&&) = delete; +#endif + virtual ~RationalLiteralExpression() = default; + + // Override base class methods. + virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override; + virtual bool isLiteral() const override; + virtual void gatherVariables(std::set& variables) const override; + virtual std::shared_ptr simplify() const override; + virtual boost::any accept(ExpressionVisitor& visitor) const override; + + /*! + * Retrieves the value of the double literal. + * + * @return The value of the double literal. + */ + double getValueAsDouble() const; + + /*! + * Retrieves the value of the double literal. + * + * @return The value of the double literal. + */ + storm::RationalNumber getValue() const; + + protected: + // Override base class method. + virtual void printToStream(std::ostream& stream) const override; + + private: + // The value of the literal. + storm::RationalNumber value; + }; + } +} + +#endif /* STORM_STORAGE_EXPRESSIONS_RationalLiteralExpression_H_ */ \ No newline at end of file diff --git a/src/storage/expressions/SubstitutionVisitor.cpp b/src/storage/expressions/SubstitutionVisitor.cpp index c736de156..1490e6f59 100644 --- a/src/storage/expressions/SubstitutionVisitor.cpp +++ b/src/storage/expressions/SubstitutionVisitor.cpp @@ -116,7 +116,7 @@ namespace storm { } template - boost::any SubstitutionVisitor::visit(DoubleLiteralExpression const& expression) { + boost::any SubstitutionVisitor::visit(RationalLiteralExpression const& expression) { return expression.getSharedPointer(); } diff --git a/src/storage/expressions/SubstitutionVisitor.h b/src/storage/expressions/SubstitutionVisitor.h index 343521335..5f1a93cb2 100644 --- a/src/storage/expressions/SubstitutionVisitor.h +++ b/src/storage/expressions/SubstitutionVisitor.h @@ -37,7 +37,7 @@ namespace storm { virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) override; virtual boost::any visit(BooleanLiteralExpression const& expression) override; virtual boost::any visit(IntegerLiteralExpression const& expression) override; - virtual boost::any visit(DoubleLiteralExpression const& expression) override; + virtual boost::any visit(RationalLiteralExpression const& expression) override; private: // A mapping of variables to expressions with which they shall be replaced. diff --git a/src/storage/expressions/ToExprtkStringVisitor.cpp b/src/storage/expressions/ToExprtkStringVisitor.cpp index 51d9c1f34..1492aeae5 100644 --- a/src/storage/expressions/ToExprtkStringVisitor.cpp +++ b/src/storage/expressions/ToExprtkStringVisitor.cpp @@ -212,7 +212,7 @@ namespace storm { return boost::any(); } - boost::any ToExprtkStringVisitor::visit(DoubleLiteralExpression const& expression) { + boost::any ToExprtkStringVisitor::visit(RationalLiteralExpression const& expression) { stream << expression.getValue(); return boost::any(); } diff --git a/src/storage/expressions/ToExprtkStringVisitor.h b/src/storage/expressions/ToExprtkStringVisitor.h index 6c285ff28..d68da589d 100644 --- a/src/storage/expressions/ToExprtkStringVisitor.h +++ b/src/storage/expressions/ToExprtkStringVisitor.h @@ -25,7 +25,7 @@ namespace storm { virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) override; virtual boost::any visit(BooleanLiteralExpression const& expression) override; virtual boost::any visit(IntegerLiteralExpression const& expression) override; - virtual boost::any visit(DoubleLiteralExpression const& expression) override; + virtual boost::any visit(RationalLiteralExpression const& expression) override; private: std::stringstream stream; diff --git a/src/storage/expressions/ToRationalFunctionVisitor.cpp b/src/storage/expressions/ToRationalFunctionVisitor.cpp index 1a3dd0fc3..a219066e4 100644 --- a/src/storage/expressions/ToRationalFunctionVisitor.cpp +++ b/src/storage/expressions/ToRationalFunctionVisitor.cpp @@ -2,6 +2,7 @@ #include +#include "src/utility/constants.h" #include "src/utility/macros.h" #include "src/exceptions/InvalidArgumentException.h" @@ -33,6 +34,7 @@ namespace storm { boost::any ToRationalFunctionVisitor::visit(BinaryNumericalFunctionExpression const& expression) { RationalFunctionType firstOperandAsRationalFunction = boost::any_cast(expression.getFirstOperand()->accept(*this)); RationalFunctionType secondOperandAsRationalFunction = boost::any_cast(expression.getSecondOperand()->accept(*this)); + uint_fast64_t exponentAsInteger = 0; switch(expression.getOperatorType()) { case BinaryNumericalFunctionExpression::OperatorType::Plus: return firstOperandAsRationalFunction + secondOperandAsRationalFunction; @@ -46,6 +48,11 @@ namespace storm { case BinaryNumericalFunctionExpression::OperatorType::Divide: return firstOperandAsRationalFunction / secondOperandAsRationalFunction; break; + case BinaryNumericalFunctionExpression::OperatorType::Power: + STORM_LOG_THROW(storm::utility::isInteger(secondOperandAsRationalFunction), storm::exceptions::InvalidArgumentException, "Exponent of power operator must be a positive integer."); + exponentAsInteger = storm::utility::convertNumber(secondOperandAsRationalFunction); + return storm::utility::pow(firstOperandAsRationalFunction, exponentAsInteger); + break; default: STORM_LOG_ASSERT(false, "Illegal operator type."); } @@ -92,8 +99,8 @@ namespace storm { } template - boost::any ToRationalFunctionVisitor::visit(DoubleLiteralExpression const& expression) { - return RationalFunctionType(carl::rationalize(expression.getValue())); + boost::any ToRationalFunctionVisitor::visit(RationalLiteralExpression const& expression) { + return storm::utility::convertNumber(expression.getValue()); } template class ToRationalFunctionVisitor; diff --git a/src/storage/expressions/ToRationalFunctionVisitor.h b/src/storage/expressions/ToRationalFunctionVisitor.h index 12603f44e..1cda5028f 100644 --- a/src/storage/expressions/ToRationalFunctionVisitor.h +++ b/src/storage/expressions/ToRationalFunctionVisitor.h @@ -27,7 +27,7 @@ namespace storm { virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) override; virtual boost::any visit(BooleanLiteralExpression const& expression) override; virtual boost::any visit(IntegerLiteralExpression const& expression) override; - virtual boost::any visit(DoubleLiteralExpression const& expression) override; + virtual boost::any visit(RationalLiteralExpression const& expression) override; private: template> = carl::dummy> diff --git a/src/storage/expressions/ToRationalNumberVisitor.cpp b/src/storage/expressions/ToRationalNumberVisitor.cpp index 785f36950..1b7319927 100644 --- a/src/storage/expressions/ToRationalNumberVisitor.cpp +++ b/src/storage/expressions/ToRationalNumberVisitor.cpp @@ -1,6 +1,7 @@ #include "src/storage/expressions/ToRationalNumberVisitor.h" #include "src/utility/macros.h" +#include "src/utility/constants.h" #include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/NotSupportedException.h" @@ -28,26 +29,36 @@ namespace storm { template boost::any ToRationalNumberVisitor::visit(BinaryNumericalFunctionExpression const& expression) { - RationalNumberType firstOperandAsRationalFunction = boost::any_cast(expression.getFirstOperand()->accept(*this)); - RationalNumberType secondOperandAsRationalFunction = boost::any_cast(expression.getSecondOperand()->accept(*this)); + RationalNumberType firstOperandAsRationalNumber = boost::any_cast(expression.getFirstOperand()->accept(*this)); + RationalNumberType secondOperandAsRationalNumber = boost::any_cast(expression.getSecondOperand()->accept(*this)); switch(expression.getOperatorType()) { case BinaryNumericalFunctionExpression::OperatorType::Plus: - return firstOperandAsRationalFunction + secondOperandAsRationalFunction; + return firstOperandAsRationalNumber + secondOperandAsRationalNumber; break; case BinaryNumericalFunctionExpression::OperatorType::Minus: - return firstOperandAsRationalFunction - secondOperandAsRationalFunction; + return firstOperandAsRationalNumber - secondOperandAsRationalNumber; break; case BinaryNumericalFunctionExpression::OperatorType::Times: - return firstOperandAsRationalFunction * secondOperandAsRationalFunction; + return firstOperandAsRationalNumber * secondOperandAsRationalNumber; break; case BinaryNumericalFunctionExpression::OperatorType::Divide: - return firstOperandAsRationalFunction / secondOperandAsRationalFunction; + return firstOperandAsRationalNumber / secondOperandAsRationalNumber; + break; + case BinaryNumericalFunctionExpression::OperatorType::Min: + return std::min(firstOperandAsRationalNumber, secondOperandAsRationalNumber); + break; + case BinaryNumericalFunctionExpression::OperatorType::Max: + return std::max(firstOperandAsRationalNumber, secondOperandAsRationalNumber); + break; + case BinaryNumericalFunctionExpression::OperatorType::Power: + STORM_LOG_THROW(storm::utility::isInteger(secondOperandAsRationalNumber), storm::exceptions::InvalidArgumentException, "Exponent of power operator must be a positive integer."); + uint_fast64_t exponentAsInteger = storm::utility::convertNumber(secondOperandAsRationalNumber); + return storm::utility::pow(firstOperandAsRationalNumber, exponentAsInteger); break; - default: - STORM_LOG_ASSERT(false, "Illegal operator type."); } // Return a dummy. This point must, however, never be reached. + STORM_LOG_ASSERT(false, "Illegal operator type."); return boost::any(); } @@ -86,9 +97,9 @@ namespace storm { } template - boost::any ToRationalNumberVisitor::visit(DoubleLiteralExpression const& expression) { + boost::any ToRationalNumberVisitor::visit(RationalLiteralExpression const& expression) { #ifdef STORM_HAVE_CARL - return RationalNumberType(carl::rationalize(expression.getValue())); + return expression.getValue(); #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Rational numbers are not supported in this build."); #endif diff --git a/src/storage/expressions/ToRationalNumberVisitor.h b/src/storage/expressions/ToRationalNumberVisitor.h index 2254931f6..3d53b8a87 100644 --- a/src/storage/expressions/ToRationalNumberVisitor.h +++ b/src/storage/expressions/ToRationalNumberVisitor.h @@ -25,7 +25,7 @@ namespace storm { virtual boost::any visit(UnaryNumericalFunctionExpression const& expression) override; virtual boost::any visit(BooleanLiteralExpression const& expression) override; virtual boost::any visit(IntegerLiteralExpression const& expression) override; - virtual boost::any visit(DoubleLiteralExpression const& expression) override; + virtual boost::any visit(RationalLiteralExpression const& expression) override; }; } } diff --git a/src/storage/expressions/UnaryNumericalFunctionExpression.cpp b/src/storage/expressions/UnaryNumericalFunctionExpression.cpp index fa7cad7e3..f5178fb6f 100644 --- a/src/storage/expressions/UnaryNumericalFunctionExpression.cpp +++ b/src/storage/expressions/UnaryNumericalFunctionExpression.cpp @@ -4,7 +4,7 @@ #include "src/storage/expressions/UnaryNumericalFunctionExpression.h" #include "src/storage/expressions/IntegerLiteralExpression.h" -#include "src/storage/expressions/DoubleLiteralExpression.h" +#include "src/storage/expressions/RationalLiteralExpression.h" #include "ExpressionVisitor.h" #include "src/utility/macros.h" #include "src/exceptions/InvalidTypeException.h" @@ -87,7 +87,7 @@ namespace storm { case OperatorType::Floor: value = std::floor(boost::get(operandEvaluation)); break; case OperatorType::Ceil: value = std::ceil(boost::get(operandEvaluation)); break; } - return std::shared_ptr(new DoubleLiteralExpression(this->getManager(), value)); + return std::shared_ptr(new RationalLiteralExpression(this->getManager(), value)); } } diff --git a/src/storage/jani/BooleanVariable.cpp b/src/storage/jani/BooleanVariable.cpp index b7a4c4e19..3eb63780b 100644 --- a/src/storage/jani/BooleanVariable.cpp +++ b/src/storage/jani/BooleanVariable.cpp @@ -11,10 +11,17 @@ namespace storm { // Intentionally left empty. } - bool BooleanVariable::isBooleanVariable() const { return true; } + std::shared_ptr makeBooleanVariable(std::string const& name, storm::expressions::Variable const& variable, boost::optional initValue, bool transient) { + if (initValue) { + return std::make_shared(name, variable, initValue.get(), transient); + } else { + return std::make_shared(name, variable, transient); + } + } + } } \ No newline at end of file diff --git a/src/storage/jani/BooleanVariable.h b/src/storage/jani/BooleanVariable.h index 7a8fe8b21..7fe9603e0 100644 --- a/src/storage/jani/BooleanVariable.h +++ b/src/storage/jani/BooleanVariable.h @@ -21,5 +21,10 @@ namespace storm { virtual bool isBooleanVariable() const override; }; + /** + * Convenience function to call the appropriate constructor and return a shared pointer to the variable. + */ + std::shared_ptr makeBooleanVariable(std::string const& name, storm::expressions::Variable const& variable, boost::optional initValue, bool transient); + } } \ No newline at end of file diff --git a/src/storage/jani/BoundedIntegerVariable.cpp b/src/storage/jani/BoundedIntegerVariable.cpp index f0872a500..58173bb76 100644 --- a/src/storage/jani/BoundedIntegerVariable.cpp +++ b/src/storage/jani/BoundedIntegerVariable.cpp @@ -47,10 +47,8 @@ namespace storm { } std::shared_ptr makeBoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, boost::optional initValue, bool transient, boost::optional lowerBound, boost::optional upperBound) { - if(!lowerBound || !upperBound) { - STORM_LOG_THROW(lowerBound && upperBound, storm::exceptions::NotImplementedException, "Jani Bounded Integer variables (for now) have to be bounded from both sides"); - } - if(initValue) { + STORM_LOG_THROW(lowerBound && upperBound, storm::exceptions::NotImplementedException, "Jani Bounded Integer variables (for now) have to be bounded from both sides"); + if (initValue) { return std::make_shared(name, variable, initValue.get(), transient, lowerBound.get(), upperBound.get()); } else { return std::make_shared(name, variable, transient, lowerBound.get(), upperBound.get()); diff --git a/src/storage/jani/BoundedIntegerVariable.h b/src/storage/jani/BoundedIntegerVariable.h index c9a42b177..1c68bd239 100644 --- a/src/storage/jani/BoundedIntegerVariable.h +++ b/src/storage/jani/BoundedIntegerVariable.h @@ -61,7 +61,7 @@ namespace storm { }; /** - * Convenience function to call the appropriate constructor and retur a shared pointer to the variable. + * Convenience function to call the appropriate constructor and return a shared pointer to the variable. */ std::shared_ptr makeBoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, boost::optional initValue, bool transient, boost::optional lowerBound, boost::optional upperBound); } diff --git a/src/storage/jani/UnboundedIntegerVariable.h b/src/storage/jani/UnboundedIntegerVariable.h index d3d3daa01..17f81d334 100644 --- a/src/storage/jani/UnboundedIntegerVariable.h +++ b/src/storage/jani/UnboundedIntegerVariable.h @@ -15,7 +15,6 @@ namespace storm { * Creates an unbounded integer variable with initial value. */ UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const&, bool transient=false); - virtual bool isUnboundedIntegerVariable() const override; }; diff --git a/src/storage/prism/BooleanVariable.cpp b/src/storage/prism/BooleanVariable.cpp index c38812ec6..422b2266f 100644 --- a/src/storage/prism/BooleanVariable.cpp +++ b/src/storage/prism/BooleanVariable.cpp @@ -1,5 +1,7 @@ #include "src/storage/prism/BooleanVariable.h" +#include "src/storage/expressions/ExpressionManager.h" + namespace storm { namespace prism { BooleanVariable::BooleanVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValueExpression, std::string const& filename, uint_fast64_t lineNumber) : Variable(variable, initialValueExpression, false, filename, lineNumber) { @@ -7,11 +9,21 @@ namespace storm { } BooleanVariable BooleanVariable::substitute(std::map const& substitution) const { - return BooleanVariable(this->getExpressionVariable(), this->getInitialValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); + return BooleanVariable(this->getExpressionVariable(), this->getInitialValueExpression().isInitialized() ? this->getInitialValueExpression().substitute(substitution) : this->getInitialValueExpression(), this->getFilename(), this->getLineNumber()); + } + + void BooleanVariable::createMissingInitialValue() { + if (!this->hasInitialValue()) { + this->setInitialValueExpression(this->getExpressionVariable().getManager().boolean(false)); + } } std::ostream& operator<<(std::ostream& stream, BooleanVariable const& variable) { - stream << variable.getName() << ": bool init " << variable.getInitialValueExpression() << ";"; + stream << variable.getName() << ": bool"; + if (variable.hasInitialValue()) { + stream << " init " << variable.getInitialValueExpression(); + } + stream << ";"; return stream; } diff --git a/src/storage/prism/BooleanVariable.h b/src/storage/prism/BooleanVariable.h index 5b43e191c..c5c3ba8e4 100644 --- a/src/storage/prism/BooleanVariable.h +++ b/src/storage/prism/BooleanVariable.h @@ -37,6 +37,8 @@ namespace storm { */ BooleanVariable substitute(std::map const& substitution) const; + virtual void createMissingInitialValue() override; + friend std::ostream& operator<<(std::ostream& stream, BooleanVariable const& variable); }; diff --git a/src/storage/prism/Constant.cpp b/src/storage/prism/Constant.cpp index 0416dc4b9..1c3b07057 100644 --- a/src/storage/prism/Constant.cpp +++ b/src/storage/prism/Constant.cpp @@ -42,7 +42,12 @@ namespace storm { } std::ostream& operator<<(std::ostream& stream, Constant const& constant) { - stream << "const " << constant.getExpressionVariable().getType() << " "; + stream << "const "; + if (constant.getType().isRationalType()) { + stream << "double" << " "; + } else { + stream << constant.getType() << " "; + } stream << constant.getName(); if (constant.isDefined()) { stream << " = " << constant.getExpression(); diff --git a/src/storage/prism/IntegerVariable.cpp b/src/storage/prism/IntegerVariable.cpp index b2306ece0..8b60b0e56 100644 --- a/src/storage/prism/IntegerVariable.cpp +++ b/src/storage/prism/IntegerVariable.cpp @@ -19,11 +19,21 @@ namespace storm { } IntegerVariable IntegerVariable::substitute(std::map const& substitution) const { - return IntegerVariable(this->getExpressionVariable(), this->getLowerBoundExpression().substitute(substitution), this->getUpperBoundExpression().substitute(substitution), this->getInitialValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); + return IntegerVariable(this->getExpressionVariable(), this->getLowerBoundExpression().substitute(substitution), this->getUpperBoundExpression().substitute(substitution), this->getInitialValueExpression().isInitialized() ? this->getInitialValueExpression().substitute(substitution) : this->getInitialValueExpression(), this->getFilename(), this->getLineNumber()); + } + + void IntegerVariable::createMissingInitialValue() { + if (!this->hasInitialValue()) { + this->setInitialValueExpression(this->getLowerBoundExpression()); + } } std::ostream& operator<<(std::ostream& stream, IntegerVariable const& variable) { - stream << variable.getName() << ": [" << variable.getLowerBoundExpression() << ".." << variable.getUpperBoundExpression() << "]" << " init " << variable.getInitialValueExpression() << ";"; + stream << variable.getName() << ": [" << variable.getLowerBoundExpression() << ".." << variable.getUpperBoundExpression() << "]"; + if (variable.hasInitialValue()) { + stream << " init " << variable.getInitialValueExpression(); + } + stream << ";"; return stream; } } // namespace prism diff --git a/src/storage/prism/IntegerVariable.h b/src/storage/prism/IntegerVariable.h index fc1c6ecf5..335c2ce05 100644 --- a/src/storage/prism/IntegerVariable.h +++ b/src/storage/prism/IntegerVariable.h @@ -60,6 +60,8 @@ namespace storm { */ IntegerVariable substitute(std::map const& substitution) const; + virtual void createMissingInitialValue() override; + friend std::ostream& operator<<(std::ostream& stream, IntegerVariable const& variable); private: diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp index d4168196d..095ac3e11 100644 --- a/src/storage/prism/Module.cpp +++ b/src/storage/prism/Module.cpp @@ -42,7 +42,7 @@ namespace storm { std::vector const& Module::getIntegerVariables() const { return this->integerVariables; } - + std::set Module::getAllExpressionVariables() const { std::set result; for (auto const& var : this->getBooleanVariables()) { @@ -188,10 +188,7 @@ namespace storm { std::vector newCommands; newCommands.reserve(this->getNumberOfCommands()); for (auto const& command : this->getCommands()) { - Command newCommand = command.substitute(substitution); - if (!newCommand.getGuardExpression().isFalse()) { - newCommands.emplace_back(newCommand); - } + newCommands.emplace_back(command.substitute(substitution)); } return Module(this->getName(), newBooleanVariables, newIntegerVariables, newCommands, this->getFilename(), this->getLineNumber()); @@ -216,12 +213,23 @@ namespace storm { } for (auto const& command : this->getCommands()) { - command.containsVariablesOnlyInUpdateProbabilities(undefinedConstantVariables); + if (!command.containsVariablesOnlyInUpdateProbabilities(undefinedConstantVariables)) { + return false; + } } return true; } + void Module::createMissingInitialValues() { + for (auto& variable : booleanVariables) { + variable.createMissingInitialValue(); + } + for (auto& variable : integerVariables) { + variable.createMissingInitialValue(); + } + } + std::ostream& operator<<(std::ostream& stream, Module const& module) { stream << "module " << module.getName() << std::endl; for (auto const& booleanVariable : module.getBooleanVariables()) { diff --git a/src/storage/prism/Module.h b/src/storage/prism/Module.h index 620432580..c3179b407 100644 --- a/src/storage/prism/Module.h +++ b/src/storage/prism/Module.h @@ -104,7 +104,6 @@ namespace storm { */ std::set getAllExpressionVariables() const; - /*! * Retrieves a list of expressions that characterize the legal ranges of all variables declared by this * module. @@ -226,6 +225,11 @@ namespace storm { */ bool containsVariablesOnlyInUpdateProbabilities(std::set const& undefinedConstantVariables) const; + /*! + * Equips all of the modules' variables without initial values with initial values based on their type. + */ + void createMissingInitialValues(); + friend std::ostream& operator<<(std::ostream& stream, Module const& module); private: diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 3562747e7..a836b5879 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -148,28 +148,15 @@ namespace storm { // Start by creating the necessary mappings from the given ones. this->createMappings(); - // Set the initial construct. + // Set the initial construct if given. if (initialConstruct) { this->initialConstruct = initialConstruct.get(); } else { - // Create a new initial construct if none was given. - storm::expressions::Expression newInitialExpression = manager->boolean(true); - - for (auto const& booleanVariable : this->getGlobalBooleanVariables()) { - newInitialExpression = newInitialExpression && storm::expressions::iff(booleanVariable.getExpression(), booleanVariable.getInitialValueExpression()); - } - for (auto const& integerVariable : this->getGlobalIntegerVariables()) { - newInitialExpression = newInitialExpression && integerVariable.getExpression() == integerVariable.getInitialValueExpression(); - } - for (auto const& module : this->getModules()) { - for (auto const& booleanVariable : module.getBooleanVariables()) { - newInitialExpression = newInitialExpression && storm::expressions::iff(booleanVariable.getExpression(), booleanVariable.getInitialValueExpression()); - } - for (auto const& integerVariable : module.getIntegerVariables()) { - newInitialExpression = newInitialExpression && integerVariable.getExpression() == integerVariable.getInitialValueExpression(); - } + // Otherwise, we create the missing initial values. + this->createMissingInitialValues(); + for (auto& modules : this->modules) { + modules.createMissingInitialValues(); } - this->initialConstruct = storm::prism::InitialConstruct(newInitialExpression, this->getInitialConstruct().getFilename(), this->getInitialConstruct().getLineNumber()); } if (finalModel) { @@ -230,7 +217,7 @@ namespace storm { // constants' variables is empty (except for the update probabilities). // Start by checking the defining expressions of all defined constants. If it contains a currently undefined - //constant, we need to mark the target constant as undefined as well. + // constant, we need to mark the target constant as undefined as well. for (auto const& constant : this->getConstants()) { if (constant.isDefined()) { if (constant.getExpression().containsVariable(undefinedConstantVariables)) { @@ -241,13 +228,17 @@ namespace storm { // Now check initial value expressions of global variables. for (auto const& booleanVariable : this->getGlobalBooleanVariables()) { - if (booleanVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) { - return false; + if (booleanVariable.hasInitialValue()) { + if (booleanVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) { + return false; + } } } for (auto const& integerVariable : this->getGlobalIntegerVariables()) { - if (integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) { - return false; + if (integerVariable.hasInitialValue()) { + if (integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) { + return false; + } } if (integerVariable.getLowerBoundExpression().containsVariable(undefinedConstantVariables)) { return false; @@ -266,7 +257,9 @@ namespace storm { // Proceed by checking each of the modules. for (auto const& module : this->getModules()) { - module.containsVariablesOnlyInUpdateProbabilities(undefinedConstantVariables); + if (!module.containsVariablesOnlyInUpdateProbabilities(undefinedConstantVariables)) { + return false; + } } // Check the reward models. @@ -275,8 +268,10 @@ namespace storm { } // Initial construct. - if (this->getInitialConstruct().getInitialStatesExpression().containsVariable(undefinedConstantVariables)) { - return false; + if (this->hasInitialConstruct()) { + if (this->getInitialConstruct().getInitialStatesExpression().containsVariable(undefinedConstantVariables)) { + return false; + } } // Labels. @@ -446,10 +441,61 @@ namespace storm { return actionToIndexMap; } + bool Program::hasInitialConstruct() const { + return static_cast(initialConstruct); + } + storm::prism::InitialConstruct const& Program::getInitialConstruct() const { + return this->initialConstruct.get(); + } + + boost::optional const& Program::getOptionalInitialConstruct() const { return this->initialConstruct; } + storm::expressions::Expression Program::getInitialStatesExpression() const { + // If there is an initial construct, return its expression. If not, we construct the expression from the + // initial values of the variables (which have to exist). + if (this->hasInitialConstruct()) { + return this->getInitialConstruct().getInitialStatesExpression(); + } else { + storm::expressions::Expression result; + + for (auto const& variable : this->getGlobalBooleanVariables()) { + if (result.isInitialized()) { + result = result && storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression()); + } else { + result = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression()); + } + } + for (auto const& variable : this->getGlobalIntegerVariables()) { + if (result.isInitialized()) { + result = result && variable.getExpressionVariable() == variable.getInitialValueExpression(); + } else { + result = variable.getExpressionVariable() == variable.getInitialValueExpression(); + } + } + for (auto const& module : this->getModules()) { + for (auto const& variable : module.getBooleanVariables()) { + if (result.isInitialized()) { + result = result && storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression()); + } else { + result = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression()); + } + } + for (auto const& variable : module.getIntegerVariables()) { + if (result.isInitialized()) { + result = result && variable.getExpressionVariable() == variable.getInitialValueExpression(); + } else { + result = variable.getExpressionVariable() == variable.getInitialValueExpression(); + } + } + } + + return result; + } + } + bool Program::specifiesSystemComposition() const { return static_cast(systemCompositionConstruct); } @@ -611,7 +657,7 @@ namespace storm { newModules.push_back(module.restrictCommands(indexSet)); } - return Program(this->manager, this->getModelType(), this->getConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), newModules, this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getInitialConstruct(), this->getOptionalSystemCompositionConstruct()); + return Program(this->manager, this->getModelType(), this->getConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), newModules, this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct()); } void Program::createMappings() { @@ -711,11 +757,11 @@ namespace storm { STORM_LOG_THROW(definedUndefinedConstants.find(constantExpressionPair.first) != definedUndefinedConstants.end(), storm::exceptions::InvalidArgumentException, "Unable to define non-existant constant."); } - return Program(this->manager, this->getModelType(), newConstants, this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), this->getModules(), this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getInitialConstruct(), this->getOptionalSystemCompositionConstruct()); + return Program(this->manager, this->getModelType(), newConstants, this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), this->getModules(), this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct()); } Program Program::substituteConstants() const { - // We start by creating the appropriate substitution + // We start by creating the appropriate substitution. std::map constantSubstitution; std::vector newConstants(this->getConstants()); for (uint_fast64_t constantIndex = 0; constantIndex < newConstants.size(); ++constantIndex) { @@ -763,7 +809,10 @@ namespace storm { newRewardModels.emplace_back(rewardModel.substitute(constantSubstitution)); } - storm::prism::InitialConstruct newInitialConstruct = this->getInitialConstruct().substitute(constantSubstitution); + boost::optional newInitialConstruct; + if (this->hasInitialConstruct()) { + newInitialConstruct = this->getInitialConstruct().substitute(constantSubstitution); + } std::vector