diff --git a/CHANGELOG.md b/CHANGELOG.md index 9fafa9849..4005ca0e1 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -18,6 +18,7 @@ Version 1.1.x - storm-pars: support for welldefinedness constraints in mdps. - symbolic (MT/BDD) bisimulation - Fixed issue related to variable names that can not be used in Exprtk. +- DRN parser improved ### Version 1.1.0 (2017/8) diff --git a/resources/3rdparty/sylvan/src/lace.c b/resources/3rdparty/sylvan/src/lace.c index 08e9f8843..64443e23b 100755 --- a/resources/3rdparty/sylvan/src/lace.c +++ b/resources/3rdparty/sylvan/src/lace.c @@ -1088,6 +1088,12 @@ void lace_exit() lace_resume(); lace_barrier(); + // Free the memory of the workers. + for (unsigned int i=0; i #include @@ -45,18 +34,18 @@ */ template void analyzeDFT(std::vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) { - storm::settings::modules::DFTSettings const& dftSettings = storm::settings::getModule(); + storm::settings::modules::DftIOSettings const& dftIOSettings = storm::settings::getModule(); std::shared_ptr> dft; // Build DFT from given file. - if (dftSettings.isDftJsonFileSet()) { + if (dftIOSettings.isDftJsonFileSet()) { storm::parser::DFTJsonParser parser; - std::cout << "Loading DFT from file " << dftSettings.getDftJsonFilename() << std::endl; - dft = std::make_shared>(parser.parseJson(dftSettings.getDftJsonFilename())); + std::cout << "Loading DFT from file " << dftIOSettings.getDftJsonFilename() << std::endl; + dft = std::make_shared>(parser.parseJson(dftIOSettings.getDftJsonFilename())); } else { storm::parser::DFTGalileoParser parser; - std::cout << "Loading DFT from file " << dftSettings.getDftFilename() << std::endl; - dft = std::make_shared>(parser.parseDFT(dftSettings.getDftFilename())); + std::cout << "Loading DFT from file " << dftIOSettings.getDftFilename() << std::endl; + dft = std::make_shared>(parser.parseDFT(dftIOSettings.getDftFilename())); } // Build properties @@ -92,83 +81,39 @@ void analyzeWithSMT(std::string filename) { //std::cout << "SMT result: " << sat << std::endl; } +void processOptions() { + // Start by setting some urgent options (log levels, resources, etc.) + storm::cli::setUrgentOptions(); -/*! - * Initialize the settings manager. - */ -void initializeSettings() { - storm::settings::mutableManager().setName("Storm-DyFTeE", "storm-dft"); - - // Register all known settings modules. - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - //storm::settings::addModule(); - //storm::settings::addModule(); - //storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - //storm::settings::addModule(); - //storm::settings::addModule(); - //storm::settings::addModule(); - //storm::settings::addModule(); - //storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - - // For translation into JANI via GSPN. - storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); -} - -/*! - * Entry point for the DyFTeE backend. - * - * @param argc The argc argument of main(). - * @param argv The argv argument of main(). - * @return Return code, 0 if successfull, not 0 otherwise. - */ -int main(const int argc, const char** argv) { - try { - storm::utility::setUp(); - storm::cli::printHeader("Storm-DyFTeE", argc, argv); - initializeSettings(); + storm::cli::processOptions(); - bool optionsCorrect = storm::cli::parseOptions(argc, argv); - if (!optionsCorrect) { - return -1; - } - - storm::settings::modules::DFTSettings const& dftSettings = storm::settings::getModule(); + storm::settings::modules::DftIOSettings const& dftIOSettings = storm::settings::getModule(); + storm::settings::modules::FaultTreeSettings const& faultTreeSettings = storm::settings::getModule(); storm::settings::modules::GeneralSettings const& generalSettings = storm::settings::getModule(); storm::settings::modules::IOSettings const& ioSettings = storm::settings::getModule(); - if (!dftSettings.isDftFileSet() && !dftSettings.isDftJsonFileSet()) { + if (!dftIOSettings.isDftFileSet() && !dftIOSettings.isDftJsonFileSet()) { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); } - if (dftSettings.isExportToJson()) { - STORM_LOG_THROW(dftSettings.isDftFileSet(), storm::exceptions::InvalidSettingsException, "No input model in Galileo format given."); + if (dftIOSettings.isExportToJson()) { + STORM_LOG_THROW(dftIOSettings.isDftFileSet(), storm::exceptions::InvalidSettingsException, "No input model in Galileo format given."); storm::parser::DFTGalileoParser parser; - storm::storage::DFT dft = parser.parseDFT(dftSettings.getDftFilename()); + storm::storage::DFT dft = parser.parseDFT(dftIOSettings.getDftFilename()); // Export to json - storm::storage::DftJsonExporter::toFile(dft, dftSettings.getExportJsonFilename()); + storm::storage::DftJsonExporter::toFile(dft, dftIOSettings.getExportJsonFilename()); storm::utility::cleanUp(); - return 0; + return; } - if (dftSettings.isTransformToGspn()) { + if (dftIOSettings.isTransformToGspn()) { std::shared_ptr> dft; - if (dftSettings.isDftJsonFileSet()) { + if (dftIOSettings.isDftJsonFileSet()) { storm::parser::DFTJsonParser parser; - dft = std::make_shared>(parser.parseJson(dftSettings.getDftJsonFilename())); + dft = std::make_shared>(parser.parseJson(dftIOSettings.getDftJsonFilename())); } else { storm::parser::DFTGalileoParser parser(true, false); - dft = std::make_shared>(parser.parseDFT(dftSettings.getDftFilename())); + dft = std::make_shared>(parser.parseDFT(dftIOSettings.getDftFilename())); } storm::transformations::dft::DftToGspnTransformator gspnTransformator(*dft); gspnTransformator.transform(); @@ -199,7 +144,7 @@ int main(const int argc, const char** argv) { delete model; delete gspn; storm::utility::cleanUp(); - return 0; + return; } bool parametric = false; @@ -208,22 +153,22 @@ int main(const int argc, const char** argv) { #endif #ifdef STORM_HAVE_Z3 - if (dftSettings.solveWithSMT()) { + if (faultTreeSettings.solveWithSMT()) { // Solve with SMT if (parametric) { // analyzeWithSMT(dftSettings.getDftFilename()); } else { - analyzeWithSMT(dftSettings.getDftFilename()); + analyzeWithSMT(dftIOSettings.getDftFilename()); } storm::utility::cleanUp(); - return 0; + return; } #endif // Set min or max std::string optimizationDirection = "min"; - if (dftSettings.isComputeMaximalValue()) { - STORM_LOG_THROW(!dftSettings.isComputeMinimalValue(), storm::exceptions::InvalidSettingsException, "Cannot compute minimal and maximal values at the same time."); + if (dftIOSettings.isComputeMaximalValue()) { + STORM_LOG_THROW(!dftIOSettings.isComputeMinimalValue(), storm::exceptions::InvalidSettingsException, "Cannot compute minimal and maximal values at the same time."); optimizationDirection = "max"; } @@ -233,19 +178,19 @@ int main(const int argc, const char** argv) { if (ioSettings.isPropertySet()) { properties.push_back(ioSettings.getProperty()); } - if (dftSettings.usePropExpectedTime()) { + if (dftIOSettings.usePropExpectedTime()) { properties.push_back("T" + optimizationDirection + "=? [F \"failed\"]"); } - if (dftSettings.usePropProbability()) { + if (dftIOSettings.usePropProbability()) { properties.push_back("P" + optimizationDirection + "=? [F \"failed\"]"); } - if (dftSettings.usePropTimebound()) { + if (dftIOSettings.usePropTimebound()) { std::stringstream stream; - stream << "P" << optimizationDirection << "=? [F<=" << dftSettings.getPropTimebound() << " \"failed\"]"; + stream << "P" << optimizationDirection << "=? [F<=" << dftIOSettings.getPropTimebound() << " \"failed\"]"; properties.push_back(stream.str()); } - if (dftSettings.usePropTimepoints()) { - for (double timepoint : dftSettings.getPropTimepoints()) { + if (dftIOSettings.usePropTimepoints()) { + for (double timepoint : dftIOSettings.getPropTimepoints()) { std::stringstream stream; stream << "P" << optimizationDirection << "=? [F<=" << timepoint << " \"failed\"]"; properties.push_back(stream.str()); @@ -258,21 +203,51 @@ int main(const int argc, const char** argv) { // Set possible approximation error double approximationError = 0.0; - if (dftSettings.isApproximationErrorSet()) { - approximationError = dftSettings.getApproximationError(); + if (faultTreeSettings.isApproximationErrorSet()) { + approximationError = faultTreeSettings.getApproximationError(); } // From this point on we are ready to carry out the actual computations. if (parametric) { #ifdef STORM_HAVE_CARL - analyzeDFT(properties, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError); + analyzeDFT(properties, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), approximationError); #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameters are not supported in this build."); #endif } else { - analyzeDFT(properties, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError); + analyzeDFT(properties, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), approximationError); } - +} + +/*! + * Entry point for the DyFTeE backend. + * + * @param argc The argc argument of main(). + * @param argv The argv argument of main(). + * @return Return code, 0 if successfull, not 0 otherwise. + */ +/*! + * Main entry point of the executable storm-pars. + */ +int main(const int argc, const char** argv) { + try { + storm::utility::setUp(); + storm::cli::printHeader("Storm-dft", argc, argv); + storm::settings::initializeDftSettings("Storm-dft", "storm-dft"); + + storm::utility::Stopwatch totalTimer(true); + if (!storm::cli::parseOptions(argc, argv)) { + return -1; + } + + processOptions(); + //storm::pars::processOptions(); + + totalTimer.stop(); + if (storm::settings::getModule().isPrintTimeAndMemorySet()) { + storm::cli::printTimeAndMemoryStatistics(totalTimer.getTimeInMilliseconds()); + } + // All operations have now been performed, so we clean up everything and terminate. storm::utility::cleanUp(); return 0; diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index 4a29b0652..2b74432ad 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -6,456 +6,824 @@ #include "storm/models/sparse/Ctmc.h" #include "storm/utility/constants.h" #include "storm/utility/vector.h" +#include "storm/utility/bitoperations.h" #include "storm/exceptions/UnexpectedException.h" #include "storm/settings/SettingsManager.h" - -#include "storm-dft/settings/modules/DFTSettings.h" +#include "storm/logic/AtomicLabelFormula.h" +#include "storm-dft/settings/modules/FaultTreeSettings.h" namespace storm { namespace builder { - template - ExplicitDFTModelBuilder::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), markovianStates(), exitRates(), choiceLabeling() { + template + ExplicitDFTModelBuilder::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), markovianStates(), exitRates(), choiceLabeling() { // Intentionally left empty. } - - template - ExplicitDFTModelBuilder::ExplicitDFTModelBuilder(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) : mDft(dft), mStates(((mDft.stateVectorSize() / 64) + 1) * 64, INITIAL_BUCKETSIZE), enableDC(enableDC) { - // stateVectorSize is bound for size of bitvector - mStateGenerationInfo = std::make_shared(mDft.buildStateGenerationInfo(symmetries)); + template + ExplicitDFTModelBuilder::MatrixBuilder::MatrixBuilder(bool canHaveNondeterminism) : mappingOffset(0), stateRemapping(), currentRowGroup(0), currentRow(0), canHaveNondeterminism((canHaveNondeterminism)) { + // Create matrix builder + builder = storm::storage::SparseMatrixBuilder(0, 0, 0, false, canHaveNondeterminism, 0); } + template + ExplicitDFTModelBuilder::LabelOptions::LabelOptions(std::vector> properties, bool buildAllLabels) : buildFailLabel(true), buildFailSafeLabel(false), buildAllLabels(buildAllLabels) { + // Get necessary labels from properties + std::vector> atomicLabels; + for (auto property : properties) { + property->gatherAtomicLabelFormulas(atomicLabels); + } + // Set usage of necessary labels + for (auto atomic : atomicLabels) { + std::string label = atomic->getLabel(); + std::size_t foundIndex = label.find("_fail"); + if (foundIndex != std::string::npos) { + elementLabels.insert(label.substr(0, foundIndex)); + } else if (label.compare("failed") == 0) { + buildFailLabel = true; + } else if (label.compare("failsafe") == 0) { + buildFailSafeLabel = true; + } else { + STORM_LOG_WARN("Label '" << label << "' not known."); + } + } + } + + template + ExplicitDFTModelBuilder::ExplicitDFTModelBuilder(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) : + dft(dft), + stateGenerationInfo(std::make_shared(dft.buildStateGenerationInfo(symmetries))), + enableDC(enableDC), + usedHeuristic(storm::settings::getModule().getApproximationHeuristic()), + generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates), + matrixBuilder(!generator.isDeterministicModel()), + stateStorage(((dft.stateVectorSize() / 64) + 1) * 64), + // TODO Matthias: make choosable + //explorationQueue(dft.nrElements()+1, 0, 1) + explorationQueue(200, 0, 0.9) + { + // Intentionally left empty. + // TODO Matthias: remove again + usedHeuristic = storm::builder::ApproximationHeuristic::DEPTH; + + // 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 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 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 subtree; + for (size_t id = 0; id < dft.nrElements(); ++id) { + if (dft.isBasicElement(id)) { + subtree.push_back(id); + } + } + subtreeBEs.push_back(subtree); + } - template - std::shared_ptr> ExplicitDFTModelBuilder::buildModel(LabelOptions const& labelOpts) { - // Initialize - bool deterministicModel = false; - size_t rowOffset = 0; - ModelComponents modelComponents; - std::vector tmpMarkovianStates; - storm::storage::SparseMatrixBuilder 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()); - STORM_LOG_TRACE("Introduce fail state with id: " << failedIndex); - modelComponents.exitRates.push_back(storm::utility::one()); - tmpMarkovianStates.push_back(failedIndex); - } - - // Explore state space - DFTStatePointer state = std::make_shared>(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(mStates.contains(pseudoStatePair.second), "Pseudo state not contained."); - STORM_LOG_ASSERT(mStates.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>(pseudoStatePair.second, mDft, *mStateGenerationInfo, newIndex); - pseudoState->construct(); - 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."); + for (auto tree : subtreeBEs) { + std::stringstream stream; + stream << "Subtree: "; + for (size_t id : tree) { + stream << id << ", "; } + STORM_LOG_TRACE(stream.str()); } - - // Replace pseudo states in matrix - 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); - - STORM_LOG_DEBUG("Generated " << mStates.size() + (mergeFailedStates ? 1 : 0) << " states"); - STORM_LOG_DEBUG("Model is " << (deterministic ? "deterministic" : "non-deterministic")); - - size_t stateSize = mStates.size() + (mergeFailedStates ? 1 : 0); - // Build Markov Automaton - modelComponents.markovianStates = storm::storage::BitVector(stateSize, tmpMarkovianStates); + } + + template + void ExplicitDFTModelBuilder::buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold) { + STORM_LOG_TRACE("Generating DFT state space"); + + if (iteration < 1) { + // 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++; + matrixBuilder.stateRemapping.push_back(0); + return this->failedStateId; + } ); + + 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(&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); + // Initialize heuristic values for inital state + STORM_LOG_ASSERT(!statesNotExplored.at(initialStateIndex).second, "Heuristic for initial state is already initialized"); + ExplorationHeuristicPointer heuristic = std::make_shared(initialStateIndex); + heuristic->markExpand(); + statesNotExplored[initialStateIndex].second = heuristic; + explorationQueue.push(heuristic); + } else { + initializeNextIteration(); + } + + if (approximationThreshold > 0) { + switch (usedHeuristic) { + case storm::builder::ApproximationHeuristic::NONE: + // Do not change anything + approximationThreshold = dft.nrElements()+10; + break; + case storm::builder::ApproximationHeuristic::DEPTH: + approximationThreshold = iteration + 1; + break; + case storm::builder::ApproximationHeuristic::PROBABILITY: + case storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE: + approximationThreshold = 10 * std::pow(2, iteration); + break; + } + } + exploreStateSpace(approximationThreshold); + + size_t stateSize = stateStorage.getNumberOfStates() + (mergeFailedStates ? 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 Matthias: 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 = transitionMatrixBuilder.build(stateSize, stateSize); + 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_TRACE("Exit rates: " << storm::utility::vector::toString(modelComponents.exitRates)); - STORM_LOG_TRACE("Markovian states: " << modelComponents.markovianStates); - + + buildLabeling(labelOpts); + } + + template + void ExplicitDFTModelBuilder::initializeNextIteration() { + STORM_LOG_TRACE("Refining DFT state space"); + + // TODO Matthias: should be easier now as skipped states all are at the end of the matrix + // Push skipped states to explore queue + // TODO Matthias: remove + for (auto const& skippedState : skippedStates) { + statesNotExplored[skippedState.second.first->getId()] = skippedState.second; + explorationQueue.push(skippedState.second.second); + } + + // 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 != 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> 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 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.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 + void ExplicitDFTModelBuilder::exploreStateSpace(double approximationThreshold) { + size_t nrExpandedStates = 0; + size_t nrSkippedStates = 0; + // TODO Matthias: do not empty queue every time but break before + while (!explorationQueue.empty()) { + // Get the first state in the queue + ExplorationHeuristicPointer currentExplorationHeuristic = explorationQueue.popTop(); + 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 Matthias: what to do when there is no unique target state? + matrixBuilder.addTransition(failedStateId, storm::utility::zero()); + // Remember skipped state + skippedStates[matrixBuilder.getCurrentRowGroup() - 1] = std::make_pair(currentState, currentExplorationHeuristic); + matrixBuilder.finishRow(); + } else { + // Explore the current state + ++nrExpandedStates; + storm::generator::StateBehavior 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 = std::make_shared(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass()); + iter->second.second = heuristic; + if (state->hasFailed(dft.getTopLevelIndex()) || state->isFailsafe(dft.getTopLevelIndex()) || state->nrFailableDependencies() > 0 || (state->nrFailableDependencies() == 0 && state->nrFailableBEs() == 0)) { + // 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 Mathias: 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(); + } + } + } // 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 + void ExplicitDFTModelBuilder::buildLabeling(LabelOptions const& labelOpts) { // Build state labeling - modelComponents.stateLabeling = storm::models::sparse::StateLabeling(mStates.size() + (mergeFailedStates ? 1 : 0)); - // Initial state is always first state without any failure + 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); // 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>> basicElements = mDft.getBasicElements(); - for (std::shared_ptr> elem : basicElements) { - if(labelOpts.beLabels.count(elem->name()) > 0) { - modelComponents.stateLabeling.addLabel(elem->name() + "_fail"); + + // Collect labels for all necessary elements + for (size_t id = 0; id < dft.nrElements(); ++id) { + std::shared_ptr const> element = dft.getElement(id); + if (labelOpts.buildAllLabels || labelOpts.elementLabels.count(element->name()) > 0) { + modelComponents.stateLabeling.addLabel(element->name() + "_fail"); } } - if(mergeFailedStates) { - modelComponents.stateLabeling.addLabelToState("failed", failedIndex); + // Set labels to states + if (mergeFailedStates) { + modelComponents.stateLabeling.addLabelToState("failed", failedStateId); } - for (auto const& stateIdPair : mStates) { + 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)) { + size_t stateId = matrixBuilder.getRemapping(stateIdPair.second); + if (!mergeFailedStates && labelOpts.buildFailLabel && dft.hasFailed(state, *stateGenerationInfo)) { modelComponents.stateLabeling.addLabelToState("failed", stateId); } - if (labelOpts.buildFailSafeLabel && mDft.isFailsafe(state, *mStateGenerationInfo)) { + if (labelOpts.buildFailSafeLabel && dft.isFailsafe(state, *stateGenerationInfo)) { modelComponents.stateLabeling.addLabelToState("failsafe", stateId); - }; - // Set fail status for each BE - for (std::shared_ptr> elem : basicElements) { - if (labelOpts.beLabels.count(elem->name()) > 0 && storm::storage::DFTState::hasFailed(state, mStateGenerationInfo->getStateIndex(elem->id())) ) { - modelComponents.stateLabeling.addLabelToState(elem->name() + "_fail", stateId); + } + // Set fail status for each necessary element + for (size_t id = 0; id < dft.nrElements(); ++id) { + std::shared_ptr const> element = dft.getElement(id); + if ((labelOpts.buildAllLabels || labelOpts.elementLabels.count(element->name()) > 0) && storm::storage::DFTState::hasFailed(state, stateGenerationInfo->getStateIndex(element->id()))) { + modelComponents.stateLabeling.addLabelToState(element->name() + "_fail", stateId); + } + } + } + + STORM_LOG_TRACE(modelComponents.stateLabeling); + } + + template + std::shared_ptr> ExplicitDFTModelBuilder::getModel() { + STORM_LOG_ASSERT(skippedStates.size() == 0, "Concrete model has skipped states"); + return createModel(false); + } + + template + std::shared_ptr> ExplicitDFTModelBuilder::getModelApproximation(bool lowerBound, bool expectedTime) { + if (expectedTime) { + // TODO Matthias: handle case with no skipped states + changeMatrixBound(modelComponents.transitionMatrix, lowerBound); + return createModel(true); + } else { + // Change model for probabilities + // TODO Matthias: make nicer + storm::storage::SparseMatrix 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() == failedStateId, "Transition has wrong target state."); + STORM_LOG_ASSERT(!it->second.first->isPseudoState(), "State is still pseudo state."); + matrixEntry->setValue(storm::utility::one()); + 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> model; + if (modelComponents.deterministicModel) { + model = std::make_shared>(std::move(matrix), std::move(labeling)); + } else { + // Build MA + // Compute exit rates + // TODO Matthias: avoid computing multiple times + modelComponents.exitRates = std::vector(modelComponents.markovianStates.size()); + std::vector::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(); + } + } + STORM_LOG_TRACE("Exit rates: " << modelComponents.exitRates); + + storm::storage::sparse::ModelComponents maComponents(std::move(matrix), std::move(labeling)); + maComponents.rateTransitions = true; + maComponents.markovianStates = modelComponents.markovianStates; + maComponents.exitRates = modelComponents.exitRates; + std::shared_ptr> ma = std::make_shared>(std::move(maComponents)); + if (ma->hasOnlyTrivialNondeterminism()) { + // Markov automaton can be converted into CTMC + // TODO Matthias: 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 + std::shared_ptr> ExplicitDFTModelBuilder::createModel(bool copy) { std::shared_ptr> model; - storm::storage::sparse::ModelComponents components(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling)); - components.exitRates = std::move(modelComponents.exitRates); - if (deterministic) { - components.transitionMatrix.makeRowGroupingTrivial(); - model = std::make_shared>(std::move(components)); + + if (modelComponents.deterministicModel) { + // Build CTMC + if (copy) { + model = std::make_shared>(modelComponents.transitionMatrix, modelComponents.stateLabeling); + } else { + model = std::make_shared>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling)); + } } else { - components.markovianStates = std::move(modelComponents.markovianStates); - std::shared_ptr> ma = std::make_shared>(std::move(components)); + // Build MA + // Compute exit rates + // TODO Matthias: avoid computing multiple times + modelComponents.exitRates = std::vector(modelComponents.markovianStates.size()); + std::vector::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(); + } + } + STORM_LOG_TRACE("Exit rates: " << modelComponents.exitRates); + + std::shared_ptr> ma; + if (copy) { + storm::storage::sparse::ModelComponents maComponents(modelComponents.transitionMatrix, modelComponents.stateLabeling); + maComponents.rateTransitions = true; + maComponents.markovianStates = modelComponents.markovianStates; + maComponents.exitRates = modelComponents.exitRates; + ma = std::make_shared>(std::move(maComponents)); + } else { + storm::storage::sparse::ModelComponents 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>(std::move(maComponents)); + } if (ma->hasOnlyTrivialNondeterminism()) { // Markov automaton can be converted into CTMC + // TODO Matthias: 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 - std::pair ExplicitDFTModelBuilder::exploreStates(DFTStatePointer const& state, size_t& rowOffset, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector& markovianStates, std::vector& 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 outgoingRates; - std::vector> outgoingProbabilities; - bool hasDependencies = state->nrFailableDependencies() > 0; - size_t failableCount = hasDependencies ? state->nrFailableDependencies() : state->nrFailableBEs(); - size_t smallest = 0; - ValueType exitRate = storm::utility::zero(); - 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()); - STORM_LOG_TRACE("Added self loop for " << stateId); - exitRates.push_back(storm::utility::one()); - 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>(*state); - std::pair const>, bool> nextBEPair = newState->letNextBEFail(smallest++); - std::shared_ptr 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)); - - // Propagate failures - storm::storage::DFTStateSpaceGenerationQueues 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); + template + void ExplicitDFTModelBuilder::changeMatrixBound(storm::storage::SparseMatrix & 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() == failedStateId, "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::isZero(heuristic->getUpperBound())) { + // Initialize bounds + ValueType lowerBound = getLowerBound(it->second.first); + ValueType upperBound = getUpperBound(it->second.first); + heuristic->setBounds(lowerBound, upperBound); } - 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; + // Change bound + if (lowerBound) { + matrixEntry->setValue(it->second.second->getLowerBound()); } else { - // Explore new state recursively - auto explorePair = exploreStates(newState, rowOffset, transitionMatrixBuilder, markovianStates, exitRates); - newStateId = explorePair.first; - deterministic &= explorePair.second; + matrixEntry->setValue(it->second.second->getUpperBound()); } + } + } - // Set transitions - if (hasDependencies) { - // Failure is due to dependency -> add non-deterministic choice - std::map choiceProbabilities; - std::shared_ptr 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>(*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() - 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())); + template + ValueType ExplicitDFTModelBuilder::getLowerBound(DFTStatePointer const& state) const { + // Get the lower bound by considering the failure of all possible BEs + ValueType lowerBound = storm::utility::zero(); + for (size_t index = 0; index < state->nrFailableBEs(); ++index) { + lowerBound += state->getFailableBERate(index); + } + return lowerBound; + } + + template + ValueType ExplicitDFTModelBuilder::getUpperBound(DFTStatePointer const& state) const { + if (state->hasFailed(dft.getTopLevelIndex())) { + return storm::utility::zero(); + } + + // Get the upper bound by considering the failure of all BEs + ValueType upperBound = storm::utility::one(); + ValueType rateSum = storm::utility::zero(); + + // Compute for each independent subtree + for (std::vector const& subtree : subtreeBEs) { + // Get all possible rates + std::vector rates; + storm::storage::BitVector coldBEs(subtree.size(), false); + for (size_t i = 0; i < subtree.size(); ++i) { + size_t id = subtree[i]; + if (state->isOperational(id)) { + // Get BE rate + ValueType rate = state->getBERate(id); + if (storm::utility::isZero(rate)) { + // Get active failure rate for cold BE + rate = dft.getBasicElement(id)->activeFailureRate(); + if (storm::utility::isZero(rate)) { + // Ignore BE which cannot fail + continue; + } + // Mark BE as cold + coldBEs.set(i, true); + } + rates.push_back(rate); + rateSum += rate; } - 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); + } + + STORM_LOG_ASSERT(rates.size() > 0, "No rates failable"); + + // Sort rates + std::sort(rates.begin(), rates.end()); + std::vector rateCount(rates.size(), 0); + size_t lastIndex = 0; + for (size_t i = 0; i < rates.size(); ++i) { + if (rates[lastIndex] != rates[i]) { + lastIndex = i; } - exitRate += rate; + ++rateCount[lastIndex]; } - } // 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); + 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); } } - 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; + } + + 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 + ValueType ExplicitDFTModelBuilder::computeMTTFAnd(std::vector const& rates, size_t size) const { + ValueType result = storm::utility::zero(); + if (size == 0) { + return result; + } + + // TODO Matthias: 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(i)); + ValueType sum = storm::utility::zero(); + do { + ValueType permResult = storm::utility::zero(); + for(size_t j = 0; j < rates.size(); ++j) { + if(permutation & static_cast(1 << static_cast(j))) { + // WARNING: if the first bit is set, it also recognizes the 32nd bit as set + // TODO: fix + permResult += rates[j]; } - } else { - ++it; } + permutation = nextBitPermutation(permutation); + STORM_LOG_ASSERT(!storm::utility::isZero(permResult), "PermResult is 0"); + sum += storm::utility::one() / permResult; + } while(permutation < (static_cast(1) << rates.size()) && permutation != 0); + if (i % 2 == 0) { + result -= sum; + } else { + result += sum; } - - // 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); + }*/ + + // Compute result with permutations of size <= 3 + ValueType one = storm::utility::one(); + 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]); + } } - - 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); + + STORM_LOG_ASSERT(!storm::utility::isZero(result), "UpperBound is 0"); + return result; } - - template - std::pair ExplicitDFTModelBuilder::checkForExploration(DFTStatePointer const& state) { + + template + StateType ExplicitDFTModelBuilder::getOrAddStateIndex(DFTStatePointer const& state) { + StateType stateId; bool changed = false; - if (mStateGenerationInfo->hasSymmetries()) { + + if (stateGenerationInfo->hasSymmetries()) { // Order state by symmetry - STORM_LOG_TRACE("Check for symmetry: " << mDft.getStateString(state)); + STORM_LOG_TRACE("Check for symmetry: " << dft.getStateString(state)); changed = state->orderBySymmetry(); - STORM_LOG_TRACE("State " << (changed ? "changed to " : "did not change") << (changed ? mDft.getStateString(state) : "")); - } - - if (mStates.contains(state->status())) { - // State already exists - uint_fast64_t stateId = mStates.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())); - mStates.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); - } + STORM_LOG_TRACE("State " << (changed ? "changed to " : "did not change") << (changed ? dft.getStateString(state) : "")); } - } - template - uint_fast64_t ExplicitDFTModelBuilder::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 (mStates.contains(state->status())) { + if (stateStorage.stateToId.contains(state->status())) { // State already exists - stateId = mStates.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(); - mStates.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; + 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 Matthias: 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 = mStates.findOrAdd(state->status(), state->getId()); - STORM_LOG_TRACE("New state: " << mDft.getStateString(state)); - return stateId; + 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 + void ExplicitDFTModelBuilder::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 + void ExplicitDFTModelBuilder::printNotExplored() const { + std::cout << "states not explored:" << std::endl; + for (auto it : statesNotExplored) { + std::cout << it.first << " -> " << dft.getStateString(it.second.first) << std::endl; } } diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.h b/src/storm-dft/builder/ExplicitDFTModelBuilder.h index 2913a78fa..b96dea410 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.h +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.h @@ -1,40 +1,42 @@ -#pragma once +#pragma once #include #include #include #include - +#include #include "storm/models/sparse/StateLabeling.h" #include "storm/models/sparse/ChoiceLabeling.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/models/sparse/Model.h" #include "storm/storage/SparseMatrix.h" -#include "storm/storage/BitVectorHashMap.h" +#include "storm/storage/sparse/StateStorage.h" +#include "storm-dft/builder/DftExplorationHeuristic.h" +#include "storm-dft/generator/DftNextStateGenerator.h" #include "storm-dft/storage/dft/DFT.h" #include "storm-dft/storage/dft/SymmetricUnits.h" - - - - +#include "storm-dft/storage/BucketPriorityQueue.h" namespace storm { namespace builder { - template + /*! + * Build a Markov chain from DFT. + */ + template class ExplicitDFTModelBuilder { - using DFTElementPointer = std::shared_ptr>; - using DFTElementCPointer = std::shared_ptr const>; - using DFTGatePointer = std::shared_ptr>; using DFTStatePointer = std::shared_ptr>; - using DFTRestrictionPointer = std::shared_ptr>; + // TODO Matthias: make choosable + using ExplorationHeuristic = DFTExplorationHeuristicDepth; + using ExplorationHeuristicPointer = std::shared_ptr; // A structure holding the individual components of a model. struct ModelComponents { + // Constructor ModelComponents(); // The transition matrix. @@ -51,52 +53,310 @@ namespace storm { // A vector that stores a labeling for each choice. boost::optional choiceLabeling; + + // A flag indicating if the model is deterministic. + 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; + } + + /*! + * Get the remapped state for the given id. + * + * @param id State. + * + * @return Remapped index. + */ + StateType getRemapping(StateType id) { + STORM_LOG_ASSERT(id < stateRemapping.size(), "Invalid index for remapping."); + return stateRemapping[id]; + } + + // 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; + + // Flag indicating if row groups are needed. + bool canHaveNondeterminism; }; - - const size_t INITIAL_BUCKETSIZE = 20000; - const uint_fast64_t OFFSET_PSEUDO_STATE = UINT_FAST64_MAX / 2; - - storm::storage::DFT const& mDft; - std::shared_ptr mStateGenerationInfo; - storm::storage::BitVectorHashMap mStates; - std::vector> mPseudoStatesMapping; // vector of (id to concrete state, bitvector) - size_t newIndex = 0; - bool mergeFailedStates = false; - bool enableDC = true; - size_t failedIndex = 0; - size_t initialStateIndex = 0; public: + // A structure holding the labeling options. struct LabelOptions { - bool buildFailLabel = true; - bool buildFailSafeLabel = false; - std::set beLabels = {}; + // Constructor + LabelOptions(std::vector> properties, bool buildAllLabels = false); + + // Flag indicating if the general fail label should be included. + bool buildFailLabel; + + // Flag indicating if the general failsafe label should be included. + bool buildFailSafeLabel; + + // Flag indicating if all possible labels should be included. + bool buildAllLabels; + + // Set of element names whose fail label to include. + std::set elementLabels; }; - + + /*! + * Constructor. + * + * @param dft DFT. + * @param symmetries Symmetries in the dft. + * @param enableDC Flag indicating if dont care propagation should be used. + */ ExplicitDFTModelBuilder(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC); - std::shared_ptr> buildModel(LabelOptions const& labelOpts); + /*! + * Build model from DFT. + * + * @param labelOpts Options for labeling. + * @param iteration Current number of iteration. + * @param approximationThreshold Threshold determining when to skip exploring states. + */ + void buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold = 0.0); + + /*! + * Get the built model. + * + * @return The model built from the DFT. + */ + std::shared_ptr> getModel(); + + /*! + * Get the built approximation model for either the lower or upper bound. + * + * @param lowerBound If true, the lower bound model is returned, else the upper bound model + * @param expectedTime If true, the bounds for expected time are computed, else the bounds for probabilities. + * + * @return The model built from the DFT. + */ + std::shared_ptr> getModelApproximation(bool lowerBound, bool expectedTime); private: - std::pair exploreStates(DFTStatePointer const& state, size_t& rowOffset, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector& markovianStates, std::vector& exitRates); - + /*! - * Adds a state to the explored states and handles pseudo states. + * Explore state space of DFT. + * + * @param approximationThreshold Threshold to determine when to skip states. + */ + void exploreStateSpace(double approximationThreshold); + + /*! + * 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. * * @param state The state to add. - * @return Id of added state. + * + * @return Id of state. + */ + StateType getOrAddStateIndex(DFTStatePointer const& state); + + /*! + * Set markovian flag for the current state. + * + * @param markovian Flag indicating if the state is markovian. + */ + void setMarkovian(bool markovian); + + /** + * Change matrix to reflect the lower or upper approximation bound. + * + * @param matrix Matrix to change. The change are reflected here. + * @param lowerBound Flag indicating if the lower bound should be used. Otherwise the upper bound is used. */ - uint_fast64_t addState(DFTStatePointer const& state); - + void changeMatrixBound(storm::storage::SparseMatrix & matrix, bool lowerBound) const; + /*! - * Check if state needs an exploration and remember pseudo states for later creation. + * Get lower bound approximation for state. + * + * @param state The state. + * + * @return Lower bound approximation. + */ + ValueType getLowerBound(DFTStatePointer const& state) const; + + /*! + * Get upper bound approximation for state. + * + * @param state The state. + * + * @return Upper bound approximation. + */ + ValueType getUpperBound(DFTStatePointer const& state) const; + + /*! + * Compute the MTTF of an AND gate via a closed formula. + * The used formula is 1/( 1/a + 1/b + 1/c + ... - 1/(a+b) - 1/(a+c) - ... + 1/(a+b+c) + ... - ...) + * + * @param rates List of rates of children of AND. + * @param size Only indices < size are considered in the vector. + * @return MTTF. + */ + ValueType computeMTTFAnd(std::vector const& rates, size_t size) const; + + /*! + * Compares the priority of two states. + * + * @param idA Id of first state + * @param idB Id of second state * - * @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. + * @return True if the priority of the first state is greater then the priority of the second one. */ - std::pair checkForExploration(DFTStatePointer const& state); + bool isPriorityGreater(StateType idA, StateType idB) const; + void printNotExplored() const; + + /*! + * Create the model model from the model components. + * + * @param copy If true, all elements of the model component are copied (used for approximation). If false + * they are moved to reduce the memory overhead. + * + * @return The model built from the model components. + */ + std::shared_ptr> createModel(bool copy); + + // Initial size of the bitvector. + const size_t INITIAL_BITVECTOR_SIZE = 20000; + // Offset used for pseudo states. + const StateType OFFSET_PSEUDO_STATE = std::numeric_limits::max() / 2; + + // Dft + storm::storage::DFT const& dft; + + // General information for state generation + // TODO Matthias: use const reference + std::shared_ptr stateGenerationInfo; + + // Flag indication if dont care propagation should be used. + bool enableDC = true; + + //TODO Matthias: make changeable + const bool mergeFailedStates = true; + + // Heuristic used for approximation + storm::builder::ApproximationHeuristic usedHeuristic; + + // 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; + + // 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 priority queue of states that still need to be explored. + storm::storage::BucketPriorityQueue explorationQueue; + + // A mapping of not yet explored states from the id to the tuple (state object, heuristic values). + std::map> statesNotExplored; + + // 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. + // TODO remove again + std::map> skippedStates; + + // List of independent subtrees and the BEs contained in them. + std::vector> subtreeBEs; }; + } } diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp deleted file mode 100644 index 0c7d69628..000000000 --- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp +++ /dev/null @@ -1,841 +0,0 @@ -#include "ExplicitDFTModelBuilderApprox.h" - -#include - -#include "storm/models/sparse/MarkovAutomaton.h" -#include "storm/models/sparse/Ctmc.h" -#include "storm/utility/constants.h" -#include "storm/utility/vector.h" -#include "storm/utility/bitoperations.h" -#include "storm/exceptions/UnexpectedException.h" -#include "storm/settings/SettingsManager.h" -#include "storm/logic/AtomicLabelFormula.h" -#include "storm-dft/settings/modules/DFTSettings.h" - - -namespace storm { - namespace builder { - - template - ExplicitDFTModelBuilderApprox::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), markovianStates(), exitRates(), choiceLabeling() { - // Intentionally left empty. - } - - template - ExplicitDFTModelBuilderApprox::MatrixBuilder::MatrixBuilder(bool canHaveNondeterminism) : mappingOffset(0), stateRemapping(), currentRowGroup(0), currentRow(0), canHaveNondeterminism((canHaveNondeterminism)) { - // Create matrix builder - builder = storm::storage::SparseMatrixBuilder(0, 0, 0, false, canHaveNondeterminism, 0); - } - - template - ExplicitDFTModelBuilderApprox::LabelOptions::LabelOptions(std::vector> properties, bool buildAllLabels) : buildFailLabel(true), buildFailSafeLabel(false), buildAllLabels(buildAllLabels) { - // Get necessary labels from properties - std::vector> atomicLabels; - for (auto property : properties) { - property->gatherAtomicLabelFormulas(atomicLabels); - } - // Set usage of necessary labels - for (auto atomic : atomicLabels) { - std::string label = atomic->getLabel(); - std::size_t foundIndex = label.find("_fail"); - if (foundIndex != std::string::npos) { - elementLabels.insert(label.substr(0, foundIndex)); - } else if (label.compare("failed") == 0) { - buildFailLabel = true; - } else if (label.compare("failsafe") == 0) { - buildFailSafeLabel = true; - } else { - STORM_LOG_WARN("Label '" << label << "' not known."); - } - } - } - - 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), - usedHeuristic(storm::settings::getModule().getApproximationHeuristic()), - generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates), - matrixBuilder(!generator.isDeterministicModel()), - stateStorage(((dft.stateVectorSize() / 64) + 1) * 64), - // TODO Matthias: make choosable - //explorationQueue(dft.nrElements()+1, 0, 1) - explorationQueue(200, 0, 0.9) - { - // Intentionally left empty. - // TODO Matthias: remove again - usedHeuristic = storm::builder::ApproximationHeuristic::DEPTH; - - // 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 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 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 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 - void ExplicitDFTModelBuilderApprox::buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold) { - STORM_LOG_TRACE("Generating DFT state space"); - - if (iteration < 1) { - // 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++; - matrixBuilder.stateRemapping.push_back(0); - return this->failedStateId; - } ); - - 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); - // Initialize heuristic values for inital state - STORM_LOG_ASSERT(!statesNotExplored.at(initialStateIndex).second, "Heuristic for initial state is already initialized"); - ExplorationHeuristicPointer heuristic = std::make_shared(initialStateIndex); - heuristic->markExpand(); - statesNotExplored[initialStateIndex].second = heuristic; - explorationQueue.push(heuristic); - } else { - initializeNextIteration(); - } - - if (approximationThreshold > 0) { - switch (usedHeuristic) { - case storm::builder::ApproximationHeuristic::NONE: - // Do not change anything - approximationThreshold = dft.nrElements()+10; - break; - case storm::builder::ApproximationHeuristic::DEPTH: - approximationThreshold = iteration + 1; - break; - case storm::builder::ApproximationHeuristic::PROBABILITY: - case storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE: - approximationThreshold = 10 * std::pow(2, iteration); - break; - } - } - exploreStateSpace(approximationThreshold); - - size_t stateSize = stateStorage.getNumberOfStates() + (mergeFailedStates ? 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 Matthias: 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(labelOpts); - } - - template - void ExplicitDFTModelBuilderApprox::initializeNextIteration() { - STORM_LOG_TRACE("Refining DFT state space"); - - // TODO Matthias: should be easier now as skipped states all are at the end of the matrix - // Push skipped states to explore queue - // TODO Matthias: remove - for (auto const& skippedState : skippedStates) { - statesNotExplored[skippedState.second.first->getId()] = skippedState.second; - explorationQueue.push(skippedState.second.second); - } - - // 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 != 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> 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 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.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 - void ExplicitDFTModelBuilderApprox::exploreStateSpace(double approximationThreshold) { - size_t nrExpandedStates = 0; - size_t nrSkippedStates = 0; - // TODO Matthias: do not empty queue every time but break before - while (!explorationQueue.empty()) { - // Get the first state in the queue - ExplorationHeuristicPointer currentExplorationHeuristic = explorationQueue.popTop(); - 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 Matthias: what to do when there is no unique target state? - matrixBuilder.addTransition(failedStateId, storm::utility::zero()); - // Remember skipped state - skippedStates[matrixBuilder.getCurrentRowGroup() - 1] = std::make_pair(currentState, currentExplorationHeuristic); - matrixBuilder.finishRow(); - } else { - // Explore the current state - ++nrExpandedStates; - storm::generator::StateBehavior behavior = generator.expand(std::bind(&ExplicitDFTModelBuilderApprox::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 = std::make_shared(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass()); - iter->second.second = heuristic; - if (state->hasFailed(dft.getTopLevelIndex()) || state->isFailsafe(dft.getTopLevelIndex()) || state->nrFailableDependencies() > 0 || (state->nrFailableDependencies() == 0 && state->nrFailableBEs() == 0)) { - // 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 Mathias: 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(); - } - } - } // 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 - void ExplicitDFTModelBuilderApprox::buildLabeling(LabelOptions const& labelOpts) { - // 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); - // 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 necessary elements - for (size_t id = 0; id < dft.nrElements(); ++id) { - std::shared_ptr const> element = dft.getElement(id); - if (labelOpts.buildAllLabels || labelOpts.elementLabels.count(element->name()) > 0) { - modelComponents.stateLabeling.addLabel(element->name() + "_fail"); - } - } - - // Set labels to states - if (mergeFailedStates) { - modelComponents.stateLabeling.addLabelToState("failed", failedStateId); - } - for (auto const& stateIdPair : stateStorage.stateToId) { - storm::storage::BitVector state = stateIdPair.first; - size_t stateId = matrixBuilder.getRemapping(stateIdPair.second); - if (!mergeFailedStates && labelOpts.buildFailLabel && dft.hasFailed(state, *stateGenerationInfo)) { - modelComponents.stateLabeling.addLabelToState("failed", stateId); - } - if (labelOpts.buildFailSafeLabel && dft.isFailsafe(state, *stateGenerationInfo)) { - modelComponents.stateLabeling.addLabelToState("failsafe", stateId); - } - // Set fail status for each necessary element - for (size_t id = 0; id < dft.nrElements(); ++id) { - std::shared_ptr const> element = dft.getElement(id); - if ((labelOpts.buildAllLabels || labelOpts.elementLabels.count(element->name()) > 0) && storm::storage::DFTState::hasFailed(state, stateGenerationInfo->getStateIndex(element->id()))) { - modelComponents.stateLabeling.addLabelToState(element->name() + "_fail", stateId); - } - } - } - - STORM_LOG_TRACE(modelComponents.stateLabeling); - } - - template - std::shared_ptr> ExplicitDFTModelBuilderApprox::getModel() { - STORM_LOG_ASSERT(skippedStates.size() == 0, "Concrete model has skipped states"); - return createModel(false); - } - - template - std::shared_ptr> ExplicitDFTModelBuilderApprox::getModelApproximation(bool lowerBound, bool expectedTime) { - if (expectedTime) { - // TODO Matthias: handle case with no skipped states - changeMatrixBound(modelComponents.transitionMatrix, lowerBound); - return createModel(true); - } else { - // Change model for probabilities - // TODO Matthias: make nicer - storm::storage::SparseMatrix 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() == failedStateId, "Transition has wrong target state."); - STORM_LOG_ASSERT(!it->second.first->isPseudoState(), "State is still pseudo state."); - matrixEntry->setValue(storm::utility::one()); - 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> model; - if (modelComponents.deterministicModel) { - model = std::make_shared>(std::move(matrix), std::move(labeling)); - } else { - // Build MA - // Compute exit rates - // TODO Matthias: avoid computing multiple times - modelComponents.exitRates = std::vector(modelComponents.markovianStates.size()); - std::vector::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(); - } - } - STORM_LOG_TRACE("Exit rates: " << modelComponents.exitRates); - - storm::storage::sparse::ModelComponents maComponents(std::move(matrix), std::move(labeling)); - maComponents.rateTransitions = true; - maComponents.markovianStates = modelComponents.markovianStates; - maComponents.exitRates = modelComponents.exitRates; - std::shared_ptr> ma = std::make_shared>(std::move(maComponents)); - if (ma->hasOnlyTrivialNondeterminism()) { - // Markov automaton can be converted into CTMC - // TODO Matthias: 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 - std::shared_ptr> ExplicitDFTModelBuilderApprox::createModel(bool copy) { - std::shared_ptr> model; - - if (modelComponents.deterministicModel) { - // Build CTMC - if (copy) { - model = std::make_shared>(modelComponents.transitionMatrix, modelComponents.stateLabeling); - } else { - model = std::make_shared>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling)); - } - } else { - // Build MA - // Compute exit rates - // TODO Matthias: avoid computing multiple times - modelComponents.exitRates = std::vector(modelComponents.markovianStates.size()); - std::vector::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(); - } - } - STORM_LOG_TRACE("Exit rates: " << modelComponents.exitRates); - - std::shared_ptr> ma; - if (copy) { - storm::storage::sparse::ModelComponents maComponents(modelComponents.transitionMatrix, modelComponents.stateLabeling); - maComponents.rateTransitions = true; - maComponents.markovianStates = modelComponents.markovianStates; - maComponents.exitRates = modelComponents.exitRates; - std::shared_ptr> ma = std::make_shared>(std::move(maComponents)); - } else { - storm::storage::sparse::ModelComponents maComponents(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling)); - maComponents.rateTransitions = true; - maComponents.markovianStates = std::move(modelComponents.markovianStates); - maComponents.exitRates = std::move(modelComponents.exitRates); - std::shared_ptr> ma = std::make_shared>(std::move(maComponents)); - } - if (ma->hasOnlyTrivialNondeterminism()) { - // Markov automaton can be converted into CTMC - // TODO Matthias: 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 - void ExplicitDFTModelBuilderApprox::changeMatrixBound(storm::storage::SparseMatrix & 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() == failedStateId, "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::isZero(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 - ValueType ExplicitDFTModelBuilderApprox::getLowerBound(DFTStatePointer const& state) const { - // Get the lower bound by considering the failure of all possible BEs - ValueType lowerBound = storm::utility::zero(); - for (size_t index = 0; index < state->nrFailableBEs(); ++index) { - lowerBound += state->getFailableBERate(index); - } - return lowerBound; - } - - template - ValueType ExplicitDFTModelBuilderApprox::getUpperBound(DFTStatePointer const& state) const { - if (state->hasFailed(dft.getTopLevelIndex())) { - return storm::utility::zero(); - } - - // Get the upper bound by considering the failure of all BEs - ValueType upperBound = storm::utility::one(); - ValueType rateSum = storm::utility::zero(); - - // Compute for each independent subtree - for (std::vector const& subtree : subtreeBEs) { - // Get all possible rates - std::vector rates; - storm::storage::BitVector coldBEs(subtree.size(), false); - for (size_t i = 0; i < subtree.size(); ++i) { - size_t id = subtree[i]; - if (state->isOperational(id)) { - // Get BE rate - ValueType rate = state->getBERate(id); - if (storm::utility::isZero(rate)) { - // Get active failure rate for cold BE - rate = dft.getBasicElement(id)->activeFailureRate(); - if (storm::utility::isZero(rate)) { - // Ignore BE which cannot fail - continue; - } - // Mark BE as cold - coldBEs.set(i, true); - } - rates.push_back(rate); - rateSum += rate; - } - } - - STORM_LOG_ASSERT(rates.size() > 0, "No rates failable"); - - // Sort rates - std::sort(rates.begin(), rates.end()); - std::vector 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 - ValueType ExplicitDFTModelBuilderApprox::computeMTTFAnd(std::vector const& rates, size_t size) const { - ValueType result = storm::utility::zero(); - if (size == 0) { - return result; - } - - // TODO Matthias: 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(i)); - ValueType sum = storm::utility::zero(); - do { - ValueType permResult = storm::utility::zero(); - for(size_t j = 0; j < rates.size(); ++j) { - if(permutation & static_cast(1 << static_cast(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() / permResult; - } while(permutation < (static_cast(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(); - 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 - StateType ExplicitDFTModelBuilderApprox::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 Matthias: 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 - 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(matrixBuilder.getCurrentRowGroup() - 1, markovian); - } - - template - void ExplicitDFTModelBuilderApprox::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 ExplicitDFTModelBuilderApprox; - -#ifdef STORM_HAVE_CARL - template class ExplicitDFTModelBuilderApprox; -#endif - - } // namespace builder -} // namespace storm - - diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h deleted file mode 100644 index 802aefe1b..000000000 --- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h +++ /dev/null @@ -1,362 +0,0 @@ -#pragma once - -#include -#include -#include -#include -#include - -#include "storm/models/sparse/StateLabeling.h" -#include "storm/models/sparse/ChoiceLabeling.h" -#include "storm/models/sparse/StandardRewardModel.h" -#include "storm/models/sparse/Model.h" -#include "storm/storage/SparseMatrix.h" -#include "storm/storage/sparse/StateStorage.h" - -#include "storm-dft/builder/DftExplorationHeuristic.h" -#include "storm-dft/generator/DftNextStateGenerator.h" -#include "storm-dft/storage/dft/DFT.h" -#include "storm-dft/storage/dft/SymmetricUnits.h" -#include "storm-dft/storage/BucketPriorityQueue.h" - -namespace storm { - namespace builder { - - /*! - * Build a Markov chain from DFT. - */ - template - class ExplicitDFTModelBuilderApprox { - - using DFTStatePointer = std::shared_ptr>; - // TODO Matthias: make choosable - using ExplorationHeuristic = DFTExplorationHeuristicDepth; - using ExplorationHeuristicPointer = std::shared_ptr; - - - // A structure holding the individual components of a model. - struct ModelComponents { - // Constructor - ModelComponents(); - - // The transition matrix. - storm::storage::SparseMatrix transitionMatrix; - - // The state labeling. - storm::models::sparse::StateLabeling stateLabeling; - - // The Markovian states. - storm::storage::BitVector markovianStates; - - // The exit rates. - std::vector exitRates; - - // A vector that stores a labeling for each choice. - boost::optional choiceLabeling; - - // A flag indicating if the model is deterministic. - 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; - } - - /*! - * Get the remapped state for the given id. - * - * @param id State. - * - * @return Remapped index. - */ - StateType getRemapping(StateType id) { - STORM_LOG_ASSERT(id < stateRemapping.size(), "Invalid index for remapping."); - return stateRemapping[id]; - } - - // 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; - - // Flag indicating if row groups are needed. - bool canHaveNondeterminism; - }; - - public: - // A structure holding the labeling options. - struct LabelOptions { - // Constructor - LabelOptions(std::vector> properties, bool buildAllLabels = false); - - // Flag indicating if the general fail label should be included. - bool buildFailLabel; - - // Flag indicating if the general failsafe label should be included. - bool buildFailSafeLabel; - - // Flag indicating if all possible labels should be included. - bool buildAllLabels; - - // Set of element names whose fail label to include. - std::set elementLabels; - }; - - /*! - * Constructor. - * - * @param dft DFT. - * @param symmetries Symmetries in the dft. - * @param enableDC Flag indicating if dont care propagation should be used. - */ - ExplicitDFTModelBuilderApprox(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC); - - /*! - * Build model from DFT. - * - * @param labelOpts Options for labeling. - * @param iteration Current number of iteration. - * @param approximationThreshold Threshold determining when to skip exploring states. - */ - void buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold = 0.0); - - /*! - * Get the built model. - * - * @return The model built from the DFT. - */ - std::shared_ptr> getModel(); - - /*! - * Get the built approximation model for either the lower or upper bound. - * - * @param lowerBound If true, the lower bound model is returned, else the upper bound model - * @param expectedTime If true, the bounds for expected time are computed, else the bounds for probabilities. - * - * @return The model built from the DFT. - */ - std::shared_ptr> getModelApproximation(bool lowerBound, bool expectedTime); - - private: - - /*! - * Explore state space of DFT. - * - * @param approximationThreshold Threshold to determine when to skip states. - */ - void exploreStateSpace(double approximationThreshold); - - /*! - * 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. - * - * @param state The state to add. - * - * @return Id of state. - */ - StateType getOrAddStateIndex(DFTStatePointer const& state); - - /*! - * Set markovian flag for the current state. - * - * @param markovian Flag indicating if the state is markovian. - */ - void setMarkovian(bool markovian); - - /** - * Change matrix to reflect the lower or upper approximation bound. - * - * @param matrix Matrix to change. The change are reflected here. - * @param lowerBound Flag indicating if the lower bound should be used. Otherwise the upper bound is used. - */ - void changeMatrixBound(storm::storage::SparseMatrix & matrix, bool lowerBound) const; - - /*! - * Get lower bound approximation for state. - * - * @param state The state. - * - * @return Lower bound approximation. - */ - ValueType getLowerBound(DFTStatePointer const& state) const; - - /*! - * Get upper bound approximation for state. - * - * @param state The state. - * - * @return Upper bound approximation. - */ - ValueType getUpperBound(DFTStatePointer const& state) const; - - /*! - * Compute the MTTF of an AND gate via a closed formula. - * The used formula is 1/( 1/a + 1/b + 1/c + ... - 1/(a+b) - 1/(a+c) - ... + 1/(a+b+c) + ... - ...) - * - * @param rates List of rates of children of AND. - * @param size Only indices < size are considered in the vector. - * @return MTTF. - */ - ValueType computeMTTFAnd(std::vector const& rates, size_t size) const; - - /*! - * Compares the priority of two states. - * - * @param idA Id of first state - * @param idB Id of second state - * - * @return True if the priority of the first state is greater then the priority of the second one. - */ - bool isPriorityGreater(StateType idA, StateType idB) const; - - void printNotExplored() const; - - /*! - * Create the model model from the model components. - * - * @param copy If true, all elements of the model component are copied (used for approximation). If false - * they are moved to reduce the memory overhead. - * - * @return The model built from the model components. - */ - std::shared_ptr> createModel(bool copy); - - // Initial size of the bitvector. - const size_t INITIAL_BITVECTOR_SIZE = 20000; - // Offset used for pseudo states. - const StateType OFFSET_PSEUDO_STATE = std::numeric_limits::max() / 2; - - // Dft - storm::storage::DFT const& dft; - - // General information for state generation - // TODO Matthias: use const reference - std::shared_ptr stateGenerationInfo; - - // Flag indication if dont care propagation should be used. - bool enableDC = true; - - //TODO Matthias: make changeable - const bool mergeFailedStates = true; - - // Heuristic used for approximation - storm::builder::ApproximationHeuristic usedHeuristic; - - // 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; - - // 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 priority queue of states that still need to be explored. - storm::storage::BucketPriorityQueue explorationQueue; - - // A mapping of not yet explored states from the id to the tuple (state object, heuristic values). - std::map> statesNotExplored; - - // 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. - // TODO remove again - std::map> skippedStates; - - // List of independent subtrees and the BEs contained in them. - std::vector> subtreeBEs; - }; - - } -} diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index 7b86d1faa..0002cd6a3 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -4,7 +4,7 @@ #include "storm/utility/macros.h" #include "storm/exceptions/NotImplementedException.h" #include "storm/settings/SettingsManager.h" -#include "storm-dft/settings/modules/DFTSettings.h" +#include "storm-dft/settings/modules/FaultTreeSettings.h" namespace storm { namespace generator { @@ -71,7 +71,7 @@ namespace storm { // Let BE fail while (currentFailable < failableCount) { - if (storm::settings::getModule().isTakeFirstDependency() && hasDependencies && currentFailable > 0) { + if (storm::settings::getModule().isTakeFirstDependency() && hasDependencies && currentFailable > 0) { // We discard further exploration as we already chose one dependent event break; } diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index d6b7e9138..d2b435c1c 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -6,9 +6,8 @@ #include "storm/utility/DirectEncodingExporter.h" #include "storm-dft/builder/ExplicitDFTModelBuilder.h" -#include "storm-dft/builder/ExplicitDFTModelBuilderApprox.h" #include "storm-dft/storage/dft/DFTIsomorphism.h" -#include "storm-dft/settings/modules/DFTSettings.h" +#include "storm-dft/settings/modules/FaultTreeSettings.h" namespace storm { @@ -192,8 +191,8 @@ namespace storm { // Build a single CTMC STORM_LOG_INFO("Building Model..."); - storm::builder::ExplicitDFTModelBuilderApprox builder(ft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions(properties); + storm::builder::ExplicitDFTModelBuilder builder(ft, symmetries, enableDC); + typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties); builder.buildModel(labeloptions, 0, 0.0); std::shared_ptr> model = builder.getModel(); explorationTimer.stop(); @@ -244,9 +243,8 @@ namespace storm { // Build a single CTMC STORM_LOG_INFO("Building Model..."); - - storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions(properties); + storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, enableDC); + typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties); builder.buildModel(labeloptions, 0, 0.0); std::shared_ptr> model = builder.getModel(); model->printModelInformationToStream(std::cout); @@ -277,8 +275,8 @@ namespace storm { approximation_result approxResult = std::make_pair(storm::utility::zero(), storm::utility::zero()); std::shared_ptr> model; std::vector newResult; - storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions(properties); + storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, enableDC); + typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties); // TODO Matthias: compute approximation for all properties simultaneously? std::shared_ptr property = properties[0]; @@ -342,18 +340,10 @@ namespace storm { } else { // Build a single Markov Automaton STORM_LOG_INFO("Building Model..."); - std::shared_ptr> model; - // TODO Matthias: use only one builder if everything works again - if (storm::settings::getModule().isApproximationErrorSet()) { - storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions(properties, storm::settings::getModule().isExportExplicitSet()); - builder.buildModel(labeloptions, 0, 0.0); - model = builder.getModel(); - } else { - storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions; - model = builder.buildModel(labeloptions); - } + storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, enableDC); + typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties, storm::settings::getModule().isExportExplicitSet()); + builder.buildModel(labeloptions, 0, 0.0); + std::shared_ptr> model = builder.getModel(); model->printModelInformationToStream(std::cout); explorationTimer.stop(); diff --git a/src/storm-dft/settings/DftSettings.cpp b/src/storm-dft/settings/DftSettings.cpp new file mode 100644 index 000000000..ce48c6fd9 --- /dev/null +++ b/src/storm-dft/settings/DftSettings.cpp @@ -0,0 +1,51 @@ +#include "storm-dft/settings/DftSettings.h" + +#include "storm-dft/settings/modules/DftIOSettings.h" +#include "storm-dft/settings/modules/FaultTreeSettings.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/GeneralSettings.h" +#include "storm/settings/modules/CoreSettings.h" +#include "storm/settings/modules/IOSettings.h" +#include "storm/settings/modules/DebugSettings.h" +#include "storm/settings/modules/EigenEquationSolverSettings.h" +#include "storm/settings/modules/GmmxxEquationSolverSettings.h" +#include "storm/settings/modules/NativeEquationSolverSettings.h" +#include "storm/settings/modules/EliminationSettings.h" +#include "storm/settings/modules/MinMaxEquationSolverSettings.h" +#include "storm/settings/modules/BisimulationSettings.h" +#include "storm/settings/modules/ResourceSettings.h" +#include "storm/settings/modules/JaniExportSettings.h" +#include "storm/settings/modules/GSPNSettings.h" +#include "storm/settings/modules/GSPNExportSettings.h" + + +namespace storm { + namespace settings { + void initializeDftSettings(std::string const& name, std::string const& executableName) { + storm::settings::mutableManager().setName(name, executableName); + + // Register relevant settings modules. + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + // storm::settings::addModule(); + storm::settings::addModule(); + + // For translation into JANI via GSPN. + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + } + + } +} diff --git a/src/storm-dft/settings/DftSettings.h b/src/storm-dft/settings/DftSettings.h new file mode 100644 index 000000000..8f67ec0b7 --- /dev/null +++ b/src/storm-dft/settings/DftSettings.h @@ -0,0 +1,11 @@ +#pragma once + +#include + +namespace storm { + namespace settings { + + void initializeDftSettings(std::string const& name, std::string const& executableName); + + } +} diff --git a/src/storm-dft/settings/modules/DFTSettings.cpp b/src/storm-dft/settings/modules/DFTSettings.cpp deleted file mode 100644 index 1a8d59d70..000000000 --- a/src/storm-dft/settings/modules/DFTSettings.cpp +++ /dev/null @@ -1,189 +0,0 @@ -#include "DFTSettings.h" - -#include "storm/settings/SettingsManager.h" -#include "storm/settings/SettingMemento.h" -#include "storm/settings/Option.h" -#include "storm/settings/OptionBuilder.h" -#include "storm/settings/ArgumentBuilder.h" -#include "storm/settings/Argument.h" - -#include "storm/exceptions/InvalidSettingsException.h" -#include "storm/exceptions/IllegalArgumentValueException.h" - -namespace storm { - namespace settings { - namespace modules { - - const std::string DFTSettings::moduleName = "dft"; - const std::string DFTSettings::dftFileOptionName = "dftfile"; - const std::string DFTSettings::dftFileOptionShortName = "dft"; - const std::string DFTSettings::dftJsonFileOptionName = "dftfile-json"; - const std::string DFTSettings::dftJsonFileOptionShortName = "dftjson"; - const std::string DFTSettings::symmetryReductionOptionName = "symmetryreduction"; - const std::string DFTSettings::symmetryReductionOptionShortName = "symred"; - const std::string DFTSettings::modularisationOptionName = "modularisation"; - const std::string DFTSettings::disableDCOptionName = "disabledc"; - const std::string DFTSettings::approximationErrorOptionName = "approximation"; - const std::string DFTSettings::approximationErrorOptionShortName = "approx"; - const std::string DFTSettings::approximationHeuristicOptionName = "approximationheuristic"; - const std::string DFTSettings::propExpectedTimeOptionName = "expectedtime"; - const std::string DFTSettings::propExpectedTimeOptionShortName = "mttf"; - const std::string DFTSettings::propProbabilityOptionName = "probability"; - const std::string DFTSettings::propTimeboundOptionName = "timebound"; - const std::string DFTSettings::propTimepointsOptionName = "timepoints"; - const std::string DFTSettings::minValueOptionName = "min"; - const std::string DFTSettings::maxValueOptionName = "max"; - const std::string DFTSettings::firstDependencyOptionName = "firstdep"; - const std::string DFTSettings::transformToGspnOptionName = "gspn"; - const std::string DFTSettings::exportToJsonOptionName = "export-json"; -#ifdef STORM_HAVE_Z3 - const std::string DFTSettings::solveWithSmtOptionName = "smt"; -#endif - - DFTSettings::DFTSettings() : ModuleSettings(moduleName) { - this->addOption(storm::settings::OptionBuilder(moduleName, dftFileOptionName, false, "Parses the model given in the Galileo format.").setShortName(dftFileOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, dftJsonFileOptionName, false, "Parses the model given in the Cytoscape JSON format.").setShortName(dftJsonFileOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, symmetryReductionOptionName, false, "Exploit symmetric structure of model.").setShortName(symmetryReductionOptionShortName).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, modularisationOptionName, false, "Use modularisation (not applicable for expected time).").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, disableDCOptionName, false, "Disable Dont Care propagation.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, firstDependencyOptionName, false, "Avoid non-determinism by always taking the first possible dependency.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, approximationErrorOptionName, false, "Approximation error allowed.").setShortName(approximationErrorOptionShortName).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("error", "The relative approximation error to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, approximationHeuristicOptionName, false, "Set the heuristic used for approximation.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "Sets which heuristic is used for approximation. Must be in {depth, probability}. Default is").setDefaultValueString("depth").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"depth", "rateratio"})).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, propExpectedTimeOptionName, false, "Compute expected time of system failure.").setShortName(propExpectedTimeOptionShortName).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, propProbabilityOptionName, false, "Compute probability of system failure.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, propTimeboundOptionName, false, "Compute probability of system failure up to given timebound.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time", "The timebound to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, propTimepointsOptionName, false, "Compute probability of system failure up to given timebound for a set of given timepoints [starttime, starttime+inc, starttime+2inc, ... ,endtime]").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("starttime", "The timebound to start from.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("endtime", "The timebound to end with.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("inc", "The value to increment with to get the next timepoint.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, minValueOptionName, false, "Compute minimal value in case of non-determinism.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, maxValueOptionName, false, "Compute maximal value in case of non-determinism.").build()); -#ifdef STORM_HAVE_Z3 - this->addOption(storm::settings::OptionBuilder(moduleName, solveWithSmtOptionName, true, "Solve the DFT with SMT.").build()); -#endif - this->addOption(storm::settings::OptionBuilder(moduleName, transformToGspnOptionName, false, "Transform DFT to GSPN.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, exportToJsonOptionName, false, "Export the model to the Cytoscape JSON format.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file to export to.").build()).build()); - } - - bool DFTSettings::isDftFileSet() const { - return this->getOption(dftFileOptionName).getHasOptionBeenSet(); - } - - std::string DFTSettings::getDftFilename() const { - return this->getOption(dftFileOptionName).getArgumentByName("filename").getValueAsString(); - } - - bool DFTSettings::isDftJsonFileSet() const { - return this->getOption(dftJsonFileOptionName).getHasOptionBeenSet(); - } - - std::string DFTSettings::getDftJsonFilename() const { - return this->getOption(dftJsonFileOptionName).getArgumentByName("filename").getValueAsString(); - } - - bool DFTSettings::useSymmetryReduction() const { - return this->getOption(symmetryReductionOptionName).getHasOptionBeenSet(); - } - - bool DFTSettings::useModularisation() const { - return this->getOption(modularisationOptionName).getHasOptionBeenSet(); - } - - bool DFTSettings::isDisableDC() const { - return this->getOption(disableDCOptionName).getHasOptionBeenSet(); - } - - bool DFTSettings::isApproximationErrorSet() const { - return this->getOption(approximationErrorOptionName).getHasOptionBeenSet(); - } - - double DFTSettings::getApproximationError() const { - return this->getOption(approximationErrorOptionName).getArgumentByName("error").getValueAsDouble(); - } - - storm::builder::ApproximationHeuristic DFTSettings::getApproximationHeuristic() const { - if (!isApproximationErrorSet() || getApproximationError() == 0.0) { - // No approximation is done - return storm::builder::ApproximationHeuristic::NONE; - } - std::string heuristicAsString = this->getOption(approximationHeuristicOptionName).getArgumentByName("heuristic").getValueAsString(); - if (heuristicAsString == "depth") { - return storm::builder::ApproximationHeuristic::DEPTH; - } else if (heuristicAsString == "probability") { - return storm::builder::ApproximationHeuristic::PROBABILITY; - } - STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal value '" << heuristicAsString << "' set as heuristic for approximation."); - } - - bool DFTSettings::usePropExpectedTime() const { - return this->getOption(propExpectedTimeOptionName).getHasOptionBeenSet(); - } - - bool DFTSettings::usePropProbability() const { - return this->getOption(propProbabilityOptionName).getHasOptionBeenSet(); - } - - bool DFTSettings::usePropTimebound() const { - return this->getOption(propTimeboundOptionName).getHasOptionBeenSet(); - } - - double DFTSettings::getPropTimebound() const { - return this->getOption(propTimeboundOptionName).getArgumentByName("time").getValueAsDouble(); - } - - bool DFTSettings::usePropTimepoints() const { - return this->getOption(propTimepointsOptionName).getHasOptionBeenSet(); - } - - std::vector DFTSettings::getPropTimepoints() const { - double starttime = this->getOption(propTimepointsOptionName).getArgumentByName("starttime").getValueAsDouble(); - double endtime = this->getOption(propTimepointsOptionName).getArgumentByName("endtime").getValueAsDouble(); - double inc = this->getOption(propTimepointsOptionName).getArgumentByName("inc").getValueAsDouble(); - std::vector timepoints; - for (double time = starttime; time <= endtime; time += inc) { - timepoints.push_back(time); - } - return timepoints; - } - - bool DFTSettings::isComputeMinimalValue() const { - return this->getOption(minValueOptionName).getHasOptionBeenSet(); - } - - bool DFTSettings::isComputeMaximalValue() const { - return this->getOption(maxValueOptionName).getHasOptionBeenSet(); - } - - bool DFTSettings::isTakeFirstDependency() const { - return this->getOption(firstDependencyOptionName).getHasOptionBeenSet(); - } - -#ifdef STORM_HAVE_Z3 - bool DFTSettings::solveWithSMT() const { - return this->getOption(solveWithSmtOptionName).getHasOptionBeenSet(); - } -#endif - - bool DFTSettings::isTransformToGspn() const { - return this->getOption(transformToGspnOptionName).getHasOptionBeenSet(); - } - - bool DFTSettings::isExportToJson() const { - return this->getOption(exportToJsonOptionName).getHasOptionBeenSet(); - } - - std::string DFTSettings::getExportJsonFilename() const { - return this->getOption(exportToJsonOptionName).getArgumentByName("filename").getValueAsString(); - } - - void DFTSettings::finalize() { - } - - bool DFTSettings::check() const { - // Ensure that at most one of min or max is set - STORM_LOG_THROW(!isComputeMinimalValue() || !isComputeMaximalValue(), storm::exceptions::InvalidSettingsException, "Min and max can not both be set."); - return true; - } - - } // namespace modules - } // namespace settings -} // namespace storm diff --git a/src/storm-dft/settings/modules/DftIOSettings.cpp b/src/storm-dft/settings/modules/DftIOSettings.cpp new file mode 100644 index 000000000..cf656333d --- /dev/null +++ b/src/storm-dft/settings/modules/DftIOSettings.cpp @@ -0,0 +1,123 @@ +#include "DftIOSettings.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/SettingMemento.h" +#include "storm/settings/Option.h" +#include "storm/settings/OptionBuilder.h" +#include "storm/settings/ArgumentBuilder.h" +#include "storm/settings/Argument.h" +#include "storm/exceptions/InvalidSettingsException.h" + +namespace storm { + namespace settings { + namespace modules { + + const std::string DftIOSettings::moduleName = "dftIO"; + const std::string DftIOSettings::dftFileOptionName = "dftfile"; + const std::string DftIOSettings::dftFileOptionShortName = "dft"; + const std::string DftIOSettings::dftJsonFileOptionName = "dftfile-json"; + const std::string DftIOSettings::dftJsonFileOptionShortName = "dftjson"; + const std::string DftIOSettings::propExpectedTimeOptionName = "expectedtime"; + const std::string DftIOSettings::propExpectedTimeOptionShortName = "mttf"; + const std::string DftIOSettings::propProbabilityOptionName = "probability"; + const std::string DftIOSettings::propTimeboundOptionName = "timebound"; + const std::string DftIOSettings::propTimepointsOptionName = "timepoints"; + const std::string DftIOSettings::minValueOptionName = "min"; + const std::string DftIOSettings::maxValueOptionName = "max"; + const std::string DftIOSettings::transformToGspnOptionName = "gspn"; + const std::string DftIOSettings::exportToJsonOptionName = "export-json"; + + DftIOSettings::DftIOSettings() : ModuleSettings(moduleName) { + this->addOption(storm::settings::OptionBuilder(moduleName, dftFileOptionName, false, "Parses the model given in the Galileo format.").setShortName(dftFileOptionShortName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, dftJsonFileOptionName, false, "Parses the model given in the Cytoscape JSON format.").setShortName(dftJsonFileOptionShortName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, propExpectedTimeOptionName, false, "Compute expected time of system failure.").setShortName(propExpectedTimeOptionShortName).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, propProbabilityOptionName, false, "Compute probability of system failure.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, propTimeboundOptionName, false, "Compute probability of system failure up to given timebound.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time", "The timebound to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, propTimepointsOptionName, false, "Compute probability of system failure up to given timebound for a set of given timepoints [starttime, starttime+inc, starttime+2inc, ... ,endtime]").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("starttime", "The timebound to start from.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("endtime", "The timebound to end with.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("inc", "The value to increment with to get the next timepoint.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, minValueOptionName, false, "Compute minimal value in case of non-determinism.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, maxValueOptionName, false, "Compute maximal value in case of non-determinism.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, transformToGspnOptionName, false, "Transform DFT to GSPN.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, exportToJsonOptionName, false, "Export the model to the Cytoscape JSON format.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file to export to.").build()).build()); + } + + bool DftIOSettings::isDftFileSet() const { + return this->getOption(dftFileOptionName).getHasOptionBeenSet(); + } + + std::string DftIOSettings::getDftFilename() const { + return this->getOption(dftFileOptionName).getArgumentByName("filename").getValueAsString(); + } + + bool DftIOSettings::isDftJsonFileSet() const { + return this->getOption(dftJsonFileOptionName).getHasOptionBeenSet(); + } + + std::string DftIOSettings::getDftJsonFilename() const { + return this->getOption(dftJsonFileOptionName).getArgumentByName("filename").getValueAsString(); + } + + bool DftIOSettings::usePropExpectedTime() const { + return this->getOption(propExpectedTimeOptionName).getHasOptionBeenSet(); + } + + bool DftIOSettings::usePropProbability() const { + return this->getOption(propProbabilityOptionName).getHasOptionBeenSet(); + } + + bool DftIOSettings::usePropTimebound() const { + return this->getOption(propTimeboundOptionName).getHasOptionBeenSet(); + } + + double DftIOSettings::getPropTimebound() const { + return this->getOption(propTimeboundOptionName).getArgumentByName("time").getValueAsDouble(); + } + + bool DftIOSettings::usePropTimepoints() const { + return this->getOption(propTimepointsOptionName).getHasOptionBeenSet(); + } + + std::vector DftIOSettings::getPropTimepoints() const { + double starttime = this->getOption(propTimepointsOptionName).getArgumentByName("starttime").getValueAsDouble(); + double endtime = this->getOption(propTimepointsOptionName).getArgumentByName("endtime").getValueAsDouble(); + double inc = this->getOption(propTimepointsOptionName).getArgumentByName("inc").getValueAsDouble(); + std::vector timepoints; + for (double time = starttime; time <= endtime; time += inc) { + timepoints.push_back(time); + } + return timepoints; + } + + bool DftIOSettings::isComputeMinimalValue() const { + return this->getOption(minValueOptionName).getHasOptionBeenSet(); + } + + bool DftIOSettings::isComputeMaximalValue() const { + return this->getOption(maxValueOptionName).getHasOptionBeenSet(); + } + + bool DftIOSettings::isTransformToGspn() const { + return this->getOption(transformToGspnOptionName).getHasOptionBeenSet(); + } + + bool DftIOSettings::isExportToJson() const { + return this->getOption(exportToJsonOptionName).getHasOptionBeenSet(); + } + + std::string DftIOSettings::getExportJsonFilename() const { + return this->getOption(exportToJsonOptionName).getArgumentByName("filename").getValueAsString(); + } + + void DftIOSettings::finalize() { + } + + bool DftIOSettings::check() const { + // Ensure that at most one of min or max is set + STORM_LOG_THROW(!isComputeMinimalValue() || !isComputeMaximalValue(), storm::exceptions::InvalidSettingsException, "Min and max can not both be set."); + return true; + } + + } // namespace modules + } // namespace settings +} // namespace storm diff --git a/src/storm-dft/settings/modules/DFTSettings.h b/src/storm-dft/settings/modules/DftIOSettings.h similarity index 63% rename from src/storm-dft/settings/modules/DFTSettings.h rename to src/storm-dft/settings/modules/DftIOSettings.h index c04ef1a23..8a8fbcdd1 100644 --- a/src/storm-dft/settings/modules/DFTSettings.h +++ b/src/storm-dft/settings/modules/DftIOSettings.h @@ -1,24 +1,21 @@ #pragma once -#include "storm-config.h" #include "storm/settings/modules/ModuleSettings.h" -#include "storm-dft/builder/DftExplorationHeuristic.h" - namespace storm { namespace settings { namespace modules { /*! - * This class represents the settings for DFT model checking. + * This class represents the settings for IO operations concerning DFTs. */ - class DFTSettings : public ModuleSettings { + class DftIOSettings : public ModuleSettings { public: /*! - * Creates a new set of DFT settings. + * Creates a new set of IO settings for DFTs. */ - DFTSettings(); + DftIOSettings(); /*! * Retrieves whether the dft file option was set. @@ -48,48 +45,6 @@ namespace storm { */ std::string getDftJsonFilename() const; - /*! - * Retrieves whether the option to use symmetry reduction is set. - * - * @return True iff the option was set. - */ - bool useSymmetryReduction() const; - - /*! - * Retrieves whether the option to use modularisation is set. - * - * @return True iff the option was set. - */ - bool useModularisation() const; - - /*! - * Retrieves whether the option to disable Dont Care propagation is set. - * - * @return True iff the option was set. - */ - bool isDisableDC() const; - - /*! - * Retrieves whether the option to compute an approximation is set. - * - * @return True iff the option was set. - */ - bool isApproximationErrorSet() const; - - /*! - * Retrieves the relative error allowed for approximating the model checking result. - * - * @return The allowed errorbound. - */ - double getApproximationError() const; - - /*! - * Retrieves the heuristic used for approximation. - * - * @return The heuristic to use. - */ - storm::builder::ApproximationHeuristic getApproximationHeuristic() const; - /*! * Retrieves whether the property expected time should be used. * @@ -146,13 +101,6 @@ namespace storm { */ bool isComputeMaximalValue() const; - /*! - * Retrieves whether the non-determinism should be avoided by always taking the first possible dependency. - * - * @return True iff the option was set. - */ - bool isTakeFirstDependency() const; - /*! * Retrieves whether the DFT should be transformed into a GSPN. * @@ -174,15 +122,6 @@ namespace storm { */ std::string getExportJsonFilename() const; -#ifdef STORM_HAVE_Z3 - /*! - * Retrieves whether the DFT should be checked via SMT. - * - * @return True iff the option was set. - */ - bool solveWithSMT() const; -#endif - bool check() const override; void finalize() override; @@ -195,13 +134,6 @@ namespace storm { static const std::string dftFileOptionShortName; static const std::string dftJsonFileOptionName; static const std::string dftJsonFileOptionShortName; - static const std::string symmetryReductionOptionName; - static const std::string symmetryReductionOptionShortName; - static const std::string modularisationOptionName; - static const std::string disableDCOptionName; - static const std::string approximationErrorOptionName; - static const std::string approximationErrorOptionShortName; - static const std::string approximationHeuristicOptionName; static const std::string propExpectedTimeOptionName; static const std::string propExpectedTimeOptionShortName; static const std::string propProbabilityOptionName; @@ -209,10 +141,6 @@ namespace storm { static const std::string propTimepointsOptionName; static const std::string minValueOptionName; static const std::string maxValueOptionName; - static const std::string firstDependencyOptionName; -#ifdef STORM_HAVE_Z3 - static const std::string solveWithSmtOptionName; -#endif static const std::string transformToGspnOptionName; static const std::string exportToJsonOptionName; diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.cpp b/src/storm-dft/settings/modules/FaultTreeSettings.cpp new file mode 100644 index 000000000..7c9ef14af --- /dev/null +++ b/src/storm-dft/settings/modules/FaultTreeSettings.cpp @@ -0,0 +1,93 @@ +#include "FaultTreeSettings.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/SettingMemento.h" +#include "storm/settings/Option.h" +#include "storm/settings/OptionBuilder.h" +#include "storm/settings/ArgumentBuilder.h" +#include "storm/settings/Argument.h" +#include "storm/exceptions/IllegalArgumentValueException.h" + +namespace storm { + namespace settings { + namespace modules { + + const std::string FaultTreeSettings::moduleName = "dft"; + const std::string FaultTreeSettings::symmetryReductionOptionName = "symmetryreduction"; + const std::string FaultTreeSettings::symmetryReductionOptionShortName = "symred"; + const std::string FaultTreeSettings::modularisationOptionName = "modularisation"; + const std::string FaultTreeSettings::disableDCOptionName = "disabledc"; + const std::string FaultTreeSettings::approximationErrorOptionName = "approximation"; + const std::string FaultTreeSettings::approximationErrorOptionShortName = "approx"; + const std::string FaultTreeSettings::approximationHeuristicOptionName = "approximationheuristic"; + const std::string FaultTreeSettings::firstDependencyOptionName = "firstdep"; +#ifdef STORM_HAVE_Z3 + const std::string FaultTreeSettings::solveWithSmtOptionName = "smt"; +#endif + + FaultTreeSettings::FaultTreeSettings() : ModuleSettings(moduleName) { + this->addOption(storm::settings::OptionBuilder(moduleName, symmetryReductionOptionName, false, "Exploit symmetric structure of model.").setShortName(symmetryReductionOptionShortName).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, modularisationOptionName, false, "Use modularisation (not applicable for expected time).").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, disableDCOptionName, false, "Disable Dont Care propagation.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, firstDependencyOptionName, false, "Avoid non-determinism by always taking the first possible dependency.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, approximationErrorOptionName, false, "Approximation error allowed.").setShortName(approximationErrorOptionShortName).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("error", "The relative approximation error to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, approximationHeuristicOptionName, false, "Set the heuristic used for approximation.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "Sets which heuristic is used for approximation. Must be in {depth, probability}. Default is").setDefaultValueString("depth").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"depth", "rateratio"})).build()).build()); +#ifdef STORM_HAVE_Z3 + this->addOption(storm::settings::OptionBuilder(moduleName, solveWithSmtOptionName, true, "Solve the DFT with SMT.").build()); +#endif + } + + bool FaultTreeSettings::useSymmetryReduction() const { + return this->getOption(symmetryReductionOptionName).getHasOptionBeenSet(); + } + + bool FaultTreeSettings::useModularisation() const { + return this->getOption(modularisationOptionName).getHasOptionBeenSet(); + } + + bool FaultTreeSettings::isDisableDC() const { + return this->getOption(disableDCOptionName).getHasOptionBeenSet(); + } + + bool FaultTreeSettings::isApproximationErrorSet() const { + return this->getOption(approximationErrorOptionName).getHasOptionBeenSet(); + } + + double FaultTreeSettings::getApproximationError() const { + return this->getOption(approximationErrorOptionName).getArgumentByName("error").getValueAsDouble(); + } + + storm::builder::ApproximationHeuristic FaultTreeSettings::getApproximationHeuristic() const { + if (!isApproximationErrorSet() || getApproximationError() == 0.0) { + // No approximation is done + return storm::builder::ApproximationHeuristic::NONE; + } + std::string heuristicAsString = this->getOption(approximationHeuristicOptionName).getArgumentByName("heuristic").getValueAsString(); + if (heuristicAsString == "depth") { + return storm::builder::ApproximationHeuristic::DEPTH; + } else if (heuristicAsString == "probability") { + return storm::builder::ApproximationHeuristic::PROBABILITY; + } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal value '" << heuristicAsString << "' set as heuristic for approximation."); + } + + bool FaultTreeSettings::isTakeFirstDependency() const { + return this->getOption(firstDependencyOptionName).getHasOptionBeenSet(); + } + +#ifdef STORM_HAVE_Z3 + bool FaultTreeSettings::solveWithSMT() const { + return this->getOption(solveWithSmtOptionName).getHasOptionBeenSet(); + } +#endif + + void FaultTreeSettings::finalize() { + } + + bool FaultTreeSettings::check() const { + return true; + } + + } // namespace modules + } // namespace settings +} // namespace storm diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.h b/src/storm-dft/settings/modules/FaultTreeSettings.h new file mode 100644 index 000000000..171d5c38e --- /dev/null +++ b/src/storm-dft/settings/modules/FaultTreeSettings.h @@ -0,0 +1,104 @@ +#pragma once + +#include "storm/settings/modules/ModuleSettings.h" +#include "storm-dft/builder/DftExplorationHeuristic.h" +#include "storm-config.h" + +namespace storm { + namespace settings { + namespace modules { + + /*! + * This class represents the settings for DFT model checking. + */ + class FaultTreeSettings : public ModuleSettings { + public: + + /*! + * Creates a new set of DFT settings. + */ + FaultTreeSettings(); + + /*! + * Retrieves whether the option to use symmetry reduction is set. + * + * @return True iff the option was set. + */ + bool useSymmetryReduction() const; + + /*! + * Retrieves whether the option to use modularisation is set. + * + * @return True iff the option was set. + */ + bool useModularisation() const; + + /*! + * Retrieves whether the option to disable Dont Care propagation is set. + * + * @return True iff the option was set. + */ + bool isDisableDC() const; + + /*! + * Retrieves whether the option to compute an approximation is set. + * + * @return True iff the option was set. + */ + bool isApproximationErrorSet() const; + + /*! + * Retrieves the relative error allowed for approximating the model checking result. + * + * @return The allowed errorbound. + */ + double getApproximationError() const; + + /*! + * Retrieves the heuristic used for approximation. + * + * @return The heuristic to use. + */ + storm::builder::ApproximationHeuristic getApproximationHeuristic() const; + + /*! + * Retrieves whether the non-determinism should be avoided by always taking the first possible dependency. + * + * @return True iff the option was set. + */ + bool isTakeFirstDependency() const; + +#ifdef STORM_HAVE_Z3 + /*! + * Retrieves whether the DFT should be checked via SMT. + * + * @return True iff the option was set. + */ + bool solveWithSMT() const; +#endif + + bool check() const override; + void finalize() override; + + // The name of the module. + static const std::string moduleName; + + private: + // Define the string names of the options as constants. + static const std::string symmetryReductionOptionName; + static const std::string symmetryReductionOptionShortName; + static const std::string modularisationOptionName; + static const std::string disableDCOptionName; + static const std::string approximationErrorOptionName; + static const std::string approximationErrorOptionShortName; + static const std::string approximationHeuristicOptionName; + static const std::string firstDependencyOptionName; +#ifdef STORM_HAVE_Z3 + static const std::string solveWithSmtOptionName; +#endif + + }; + + } // namespace modules + } // namespace settings +} // namespace storm diff --git a/src/storm-pars-cli/CMakeLists.txt b/src/storm-pars-cli/CMakeLists.txt index bda5ad6c2..9e2f6f315 100644 --- a/src/storm-pars-cli/CMakeLists.txt +++ b/src/storm-pars-cli/CMakeLists.txt @@ -1,6 +1,6 @@ # Create storm-pars. add_executable(storm-pars-cli ${PROJECT_SOURCE_DIR}/src/storm-pars-cli/storm-pars.cpp) -target_link_libraries(storm-pars-cli storm-pars) # Adding headers for xcode +target_link_libraries(storm-pars-cli storm-pars storm-cli-utilities) # Adding headers for xcode set_target_properties(storm-pars-cli PROPERTIES OUTPUT_NAME "storm-pars") add_dependencies(binaries storm-pars-cli) diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 5fa744c59..907688ef4 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -7,6 +7,7 @@ #include "storm/settings/SettingsManager.h" #include "storm/api/storm.h" #include "storm-cli-utilities/cli.h" +#include "storm-cli-utilities/model-handling.h" #include "storm/models/ModelBase.h" #include "storm/storage/SymbolicModelDescription.h" #include "storm/utility/file.h" @@ -23,8 +24,6 @@ #include "storm/exceptions/InvalidSettingsException.h" #include "storm/exceptions/NotSupportedException.h" -#include "storm-cli-utilities/cli.cpp" - namespace storm { namespace pars { diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp index 485aa8a64..ca79ccfac 100644 --- a/src/storm/models/sparse/MarkovAutomaton.cpp +++ b/src/storm/models/sparse/MarkovAutomaton.cpp @@ -50,7 +50,9 @@ namespace storm { if (components.exitRates) { exitRates = std::move(components.exitRates.get()); - } else { + } + + if (components.rateTransitions) { this->turnRatesToProbabilities(); } closed = this->checkIsClosed(); @@ -150,7 +152,7 @@ namespace storm { uint_fast64_t row = this->getTransitionMatrix().getRowGroupIndices()[state]; if (this->markovianStates.get(state)) { if (assertRates) { - STORM_LOG_THROW(this->exitRates[state] == this->getTransitionMatrix().getRowSum(row), storm::exceptions::InvalidArgumentException, "The specified exit rate is inconsistent with the rate matrix. Difference is " << (this->exitRates[state] - this->getTransitionMatrix().getRowSum(row)) << "."); + STORM_LOG_THROW(this->exitRates[state] == this->getTransitionMatrix().getRowSum(row), storm::exceptions::InvalidArgumentException, "The specified exit rate is inconsistent with the rate matrix. Difference is " << (this->exitRates[state] - this->getTransitionMatrix().getRowSum(row)) << "."); } else { this->exitRates.push_back(this->getTransitionMatrix().getRowSum(row)); } @@ -159,7 +161,11 @@ namespace storm { } ++row; } else { - this->exitRates.push_back(storm::utility::zero()); + if (assertRates) { + STORM_LOG_THROW(storm::utility::isZero(this->exitRates[state]), storm::exceptions::InvalidArgumentException, "The specified exit rate for (non-Markovian) choice should be 0."); + } else { + this->exitRates.push_back(storm::utility::zero()); + } } for (; row < this->getTransitionMatrix().getRowGroupIndices()[state+1]; ++row) { STORM_LOG_THROW(storm::utility::isOne(this->getTransitionMatrix().getRowSum(row)), storm::exceptions::InvalidArgumentException, "Entries of transition matrix do not sum up to one for (non-Markovian) choice " << row << " of state " << state << " (sum is " << this->getTransitionMatrix().getRowSum(row) << ")."); diff --git a/src/storm/models/sparse/MarkovAutomaton.h b/src/storm/models/sparse/MarkovAutomaton.h index 249766b62..89c73f83c 100644 --- a/src/storm/models/sparse/MarkovAutomaton.h +++ b/src/storm/models/sparse/MarkovAutomaton.h @@ -22,7 +22,7 @@ namespace storm { * For hybrid states (i.e., states with Markovian and probabilistic transitions), it is assumed that the first * choice corresponds to the markovian transitions. * - * @param transitionMatrix The matrix representing the transitions in the model in terms of rates (markocian choices) and probabilities (probabilistic choices). + * @param transitionMatrix The matrix representing the transitions in the model in terms of rates (Markovian choices) and probabilities (probabilistic choices). * @param stateLabeling The labeling of the states. * @param markovianStates A bit vector indicating the Markovian states of the automaton (i.e., states with at least one markovian transition). * @param rewardModels A mapping of reward model names to reward models. @@ -38,7 +38,7 @@ namespace storm { * For hybrid states (i.e., states with Markovian and probabilistic transitions), it is assumed that the first * choice corresponds to the markovian transitions. * - * @param transitionMatrix The matrix representing the transitions in the model in terms of rates (markocian choices) and probabilities (probabilistic choices). + * @param transitionMatrix The matrix representing the transitions in the model in terms of rates (Markovian choices) and probabilities (probabilistic choices). * @param stateLabeling The labeling of the states. * @param markovianStates A bit vector indicating the Markovian states of the automaton (i.e., states with at least one markovian transition). * @param rewardModels A mapping of reward model names to reward models. diff --git a/src/storm/parser/ExpressionParser.cpp b/src/storm/parser/ExpressionParser.cpp index cd3ccd595..519bc2b9f 100644 --- a/src/storm/parser/ExpressionParser.cpp +++ b/src/storm/parser/ExpressionParser.cpp @@ -197,7 +197,7 @@ namespace storm { try { // Start parsing. bool succeeded = qi::phrase_parse(iter, last, *this, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result); - STORM_LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Could not parse expression."); + STORM_LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Could not parse expression '" << expressionString << "'."); STORM_LOG_DEBUG("Parsed expression successfully."); } catch (qi::expectation_failure const& e) { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, e.what_);