From c1119fcd8d418d271df497cd17f2bc9ae4605869 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 7 Dec 2018 11:26:53 +0100
Subject: [PATCH 1/8] Triggered conversion from PRISM to JANI when building an
MA with the dd engine since MAs are unsupported in the DdPrismModelBuilder.
---
src/storm-cli-utilities/model-handling.h | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
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();
From cab2b3d8f1e349bb92eb3498becd4c654267aeb4 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Fri, 7 Dec 2018 11:41:04 +0100
Subject: [PATCH 2/8] changelog preparation for version 1.3.0
---
CHANGELOG.md | 16 ++++++++++++++++
1 file changed, 16 insertions(+)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 0f7f73282..88b9d62f0 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -4,6 +4,22 @@ 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.3.x
+-------------
+
+
+### Version 1.3.0 (2018/12)
+- Slightly improved scheduler extraction
+- Environments are now part of the c++ API
+
+
+### 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
-------------
From 03b5c70c79e5fa376e177d3bab3c082ac5ef62cd Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Fri, 7 Dec 2018 13:12:46 +0100
Subject: [PATCH 3/8] support for POMDPs in symoblic description
---
src/storm/storage/SymbolicModelDescription.cpp | 1 +
src/storm/storage/SymbolicModelDescription.h | 2 +-
2 files changed, 2 insertions(+), 1 deletion(-)
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;
From 384e7ace069905c57cb9cdff3d218cc8597d9d6b Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 7 Dec 2018 16:05:08 +0100
Subject: [PATCH 4/8] TopologicalMinMaxLinearEquationSolver: Reduced clutter in
the --verbose output.
---
src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
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<double>(this->A->getRowGroupCount()) / static_cast<double>(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<double>(this->A->getRowGroupCount()) / static_cast<double>(this->sortedSccDecomposition->size()) << ".");
if (this->longestSccChainSize) {
STORM_LOG_INFO("Longest SCC chain size is " << this->longestSccChainSize.get());
}
From 0c905e23230ef0ec1901891b28a30e2b1c1414ff Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 7 Dec 2018 16:06:04 +0100
Subject: [PATCH 5/8] Fixed an issue where time-bounded properties were wrongly
computed on a ctmc that only consists of goal-states.
---
.../csl/helper/SparseCtmcCslHelper.cpp | 100 +++++++++---------
1 file changed, 52 insertions(+), 48 deletions(-)
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<ValueType>(numberOfStates, storm::utility::zero<ValueType>());
@@ -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<ValueType> uniformizedMatrix = computeUniformizedMatrix(rateMatrix, statesWithProbabilityGreater0NonPsi, uniformizationRate, exitRates);
-
- // Compute the vector that is to be added as a compensation for removing the absorbing states.
- std::vector<ValueType> b = rateMatrix.getConstrainedRowSumVector(statesWithProbabilityGreater0NonPsi, psiStates);
- for (auto& element : b) {
- element /= uniformizationRate;
- }
-
- // Finally compute the transient probabilities.
- std::vector<ValueType> values(statesWithProbabilityGreater0NonPsi.getNumberOfSetBits(), storm::utility::zero<ValueType>());
- std::vector<ValueType> subresult = computeTransientProbabilities(env, uniformizedMatrix, &b, upperBound, uniformizationRate, values);
result = std::vector<ValueType>(numberOfStates, storm::utility::zero<ValueType>());
-
- storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0NonPsi, subresult);
- storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one<ValueType>());
+ storm::utility::vector::setVectorValues<ValueType>(result, psiStates, storm::utility::one<ValueType>());
+ 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<ValueType> uniformizedMatrix = computeUniformizedMatrix(rateMatrix, statesWithProbabilityGreater0NonPsi, uniformizationRate, exitRates);
+
+ // Compute the vector that is to be added as a compensation for removing the absorbing states.
+ std::vector<ValueType> b = rateMatrix.getConstrainedRowSumVector(statesWithProbabilityGreater0NonPsi, psiStates);
+ for (auto& element : b) {
+ element /= uniformizationRate;
+ }
+
+ // Finally compute the transient probabilities.
+ std::vector<ValueType> values(statesWithProbabilityGreater0NonPsi.getNumberOfSetBits(), storm::utility::zero<ValueType>());
+ std::vector<ValueType> subresult = computeTransientProbabilities(env, uniformizedMatrix, &b, upperBound, uniformizationRate, values);
+ storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0NonPsi, subresult);
+ }
} else if (upperBound == storm::utility::infinity<ValueType>()) {
// 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<ValueType>();
- 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<ValueType> uniformizedMatrix = computeUniformizedMatrix(rateMatrix, statesWithProbabilityGreater0NonPsi, uniformizationRate, exitRates);
-
- // Compute the vector that is to be added as a compensation for removing the absorbing states.
- std::vector<ValueType> 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<ValueType> values(statesWithProbabilityGreater0NonPsi.getNumberOfSetBits(), storm::utility::zero<ValueType>());
- std::vector<ValueType> subresult = computeTransientProbabilities(env, uniformizedMatrix, &b, upperBound - lowerBound, uniformizationRate, values);
storm::storage::BitVector relevantStates = statesWithProbabilityGreater0 & phiStates;
- std::vector<ValueType> newSubresult = std::vector<ValueType>(relevantStates.getNumberOfSetBits());
- storm::utility::vector::setVectorValues(newSubresult, statesWithProbabilityGreater0NonPsi % relevantStates, subresult);
+ std::vector<ValueType> newSubresult(relevantStates.getNumberOfSetBits(), storm::utility::zero<ValueType>());
storm::utility::vector::setVectorValues(newSubresult, psiStates % relevantStates, storm::utility::one<ValueType>());
+ if (!statesWithProbabilityGreater0NonPsi.empty()) {
+ // Find the maximal rate of all 'maybe' states to take it as the uniformization rate.
+ ValueType uniformizationRate = storm::utility::zero<ValueType>();
+ 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<ValueType> uniformizedMatrix = computeUniformizedMatrix(rateMatrix, statesWithProbabilityGreater0NonPsi, uniformizationRate, exitRates);
+
+ // Compute the vector that is to be added as a compensation for removing the absorbing states.
+ std::vector<ValueType> 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<ValueType> values(statesWithProbabilityGreater0NonPsi.getNumberOfSetBits(), storm::utility::zero<ValueType>());
+ std::vector<ValueType> subresult = computeTransientProbabilities(env, uniformizedMatrix, &b, upperBound - lowerBound, uniformizationRate, values);
+ newSubresult = std::vector<ValueType>(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>();
+ ValueType uniformizationRate = storm::utility::zero<ValueType>();
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<ValueType> uniformizedMatrix = computeUniformizedMatrix(rateMatrix, relevantStates, uniformizationRate, exitRates);
newSubresult = computeTransientProbabilities<ValueType>(env, uniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult);
// Fill in the correct values.
From 629de20da04e66901eaee5b99f3250c38afb49dc Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 7 Dec 2018 16:06:45 +0100
Subject: [PATCH 6/8] Fixed running in an infinite loop when computing LRA on
markov automata with relative precision.
---
.../modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
index a0c8829bc..c78948727 100644
--- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
+++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
@@ -1047,7 +1047,7 @@ namespace storm {
}
// Check for convergence
- if ((maxDiff - minDiff) <= (relative ? (precision * minDiff) : precision)) {
+ if ((maxDiff - minDiff) <= (relative ? (precision * (v.front() + minDiff)) : precision)) {
break;
}
From aacdf5c0b5fd5d8cb700b3d22ff6793bcd1afa02 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 7 Dec 2018 16:16:47 +0100
Subject: [PATCH 7/8] Updated changelog.
---
CHANGELOG.md | 25 +++++++++++--------------
1 file changed, 11 insertions(+), 14 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 88b9d62f0..665781bd9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -11,26 +11,13 @@ Version 1.3.x
### Version 1.3.0 (2018/12)
- Slightly improved scheduler extraction
- Environments are now part of the c++ API
-
-
-### 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.4 (2018/08)
- 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
@@ -39,6 +26,16 @@ Version 1.2.x
- `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
+### 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
From 2197f3c34a2f27b748669dd8182fc1d74e24273b Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Fri, 7 Dec 2018 16:47:35 +0100
Subject: [PATCH 8/8] Updated changelog
---
CHANGELOG.md | 5 +++++
1 file changed, 5 insertions(+)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 665781bd9..2f9274625 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -25,6 +25,11 @@ Version 1.3.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