diff --git a/CHANGELOG.md b/CHANGELOG.md index 0f7f73282..2f9274625 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,17 +4,20 @@ Changelog This changelog lists only the most important changes. Smaller (bug)fixes as well as non-mature features are not part of the changelog. The releases of major and minor versions contain an overview of changes since the last major/minor update. -Version 1.2.x +Version 1.3.x ------------- -### Version 1.2.4 (2018/08) + +### Version 1.3.0 (2018/12) +- Slightly improved scheduler extraction +- Environments are now part of the c++ API - Heavily extended JANI support, in particular: * arrays, functions, state-exit-rewards (all engines) * indexed assignments, complex reward expressions (sparse engine) * several jani-related bug fixes - New binary `storm-conv` that handles conversions between model files - New binary `storm-pomdp` that handles the translation of POMDPs to pMCs. -- Closing a Markov automaton now removes unreachable states +- Maximal progress assumption is now applied while building Markov Automata (sparse engine). - Added support for expected time properties for discrete time models - Bug fix in the parser for DRN (MDPs and MAs might have been affected). - `storm-gspn`: Improved .pnpro parser @@ -22,6 +25,21 @@ Version 1.2.x - `storm-gspn`: Added option to set a global capacity for all places - `storm-gspn`: Added option to include a set of standard properties when converting GSPNs to jani - `storm-pars`: Added possibility to compute the extremal value within a given region using parameter lifting +- `storm-dft`: DFT translation to GSPN supports Don't Care propagation +- `storm-dft`: Support DFT analysis via transformation from DFT to GSPN to JANI +- `storm-dft`: Added SMT encoding for DFTs +- `storm-dft`: Improved Galileo and JSON parser +- Several bug fixes + +### Comparison with Version 1.2.0 (details see below) +- Heavily extended JANI-support +- New binary `storm-conv` that handles conversion between model files +- New binary `storm-pomdp` that handles the translation of POMDPs to pMCs. +- `storm-gspn` improved +- Sound value iteration + +Version 1.2.x +------------- ### Version 1.2.3 (2018/07) - Fix in version parsing diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 7a5b6d13d..4c7a9f01b 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -148,7 +148,9 @@ namespace storm { bool transformToJani = ioSettings.isPrismToJaniSet(); bool transformToJaniForJit = builderType == storm::builder::BuilderType::Jit; STORM_LOG_WARN_COND(transformToJani || !transformToJaniForJit, "The JIT-based model builder is only available for JANI models, automatically converting the PRISM input model."); - transformToJani |= transformToJaniForJit; + bool transformToJaniForDdMA = (builderType == storm::builder::BuilderType::Dd) && (input.model->getModelType() == storm::storage::SymbolicModelDescription::ModelType::MA); + STORM_LOG_WARN_COND(transformToJani || !transformToJaniForDdMA, "Dd-based model builder for Markov Automata is only available for JANI models, automatically converting the PRISM input model."); + transformToJani |= (transformToJaniForJit || transformToJaniForDdMA); if (transformToJani) { storm::prism::Program const& model = output.model.get().asPrismProgram(); diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 634eaf806..2f247b8bd 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -52,7 +52,7 @@ namespace storm { storm::storage::BitVector statesWithProbabilityGreater0NonPsi = statesWithProbabilityGreater0 & ~psiStates; STORM_LOG_INFO("Found " << statesWithProbabilityGreater0NonPsi.getNumberOfSetBits() << " 'maybe' states."); - if (!statesWithProbabilityGreater0NonPsi.empty()) { + if (!statesWithProbabilityGreater0.empty()) { if (storm::utility::isZero(upperBound)) { // In this case, the interval is of the form [0, 0]. result = std::vector(numberOfStates, storm::utility::zero()); @@ -62,30 +62,31 @@ namespace storm { // In this case, the interval is of the form [0, t]. // Note that this excludes [0, inf] since this is untimed reachability and we considered this case earlier. - // Find the maximal rate of all 'maybe' states to take it as the uniformization rate. - ValueType uniformizationRate = 0; - for (auto const& state : statesWithProbabilityGreater0NonPsi) { - uniformizationRate = std::max(uniformizationRate, exitRates[state]); - } - uniformizationRate *= 1.02; - STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); - - // Compute the uniformized matrix. - storm::storage::SparseMatrix uniformizedMatrix = computeUniformizedMatrix(rateMatrix, statesWithProbabilityGreater0NonPsi, uniformizationRate, exitRates); - - // Compute the vector that is to be added as a compensation for removing the absorbing states. - std::vector b = rateMatrix.getConstrainedRowSumVector(statesWithProbabilityGreater0NonPsi, psiStates); - for (auto& element : b) { - element /= uniformizationRate; - } - - // Finally compute the transient probabilities. - std::vector values(statesWithProbabilityGreater0NonPsi.getNumberOfSetBits(), storm::utility::zero()); - std::vector subresult = computeTransientProbabilities(env, uniformizedMatrix, &b, upperBound, uniformizationRate, values); result = std::vector(numberOfStates, storm::utility::zero()); - - storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0NonPsi, subresult); - storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); + storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); + if (!statesWithProbabilityGreater0NonPsi.empty()) { + // Find the maximal rate of all 'maybe' states to take it as the uniformization rate. + ValueType uniformizationRate = 0; + for (auto const& state : statesWithProbabilityGreater0NonPsi) { + uniformizationRate = std::max(uniformizationRate, exitRates[state]); + } + uniformizationRate *= 1.02; + STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); + + // Compute the uniformized matrix. + storm::storage::SparseMatrix uniformizedMatrix = computeUniformizedMatrix(rateMatrix, statesWithProbabilityGreater0NonPsi, uniformizationRate, exitRates); + + // Compute the vector that is to be added as a compensation for removing the absorbing states. + std::vector b = rateMatrix.getConstrainedRowSumVector(statesWithProbabilityGreater0NonPsi, psiStates); + for (auto& element : b) { + element /= uniformizationRate; + } + + // Finally compute the transient probabilities. + std::vector values(statesWithProbabilityGreater0NonPsi.getNumberOfSetBits(), storm::utility::zero()); + std::vector subresult = computeTransientProbabilities(env, uniformizedMatrix, &b, upperBound, uniformizationRate, values); + storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0NonPsi, subresult); + } } else if (upperBound == storm::utility::infinity()) { // In this case, the interval is of the form [t, inf] with t != 0. @@ -120,35 +121,38 @@ namespace storm { if (lowerBound != upperBound) { // In this case, the interval is of the form [t, t'] with t != 0, t' != inf and t != t'. - // Find the maximal rate of all 'maybe' states to take it as the uniformization rate. - ValueType uniformizationRate = storm::utility::zero(); - for (auto const& state : statesWithProbabilityGreater0NonPsi) { - uniformizationRate = std::max(uniformizationRate, exitRates[state]); - } - uniformizationRate *= 1.02; - STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); - - // Compute the (first) uniformized matrix. - storm::storage::SparseMatrix uniformizedMatrix = computeUniformizedMatrix(rateMatrix, statesWithProbabilityGreater0NonPsi, uniformizationRate, exitRates); - - // Compute the vector that is to be added as a compensation for removing the absorbing states. - std::vector b = rateMatrix.getConstrainedRowSumVector(statesWithProbabilityGreater0NonPsi, psiStates); - for (auto& element : b) { - element /= uniformizationRate; - } - - // Start by computing the transient probabilities of reaching a psi state in time t' - t. - std::vector values(statesWithProbabilityGreater0NonPsi.getNumberOfSetBits(), storm::utility::zero()); - std::vector subresult = computeTransientProbabilities(env, uniformizedMatrix, &b, upperBound - lowerBound, uniformizationRate, values); storm::storage::BitVector relevantStates = statesWithProbabilityGreater0 & phiStates; - std::vector newSubresult = std::vector(relevantStates.getNumberOfSetBits()); - storm::utility::vector::setVectorValues(newSubresult, statesWithProbabilityGreater0NonPsi % relevantStates, subresult); + std::vector newSubresult(relevantStates.getNumberOfSetBits(), storm::utility::zero()); storm::utility::vector::setVectorValues(newSubresult, psiStates % relevantStates, storm::utility::one()); + if (!statesWithProbabilityGreater0NonPsi.empty()) { + // Find the maximal rate of all 'maybe' states to take it as the uniformization rate. + ValueType uniformizationRate = storm::utility::zero(); + for (auto const& state : statesWithProbabilityGreater0NonPsi) { + uniformizationRate = std::max(uniformizationRate, exitRates[state]); + } + uniformizationRate *= 1.02; + STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); + + // Compute the (first) uniformized matrix. + storm::storage::SparseMatrix uniformizedMatrix = computeUniformizedMatrix(rateMatrix, statesWithProbabilityGreater0NonPsi, uniformizationRate, exitRates); + + // Compute the vector that is to be added as a compensation for removing the absorbing states. + std::vector b = rateMatrix.getConstrainedRowSumVector(statesWithProbabilityGreater0NonPsi, psiStates); + for (auto& element : b) { + element /= uniformizationRate; + } + + // Start by computing the transient probabilities of reaching a psi state in time t' - t. + std::vector values(statesWithProbabilityGreater0NonPsi.getNumberOfSetBits(), storm::utility::zero()); + std::vector subresult = computeTransientProbabilities(env, uniformizedMatrix, &b, upperBound - lowerBound, uniformizationRate, values); + newSubresult = std::vector(relevantStates.getNumberOfSetBits()); + storm::utility::vector::setVectorValues(newSubresult, statesWithProbabilityGreater0NonPsi % relevantStates, subresult); + } // Then compute the transient probabilities of being in such a state after t time units. For this, // we must re-uniformize the CTMC, so we need to compute the second uniformized matrix. - uniformizationRate = storm::utility::zero(); + ValueType uniformizationRate = storm::utility::zero(); for (auto const& state : relevantStates) { uniformizationRate = std::max(uniformizationRate, exitRates[state]); } @@ -156,7 +160,7 @@ namespace storm { STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); // Finally, we compute the second set of transient probabilities. - uniformizedMatrix = computeUniformizedMatrix(rateMatrix, relevantStates, uniformizationRate, exitRates); + storm::storage::SparseMatrix uniformizedMatrix = computeUniformizedMatrix(rateMatrix, relevantStates, uniformizationRate, exitRates); newSubresult = computeTransientProbabilities(env, uniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult); // Fill in the correct values. diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index ccc0cc324..b2fcad350 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -1092,7 +1092,7 @@ namespace storm { } // Check for convergence - if ((maxDiff - minDiff) <= (relative ? (precision * minDiff) : precision)) { + if ((maxDiff - minDiff) <= (relative ? (precision * (v.front() + minDiff)) : precision)) { break; } diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp index bed0ab312..1f517fc10 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -51,6 +51,7 @@ namespace storm { if (!this->sortedSccDecomposition || (needAdaptPrecision && !this->longestSccChainSize)) { STORM_LOG_TRACE("Creating SCC decomposition."); createSortedSccDecomposition(needAdaptPrecision); + STORM_LOG_INFO("Found " << this->sortedSccDecomposition->size() << " SCC(s). Average size is " << static_cast(this->A->getRowGroupCount()) / static_cast(this->sortedSccDecomposition->size()) << "."); } // We do not need to adapt the precision if all SCCs are trivial (i.e., the system is acyclic) @@ -58,7 +59,6 @@ namespace storm { storm::Environment sccSolverEnvironment = getEnvironmentForUnderlyingSolver(env, needAdaptPrecision); - STORM_LOG_INFO("Found " << this->sortedSccDecomposition->size() << " SCC(s). Average size is " << static_cast(this->A->getRowGroupCount()) / static_cast(this->sortedSccDecomposition->size()) << "."); if (this->longestSccChainSize) { STORM_LOG_INFO("Longest SCC chain size is " << this->longestSccChainSize.get()); } diff --git a/src/storm/storage/SymbolicModelDescription.cpp b/src/storm/storage/SymbolicModelDescription.cpp index 9a7bc1388..243cb8372 100644 --- a/src/storm/storage/SymbolicModelDescription.cpp +++ b/src/storm/storage/SymbolicModelDescription.cpp @@ -63,6 +63,7 @@ namespace storm { case storm::prism::Program::ModelType::DTMC: return SymbolicModelDescription::ModelType::DTMC; case storm::prism::Program::ModelType::CTMC: return SymbolicModelDescription::ModelType::CTMC; case storm::prism::Program::ModelType::MDP: return SymbolicModelDescription::ModelType::MDP; + case storm::prism::Program::ModelType::POMDP: return SymbolicModelDescription::ModelType::POMDP; case storm::prism::Program::ModelType::MA: return SymbolicModelDescription::ModelType::MA; default: STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Expected other PRISM model type."); diff --git a/src/storm/storage/SymbolicModelDescription.h b/src/storm/storage/SymbolicModelDescription.h index a22e3afd6..fb1f0e2ac 100644 --- a/src/storm/storage/SymbolicModelDescription.h +++ b/src/storm/storage/SymbolicModelDescription.h @@ -11,7 +11,7 @@ namespace storm { class SymbolicModelDescription { public: enum class ModelType { - DTMC, CTMC, MDP, MA + DTMC, CTMC, MDP, MA, POMDP }; SymbolicModelDescription() = default;