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

Temporarily split new approximating state generation into own builder 

Former-commit-id: 70be02f2ae
main
Mavo 9 years ago
parent
12f7c08bac
commit
495b42ff4c
10 changed files with 875 additions and 82 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. 58
      examples/dft/mas.dft
  2. 8
      examples/dft/nonmonoton_param.dft
  3. 40
      src/builder/ExplicitDFTModelBuilder.cpp
  4. 3
      src/builder/ExplicitDFTModelBuilder.h
  5. 666
      src/builder/ExplicitDFTModelBuilderApprox.cpp
  6. 105
      src/builder/ExplicitDFTModelBuilderApprox.h
  7. 31
      src/generator/DftNextStateGenerator.cpp
  8. 15
      src/generator/DftNextStateGenerator.h
  9. 30
      src/modelchecker/DFTAnalyser.h
  10. 1
      src/storage/sparse/StateStorage.cpp

58
examples/dft/mas.dft
View File

@ -0,0 +1,58 @@
toplevel "MAS";
"MAS" or "CPU" "DB" "MB" "VMB" "MEM" "VMS";
"CPU" or "CW" "SO1" "SO2" "PG" "SM";
"CW" and "CWA" "CWB";
"SO1" and "SO1A" "SO1B";
"SO2" and "SO2A" "SO2B";
"PG" and "PGA" "PGB";
"SM" and "SMA" "SMB";
"CWA" csp "CWAev" "S1" "S2";
"CWB" csp "CWBev" "S1" "S2";
"SO1A" csp "SO1Aev" "S1" "S2";
"SO1B" csp "SO1Bev" "S1" "S2";
"SO2A" csp "SO2Aev" "S1" "S2";
"SO2B" csp "SO2Bev" "S1" "S2";
"PGA" csp "PGAev" "S1" "S2";
"PGB" csp "PGBev" "S1" "S2";
"SMA" csp "SMAev" "S1" "S2";
"SMB" csp "SMBev" "S1" "S2";
"CWAev" lambda=1.0e-6 dorm=0;
"CWBev" lambda=1.0e-6 dorm=0;
"SO1Aev" lambda=1.0e-6 dorm=0;
"SO1Bev" lambda=1.0e-6 dorm=0;
"SO2Aev" lambda=1.0e-6 dorm=0;
"SO2Bev" lambda=1.0e-6 dorm=0;
"PGAev" lambda=1.0e-6 dorm=0;
"PGBev" lambda=1.0e-6 dorm=0;
"SMAev" lambda=1.0e-6 dorm=0;
"SMBev" lambda=1.0e-6 dorm=0;
"S1" lambda=1.0e-6 dorm=0;
"S2" lambda=1.0e-6 dorm=0;
"DB" and "DB1" "DB2" "DB3";
"DB1" lambda=5.0e-6 dorm=0;
"DB2" lambda=5.0e-6 dorm=0;
"DB3" lambda=5.0e-6 dorm=0;
"MB" and "MB1" "MB2" "MB3";
"MB1" lambda=5.0e-6 dorm=0;
"MB2" lambda=5.0e-6 dorm=0;
"MB3" lambda=5.0e-6 dorm=0;
"VMB" and "VMB1" "VMB2";
"VMB1" lambda=5.0e-6 dorm=0;
"VMB2" lambda=5.0e-6 dorm=0;
"MEM" and "MEM1" "MEM2";
"MEM1" lambda=1.0e-5 dorm=0;
"MEM2" lambda=1.0e-5 dorm=0;
"VMS" or "VM1" "VM2";
"VM1" and "VM1A" "VM1B";
"VM2" and "VM2A" "VM2B";
"VM1A" csp "VM1Aev" "VMS1" "VMS2";
"VM1B" csp "VM1Bev" "VMS1" "VMS2";
"VM2A" csp "VM2Aev" "VMS1" "VMS2";
"VM2B" csp "VM2Bev" "VMS1" "VMS2";
"VM1Aev" lambda=1.0e-6 dorm=0;
"VM1Bev" lambda=1.0e-6 dorm=0;
"VM2Aev" lambda=1.0e-6 dorm=0;
"VM2Bev" lambda=1.0e-6 dorm=0;
"VMS1" lambda=1.0e-6 dorm=0;
"VMS2" lambda=1.0e-6 dorm=0;

8
examples/dft/nonmonoton_param.dft
View File

@ -2,7 +2,7 @@ param x;
param y;
toplevel "A";
"A" or "B" "Z";
"B" pand "D" "S";
"Z" lambda=y dorm=0;
"D" lambda=100 dorm=0;
"S" lambda=100*x dorm=0;
"Z" pand "C" "D";
"B" lambda=y dorm=0;
"C" lambda=100 dorm=0;
"D" lambda=100*x dorm=0;

40
src/builder/ExplicitDFTModelBuilder.cpp
View File

@ -160,23 +160,6 @@ namespace storm {
return model;
}
template<>
bool belowThreshold(double const& number) {
return number < 0.1;
}
template<>
bool belowThreshold(storm::RationalFunction const& number) {
storm::RationalFunction threshold = storm::utility::one<storm::RationalFunction>() / 10;
std::cout << number << " < " << threshold << ": " << (number < threshold) << std::endl;
std::map<storm::Variable, storm::RationalNumber> mapping;
storm::RationalFunction eval(number.evaluate(mapping));
std::cout << "Evaluated: " << eval << std::endl;
return eval < threshold;
}
template <typename ValueType>
std::pair<uint_fast64_t, bool> ExplicitDFTModelBuilder<ValueType>::exploreStates(DFTStatePointer const& state, size_t& rowOffset, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<uint_fast64_t>& markovianStates, std::vector<ValueType>& exitRates) {
STORM_LOG_TRACE("Explore state: " << mDft.getStateString(state));
@ -225,29 +208,6 @@ namespace storm {
STORM_LOG_ASSERT(nextBE, "NextBE is null.");
STORM_LOG_ASSERT(nextBEPair.second == hasDependencies, "Failure due to dependencies does not match.");
STORM_LOG_TRACE("With the failure of: " << nextBE->name() << " [" << nextBE->id() << "] in " << mDft.getStateString(state));
if (storm::settings::getModule<storm::settings::modules::DFTSettings>().computeApproximation()) {
if (!storm::utility::isZero(exitRate)) {
ValueType rate = nextBE->activeFailureRate();
ValueType div = rate / exitRate;
if (!storm::utility::isZero(exitRate) && belowThreshold(div)) {
// Set transition directly to failed state
auto resultFind = outgoingRates.find(failedIndex);
if (resultFind != outgoingRates.end()) {
// Add to existing transition
resultFind->second += rate;
STORM_LOG_TRACE("Updated transition to " << resultFind->first << " with rate " << rate << " to new rate " << resultFind->second);
} else {
// Insert new transition
outgoingRates.insert(std::make_pair(failedIndex, rate));
STORM_LOG_TRACE("Added transition to " << failedIndex << " with rate " << rate);
}
exitRate += rate;
std::cout << "IGNORE: " << nextBE->name() << " [" << nextBE->id() << "] with rate " << rate << std::endl;
//STORM_LOG_TRACE("Ignore: " << nextBE->name() << " [" << nextBE->id() << "] with rate " << rate);
continue;
}}
}
// Propagate failures
storm::storage::DFTStateSpaceGenerationQueues<ValueType> queues;

3
src/builder/ExplicitDFTModelBuilder.h
View File

@ -91,9 +91,6 @@ namespace storm {
std::pair<bool, uint_fast64_t> checkForExploration(DFTStatePointer const& state);
};
template<typename ValueType>
bool belowThreshold(ValueType const& number);
}
}

666
src/builder/ExplicitDFTModelBuilderApprox.cpp
View File

@ -0,0 +1,666 @@
#include "src/builder/ExplicitDFTModelBuilderApprox.h"
#include <src/models/sparse/MarkovAutomaton.h>
#include <src/models/sparse/Ctmc.h>
#include <src/utility/constants.h>
#include <src/utility/vector.h>
#include <src/exceptions/UnexpectedException.h>
#include "src/settings/modules/DFTSettings.h"
#include "src/settings/SettingsManager.h"
#include "src/generator/DftNextStateGenerator.h"
#include <map>
namespace storm {
namespace builder {
template <typename ValueType>
ExplicitDFTModelBuilderApprox<ValueType>::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), markovianStates(), exitRates(), choiceLabeling() {
// Intentionally left empty.
}
template <typename ValueType>
ExplicitDFTModelBuilderApprox<ValueType>::ExplicitDFTModelBuilderApprox(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) : mDft(dft), enableDC(enableDC), stateStorage(((mDft.stateVectorSize() / 64) + 1) * 64) {
// stateVectorSize is bound for size of bitvector
mStateGenerationInfo = std::make_shared<storm::storage::DFTStateGenerationInfo>(mDft.buildStateGenerationInfo(symmetries));
}
template <typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilderApprox<ValueType>::buildModel(LabelOptions const& labelOpts) {
// Initialize
bool deterministicModel = false;
size_t rowOffset = 0;
ModelComponents modelComponents;
std::vector<uint_fast64_t> tmpMarkovianStates;
storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0);
if(mergeFailedStates) {
// Introduce explicit fail state
failedIndex = newIndex;
newIndex++;
transitionMatrixBuilder.newRowGroup(failedIndex);
transitionMatrixBuilder.addNextValue(failedIndex, failedIndex, storm::utility::one<ValueType>());
STORM_LOG_TRACE("Introduce fail state with id: " << failedIndex);
modelComponents.exitRates.push_back(storm::utility::one<ValueType>());
tmpMarkovianStates.push_back(failedIndex);
}
// Explore state space
DFTStatePointer state = std::make_shared<storm::storage::DFTState<ValueType>>(mDft, *mStateGenerationInfo, newIndex);
auto exploreResult = exploreStates(state, rowOffset, transitionMatrixBuilder, tmpMarkovianStates, modelComponents.exitRates);
initialStateIndex = exploreResult.first;
bool deterministic = exploreResult.second;
// Before ending the exploration check for pseudo states which are not initialized yet
for (auto & pseudoStatePair : mPseudoStatesMapping) {
if (pseudoStatePair.first == 0) {
// Create state from pseudo state and explore
STORM_LOG_ASSERT(stateStorage.stateToId.contains(pseudoStatePair.second), "Pseudo state not contained.");
STORM_LOG_ASSERT(stateStorage.stateToId.getValue(pseudoStatePair.second) >= OFFSET_PSEUDO_STATE, "State is no pseudo state.");
STORM_LOG_TRACE("Create pseudo state from bit vector " << pseudoStatePair.second);
DFTStatePointer pseudoState = std::make_shared<storm::storage::DFTState<ValueType>>(pseudoStatePair.second, mDft, *mStateGenerationInfo, newIndex);
STORM_LOG_ASSERT(pseudoStatePair.second == pseudoState->status(), "Pseudo states do not coincide.");
STORM_LOG_TRACE("Explore pseudo state " << mDft.getStateString(pseudoState) << " with id " << pseudoState->getId());
auto exploreResult = exploreStates(pseudoState, rowOffset, transitionMatrixBuilder, tmpMarkovianStates, modelComponents.exitRates);
deterministic &= exploreResult.second;
STORM_LOG_ASSERT(pseudoStatePair.first == pseudoState->getId(), "Pseudo state ids do not coincide");
STORM_LOG_ASSERT(pseudoState->getId() == exploreResult.first, "Pseudo state ids do not coincide.");
}
}
// Replace pseudo states in matrix
std::vector<uint_fast64_t> pseudoStatesVector;
for (auto const& pseudoStatePair : mPseudoStatesMapping) {
pseudoStatesVector.push_back(pseudoStatePair.first);
}
STORM_LOG_ASSERT(std::find(pseudoStatesVector.begin(), pseudoStatesVector.end(), 0) == pseudoStatesVector.end(), "Unexplored pseudo state still contained.");
transitionMatrixBuilder.replaceColumns(pseudoStatesVector, OFFSET_PSEUDO_STATE);
STORM_LOG_DEBUG("Generated " << stateStorage.getNumberOfStates() + (mergeFailedStates ? 1 : 0) << " states");
STORM_LOG_DEBUG("Model is " << (deterministic ? "deterministic" : "non-deterministic"));
size_t stateSize = stateStorage.getNumberOfStates() + (mergeFailedStates ? 1 : 0);
// Build Markov Automaton
modelComponents.markovianStates = storm::storage::BitVector(stateSize, tmpMarkovianStates);
// Build transition matrix
modelComponents.transitionMatrix = transitionMatrixBuilder.build(stateSize, stateSize);
if (stateSize <= 15) {
STORM_LOG_TRACE("Transition matrix: " << std::endl << modelComponents.transitionMatrix);
} else {
STORM_LOG_TRACE("Transition matrix: too big to print");
}
STORM_LOG_TRACE("Exit rates: " << modelComponents.exitRates);
STORM_LOG_TRACE("Markovian states: " << modelComponents.markovianStates);
// Build state labeling
modelComponents.stateLabeling = storm::models::sparse::StateLabeling(stateStorage.getNumberOfStates() + (mergeFailedStates ? 1 : 0));
// Initial state is always first state without any failure
modelComponents.stateLabeling.addLabel("init");
modelComponents.stateLabeling.addLabelToState("init", initialStateIndex);
// Label all states corresponding to their status (failed, failsafe, failed BE)
if(labelOpts.buildFailLabel) {
modelComponents.stateLabeling.addLabel("failed");
}
if(labelOpts.buildFailSafeLabel) {
modelComponents.stateLabeling.addLabel("failsafe");
}
// Collect labels for all BE
std::vector<std::shared_ptr<storage::DFTBE<ValueType>>> basicElements = mDft.getBasicElements();
for (std::shared_ptr<storage::DFTBE<ValueType>> elem : basicElements) {
if(labelOpts.beLabels.count(elem->name()) > 0) {
modelComponents.stateLabeling.addLabel(elem->name() + "_fail");
}
}
if(mergeFailedStates) {
modelComponents.stateLabeling.addLabelToState("failed", failedIndex);
}
for (auto const& stateIdPair : stateStorage.stateToId) {
storm::storage::BitVector state = stateIdPair.first;
size_t stateId = stateIdPair.second;
if (!mergeFailedStates && labelOpts.buildFailLabel && mDft.hasFailed(state, *mStateGenerationInfo)) {
modelComponents.stateLabeling.addLabelToState("failed", stateId);
}
if (labelOpts.buildFailSafeLabel && mDft.isFailsafe(state, *mStateGenerationInfo)) {
modelComponents.stateLabeling.addLabelToState("failsafe", stateId);
};
// Set fail status for each BE
for (std::shared_ptr<storage::DFTBE<ValueType>> elem : basicElements) {
if (labelOpts.beLabels.count(elem->name()) > 0 && storm::storage::DFTState<ValueType>::hasFailed(state, mStateGenerationInfo->getStateIndex(elem->id())) ) {
modelComponents.stateLabeling.addLabelToState(elem->name() + "_fail", stateId);
}
}
}
std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
if (deterministic) {
// Turn the probabilities into rates by multiplying each row with the exit rate of the state.
// TODO Matthias: avoid transforming back and forth
storm::storage::SparseMatrix<ValueType> rateMatrix(modelComponents.transitionMatrix);
for (uint_fast64_t row = 0; row < rateMatrix.getRowCount(); ++row) {
STORM_LOG_ASSERT(row < modelComponents.markovianStates.size(), "Row exceeds no. of markovian states.");
if (modelComponents.markovianStates.get(row)) {
for (auto& entry : rateMatrix.getRow(row)) {
entry.setValue(entry.getValue() * modelComponents.exitRates[row]);
}
}
}
model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(std::move(rateMatrix), std::move(modelComponents.exitRates), std::move(modelComponents.stateLabeling));
} else {
std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates), true);
if (ma->hasOnlyTrivialNondeterminism()) {
// Markov automaton can be converted into CTMC
model = ma->convertToCTMC();
} else {
model = ma;
}
}
return model;
}
template <typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilderApprox<ValueType>::buildModelApprox(LabelOptions const& labelOpts) {
// Initialize
bool deterministicModel = false;
size_t rowOffset = 0;
ModelComponents modelComponents;
std::vector<uint_fast64_t> tmpMarkovianStates;
storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0);
if(mergeFailedStates) {
// Introduce explicit fail state
failedIndex = newIndex;
newIndex++;
transitionMatrixBuilder.newRowGroup(failedIndex);
transitionMatrixBuilder.addNextValue(failedIndex, failedIndex, storm::utility::one<ValueType>());
STORM_LOG_TRACE("Introduce fail state with id: " << failedIndex);
modelComponents.exitRates.push_back(storm::utility::one<ValueType>());
tmpMarkovianStates.push_back(failedIndex);
}
// Initialize generator
storm::generator::DftNextStateGenerator<ValueType, uint_fast64_t> generator(mDft, *mStateGenerationInfo);
// Explore state space
typename storm::generator::DftNextStateGenerator<ValueType, uint_fast64_t>::StateToIdCallback stateToIdCallback = [this] (DFTStatePointer const& state) -> uint_fast64_t {
uint_fast64_t id = newIndex++;
std::cout << "Added state " << id << std::endl;
return id;
};
uint_fast64_t id = generator.getInitialStates(stateToIdCallback)[0];
std::cout << "Initial state " << id << std::endl;
DFTStatePointer state = std::make_shared<storm::storage::DFTState<ValueType>>(mDft, *mStateGenerationInfo, newIndex);
auto exploreResult = exploreStates(state, rowOffset, transitionMatrixBuilder, tmpMarkovianStates, modelComponents.exitRates);
initialStateIndex = exploreResult.first;
bool deterministic = exploreResult.second;
// Before ending the exploration check for pseudo states which are not initialized yet
for (auto & pseudoStatePair : mPseudoStatesMapping) {
if (pseudoStatePair.first == 0) {
// Create state from pseudo state and explore
STORM_LOG_ASSERT(stateStorage.stateToId.contains(pseudoStatePair.second), "Pseudo state not contained.");
STORM_LOG_ASSERT(stateStorage.stateToId.getValue(pseudoStatePair.second) >= OFFSET_PSEUDO_STATE, "State is no pseudo state.");
STORM_LOG_TRACE("Create pseudo state from bit vector " << pseudoStatePair.second);
DFTStatePointer pseudoState = std::make_shared<storm::storage::DFTState<ValueType>>(pseudoStatePair.second, mDft, *mStateGenerationInfo, newIndex);
STORM_LOG_ASSERT(pseudoStatePair.second == pseudoState->status(), "Pseudo states do not coincide.");
STORM_LOG_TRACE("Explore pseudo state " << mDft.getStateString(pseudoState) << " with id " << pseudoState->getId());
auto exploreResult = exploreStates(pseudoState, rowOffset, transitionMatrixBuilder, tmpMarkovianStates, modelComponents.exitRates);
deterministic &= exploreResult.second;
STORM_LOG_ASSERT(pseudoStatePair.first == pseudoState->getId(), "Pseudo state ids do not coincide");
STORM_LOG_ASSERT(pseudoState->getId() == exploreResult.first, "Pseudo state ids do not coincide.");
}
}
// Replace pseudo states in matrix
std::vector<uint_fast64_t> pseudoStatesVector;
for (auto const& pseudoStatePair : mPseudoStatesMapping) {
pseudoStatesVector.push_back(pseudoStatePair.first);
}
STORM_LOG_ASSERT(std::find(pseudoStatesVector.begin(), pseudoStatesVector.end(), 0) == pseudoStatesVector.end(), "Unexplored pseudo state still contained.");
transitionMatrixBuilder.replaceColumns(pseudoStatesVector, OFFSET_PSEUDO_STATE);
STORM_LOG_DEBUG("Generated " << stateStorage.getNumberOfStates() + (mergeFailedStates ? 1 : 0) << " states");
STORM_LOG_DEBUG("Model is " << (deterministic ? "deterministic" : "non-deterministic"));
size_t stateSize = stateStorage.getNumberOfStates() + (mergeFailedStates ? 1 : 0);
// Build Markov Automaton
modelComponents.markovianStates = storm::storage::BitVector(stateSize, tmpMarkovianStates);
// Build transition matrix
modelComponents.transitionMatrix = transitionMatrixBuilder.build(stateSize, stateSize);
if (stateSize <= 15) {
STORM_LOG_TRACE("Transition matrix: " << std::endl << modelComponents.transitionMatrix);
} else {
STORM_LOG_TRACE("Transition matrix: too big to print");
}
STORM_LOG_TRACE("Exit rates: " << modelComponents.exitRates);
STORM_LOG_TRACE("Markovian states: " << modelComponents.markovianStates);
// Build state labeling
modelComponents.stateLabeling = storm::models::sparse::StateLabeling(stateStorage.getNumberOfStates() + (mergeFailedStates ? 1 : 0));
// Initial state is always first state without any failure
modelComponents.stateLabeling.addLabel("init");
modelComponents.stateLabeling.addLabelToState("init", initialStateIndex);
// Label all states corresponding to their status (failed, failsafe, failed BE)
if(labelOpts.buildFailLabel) {
modelComponents.stateLabeling.addLabel("failed");
}
if(labelOpts.buildFailSafeLabel) {
modelComponents.stateLabeling.addLabel("failsafe");
}
// Collect labels for all BE
std::vector<std::shared_ptr<storage::DFTBE<ValueType>>> basicElements = mDft.getBasicElements();
for (std::shared_ptr<storage::DFTBE<ValueType>> elem : basicElements) {
if(labelOpts.beLabels.count(elem->name()) > 0) {
modelComponents.stateLabeling.addLabel(elem->name() + "_fail");
}
}
if(mergeFailedStates) {
modelComponents.stateLabeling.addLabelToState("failed", failedIndex);
}
for (auto const& stateIdPair : stateStorage.stateToId) {
storm::storage::BitVector state = stateIdPair.first;
size_t stateId = stateIdPair.second;
if (!mergeFailedStates && labelOpts.buildFailLabel && mDft.hasFailed(state, *mStateGenerationInfo)) {
modelComponents.stateLabeling.addLabelToState("failed", stateId);
}
if (labelOpts.buildFailSafeLabel && mDft.isFailsafe(state, *mStateGenerationInfo)) {
modelComponents.stateLabeling.addLabelToState("failsafe", stateId);
};
// Set fail status for each BE
for (std::shared_ptr<storage::DFTBE<ValueType>> elem : basicElements) {
if (labelOpts.beLabels.count(elem->name()) > 0 && storm::storage::DFTState<ValueType>::hasFailed(state, mStateGenerationInfo->getStateIndex(elem->id())) ) {
modelComponents.stateLabeling.addLabelToState(elem->name() + "_fail", stateId);
}
}
}
std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
if (deterministic) {
// Turn the probabilities into rates by multiplying each row with the exit rate of the state.
// TODO Matthias: avoid transforming back and forth
storm::storage::SparseMatrix<ValueType> rateMatrix(modelComponents.transitionMatrix);
for (uint_fast64_t row = 0; row < rateMatrix.getRowCount(); ++row) {
STORM_LOG_ASSERT(row < modelComponents.markovianStates.size(), "Row exceeds no. of markovian states.");
if (modelComponents.markovianStates.get(row)) {
for (auto& entry : rateMatrix.getRow(row)) {
entry.setValue(entry.getValue() * modelComponents.exitRates[row]);
}
}
}
model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(std::move(rateMatrix), std::move(modelComponents.exitRates), std::move(modelComponents.stateLabeling));
} else {
std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates), true);
if (ma->hasOnlyTrivialNondeterminism()) {
// Markov automaton can be converted into CTMC
model = ma->convertToCTMC();
} else {
model = ma;
}
}
return model;
}
template<>
bool belowThreshold(double const& number) {
return number < 0.1;
}
template<>
bool belowThreshold(storm::RationalFunction const& number) {
storm::RationalFunction threshold = storm::utility::one<storm::RationalFunction>() / 10;
std::cout << number << " < " << threshold << ": " << (number < threshold) << std::endl;
std::map<storm::Variable, storm::RationalNumber> mapping;
storm::RationalFunction eval(number.evaluate(mapping));
std::cout << "Evaluated: " << eval << std::endl;
return eval < threshold;
}
template <typename ValueType>
std::pair<uint_fast64_t, bool> ExplicitDFTModelBuilderApprox<ValueType>::exploreStates(DFTStatePointer const& state, size_t& rowOffset, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<uint_fast64_t>& markovianStates, std::vector<ValueType>& exitRates) {
STORM_LOG_TRACE("Explore state: " << mDft.getStateString(state));
auto explorePair = checkForExploration(state);
if (!explorePair.first) {
// State does not need any exploration
return std::make_pair(explorePair.second, true);
}
// Initialization
// TODO Matthias: set Markovian states directly as bitvector?
std::map<uint_fast64_t, ValueType> outgoingRates;
std::vector<std::map<uint_fast64_t, ValueType>> outgoingProbabilities;
bool hasDependencies = state->nrFailableDependencies() > 0;
size_t failableCount = hasDependencies ? state->nrFailableDependencies() : state->nrFailableBEs();
size_t smallest = 0;
ValueType exitRate = storm::utility::zero<ValueType>();
bool deterministic = !hasDependencies;
// Absorbing state
if (mDft.hasFailed(state) || mDft.isFailsafe(state) || state->nrFailableBEs() == 0) {
uint_fast64_t stateId = addState(state);
STORM_LOG_ASSERT(stateId == state->getId(), "Ids do not coincide.");
// Add self loop
transitionMatrixBuilder.newRowGroup(stateId + rowOffset);
transitionMatrixBuilder.addNextValue(stateId + rowOffset, stateId, storm::utility::one<ValueType>());
STORM_LOG_TRACE("Added self loop for " << stateId);
exitRates.push_back(storm::utility::one<ValueType>());
STORM_LOG_ASSERT(exitRates.size()-1 == stateId, "No. of considered states does not match state id.");
markovianStates.push_back(stateId);
// No further exploration required
return std::make_pair(stateId, true);
}
// Let BE fail
while (smallest < failableCount) {
STORM_LOG_ASSERT(!mDft.hasFailed(state), "Dft has failed.");
// Construct new state as copy from original one
DFTStatePointer newState = std::make_shared<storm::storage::DFTState<ValueType>>(*state);
std::pair<std::shared_ptr<storm::storage::DFTBE<ValueType> const>, bool> nextBEPair = newState->letNextBEFail(smallest++);
std::shared_ptr<storm::storage::DFTBE<ValueType> const>& nextBE = nextBEPair.first;
STORM_LOG_ASSERT(nextBE, "NextBE is null.");
STORM_LOG_ASSERT(nextBEPair.second == hasDependencies, "Failure due to dependencies does not match.");
STORM_LOG_TRACE("With the failure of: " << nextBE->name() << " [" << nextBE->id() << "] in " << mDft.getStateString(state));
if (storm::settings::getModule<storm::settings::modules::DFTSettings>().computeApproximation()) {
if (!storm::utility::isZero(exitRate)) {
ValueType rate = nextBE->activeFailureRate();
ValueType div = rate / exitRate;
if (!storm::utility::isZero(exitRate) && belowThreshold(div)) {
// Set transition directly to failed state
auto resultFind = outgoingRates.find(failedIndex);
if (resultFind != outgoingRates.end()) {
// Add to existing transition
resultFind->second += rate;
STORM_LOG_TRACE("Updated transition to " << resultFind->first << " with rate " << rate << " to new rate " << resultFind->second);
} else {
// Insert new transition
outgoingRates.insert(std::make_pair(failedIndex, rate));
STORM_LOG_TRACE("Added transition to " << failedIndex << " with rate " << rate);
}
exitRate += rate;
std::cout << "IGNORE: " << nextBE->name() << " [" << nextBE->id() << "] with rate " << rate << std::endl;
//STORM_LOG_TRACE("Ignore: " << nextBE->name() << " [" << nextBE->id() << "] with rate " << rate);
continue;
}
}
}
// Propagate failures
storm::storage::DFTStateSpaceGenerationQueues<ValueType> queues;
for (DFTGatePointer parent : nextBE->parents()) {
if (newState->isOperational(parent->id())) {
queues.propagateFailure(parent);
}
}
for (DFTRestrictionPointer restr : nextBE->restrictions()) {
queues.checkRestrictionLater(restr);
}
while (!queues.failurePropagationDone()) {
DFTGatePointer next = queues.nextFailurePropagation();
next->checkFails(*newState, queues);
newState->updateFailableDependencies(next->id());
}
while(!queues.restrictionChecksDone()) {
DFTRestrictionPointer next = queues.nextRestrictionCheck();
next->checkFails(*newState, queues);
newState->updateFailableDependencies(next->id());
}
if(newState->isInvalid()) {
continue;
}
bool dftFailed = newState->hasFailed(mDft.getTopLevelIndex());
while (!dftFailed && !queues.failsafePropagationDone()) {
DFTGatePointer next = queues.nextFailsafePropagation();
next->checkFailsafe(*newState, queues);
}
while (!dftFailed && enableDC && !queues.dontCarePropagationDone()) {
DFTElementPointer next = queues.nextDontCarePropagation();
next->checkDontCareAnymore(*newState, queues);
}
// Update failable dependencies
if (!dftFailed) {
newState->updateFailableDependencies(nextBE->id());
newState->updateDontCareDependencies(nextBE->id());
}
uint_fast64_t newStateId;
if(dftFailed && mergeFailedStates) {
newStateId = failedIndex;
} else {
// Explore new state recursively
auto explorePair = exploreStates(newState, rowOffset, transitionMatrixBuilder, markovianStates, exitRates);
newStateId = explorePair.first;
deterministic &= explorePair.second;
}
// Set transitions
if (hasDependencies) {
// Failure is due to dependency -> add non-deterministic choice
std::map<uint_fast64_t, ValueType> choiceProbabilities;
std::shared_ptr<storm::storage::DFTDependency<ValueType> const> dependency = mDft.getDependency(state->getDependencyId(smallest-1));
choiceProbabilities.insert(std::make_pair(newStateId, dependency->probability()));
STORM_LOG_TRACE("Added transition to " << newStateId << " with probability " << dependency->probability());
if (!storm::utility::isOne(dependency->probability())) {
// Add transition to state where dependency was unsuccessful
DFTStatePointer unsuccessfulState = std::make_shared<storm::storage::DFTState<ValueType>>(*state);
unsuccessfulState->letDependencyBeUnsuccessful(smallest-1);
auto explorePair = exploreStates(unsuccessfulState, rowOffset, transitionMatrixBuilder, markovianStates, exitRates);
uint_fast64_t unsuccessfulStateId = explorePair.first;
deterministic &= explorePair.second;
ValueType remainingProbability = storm::utility::one<ValueType>() - dependency->probability();
choiceProbabilities.insert(std::make_pair(unsuccessfulStateId, remainingProbability));
STORM_LOG_TRACE("Added transition to " << unsuccessfulStateId << " with remaining probability " << remainingProbability);
}
outgoingProbabilities.push_back(choiceProbabilities);
} else {
// Set failure rate according to activation
bool isActive = true;
if (mDft.hasRepresentant(nextBE->id())) {
// Active must be checked for the state we are coming from as this state is responsible for the
// rate and not the new state we are going to
isActive = state->isActive(mDft.getRepresentant(nextBE->id())->id());
}
ValueType rate = isActive ? nextBE->activeFailureRate() : nextBE->passiveFailureRate();
STORM_LOG_ASSERT(!storm::utility::isZero(rate), "Rate is 0.");
auto resultFind = outgoingRates.find(newStateId);
if (resultFind != outgoingRates.end()) {
// Add to existing transition
resultFind->second += rate;
STORM_LOG_TRACE("Updated transition to " << resultFind->first << " with " << (isActive ? "active" : "passive") << " rate " << rate << " to new rate " << resultFind->second);
} else {
// Insert new transition
outgoingRates.insert(std::make_pair(newStateId, rate));
STORM_LOG_TRACE("Added transition to " << newStateId << " with " << (isActive ? "active" : "passive") << " rate " << rate);
}
exitRate += rate;
}
} // end while failing BE
// Add state
uint_fast64_t stateId = addState(state);
STORM_LOG_ASSERT(stateId == state->getId(), "Ids do not match.");
STORM_LOG_ASSERT(stateId == newIndex-1, "Id does not match no. of states.");
if (hasDependencies) {
// Add all probability transitions
STORM_LOG_ASSERT(outgoingRates.empty(), "Outgoing transitions not empty.");
transitionMatrixBuilder.newRowGroup(stateId + rowOffset);
for (size_t i = 0; i < outgoingProbabilities.size(); ++i, ++rowOffset) {
STORM_LOG_ASSERT(outgoingProbabilities[i].size() == 1 || outgoingProbabilities[i].size() == 2, "No. of outgoing transitions is not valid.");
for (auto it = outgoingProbabilities[i].begin(); it != outgoingProbabilities[i].end(); ++it)
{
STORM_LOG_TRACE("Set transition from " << stateId << " to " << it->first << " with probability " << it->second);
transitionMatrixBuilder.addNextValue(stateId + rowOffset, it->first, it->second);
}
}
rowOffset--; // One increment too many
} else {
// Try to merge pseudo states with their instantiation
// TODO Matthias: improve?
for (auto it = outgoingRates.begin(); it != outgoingRates.end(); ) {
if (it->first >= OFFSET_PSEUDO_STATE) {
uint_fast64_t newId = it->first - OFFSET_PSEUDO_STATE;
STORM_LOG_ASSERT(newId < mPseudoStatesMapping.size(), "Id is not valid.");
if (mPseudoStatesMapping[newId].first > 0) {
// State exists already
newId = mPseudoStatesMapping[newId].first;
auto itFind = outgoingRates.find(newId);
if (itFind != outgoingRates.end()) {
// Add probability from pseudo state to instantiation
itFind->second += it->second;
STORM_LOG_TRACE("Merged pseudo state " << newId << " adding rate " << it->second << " to total rate of " << itFind->second);
} else {
// Only change id
outgoingRates.emplace(newId, it->second);
STORM_LOG_TRACE("Instantiated pseudo state " << newId << " with rate " << it->second);
}
// Remove pseudo state
it = outgoingRates.erase(it);
} else {
++it;
}
} else {
++it;
}
}
// Add all rate transitions
STORM_LOG_ASSERT(outgoingProbabilities.empty(), "Outgoing probabilities not empty.");
transitionMatrixBuilder.newRowGroup(state->getId() + rowOffset);
STORM_LOG_TRACE("Exit rate for " << state->getId() << ": " << exitRate);
for (auto it = outgoingRates.begin(); it != outgoingRates.end(); ++it)
{
ValueType probability = it->second / exitRate; // Transform rate to probability
STORM_LOG_TRACE("Set transition from " << state->getId() << " to " << it->first << " with rate " << it->second);
transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, it->first, probability);
}
markovianStates.push_back(state->getId());
}
STORM_LOG_TRACE("Finished exploring state: " << mDft.getStateString(state));
exitRates.push_back(exitRate);
STORM_LOG_ASSERT(exitRates.size()-1 == state->getId(), "Id does not match no. of states.");
return std::make_pair(state->getId(), deterministic);
}
template <typename ValueType>
std::pair<bool, uint_fast64_t> ExplicitDFTModelBuilderApprox<ValueType>::checkForExploration(DFTStatePointer const& state) {
bool changed = false;
if (mStateGenerationInfo->hasSymmetries()) {
// Order state by symmetry
STORM_LOG_TRACE("Check for symmetry: " << mDft.getStateString(state));
changed = state->orderBySymmetry();
STORM_LOG_TRACE("State " << (changed ? "changed to " : "did not change") << (changed ? mDft.getStateString(state) : ""));
}
if (stateStorage.stateToId.contains(state->status())) {
// State already exists
uint_fast64_t stateId = stateStorage.stateToId.getValue(state->status());
STORM_LOG_TRACE("State " << mDft.getStateString(state) << " with id " << stateId << " already exists");
if (changed || stateId < OFFSET_PSEUDO_STATE) {
// State is changed or an explored "normal" state
return std::make_pair(false, stateId);
}
stateId -= OFFSET_PSEUDO_STATE;
STORM_LOG_ASSERT(stateId < mPseudoStatesMapping.size(), "Id not valid.");
if (mPseudoStatesMapping[stateId].first > 0) {
// Pseudo state already explored
return std::make_pair(false, mPseudoStatesMapping[stateId].first);
}
STORM_LOG_ASSERT(mPseudoStatesMapping[stateId].second == state->status(), "States do not coincide.");
STORM_LOG_TRACE("Pseudo state " << mDft.getStateString(state) << " can be explored now");
return std::make_pair(true, stateId);
} else {
// State does not exists
if (changed) {
// Remember state for later creation
state->setId(mPseudoStatesMapping.size() + OFFSET_PSEUDO_STATE);
mPseudoStatesMapping.push_back(std::make_pair(0, state->status()));
stateStorage.stateToId.findOrAdd(state->status(), state->getId());
STORM_LOG_TRACE("Remember state for later creation: " << mDft.getStateString(state));
return std::make_pair(false, state->getId());
} else {
// State needs exploration
return std::make_pair(true, 0);
}
}
}
template <typename ValueType>
uint_fast64_t ExplicitDFTModelBuilderApprox<ValueType>::addState(DFTStatePointer const& state) {
uint_fast64_t stateId;
// TODO remove
bool changed = state->orderBySymmetry();
STORM_LOG_ASSERT(!changed, "State to add has changed by applying symmetry.");
// Check if state already exists
if (stateStorage.stateToId.contains(state->status())) {
// State already exists
stateId = stateStorage.stateToId.getValue(state->status());
STORM_LOG_TRACE("State " << mDft.getStateString(state) << " with id " << stateId << " already exists");
// Check if possible pseudo state can be created now
STORM_LOG_ASSERT(stateId >= OFFSET_PSEUDO_STATE, "State is no pseudo state.");
stateId -= OFFSET_PSEUDO_STATE;
STORM_LOG_ASSERT(stateId < mPseudoStatesMapping.size(), "Pseudo state not known.");
if (mPseudoStatesMapping[stateId].first == 0) {
// Create pseudo state now
STORM_LOG_ASSERT(mPseudoStatesMapping[stateId].second == state->status(), "Pseudo states do not coincide.");
state->setId(newIndex++);
mPseudoStatesMapping[stateId].first = state->getId();
stateId = state->getId();
stateStorage.stateToId.setOrAdd(state->status(), stateId);
STORM_LOG_TRACE("Now create state " << mDft.getStateString(state) << " with id " << stateId);
return stateId;
} else {
STORM_LOG_ASSERT(false, "Pseudo state already created.");
return 0;
}
} else {
// Create new state
state->setId(newIndex++);
stateId = stateStorage.stateToId.findOrAdd(state->status(), state->getId());
STORM_LOG_TRACE("New state: " << mDft.getStateString(state));
return stateId;
}
}
// Explicitly instantiate the class.
template class ExplicitDFTModelBuilderApprox<double>;
#ifdef STORM_HAVE_CARL
template class ExplicitDFTModelBuilderApprox<storm::RationalFunction>;
#endif
} // namespace builder
} // namespace storm

105
src/builder/ExplicitDFTModelBuilderApprox.h
View File

@ -0,0 +1,105 @@
#ifndef EXPLICITDFTMODELBUILDERAPPROX_H
#define EXPLICITDFTMODELBUILDERAPPROX_H
#include <src/models/sparse/StateLabeling.h>
#include <src/models/sparse/StandardRewardModel.h>
#include <src/models/sparse/Model.h>
#include <src/storage/SparseMatrix.h>
#include "src/storage/sparse/StateStorage.h"
#include <src/storage/dft/DFT.h>
#include <src/storage/dft/SymmetricUnits.h>
#include <boost/container/flat_set.hpp>
#include <boost/optional/optional.hpp>
#include <stack>
#include <unordered_set>
namespace storm {
namespace builder {
template<typename ValueType>
class ExplicitDFTModelBuilderApprox {
using DFTElementPointer = std::shared_ptr<storm::storage::DFTElement<ValueType>>;
using DFTElementCPointer = std::shared_ptr<storm::storage::DFTElement<ValueType> const>;
using DFTGatePointer = std::shared_ptr<storm::storage::DFTGate<ValueType>>;
using DFTStatePointer = std::shared_ptr<storm::storage::DFTState<ValueType>>;
using DFTRestrictionPointer = std::shared_ptr<storm::storage::DFTRestriction<ValueType>>;
// A structure holding the individual components of a model.
struct ModelComponents {
ModelComponents();
// The transition matrix.
storm::storage::SparseMatrix<ValueType> transitionMatrix;
// The state labeling.
storm::models::sparse::StateLabeling stateLabeling;
// The Markovian states.
storm::storage::BitVector markovianStates;
// The exit rates.
std::vector<ValueType> exitRates;
// A vector that stores a labeling for each choice.
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> choiceLabeling;
};
const uint_fast64_t OFFSET_PSEUDO_STATE = UINT_FAST64_MAX / 2;
storm::storage::DFT<ValueType> const& mDft;
std::shared_ptr<storm::storage::DFTStateGenerationInfo> mStateGenerationInfo;
//TODO Matthias: remove when everything works
std::vector<std::pair<uint_fast64_t, storm::storage::BitVector>> mPseudoStatesMapping; // vector of (id to concrete state, bitvector)
size_t newIndex = 0;
bool mergeFailedStates = true;
bool enableDC = true;
size_t failedIndex = 0;
size_t initialStateIndex = 0;
// Internal information about the states that were explored.
storm::storage::sparse::StateStorage<uint_fast64_t> stateStorage;
public:
struct LabelOptions {
bool buildFailLabel = true;
bool buildFailSafeLabel = false;
std::set<std::string> beLabels = {};
};
ExplicitDFTModelBuilderApprox(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC);
std::shared_ptr<storm::models::sparse::Model<ValueType>> buildModel(LabelOptions const& labelOpts);
// TODO Matthias: only temporary used for avoiding crashing everything
std::shared_ptr<storm::models::sparse::Model<ValueType>> buildModelApprox(LabelOptions const& labelOpts);
private:
std::pair<uint_fast64_t, bool> exploreStates(DFTStatePointer const& state, size_t& rowOffset, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<uint_fast64_t>& markovianStates, std::vector<ValueType>& exitRates);
/*!
* Adds a state to the explored states and handles pseudo states.
*
* @param state The state to add.
* @return Id of added state.
*/
uint_fast64_t addState(DFTStatePointer const& state);
/*!
* Check if state needs an exploration and remember pseudo states for later creation.
*
* @param state State which might need exploration.
* @return Pair of flag indicating whether the state needs exploration now and the state id if the state already
* exists.
*/
std::pair<bool, uint_fast64_t> checkForExploration(DFTStatePointer const& state);
};
template<typename ValueType>
bool belowThreshold(ValueType const& number);
}
}
#endif /* EXPLICITDFTMODELBUILDERAPPROX_H */

31
src/generator/DftNextStateGenerator.cpp
View File

@ -2,38 +2,30 @@
#include "src/utility/constants.h"
#include "src/utility/macros.h"
#include "src/exceptions/WrongFormatException.h"
#include "src/exceptions/NotImplementedException.h"
namespace storm {
namespace generator {
template<typename ValueType, typename StateType>
DftNextStateGenerator<ValueType, StateType>::DftNextStateGenerator(storm::storage::DFT<ValueType> const& dft) : mDft(dft), state(nullptr), comparator() {
DftNextStateGenerator<ValueType, StateType>::DftNextStateGenerator(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo) : mDft(dft), mStateGenerationInfo(stateGenerationInfo), state(nullptr), comparator() {
// Intentionally left empty.
}
template<typename ValueType, typename StateType>
bool DftNextStateGenerator<ValueType, StateType>::isDeterministicModel() const {
assert(false);
return true;
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented.");
}
template<typename ValueType, typename StateType>
std::vector<StateType> DftNextStateGenerator<ValueType, StateType>::getInitialStates(StateToIdCallback const& stateToIdCallback) {
// FIXME: This only works for models with exactly one initial state. We should make this more general.
/*CompressedState initialState(variableInformation.getTotalBitOffset());
// We need to initialize the values of the variables to their initial value.
for (auto const& booleanVariable : variableInformation.booleanVariables) {
initialState.set(booleanVariable.bitOffset, booleanVariable.initialValue);
}
for (auto const& integerVariable : variableInformation.integerVariables) {
initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast<uint_fast64_t>(integerVariable.initialValue - integerVariable.lowerBound));
}
DFTStatePointer initialState = std::make_shared<storm::storage::DFTState<ValueType>>(mDft, mStateGenerationInfo, 0);
// Register initial state and return it.
// Register initial state
StateType id = stateToIdCallback(initialState);
return {id};*/
initialState->setId(id);
return {id};
}
template<typename ValueType, typename StateType>
@ -43,14 +35,12 @@ namespace storm {
// Also, we need to store a pointer to the state itself, because we need to be able to access it when expanding it.
this->state = &state;*/
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented.");
}
template<typename ValueType, typename StateType>
bool DftNextStateGenerator<ValueType, StateType>::satisfies(storm::expressions::Expression const& expression) const {
/* if (expression.isTrue()) {
return true;
}
return evaluator.asBool(expression);*/
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented.");
}
template<typename ValueType, typename StateType>
@ -147,6 +137,7 @@ namespace storm {
result.setExpanded();
return result;*/
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented.");
}

15
src/generator/DftNextStateGenerator.h
View File

@ -9,17 +9,20 @@
namespace storm {
namespace generator {
template<typename ValueType, typename StateType = uint32_t>
template<typename ValueType, typename StateType = uint_fast64_t>
class DftNextStateGenerator : public NextStateGenerator<ValueType, std::shared_ptr<storm::storage::DFTState<ValueType>>, StateType> {
using DFTStatePointer = std::shared_ptr<storm::storage::DFTState<ValueType>>;
public:
typedef typename NextStateGenerator<ValueType, std::shared_ptr<storm::storage::DFTState<ValueType>>, StateType>::StateToIdCallback StateToIdCallback;
typedef typename NextStateGenerator<ValueType, DFTStatePointer, StateType>::StateToIdCallback StateToIdCallback;
DftNextStateGenerator(storm::storage::DFT<ValueType> const& dft);
DftNextStateGenerator(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo);
virtual bool isDeterministicModel() const override;
virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) override;
virtual void load(std::shared_ptr<storm::storage::DFTState<ValueType>> const& state) override;
virtual void load(DFTStatePointer const& state) override;
virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) override;
virtual bool satisfies(storm::expressions::Expression const& expression) const override;
@ -28,7 +31,9 @@ namespace storm {
// The program used for the generation of next states.
storm::storage::DFT<ValueType> const& mDft;
CompressedState const* state;
storm::storage::DFTStateGenerationInfo const& mStateGenerationInfo;
DFTStatePointer const state;
// A comparator used to compare constants.
storm::utility::ConstantsComparator<ValueType> comparator;

30
src/modelchecker/DFTAnalyser.h
View File

@ -1,12 +1,14 @@
#pragma once
#include "logic/Formula.h"
#include "parser/DFTGalileoParser.h"
#include "builder/ExplicitDFTModelBuilder.h"
#include "modelchecker/results/CheckResult.h"
#include "utility/storm.h"
#include "storage/dft/DFTIsomorphism.h"
#include "utility/bitoperations.h"
#include "src/logic/Formula.h"
#include "src/parser/DFTGalileoParser.h"
#include "src/builder/ExplicitDFTModelBuilder.h"
#include "src/builder/ExplicitDFTModelBuilderApprox.h"
#include "src/modelchecker/results/CheckResult.h"
#include "src/utility/storm.h"
#include "src/storage/dft/DFTIsomorphism.h"
#include "src/settings/modules/DFTSettings.h"
#include "src/utility/bitoperations.h"
#include <chrono>
@ -149,9 +151,17 @@ private:
// Building Markov Automaton
STORM_LOG_INFO("Building Model...");
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);
typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.buildModel(labeloptions);
std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
// TODO Matthias: use only one builder if everything works again
if (storm::settings::getModule<storm::settings::modules::DFTSettings>().computeApproximation()) {
storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
model = builder.buildModel(labeloptions);
} else {
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);
typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
model = builder.buildModel(labeloptions);
}
//model->printModelInformationToStream(std::cout);
STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates());
STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions());

1
src/storage/sparse/StateStorage.cpp
View File

@ -15,6 +15,7 @@ namespace storm {
}
template class StateStorage<uint32_t>;
template class StateStorage<uint_fast64_t>;
}
}
}
Write Preview
Loading…
Cancel
Save