diff --git a/.github/workflows/buildtest.yml b/.github/workflows/buildtest.yml index 063eb868f..59aba0cc3 100644 --- a/.github/workflows/buildtest.yml +++ b/.github/workflows/buildtest.yml @@ -14,7 +14,7 @@ env: CARL_BRANCH: "master14" CARL_GIT_URL: "https://github.com/smtrat/carl.git" STORM_GIT_URL: "${{ github.server_url }}/${{ github.repository }}.git" - STORM_BRANCH: "master" + STORM_BRANCH: "${{ github.ref }}" # github runners currently have two cores NR_JOBS: "2" @@ -45,7 +45,10 @@ jobs: - name: Init Docker run: sudo docker run -d -it --name storm --privileged movesrwth/storm-basesystem:${{ matrix.distro }} - name: Git clone - run: sudo docker exec storm git clone --branch $STORM_BRANCH $STORM_GIT_URL /opt/storm + # git clone cannot clone individual commits based on a sha and some other refs + # this workaround fixes this and fetches only one commit + run: | + sudo docker exec storm bash -c "mkdir /opt/storm; cd /opt/storm; git init && git remote add origin ${STORM_GIT_URL} && git fetch --depth 1 origin ${STORM_BRANCH} && git checkout FETCH_HEAD" - name: Run cmake run: sudo docker exec storm bash -c "mkdir /opt/storm/build; cd /opt/storm/build; cmake .. ${CMAKE_ARGS}" - name: Build storm @@ -83,6 +86,8 @@ jobs: ([[ ${{ matrix.debugOrRelease }} == "debug" ]] && echo "CARL_CMAKE_ARGS=${CARL_CMAKE_DEBUG}" || echo "CARL_CMAKE_ARGS=${CARL_CMAKE_RELEASE}") >> $GITHUB_ENV - name: Login into docker + # Only login if using master on original repo (and not for pull requests or forks) + if: github.repository_owner == 'moves-rwth' && github.ref == 'refs/heads/master' run: echo "${{ secrets.STORM_CI_DOCKER_PASSWORD }}" | sudo docker login -u "${{ secrets.STORM_CI_DOCKER_USERNAME }}" --password-stdin - name: Init Docker run: sudo docker run -d -it --name storm --privileged movesrwth/storm-basesystem:${DISTRO} @@ -106,6 +111,8 @@ jobs: - name: Build carl run: sudo docker exec storm bash -c "cd /opt/carl/build; make lib_carl -j ${NR_JOBS}" - name: Deploy carl + # Only deploy if using master on original repo (and not for pull requests or forks) + if: github.repository_owner == 'moves-rwth' && github.ref == 'refs/heads/master' run: | sudo docker commit storm movesrwth/carl:ci-${{ matrix.debugOrRelease }} sudo docker push movesrwth/carl:ci-${{ matrix.debugOrRelease }} @@ -114,8 +121,17 @@ jobs: ##### # Build & TEST & DEPLOY STORM ##### - - name: Git clone - run: sudo docker exec storm git clone --branch $STORM_BRANCH $STORM_GIT_URL /opt/storm + - name: Git shallow clone + # Only clone shallow if not using master on original repo (and not for pull requests or forks) + if: ${{ !(github.repository_owner == 'moves-rwth' && github.ref == 'refs/heads/master') }} + run: | + # git clone cannot clone individual commits based on a sha and some other refs + sudo docker exec storm bash -c "mkdir /opt/storm; cd /opt/storm; git init && git remote add origin ${STORM_GIT_URL} && git fetch --depth 1 origin ${STORM_BRANCH} && git checkout FETCH_HEAD" + - name: Git deep clone + # needed for versioning for now on deployment + if: github.repository_owner == 'moves-rwth' && github.ref == 'refs/heads/master' + run: | + sudo docker exec storm git clone --branch master $STORM_GIT_URL /opt/storm - name: Run cmake run: sudo docker exec storm bash -c "mkdir /opt/storm/build; cd /opt/storm/build; cmake .. ${CMAKE_ARGS}" - name: Build storm @@ -135,8 +151,8 @@ jobs: run: sudo docker exec storm bash -c "cd /opt/storm/build; ctest test --output-on-failure" - name: Deploy storm - # Only deploy if using master (and not for pull requests) - if: github.ref == 'refs/heads/master' + # Only deploy if using master on original repo (and not for pull requests or forks) + if: github.repository_owner == 'moves-rwth' && github.ref == 'refs/heads/master' run: | sudo docker commit storm movesrwth/storm:ci-${{ matrix.debugOrRelease }} sudo docker push movesrwth/storm:ci-${{ matrix.debugOrRelease }} @@ -145,7 +161,8 @@ jobs: name: Email notification runs-on: ubuntu-latest needs: [noDeploy, deploy] - if: always() # set always + # Only run in main repo and even if previous step failed + if: github.repository_owner == 'moves-rwth' && always() steps: - uses: technote-space/workflow-conclusion-action@v2 - uses: dawidd6/action-send-mail@v2 diff --git a/.github/workflows/doxygen.yml b/.github/workflows/doxygen.yml index 6927e72fc..082acc037 100644 --- a/.github/workflows/doxygen.yml +++ b/.github/workflows/doxygen.yml @@ -21,6 +21,8 @@ jobs: deploy: name: Create documentation runs-on: ubuntu-latest + # Do not run on forks + if: github.repository_owner == 'moves-rwth' steps: - name: Init Docker run: sudo docker run -d -it --name storm --privileged ${BASE_IMG} @@ -55,7 +57,8 @@ jobs: name: Email notification runs-on: ubuntu-latest needs: [deploy] - if: always() # set always + # Only run in main repo and even if previous step failed + if: github.repository_owner == 'moves-rwth' && always() steps: - uses: technote-space/workflow-conclusion-action@v2 - uses: dawidd6/action-send-mail@v2 diff --git a/CHANGELOG.md b/CHANGELOG.md index 0d2ca6203..b82cfeaf9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,4 @@ + Changelog ============== @@ -10,6 +11,7 @@ Branch Changes Version 1.6.x ------------- ## Version 1.6.4 (20xx/xx) +- Added support for PRISM models that use unbounded integer variables. - Added an export of check results to json. Use `--exportresult` in the command line interface. - Added computation of steady state probabilities for DTMC/CTMC in the sparse engine. Use `--steadystate` in the command line interface. - Implemented parsing and model building of Stochastic multiplayer games (SMGs) in the PRISM language. No model checking implemented, for now. diff --git a/CMakeLists.txt b/CMakeLists.txt index 1b3bee076..ab84c14f8 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -47,7 +47,9 @@ set(STORM_CARL_DIR_HINT "" CACHE STRING "A hint where the preferred CArL version option(STORM_FORCE_SHIPPED_CARL "Sets whether the shipped version of carl is to be used no matter whether carl is found or not." OFF) MARK_AS_ADVANCED(STORM_FORCE_SHIPPED_CARL) option(USE_SMTRAT "Sets whether SMT-RAT should be included." OFF) +mark_as_advanced(USE_SMTRAT) option(USE_HYPRO "Sets whether HyPro should be included." OFF) +mark_as_advanced(USE_HYPRO) option(XML_SUPPORT "Sets whether xml based format parsing should be included." ON) option(FORCE_COLOR "Force color output" OFF) mark_as_advanced(FORCE_COLOR) diff --git a/README.md b/README.md index 7fa7dac2d..41c7e7c61 100644 --- a/README.md +++ b/README.md @@ -48,10 +48,12 @@ Storm has been developed at RWTH Aachen University. * Jip Spel ###### Contributors (lexicographical order) +* Daniel Basgöze * Dimitri Bohlender * Alexander Bork * Harold Bruintjes * Michael Deutschen +* Linus Heck * Thomas Heinemann * Thomas Henn * Tom Janson diff --git a/resources/3rdparty/carl/CMakeLists.txt b/resources/3rdparty/carl/CMakeLists.txt index 8e7f345b6..9b36c4fb0 100644 --- a/resources/3rdparty/carl/CMakeLists.txt +++ b/resources/3rdparty/carl/CMakeLists.txt @@ -7,7 +7,7 @@ option(STORM_3RDPARTY_BINARY_DIR "3rd party bin dir") message(STATUS "Carl - Storm 3rdparty binary dir: ${STORM_3RDPARTY_BINARY_DIR}") ExternalProject_Add(carl-config - GIT_REPOSITORY https://github.com/smtrat/carl + GIT_REPOSITORY https://github.com/ths-rwth/carl GIT_TAG master14 PREFIX here SOURCE_DIR source_dir diff --git a/resources/3rdparty/include_cudd.cmake b/resources/3rdparty/include_cudd.cmake index 0970cd9e8..6ed57d456 100644 --- a/resources/3rdparty/include_cudd.cmake +++ b/resources/3rdparty/include_cudd.cmake @@ -36,7 +36,7 @@ endif() set(CUDD_CXX_COMPILER "${CMAKE_CXX_COMPILER}") if ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "AppleClang") - if (CMAKE_CXX_COMPILER_VERSION VERSION_EQUAL 12.0.0.12000032) + if (CMAKE_CXX_COMPILER_VERSION VERSION_GREATER_EQUAL 12.0.0.12000032) if (CMAKE_HOST_SYSTEM_VERSION VERSION_GREATER_EQUAL 20.1.0) message(WARNING "There are some known issues compiling CUDD on some setups. We implemented a workaround that mostly works, but if you still have problems compiling CUDD, especially if you do not use the default compiler of your system, please contact the Storm developers.") # The issue is known to occur using the Command Line Tools for XCode 12.2. Apparently, it is fixed in the beta for XCode 12.3. diff --git a/resources/examples/testfiles/mdp/unbounded.nm b/resources/examples/testfiles/mdp/unbounded.nm new file mode 100644 index 000000000..235caa982 --- /dev/null +++ b/resources/examples/testfiles/mdp/unbounded.nm @@ -0,0 +1,8 @@ +mdp +const int N; +module main + x : int; + [] x<=0 -> (x'=x+1); + [] x>0 -> (x'=N*x); +endmodule + diff --git a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h index 609bd8d50..6459be5d1 100644 --- a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h @@ -423,13 +423,11 @@ namespace storm { // Then add the constraints for bounds of the integer variables. for (auto const& integerVariable : program.getGlobalIntegerVariables()) { - localSolver->add(integerVariable.getExpressionVariable() >= integerVariable.getLowerBoundExpression()); - localSolver->add(integerVariable.getExpressionVariable() <= integerVariable.getUpperBoundExpression()); + localSolver->add(integerVariable.getRangeExpression()); } for (auto const& module : program.getModules()) { for (auto const& integerVariable : module.getIntegerVariables()) { - localSolver->add(integerVariable.getExpressionVariable() >= integerVariable.getLowerBoundExpression()); - localSolver->add(integerVariable.getExpressionVariable() <= integerVariable.getUpperBoundExpression()); + localSolver->add(integerVariable.getRangeExpression()); } } } else { diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index 09188848b..a46e20e39 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -129,8 +129,8 @@ namespace storm { */ template storm::utility::RelevantEvents computeRelevantEvents(storm::storage::DFT const& dft, std::vector> const& properties, std::vector const& additionalRelevantEventNames) { - storm::utility::RelevantEvents events(additionalRelevantEventNames); - events.addNamesFromProperty(properties); + storm::utility::RelevantEvents events(additionalRelevantEventNames.begin(), additionalRelevantEventNames.end()); + events.insertNamesFromProperties(properties.begin(), properties.end()); return events; } @@ -153,7 +153,7 @@ namespace storm { */ template typename storm::modelchecker::DFTModelChecker::dft_results - analyzeDFT(storm::storage::DFT const& dft, std::vector> const& properties, bool symred = true, bool allowModularisation = true, storm::utility::RelevantEvents const& relevantEvents = storm::utility::RelevantEvents(), bool allowDCForRelevant = false, + analyzeDFT(storm::storage::DFT const& dft, std::vector> const& properties, bool symred = true, bool allowModularisation = true, storm::utility::RelevantEvents const& relevantEvents = {}, bool allowDCForRelevant = false, double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, bool eliminateChains = false, storm::transformer::EliminationLabelBehavior labelBehavior = storm::transformer::EliminationLabelBehavior::KeepLabels, bool printOutput = false) { storm::modelchecker::DFTModelChecker modelChecker(printOutput); diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.h b/src/storm-dft/modelchecker/dft/DFTModelChecker.h index 71a5c8fdf..30f95b856 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.h @@ -56,7 +56,7 @@ namespace storm { * @return Model checking results for the given properties.. */ dft_results check(storm::storage::DFT const& origDft, property_vector const& properties, bool symred = true, bool allowModularisation = true, - storm::utility::RelevantEvents const& relevantEvents = storm::utility::RelevantEvents(), bool allowDCForRelevant = false, + storm::utility::RelevantEvents const& relevantEvents = {}, bool allowDCForRelevant = false, double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, bool eliminateChains = false, storm::transformer::EliminationLabelBehavior labelBehavior = storm::transformer::EliminationLabelBehavior::KeepLabels); diff --git a/src/storm-dft/utility/RelevantEvents.h b/src/storm-dft/utility/RelevantEvents.h index ddca1e1f1..16fde5118 100644 --- a/src/storm-dft/utility/RelevantEvents.h +++ b/src/storm-dft/utility/RelevantEvents.h @@ -7,6 +7,7 @@ #include "storm-dft/storage/dft/DFT.h" #include "storm-dft/settings/modules/FaultTreeSettings.h" +#include namespace storm { namespace utility { @@ -15,47 +16,65 @@ namespace storm { public: /*! - * Create relevant events from given event names. + * Constructs empty RelevantEvents object + */ + RelevantEvents() = default; + + /*! + * Create relevant events from given event names in an initializer list. * If name 'all' occurs, all elements are stored as relevant. * - * @param relevantEvents List of relevant event names. + * Allows syntactic sugar like: + * RelevantEvents e = {}; + * and + * RelevantEvents e{"a"}; + * + * @param init The initializer list. */ - RelevantEvents(std::vector const& relevantEvents = {}) { - // check if the name "all" occurs - if (std::any_of(relevantEvents.begin(), relevantEvents.end(), - [](auto const& name) { return name == "all"; })) { - this->allRelevant = true; - } else { - this->names.insert(relevantEvents.begin(), relevantEvents.end()); - } + RelevantEvents(std::initializer_list init) { + insert(init.begin(), init.end()); + } + + /*! + * Create relevant events from given event names in a range. + * If name 'all' occurs, all elements are stored as relevant. + * + * @param first Iterator pointing to the start of a range of names. + * @param last Iterator pointing to the end of a range of names. + */ + template + RelevantEvents(ForwardIt first, ForwardIt last) { + insert(first, last); } - bool operator==(RelevantEvents const& rhs) { + bool operator==(RelevantEvents const& rhs) const { return this->allRelevant == rhs.allRelevant || this->names == rhs.names; } - bool operator!=(RelevantEvents const& rhs) { + bool operator!=(RelevantEvents const& rhs) const { return !(*this == rhs); } /*! - * Add relevant event names required by the labels in properties. + * Add relevant event names required by the labels in properties of a range. * - * @param properties List of properties. All events occurring in a property are relevant. + * @param first Iterator pointing to the start of a std::shared_ptr range. + * @param last Iterator pointing to the end of a std::shared_ptr range. */ - void addNamesFromProperty(std::vector> const& properties) { + template + void insertNamesFromProperties(ForwardIt first, ForwardIt last) { if (this->allRelevant) { return; } // Get necessary labels from properties - std::vector> atomicLabels; - for (auto property : properties) { - property->gatherAtomicLabelFormulas(atomicLabels); - } + std::vector> atomicLabels{}; + std::for_each(first, last, [&atomicLabels](auto const& property){ + property->gatherAtomicLabelFormulas(atomicLabels); + }); // Add relevant event names from properties - for (auto atomic : atomicLabels) { + for (auto const& atomic : atomicLabels) { std::string label = atomic->getLabel(); if (label == "failed" or label == "skipped") { // Ignore as these label will always be added if necessary @@ -63,10 +82,10 @@ namespace storm { // Get name of event if (boost::ends_with(label, "_failed")) { // length of "_failed" = 7 - this->addEvent(label.substr(0, label.size() - 7)); + this->names.insert(label.substr(0, label.size() - 7)); } else if (boost::ends_with(label, "_dc")) { // length of "_dc" = 3 - this->addEvent(label.substr(0, label.size() - 3)); + this->names.insert(label.substr(0, label.size() - 3)); } else if (label.find("_claimed_") != std::string::npos) { STORM_LOG_THROW(storm::settings::getModule().isAddLabelsClaiming(), storm::exceptions::InvalidArgumentException, "Claiming labels will not be exported but are required for label '" << label << "'. Try setting --labels-claiming."); } else { @@ -76,6 +95,36 @@ namespace storm { } } + /*! + * Add relevant event. + * If name 'all' occurs, all elements are stored as relevant. + * + * @param name Name of relevant event. + */ + void insert(std::string const& name) { + if(name == "all") { + setAllRelevant(); + } + names.insert(name); + } + + /*! + * Add relevant event names from a range. + * If name 'all' occurs, all elements are stored as relevant. + * + * @param first Iterator pointing to the start of a range of names. + * @param last Iterator pointing to the end of a range of names. + */ + template + void insert(ForwardIt first, ForwardIt last) { + // check if the name "all" occurs + if (std::any_of(first, last, [](auto const& name) { return name == "all"; })) { + setAllRelevant(); + } else { + this->names.insert(first, last); + } + } + /*! * Check that the relevant names correspond to existing elements in the DFT. * @@ -103,15 +152,26 @@ namespace storm { } } - private: - /*! - * Add relevant event. + * Merge the given RelevantEvents with *this * - * @param name Name of relevant event. + * @return A reference to *this, allowing chaining i.e. e.merge(a).merge(b) */ - void addEvent(std::string const& name) { - names.insert(name); + RelevantEvents& merge(RelevantEvents const &other) { + if (!this->allRelevant) { + if(other.allRelevant) { + setAllRelevant(); + } else { + this->names.insert(other.names.begin(), other.names.end()); + } + } + return *this; + } + + private: + void setAllRelevant() { + this->allRelevant = true; + this->names.clear(); } // Names of relevant events. diff --git a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp index eac3df86a..ddeb32cb3 100644 --- a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp +++ b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp @@ -140,7 +140,7 @@ namespace storm { // Check the formula and store the result as a hint for the next call. // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula if(this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { - std::unique_ptr result = modelChecker.check(env, *this->currentCheckTask); + result = modelChecker.check(env, *this->currentCheckTask); storm::storage::Scheduler const& scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); hint.setResultHint(result->template asExplicitQuantitativeCheckResult().getValueVector()); hint.setSchedulerHint(dynamic_cast const&>(scheduler)); diff --git a/src/storm-parsers/parser/PrismParser.cpp b/src/storm-parsers/parser/PrismParser.cpp index 025baa74f..9f88b3a83 100644 --- a/src/storm-parsers/parser/PrismParser.cpp +++ b/src/storm-parsers/parser/PrismParser.cpp @@ -151,7 +151,13 @@ namespace storm { booleanVariableDefinition = (((freshIdentifier > qi::lit(":")) >> qi::lit("bool")) > -((qi::lit("init") > boolExpression[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 = (((freshIdentifier > qi::lit(":")) >> qi::lit("[")) > intExpression > qi::lit("..") > intExpression > qi::lit("]") > -(qi::lit("init") > intExpression[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createIntegerVariable, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_a)]; + boundedIntegerVariableDefinition = (((freshIdentifier > qi::lit(":")) >> qi::lit("[")) > intExpression > qi::lit("..") > intExpression > qi::lit("]") > -(qi::lit("init") > intExpression[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createIntegerVariable, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_a)]; + boundedIntegerVariableDefinition.name("bounded integer variable definition"); + + unboundedIntegerVariableDefinition = (((freshIdentifier > qi::lit(":")) >> qi::lit("int")) > -(qi::lit("init") > intExpression[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createIntegerVariable, phoenix::ref(*this), qi::_1, storm::expressions::Expression(), storm::expressions::Expression(), qi::_a)]; + unboundedIntegerVariableDefinition.name("unbounded integer variable definition"); + + integerVariableDefinition = boundedIntegerVariableDefinition | unboundedIntegerVariableDefinition; integerVariableDefinition.name("integer variable definition"); clockVariableDefinition = (((freshIdentifier > qi::lit(":")) >> qi::lit("clock")) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createClockVariable, phoenix::ref(*this), qi::_1)]; diff --git a/src/storm-parsers/parser/PrismParser.h b/src/storm-parsers/parser/PrismParser.h index 7471ef52d..2b5bb8cfe 100644 --- a/src/storm-parsers/parser/PrismParser.h +++ b/src/storm-parsers/parser/PrismParser.h @@ -243,8 +243,6 @@ namespace storm { // Rules for global variable definitions. qi::rule globalVariableDefinition; - qi::rule globalBooleanVariableDefinition; - qi::rule globalIntegerVariableDefinition; // Rules for modules definition. qi::rule knownModuleName; @@ -257,6 +255,8 @@ namespace storm { qi::rule&, std::vector&, std::vector&), Skipper> variableDefinition; qi::rule, Skipper> booleanVariableDefinition; qi::rule, Skipper> integerVariableDefinition; + qi::rule, Skipper> boundedIntegerVariableDefinition; + qi::rule, Skipper> unboundedIntegerVariableDefinition; qi::rule, Skipper> clockVariableDefinition; // Rules for command definitions. diff --git a/src/storm/builder/DdPrismModelBuilder.cpp b/src/storm/builder/DdPrismModelBuilder.cpp index 79c7fb8a3..6a879d9ba 100644 --- a/src/storm/builder/DdPrismModelBuilder.cpp +++ b/src/storm/builder/DdPrismModelBuilder.cpp @@ -541,7 +541,7 @@ namespace storm { template bool DdPrismModelBuilder::canHandle(storm::prism::Program const& program) { - return program.getModelType() != storm::prism::Program::ModelType::PTA; + return !program.hasUnboundedVariables() && (program.getModelType() != storm::prism::Program::ModelType::PTA); } template @@ -1311,6 +1311,7 @@ namespace storm { stream << "."; STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str()); } + STORM_LOG_THROW(!program.hasUnboundedVariables(), storm::exceptions::InvalidArgumentException, "Program contains unbounded variables which is not supported by the DD engine."); STORM_LOG_TRACE("Building representation of program:" << std::endl << program << std::endl); diff --git a/src/storm/builder/TerminalStatesGetter.cpp b/src/storm/builder/TerminalStatesGetter.cpp index 16779b8d9..9571c8102 100644 --- a/src/storm/builder/TerminalStatesGetter.cpp +++ b/src/storm/builder/TerminalStatesGetter.cpp @@ -26,7 +26,7 @@ namespace storm { } else if (left.isAtomicLabelFormula()) { terminalLabelCallback(left.asAtomicLabelFormula().getLabel(), false); } - } else if (formula.isBoundedUntilFormula()) { + } else if (formula.isBoundedUntilFormula() && !formula.asBoundedUntilFormula().hasMultiDimensionalSubformulas()) { storm::logic::BoundedUntilFormula const& boundedUntil = formula.asBoundedUntilFormula(); bool hasLowerBound = false; for (uint64_t i = 0; i < boundedUntil.getDimension(); ++i) { diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index cfe694c2b..d97ed6c3d 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -98,10 +98,9 @@ namespace storm { if (this->options.hasTerminalStates()) { for (auto const& expressionOrLabelAndBool : this->options.getTerminalStates()) { if (expressionOrLabelAndBool.first.isExpression()) { - this->terminalStates.push_back(std::make_pair(expressionOrLabelAndBool.first.getExpression(), expressionOrLabelAndBool.second)); + this->terminalStates.emplace_back(expressionOrLabelAndBool.first.getExpression(), expressionOrLabelAndBool.second); } else { - // If it's a label, i.e. refers to a transient boolean variable we need to derive the expression - // for the label so we can cut off the exploration there. + // If it's a label, i.e. refers to a transient boolean variable we do some sanity checks first if (expressionOrLabelAndBool.first.getLabel() != "init" && expressionOrLabelAndBool.first.getLabel() != "deadlock") { STORM_LOG_THROW(this->model.getGlobalVariables().hasVariable(expressionOrLabelAndBool.first.getLabel()) , storm::exceptions::InvalidSettingsException, "Terminal states refer to illegal label '" << expressionOrLabelAndBool.first.getLabel() << "'."); @@ -109,7 +108,7 @@ namespace storm { STORM_LOG_THROW(variable.isBooleanVariable(), storm::exceptions::InvalidSettingsException, "Terminal states refer to non-boolean variable '" << expressionOrLabelAndBool.first.getLabel() << "'."); STORM_LOG_THROW(variable.isTransient(), storm::exceptions::InvalidSettingsException, "Terminal states refer to non-transient variable '" << expressionOrLabelAndBool.first.getLabel() << "'."); - this->terminalStates.push_back(std::make_pair(this->model.getLabelExpression(variable.asBooleanVariable(), this->parallelAutomata), expressionOrLabelAndBool.second)); + this->terminalStates.emplace_back(variable.getExpressionVariable().getExpression(), expressionOrLabelAndBool.second); } } } @@ -550,6 +549,8 @@ namespace storm { template StateBehavior JaniNextStateGenerator::expand(StateToIdCallback const& stateToIdCallback) { + // The evaluator should have the default values of the transient variables right now. + // Prepare the result, in case we return early. StateBehavior result; @@ -561,18 +562,22 @@ namespace storm { auto transientVariableValuation = getTransientVariableValuationAtLocations(locations, *this->evaluator); transientVariableValuation.setInEvaluator(*this->evaluator, this->getOptions().isExplorationChecksSet()); result.addStateRewards(evaluateRewardExpressions()); - this->transientVariableInformation.setDefaultValuesInEvaluator(*this->evaluator); - // If a terminal expression was set and we must not expand this state, return now. + // Terminal state expressions do not consider transient variables. if (!this->terminalStates.empty()) { for (auto const& expressionBool : this->terminalStates) { if (this->evaluator->asBool(expressionBool.first) == expressionBool.second) { + // Set back transient variables to default values so we are ready to process the next state + this->transientVariableInformation.setDefaultValuesInEvaluator(*this->evaluator); return result; } } } + // Set back transient variables to default values so we are ready to process the transition assignments + this->transientVariableInformation.setDefaultValuesInEvaluator(*this->evaluator); + // Get all choices for the state. result.setExpanded(); std::vector> allChoices; diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index eeb7db84f..88de55e02 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/src/storm/generator/PrismNextStateGenerator.cpp @@ -33,7 +33,7 @@ namespace storm { // Only after checking validity of the program, we initialize the variable information. this->checkValid(); - this->variableInformation = VariableInformation(program, options.isAddOutOfBoundsStateSet()); + this->variableInformation = VariableInformation(program, options.getReservedBitsForUnboundedVariables(), options.isAddOutOfBoundsStateSet()); // Create a proper evalator. this->evaluator = std::make_unique>(program.getManager()); diff --git a/src/storm/generator/VariableInformation.cpp b/src/storm/generator/VariableInformation.cpp index 91dcf30ee..7fc2c3403 100644 --- a/src/storm/generator/VariableInformation.cpp +++ b/src/storm/generator/VariableInformation.cpp @@ -34,7 +34,47 @@ namespace storm { // Intentionally left empty. } - VariableInformation::VariableInformation(storm::prism::Program const& program, bool outOfBoundsState) : totalBitOffset(0) { + /*! + * Small helper function that sets unspecified lower/upper bounds for an integer variable based on the provided reservedBitsForUnboundedVariables and returns the number of bits required to represent the final variable range + * @pre If has[Lower,Upper]Bound is true, [lower,upper]Bound must be set to the corresponding bound. + * @post lowerBound and upperBound are set to the considered bound for this variable + * @param hasLowerBound shall be true iff there is a lower bound given + * @param lowerBound a reference to the lower bound value + * @param hasUpperBound shall be true iff there is an upper bound given + * @param upperBound a reference to the upper bound + * @param reservedBitsForUnboundedVariables the number of bits that shall be used to represent unbounded variables + * @return the number of bits required to represent the final variable range + */ + uint64_t getBitWidthLowerUpperBound(bool const& hasLowerBound, int64_t& lowerBound, bool const& hasUpperBound, int64_t& upperBound, uint64_t const& reservedBitsForUnboundedVariables) { + if (hasLowerBound) { + if (hasUpperBound) { + STORM_LOG_THROW(lowerBound <= upperBound, storm::exceptions::WrongFormatException, "Lower bound must not be above upper bound"); + // We do not have to set any bounds in this case. + // Return the number of bits required to store all the values between lower and upper bound + return static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); + } else { + // We only have a lower bound. Find the largest upper bound we can store with the given number of bits. + upperBound = lowerBound + ((1ll << reservedBitsForUnboundedVariables) - 1); + } + } else { + if (hasUpperBound) { + // We only have an upper bound. Find the smallest lower bound we can store with the given number of bits + lowerBound = upperBound - ((1ll << reservedBitsForUnboundedVariables) - 1); + } else { + // We neither have a lower nor an upper bound. Take the usual n-bit integer values for lower/upper bounds + lowerBound = -(1ll << (reservedBitsForUnboundedVariables - 1)); // = -2^(reservedBits-1) + upperBound = (1ll << (reservedBitsForUnboundedVariables - 1)) - 1; // = 2^(reservedBits-1) - 1 + } + } + // If we reach this point, it means that the variable is unbounded. + // Lets check for potential overflows. + STORM_LOG_THROW(lowerBound <= upperBound, storm::exceptions::WrongFormatException, "Lower bound must not be above upper bound. Has there been an integer over-/underflow?"); + // By choice of the lower/upper bound, the number of reserved bits must coincide with the bitwidth + STORM_LOG_ASSERT(reservedBitsForUnboundedVariables == static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))), "Unexpected bitwidth for unbounded variable."); + return reservedBitsForUnboundedVariables; + } + + VariableInformation::VariableInformation(storm::prism::Program const& program, uint64_t reservedBitsForUnboundedVariables, bool outOfBoundsState) : totalBitOffset(0) { if (outOfBoundsState) { outOfBoundsBit = 0; ++totalBitOffset; @@ -47,11 +87,15 @@ namespace storm { ++totalBitOffset; } for (auto const& integerVariable : program.getGlobalIntegerVariables()) { - int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt(); - int_fast64_t upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt(); - STORM_LOG_THROW(lowerBound <= upperBound, storm::exceptions::WrongFormatException, "Lower bound must not be above upper bound"); - uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); - integerVariables.emplace_back(integerVariable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true, integerVariable.isObservable()); + int64_t lowerBound, upperBound; + if (integerVariable.hasLowerBoundExpression()) { + lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt(); + } + if (integerVariable.hasUpperBoundExpression()) { + upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt(); + } + uint64_t bitwidth = getBitWidthLowerUpperBound(integerVariable.hasLowerBoundExpression(), lowerBound, integerVariable.hasUpperBoundExpression(), upperBound, reservedBitsForUnboundedVariables); + integerVariables.emplace_back(integerVariable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true, integerVariable.isObservable(), !integerVariable.hasLowerBoundExpression() || !integerVariable.hasUpperBoundExpression()); totalBitOffset += bitwidth; } for (auto const& module : program.getModules()) { @@ -60,11 +104,15 @@ namespace storm { ++totalBitOffset; } for (auto const& integerVariable : module.getIntegerVariables()) { - int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt(); - int_fast64_t upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt(); - STORM_LOG_THROW(lowerBound <= upperBound, storm::exceptions::WrongFormatException, "Lower bound must not be above upper bound"); - uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); - integerVariables.emplace_back(integerVariable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, false, integerVariable.isObservable()); + int64_t lowerBound, upperBound; + if (integerVariable.hasLowerBoundExpression()) { + lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt(); + } + if (integerVariable.hasUpperBoundExpression()) { + upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt(); + } + uint64_t bitwidth = getBitWidthLowerUpperBound(integerVariable.hasLowerBoundExpression(), lowerBound, integerVariable.hasUpperBoundExpression(), upperBound, reservedBitsForUnboundedVariables); + integerVariables.emplace_back(integerVariable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, false, integerVariable.isObservable(), !integerVariable.hasLowerBoundExpression() || !integerVariable.hasUpperBoundExpression()); totalBitOffset += bitwidth; } } @@ -81,22 +129,6 @@ namespace storm { for (auto const& automaton : model.getAutomata()) { STORM_LOG_THROW(!automaton.getVariables().containsNonTransientRealVariables(), storm::exceptions::InvalidArgumentException, "Cannot build model from JANI model that contains non-transient real variables in automaton '" << automaton.getName() << "'."); } -// -// for (auto const& variable : model.getGlobalVariables().getBooleanVariables()) { -// if (!variable.isTransient()) { -// booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset, true, true); -// ++totalBitOffset; -// } -// } -// for (auto const& variable : model.getGlobalVariables().getBoundedIntegerVariables()) { -// if (!variable.isTransient()) { -// int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt(); -// int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt(); -// uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); -// integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true, true); -// totalBitOffset += bitwidth; -// } -// } if (outOfBoundsState) { outOfBoundsBit = 0; @@ -181,30 +213,24 @@ namespace storm { } for (auto const& variable : variableSet.getBoundedIntegerVariables()) { if (!variable.isTransient()) { - int64_t lowerBound; - int64_t upperBound; + int64_t lowerBound, upperBound; + STORM_LOG_ASSERT(variable.hasLowerBound() || variable.hasUpperBound(), "Bounded integer variable has neither a lower nor an upper bound."); if (variable.hasLowerBound()) { lowerBound = variable.getLowerBound().evaluateAsInt(); - if (variable.hasUpperBound()) { - upperBound = variable.getUpperBound().evaluateAsInt(); - } else { - upperBound = lowerBound + ((1ll << reservedBitsForUnboundedVariables) - 1); - } - } else { - STORM_LOG_THROW(variable.hasUpperBound(), storm::exceptions::WrongFormatException, "Bounded integer variable has neither a lower nor an upper bound."); + } + if (variable.hasUpperBound()) { upperBound = variable.getUpperBound().evaluateAsInt(); - lowerBound = upperBound - ((1ll << reservedBitsForUnboundedVariables) - 1); } - uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); + uint64_t bitwidth = getBitWidthLowerUpperBound(variable.hasLowerBound(), lowerBound, variable.hasUpperBound(), upperBound, reservedBitsForUnboundedVariables); integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, global, true, !variable.hasLowerBound() || !variable.hasUpperBound()); totalBitOffset += bitwidth; } } for (auto const& variable : variableSet.getUnboundedIntegerVariables()) { if (!variable.isTransient()) { - int64_t lowerBound = -(1ll << (reservedBitsForUnboundedVariables - 1)); - int64_t upperBound = (1ll << (reservedBitsForUnboundedVariables - 1)) - 1; - integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, reservedBitsForUnboundedVariables, global, true, true); + int64_t lowerBound, upperBound; + uint64_t bitwidth = getBitWidthLowerUpperBound(false, lowerBound, false, upperBound, reservedBitsForUnboundedVariables); + integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, global, true, true); totalBitOffset += reservedBitsForUnboundedVariables; } } diff --git a/src/storm/generator/VariableInformation.h b/src/storm/generator/VariableInformation.h index be97290f8..7c2586dbb 100644 --- a/src/storm/generator/VariableInformation.h +++ b/src/storm/generator/VariableInformation.h @@ -98,7 +98,7 @@ namespace storm { // A structure storing information about the used variables of the program. struct VariableInformation { - VariableInformation(storm::prism::Program const& program, bool outOfBoundsState = false); + VariableInformation(storm::prism::Program const& program, uint64_t reservedBitsForUnboundedVariables, bool outOfBoundsState = false); VariableInformation(storm::jani::Model const& model, std::vector> const& parallelAutomata, uint64_t reservedBitsForUnboundedVariables, bool outOfBoundsState); VariableInformation() = default; diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.cpp index 2471093d7..3660a792a 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/CostLimitClosure.cpp @@ -92,7 +92,7 @@ namespace storm { bool CostLimitClosure::containsUpwardClosure(CostLimits const& costLimits) const { CostLimits infinityProjection(costLimits); - for (auto const& dim : downwardDimensions) { + for (auto dim : downwardDimensions) { infinityProjection[dim] = CostLimit::infinity(); } return contains(infinityProjection); @@ -104,7 +104,7 @@ namespace storm { bool CostLimitClosure::full() const { CostLimits p(dimension(), CostLimit(0)); - for (auto const& dim : downwardDimensions) { + for (auto dim : downwardDimensions) { p[dim] = CostLimit::infinity(); } return contains(p); diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/MemoryStateManager.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/MemoryStateManager.cpp index 1bbd69892..9defc53eb 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/MemoryStateManager.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/MemoryStateManager.cpp @@ -61,12 +61,12 @@ namespace storm { STORM_LOG_ASSERT(dimensionCount > 0, "Invoked MemoryStateManager with zero dimension count."); STORM_LOG_ASSERT(dimensions.size() == dimensionCount, "Invalid size of given bitset."); if (value) { - for (auto const& d : dimensions) { + for (auto d : dimensions) { STORM_LOG_ASSERT(((dimensionBitMask << d) & dimensionsWithoutMemoryMask) == 0, "Tried to set a dimension to 'relevant'-memory state but the dimension is assumed to have no memory."); state |= (dimensionBitMask << d); } } else { - for (auto const& d : dimensions) { + for (auto d : dimensions) { STORM_LOG_ASSERT(((dimensionBitMask << d) & dimensionsWithoutMemoryMask) == 0, "Tried to set a dimension to 'unrelevant'-memory state but the dimension is assumed to have no memory."); state &= ~(dimensionBitMask << d); } diff --git a/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.cpp b/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.cpp index 0313cd8dc..fa2f539ab 100644 --- a/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.cpp @@ -215,7 +215,7 @@ namespace storm { if (this->isResultForAllStates()) { map_type newMap; - for (auto const& element : filterTruthValues) { + for (auto element : filterTruthValues) { newMap.emplace(element, this->getTruthValuesVector().get(element)); } this->truthValues = newMap; diff --git a/src/storm/solver/AbstractEquationSolver.cpp b/src/storm/solver/AbstractEquationSolver.cpp index c068e5d31..ecfa4600e 100644 --- a/src/storm/solver/AbstractEquationSolver.cpp +++ b/src/storm/solver/AbstractEquationSolver.cpp @@ -125,7 +125,22 @@ namespace storm { ValueType const& AbstractEquationSolver::getLowerBound() const { return lowerBound.get(); } - + + template + ValueType const& AbstractEquationSolver::getLowerBound(uint64_t const& index) const { + if (lowerBounds) { + STORM_LOG_ASSERT(index < lowerBounds->size(), "Invalid row index " << index << " for vector of size " << lowerBounds->size()); + if (lowerBound) { + return std::max(lowerBound.get(), lowerBounds.get()[index]); + } else { + return lowerBounds.get()[index]; + } + } else { + STORM_LOG_ASSERT(lowerBound, "Lower bound requested but was not specified before."); + return lowerBound.get(); + } + } + template ValueType AbstractEquationSolver::getLowerBound(bool convertLocalBounds) const { if (lowerBound) { @@ -142,6 +157,21 @@ namespace storm { return upperBound.get(); } + template + ValueType const& AbstractEquationSolver::getUpperBound(uint64_t const& index) const { + if (upperBounds) { + STORM_LOG_ASSERT(index < upperBounds->size(), "Invalid row index " << index << " for vector of size " << upperBounds->size()); + if (upperBound) { + return std::min(upperBound.get(), upperBounds.get()[index]); + } else { + return upperBounds.get()[index]; + } + } else { + STORM_LOG_ASSERT(upperBound, "Upper bound requested but was not specified before."); + return upperBound.get(); + } + } + template ValueType AbstractEquationSolver::getUpperBound(bool convertLocalBounds) const { if (upperBound) { diff --git a/src/storm/solver/AbstractEquationSolver.h b/src/storm/solver/AbstractEquationSolver.h index 0301ad42e..4dca210f8 100644 --- a/src/storm/solver/AbstractEquationSolver.h +++ b/src/storm/solver/AbstractEquationSolver.h @@ -100,6 +100,13 @@ namespace storm { */ ValueType const& getLowerBound() const; + /*! + * Retrieves the lower bound for the variable with the given index (if there is any lower bound). + * @pre some lower bound (local or global) has been specified + * @return the largest lower bound known for the given row + */ + ValueType const& getLowerBound(uint64_t const& index) const; + /*! * Retrieves the lower bound (if there is any). * If the given flag is true and if there are only local bounds, @@ -112,6 +119,13 @@ namespace storm { */ ValueType const& getUpperBound() const; + /*! + * Retrieves the upper bound for the variable with the given index (if there is any upper bound). + * @pre some upper bound (local or global) has been specified + * @return the smallest upper bound known for the given row + */ + ValueType const& getUpperBound(uint64_t const& index) const; + /*! * Retrieves the upper bound (if there is any). * If the given flag is true and if there are only local bounds, diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp index 2b371aae3..cbbba9922 100644 --- a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp @@ -3,6 +3,8 @@ #include "storm/environment/solver/MinMaxSolverEnvironment.h" #include "storm/utility/vector.h" #include "storm/utility/macros.h" +#include "storm/storage/expressions/VariableExpression.h" +#include "storm/storage/expressions/RationalLiteralExpression.h" #include "storm/exceptions/InvalidEnvironmentException.h" #include "storm/exceptions/UnexpectedException.h" @@ -26,28 +28,35 @@ namespace storm { template bool LpMinMaxLinearEquationSolver::internalSolveEquations(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const { - + STORM_LOG_THROW(env.solver().minMax().getMethod() == MinMaxMethod::LinearProgramming, storm::exceptions::InvalidEnvironmentException, "This min max solver does not support the selected technique."); - + // Set up the LP solver std::unique_ptr> solver = lpSolverFactory->create(""); - solver->setOptimizationDirection(invert(dir)); - + // Create a variable for each row group - std::vector variables; - variables.reserve(this->A->getRowGroupCount()); + std::vector variableExpressions; + variableExpressions.reserve(this->A->getRowGroupCount()); for (uint64_t rowGroup = 0; rowGroup < this->A->getRowGroupCount(); ++rowGroup) { - if (this->lowerBound) { - if (this->upperBound) { - variables.push_back(solver->addBoundedContinuousVariable("x" + std::to_string(rowGroup), this->lowerBound.get(), this->upperBound.get(), storm::utility::one())); + if (this->hasLowerBound()) { + ValueType lowerBound = this->getLowerBound(rowGroup); + if (this->hasUpperBound()) { + ValueType upperBound = this->getUpperBound(rowGroup); + if (lowerBound == upperBound) { + // Some solvers (like glpk) don't support variables with bounds [x,x]. We therefore just use a constant instead. This should be more efficient anyways. + variableExpressions.push_back(solver->getConstant(lowerBound)); + } else { + STORM_LOG_ASSERT(lowerBound <= upperBound, "Lower Bound at row group " << rowGroup << " is " << lowerBound << " which exceeds the upper bound " << upperBound << "."); + variableExpressions.emplace_back(solver->addBoundedContinuousVariable("x" + std::to_string(rowGroup), lowerBound, upperBound, storm::utility::one())); + } } else { - variables.push_back(solver->addLowerBoundedContinuousVariable("x" + std::to_string(rowGroup), this->lowerBound.get(), storm::utility::one())); + variableExpressions.emplace_back(solver->addLowerBoundedContinuousVariable("x" + std::to_string(rowGroup), lowerBound, storm::utility::one())); } } else { if (this->upperBound) { - variables.push_back(solver->addUpperBoundedContinuousVariable("x" + std::to_string(rowGroup), this->upperBound.get(), storm::utility::one())); + variableExpressions.emplace_back(solver->addUpperBoundedContinuousVariable("x" + std::to_string(rowGroup), this->getUpperBound(rowGroup), storm::utility::one())); } else { - variables.push_back(solver->addUnboundedContinuousVariable("x" + std::to_string(rowGroup), storm::utility::one())); + variableExpressions.emplace_back(solver->addUnboundedContinuousVariable("x" + std::to_string(rowGroup), storm::utility::one())); } } } @@ -55,15 +64,19 @@ namespace storm { // Add a constraint for each row for (uint64_t rowGroup = 0; rowGroup < this->A->getRowGroupCount(); ++rowGroup) { - for (uint64_t row = this->A->getRowGroupIndices()[rowGroup]; row < this->A->getRowGroupIndices()[rowGroup + 1]; ++row) { - storm::expressions::Expression rowConstraint = solver->getConstant(b[row]); - for (auto const& entry : this->A->getRow(row)) { - rowConstraint = rowConstraint + (solver->getConstant(entry.getValue()) * variables[entry.getColumn()].getExpression()); + for (uint64_t rowIndex = this->A->getRowGroupIndices()[rowGroup]; rowIndex < this->A->getRowGroupIndices()[rowGroup + 1]; ++rowIndex) { + auto row = this->A->getRow(rowIndex); + std::vector summands; + summands.reserve(1+row.getNumberOfEntries()); + summands.push_back(solver->getConstant(b[rowIndex])); + for (auto const& entry : row) { + summands.push_back(solver->getConstant(entry.getValue()) * variableExpressions[entry.getColumn()]); } + storm::expressions::Expression rowConstraint = storm::expressions::sum(summands); if (minimize(dir)) { - rowConstraint = variables[rowGroup].getExpression() <= rowConstraint; + rowConstraint = variableExpressions[rowGroup] <= rowConstraint; } else { - rowConstraint = variables[rowGroup].getExpression() >= rowConstraint; + rowConstraint = variableExpressions[rowGroup] >= rowConstraint; } solver->addConstraint("", rowConstraint); } @@ -76,11 +89,17 @@ namespace storm { STORM_LOG_THROW(solver->isOptimal(), storm::exceptions::UnexpectedException, "Unable to find optimal solution for MinMax equation system."); // write the solution into the solution vector - STORM_LOG_ASSERT(x.size() == variables.size(), "Dimension of x-vector does not match number of varibales."); + STORM_LOG_ASSERT(x.size() == variableExpressions.size(), "Dimension of x-vector does not match number of varibales."); auto xIt = x.begin(); - auto vIt = variables.begin(); + auto vIt = variableExpressions.begin(); for (; xIt != x.end(); ++xIt, ++vIt) { - *xIt = solver->getContinuousValue(*vIt); + auto const& vBaseExpr = vIt->getBaseExpression(); + if (vBaseExpr.isVariable()) { + *xIt = solver->getContinuousValue(vBaseExpr.asVariableExpression().getVariable()); + } else { + STORM_LOG_ASSERT(vBaseExpr.isRationalLiteralExpression(), "Variable expression has unexpected type."); + *xIt = storm::utility::convertNumber(vBaseExpr.asRationalLiteralExpression().getValue()); + } } // If requested, we store the scheduler for retrieval. diff --git a/src/storm/solver/TerminationCondition.cpp b/src/storm/solver/TerminationCondition.cpp index db3f12efd..e3d629c65 100644 --- a/src/storm/solver/TerminationCondition.cpp +++ b/src/storm/solver/TerminationCondition.cpp @@ -69,7 +69,7 @@ namespace storm { if (useMinimum) { if (this->strict) { - for (auto const& pos : this->filter) { + for (auto pos : this->filter) { extremum = std::min(valueGetter(pos), extremum); if (extremum <= this->threshold) { cachedExtremumIndex = pos; @@ -77,7 +77,7 @@ namespace storm { } } } else { - for (auto const& pos : this->filter) { + for (auto pos : this->filter) { extremum = std::min(valueGetter(pos), extremum); if (extremum < this->threshold) { cachedExtremumIndex = pos; @@ -86,7 +86,7 @@ namespace storm { } } } else { - for (auto const& pos : this->filter) { + for (auto pos : this->filter) { extremum = std::max(valueGetter(pos), extremum); } } @@ -118,12 +118,12 @@ namespace storm { } if (useMinimum) { - for (auto const& pos : this->filter) { + for (auto pos : this->filter) { extremum = std::min(valueGetter(pos), extremum); } } else { if (this->strict) { - for (auto const& pos : this->filter) { + for (auto pos : this->filter) { extremum = std::max(valueGetter(pos), extremum); if (extremum >= this->threshold) { cachedExtremumIndex = pos; @@ -131,7 +131,7 @@ namespace storm { } } } else { - for (auto const& pos : this->filter) { + for (auto pos : this->filter) { extremum = std::max(valueGetter(pos), extremum); if (extremum > this->threshold) { cachedExtremumIndex = pos; diff --git a/src/storm/storage/expressions/LinearCoefficientVisitor.cpp b/src/storm/storage/expressions/LinearCoefficientVisitor.cpp index 6f3e45c80..98d2df85e 100644 --- a/src/storm/storage/expressions/LinearCoefficientVisitor.cpp +++ b/src/storm/storage/expressions/LinearCoefficientVisitor.cpp @@ -42,8 +42,8 @@ namespace storm { LinearCoefficientVisitor::VariableCoefficients& LinearCoefficientVisitor::VariableCoefficients::operator/=(VariableCoefficients&& other) { STORM_LOG_THROW(other.variableToCoefficientMapping.size() == 0, storm::exceptions::InvalidArgumentException, "Expression is non-linear."); - for (auto const& otherVariableCoefficientPair : other.variableToCoefficientMapping) { - this->variableToCoefficientMapping[otherVariableCoefficientPair.first] /= other.constantPart; + for (auto& variableCoefficientPair : this->variableToCoefficientMapping) { + variableCoefficientPair.second /= other.constantPart; } constantPart /= other.constantPart; return *this; diff --git a/src/storm/storage/expressions/SimpleValuation.cpp b/src/storm/storage/expressions/SimpleValuation.cpp index b91cd1f0f..3e2d6f029 100644 --- a/src/storm/storage/expressions/SimpleValuation.cpp +++ b/src/storm/storage/expressions/SimpleValuation.cpp @@ -122,7 +122,7 @@ namespace storm { sstr << "[" << std::endl; sstr << getManager() << std::endl; if (!booleanValues.empty()) { - for (auto const& element : booleanValues) { + for (auto element : booleanValues) { sstr << element << " "; } sstr << std::endl; diff --git a/src/storm/storage/geometry/ReduceVertexCloud.cpp b/src/storm/storage/geometry/ReduceVertexCloud.cpp index e3042ccaf..71e725d78 100644 --- a/src/storm/storage/geometry/ReduceVertexCloud.cpp +++ b/src/storm/storage/geometry/ReduceVertexCloud.cpp @@ -115,7 +115,7 @@ namespace storm { } if (timeOut > ) #endif - if (timeOut > 0 && totalTime.getTimeInMilliseconds() > timeOut) { + if (timeOut > 0 && static_cast(totalTime.getTimeInMilliseconds()) > timeOut) { for (uint64_t remainingPoint = pointIndex + 1; remainingPoint < input.size(); ++remainingPoint) { vertices.set(remainingPoint); } diff --git a/src/storm/storage/jani/UnboundedIntegerVariable.cpp b/src/storm/storage/jani/UnboundedIntegerVariable.cpp index a57d3acde..bbb88e307 100644 --- a/src/storm/storage/jani/UnboundedIntegerVariable.cpp +++ b/src/storm/storage/jani/UnboundedIntegerVariable.cpp @@ -19,5 +19,14 @@ namespace storm { return true; } + std::shared_ptr makeUnboundedIntegerVariable(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 { + assert(!transient); + return std::make_shared(name, variable); + } + } + } } diff --git a/src/storm/storage/jani/UnboundedIntegerVariable.h b/src/storm/storage/jani/UnboundedIntegerVariable.h index fe0649ce5..8ea5d52bd 100644 --- a/src/storm/storage/jani/UnboundedIntegerVariable.h +++ b/src/storm/storage/jani/UnboundedIntegerVariable.h @@ -21,5 +21,10 @@ namespace storm { virtual bool isUnboundedIntegerVariable() const override; }; + /** + * Convenience function to call the appropriate constructor and return a shared pointer to the variable. + */ + std::shared_ptr makeUnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, boost::optional initValue, bool transient); + } } diff --git a/src/storm/storage/jani/VariableSet.cpp b/src/storm/storage/jani/VariableSet.cpp index a2fd5a660..0c2b21455 100644 --- a/src/storm/storage/jani/VariableSet.cpp +++ b/src/storm/storage/jani/VariableSet.cpp @@ -214,7 +214,7 @@ namespace storm { std::shared_ptr janiVar = std::move(vToVIt->second); variableToVariable.erase(vToVIt); - nameToVariable.erase(variable.getName()); + nameToVariable.erase(janiVar->getName()); eraseFromVariableVector(variables, variable); if (janiVar->isBooleanVariable()) { eraseFromVariableVector(booleanVariables, variable); diff --git a/src/storm/storage/prism/IntegerVariable.cpp b/src/storm/storage/prism/IntegerVariable.cpp index 6cd4f5759..659c0984f 100644 --- a/src/storm/storage/prism/IntegerVariable.cpp +++ b/src/storm/storage/prism/IntegerVariable.cpp @@ -1,25 +1,53 @@ #include "storm/storage/prism/IntegerVariable.h" +#include "storm/storage/expressions/ExpressionManager.h" + namespace storm { namespace prism { IntegerVariable::IntegerVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression, bool observable, std::string const& filename, uint_fast64_t lineNumber) : Variable(variable, initialValueExpression, observable, filename, lineNumber), lowerBoundExpression(lowerBoundExpression), upperBoundExpression(upperBoundExpression) { // Intentionally left empty. } + bool IntegerVariable::hasLowerBoundExpression() const { + return this->lowerBoundExpression.isInitialized(); + } + storm::expressions::Expression const& IntegerVariable::getLowerBoundExpression() const { + STORM_LOG_ASSERT(hasLowerBoundExpression(), "Tried to get the lower bound expression of variable '" << this->getExpressionVariable().getName() << "' which is not bounded from below."); return this->lowerBoundExpression; } + bool IntegerVariable::hasUpperBoundExpression() const { + return this->upperBoundExpression.isInitialized(); + } + storm::expressions::Expression const& IntegerVariable::getUpperBoundExpression() const { + STORM_LOG_ASSERT(hasUpperBoundExpression(), "Tried to get the lower bound expression of variable '" << this->getExpressionVariable().getName() << "' which is not bounded from above."); return this->upperBoundExpression; } storm::expressions::Expression IntegerVariable::getRangeExpression() const { - return this->getLowerBoundExpression() <= this->getExpressionVariable() && this->getExpressionVariable() <= this->getUpperBoundExpression(); + if (hasLowerBoundExpression()) { + if (hasUpperBoundExpression()) { + return this->getLowerBoundExpression() <= this->getExpressionVariable() && this->getExpressionVariable() <= this->getUpperBoundExpression(); + } else { + return this->getLowerBoundExpression() <= this->getExpressionVariable(); + } + } else { + if (hasUpperBoundExpression()) { + return this->getExpressionVariable() <= this->getUpperBoundExpression(); + } else { + return this->getExpressionVariable().getManager().boolean(true); + } + } } IntegerVariable IntegerVariable::substitute(std::map const& substitution) const { - return IntegerVariable(this->getExpressionVariable(), this->getLowerBoundExpression().substitute(substitution), this->getUpperBoundExpression().substitute(substitution), this->getInitialValueExpression().isInitialized() ? this->getInitialValueExpression().substitute(substitution) : this->getInitialValueExpression(), this->isObservable(), this->getFilename(), this->getLineNumber()); + return IntegerVariable(this->getExpressionVariable(), + this->hasLowerBoundExpression() ? this->getLowerBoundExpression().substitute(substitution) : storm::expressions::Expression(), + this->hasUpperBoundExpression() ? this->getUpperBoundExpression().substitute(substitution) : storm::expressions::Expression(), + this->getInitialValueExpression().isInitialized() ? this->getInitialValueExpression().substitute(substitution) : this->getInitialValueExpression(), + this->isObservable(), this->getFilename(), this->getLineNumber()); } IntegerVariable IntegerVariable::substituteNonStandardPredicates() const { @@ -28,12 +56,30 @@ namespace storm { void IntegerVariable::createMissingInitialValue() { if (!this->hasInitialValue()) { - this->setInitialValueExpression(this->getLowerBoundExpression()); + if (this->hasLowerBoundExpression()) { + this->setInitialValueExpression(this->getLowerBoundExpression()); + } else { + this->setInitialValueExpression(this->getExpressionVariable().getManager().integer(0)); + } } } std::ostream& operator<<(std::ostream& stream, IntegerVariable const& variable) { - stream << variable.getName() << ": [" << variable.getLowerBoundExpression() << ".." << variable.getUpperBoundExpression() << "]"; + stream << variable.getName() << ": "; + if (variable.hasLowerBoundExpression() || variable.hasUpperBoundExpression()) { + // The syntax for the case where there is only one bound is not standardized, yet. + std::cout << "["; + if (variable.hasLowerBoundExpression()) { + std::cout << variable.getLowerBoundExpression(); + } + std::cout << ".."; + if (variable.hasUpperBoundExpression()) { + std::cout << variable.getUpperBoundExpression(); + } + std::cout << "]"; + } else { + std::cout << "int"; + } if (variable.hasInitialValue()) { stream << " init " << variable.getInitialValueExpression(); } diff --git a/src/storm/storage/prism/IntegerVariable.h b/src/storm/storage/prism/IntegerVariable.h index 3069ff45a..97d03873e 100644 --- a/src/storm/storage/prism/IntegerVariable.h +++ b/src/storm/storage/prism/IntegerVariable.h @@ -28,23 +28,36 @@ namespace storm { * @param lineNumber The line number in which the variable is defined. */ IntegerVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression, bool observable, std::string const& filename = "", uint_fast64_t lineNumber = 0); + + /*! + * @return true if a lower bound for this integer variable is defined + */ + bool hasLowerBoundExpression() const; /*! * Retrieves an expression defining the lower bound for this integer variable. - * + * @pre A lower bound for this integer variable is defined * @return An expression defining the lower bound for this integer variable. */ storm::expressions::Expression const& getLowerBoundExpression() const; - + + /*! + * @return true if an upper bound for this integer variable is defined + */ + bool hasUpperBoundExpression() const; + /*! * Retrieves an expression defining the upper bound for this integer variable. - * + * @pre An upper bound for this integer variable is defined * @return An expression defining the upper bound for this integer variable. */ storm::expressions::Expression const& getUpperBoundExpression() const; + /*! * Retrieves an expression characterizing the legal range of the variable. + * Only bounds that are defined will be considered in this expression. + * If neither a lower nor an upper bound is defined, this expression will be equivalent to true. * * @return An expression characterizing the legal range of the variable. */ diff --git a/src/storm/storage/prism/Module.cpp b/src/storm/storage/prism/Module.cpp index 232979c87..64e7a1cd3 100644 --- a/src/storm/storage/prism/Module.cpp +++ b/src/storm/storage/prism/Module.cpp @@ -15,6 +15,15 @@ namespace storm { this->createMappings(); } + bool Module::hasUnboundedVariables() const { + for (auto const& integerVariable : this->integerVariables) { + if (!integerVariable.hasLowerBoundExpression() || !integerVariable.hasUpperBoundExpression()) { + return true; + } + } + return false; + } + std::size_t Module::getNumberOfBooleanVariables() const { return this->booleanVariables.size(); } @@ -74,7 +83,9 @@ namespace storm { std::vector Module::getAllRangeExpressions() const { std::vector result; for (auto const& integerVariable : this->integerVariables) { - result.push_back(integerVariable.getRangeExpression()); + if (integerVariable.hasLowerBoundExpression() || integerVariable.hasUpperBoundExpression()) { + result.push_back(integerVariable.getRangeExpression()); + } } return result; } @@ -299,10 +310,10 @@ namespace storm { if (integerVariable.hasInitialValue() && integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) { return false; } - if (integerVariable.getLowerBoundExpression().containsVariable(undefinedConstantVariables)) { + if (integerVariable.hasLowerBoundExpression() && integerVariable.getLowerBoundExpression().containsVariable(undefinedConstantVariables)) { return false; } - if (integerVariable.getUpperBoundExpression().containsVariable(undefinedConstantVariables)) { + if (integerVariable.hasUpperBoundExpression() && integerVariable.getUpperBoundExpression().containsVariable(undefinedConstantVariables)) { return false; } } diff --git a/src/storm/storage/prism/Module.h b/src/storm/storage/prism/Module.h index 803e5240b..1ba8e7455 100644 --- a/src/storm/storage/prism/Module.h +++ b/src/storm/storage/prism/Module.h @@ -57,6 +57,11 @@ namespace storm { Module(Module&& other) = default; Module& operator=(Module&& other) = default; + /*! + * @return True iff the module contains at least one variable with infinite domain + */ + bool hasUnboundedVariables() const; + /*! * Retrieves the number of boolean variables in the module. * diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index 019b0419c..617479343 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -224,7 +224,21 @@ namespace storm { } return res; } - + + bool Program::hasUnboundedVariables() const { + for (auto const& globalIntegerVariable : this->globalIntegerVariables) { + if (!globalIntegerVariable.hasLowerBoundExpression() || !globalIntegerVariable.hasUpperBoundExpression()) { + return true; + } + } + for (auto const& module : modules) { + if (module.hasUnboundedVariables()) { + return true; + } + } + return false; + } + bool Program::hasUndefinedConstants() const { for (auto const& constant : this->getConstants()) { if (!constant.isDefined()) { @@ -271,10 +285,10 @@ namespace storm { return false; } } - if (integerVariable.getLowerBoundExpression().containsVariable(undefinedConstantVariables)) { + if (integerVariable.hasLowerBoundExpression() && integerVariable.getLowerBoundExpression().containsVariable(undefinedConstantVariables)) { return false; } - if (integerVariable.getUpperBoundExpression().containsVariable(undefinedConstantVariables)) { + if (integerVariable.hasUpperBoundExpression() && integerVariable.getUpperBoundExpression().containsVariable(undefinedConstantVariables)) { return false; } } @@ -454,7 +468,9 @@ namespace storm { std::vector Program::getAllRangeExpressions() const { std::vector result; for (auto const& globalIntegerVariable : this->globalIntegerVariables) { - result.push_back(globalIntegerVariable.getRangeExpression()); + if (globalIntegerVariable.hasLowerBoundExpression() || globalIntegerVariable.hasUpperBoundExpression()) { + result.push_back(globalIntegerVariable.getRangeExpression()); + } } for (auto const& module : modules) { @@ -1157,37 +1173,43 @@ namespace storm { } for (auto const& variable : this->getGlobalIntegerVariables()) { // Check that bound expressions of the range. - std::set containedVariables = variable.getLowerBoundExpression().getVariables(); - std::set illegalVariables; - std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); - bool isValid = illegalVariables.empty(); - - if (!isValid) { - std::vector illegalVariableNames; - for (auto const& var : illegalVariables) { - illegalVariableNames.push_back(var.getName()); + if (variable.hasLowerBoundExpression()) { + std::set containedVariables = variable.getLowerBoundExpression().getVariables(); + std::set illegalVariables; + std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); + bool isValid = illegalVariables.empty(); + + if (!isValid) { + std::vector illegalVariableNames; + for (auto const& var : illegalVariables) { + illegalVariableNames.push_back(var.getName()); + } + STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); } - STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); } - containedVariables = variable.getLowerBoundExpression().getVariables(); - std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); - isValid = illegalVariables.empty(); - if (!isValid) { - std::vector illegalVariableNames; - for (auto const& var : illegalVariables) { - illegalVariableNames.push_back(var.getName()); + if (variable.hasUpperBoundExpression()) { + std::set containedVariables = variable.getUpperBoundExpression().getVariables(); + std::set illegalVariables; + std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); + bool isValid = illegalVariables.empty(); + if (!isValid) { + std::vector illegalVariableNames; + for (auto const& var : illegalVariables) { + illegalVariableNames.push_back(var.getName()); + } + STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); } - STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); } if (variable.hasInitialValue()) { STORM_LOG_THROW(!this->hasInitialConstruct(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": illegal to specify initial value if an initial construct is present."); // Check the initial value of the variable. - containedVariables = variable.getInitialValueExpression().getVariables(); + std::set containedVariables = variable.getInitialValueExpression().getVariables(); + std::set illegalVariables; std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); - isValid = illegalVariables.empty(); + bool isValid = illegalVariables.empty(); if (!isValid) { std::vector illegalVariableNames; for (auto const& var : illegalVariables) { @@ -1230,38 +1252,45 @@ namespace storm { } for (auto const& variable : module.getIntegerVariables()) { // Check that bound expressions of the range. - std::set containedVariables = variable.getLowerBoundExpression().getVariables(); - std::set illegalVariables; - std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); - bool isValid = illegalVariables.empty(); - if (!isValid) { - std::vector illegalVariableNames; - for (auto const& var : illegalVariables) { - illegalVariableNames.push_back(var.getName()); + if (variable.hasLowerBoundExpression()) { + std::set containedVariables = variable.getLowerBoundExpression().getVariables(); + std::set illegalVariables; + std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); + bool isValid = illegalVariables.empty(); + if (!isValid) { + std::vector illegalVariableNames; + for (auto const& var : illegalVariables) { + illegalVariableNames.push_back(var.getName()); + } + STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); } - STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); } - - containedVariables = variable.getLowerBoundExpression().getVariables(); - illegalVariables.clear(); - std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); - isValid = illegalVariables.empty(); - if (!isValid) { - std::vector illegalVariableNames; - for (auto const& var : illegalVariables) { - illegalVariableNames.push_back(var.getName()); + + if (variable.hasUpperBoundExpression()) { + std::set containedVariables = variable.getUpperBoundExpression().getVariables(); + std::set illegalVariables; + + illegalVariables.clear(); + std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); + bool isValid = illegalVariables.empty(); + if (!isValid) { + std::vector illegalVariableNames; + for (auto const& var : illegalVariables) { + illegalVariableNames.push_back(var.getName()); + } + STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); } - STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); } if (variable.hasInitialValue()) { STORM_LOG_THROW(!this->hasInitialConstruct(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": illegal to specify initial value if an initial construct is present."); // Check the initial value of the variable. - containedVariables = variable.getInitialValueExpression().getVariables(); + std::set containedVariables = variable.getInitialValueExpression().getVariables(); + std::set illegalVariables; illegalVariables.clear(); std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); - isValid = illegalVariables.empty(); + bool isValid = illegalVariables.empty(); if (!isValid) { std::vector illegalVariableNames; for (auto const& var : illegalVariables) { @@ -1715,8 +1744,7 @@ namespace storm { // Assert the bounds of the global variables. for (auto const& variable : this->getGlobalIntegerVariables()) { - solver->add(variable.getExpression() >= variable.getLowerBoundExpression()); - solver->add(variable.getExpression() <= variable.getUpperBoundExpression()); + solver->add(variable.getRangeExpression()); } // Make the global variables local, such that the resulting module covers all occurring variables. Note that @@ -1734,8 +1762,7 @@ namespace storm { allClockVariables.insert(allClockVariables.end(), module.getClockVariables().begin(), module.getClockVariables().end()); for (auto const& variable : module.getIntegerVariables()) { - solver->add(variable.getExpression() >= variable.getLowerBoundExpression()); - solver->add(variable.getExpression() <= variable.getUpperBoundExpression()); + solver->add(variable.getRangeExpression()); } if (module.hasInvariant()) { @@ -2079,14 +2106,10 @@ namespace storm { void Program::createMissingInitialValues() { for (auto& variable : globalBooleanVariables) { - if (!variable.hasInitialValue()) { - variable.setInitialValueExpression(manager->boolean(false)); - } + variable.createMissingInitialValue(); } for (auto& variable : globalIntegerVariables) { - if (!variable.hasInitialValue()) { - variable.setInitialValueExpression(variable.getLowerBoundExpression()); - } + variable.createMissingInitialValue(); } } diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h index e49925d5e..3b2240e0c 100644 --- a/src/storm/storage/prism/Program.h +++ b/src/storm/storage/prism/Program.h @@ -93,6 +93,11 @@ namespace storm { */ bool isPartiallyObservable() const; + /*! + * @return True iff the program contains at least one variable with infinite domain + */ + bool hasUnboundedVariables() const; + /*! * Retrieves whether there are undefined constants of any type in the program. * diff --git a/src/storm/storage/prism/ToJaniConverter.cpp b/src/storm/storage/prism/ToJaniConverter.cpp index f6097aaec..1baa10e59 100644 --- a/src/storm/storage/prism/ToJaniConverter.cpp +++ b/src/storm/storage/prism/ToJaniConverter.cpp @@ -129,11 +129,21 @@ namespace storm { // Add all global variables of the PRISM program to the JANI model. for (auto const& variable : program.getGlobalIntegerVariables()) { - if (variable.hasInitialValue()) { - storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression(), false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression())); + if (variable.hasLowerBoundExpression() || variable.hasUpperBoundExpression()) { + storm::jani::BoundedIntegerVariable newBoundedIntegerVariable = *storm::jani::makeBoundedIntegerVariable(variable.getName(), + variable.getExpressionVariable(), + variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, + false, + variable.hasLowerBoundExpression() ? boost::make_optional(variable.getLowerBoundExpression()) : boost::none, + variable.hasUpperBoundExpression() ? boost::make_optional(variable.getUpperBoundExpression()) : boost::none); + storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(newBoundedIntegerVariable); variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); } else { - storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression())); + storm::jani::UnboundedIntegerVariable newUnboundedIntegerVariable = *storm::jani::makeUnboundedIntegerVariable(variable.getName(), + variable.getExpressionVariable(), + variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, + false); + storm::jani::UnboundedIntegerVariable const& createdVariable = janiModel.addVariable(newUnboundedIntegerVariable); variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); } } @@ -344,21 +354,35 @@ namespace storm { storm::jani::Automaton automaton(module.getName(), manager->declareIntegerVariable("_loc_prism2jani_" + module.getName() + "_" + suffix)); for (auto const& variable : module.getIntegerVariables()) { - storm::jani::BoundedIntegerVariable newIntegerVariable = *storm::jani::makeBoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression()); auto findRes = variablesToMakeGlobal.find(variable.getExpressionVariable()); if (findRes != variablesToMakeGlobal.end()) { bool makeVarGlobal = findRes->second; - storm::jani::BoundedIntegerVariable const& createdVariable = makeVarGlobal ? janiModel.addVariable(newIntegerVariable) : automaton.addVariable(newIntegerVariable); - variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); + if (variable.hasLowerBoundExpression() || variable.hasUpperBoundExpression()) { + storm::jani::BoundedIntegerVariable newBoundedIntegerVariable = *storm::jani::makeBoundedIntegerVariable(variable.getName(), + variable.getExpressionVariable(), + variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, + false, + variable.hasLowerBoundExpression() ? boost::make_optional(variable.getLowerBoundExpression()) : boost::none, + variable.hasUpperBoundExpression() ? boost::make_optional(variable.getUpperBoundExpression()) : boost::none); + storm::jani::BoundedIntegerVariable const& createdVariable = makeVarGlobal ? janiModel.addVariable(newBoundedIntegerVariable) : automaton.addVariable(newBoundedIntegerVariable); + variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); + } else { + storm::jani::UnboundedIntegerVariable newUnboundedIntegerVariable = *storm::jani::makeUnboundedIntegerVariable(variable.getName(), + variable.getExpressionVariable(), + variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, + false); + storm::jani::UnboundedIntegerVariable const& createdVariable = makeVarGlobal ? janiModel.addVariable(newUnboundedIntegerVariable) : automaton.addVariable(newUnboundedIntegerVariable); + variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); + } } else { STORM_LOG_INFO("Variable " << variable.getName() << " is declared but never used."); } } for (auto const& variable : module.getBooleanVariables()) { - storm::jani::BooleanVariable newBooleanVariable = *storm::jani::makeBooleanVariable(variable.getName(), variable.getExpressionVariable(), variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, false); auto findRes = variablesToMakeGlobal.find(variable.getExpressionVariable()); if (findRes != variablesToMakeGlobal.end()) { bool makeVarGlobal = findRes->second; + storm::jani::BooleanVariable newBooleanVariable = *storm::jani::makeBooleanVariable(variable.getName(), variable.getExpressionVariable(), variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, false); storm::jani::BooleanVariable const& createdVariable = makeVarGlobal ? janiModel.addVariable(newBooleanVariable) : automaton.addVariable(newBooleanVariable); variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); } else { diff --git a/src/test/storm/builder/DdPrismModelBuilderTest.cpp b/src/test/storm/builder/DdPrismModelBuilderTest.cpp index fef10b9a3..b64e2d277 100644 --- a/src/test/storm/builder/DdPrismModelBuilderTest.cpp +++ b/src/test/storm/builder/DdPrismModelBuilderTest.cpp @@ -319,3 +319,14 @@ TEST(DdPrismModelBuilderTest_Cudd, Composition) { EXPECT_EQ(21ul, mdp->getNumberOfChoices()); } +TEST(UnboundedTest_Sylvan, Mdp) { + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/unbounded.nm"); + storm::prism::Program program = modelDescription.preprocess("N=1").asPrismProgram(); + EXPECT_FALSE(storm::builder::DdPrismModelBuilder().canHandle(program)); +} + +TEST(UnboundedTest_Cudd, Mdp) { + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/unbounded.nm"); + storm::prism::Program program = modelDescription.preprocess("N=1").asPrismProgram(); + EXPECT_FALSE(storm::builder::DdPrismModelBuilder().canHandle(program)); +} \ No newline at end of file diff --git a/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp b/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp index f654d28f1..d7d324112 100644 --- a/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp +++ b/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp @@ -94,6 +94,12 @@ TEST(ExplicitPrismModelBuilderTest, Mdp) { model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(37ul, model->getNumberOfStates()); EXPECT_EQ(59ul, model->getNumberOfTransitions()); + + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/unbounded.nm"); + program = modelDescription.preprocess("N=-7").asPrismProgram(); + model = storm::builder::ExplicitModelBuilder(program).build(); + EXPECT_EQ(9ul, model->getNumberOfStates()); + EXPECT_EQ(9ul, model->getNumberOfTransitions()); } TEST(ExplicitPrismModelBuilderTest, Ma) { @@ -125,3 +131,9 @@ TEST(ExplicitPrismModelBuilderTest, FailComposition) { STORM_SILENT_ASSERT_THROW(storm::builder::ExplicitModelBuilder(program).build(), storm::exceptions::WrongFormatException); } + +TEST(ExplicitPrismModelBuilderTest, FailUnbounded) { + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/unbounded.nm"); + storm::prism::Program program = modelDescription.preprocess("N=7").asPrismProgram(); + STORM_SILENT_ASSERT_THROW(storm::builder::ExplicitModelBuilder(program).build(), storm::exceptions::WrongFormatException); +} diff --git a/src/test/storm/parser/PrismParserTest.cpp b/src/test/storm/parser/PrismParserTest.cpp index 9caba734f..ad509af46 100644 --- a/src/test/storm/parser/PrismParserTest.cpp +++ b/src/test/storm/parser/PrismParserTest.cpp @@ -28,6 +28,7 @@ TEST(PrismParser, SimpleTest) { EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile")); EXPECT_EQ(1ul, result.getNumberOfModules()); EXPECT_EQ(storm::prism::Program::ModelType::DTMC, result.getModelType()); + EXPECT_FALSE(result.hasUnboundedVariables()); testInput = R"(mdp @@ -44,6 +45,7 @@ TEST(PrismParser, SimpleTest) { EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile")); EXPECT_EQ(1ul, result.getNumberOfModules()); EXPECT_EQ(storm::prism::Program::ModelType::MDP, result.getModelType()); + EXPECT_FALSE(result.hasUnboundedVariables()); } TEST(PrismParser, ComplexTest) { @@ -97,8 +99,23 @@ TEST(PrismParser, ComplexTest) { EXPECT_EQ(3ul, result.getNumberOfModules()); EXPECT_EQ(2ul, result.getNumberOfRewardModels()); EXPECT_EQ(1ul, result.getNumberOfLabels()); + EXPECT_FALSE(result.hasUnboundedVariables()); } +TEST(PrismParser, UnboundedTest) { + std::string testInput = + R"(mdp + module main + b : int; + [a] true -> 1: (b'=b+1); + endmodule)"; + + storm::prism::Program result; + EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile")); + EXPECT_EQ(1ul, result.getNumberOfModules()); + EXPECT_EQ(storm::prism::Program::ModelType::MDP, result.getModelType()); + EXPECT_TRUE(result.hasUnboundedVariables()); +} TEST(PrismParser, POMDPInputTest) { std::string testInput = diff --git a/src/test/storm/storage/PrismProgramTest.cpp b/src/test/storm/storage/PrismProgramTest.cpp index dc3ba04b6..73f019e30 100644 --- a/src/test/storm/storage/PrismProgramTest.cpp +++ b/src/test/storm/storage/PrismProgramTest.cpp @@ -1,5 +1,5 @@ -#include "test/storm_gtest.h" #include "storm-config.h" +#include "test/storm_gtest.h" #include "storm-parsers/parser/PrismParser.h" #include "storm/utility/solver.h" @@ -163,4 +163,7 @@ TEST(PrismProgramTest, ConvertToJani) { ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/nand-5-2.pm")); ASSERT_NO_THROW(janiModel = prismProgram.toJani()); + + ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/unbounded.nm")); + ASSERT_NO_THROW(janiModel = prismProgram.toJani()); }