Browse Source
Added a pseudo model which can be constructed from only a matrix to look and behave like a model for use in Decomposition classes
Added a pseudo model which can be constructed from only a matrix to look and behave like a model for use in Decomposition classes
Former-commit-id: f8fdc5a9b6
tempestpy_adaptions
PBerger
11 years ago
9 changed files with 304 additions and 103 deletions
-
2src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h
-
108src/models/PseudoModel.cpp
-
90src/models/PseudoModel.h
-
2src/solver/NondeterministicLinearEquationSolver.h
-
105src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp
-
3src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.h
-
5src/storage/Decomposition.h
-
37src/storage/StronglyConnectedComponentDecomposition.cpp
-
55src/storage/StronglyConnectedComponentDecomposition.h
@ -0,0 +1,108 @@ |
|||
#include "src/models/PseudoModel.h"
|
|||
#include "src/utility/constants.h"
|
|||
#include "src/models/AbstractModel.h"
|
|||
|
|||
namespace storm { |
|||
namespace models { |
|||
|
|||
template<typename ValueType> |
|||
ModelBasedPseudoModel<ValueType>::ModelBasedPseudoModel(storm::models::AbstractModel<ValueType> const& model) : _model(model) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template<typename ValueType> |
|||
NonDeterministicMatrixBasedPseudoModel<ValueType>::NonDeterministicMatrixBasedPseudoModel(storm::storage::SparseMatrix<ValueType> const& matrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices) : _matrix(matrix), _nondeterministicChoiceIndices(nondeterministicChoiceIndices) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template<typename ValueType> |
|||
DeterministicMatrixBasedPseudoModel<ValueType>::DeterministicMatrixBasedPseudoModel(storm::storage::SparseMatrix<ValueType> const& matrix) : _matrix(matrix) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template<typename ValueType> |
|||
typename storm::storage::SparseMatrix<ValueType>::const_rows |
|||
ModelBasedPseudoModel<ValueType>::getRows(uint_fast64_t state) const { |
|||
return this->_model.getRows(state); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
typename storm::storage::SparseMatrix<ValueType>::const_rows |
|||
NonDeterministicMatrixBasedPseudoModel<ValueType>::getRows(uint_fast64_t state) const { |
|||
return this->_matrix.getRows(this->_nondeterministicChoiceIndices[state], this->_nondeterministicChoiceIndices[state + 1] - 1); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
typename storm::storage::SparseMatrix<ValueType>::const_rows |
|||
DeterministicMatrixBasedPseudoModel<ValueType>::getRows(uint_fast64_t state) const { |
|||
return this->_matrix.getRows(state, state); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
uint_fast64_t |
|||
ModelBasedPseudoModel<ValueType>::getNumberOfStates() const { |
|||
return this->_model.getNumberOfStates(); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
uint_fast64_t |
|||
NonDeterministicMatrixBasedPseudoModel<ValueType>::getNumberOfStates() const { |
|||
return this->_matrix.getColumnCount(); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
uint_fast64_t |
|||
DeterministicMatrixBasedPseudoModel<ValueType>::getNumberOfStates() const { |
|||
return this->_matrix.getColumnCount(); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
storm::storage::SparseMatrix<ValueType> |
|||
AbstractPseudoModel<ValueType>::extractPartitionDependencyGraph(storm::storage::Decomposition<storm::storage::StateBlock> const& decomposition) const { |
|||
uint_fast64_t numberOfStates = decomposition.size(); |
|||
|
|||
// First, we need to create a mapping of states to their SCC index, to ease the computation of dependency transitions later.
|
|||
std::vector<uint_fast64_t> stateToBlockMap(this->getNumberOfStates()); |
|||
for (uint_fast64_t i = 0; i < decomposition.size(); ++i) { |
|||
for (auto state : decomposition[i]) { |
|||
stateToBlockMap[state] = i; |
|||
} |
|||
} |
|||
|
|||
// The resulting sparse matrix will have as many rows/columns as there are blocks in the partition.
|
|||
storm::storage::SparseMatrixBuilder<ValueType> dependencyGraphBuilder(numberOfStates, numberOfStates); |
|||
|
|||
for (uint_fast64_t currentBlockIndex = 0; currentBlockIndex < decomposition.size(); ++currentBlockIndex) { |
|||
// Get the next block.
|
|||
typename storm::storage::StateBlock const& block = decomposition[currentBlockIndex]; |
|||
|
|||
// Now, we determine the blocks which are reachable (in one step) from the current block.
|
|||
boost::container::flat_set<uint_fast64_t> allTargetBlocks; |
|||
for (auto state : block) { |
|||
for (auto const& transitionEntry : this->getRows(state)) { |
|||
uint_fast64_t targetBlock = stateToBlockMap[transitionEntry.first]; |
|||
|
|||
// We only need to consider transitions that are actually leaving the SCC.
|
|||
if (targetBlock != currentBlockIndex) { |
|||
allTargetBlocks.insert(targetBlock); |
|||
} |
|||
} |
|||
} |
|||
|
|||
// Now we can just enumerate all the target SCCs and insert the corresponding transitions.
|
|||
for (auto targetBlock : allTargetBlocks) { |
|||
dependencyGraphBuilder.addNextValue(currentBlockIndex, targetBlock, storm::utility::constantOne<ValueType>()); |
|||
} |
|||
} |
|||
|
|||
return dependencyGraphBuilder.build(); |
|||
} |
|||
|
|||
template class ModelBasedPseudoModel<double>; |
|||
template class NonDeterministicMatrixBasedPseudoModel<double>; |
|||
template class DeterministicMatrixBasedPseudoModel<double>; |
|||
template class ModelBasedPseudoModel<int>; |
|||
template class NonDeterministicMatrixBasedPseudoModel<int>; |
|||
template class DeterministicMatrixBasedPseudoModel<int>; |
|||
} // namespace models
|
|||
} // namespace storm
|
|||
@ -0,0 +1,90 @@ |
|||
#ifndef STORM_MODELS_PSEUDOMODEL_H_ |
|||
#define STORM_MODELS_PSEUDOMODEL_H_ |
|||
|
|||
#include <cstdint> |
|||
#include "src/storage/SparseMatrix.h" |
|||
#include "src/storage/Decomposition.h" |
|||
|
|||
namespace storm { |
|||
namespace models { |
|||
// Forward declare the abstract model class. |
|||
template <typename ValueType> class AbstractModel; |
|||
|
|||
/*! |
|||
* This classes encapsulate the model/transitionmatrix on which the SCC decomposition is performed. |
|||
* The Abstract Base class is specialized by the two possible representations: |
|||
* - For a model the implementation ModelBasedPseudoModel hands the call to getRows() through to the model |
|||
* - For a matrix of a nondeterministic model the implementation NonDeterministicMatrixBasedPseudoModel emulates the call |
|||
* on the matrix itself like the model function would |
|||
* - For a matrix of a deterministic model the implementation DeterministicMatrixBasedPseudoModel emulates the call |
|||
* on the matrix itself like the model function would |
|||
*/ |
|||
template <typename ValueType> |
|||
class AbstractPseudoModel { |
|||
public: |
|||
AbstractPseudoModel() {} |
|||
virtual ~AbstractPseudoModel() {} |
|||
|
|||
virtual typename storm::storage::SparseMatrix<ValueType>::const_rows getRows(uint_fast64_t state) const = 0; |
|||
|
|||
/*! |
|||
* Calculates the number of states in the represented system. |
|||
* @return The Number of States in the underlying model/transition matrix |
|||
*/ |
|||
virtual uint_fast64_t getNumberOfStates() const = 0; |
|||
|
|||
/*! |
|||
* Extracts the dependency graph from a (pseudo-) model according to the given partition. |
|||
* |
|||
* @param decomposition A decomposition containing the blocks of the partition of the system. |
|||
* @return A sparse matrix with bool entries that represents the dependency graph of the blocks of the partition. |
|||
*/ |
|||
virtual storm::storage::SparseMatrix<ValueType> extractPartitionDependencyGraph(storm::storage::Decomposition<storm::storage::StateBlock> const& decomposition) const; |
|||
}; |
|||
|
|||
template <typename ValueType> |
|||
class ModelBasedPseudoModel : public AbstractPseudoModel<ValueType> { |
|||
public: |
|||
/*! |
|||
* Creates an encapsulation for the SCC decomposition based on a model |
|||
* @param model The Model on which the decomposition is to be performed |
|||
*/ |
|||
ModelBasedPseudoModel(storm::models::AbstractModel<ValueType> const& model); |
|||
virtual typename storm::storage::SparseMatrix<ValueType>::const_rows getRows(uint_fast64_t state) const override; |
|||
virtual uint_fast64_t getNumberOfStates() const override; |
|||
private: |
|||
storm::models::AbstractModel<ValueType> const& _model; |
|||
}; |
|||
|
|||
template <typename ValueType> |
|||
class NonDeterministicMatrixBasedPseudoModel : public AbstractPseudoModel<ValueType> { |
|||
public: |
|||
/*! |
|||
* Creates an encapsulation for the SCC decomposition based on a matrix |
|||
* @param matrix The Matrix on which the decomposition is to be performed |
|||
*/ |
|||
NonDeterministicMatrixBasedPseudoModel(storm::storage::SparseMatrix<ValueType> const& matrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices); |
|||
virtual typename storm::storage::SparseMatrix<ValueType>::const_rows getRows(uint_fast64_t state) const override; |
|||
virtual uint_fast64_t getNumberOfStates() const override; |
|||
private: |
|||
storm::storage::SparseMatrix<ValueType> const& _matrix; |
|||
std::vector<uint_fast64_t> const& _nondeterministicChoiceIndices; |
|||
}; |
|||
|
|||
template <typename ValueType> |
|||
class DeterministicMatrixBasedPseudoModel : public AbstractPseudoModel<ValueType> { |
|||
public: |
|||
/*! |
|||
* Creates an encapsulation for the SCC decomposition based on a matrix |
|||
* @param matrix The Matrix on which the decomposition is to be performed |
|||
*/ |
|||
DeterministicMatrixBasedPseudoModel(storm::storage::SparseMatrix<ValueType> const& matrix); |
|||
virtual typename storm::storage::SparseMatrix<ValueType>::const_rows getRows(uint_fast64_t state) const override; |
|||
virtual uint_fast64_t getNumberOfStates() const override; |
|||
private: |
|||
storm::storage::SparseMatrix<ValueType> const& _matrix; |
|||
}; |
|||
} |
|||
} |
|||
|
|||
#endif // STORM_MODELS_PSEUDOMODEL_H_ |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue