You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
939 lines
53 KiB
939 lines
53 KiB
#include "ExplicitDFTModelBuilder.h"
|
|
|
|
#include <map>
|
|
|
|
#include <storm/exceptions/IllegalArgumentException.h>
|
|
#include "storm/exceptions/InvalidArgumentException.h"
|
|
#include "storm/exceptions/UnexpectedException.h"
|
|
#include "storm/logic/AtomicLabelFormula.h"
|
|
#include "storm/models/sparse/MarkovAutomaton.h"
|
|
#include "storm/models/sparse/Ctmc.h"
|
|
#include "storm/utility/bitoperations.h"
|
|
#include "storm/utility/constants.h"
|
|
#include "storm/utility/ProgressMeasurement.h"
|
|
#include "storm/utility/SignalHandler.h"
|
|
#include "storm/utility/vector.h"
|
|
#include "storm/settings/SettingsManager.h"
|
|
#include "storm/transformer/NonMarkovianChainTransformer.h"
|
|
|
|
#include "storm-dft/settings/modules/FaultTreeSettings.h"
|
|
|
|
|
|
namespace storm {
|
|
namespace builder {
|
|
|
|
template<typename ValueType, typename StateType>
|
|
ExplicitDFTModelBuilder<ValueType, StateType>::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), markovianStates(), exitRates(), choiceLabeling() {
|
|
// Intentionally left empty.
|
|
}
|
|
|
|
template<typename ValueType, typename StateType>
|
|
ExplicitDFTModelBuilder<ValueType, StateType>::MatrixBuilder::MatrixBuilder(bool canHaveNondeterminism) : mappingOffset(0), stateRemapping(), currentRowGroup(0), currentRow(0), canHaveNondeterminism((canHaveNondeterminism)) {
|
|
// Create matrix builder
|
|
builder = storm::storage::SparseMatrixBuilder<ValueType>(0, 0, 0, false, canHaveNondeterminism, 0);
|
|
}
|
|
|
|
template<typename ValueType, typename StateType>
|
|
ExplicitDFTModelBuilder<ValueType, StateType>::ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, std::set<size_t> const& relevantEvents, bool allowDCForRelevantEvents) :
|
|
dft(dft),
|
|
stateGenerationInfo(std::make_shared<storm::storage::DFTStateGenerationInfo>(dft.buildStateGenerationInfo(symmetries))),
|
|
relevantEvents(relevantEvents),
|
|
generator(dft, *stateGenerationInfo),
|
|
matrixBuilder(!generator.isDeterministicModel()),
|
|
stateStorage(dft.stateBitVectorSize()),
|
|
explorationQueue(1, 0, 0.9, false)
|
|
{
|
|
// Set relevant events
|
|
this->dft.setRelevantEvents(this->relevantEvents, allowDCForRelevantEvents);
|
|
STORM_LOG_DEBUG("Relevant events: " << this->dft.getRelevantEventsString());
|
|
if (this->relevantEvents.empty()) {
|
|
// Only interested in top level event -> introduce unique failed state
|
|
this->uniqueFailedState = true;
|
|
STORM_LOG_DEBUG("Using unique failed state with id 0.");
|
|
}
|
|
|
|
// Compute independent subtrees
|
|
if (dft.topLevelType() == storm::storage::DFTElementType::OR) {
|
|
// We only support this for approximation with top level element OR
|
|
for (auto const& child : dft.getGate(dft.getTopLevelIndex())->children()) {
|
|
// Consider all children of the top level gate
|
|
std::vector<size_t> isubdft;
|
|
if (child->nrParents() > 1 || child->hasOutgoingDependencies()) {
|
|
STORM_LOG_TRACE("child " << child->name() << " does not allow modularisation.");
|
|
isubdft.clear();
|
|
} else if (dft.isGate(child->id())) {
|
|
isubdft = dft.getGate(child->id())->independentSubDft(false);
|
|
} else {
|
|
STORM_LOG_ASSERT(dft.isBasicElement(child->id()), "Child is no BE.");
|
|
if(dft.getBasicElement(child->id())->hasIngoingDependencies()) {
|
|
STORM_LOG_TRACE("child " << child->name() << " does not allow modularisation.");
|
|
isubdft.clear();
|
|
} else {
|
|
isubdft = {child->id()};
|
|
}
|
|
}
|
|
if(isubdft.empty()) {
|
|
subtreeBEs.clear();
|
|
break;
|
|
} else {
|
|
// Add new independent subtree
|
|
std::vector<size_t> subtree;
|
|
for (size_t id : isubdft) {
|
|
if (dft.isBasicElement(id)) {
|
|
subtree.push_back(id);
|
|
}
|
|
}
|
|
subtreeBEs.push_back(subtree);
|
|
}
|
|
}
|
|
}
|
|
if (subtreeBEs.empty()) {
|
|
// Consider complete tree
|
|
std::vector<size_t> subtree;
|
|
for (size_t id = 0; id < dft.nrElements(); ++id) {
|
|
if (dft.isBasicElement(id)) {
|
|
subtree.push_back(id);
|
|
}
|
|
}
|
|
subtreeBEs.push_back(subtree);
|
|
}
|
|
|
|
for (auto tree : subtreeBEs) {
|
|
std::stringstream stream;
|
|
stream << "Subtree: ";
|
|
for (size_t id : tree) {
|
|
stream << id << ", ";
|
|
}
|
|
STORM_LOG_TRACE(stream.str());
|
|
}
|
|
}
|
|
|
|
template<typename ValueType, typename StateType>
|
|
void ExplicitDFTModelBuilder<ValueType, StateType>::buildModel(size_t iteration, double approximationThreshold, storm::builder::ApproximationHeuristic approximationHeuristic) {
|
|
STORM_LOG_TRACE("Generating DFT state space");
|
|
usedHeuristic = approximationHeuristic;
|
|
|
|
if (approximationThreshold > 0 && !this->uniqueFailedState) {
|
|
// Approximation requires unique failed states
|
|
// TODO lift this restriction
|
|
STORM_LOG_WARN("Approximation requires unique failed state. Forcing use of unique failed state.");
|
|
this->uniqueFailedState = true;
|
|
}
|
|
|
|
if (iteration < 1) {
|
|
// Initialize
|
|
switch (usedHeuristic) {
|
|
case storm::builder::ApproximationHeuristic::DEPTH:
|
|
explorationQueue = storm::storage::BucketPriorityQueue<ExplorationHeuristic>(dft.nrElements()+1, 0, 0.9, false);
|
|
break;
|
|
case storm::builder::ApproximationHeuristic::PROBABILITY:
|
|
explorationQueue = storm::storage::BucketPriorityQueue<ExplorationHeuristic>(200, 0, 0.9, true);
|
|
break;
|
|
case storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE:
|
|
explorationQueue = storm::storage::BucketPriorityQueue<ExplorationHeuristic>(200, 0, 0.9, true);
|
|
break;
|
|
default:
|
|
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Heuristic not known.");
|
|
}
|
|
modelComponents.markovianStates = storm::storage::BitVector(INITIAL_BITVECTOR_SIZE);
|
|
|
|
if (this->uniqueFailedState) {
|
|
// Introduce explicit fail state
|
|
storm::generator::StateBehavior<ValueType, StateType> behavior = generator.createMergeFailedState([this] (DFTStatePointer const& state) {
|
|
size_t failedStateId = newIndex++;
|
|
STORM_LOG_ASSERT(failedStateId == 0, "Unique failed id is not 0.");
|
|
matrixBuilder.stateRemapping.push_back(0);
|
|
return failedStateId;
|
|
} );
|
|
|
|
matrixBuilder.setRemapping(0);
|
|
STORM_LOG_ASSERT(!behavior.empty(), "Behavior is empty.");
|
|
matrixBuilder.newRowGroup();
|
|
setMarkovian(behavior.begin()->isMarkovian());
|
|
|
|
// Now add self loop.
|
|
// TODO: maybe use general method.
|
|
STORM_LOG_ASSERT(behavior.getNumberOfChoices() == 1, "Wrong number of choices for failed state.");
|
|
STORM_LOG_ASSERT(behavior.begin()->size() == 1, "Wrong number of transitions for failed state.");
|
|
std::pair<StateType, ValueType> stateProbabilityPair = *(behavior.begin()->begin());
|
|
STORM_LOG_ASSERT(stateProbabilityPair.first == 0, "No self loop for failed state.");
|
|
STORM_LOG_ASSERT(storm::utility::isOne<ValueType>(stateProbabilityPair.second), "Probability for failed state != 1.");
|
|
matrixBuilder.addTransition(stateProbabilityPair.first, stateProbabilityPair.second);
|
|
matrixBuilder.finishRow();
|
|
}
|
|
|
|
// Build initial state
|
|
this->stateStorage.initialStateIndices = generator.getInitialStates(std::bind(&ExplicitDFTModelBuilder::getOrAddStateIndex, this, std::placeholders::_1));
|
|
STORM_LOG_ASSERT(stateStorage.initialStateIndices.size() == 1, "Only one initial state assumed.");
|
|
initialStateIndex = stateStorage.initialStateIndices[0];
|
|
STORM_LOG_TRACE("Initial state: " << initialStateIndex);
|
|
|
|
// DFT may be instantly failed due to a constant failure
|
|
// in this case a model only consisting of the uniqueFailedState suffices
|
|
if (initialStateIndex == 0 && this->uniqueFailedState) {
|
|
modelComponents.markovianStates.resize(1);
|
|
modelComponents.deterministicModel = generator.isDeterministicModel();
|
|
|
|
STORM_LOG_TRACE("Markovian states: " << modelComponents.markovianStates);
|
|
STORM_LOG_DEBUG("Model has 1 state");
|
|
STORM_LOG_DEBUG(
|
|
"Model is " << (generator.isDeterministicModel() ? "deterministic" : "non-deterministic"));
|
|
|
|
// Build transition matrix
|
|
modelComponents.transitionMatrix = matrixBuilder.builder.build(1, 1);
|
|
STORM_LOG_TRACE("Transition matrix: " << std::endl << modelComponents.transitionMatrix);
|
|
|
|
buildLabeling();
|
|
return;
|
|
}
|
|
|
|
// Initialize heuristic values for inital state
|
|
STORM_LOG_ASSERT(!statesNotExplored.at(initialStateIndex).second, "Heuristic for initial state is already initialized");
|
|
ExplorationHeuristicPointer heuristic;
|
|
switch (usedHeuristic) {
|
|
case storm::builder::ApproximationHeuristic::DEPTH:
|
|
heuristic = std::make_shared<DFTExplorationHeuristicDepth<ValueType>>(initialStateIndex);
|
|
break;
|
|
case storm::builder::ApproximationHeuristic::PROBABILITY:
|
|
heuristic = std::make_shared<DFTExplorationHeuristicProbability<ValueType>>(initialStateIndex);
|
|
break;
|
|
case storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE:
|
|
heuristic = std::make_shared<DFTExplorationHeuristicBoundDifference<ValueType>>(initialStateIndex);
|
|
break;
|
|
default:
|
|
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Heuristic not known.");
|
|
}
|
|
heuristic->markExpand();
|
|
statesNotExplored[initialStateIndex].second = heuristic;
|
|
explorationQueue.push(heuristic);
|
|
} else {
|
|
initializeNextIteration();
|
|
}
|
|
|
|
if (approximationThreshold > 0.0) {
|
|
switch (usedHeuristic) {
|
|
case storm::builder::ApproximationHeuristic::DEPTH:
|
|
approximationThreshold = iteration + 1;
|
|
break;
|
|
case storm::builder::ApproximationHeuristic::PROBABILITY:
|
|
case storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE:
|
|
approximationThreshold = std::pow(2, -(double)iteration); // Need conversion to avoid overflow when negating
|
|
break;
|
|
default:
|
|
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Heuristic not known.");
|
|
}
|
|
}
|
|
|
|
auto ftSettings = storm::settings::getModule<storm::settings::modules::FaultTreeSettings>();
|
|
if (ftSettings.isMaxDepthSet()) {
|
|
STORM_LOG_ASSERT(usedHeuristic == storm::builder::ApproximationHeuristic::DEPTH, "MaxDepth requires 'depth' exploration heuristic.");
|
|
approximationThreshold = ftSettings.getMaxDepth();
|
|
}
|
|
|
|
exploreStateSpace(approximationThreshold);
|
|
|
|
size_t stateSize = stateStorage.getNumberOfStates() + (this->uniqueFailedState ? 1 : 0);
|
|
modelComponents.markovianStates.resize(stateSize);
|
|
modelComponents.deterministicModel = generator.isDeterministicModel();
|
|
|
|
// Fix the entries in the transition matrix according to the mapping of ids to row group indices
|
|
STORM_LOG_ASSERT(matrixBuilder.getRemapping(initialStateIndex) == initialStateIndex, "Initial state should not be remapped.");
|
|
// TODO: do not consider all rows?
|
|
STORM_LOG_TRACE("Remap matrix: " << matrixBuilder.stateRemapping << ", offset: " << matrixBuilder.mappingOffset);
|
|
matrixBuilder.remap();
|
|
|
|
STORM_LOG_TRACE("State remapping: " << matrixBuilder.stateRemapping);
|
|
STORM_LOG_TRACE("Markovian states: " << modelComponents.markovianStates);
|
|
STORM_LOG_DEBUG("Model has " << stateSize << " states");
|
|
STORM_LOG_DEBUG("Model is " << (generator.isDeterministicModel() ? "deterministic" : "non-deterministic"));
|
|
|
|
// Build transition matrix
|
|
modelComponents.transitionMatrix = matrixBuilder.builder.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");
|
|
}
|
|
|
|
buildLabeling();
|
|
}
|
|
|
|
template<typename ValueType, typename StateType>
|
|
void ExplicitDFTModelBuilder<ValueType, StateType>::initializeNextIteration() {
|
|
STORM_LOG_TRACE("Refining DFT state space");
|
|
|
|
// TODO: should be easier now as skipped states all are at the end of the matrix
|
|
// Push skipped states to explore queue
|
|
// TODO: remove
|
|
for (auto const& skippedState : skippedStates) {
|
|
statesNotExplored[skippedState.second.first->getId()] = skippedState.second;
|
|
explorationQueue.push(skippedState.second.second);
|
|
}
|
|
|
|
// Initialize matrix builder again
|
|
// TODO: avoid copy
|
|
std::vector<uint_fast64_t> copyRemapping = matrixBuilder.stateRemapping;
|
|
matrixBuilder = MatrixBuilder(!generator.isDeterministicModel());
|
|
matrixBuilder.stateRemapping = copyRemapping;
|
|
StateType nrStates = modelComponents.transitionMatrix.getRowGroupCount();
|
|
STORM_LOG_ASSERT(nrStates == matrixBuilder.stateRemapping.size(), "No. of states does not coincide with mapping size.");
|
|
|
|
// Start by creating a remapping from the old indices to the new indices
|
|
std::vector<StateType> indexRemapping = std::vector<StateType>(nrStates, 0);
|
|
auto iterSkipped = skippedStates.begin();
|
|
size_t skippedBefore = 0;
|
|
for (size_t i = 0; i < indexRemapping.size(); ++i) {
|
|
while (iterSkipped != skippedStates.end() && iterSkipped->first <= i) {
|
|
STORM_LOG_ASSERT(iterSkipped->first < indexRemapping.size(), "Skipped is too high.");
|
|
++skippedBefore;
|
|
++iterSkipped;
|
|
}
|
|
indexRemapping[i] = i - skippedBefore;
|
|
}
|
|
|
|
// Set remapping
|
|
size_t nrExpandedStates = nrStates - skippedBefore;
|
|
matrixBuilder.mappingOffset = nrStates;
|
|
STORM_LOG_TRACE("# expanded states: " << nrExpandedStates);
|
|
StateType skippedIndex = nrExpandedStates;
|
|
std::map<StateType, std::pair<DFTStatePointer, ExplorationHeuristicPointer>> skippedStatesNew;
|
|
for (size_t id = 0; id < matrixBuilder.stateRemapping.size(); ++id) {
|
|
StateType index = matrixBuilder.getRemapping(id);
|
|
auto itFind = skippedStates.find(index);
|
|
if (itFind != skippedStates.end()) {
|
|
// Set new mapping for skipped state
|
|
matrixBuilder.stateRemapping[id] = skippedIndex;
|
|
skippedStatesNew[skippedIndex] = itFind->second;
|
|
indexRemapping[index] = skippedIndex;
|
|
++skippedIndex;
|
|
} else {
|
|
// Set new mapping for expanded state
|
|
matrixBuilder.stateRemapping[id] = indexRemapping[index];
|
|
}
|
|
}
|
|
STORM_LOG_TRACE("New state remapping: " << matrixBuilder.stateRemapping);
|
|
std::stringstream ss;
|
|
ss << "Index remapping:" << std::endl;
|
|
for (auto tmp : indexRemapping) {
|
|
ss << tmp << " ";
|
|
}
|
|
STORM_LOG_TRACE(ss.str());
|
|
|
|
// Remap markovian states
|
|
storm::storage::BitVector markovianStatesNew = storm::storage::BitVector(modelComponents.markovianStates.size(), true);
|
|
// Iterate over all not set bits
|
|
modelComponents.markovianStates.complement();
|
|
size_t index = modelComponents.markovianStates.getNextSetIndex(0);
|
|
while (index < modelComponents.markovianStates.size()) {
|
|
markovianStatesNew.set(indexRemapping[index], false);
|
|
index = modelComponents.markovianStates.getNextSetIndex(index+1);
|
|
}
|
|
STORM_LOG_ASSERT(modelComponents.markovianStates.size() - modelComponents.markovianStates.getNumberOfSetBits() == markovianStatesNew.getNumberOfSetBits(), "Remapping of markovian states is wrong.");
|
|
STORM_LOG_ASSERT(markovianStatesNew.size() == nrStates, "No. of states does not coincide with markovian size.");
|
|
modelComponents.markovianStates = markovianStatesNew;
|
|
|
|
// Build submatrix for expanded states
|
|
// TODO: only use row groups when necessary
|
|
for (StateType oldRowGroup = 0; oldRowGroup < modelComponents.transitionMatrix.getRowGroupCount(); ++oldRowGroup) {
|
|
if (indexRemapping[oldRowGroup] < nrExpandedStates) {
|
|
// State is expanded -> copy to new matrix
|
|
matrixBuilder.newRowGroup();
|
|
for (StateType oldRow = modelComponents.transitionMatrix.getRowGroupIndices()[oldRowGroup]; oldRow < modelComponents.transitionMatrix.getRowGroupIndices()[oldRowGroup+1]; ++oldRow) {
|
|
for (typename storm::storage::SparseMatrix<ValueType>::const_iterator itEntry = modelComponents.transitionMatrix.begin(oldRow); itEntry != modelComponents.transitionMatrix.end(oldRow); ++itEntry) {
|
|
auto itFind = skippedStates.find(itEntry->getColumn());
|
|
if (itFind != skippedStates.end()) {
|
|
// Set id for skipped states as we remap it later
|
|
matrixBuilder.addTransition(matrixBuilder.mappingOffset + itFind->second.first->getId(), itEntry->getValue());
|
|
} else {
|
|
// Set newly remapped index for expanded states
|
|
matrixBuilder.addTransition(indexRemapping[itEntry->getColumn()], itEntry->getValue());
|
|
}
|
|
}
|
|
matrixBuilder.finishRow();
|
|
}
|
|
}
|
|
}
|
|
|
|
skippedStates = skippedStatesNew;
|
|
|
|
STORM_LOG_ASSERT(matrixBuilder.getCurrentRowGroup() == nrExpandedStates, "Row group size does not match.");
|
|
skippedStates.clear();
|
|
}
|
|
|
|
template<typename ValueType, typename StateType>
|
|
void ExplicitDFTModelBuilder<ValueType, StateType>::exploreStateSpace(double approximationThreshold) {
|
|
size_t nrExpandedStates = 0;
|
|
size_t nrSkippedStates = 0;
|
|
storm::utility::ProgressMeasurement progress("explored states");
|
|
progress.startNewMeasurement(0);
|
|
// TODO: do not empty queue every time but break before
|
|
while (!explorationQueue.empty()) {
|
|
// Get the first state in the queue
|
|
ExplorationHeuristicPointer currentExplorationHeuristic = explorationQueue.pop();
|
|
StateType currentId = currentExplorationHeuristic->getId();
|
|
auto itFind = statesNotExplored.find(currentId);
|
|
STORM_LOG_ASSERT(itFind != statesNotExplored.end(), "Id " << currentId << " not found");
|
|
DFTStatePointer currentState = itFind->second.first;
|
|
STORM_LOG_ASSERT(currentExplorationHeuristic == itFind->second.second, "Exploration heuristics do not match");
|
|
STORM_LOG_ASSERT(currentState->getId() == currentId, "Ids do not match");
|
|
// Remove it from the list of not explored states
|
|
statesNotExplored.erase(itFind);
|
|
STORM_LOG_ASSERT(stateStorage.stateToId.contains(currentState->status()), "State is not contained in state storage.");
|
|
STORM_LOG_ASSERT(stateStorage.stateToId.getValue(currentState->status()) == currentId, "Ids of states do not coincide.");
|
|
|
|
// Get concrete state if necessary
|
|
if (currentState->isPseudoState()) {
|
|
// Create concrete state from pseudo state
|
|
currentState->construct();
|
|
}
|
|
STORM_LOG_ASSERT(!currentState->isPseudoState(), "State is pseudo state.");
|
|
|
|
// Remember that the current row group was actually filled with the transitions of a different state
|
|
matrixBuilder.setRemapping(currentId);
|
|
|
|
matrixBuilder.newRowGroup();
|
|
|
|
// Try to explore the next state
|
|
generator.load(currentState);
|
|
|
|
//if (approximationThreshold > 0.0 && nrExpandedStates > approximationThreshold && !currentExplorationHeuristic->isExpand()) {
|
|
if (approximationThreshold > 0.0 && currentExplorationHeuristic->isSkip(approximationThreshold)) {
|
|
// Skip the current state
|
|
++nrSkippedStates;
|
|
STORM_LOG_TRACE("Skip expansion of state: " << dft.getStateString(currentState));
|
|
setMarkovian(true);
|
|
// Add transition to target state with temporary value 0
|
|
// TODO: what to do when there is no unique target state?
|
|
//STORM_LOG_ASSERT(this->uniqueFailedState, "Approximation only works with unique failed state");
|
|
matrixBuilder.addTransition(0, storm::utility::zero<ValueType>());
|
|
// Remember skipped state
|
|
skippedStates[matrixBuilder.getCurrentRowGroup() - 1] = std::make_pair(currentState, currentExplorationHeuristic);
|
|
matrixBuilder.finishRow();
|
|
} else {
|
|
// Explore the current state
|
|
++nrExpandedStates;
|
|
storm::generator::StateBehavior<ValueType, StateType> behavior = generator.expand(std::bind(&ExplicitDFTModelBuilder::getOrAddStateIndex, this, std::placeholders::_1));
|
|
STORM_LOG_ASSERT(!behavior.empty(), "Behavior is empty.");
|
|
setMarkovian(behavior.begin()->isMarkovian());
|
|
|
|
// Now add all choices.
|
|
for (auto const& choice : behavior) {
|
|
// Add the probabilistic behavior to the matrix.
|
|
for (auto const& stateProbabilityPair : choice) {
|
|
STORM_LOG_ASSERT(!storm::utility::isZero(stateProbabilityPair.second), "Probability zero.");
|
|
// Set transition to state id + offset. This helps in only remapping all previously skipped states.
|
|
matrixBuilder.addTransition(matrixBuilder.mappingOffset + stateProbabilityPair.first, stateProbabilityPair.second);
|
|
// Set heuristic values for reached states
|
|
auto iter = statesNotExplored.find(stateProbabilityPair.first);
|
|
if (iter != statesNotExplored.end()) {
|
|
// Update heuristic values
|
|
DFTStatePointer state = iter->second.first;
|
|
if (!iter->second.second) {
|
|
// Initialize heuristic values
|
|
ExplorationHeuristicPointer heuristic;
|
|
switch (usedHeuristic) {
|
|
case storm::builder::ApproximationHeuristic::DEPTH:
|
|
heuristic = std::make_shared<DFTExplorationHeuristicDepth<ValueType>>(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass());
|
|
break;
|
|
case storm::builder::ApproximationHeuristic::PROBABILITY:
|
|
heuristic = std::make_shared<DFTExplorationHeuristicProbability<ValueType>>(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass());
|
|
break;
|
|
case storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE:
|
|
heuristic = std::make_shared<DFTExplorationHeuristicBoundDifference<ValueType>>(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass());
|
|
break;
|
|
default:
|
|
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Heuristic not known.");
|
|
}
|
|
|
|
iter->second.second = heuristic;
|
|
//if (state->hasFailed(dft.getTopLevelIndex()) || state->isFailsafe(dft.getTopLevelIndex()) || state->getFailableElements().hasDependencies() || (!state->getFailableElements().hasDependencies() && !state->getFailableElements().hasBEs())) {
|
|
if (state->getFailableElements().hasDependencies() || (!state->getFailableElements().hasDependencies() && !state->getFailableElements().hasBEs())) {
|
|
// Do not skip absorbing state or if reached by dependencies
|
|
iter->second.second->markExpand();
|
|
}
|
|
if (usedHeuristic == storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE) {
|
|
// Compute bounds for heuristic now
|
|
if (state->isPseudoState()) {
|
|
// Create concrete state from pseudo state
|
|
state->construct();
|
|
}
|
|
STORM_LOG_ASSERT(!currentState->isPseudoState(), "State is pseudo state.");
|
|
|
|
// Initialize bounds
|
|
// TODO: avoid hack
|
|
ValueType lowerBound = getLowerBound(state);
|
|
ValueType upperBound = getUpperBound(state);
|
|
heuristic->setBounds(lowerBound, upperBound);
|
|
}
|
|
|
|
explorationQueue.push(heuristic);
|
|
} else if (!iter->second.second->isExpand()) {
|
|
double oldPriority = iter->second.second->getPriority();
|
|
if (iter->second.second->updateHeuristicValues(*currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass())) {
|
|
// Update priority queue
|
|
explorationQueue.update(iter->second.second, oldPriority);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
matrixBuilder.finishRow();
|
|
}
|
|
}
|
|
if (storm::utility::resources::isTerminate()) {
|
|
break;
|
|
}
|
|
// Output number of currently explored states
|
|
if (nrExpandedStates % 100 == 0) {
|
|
progress.updateProgress(nrExpandedStates);
|
|
}
|
|
} // end exploration
|
|
|
|
STORM_LOG_INFO("Expanded " << nrExpandedStates << " states");
|
|
STORM_LOG_INFO("Skipped " << nrSkippedStates << " states");
|
|
STORM_LOG_ASSERT(nrSkippedStates == skippedStates.size(), "Nr skipped states is wrong");
|
|
}
|
|
|
|
template<typename ValueType, typename StateType>
|
|
void ExplicitDFTModelBuilder<ValueType, StateType>::buildLabeling() {
|
|
// Build state labeling
|
|
modelComponents.stateLabeling = storm::models::sparse::StateLabeling(modelComponents.transitionMatrix.getRowGroupCount());
|
|
// Initial state
|
|
modelComponents.stateLabeling.addLabel("init");
|
|
STORM_LOG_ASSERT(matrixBuilder.getRemapping(initialStateIndex) == initialStateIndex, "Initial state should not be remapped.");
|
|
modelComponents.stateLabeling.addLabelToState("init", initialStateIndex);
|
|
// System failure
|
|
modelComponents.stateLabeling.addLabel("failed");
|
|
|
|
// Label all states corresponding to their status (failed, don't care BE)
|
|
// Collect labels for all necessary elements
|
|
for (size_t id = 0; id < dft.nrElements(); ++id) {
|
|
std::shared_ptr<storage::DFTElement<ValueType> const> element = dft.getElement(id);
|
|
if (element->isRelevant()) {
|
|
modelComponents.stateLabeling.addLabel(element->name() + "_failed");
|
|
modelComponents.stateLabeling.addLabel(element->name() + "_dc");
|
|
}
|
|
}
|
|
|
|
// Set labels to states
|
|
if (this->uniqueFailedState) {
|
|
// Unique failed state has label 0
|
|
modelComponents.stateLabeling.addLabelToState("failed", 0);
|
|
}
|
|
for (auto const& stateIdPair : stateStorage.stateToId) {
|
|
storm::storage::BitVector state = stateIdPair.first;
|
|
size_t stateId = matrixBuilder.getRemapping(stateIdPair.second);
|
|
if (dft.hasFailed(state, *stateGenerationInfo)) {
|
|
modelComponents.stateLabeling.addLabelToState("failed", stateId);
|
|
}
|
|
// Set failed/don't care status for each necessary element
|
|
for (size_t id = 0; id < dft.nrElements(); ++id) {
|
|
std::shared_ptr<storage::DFTElement<ValueType> const> element = dft.getElement(id);
|
|
if (element->isRelevant()){
|
|
storm::storage::DFTElementState elementState = storm::storage::DFTState<ValueType>::getElementState(state, *stateGenerationInfo, element->id());
|
|
switch (elementState) {
|
|
case storm::storage::DFTElementState::Failed:
|
|
modelComponents.stateLabeling.addLabelToState(element->name() + "_failed", stateId);
|
|
break;
|
|
case storm::storage::DFTElementState::DontCare:
|
|
modelComponents.stateLabeling.addLabelToState(element->name() + "_dc", stateId);
|
|
break;
|
|
case storm::storage::DFTElementState::Operational:
|
|
case storm::storage::DFTElementState::Failsafe:
|
|
// do nothing
|
|
break;
|
|
default:
|
|
STORM_LOG_ASSERT(false, "Unknown element state " << elementState);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
STORM_LOG_TRACE(modelComponents.stateLabeling);
|
|
}
|
|
|
|
template<typename ValueType, typename StateType>
|
|
std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilder<ValueType, StateType>::getModel() {
|
|
if (storm::settings::getModule<storm::settings::modules::FaultTreeSettings>().isMaxDepthSet() && skippedStates.size() > 0) {
|
|
// Give skipped states separate label "skipped"
|
|
modelComponents.stateLabeling.addLabel("skipped");
|
|
for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) {
|
|
modelComponents.stateLabeling.addLabelToState("skipped", it->first);
|
|
}
|
|
} else{
|
|
STORM_LOG_ASSERT(skippedStates.size() == 0, "Concrete model has skipped states");
|
|
}
|
|
|
|
return createModel(false);
|
|
}
|
|
|
|
template<typename ValueType, typename StateType>
|
|
std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilder<ValueType, StateType>::getModelApproximation(bool lowerBound, bool expectedTime) {
|
|
if (expectedTime) {
|
|
// TODO: handle case with no skipped states
|
|
changeMatrixBound(modelComponents.transitionMatrix, lowerBound);
|
|
return createModel(true);
|
|
} else {
|
|
// Change model for probabilities
|
|
// TODO: make nicer
|
|
storm::storage::SparseMatrix<ValueType> matrix = modelComponents.transitionMatrix;
|
|
storm::models::sparse::StateLabeling labeling = modelComponents.stateLabeling;
|
|
if (lowerBound) {
|
|
// Set self loop for lower bound
|
|
for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) {
|
|
auto matrixEntry = matrix.getRow(it->first, 0).begin();
|
|
STORM_LOG_ASSERT(matrixEntry->getColumn() == 0, "Transition has wrong target state.");
|
|
STORM_LOG_ASSERT(!it->second.first->isPseudoState(), "State is still pseudo state.");
|
|
matrixEntry->setValue(storm::utility::one<ValueType>());
|
|
matrixEntry->setColumn(it->first);
|
|
}
|
|
} else {
|
|
// Make skipped states failed states for upper bound
|
|
storm::storage::BitVector failedStates = modelComponents.stateLabeling.getStates("failed");
|
|
for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) {
|
|
failedStates.set(it->first);
|
|
}
|
|
labeling.setStates("failed", failedStates);
|
|
}
|
|
|
|
std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
|
|
if (modelComponents.deterministicModel) {
|
|
model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(std::move(matrix), std::move(labeling));
|
|
} else {
|
|
// Build MA
|
|
// Compute exit rates
|
|
// TODO: avoid computing multiple times
|
|
modelComponents.exitRates = std::vector<ValueType>(modelComponents.markovianStates.size());
|
|
std::vector<typename storm::storage::SparseMatrix<ValueType>::index_type> indices = matrix.getRowGroupIndices();
|
|
for (StateType stateIndex = 0; stateIndex < modelComponents.markovianStates.size(); ++stateIndex) {
|
|
if (modelComponents.markovianStates[stateIndex]) {
|
|
modelComponents.exitRates[stateIndex] = matrix.getRowSum(indices[stateIndex]);
|
|
} else {
|
|
modelComponents.exitRates[stateIndex] = storm::utility::zero<ValueType>();
|
|
}
|
|
}
|
|
STORM_LOG_TRACE("Exit rates: " << modelComponents.exitRates);
|
|
|
|
storm::storage::sparse::ModelComponents<ValueType> maComponents(std::move(matrix), std::move(labeling));
|
|
maComponents.rateTransitions = true;
|
|
maComponents.markovianStates = modelComponents.markovianStates;
|
|
maComponents.exitRates = modelComponents.exitRates;
|
|
std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(maComponents));
|
|
if (ma->hasOnlyTrivialNondeterminism()) {
|
|
// Markov automaton can be converted into CTMC
|
|
// TODO: change components which were not moved accordingly
|
|
model = ma->convertToCtmc();
|
|
} else {
|
|
model = ma;
|
|
}
|
|
|
|
}
|
|
|
|
if (model->getNumberOfStates() <= 15) {
|
|
STORM_LOG_TRACE("Transition matrix: " << std::endl << model->getTransitionMatrix());
|
|
} else {
|
|
STORM_LOG_TRACE("Transition matrix: too big to print");
|
|
}
|
|
return model;
|
|
}
|
|
}
|
|
|
|
template<typename ValueType, typename StateType>
|
|
std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilder<ValueType, StateType>::createModel(bool copy) {
|
|
std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
|
|
|
|
if (modelComponents.deterministicModel) {
|
|
// Build CTMC
|
|
if (copy) {
|
|
model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(modelComponents.transitionMatrix, modelComponents.stateLabeling);
|
|
} else {
|
|
model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling));
|
|
}
|
|
} else {
|
|
// Build MA
|
|
// Compute exit rates
|
|
// TODO: avoid computing multiple times
|
|
modelComponents.exitRates = std::vector<ValueType>(modelComponents.markovianStates.size());
|
|
std::vector<typename storm::storage::SparseMatrix<ValueType>::index_type> indices = modelComponents.transitionMatrix.getRowGroupIndices();
|
|
for (StateType stateIndex = 0; stateIndex < modelComponents.markovianStates.size(); ++stateIndex) {
|
|
if (modelComponents.markovianStates[stateIndex]) {
|
|
modelComponents.exitRates[stateIndex] = modelComponents.transitionMatrix.getRowSum(indices[stateIndex]);
|
|
} else {
|
|
modelComponents.exitRates[stateIndex] = storm::utility::zero<ValueType>();
|
|
}
|
|
}
|
|
STORM_LOG_TRACE("Exit rates: " << modelComponents.exitRates);
|
|
|
|
std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma;
|
|
if (copy) {
|
|
storm::storage::sparse::ModelComponents<ValueType> maComponents(modelComponents.transitionMatrix, modelComponents.stateLabeling);
|
|
maComponents.rateTransitions = true;
|
|
maComponents.markovianStates = modelComponents.markovianStates;
|
|
maComponents.exitRates = modelComponents.exitRates;
|
|
ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(maComponents));
|
|
} else {
|
|
storm::storage::sparse::ModelComponents<ValueType> maComponents(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling));
|
|
maComponents.rateTransitions = true;
|
|
maComponents.markovianStates = std::move(modelComponents.markovianStates);
|
|
maComponents.exitRates = std::move(modelComponents.exitRates);
|
|
ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(maComponents));
|
|
}
|
|
if (ma->hasOnlyTrivialNondeterminism()) {
|
|
model = ma->convertToCtmc();
|
|
} else {
|
|
model = ma;
|
|
}
|
|
}
|
|
|
|
if (model->getNumberOfStates() <= 15) {
|
|
STORM_LOG_TRACE("Transition matrix: " << std::endl << model->getTransitionMatrix());
|
|
} else {
|
|
STORM_LOG_TRACE("Transition matrix: too big to print");
|
|
}
|
|
return model;
|
|
}
|
|
|
|
template<typename ValueType, typename StateType>
|
|
void ExplicitDFTModelBuilder<ValueType, StateType>::changeMatrixBound(storm::storage::SparseMatrix<ValueType> & matrix, bool lowerBound) const {
|
|
// Set lower bound for skipped states
|
|
for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) {
|
|
auto matrixEntry = matrix.getRow(it->first, 0).begin();
|
|
STORM_LOG_ASSERT(matrixEntry->getColumn() == 0, "Transition has wrong target state.");
|
|
STORM_LOG_ASSERT(!it->second.first->isPseudoState(), "State is still pseudo state.");
|
|
|
|
ExplorationHeuristicPointer heuristic = it->second.second;
|
|
if (storm::utility::isInfinity(heuristic->getUpperBound())) {
|
|
// Initialize bounds
|
|
ValueType lowerBound = getLowerBound(it->second.first);
|
|
ValueType upperBound = getUpperBound(it->second.first);
|
|
heuristic->setBounds(lowerBound, upperBound);
|
|
}
|
|
|
|
// Change bound
|
|
if (lowerBound) {
|
|
matrixEntry->setValue(it->second.second->getLowerBound());
|
|
} else {
|
|
matrixEntry->setValue(it->second.second->getUpperBound());
|
|
}
|
|
}
|
|
}
|
|
|
|
template<typename ValueType, typename StateType>
|
|
ValueType ExplicitDFTModelBuilder<ValueType, StateType>::getLowerBound(DFTStatePointer const& state) const {
|
|
// Get the lower bound by considering the failure of all possible BEs
|
|
ValueType lowerBound = storm::utility::zero<ValueType>();
|
|
for (state->getFailableElements().init(false); !state->getFailableElements().isEnd(); state->getFailableElements().next()) {
|
|
lowerBound += state->getBERate(state->getFailableElements().get());
|
|
}
|
|
STORM_LOG_TRACE("Lower bound is " << lowerBound << " for state " << state->getId());
|
|
return lowerBound;
|
|
}
|
|
|
|
template<typename ValueType, typename StateType>
|
|
ValueType ExplicitDFTModelBuilder<ValueType, StateType>::getUpperBound(DFTStatePointer const& state) const {
|
|
if (state->hasFailed(dft.getTopLevelIndex())) {
|
|
return storm::utility::zero<ValueType>();
|
|
}
|
|
|
|
// Get the upper bound by considering the failure of all BEs
|
|
ValueType upperBound = storm::utility::one<ValueType>();
|
|
ValueType rateSum = storm::utility::zero<ValueType>();
|
|
|
|
// Compute for each independent subtree
|
|
for (std::vector<size_t> const& subtree : subtreeBEs) {
|
|
// Get all possible rates
|
|
std::vector<ValueType> rates;
|
|
storm::storage::BitVector coldBEs(subtree.size(), false);
|
|
for (size_t i = 0; i < subtree.size(); ++i) {
|
|
size_t id = subtree[i];
|
|
// Consider only still operational BEs
|
|
if (state->isOperational(id)) {
|
|
auto be = dft.getBasicElement(id);
|
|
switch (be->type()) {
|
|
case storm::storage::DFTElementType::BE_EXP:
|
|
{
|
|
// Get BE rate
|
|
ValueType rate = state->getBERate(id);
|
|
if (storm::utility::isZero<ValueType>(rate)) {
|
|
// Get active failure rate for cold BE
|
|
auto beExp = std::static_pointer_cast<storm::storage::BEExponential<ValueType> const>(be);
|
|
rate = beExp->activeFailureRate();
|
|
STORM_LOG_ASSERT(!storm::utility::isZero<ValueType>(rate), "Failure rate should not be zero.");
|
|
// Mark BE as cold
|
|
coldBEs.set(i, true);
|
|
}
|
|
rates.push_back(rate);
|
|
rateSum += rate;
|
|
break;
|
|
}
|
|
case storm::storage::DFTElementType::BE_CONST:
|
|
// Ignore BE which cannot fail
|
|
continue;
|
|
default:
|
|
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE of type '" << be->type() << "' is not known.");
|
|
break;
|
|
}
|
|
}
|
|
}
|
|
STORM_LOG_ASSERT(rates.size() > 0, "No rates failable");
|
|
|
|
// Sort rates
|
|
std::sort(rates.begin(), rates.end());
|
|
std::vector<size_t> rateCount(rates.size(), 0);
|
|
size_t lastIndex = 0;
|
|
for (size_t i = 0; i < rates.size(); ++i) {
|
|
if (rates[lastIndex] != rates[i]) {
|
|
lastIndex = i;
|
|
}
|
|
++rateCount[lastIndex];
|
|
}
|
|
|
|
for (size_t i = 0; i < rates.size(); ++i) {
|
|
// Cold BEs cannot fail in the first step
|
|
if (!coldBEs.get(i) && rateCount[i] > 0) {
|
|
std::iter_swap(rates.begin() + i, rates.end() - 1);
|
|
// Compute AND MTTF of subtree without current rate and scale with current rate
|
|
upperBound += rates.back() * rateCount[i] * computeMTTFAnd(rates, rates.size() - 1);
|
|
// Swap back
|
|
// TODO try to avoid swapping back
|
|
std::iter_swap(rates.begin() + i, rates.end() - 1);
|
|
}
|
|
}
|
|
}
|
|
|
|
STORM_LOG_TRACE("Upper bound is " << (rateSum / upperBound) << " for state " << state->getId());
|
|
STORM_LOG_ASSERT(!storm::utility::isZero(upperBound), "Upper bound is 0");
|
|
STORM_LOG_ASSERT(!storm::utility::isZero(rateSum), "State is absorbing");
|
|
return rateSum / upperBound;
|
|
}
|
|
|
|
template<typename ValueType, typename StateType>
|
|
ValueType ExplicitDFTModelBuilder<ValueType, StateType>::computeMTTFAnd(std::vector<ValueType> const& rates, size_t size) const {
|
|
ValueType result = storm::utility::zero<ValueType>();
|
|
if (size == 0) {
|
|
return result;
|
|
}
|
|
|
|
// TODO: works only for <64 BEs!
|
|
// WARNING: this code produces wrong results for more than 32 BEs
|
|
/*for (size_t i = 1; i < 4 && i <= rates.size(); ++i) {
|
|
size_t permutation = smallestIntWithNBitsSet(static_cast<size_t>(i));
|
|
ValueType sum = storm::utility::zero<ValueType>();
|
|
do {
|
|
ValueType permResult = storm::utility::zero<ValueType>();
|
|
for(size_t j = 0; j < rates.size(); ++j) {
|
|
if(permutation & static_cast<size_t>(1 << static_cast<size_t>(j))) {
|
|
// WARNING: if the first bit is set, it also recognizes the 32nd bit as set
|
|
// TODO: fix
|
|
permResult += rates[j];
|
|
}
|
|
}
|
|
permutation = nextBitPermutation(permutation);
|
|
STORM_LOG_ASSERT(!storm::utility::isZero(permResult), "PermResult is 0");
|
|
sum += storm::utility::one<ValueType>() / permResult;
|
|
} while(permutation < (static_cast<size_t>(1) << rates.size()) && permutation != 0);
|
|
if (i % 2 == 0) {
|
|
result -= sum;
|
|
} else {
|
|
result += sum;
|
|
}
|
|
}*/
|
|
|
|
// Compute result with permutations of size <= 3
|
|
ValueType one = storm::utility::one<ValueType>();
|
|
for (size_t i1 = 0; i1 < size; ++i1) {
|
|
// + 1/a
|
|
ValueType sum = rates[i1];
|
|
result += one / sum;
|
|
for (size_t i2 = 0; i2 < i1; ++i2) {
|
|
// - 1/(a+b)
|
|
ValueType sum2 = sum + rates[i2];
|
|
result -= one / sum2;
|
|
for (size_t i3 = 0; i3 < i2; ++i3) {
|
|
// + 1/(a+b+c)
|
|
result += one / (sum2 + rates[i3]);
|
|
}
|
|
}
|
|
}
|
|
|
|
STORM_LOG_ASSERT(!storm::utility::isZero(result), "UpperBound is 0");
|
|
return result;
|
|
}
|
|
|
|
template<typename ValueType, typename StateType>
|
|
StateType ExplicitDFTModelBuilder<ValueType, StateType>::getOrAddStateIndex(DFTStatePointer const& state) {
|
|
StateType stateId;
|
|
bool changed = false;
|
|
|
|
if (stateGenerationInfo->hasSymmetries()) {
|
|
// Order state by symmetry
|
|
STORM_LOG_TRACE("Check for symmetry: " << dft.getStateString(state));
|
|
changed = state->orderBySymmetry();
|
|
STORM_LOG_TRACE("State " << (changed ? "changed to " : "did not change") << (changed ? dft.getStateString(state) : ""));
|
|
}
|
|
|
|
if (stateStorage.stateToId.contains(state->status())) {
|
|
// State already exists
|
|
stateId = stateStorage.stateToId.getValue(state->status());
|
|
STORM_LOG_TRACE("State " << dft.getStateString(state) << " with id " << stateId << " already exists");
|
|
if (!changed) {
|
|
// Check if state is pseudo state
|
|
// If state is explored already the possible pseudo state was already constructed
|
|
auto iter = statesNotExplored.find(stateId);
|
|
if (iter != statesNotExplored.end() && iter->second.first->isPseudoState()) {
|
|
// Create pseudo state now
|
|
STORM_LOG_ASSERT(iter->second.first->getId() == stateId, "Ids do not match.");
|
|
STORM_LOG_ASSERT(iter->second.first->status() == state->status(), "Pseudo states do not coincide.");
|
|
state->setId(stateId);
|
|
// Update mapping to map to concrete state now
|
|
// TODO: just change pointer?
|
|
statesNotExplored[stateId] = std::make_pair(state, iter->second.second);
|
|
// We do not push the new state on the exploration queue as the pseudo state was already pushed
|
|
STORM_LOG_TRACE("Created pseudo state " << dft.getStateString(state));
|
|
}
|
|
}
|
|
} else {
|
|
// State does not exist yet
|
|
STORM_LOG_ASSERT(state->isPseudoState() == changed, "State type (pseudo/concrete) wrong.");
|
|
// Create new state
|
|
state->setId(newIndex++);
|
|
stateId = stateStorage.stateToId.findOrAdd(state->status(), state->getId());
|
|
STORM_LOG_ASSERT(stateId == state->getId(), "Ids do not match.");
|
|
// Insert state as not yet explored
|
|
ExplorationHeuristicPointer nullHeuristic;
|
|
statesNotExplored[stateId] = std::make_pair(state, nullHeuristic);
|
|
// Reserve one slot for the new state in the remapping
|
|
matrixBuilder.stateRemapping.push_back(0);
|
|
STORM_LOG_TRACE("New " << (state->isPseudoState() ? "pseudo" : "concrete") << " state: " << dft.getStateString(state));
|
|
}
|
|
return stateId;
|
|
}
|
|
|
|
template<typename ValueType, typename StateType>
|
|
void ExplicitDFTModelBuilder<ValueType, StateType>::setMarkovian(bool markovian) {
|
|
if (matrixBuilder.getCurrentRowGroup() > modelComponents.markovianStates.size()) {
|
|
// Resize BitVector
|
|
modelComponents.markovianStates.resize(modelComponents.markovianStates.size() + INITIAL_BITVECTOR_SIZE);
|
|
}
|
|
modelComponents.markovianStates.set(matrixBuilder.getCurrentRowGroup() - 1, markovian);
|
|
}
|
|
|
|
template<typename ValueType, typename StateType>
|
|
void ExplicitDFTModelBuilder<ValueType, StateType>::printNotExplored() const {
|
|
std::cout << "states not explored:" << std::endl;
|
|
for (auto it : statesNotExplored) {
|
|
std::cout << it.first << " -> " << dft.getStateString(it.second.first) << std::endl;
|
|
}
|
|
}
|
|
|
|
|
|
// Explicitly instantiate the class.
|
|
template class ExplicitDFTModelBuilder<double>;
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template class ExplicitDFTModelBuilder<storm::RationalFunction>;
|
|
#endif
|
|
|
|
} // namespace builder
|
|
} // namespace storm
|
|
|
|
|