From aab45d4eabe6097de9c9f3e409e456cc64f989a5 Mon Sep 17 00:00:00 2001 From: Mavo Date: Mon, 10 Oct 2016 16:40:10 +0200 Subject: [PATCH] Naive iterative refinement of approximation Former-commit-id: e1620cdefd307b984df1ac164a77797d3c838c99 --- src/builder/ExplicitDFTModelBuilderApprox.cpp | 321 ++++++++++++------ src/builder/ExplicitDFTModelBuilderApprox.h | 147 ++++++-- src/generator/DftNextStateGenerator.cpp | 2 +- src/generator/DftNextStateGenerator.h | 2 +- src/modelchecker/dft/DFTModelChecker.cpp | 25 +- src/storage/dft/DFTState.h | 4 +- 6 files changed, 340 insertions(+), 161 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index 74c448c25..b9eda6308 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -6,7 +6,6 @@ #include #include "src/settings/modules/DFTSettings.h" #include "src/settings/SettingsManager.h" -#include "src/generator/DftNextStateGenerator.h" #include namespace storm { @@ -18,80 +17,212 @@ namespace storm { } template - ExplicitDFTModelBuilderApprox::ExplicitDFTModelBuilderApprox(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) : dft(dft), enableDC(enableDC), stateStorage(((dft.stateVectorSize() / 64) + 1) * 64) { + ExplicitDFTModelBuilderApprox::MatrixBuilder::MatrixBuilder(bool canHaveNondeterminism) : mappingOffset(0), stateRemapping(), currentRowGroup(0), currentRow(0) { + // Create matrix builder + builder = storm::storage::SparseMatrixBuilder(0, 0, 0, false, canHaveNondeterminism, 0); + } + + template + ExplicitDFTModelBuilderApprox::ExplicitDFTModelBuilderApprox(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) : dft(dft), stateGenerationInfo(std::make_shared(dft.buildStateGenerationInfo(symmetries))), enableDC(enableDC), generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates), matrixBuilder(!generator.isDeterministicModel()), stateStorage(((dft.stateVectorSize() / 64) + 1) * 64) { // stateVectorSize is bound for size of bitvector - stateGenerationInfo = std::make_shared(dft.buildStateGenerationInfo(symmetries)); } template - void ExplicitDFTModelBuilderApprox::buildModel(LabelOptions const& labelOpts, double approximationError) { + void ExplicitDFTModelBuilderApprox::buildModel(LabelOptions const& labelOpts, bool firstTime, double approximationError) { STORM_LOG_TRACE("Generating DFT state space"); // Initialize - StateType currentRowGroup = 0; - StateType currentRow = 0; - size_t pseudoStatesToCheck = 0; - modelComponents.markovianStates = storm::storage::BitVector(INITIAL_BITVECTOR_SIZE); - // Create generator - storm::generator::DftNextStateGenerator generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates); generator.setApproximationError(approximationError); - // Create sparse matrix builder - storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, 0, 0, false, !generator.isDeterministicModel(), 0); - if(mergeFailedStates) { - // Introduce explicit fail state - storm::generator::StateBehavior behavior = generator.createMergeFailedState([this] (DFTStatePointer const& state) { + if (firstTime) { + // Initialize + modelComponents.markovianStates = storm::storage::BitVector(INITIAL_BITVECTOR_SIZE); + + if(mergeFailedStates) { + // Introduce explicit fail state + storm::generator::StateBehavior behavior = generator.createMergeFailedState([this] (DFTStatePointer const& state) { this->failedStateId = newIndex++; - stateRemapping.push_back(0); + matrixBuilder.stateRemapping.push_back(0); return this->failedStateId; } ); - setRemapping(failedStateId, currentRowGroup); + matrixBuilder.setRemapping(failedStateId); + STORM_LOG_ASSERT(!behavior.empty(), "Behavior is empty."); + matrixBuilder.newRowGroup(); + setMarkovian(behavior.begin()->isMarkovian()); + + // Now add self loop. + // TODO Matthias: 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 stateProbabilityPair = *(behavior.begin()->begin()); + STORM_LOG_ASSERT(stateProbabilityPair.first == failedStateId, "No self loop for failed state."); + STORM_LOG_ASSERT(storm::utility::isOne(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(&ExplicitDFTModelBuilderApprox::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); + + } else { + initializeNextIteration(); + } + + exploreStateSpace(); + + size_t stateSize = stateStorage.getNumberOfStates() + (mergeFailedStates ? 1 : 0); + modelComponents.markovianStates.resize(stateSize); + modelComponents.deterministicModel = generator.isDeterministicModel(); + + // Replace pseudo states in matrix + // TODO Matthias: avoid hack with fixed int type + std::vector 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."); + matrixBuilder.builder.replaceColumns(pseudoStatesVector, OFFSET_PSEUDO_STATE); + mPseudoStatesMapping.clear(); + + // Fix the entries in the transition matrix according to the mapping of ids to row group indices + STORM_LOG_ASSERT(matrixBuilder.stateRemapping[initialStateIndex] == initialStateIndex, "Initial state should not be remapped."); + // TODO Matthias: do not consider all rows? + matrixBuilder.remap(); + + STORM_LOG_TRACE("State remapping: " << matrixBuilder.stateRemapping); + STORM_LOG_TRACE("Markovian states: " << modelComponents.markovianStates); + STORM_LOG_DEBUG("Generated " << stateSize << " states"); + STORM_LOG_DEBUG("Skipped " << skippedStates.size() << " 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"); + } - STORM_LOG_ASSERT(!behavior.empty(), "Behavior is empty."); - setMarkovian(currentRowGroup, behavior.begin()->isMarkovian()); + buildLabeling(labelOpts); + } - // If the model is nondeterministic, we need to open a row group. - if (!generator.isDeterministicModel()) { - transitionMatrixBuilder.newRowGroup(currentRow); + template + void ExplicitDFTModelBuilderApprox::initializeNextIteration() { + STORM_LOG_TRACE("Refining DFT state space"); + + // Initialize matrix builder again + // TODO Matthias: avoid copy + std::vector 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 indexRemapping = std::vector(nrStates, 0); + auto iterSkipped = skippedStates.begin(); + size_t skippedBefore = 0; + for (size_t i = 0; i < indexRemapping.size(); ++i) { + while (iterSkipped->first <= i) { + ++skippedBefore; + ++iterSkipped; } + indexRemapping[i] = i - skippedBefore; + } - // Now add self loop. - // TODO Matthias: 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 stateProbabilityPair = *(behavior.begin()->begin()); - STORM_LOG_ASSERT(stateProbabilityPair.first == failedStateId, "No self loop for failed state."); - STORM_LOG_ASSERT(storm::utility::isOne(stateProbabilityPair.second), "Probability for failed state != 1."); - transitionMatrixBuilder.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); - ++currentRow; - ++currentRowGroup; + // Set remapping + size_t nrExpandedStates = nrStates - skippedBefore; + matrixBuilder.mappingOffset = nrStates; + STORM_LOG_TRACE("# expanded states: " << nrExpandedStates); + StateType skippedIndex = nrExpandedStates; + std::map skippedStatesNew; + for (size_t id = 0; id < matrixBuilder.stateRemapping.size(); ++id) { + StateType index = matrixBuilder.stateRemapping[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); } + 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 Matthias: 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::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->getId(), itEntry->getValue()); + } else { + // Set newly remapped index for expanded states + matrixBuilder.addTransition(indexRemapping[itEntry->getColumn()], itEntry->getValue()); + } + } + matrixBuilder.finishRow(); + } + } + } + + skippedStates = skippedStatesNew; - // Create a callback for the next-state generator to enable it to add states - std::function stateToIdCallback = std::bind(&ExplicitDFTModelBuilderApprox::getOrAddStateIndex, this, std::placeholders::_1); + STORM_LOG_ASSERT(matrixBuilder.getCurrentRowGroup() == nrExpandedStates, "Row group size does not match."); - // Build initial states - this->stateStorage.initialStateIndices = generator.getInitialStates(stateToIdCallback); - STORM_LOG_ASSERT(stateStorage.initialStateIndices.size() == 1, "Only one initial state assumed."); - StateType initialStateIndex = stateStorage.initialStateIndices[0]; - STORM_LOG_TRACE("Initial state: " << initialStateIndex); + // Explore all skipped states now + for (auto const& skippedState : skippedStates) { + skippedState.second->setSkip(false); + statesToExplore.push_front(skippedState.second); + } + skippedStates.clear(); + } - // Explore state space + template + void ExplicitDFTModelBuilderApprox::exploreStateSpace() { bool explorationFinished = false; + size_t pseudoStatesToCheck = 0; while (!explorationFinished) { // Get the first state in the queue DFTStatePointer currentState = statesToExplore.front(); STORM_LOG_ASSERT(stateStorage.stateToId.getValue(currentState->status()) == currentState->getId(), "Ids of states do not coincide."); statesToExplore.pop_front(); - // Remember that this row group was actually filled with the transitions of a different state - setRemapping(currentState->getId(), currentRowGroup); + // Remember that the current row group was actually filled with the transitions of a different state + matrixBuilder.setRemapping(currentState->getId()); - // If the model is nondeterministic, we need to open a row group. - if (!generator.isDeterministicModel()) { - transitionMatrixBuilder.newRowGroup(currentRow); - } + matrixBuilder.newRowGroup(); // Try to explore the next state generator.load(currentState); @@ -99,18 +230,18 @@ namespace storm { if (currentState->isSkip()) { // Skip the current state STORM_LOG_TRACE("Skip expansion of state: " << dft.getStateString(currentState)); - setMarkovian(currentRowGroup, true); + setMarkovian(true); // Add transition to target state with temporary value 0 // TODO Matthias: what to do when there is no unique target state? - transitionMatrixBuilder.addNextValue(currentRow, failedStateId, storm::utility::zero()); + matrixBuilder.addTransition(failedStateId, storm::utility::zero()); // Remember skipped state - skippedStates[currentRow] = currentState; - ++currentRow; + skippedStates[matrixBuilder.getCurrentRowGroup() - 1] = currentState; + matrixBuilder.finishRow(); } else { // Explore the current state - storm::generator::StateBehavior behavior = generator.expand(stateToIdCallback); + storm::generator::StateBehavior behavior = generator.expand(std::bind(&ExplicitDFTModelBuilderApprox::getOrAddStateIndex, this, std::placeholders::_1)); STORM_LOG_ASSERT(!behavior.empty(), "Behavior is empty."); - setMarkovian(currentRowGroup, behavior.begin()->isMarkovian()); + setMarkovian(behavior.begin()->isMarkovian()); // Now add all choices. for (auto const& choice : behavior) { @@ -130,15 +261,12 @@ namespace storm { } } } - - transitionMatrixBuilder.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); + matrixBuilder.addTransition(matrixBuilder.mappingOffset + stateProbabilityPair.first, stateProbabilityPair.second); } - ++currentRow; + matrixBuilder.finishRow(); } } - ++currentRowGroup; - if (statesToExplore.empty()) { explorationFinished = true; // Before ending the exploration check for pseudo states which are not initialized yet @@ -161,45 +289,13 @@ namespace storm { } } // end exploration + } - size_t stateSize = stateStorage.getNumberOfStates() + (mergeFailedStates ? 1 : 0); - modelComponents.markovianStates.resize(stateSize); - modelComponents.deterministicModel = generator.isDeterministicModel(); - - // Replace pseudo states in matrix - // TODO Matthias: avoid hack with fixed int type - std::vector 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); - - - // Fix the entries in the matrix according to the (reversed) mapping of row groups to indices - STORM_LOG_ASSERT(stateRemapping[initialStateIndex] == initialStateIndex, "Initial state should not be remapped."); - // Fix the transition matrix - transitionMatrixBuilder.replaceColumns(stateRemapping, 0); - // Fix the hash map storing the mapping states -> ids - this->stateStorage.stateToId.remap([this] (StateType const& state) { return this->stateRemapping[state]; } ); - - STORM_LOG_TRACE("State remapping: " << stateRemapping); - STORM_LOG_TRACE("Markovian states: " << modelComponents.markovianStates); - STORM_LOG_DEBUG("Generated " << stateSize << " states"); - STORM_LOG_DEBUG("Skipped " << skippedStates.size() << " states"); - STORM_LOG_DEBUG("Model is " << (generator.isDeterministicModel() ? "deterministic" : "non-deterministic")); - - // 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"); - } - + template + void ExplicitDFTModelBuilderApprox::buildLabeling(LabelOptions const& labelOpts) { // Build state labeling - modelComponents.stateLabeling = storm::models::sparse::StateLabeling(stateSize); - // Initial state is always first state without any failure + modelComponents.stateLabeling = storm::models::sparse::StateLabeling(modelComponents.transitionMatrix.getRowGroupCount()); + // Initial state modelComponents.stateLabeling.addLabel("init"); modelComponents.stateLabeling.addLabelToState("init", initialStateIndex); // Label all states corresponding to their status (failed, failsafe, failed BE) @@ -259,13 +355,14 @@ namespace storm { template std::shared_ptr> ExplicitDFTModelBuilderApprox::createModel(bool copy) { + std::shared_ptr> model; + if (modelComponents.deterministicModel) { // Build CTMC if (copy) { - return std::make_shared>(modelComponents.transitionMatrix, modelComponents.stateLabeling); - + model = std::make_shared>(modelComponents.transitionMatrix, modelComponents.stateLabeling); } else { - return std::make_shared>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling)); + model = std::make_shared>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling)); } } else { // Build MA @@ -290,11 +387,21 @@ namespace storm { } if (ma->hasOnlyTrivialNondeterminism()) { // Markov automaton can be converted into CTMC - return ma->convertToCTMC(); + // TODO Matthias: change components which were not moved accordingly + model = ma->convertToCTMC(); } else { - return ma; + model = ma; } } + + STORM_LOG_DEBUG("No. states: " << model->getNumberOfStates()); + STORM_LOG_DEBUG("No. transitions: " << model->getNumberOfTransitions()); + 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 @@ -369,7 +476,7 @@ namespace storm { STORM_LOG_ASSERT(stateId == state->getId(), "Ids do not match."); STORM_LOG_TRACE("Remember state for later creation: " << dft.getStateString(state)); // Reserve one slot for the coming state in the remapping - stateRemapping.push_back(0); + matrixBuilder.stateRemapping.push_back(0); } else { // Create new state state->setId(newIndex++); @@ -379,25 +486,19 @@ namespace storm { statesToExplore.push_front(state); // Reserve one slot for the new state in the remapping - stateRemapping.push_back(0); + matrixBuilder.stateRemapping.push_back(0); } } return stateId; } template - void ExplicitDFTModelBuilderApprox::setMarkovian(StateType id, bool markovian) { - if (id >= modelComponents.markovianStates.size()) { + void ExplicitDFTModelBuilderApprox::setMarkovian(bool markovian) { + if (matrixBuilder.getCurrentRowGroup() > modelComponents.markovianStates.size()) { // Resize BitVector modelComponents.markovianStates.resize(modelComponents.markovianStates.size() + INITIAL_BITVECTOR_SIZE); } - modelComponents.markovianStates.set(id, markovian); - } - - template - void ExplicitDFTModelBuilderApprox::setRemapping(StateType id, StateType mappedId) { - STORM_LOG_ASSERT(id < stateRemapping.size(), "Invalid index for remapping."); - stateRemapping[id] = mappedId; + modelComponents.markovianStates.set(matrixBuilder.getCurrentRowGroup() - 1, markovian); } diff --git a/src/builder/ExplicitDFTModelBuilderApprox.h b/src/builder/ExplicitDFTModelBuilderApprox.h index fa529f221..3f8af519f 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.h +++ b/src/builder/ExplicitDFTModelBuilderApprox.h @@ -4,6 +4,7 @@ #include #include #include +#include "src/generator/DftNextStateGenerator.h" #include #include "src/storage/sparse/StateStorage.h" #include @@ -32,6 +33,7 @@ namespace storm { // A structure holding the individual components of a model. struct ModelComponents { + // Constructor ModelComponents(); // The transition matrix. @@ -53,6 +55,87 @@ namespace storm { bool deterministicModel; }; + // A class holding the information for building the transition matrix. + class MatrixBuilder { + public: + // Constructor + MatrixBuilder(bool canHaveNondeterminism); + + /*! + * Set a mapping from a state id to the index in the matrix. + * + * @param id Id of the state. + */ + void setRemapping(StateType id) { + STORM_LOG_ASSERT(id < stateRemapping.size(), "Invalid index for remapping."); + stateRemapping[id] = currentRowGroup; + } + + /*! + * Create a new row group if the model is nondeterministic. + */ + void newRowGroup() { + if (canHaveNondeterminism) { + builder.newRowGroup(currentRow); + } + ++currentRowGroup; + } + + /*! + * Add a transition from the current row. + * + * @param index Target index + * @param value Value of transition + */ + void addTransition(StateType index, ValueType value) { + builder.addNextValue(currentRow, index, value); + } + + /*! + * Finish the current row. + */ + void finishRow() { + ++currentRow; + } + + /*! + * Remap the columns in the matrix. + */ + void remap() { + builder.replaceColumns(stateRemapping, mappingOffset); + } + + /*! + * Get the current row group. + * + * @return The current row group. + */ + StateType getCurrentRowGroup() { + return currentRowGroup; + } + + // Flag indicating if row groups are needed. + bool canHaveNondeterminism; + + // Matrix builder. + storm::storage::SparseMatrixBuilder builder; + + // Offset to distinguish states which will not be remapped anymore and those which will. + size_t mappingOffset; + + // A mapping from state ids to the row group indices in which they actually reside. + // TODO Matthias: avoid hack with fixed int type + std::vector stateRemapping; + + private: + + // Index of the current row group. + StateType currentRowGroup; + + // Index of the current row. + StateType currentRow; + }; + public: // A structure holding the labeling options. struct LabelOptions { @@ -74,9 +157,10 @@ namespace storm { * Build model from DFT. * * @param labelOpts Options for labeling. + * @param firstTime Flag indicating if the model is built for the first time or rebuilt. * @param approximationError Error allowed for approximation. */ - void buildModel(LabelOptions const& labelOpts, double approximationError = 0.0); + void buildModel(LabelOptions const& labelOpts, bool firstTime, double approximationError = 0.0); /*! * Get the built model. @@ -96,6 +180,23 @@ namespace storm { private: + /*! + * Explore state space of DFT. + */ + void exploreStateSpace(); + + /*! + * Initialize the matrix for a refinement iteration. + */ + void initializeNextIteration(); + + /*! + * Build the labeling. + * + * @param labelOpts Options for labeling. + */ + void buildLabeling(LabelOptions const& labelOpts); + /*! * Add a state to the explored states (if not already there). It also handles pseudo states. * @@ -106,20 +207,11 @@ namespace storm { StateType getOrAddStateIndex(DFTStatePointer const& state); /*! - * Set if the given state is markovian. + * Set markovian flag for the current state. * - * @param id Id of the state. * @param markovian Flag indicating if the state is markovian. */ - void setMarkovian(StateType id, bool markovian); - - /*! - * Set a mapping from a state id to its new id. - * - * @param id Id of the state. - * @param mappedId New id to use. - */ - void setRemapping(StateType id, StateType mappedId); + void setMarkovian(bool markovian); /** * Change matrix to reflect the lower approximation bound. @@ -158,40 +250,43 @@ namespace storm { // TODO Matthias: use const reference std::shared_ptr stateGenerationInfo; - // Current id for new state - size_t newIndex = 0; - - // Mapping from pseudo states to (id of concrete state, bitvector) - std::vector> mPseudoStatesMapping; + // Flag indication if dont care propagation should be used. + bool enableDC = true; //TODO Matthias: make changeable const bool mergeFailedStates = true; + // Current id for new state + size_t newIndex = 0; + // Id of failed state size_t failedStateId = 0; // Id of initial state size_t initialStateIndex = 0; - // Flag indication if dont care propagation should be used. - bool enableDC = true; + // Mapping from pseudo states to (id of concrete state, bitvector representation) + std::vector> mPseudoStatesMapping; + + // Next state generator for exploring the state space + storm::generator::DftNextStateGenerator generator; // Structure for the components of the model. ModelComponents modelComponents; + // Structure for the transition matrix builder. + MatrixBuilder matrixBuilder; + // Internal information about the states that were explored. storm::storage::sparse::StateStorage stateStorage; // A set of states that still need to be explored. std::deque statesToExplore; - // A mapping from state indices to the row groups in which they actually reside - // TODO Matthias: avoid hack with fixed int type - std::vector stateRemapping; - - // Holds all skipped states which were not yet expanded. More concrete it is a mapping from matrix indices - // to the corresponding skipped state. - std::unordered_map skippedStates; + // Holds all skipped states which were not yet expanded. More concretely it is a mapping from matrix indices + // to the corresponding skipped states. + // Notice that we need an ordered map here to easily iterate in increasing order over state ids. + std::map skippedStates; }; } } diff --git a/src/generator/DftNextStateGenerator.cpp b/src/generator/DftNextStateGenerator.cpp index f468c673e..119ff9342 100644 --- a/src/generator/DftNextStateGenerator.cpp +++ b/src/generator/DftNextStateGenerator.cpp @@ -176,7 +176,7 @@ namespace storm { if (approximationError > 0.0) { if (checkSkipState(newState, rate, choice.getTotalMass(), approximationError)) { STORM_LOG_TRACE("Will skip state " << newStateId); - newState->markSkip(); + newState->setSkip(true); } } } diff --git a/src/generator/DftNextStateGenerator.h b/src/generator/DftNextStateGenerator.h index 7c9e1bb48..6fa815e44 100644 --- a/src/generator/DftNextStateGenerator.h +++ b/src/generator/DftNextStateGenerator.h @@ -70,7 +70,7 @@ namespace storm { StateType mergeFailedStateId = 0; // Flag indicating if the model is deterministic. - bool deterministicModel = true; + bool deterministicModel = false; // Allowed approximation error. double approximationError = 0.0; diff --git a/src/modelchecker/dft/DFTModelChecker.cpp b/src/modelchecker/dft/DFTModelChecker.cpp index 1c0772bf8..7ac2f1a8a 100644 --- a/src/modelchecker/dft/DFTModelChecker.cpp +++ b/src/modelchecker/dft/DFTModelChecker.cpp @@ -158,26 +158,17 @@ namespace storm { size_t iteration = 0; do { // Iteratively build finer models - // TODO Matthias: implement refinement - STORM_LOG_ASSERT(iteration < 1, "Iterative refinement not yet implemented."); explorationStart = std::chrono::high_resolution_clock::now(); STORM_LOG_INFO("Building model..."); // TODO Matthias refine model using existing model and MC results currentApproximationError = pow(0.1, iteration) * approximationError; - builder.buildModel(labeloptions, currentApproximationError); + builder.buildModel(labeloptions, iteration < 1, currentApproximationError); + // TODO Matthias: possible to do bisimulation on approximated model and not on concrete one? // Build model for lower bound STORM_LOG_INFO("Getting model for lower bound..."); model = builder.getModelApproximation(true); - //model->printModelInformationToStream(std::cout); - STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates()); - STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions()); - if (model->getNumberOfStates() <= 15) { - STORM_LOG_TRACE("Transition matrix: " << std::endl << model->getTransitionMatrix()); - } else { - STORM_LOG_TRACE("Transition matrix: too big to print"); - } explorationTime += std::chrono::high_resolution_clock::now() - explorationStart; // Check lower bound std::unique_ptr result = checkModel(model, formula); @@ -188,14 +179,6 @@ namespace storm { STORM_LOG_INFO("Getting model for upper bound..."); explorationStart = std::chrono::high_resolution_clock::now(); model = builder.getModelApproximation(false); - //model->printModelInformationToStream(std::cout); - STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates()); - STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions()); - if (model->getNumberOfStates() <= 15) { - STORM_LOG_TRACE("Transition matrix: " << std::endl << model->getTransitionMatrix()); - } else { - STORM_LOG_TRACE("Transition matrix: too big to print"); - } explorationTime += std::chrono::high_resolution_clock::now() - explorationStart; // Check upper bound result = checkModel(model, formula); @@ -203,7 +186,7 @@ namespace storm { approxResult.second = result->asExplicitQuantitativeCheckResult().getValueMap().begin()->second; ++iteration; - STORM_LOG_TRACE("Result after iteration " << iteration << ": (" << approxResult.first << ", " << approxResult.second << ")"); + STORM_LOG_INFO("Result after iteration " << iteration << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")"); } while (!isApproximationSufficient(approxResult.first, approxResult.second, approximationError)); STORM_LOG_INFO("Finished approximation after " << iteration << " iteration" << (iteration > 1 ? "s." : ".")); @@ -216,7 +199,7 @@ namespace storm { if (approximationError >= 0.0) { storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions; // TODO initialize this with the formula - builder.buildModel(labeloptions); + builder.buildModel(labeloptions, true); model = builder.getModel(); } else { storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, enableDC); diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index 5558e63ae..c87008c9c 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -97,8 +97,8 @@ namespace storm { return !mValid; } - void markSkip() { - mSkip = true; + void setSkip(bool skip) { + mSkip = skip; } bool isSkip() const {