From eaff65ef27593d6d1ee3be67ebc2c62b9d039c1a Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 9 Mar 2021 07:15:22 +0100 Subject: [PATCH 01/27] LinearCoefficientVisitor: Fixed translation of division expressions. --- src/storm/storage/expressions/LinearCoefficientVisitor.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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; From 6df0efcd3e0c52be97a8f36abd9cba4e89b4d3ee Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 9 Mar 2021 13:03:17 +0100 Subject: [PATCH 02/27] Set result correctly for reachability rewards in MdpInstantiationChecker --- .../instantiation/SparseMdpInstantiationModelChecker.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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)); From e59918668e577c2f07a7ac1068fab19c194f8a12 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 10 Mar 2021 06:26:59 +0100 Subject: [PATCH 03/27] AbstractEquationSolver: Added more convenient getters for the most appropriate lower/upper bound of a given variable --- src/storm/solver/AbstractEquationSolver.cpp | 32 ++++++++++++++++++++- src/storm/solver/AbstractEquationSolver.h | 14 +++++++++ 2 files changed, 45 insertions(+), 1 deletion(-) 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, From 45a7db822283b4b2a57280c39618aa1150f5ff22 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 10 Mar 2021 06:31:18 +0100 Subject: [PATCH 04/27] LpMinMaxLinearEquationSolver: Fixed an issue when using glpk occurring when the lower bound of a variable matches the upper bound. Also revamped retrieving of lower/upper bounds. --- .../solver/LpMinMaxLinearEquationSolver.cpp | 61 ++++++++++++------- 1 file changed, 40 insertions(+), 21 deletions(-) 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. From 168b5fabd69c8592de909cc8089e057add4e0552 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 11 Mar 2021 08:03:42 +0100 Subject: [PATCH 05/27] Silenced several warnings --- .../prctl/helper/rewardbounded/CostLimitClosure.cpp | 4 ++-- .../helper/rewardbounded/MemoryStateManager.cpp | 4 ++-- .../results/ExplicitQualitativeCheckResult.cpp | 2 +- src/storm/solver/TerminationCondition.cpp | 12 ++++++------ src/storm/storage/expressions/SimpleValuation.cpp | 2 +- src/storm/storage/geometry/ReduceVertexCloud.cpp | 2 +- 6 files changed, 13 insertions(+), 13 deletions(-) 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/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/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); } From 6f39d431a371a7739c98f2550e000cae55e5edb5 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 12 Mar 2021 13:45:42 +0100 Subject: [PATCH 06/27] Github Actions: only run doxygen and deploy on master branch of original repository (and not on forks or pull requests). --- .github/workflows/buildtest.yml | 11 ++++++++--- .github/workflows/doxygen.yml | 5 ++++- 2 files changed, 12 insertions(+), 4 deletions(-) diff --git a/.github/workflows/buildtest.yml b/.github/workflows/buildtest.yml index 063eb868f..1b998d80a 100644 --- a/.github/workflows/buildtest.yml +++ b/.github/workflows/buildtest.yml @@ -83,6 +83,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 +108,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 }} @@ -135,8 +139,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 +149,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 From 66e6938d2037e07143c48365286d79944b641c23 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 30 Mar 2021 10:43:20 +0200 Subject: [PATCH 07/27] added a few clarifying comments in JaniNextStateGenerator --- src/storm/generator/JaniNextStateGenerator.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index cfe694c2b..9e53c7076 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -550,6 +550,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,10 +563,11 @@ namespace storm { auto transientVariableValuation = getTransientVariableValuationAtLocations(locations, *this->evaluator); transientVariableValuation.setInEvaluator(*this->evaluator, this->getOptions().isExplorationChecksSet()); result.addStateRewards(evaluateRewardExpressions()); + // Set back transient variables to default values so we are ready to process the transition assignments 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) { From 95d53e444b0671fa7b2e05717bcd2c93320cc2f8 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 6 Apr 2021 06:53:35 +0200 Subject: [PATCH 08/27] Fixed an issue with jani::VariablSet using different kinds of variable names when adding and deleting variables. --- src/storm/storage/jani/VariableSet.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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); From d5c6a509a2f214b604c60becc4611fe6415a6789 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 6 Apr 2021 06:54:33 +0200 Subject: [PATCH 09/27] JaniNextStateGenerator: Fixed evaluation of terminal states using expressions over transient variables --- src/storm/generator/JaniNextStateGenerator.cpp | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index 9e53c7076..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); } } } @@ -563,19 +562,22 @@ namespace storm { auto transientVariableValuation = getTransientVariableValuationAtLocations(locations, *this->evaluator); transientVariableValuation.setInEvaluator(*this->evaluator, this->getOptions().isExplorationChecksSet()); result.addStateRewards(evaluateRewardExpressions()); - // Set back transient variables to default values so we are ready to process the transition assignments - 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; From 7cd2394078f358ba4a7ac598ac02fddeb41fdf4d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Basg=C3=B6ze?= Date: Fri, 2 Apr 2021 14:53:32 +0200 Subject: [PATCH 10/27] Make RelevantEvents independent of std::vector Instead use a flexible iterator based api --- src/storm-dft/api/storm-dft.h | 6 +- .../modelchecker/dft/DFTModelChecker.h | 2 +- src/storm-dft/utility/RelevantEvents.h | 100 +++++++++++++----- 3 files changed, 76 insertions(+), 32 deletions(-) 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..4823aad3c 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,19 +16,35 @@ 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) { @@ -39,23 +56,25 @@ namespace storm { } /*! - * 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. * @@ -104,14 +153,9 @@ namespace storm { } private: - - /*! - * Add relevant event. - * - * @param name Name of relevant event. - */ - void addEvent(std::string const& name) { - names.insert(name); + void setAllRelevant() { + this->allRelevant = true; + this->names.clear(); } // Names of relevant events. From 8bccb7ffa10f9b366e92092e1f27657087ca1785 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Basg=C3=B6ze?= Date: Fri, 2 Apr 2021 15:02:46 +0200 Subject: [PATCH 11/27] Fix const correctness in RelevantEvents --- src/storm-dft/utility/RelevantEvents.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm-dft/utility/RelevantEvents.h b/src/storm-dft/utility/RelevantEvents.h index 4823aad3c..4fa2d0769 100644 --- a/src/storm-dft/utility/RelevantEvents.h +++ b/src/storm-dft/utility/RelevantEvents.h @@ -47,11 +47,11 @@ namespace storm { 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); } From c3859ec021a047a221bb0129050ab22a0280e9a4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Basg=C3=B6ze?= Date: Fri, 2 Apr 2021 15:04:27 +0200 Subject: [PATCH 12/27] Add merge operation to RelevantEvents --- src/storm-dft/utility/RelevantEvents.h | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/storm-dft/utility/RelevantEvents.h b/src/storm-dft/utility/RelevantEvents.h index 4fa2d0769..16fde5118 100644 --- a/src/storm-dft/utility/RelevantEvents.h +++ b/src/storm-dft/utility/RelevantEvents.h @@ -152,6 +152,22 @@ namespace storm { } } + /*! + * Merge the given RelevantEvents with *this + * + * @return A reference to *this, allowing chaining i.e. e.merge(a).merge(b) + */ + 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; From aac792bd1d9c8c3a1f3e23329bc7eb4cc6ce8804 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 12 Apr 2021 16:38:44 +0200 Subject: [PATCH 13/27] Updated list of contributers in Readme --- README.md | 2 ++ 1 file changed, 2 insertions(+) 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 From b6c8ab1cf602c77425f611c386eb7a180aba9ba4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Basg=C3=B6ze?= Date: Mon, 12 Apr 2021 14:08:03 +0200 Subject: [PATCH 14/27] Github Actions: use current ref instead of hardcoded master --- .github/workflows/buildtest.yml | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) diff --git a/.github/workflows/buildtest.yml b/.github/workflows/buildtest.yml index 1b998d80a..08f62f29c 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.head_ref || github.sha }}" # 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 @@ -118,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 From b58addcf505feb699412135e8eebce827226b484 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Basg=C3=B6ze?= Date: Tue, 13 Apr 2021 12:53:17 +0200 Subject: [PATCH 15/27] Github Actions: fix PR testing originating from different branches --- .github/workflows/buildtest.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/buildtest.yml b/.github/workflows/buildtest.yml index 08f62f29c..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: "${{ github.head_ref || github.sha }}" + STORM_BRANCH: "${{ github.ref }}" # github runners currently have two cores NR_JOBS: "2" From 871efc0d8c5bba09e1a412923751eb087d25d315 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 14 Apr 2021 16:30:13 +0200 Subject: [PATCH 16/27] Fixed TerminalStatesGetter with multi-bounded formulae. --- src/storm/builder/TerminalStatesGetter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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) { From aa5bb9cb7dbd6f07f815839788a82337f89fcd7f Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 19 Apr 2021 12:21:45 +0200 Subject: [PATCH 17/27] PrismParser: Parsing unbounded integer variables --- src/storm-parsers/parser/PrismParser.cpp | 8 +++++++- src/storm-parsers/parser/PrismParser.h | 4 ++-- 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/src/storm-parsers/parser/PrismParser.cpp b/src/storm-parsers/parser/PrismParser.cpp index 36a01f05f..771578f17 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 2a1d5beeb..0554d088f 100644 --- a/src/storm-parsers/parser/PrismParser.h +++ b/src/storm-parsers/parser/PrismParser.h @@ -240,8 +240,6 @@ namespace storm { // Rules for global variable definitions. qi::rule globalVariableDefinition; - qi::rule globalBooleanVariableDefinition; - qi::rule globalIntegerVariableDefinition; // Rules for modules definition. qi::rule knownModuleName; @@ -254,6 +252,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. From 5c2b9c503c14d1b378617dea509f81b712b3541a Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 19 Apr 2021 12:25:02 +0200 Subject: [PATCH 18/27] prism/Program: Integer variables can now have no lower and/or upper bound. --- src/storm/storage/prism/IntegerVariable.cpp | 54 +++++++- src/storm/storage/prism/IntegerVariable.h | 19 ++- src/storm/storage/prism/Module.cpp | 17 ++- src/storm/storage/prism/Module.h | 5 + src/storm/storage/prism/Program.cpp | 133 ++++++++++++-------- src/storm/storage/prism/Program.h | 5 + 6 files changed, 168 insertions(+), 65 deletions(-) diff --git a/src/storm/storage/prism/IntegerVariable.cpp b/src/storm/storage/prism/IntegerVariable.cpp index d53ea618b..125df94d5 100644 --- a/src/storm/storage/prism/IntegerVariable.cpp +++ b/src/storm/storage/prism/IntegerVariable.cpp @@ -1,35 +1,81 @@ #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()); } 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 67618f6eb..a4faba92a 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 512985ded..bd2e05976 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; } @@ -246,10 +257,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 138dfbe09..2f19ecec7 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 0a892e20c..46db1067a 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -207,7 +207,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()) { @@ -254,10 +268,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; } } @@ -437,7 +451,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) { @@ -1065,37 +1081,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) { @@ -1138,38 +1160,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) { @@ -1623,8 +1652,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 @@ -1642,8 +1670,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()) { @@ -1987,14 +2014,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 496ac7bf8..49db27835 100644 --- a/src/storm/storage/prism/Program.h +++ b/src/storm/storage/prism/Program.h @@ -92,6 +92,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. * From 8f9ff95531b30d121087c30d4ba1f2119f91ae4c Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 19 Apr 2021 12:25:18 +0200 Subject: [PATCH 19/27] Added Test cases for parsing/processing prism programs that use unbounded integer variables --- src/test/storm/parser/PrismParserTest.cpp | 17 +++++++++++++++++ src/test/storm/storage/PrismProgramTest.cpp | 5 ++++- 2 files changed, 21 insertions(+), 1 deletion(-) 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()); } From 171ff270e087ed9e475958e54207c4557e30ce55 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 19 Apr 2021 12:25:56 +0200 Subject: [PATCH 20/27] Prism to Jani conversion now supports unbounded integer variables --- .../storage/jani/UnboundedIntegerVariable.cpp | 9 +++++ .../storage/jani/UnboundedIntegerVariable.h | 5 +++ src/storm/storage/prism/ToJaniConverter.cpp | 38 +++++++++++++++---- 3 files changed, 45 insertions(+), 7 deletions(-) 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/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 { From 9f1c540f050bc3f70ea12e1f8570f381bf1d30f1 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 19 Apr 2021 12:26:51 +0200 Subject: [PATCH 21/27] Counterexamples:making minimal label set generator aware of unbounded integer variables --- .../counterexamples/SMTMinimalLabelSetGenerator.h | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) 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 { From 1fe0254f5d1bbe65dac412836b8fb3885c927187 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 19 Apr 2021 12:27:35 +0200 Subject: [PATCH 22/27] DdPrismModelBuilder now errors in case it has a program with unbounded integer variables as input --- resources/examples/testfiles/mdp/unbounded.nm | 8 ++++++++ src/storm/builder/DdPrismModelBuilder.cpp | 3 ++- src/test/storm/builder/DdPrismModelBuilderTest.cpp | 11 +++++++++++ 3 files changed, 21 insertions(+), 1 deletion(-) create mode 100644 resources/examples/testfiles/mdp/unbounded.nm 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/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/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 From bdd89d87b20bd33f83366339b0b5d5fc35508d62 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 19 Apr 2021 12:28:41 +0200 Subject: [PATCH 23/27] Prism next state generator now deals with unbounded integer variables. --- .../generator/PrismNextStateGenerator.cpp | 2 +- src/storm/generator/VariableInformation.cpp | 108 +++++++++++------- src/storm/generator/VariableInformation.h | 2 +- .../builder/ExplicitPrismModelBuilderTest.cpp | 12 ++ 4 files changed, 81 insertions(+), 43 deletions(-) diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index ead36e763..5bad7e1ba 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/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); +} From a07ee8a018d70f83a2571113bde020f96dfb2a38 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 19 Apr 2021 12:28:55 +0200 Subject: [PATCH 24/27] Updated Changelog --- CHANGELOG.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 65e10cd4b..8ffc256d4 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,4 @@ + Changelog ============== @@ -8,6 +9,7 @@ The releases of major and minor versions contain an overview of changes since th 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. From b3a6d91d5838fcceb6bd0cbf8db690ec3924f813 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 19 Apr 2021 13:17:48 +0200 Subject: [PATCH 25/27] CMake: Changed github address of Carl. --- resources/3rdparty/carl/CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 From a7a10136fa074a7463c785deb06927c061361ba8 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 19 Apr 2021 13:22:16 +0200 Subject: [PATCH 26/27] Cmake: Marking two options as advanced. --- CMakeLists.txt | 2 ++ 1 file changed, 2 insertions(+) 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) From db9097be8c4067a098e31f9edf4d691cfabdbfb3 Mon Sep 17 00:00:00 2001 From: Alex Bork Date: Wed, 28 Apr 2021 16:20:24 +0200 Subject: [PATCH 27/27] Fix for CUDD --- resources/3rdparty/include_cudd.cmake | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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.