sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Merge branch 'master' into unifplus_refactor

main
Matthias Volk 6 years ago
parent
230ac20480 2197f3c34a
commit
8c572ba550
7 changed files with 80 additions and 55 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 24
      CHANGELOG.md
  2. 4
      src/storm-cli-utilities/model-handling.h
  3. 100
      src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
  4. 2
      src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
  5. 2
      src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp
  6. 1
      src/storm/storage/SymbolicModelDescription.cpp
  7. 2
      src/storm/storage/SymbolicModelDescription.h

24
CHANGELOG.md
View File

@ -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

4
src/storm-cli-utilities/model-handling.h
View File

@ -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();

100
src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
View File

@ -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.

2
src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
View File

@ -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;
}

2
src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp
View File

@ -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());
}

1
src/storm/storage/SymbolicModelDescription.cpp
View File

@ -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.");

2
src/storm/storage/SymbolicModelDescription.h
View File

@ -11,7 +11,7 @@ namespace storm {
class SymbolicModelDescription {
public:
enum class ModelType {
DTMC, CTMC, MDP, MA
DTMC, CTMC, MDP, MA, POMDP
};
SymbolicModelDescription() = default;

Write Preview
Loading…
Cancel
Save