diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp index 0f0aa68fa..6b032534e 100644 --- a/src/storm-dft-cli/storm-dyftee.cpp +++ b/src/storm-dft-cli/storm-dyftee.cpp @@ -20,7 +20,7 @@ #include "storm-dft/modelchecker/dft/DFTModelChecker.h" #include "storm-dft/modelchecker/dft/DFTASFChecker.h" #include "storm-dft/transformations/DftToGspnTransformator.h" - +#include "storm-dft/storage/dft/DftJsonExporter.h" #include "storm-dft/settings/modules/DFTSettings.h" @@ -34,27 +34,44 @@ #include /*! - * Load DFT from filename, build corresponding Model and check against given property. + * Analyse the given DFT according to the given properties. + * We first load the DFT from the given file, then build the corresponding model and last check against the given properties. * - * @param filename Path to DFT file in Galileo format. - * @param property PCTC formula capturing the property to check. + * @param properties PCTL formulas capturing the properties to check. * @param symred Flag whether symmetry reduction should be used. * @param allowModularisation Flag whether modularisation should be applied if possible. * @param enableDC Flag whether Don't Care propagation should be used. + * @param approximationError Allowed approximation error. */ template -void analyzeDFT(std::string filename, std::string property, bool symred, bool allowModularisation, bool enableDC, double approximationError) { - std::cout << "Running DFT analysis on file " << filename << " with property " << property << std::endl; +void analyzeDFT(std::vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) { + storm::settings::modules::DFTSettings const& dftSettings = storm::settings::getModule(); + std::shared_ptr> dft; - storm::parser::DFTGalileoParser parser; - storm::storage::DFT dft = parser.parseDFT(filename); - std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForExplicit(property)); - STORM_LOG_ASSERT(formulas.size() == 1, "Wrong number of formulas."); + // Build DFT from given file. + if (dftSettings.isDftJsonFileSet()) { + storm::parser::DFTJsonParser parser; + std::cout << "Loading DFT from file " << dftSettings.getDftJsonFilename() << std::endl; + dft = std::make_shared>(parser.parseJson(dftSettings.getDftJsonFilename())); + } else { + storm::parser::DFTGalileoParser parser; + std::cout << "Loading DFT from file " << dftSettings.getDftFilename() << std::endl; + dft = std::make_shared>(parser.parseDFT(dftSettings.getDftFilename())); + } + // Build properties + std::string propString = properties[0]; + for (size_t i = 1; i < properties.size(); ++i) { + propString += ";" + properties[i]; + } + std::vector> props = storm::extractFormulasFromProperties(storm::parsePropertiesForExplicit(propString)); + STORM_LOG_ASSERT(props.size() > 0, "No properties found."); + + // Check model storm::modelchecker::DFTModelChecker modelChecker; - modelChecker.check(dft, formulas[0], symred, allowModularisation, enableDC, approximationError); + modelChecker.check(*dft, props, symred, allowModularisation, enableDC, approximationError); modelChecker.printTimings(); - modelChecker.printResult(); + modelChecker.printResults(); } /*! @@ -133,6 +150,16 @@ int main(const int argc, const char** argv) { 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."); + storm::parser::DFTGalileoParser parser; + storm::storage::DFT dft = parser.parseDFT(dftSettings.getDftFilename()); + // Export to json + storm::storage::DftJsonExporter::toFile(dft, dftSettings.getExportJsonFilename()); + storm::utility::cleanUp(); + return 0; + } + if (dftSettings.isTransformToGspn()) { std::shared_ptr> dft; @@ -194,43 +221,42 @@ int main(const int argc, const char** argv) { #endif // Set min or max - bool minimal = true; + 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."); - minimal = false; + optimizationDirection = "max"; } - // Construct pctlFormula - std::string pctlFormula = ""; - std::string operatorType = ""; - std::string targetFormula = ""; + // Construct properties to check for + std::vector properties; if (ioSettings.isPropertySet()) { - STORM_LOG_THROW(!dftSettings.usePropExpectedTime() && !dftSettings.usePropProbability() && !dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given."); - pctlFormula = ioSettings.getProperty(); - } else if (dftSettings.usePropExpectedTime()) { - STORM_LOG_THROW(!dftSettings.usePropProbability() && !dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given."); - operatorType = "T"; - targetFormula = "F \"failed\""; - } else if (dftSettings.usePropProbability()) { - STORM_LOG_THROW(!dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given."); - operatorType = "P";; - targetFormula = "F \"failed\""; - } else { - STORM_LOG_THROW(dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "No property given."); + properties.push_back(ioSettings.getProperty()); + } + if (dftSettings.usePropExpectedTime()) { + properties.push_back("T" + optimizationDirection + "=? [F \"failed\"]"); + } + if (dftSettings.usePropProbability()) { + properties.push_back("P" + optimizationDirection + "=? [F \"failed\"]"); + } + if (dftSettings.usePropTimebound()) { std::stringstream stream; - stream << "F<=" << dftSettings.getPropTimebound() << " \"failed\""; - operatorType = "P"; - targetFormula = stream.str(); + stream << "P" << optimizationDirection << "=? [F<=" << dftSettings.getPropTimebound() << " \"failed\"]"; + properties.push_back(stream.str()); } - - if (!targetFormula.empty()) { - STORM_LOG_ASSERT(pctlFormula.empty(), "Pctl formula not empty."); - pctlFormula = operatorType + (minimal ? "min" : "max") + "=?[" + targetFormula + "]"; + if (dftSettings.usePropTimepoints()) { + for (double timepoint : dftSettings.getPropTimepoints()) { + std::stringstream stream; + stream << "P" << optimizationDirection << "=? [F<=" << timepoint << " \"failed\"]"; + properties.push_back(stream.str()); + } + } + + if (properties.empty()) { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No property given."); } - - STORM_LOG_ASSERT(!pctlFormula.empty(), "Pctl formula empty."); + // Set possible approximation error double approximationError = 0.0; if (dftSettings.isApproximationErrorSet()) { approximationError = dftSettings.getApproximationError(); @@ -239,12 +265,12 @@ int main(const int argc, const char** argv) { // From this point on we are ready to carry out the actual computations. if (parametric) { #ifdef STORM_HAVE_CARL - analyzeDFT(dftSettings.getDftFilename(), pctlFormula, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError); + analyzeDFT(properties, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError); #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameters are not supported in this build."); #endif } else { - analyzeDFT(dftSettings.getDftFilename(), pctlFormula, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError); + analyzeDFT(properties, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError); } // All operations have now been performed, so we clean up everything and terminate. diff --git a/src/storm-dft/CMakeLists.txt b/src/storm-dft/CMakeLists.txt index 16fa40e48..3951551ae 100644 --- a/src/storm-dft/CMakeLists.txt +++ b/src/storm-dft/CMakeLists.txt @@ -10,7 +10,31 @@ file(GLOB_RECURSE STORM_DFT_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-dft/*/*.h) # Create storm-pgcl. add_library(storm-dft SHARED ${STORM_DFT_SOURCES} ${STORM_DFT_HEADERS}) -target_link_libraries(storm-dft storm storm-gspn ${STORM_DFT_LINK_LIBRARIES}) + +# Remove define symbol for shared libstorm. +set_target_properties(storm-dft PROPERTIES DEFINE_SYMBOL "") +#add_dependencies(storm resources) +list(APPEND STORM_TARGETS storm-dft) +set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) + +target_link_libraries(storm-dft PUBLIC storm storm-gspn ${STORM_DFT_LINK_LIBRARIES}) + +# Install storm headers to include directory. +foreach(HEADER ${STORM_DFT_HEADERS}) + string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER}) + string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH}) + string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH}) + add_custom_command( + OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} + COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY} + COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} + DEPENDS ${HEADER} + ) + list(APPEND STORM_DFT_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}") +endforeach() +add_custom_target(copy_storm_dft_headers DEPENDS ${STORM_DFT_OUTPUT_HEADERS} ${STORM_DFT_HEADERS}) +add_dependencies(storm-dft copy_storm_dft_headers) # installation install(TARGETS storm-dft RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) + diff --git a/src/storm-dft/builder/DftExplorationHeuristic.h b/src/storm-dft/builder/DftExplorationHeuristic.h index 874cfb586..f4cc3c1ce 100644 --- a/src/storm-dft/builder/DftExplorationHeuristic.h +++ b/src/storm-dft/builder/DftExplorationHeuristic.h @@ -107,8 +107,8 @@ namespace storm { } bool updateHeuristicValues(DFTExplorationHeuristic const& predecessor, ValueType, ValueType) override { - if (predecessor.getDepth() < this->depth) { - this->depth = predecessor.getDepth(); + if (predecessor.getDepth() + 1 < this->depth) { + this->depth = predecessor.getDepth() + 1; return true; } return false; diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.h b/src/storm-dft/builder/ExplicitDFTModelBuilder.h index d3d191a8a..d61043368 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.h +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.h @@ -60,7 +60,7 @@ namespace storm { storm::storage::BitVectorHashMap mStates; std::vector> mPseudoStatesMapping; // vector of (id to concrete state, bitvector) size_t newIndex = 0; - bool mergeFailedStates = true; + bool mergeFailedStates = false; bool enableDC = true; size_t failedIndex = 0; size_t initialStateIndex = 0; diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp index 194372a30..84eaa21a7 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp @@ -9,7 +9,7 @@ #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" @@ -27,6 +27,29 @@ namespace storm { 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), @@ -42,7 +65,7 @@ namespace storm { { // Intentionally left empty. // TODO Matthias: remove again - usedHeuristic = storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE; + usedHeuristic = storm::builder::ApproximationHeuristic::DEPTH; // Compute independent subtrees if (dft.topLevelType() == storm::storage::DFTElementType::OR) { @@ -154,7 +177,7 @@ namespace storm { approximationThreshold = dft.nrElements()+10; break; case storm::builder::ApproximationHeuristic::DEPTH: - approximationThreshold = iteration; + approximationThreshold = iteration + 1; break; case storm::builder::ApproximationHeuristic::PROBABILITY: case storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE: @@ -169,7 +192,7 @@ namespace storm { 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.stateRemapping[initialStateIndex] == initialStateIndex, "Initial state should not be remapped."); + 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(); @@ -230,7 +253,7 @@ namespace storm { StateType skippedIndex = nrExpandedStates; std::map> skippedStatesNew; for (size_t id = 0; id < matrixBuilder.stateRemapping.size(); ++id) { - StateType index = matrixBuilder.stateRemapping[id]; + StateType index = matrixBuilder.getRemapping(id); auto itFind = skippedStates.find(index); if (itFind != skippedStates.end()) { // Set new mapping for skipped state @@ -326,8 +349,8 @@ namespace storm { // Try to explore the next state generator.load(currentState); - if (approximationThreshold > 0.0 && nrExpandedStates > approximationThreshold && !currentExplorationHeuristic->isExpand()) { - //if (currentExplorationHeuristic->isSkip(approximationThreshold)) { + //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)); @@ -374,6 +397,7 @@ namespace storm { 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); @@ -405,6 +429,7 @@ namespace storm { 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) { @@ -414,34 +439,37 @@ namespace storm { modelComponents.stateLabeling.addLabel("failsafe"); } - // Collect labels for all BE - std::vector>> basicElements = dft.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"); } } // Set labels to states - if(mergeFailedStates) { + if (mergeFailedStates) { modelComponents.stateLabeling.addLabelToState("failed", failedStateId); } for (auto const& stateIdPair : stateStorage.stateToId) { storm::storage::BitVector state = stateIdPair.first; - size_t stateId = stateIdPair.second; + 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 BE - for (std::shared_ptr> elem : basicElements) { - if (labelOpts.beLabels.count(elem->name()) > 0 && storm::storage::DFTState::hasFailed(state, stateGenerationInfo->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 @@ -451,10 +479,70 @@ namespace storm { } template - std::shared_ptr> ExplicitDFTModelBuilderApprox::getModelApproximation(bool lowerBound) { - // TODO Matthias: handle case with no skipped states - changeMatrixBound(modelComponents.transitionMatrix, lowerBound); - return createModel(true); + 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); + + std::shared_ptr> ma = std::make_shared>(std::move(matrix), std::move(labeling), modelComponents.markovianStates, modelComponents.exitRates); + 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 @@ -498,8 +586,6 @@ namespace storm { } } - STORM_LOG_DEBUG("No. states: " << model->getNumberOfStates()); - STORM_LOG_DEBUG("No. transitions: " << model->getNumberOfTransitions()); if (model->getNumberOfStates() <= 15) { STORM_LOG_TRACE("Transition matrix: " << std::endl << model->getTransitionMatrix()); } else { @@ -545,6 +631,10 @@ namespace storm { 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(); @@ -562,6 +652,10 @@ namespace storm { 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); } diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h index 52bcbf2c9..97439f47a 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h +++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h @@ -29,7 +29,7 @@ namespace storm { using DFTStatePointer = std::shared_ptr>; // TODO Matthias: make choosable - using ExplorationHeuristic = DFTExplorationHeuristicBoundDifference; + using ExplorationHeuristic = DFTExplorationHeuristicDepth; using ExplorationHeuristicPointer = std::shared_ptr; @@ -116,6 +116,18 @@ namespace storm { 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; @@ -141,9 +153,20 @@ namespace storm { 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; }; /*! @@ -174,11 +197,12 @@ namespace storm { /*! * 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 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 = true); + std::shared_ptr> getModelApproximation(bool lowerBound, bool expectedTime); private: @@ -220,14 +244,16 @@ namespace storm { /** * 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. + * @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; @@ -235,6 +261,8 @@ namespace storm { /*! * Get upper bound approximation for state. * + * @param state The state. + * * @return Upper bound approximation. */ ValueType getUpperBound(DFTStatePointer const& state) const; @@ -315,7 +343,6 @@ namespace storm { // A priority queue of states that still need to be explored. storm::storage::BucketPriorityQueue explorationQueue; - //storm::storage::DynamicPriorityQueue, std::function> explorationQueue; // A mapping of not yet explored states from the id to the tuple (state object, heuristic values). std::map> statesNotExplored; diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index 3f1361f93..7b86d1faa 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -3,6 +3,8 @@ #include "storm/utility/constants.h" #include "storm/utility/macros.h" #include "storm/exceptions/NotImplementedException.h" +#include "storm/settings/SettingsManager.h" +#include "storm-dft/settings/modules/DFTSettings.h" namespace storm { namespace generator { @@ -43,7 +45,7 @@ namespace storm { template StateBehavior DftNextStateGenerator::expand(StateToIdCallback const& stateToIdCallback) { - STORM_LOG_TRACE("Explore state: " << mDft.getStateString(state)); + STORM_LOG_DEBUG("Explore state: " << mDft.getStateString(state)); // Prepare the result, in case we return early. StateBehavior result; @@ -52,10 +54,10 @@ namespace storm { bool hasDependencies = state->nrFailableDependencies() > 0; size_t failableCount = hasDependencies ? state->nrFailableDependencies() : state->nrFailableBEs(); size_t currentFailable = 0; - Choice choice(0, !hasDependencies); // Check for absorbing state if (mDft.hasFailed(state) || mDft.isFailsafe(state) || failableCount == 0) { + Choice choice(0, true); // Add self loop choice.addProbability(state->getId(), storm::utility::one()); STORM_LOG_TRACE("Added self loop for " << state->getId()); @@ -65,8 +67,14 @@ namespace storm { return result; } + Choice choice(0, !hasDependencies); + // Let BE fail while (currentFailable < failableCount) { + if (storm::settings::getModule().isTakeFirstDependency() && hasDependencies && currentFailable > 0) { + // We discard further exploration as we already chose one dependent event + break; + } STORM_LOG_ASSERT(!mDft.hasFailed(state), "Dft has failed."); // Construct new state as copy from original one @@ -104,7 +112,7 @@ namespace storm { newState->updateFailableDependencies(next->id()); } - if(newState->isInvalid()) { + if(newState->isInvalid() || (nextBE->isTransient() && !newState->hasFailed(mDft.getTopLevelIndex()))) { // Continue with next possible state ++currentFailable; continue; diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 8ca775432..79ed0ef95 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -2,6 +2,7 @@ #include "storm/builder/ParallelCompositionBuilder.h" #include "storm/utility/bitoperations.h" +#include "storm/utility/DirectEncodingExporter.h" #include "storm-dft/builder/ExplicitDFTModelBuilder.h" #include "storm-dft/builder/ExplicitDFTModelBuilderApprox.h" @@ -13,12 +14,7 @@ namespace storm { namespace modelchecker { template - DFTModelChecker::DFTModelChecker() { - checkResult = storm::utility::zero(); - } - - template - void DFTModelChecker::check(storm::storage::DFT const& origDft, std::shared_ptr const& formula, bool symred, bool allowModularisation, bool enableDC, double approximationError) { + void DFTModelChecker::check(storm::storage::DFT const& origDft, std::vector> const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) { // Initialize this->approximationError = approximationError; totalTimer.start(); @@ -29,31 +25,31 @@ namespace storm { // TODO Matthias: check that all paths reach the target state for approximation // Checking DFT - if (formula->isProbabilityOperatorFormula() || !allowModularisation) { - checkResult = checkHelper(dft, formula, symred, allowModularisation, enableDC, approximationError); - } else { - std::shared_ptr> model = buildModelComposition(dft, formula, symred, allowModularisation, enableDC); + if (properties[0]->isTimeOperatorFormula() && allowModularisation) { + // Use parallel composition as modularisation approach for expected time + std::shared_ptr> model = buildModelViaComposition(dft, properties, symred, true, enableDC, approximationError); // Model checking - std::unique_ptr result = checkModel(model, formula); - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); - checkResult = result->asExplicitQuantitativeCheckResult().getValueMap().begin()->second; + std::vector resultsValue = checkModel(model, properties); + for (ValueType result : resultsValue) { + checkResults.push_back(result); + } + } else { + checkResults = checkHelper(dft, properties, symred, allowModularisation, enableDC, approximationError); } totalTimer.stop(); } template - typename DFTModelChecker::dft_result DFTModelChecker::checkHelper(storm::storage::DFT const& dft, std::shared_ptr const& formula, bool symred, bool allowModularisation, bool enableDC, double approximationError) { + typename DFTModelChecker::dft_results DFTModelChecker::checkHelper(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) { STORM_LOG_TRACE("Check helper called"); - bool modularisationPossible = allowModularisation; + std::vector> dfts; + bool invResults = false; + size_t nrK = 0; // K out of M + size_t nrM = 0; // K out of M // Try modularisation - if(modularisationPossible) { - bool invResults = false; - std::vector> dfts; - size_t nrK = 0; // K out of M - size_t nrM = 0; // K out of M - + if(allowModularisation) { switch (dft.topLevelType()) { case storm::storage::DFTElementType::AND: STORM_LOG_TRACE("top modularisation called AND"); @@ -61,7 +57,6 @@ namespace storm { STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules."); nrK = dfts.size(); nrM = dfts.size(); - modularisationPossible = dfts.size() > 1; break; case storm::storage::DFTElementType::OR: STORM_LOG_TRACE("top modularisation called OR"); @@ -70,7 +65,6 @@ namespace storm { nrK = 0; nrM = dfts.size(); invResults = true; - modularisationPossible = dfts.size() > 1; break; case storm::storage::DFTElementType::VOT: STORM_LOG_TRACE("top modularisation called VOT"); @@ -82,22 +76,29 @@ namespace storm { nrK -= 1; invResults = true; } - modularisationPossible = dfts.size() > 1; break; default: // No static gate -> no modularisation applicable - modularisationPossible = false; break; } + } - if(modularisationPossible) { - STORM_LOG_TRACE("Recursive CHECK Call"); - if (formula->isProbabilityOperatorFormula()) { + // Perform modularisation + if(dfts.size() > 1) { + STORM_LOG_TRACE("Recursive CHECK Call"); + // TODO Matthias: compute simultaneously + dft_results results; + for (auto property : properties) { + if (!property->isProbabilityOperatorFormula()) { + STORM_LOG_WARN("Could not check property: " << *property); + } else { // Recursively call model checking std::vector res; for(auto const ft : dfts) { - dft_result ftResult = checkHelper(ft, formula, symred, true, enableDC, 0.0); - res.push_back(boost::get(ftResult)); + // TODO Matthias: allow approximation in modularisation + dft_results ftResults = checkHelper(ft, {property}, symred, true, enableDC, 0.0); + STORM_LOG_ASSERT(ftResults.size() == 1, "Wrong number of results"); + res.push_back(boost::get(ftResults[0])); } // Combine modularisation results @@ -128,149 +129,134 @@ namespace storm { if(invResults) { result = storm::utility::one() - result; } - return result; + results.push_back(result); } } + return results; + } else { + // No modularisation was possible + return checkDFT(dft, properties, symred, enableDC, approximationError); } - - // If we are here, no modularisation was possible - STORM_LOG_ASSERT(!modularisationPossible, "Modularisation should not be possible."); - return checkDFT(dft, formula, symred, enableDC, approximationError); } template - std::shared_ptr> DFTModelChecker::buildModelComposition(storm::storage::DFT const& dft, std::shared_ptr const& formula, bool symred, bool allowModularisation, bool enableDC) { + std::shared_ptr> DFTModelChecker::buildModelViaComposition(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) { + // TODO Matthias: use approximation? STORM_LOG_TRACE("Build model via composition"); - // Use parallel composition for CTMCs for expected time - STORM_LOG_ASSERT(formula->isTimeOperatorFormula(), "Formula is not a time operator formula"); - bool modularisationPossible = allowModularisation; + std::vector> dfts; + bool isAnd = true; // Try modularisation - if(modularisationPossible) { - std::vector> dfts; - bool isAnd = true; - + if(allowModularisation) { switch (dft.topLevelType()) { case storm::storage::DFTElementType::AND: STORM_LOG_TRACE("top modularisation called AND"); dfts = dft.topModularisation(); STORM_LOG_TRACE("Modularisation into " << dfts.size() << " submodules."); - modularisationPossible = dfts.size() > 1; isAnd = true; break; case storm::storage::DFTElementType::OR: STORM_LOG_TRACE("top modularisation called OR"); dfts = dft.topModularisation(); STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules."); - modularisationPossible = dfts.size() > 1; isAnd = false; break; case storm::storage::DFTElementType::VOT: - /*STORM_LOG_TRACE("top modularisation called VOT"); - dfts = dft.topModularisation(); - STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules."); - std::static_pointer_cast const>(dft.getTopLevelGate())->threshold(); - */ // TODO enable modularisation for voting gate - modularisationPossible = false; break; default: // No static gate -> no modularisation applicable - modularisationPossible = false; break; } + } - if(modularisationPossible) { - STORM_LOG_TRACE("Recursive CHECK Call"); - bool firstTime = true; - std::shared_ptr> composedModel; - for (auto const ft : dfts) { - STORM_LOG_INFO("Building Model via parallel composition..."); - explorationTimer.start(); + // Perform modularisation via parallel composition + if(dfts.size() > 1) { + STORM_LOG_TRACE("Recursive CHECK Call"); + bool firstTime = true; + std::shared_ptr> composedModel; + for (auto const ft : dfts) { + STORM_LOG_INFO("Building Model via parallel composition..."); + explorationTimer.start(); + + // Find symmetries + std::map>> emptySymmetry; + storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); + if(symred) { + auto colouring = ft.colourDFT(); + symmetries = ft.findSymmetries(colouring); + STORM_LOG_INFO("Found " << symmetries.groups.size() << " symmetries."); + STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries); + } - // Find symmetries - std::map>> emptySymmetry; - storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); - if(symred) { - auto colouring = ft.colourDFT(); - symmetries = ft.findSymmetries(colouring); - STORM_LOG_INFO("Found " << symmetries.groups.size() << " symmetries."); - STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries); - } + // Build a single CTMC + STORM_LOG_INFO("Building Model..."); + storm::builder::ExplicitDFTModelBuilderApprox builder(ft, symmetries, enableDC); + typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions(properties); + builder.buildModel(labeloptions, 0, 0.0); + std::shared_ptr> model = builder.getModel(); + explorationTimer.stop(); - // Build a single CTMC - STORM_LOG_INFO("Building Model..."); - storm::builder::ExplicitDFTModelBuilderApprox builder(ft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions; // TODO initialize this with the formula - builder.buildModel(labeloptions, 0, 0.0); - std::shared_ptr> model = builder.getModel(); - //model->printModelInformationToStream(std::cout); - STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates()); - STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions()); - explorationTimer.stop(); - - STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs"); - std::shared_ptr> ctmc = model->template as>(); - - ctmc = storm::performDeterministicSparseBisimulationMinimization>(ctmc, {formula}, storm::storage::BisimulationType::Weak)->template as>(); - - if (firstTime) { - composedModel = ctmc; - firstTime = false; - } else { - composedModel = storm::builder::ParallelCompositionBuilder::compose(composedModel, ctmc, isAnd); - } + STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs"); + std::shared_ptr> ctmc = model->template as>(); - // Apply bisimulation - bisimulationTimer.start(); - composedModel = storm::performDeterministicSparseBisimulationMinimization>(composedModel, {formula}, storm::storage::BisimulationType::Weak)->template as>(); - std::chrono::high_resolution_clock::time_point bisimulationEnd = std::chrono::high_resolution_clock::now(); - bisimulationTimer.stop(); - - STORM_LOG_INFO("No. states (Composed): " << composedModel->getNumberOfStates()); - STORM_LOG_INFO("No. transitions (Composed): " << composedModel->getNumberOfTransitions()); - if (composedModel->getNumberOfStates() <= 15) { - STORM_LOG_TRACE("Transition matrix: " << std::endl << composedModel->getTransitionMatrix()); - } else { - STORM_LOG_TRACE("Transition matrix: too big to print"); - } + // Apply bisimulation to new CTMC + bisimulationTimer.start(); + ctmc = storm::performDeterministicSparseBisimulationMinimization>(ctmc, properties, storm::storage::BisimulationType::Weak)->template as>(); + bisimulationTimer.stop(); + if (firstTime) { + composedModel = ctmc; + firstTime = false; + } else { + composedModel = storm::builder::ParallelCompositionBuilder::compose(composedModel, ctmc, isAnd); } - return composedModel; - } - } - // If we are here, no composition was possible - STORM_LOG_ASSERT(!modularisationPossible, "Modularisation should not be possible."); - explorationTimer.start(); - // Find symmetries - std::map>> emptySymmetry; - storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); - if(symred) { - auto colouring = dft.colourDFT(); - symmetries = dft.findSymmetries(colouring); - STORM_LOG_INFO("Found " << symmetries.groups.size() << " symmetries."); - STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries); - } - // Build a single CTMC - STORM_LOG_INFO("Building Model..."); + // Apply bisimulation to parallel composition + bisimulationTimer.start(); + composedModel = storm::performDeterministicSparseBisimulationMinimization>(composedModel, properties, storm::storage::BisimulationType::Weak)->template as>(); + bisimulationTimer.stop(); + + STORM_LOG_DEBUG("No. states (Composed): " << composedModel->getNumberOfStates()); + STORM_LOG_DEBUG("No. transitions (Composed): " << composedModel->getNumberOfTransitions()); + if (composedModel->getNumberOfStates() <= 15) { + STORM_LOG_TRACE("Transition matrix: " << std::endl << composedModel->getTransitionMatrix()); + } else { + STORM_LOG_TRACE("Transition matrix: too big to print"); + } + } + composedModel->printModelInformationToStream(std::cout); + return composedModel; + } else { + // No composition was possible + explorationTimer.start(); + // Find symmetries + std::map>> emptySymmetry; + storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); + if(symred) { + auto colouring = dft.colourDFT(); + symmetries = dft.findSymmetries(colouring); + STORM_LOG_INFO("Found " << symmetries.groups.size() << " symmetries."); + STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries); + } + // Build a single CTMC + STORM_LOG_INFO("Building Model..."); - storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions; // TODO initialize this with the formula - builder.buildModel(labeloptions, 0, 0.0); - std::shared_ptr> model = builder.getModel(); - //model->printModelInformationToStream(std::cout); - STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates()); - STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions()); - explorationTimer.stop(); - STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs"); - return model->template as>(); + storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); + typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions(properties); + builder.buildModel(labeloptions, 0, 0.0); + std::shared_ptr> model = builder.getModel(); + model->printModelInformationToStream(std::cout); + explorationTimer.stop(); + STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs"); + return model->template as>(); + } } template - typename DFTModelChecker::dft_result DFTModelChecker::checkDFT(storm::storage::DFT const& dft, std::shared_ptr const& formula, bool symred, bool enableDC, double approximationError) { + typename DFTModelChecker::dft_results DFTModelChecker::checkDFT(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool enableDC, double approximationError) { explorationTimer.start(); // Find symmetries @@ -289,11 +275,18 @@ namespace storm { // Build approximate Markov Automata for lower and upper bound 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; // TODO initialize this with the formula + typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions(properties); - bool probabilityFormula = formula->isProbabilityOperatorFormula(); - STORM_LOG_ASSERT((formula->isTimeOperatorFormula() && !probabilityFormula) || (!formula->isTimeOperatorFormula() && probabilityFormula), "Probability formula not initialized correctly"); + // TODO Matthias: compute approximation for all properties simultaneously? + std::shared_ptr property = properties[0]; + if (properties.size() > 1) { + STORM_LOG_WARN("Computing approximation only for first property: " << *property); + } + + bool probabilityFormula = property->isProbabilityOperatorFormula(); + STORM_LOG_ASSERT((property->isTimeOperatorFormula() && !probabilityFormula) || (!property->isTimeOperatorFormula() && probabilityFormula), "Probability formula not initialized correctly"); size_t iteration = 0; do { // Iteratively build finer models @@ -310,32 +303,30 @@ namespace storm { // Build model for lower bound STORM_LOG_INFO("Getting model for lower bound..."); - model = builder.getModelApproximation(probabilityFormula ? false : true); + model = builder.getModelApproximation(true, !probabilityFormula); // We only output the info from the lower bound as the info for the upper bound is the same - STORM_LOG_INFO("No. states: " << model->getNumberOfStates()); - STORM_LOG_INFO("No. transitions: " << model->getNumberOfTransitions()); + model->printModelInformationToStream(std::cout); buildingTimer.stop(); - // Check lower bound - std::unique_ptr result = checkModel(model, formula); - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); - ValueType newResult = result->asExplicitQuantitativeCheckResult().getValueMap().begin()->second; - STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(newResult, approxResult.first), "New under-approximation " << newResult << " is smaller than old result " << approxResult.first); - approxResult.first = newResult; + // Check lower bounds + newResult = checkModel(model, {property}); + STORM_LOG_ASSERT(newResult.size() == 1, "Wrong size for result vector."); + STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(newResult[0], approxResult.first), "New under-approximation " << newResult[0] << " is smaller than old result " << approxResult.first); + approxResult.first = newResult[0]; // Build model for upper bound STORM_LOG_INFO("Getting model for upper bound..."); buildingTimer.start(); - model = builder.getModelApproximation(probabilityFormula ? true : false); + model = builder.getModelApproximation(false, !probabilityFormula); buildingTimer.stop(); // Check upper bound - result = checkModel(model, formula); - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); - newResult = result->asExplicitQuantitativeCheckResult().getValueMap().begin()->second; - STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(approxResult.second, newResult), "New over-approximation " << newResult << " is greater than old result " << approxResult.second); - approxResult.second = newResult; + newResult = checkModel(model, {property}); + STORM_LOG_ASSERT(newResult.size() == 1, "Wrong size for result vector."); + STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(approxResult.second, newResult[0]), "New over-approximation " << newResult[0] << " is greater than old result " << approxResult.second); + approxResult.second = newResult[0]; ++iteration; + STORM_LOG_ASSERT(comparator.isLess(approxResult.first, approxResult.second) || comparator.isEqual(approxResult.first, approxResult.second), "Under-approximation " << approxResult.first << " is greater than over-approximation " << approxResult.second); STORM_LOG_INFO("Result after iteration " << iteration << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")"); totalTimer.stop(); printTimings(); @@ -344,7 +335,9 @@ namespace storm { } while (!isApproximationSufficient(approxResult.first, approxResult.second, approximationError, probabilityFormula)); STORM_LOG_INFO("Finished approximation after " << iteration << " iteration" << (iteration > 1 ? "s." : ".")); - return approxResult; + dft_results results; + results.push_back(approxResult); + return results; } else { // Build a single Markov Automaton STORM_LOG_INFO("Building Model..."); @@ -352,46 +345,72 @@ namespace storm { // 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; // TODO initialize this with the formula + 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; // TODO initialize this with the formula + typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions; model = builder.buildModel(labeloptions); } - //model->printModelInformationToStream(std::cout); - STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates()); - STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions()); + model->printModelInformationToStream(std::cout); explorationTimer.stop(); + // Export the model if required + if (storm::settings::getModule().isExportExplicitSet()) { + std::ofstream stream; + storm::utility::openFile(storm::settings::getModule().getExportExplicitFilename(), stream); + std::vector parameterNames; + // TODO fill parameter names + storm::exporter::explicitExportSparseModel(stream, model, parameterNames); + storm::utility::closeFile(stream); + } + // Model checking - std::unique_ptr result = checkModel(model, formula); - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); - return result->asExplicitQuantitativeCheckResult().getValueMap().begin()->second; + std::vector resultsValue = checkModel(model, properties); + dft_results results; + for (ValueType result : resultsValue) { + results.push_back(result); + } + return results; } } template - std::unique_ptr DFTModelChecker::checkModel(std::shared_ptr>& model, std::shared_ptr const& formula) { + std::vector DFTModelChecker::checkModel(std::shared_ptr>& model, property_vector const& properties) { // Bisimulation - bisimulationTimer.start(); if (model->isOfType(storm::models::ModelType::Ctmc) && storm::settings::getModule().isBisimulationSet()) { + bisimulationTimer.start(); STORM_LOG_INFO("Bisimulation..."); - model = storm::performDeterministicSparseBisimulationMinimization>(model->template as>(), {formula}, storm::storage::BisimulationType::Weak)->template as>(); + model = storm::performDeterministicSparseBisimulationMinimization>(model->template as>(), properties, storm::storage::BisimulationType::Weak)->template as>(); STORM_LOG_INFO("No. states (Bisimulation): " << model->getNumberOfStates()); STORM_LOG_INFO("No. transitions (Bisimulation): " << model->getNumberOfTransitions()); + bisimulationTimer.stop(); } - bisimulationTimer.stop(); - modelCheckingTimer.start(); // Check the model STORM_LOG_INFO("Model checking..."); - std::unique_ptr result(storm::verifySparseModel(model, formula)); - STORM_LOG_INFO("Model checking done."); - STORM_LOG_ASSERT(result, "Result does not exist."); + modelCheckingTimer.start(); + std::vector results; + + // Check each property + storm::utility::Stopwatch singleModelCheckingTimer; + for (auto property : properties) { + singleModelCheckingTimer.reset(); + singleModelCheckingTimer.start(); + STORM_PRINT_AND_LOG("Model checking property " << *property << " ..." << std::endl); + std::unique_ptr result(storm::verifySparseModel(model, property, true)); + STORM_LOG_ASSERT(result, "Result does not exist."); + result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); + ValueType resultValue = result->asExplicitQuantitativeCheckResult().getValueMap().begin()->second; + STORM_PRINT_AND_LOG("Result (initial states): " << resultValue << std::endl); + results.push_back(resultValue); + singleModelCheckingTimer.stop(); + STORM_PRINT_AND_LOG("Time for model checking: " << singleModelCheckingTimer << "." << std::endl); + } modelCheckingTimer.stop(); - return result; + STORM_LOG_INFO("Model checking done."); + return results; } template @@ -412,21 +431,30 @@ namespace storm { template void DFTModelChecker::printTimings(std::ostream& os) { os << "Times:" << std::endl; - os << "Exploration:\t" << explorationTimer.getTimeInSeconds() << "s" << std::endl; - os << "Building:\t" << buildingTimer.getTimeInSeconds() << "s" << std::endl; - os << "Bisimulation:\t" << bisimulationTimer.getTimeInSeconds() << "s" << std::endl; - os << "Modelchecking:\t" << modelCheckingTimer.getTimeInSeconds() << "s" << std::endl; - os << "Total:\t\t" << totalTimer.getTimeInSeconds() << "s" << std::endl; + os << "Exploration:\t" << explorationTimer << std::endl; + os << "Building:\t" << buildingTimer << std::endl; + os << "Bisimulation:\t" << bisimulationTimer<< std::endl; + os << "Modelchecking:\t" << modelCheckingTimer << std::endl; + os << "Total:\t\t" << totalTimer << std::endl; } template - void DFTModelChecker::printResult(std::ostream& os) { + void DFTModelChecker::printResults(std::ostream& os) { + bool first = true; os << "Result: ["; - if (this->approximationError > 0.0) { - approximation_result result = boost::get(checkResult); - os << "(" << result.first << ", " << result.second << ")"; - } else { - os << boost::get(checkResult); + for (auto result : checkResults) { + if (!first) { + os << ", "; + } + if (this->approximationError > 0.0) { + approximation_result resultApprox = boost::get(result); + os << "(" << resultApprox.first << ", " << resultApprox.second << ")"; + } else { + os << boost::get(result); + } + if (first) { + first = false; + } } os << "]" << std::endl; } diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.h b/src/storm-dft/modelchecker/dft/DFTModelChecker.h index c714999a8..f67fe125e 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.h @@ -18,26 +18,28 @@ namespace storm { class DFTModelChecker { typedef std::pair approximation_result; - typedef boost::variant dft_result; + typedef std::vector> dft_results; + typedef std::vector> property_vector; public: /*! * Constructor. */ - DFTModelChecker(); + DFTModelChecker() { + } /*! * Main method for checking DFTs. * * @param origDft Original DFT - * @param formula Formula to check for + * @param properties Properties to check for * @param symred Flag indicating if symmetry reduction should be used * @param allowModularisation Flag indication if modularisation is allowed * @param enableDC Flag indicating if dont care propagation should be used * @param approximationError Error allowed for approximation. Value 0 indicates no approximation */ - void check(storm::storage::DFT const& origDft, std::shared_ptr const& formula, bool symred = true, bool allowModularisation = true, bool enableDC = true, double approximationError = 0.0); + void check(storm::storage::DFT const& origDft, property_vector const& properties, bool symred = true, bool allowModularisation = true, bool enableDC = true, double approximationError = 0.0); /*! * Print timings of all operations to stream. @@ -51,7 +53,7 @@ namespace storm { * * @param os Output stream to write to. */ - void printResult(std::ostream& os = std::cout); + void printResults(std::ostream& os = std::cout); private: @@ -62,8 +64,8 @@ namespace storm { storm::utility::Stopwatch modelCheckingTimer; storm::utility::Stopwatch totalTimer; - // Model checking result - dft_result checkResult; + // Model checking results + dft_results checkResults; // Allowed error bound for approximation double approximationError; @@ -72,21 +74,21 @@ namespace storm { * Internal helper for model checking a DFT. * * @param dft DFT - * @param formula Formula to check for + * @param properties Properties to check for * @param symred Flag indicating if symmetry reduction should be used * @param allowModularisation Flag indication if modularisation is allowed * @param enableDC Flag indicating if dont care propagation should be used * @param approximationError Error allowed for approximation. Value 0 indicates no approximation * - * @return Model checking result (or in case of approximation two results for lower and upper bound) + * @return Model checking results (or in case of approximation two results for lower and upper bound) */ - dft_result checkHelper(storm::storage::DFT const& dft, std::shared_ptr const& formula, bool symred, bool allowModularisation, bool enableDC, double approximationError); + dft_results checkHelper(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError); /*! * Internal helper for building a CTMC from a DFT via parallel composition. * * @param dft DFT - * @param formula Formula to check for + * @param properties Properties to check for * @param symred Flag indicating if symmetry reduction should be used * @param allowModularisation Flag indication if modularisation is allowed * @param enableDC Flag indicating if dont care propagation should be used @@ -94,30 +96,30 @@ namespace storm { * * @return CTMC representing the DFT */ - std::shared_ptr> buildModelComposition(storm::storage::DFT const& dft, std::shared_ptr const& formula, bool symred, bool allowModularisation, bool enableDC); + std::shared_ptr> buildModelViaComposition(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError); /*! * Check model generated from DFT. * * @param dft The DFT - * @param formula Formula to check for + * @param properties Properties to check for * @param symred Flag indicating if symmetry reduction should be used * @param enableDC Flag indicating if dont care propagation should be used * @param approximationError Error allowed for approximation. Value 0 indicates no approximation * * @return Model checking result */ - dft_result checkDFT(storm::storage::DFT const& dft, std::shared_ptr const& formula, bool symred, bool enableDC, double approximationError = 0.0); + dft_results checkDFT(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool enableDC, double approximationError = 0.0); /*! - * Check the given markov model for the given property. + * Check the given markov model for the given properties. * - * @param model Model to check - * @param formula Formula to check for + * @param model Model to check + * @param properties Properties to check for * * @return Model checking result */ - std::unique_ptr checkModel(std::shared_ptr>& model, std::shared_ptr const& formula); + std::vector checkModel(std::shared_ptr>& model, property_vector const& properties); /*! * Checks if the computed approximation is sufficient, i.e. diff --git a/src/storm-dft/parser/DFTGalileoParser.cpp b/src/storm-dft/parser/DFTGalileoParser.cpp index c5a88716c..c81c2767a 100644 --- a/src/storm-dft/parser/DFTGalileoParser.cpp +++ b/src/storm-dft/parser/DFTGalileoParser.cpp @@ -5,7 +5,6 @@ #include #include #include -#include "storm/storage/expressions/ExpressionManager.h" #include "storm/exceptions/NotImplementedException.h" #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/NotSupportedException.h" @@ -125,7 +124,7 @@ namespace storm { } else if (boost::starts_with(tokens[1], "lambda=")) { ValueType failureRate = parseRationalExpression(tokens[1].substr(7)); ValueType dormancyFactor = parseRationalExpression(tokens[2].substr(5)); - success = builder.addBasicElement(name, failureRate, dormancyFactor); + success = builder.addBasicElement(name, failureRate, dormancyFactor, false); // TODO set transient BEs } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Type name: " << tokens[1] << " not recognized."); success = false; diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp index faff4a099..0d6f312f2 100644 --- a/src/storm-dft/parser/DFTJsonParser.cpp +++ b/src/storm-dft/parser/DFTJsonParser.cpp @@ -5,7 +5,6 @@ #include #include #include -#include "storm/storage/expressions/ExpressionManager.h" #include "storm/exceptions/NotImplementedException.h" #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/NotSupportedException.h" @@ -25,27 +24,11 @@ namespace storm { } template - std::string DFTJsonParser::stripQuotsFromName(std::string const& name) { - size_t firstQuots = name.find("\""); - size_t secondQuots = name.find("\"", firstQuots+1); - - if(firstQuots == std::string::npos) { - return name; - } else { - STORM_LOG_THROW(secondQuots != std::string::npos, storm::exceptions::FileIoException, "No ending quotation mark found in " << name); - return name.substr(firstQuots+1,secondQuots-1); - } - } - - template - std::string DFTJsonParser::getString(json const& structure, std::string const& errorInfo) { - STORM_LOG_THROW(structure.is_string(), storm::exceptions::FileIoException, "Expected a string in " << errorInfo << ", got '" << structure.dump() << "'"); - return structure.front(); - } - - template - std::string DFTJsonParser::parseNodeIdentifier(std::string const& name) { - return boost::replace_all_copy(name, "'", "__prime__"); + std::string DFTJsonParser::generateUniqueName(std::string const& id, std::string const& name) { + std::string newId = name; + std::replace(newId.begin(), newId.end(), ' ', '_'); + std::replace(newId.begin(), newId.end(), '-', '_'); + return newId + "_" + id; } template @@ -58,40 +41,49 @@ namespace storm { parsedJson << file; storm::utility::closeFile(file); - // Start by building mapping from ids to names - std::map nameMapping; - for (auto& element: parsedJson) { - if (element.at("classes") != "") { - json data = element.at("data"); - std::string id = data.at("id"); - std::string name = data.at("name"); - nameMapping[id] = name; - } + json parameters = parsedJson.at("parameters"); +#ifdef STORM_HAVE_CARL + for (auto it = parameters.begin(); it != parameters.end(); ++it) { + STORM_LOG_THROW((std::is_same::value), storm::exceptions::NotSupportedException, "Parameters only allowed when using rational functions."); + std::string parameter = it.key(); + storm::expressions::Variable var = manager->declareRationalVariable(parameter); + identifierMapping.emplace(var.getName(), var); + parser.setIdentifierMapping(identifierMapping); + STORM_LOG_TRACE("Added parameter: " << var.getName()); } +#endif - // TODO: avoid hack - std::string toplevelId = nameMapping["1"]; + json nodes = parsedJson.at("nodes"); - for (auto& element : parsedJson) { + // Start by building mapping from ids to their unique names + std::map nameMapping; + for (auto& element: nodes) { + json data = element.at("data"); + std::string id = data.at("id"); + nameMapping[id] = generateUniqueName(id, data.at("name")); + } + + for (auto& element : nodes) { + STORM_LOG_TRACE("Parsing: " << element); bool success = true; - if (element.at("classes") == "") { - continue; - } json data = element.at("data"); - std::string name = data.at("name"); + std::string name = generateUniqueName(data.at("id"), data.at("name")); std::vector childNames; if (data.count("children") > 0) { - for (auto& child : data.at("children")) { + for (std::string const& child : data.at("children")) { childNames.push_back(nameMapping[child]); } } - std::string type = getString(element.at("classes"), "classes"); + std::string type = data.at("type"); if(type == "and") { success = builder.addAndElement(name, childNames); } else if (type == "or") { success = builder.addOrElement(name, childNames); + } else if (type == "vot") { + std::string votThreshold = data.at("voting"); + success = builder.addVotElement(name, boost::lexical_cast(votThreshold), childNames); } else if (type == "pand") { success = builder.addPandElement(name, childNames); } else if (type == "por") { @@ -108,21 +100,31 @@ namespace storm { } else if (type == "be") { ValueType failureRate = parseRationalExpression(data.at("rate")); ValueType dormancyFactor = parseRationalExpression(data.at("dorm")); - success = builder.addBasicElement(name, failureRate, dormancyFactor); + bool transient = false; + if (data.count("transient") > 0) { + transient = data.at("transient"); + } + success = builder.addBasicElement(name, failureRate, dormancyFactor, transient); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Type name: " << type << " not recognized."); success = false; } - // Set layout positions - json position = element.at("position"); - double x = position.at("x"); - double y = position.at("y"); - builder.addLayoutInfo(name, x / 7, y / 7); + // Do not set layout for dependencies + // This does not work because dependencies might be splitted + // TODO: do splitting later in rewriting step + if (type != "fdep" && type != "pdep") { + // Set layout positions + json position = element.at("position"); + double x = position.at("x"); + double y = position.at("y"); + builder.addLayoutInfo(name, x / 7, y / 7); + } STORM_LOG_THROW(success, storm::exceptions::FileIoException, "Error while adding element '" << element << "'."); } - if(!builder.setTopLevel(toplevelId)) { + std::string toplevelName = nameMapping[parsedJson.at("toplevel")]; + if(!builder.setTopLevel(toplevelName)) { STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Top level id unknown."); } } diff --git a/src/storm-dft/parser/DFTJsonParser.h b/src/storm-dft/parser/DFTJsonParser.h index cf2e83826..d23baf58e 100644 --- a/src/storm-dft/parser/DFTJsonParser.h +++ b/src/storm-dft/parser/DFTJsonParser.h @@ -38,9 +38,7 @@ namespace storm { private: void readFile(std::string const& filename); - std::string stripQuotsFromName(std::string const& name); - std::string parseNodeIdentifier(std::string const& name); - std::string getString(json const& structure, std::string const& errorInfo); + std::string generateUniqueName(std::string const& id, std::string const& name); ValueType parseRationalExpression(std::string const& expr); }; diff --git a/src/storm-dft/settings/modules/DFTSettings.cpp b/src/storm-dft/settings/modules/DFTSettings.cpp index cf9160bd1..1a8d59d70 100644 --- a/src/storm-dft/settings/modules/DFTSettings.cpp +++ b/src/storm-dft/settings/modules/DFTSettings.cpp @@ -29,10 +29,13 @@ namespace storm { 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::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 @@ -45,19 +48,22 @@ namespace storm { 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, 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(); } @@ -117,13 +123,28 @@ namespace storm { } bool DFTSettings::usePropTimebound() const { - return this->getOption(propTimeBoundOptionName).getHasOptionBeenSet(); + return this->getOption(propTimeboundOptionName).getHasOptionBeenSet(); } - + double DFTSettings::getPropTimebound() const { - return this->getOption(propTimeBoundOptionName).getArgumentByName("time").getValueAsDouble(); + 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(); } @@ -132,6 +153,10 @@ namespace storm { 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(); @@ -142,17 +167,18 @@ namespace storm { 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 only one property is given. - if (usePropExpectedTime()) { - STORM_LOG_THROW(!usePropProbability() && !usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given."); - } else if (usePropProbability()) { - STORM_LOG_THROW(!usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given."); - } - // 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; diff --git a/src/storm-dft/settings/modules/DFTSettings.h b/src/storm-dft/settings/modules/DFTSettings.h index c1a9df7e5..c04ef1a23 100644 --- a/src/storm-dft/settings/modules/DFTSettings.h +++ b/src/storm-dft/settings/modules/DFTSettings.h @@ -110,7 +110,28 @@ namespace storm { * @return True iff the option was set. */ bool usePropTimebound() const; - + + /*! + * Retrieves the timebound for the timebound property. + * + * @return The timebound. + */ + double getPropTimebound() const; + + /*! + * Retrieves whether the property timepoints should be used. + * + * @return True iff the option was set. + */ + bool usePropTimepoints() const; + + /*! + * Retrieves the settings for the timepoints property. + * + * @return The timepoints. + */ + std::vector getPropTimepoints() const; + /*! * Retrieves whether the minimal value should be computed for non-determinism. * @@ -124,13 +145,13 @@ namespace storm { * @return True iff the option was set. */ bool isComputeMaximalValue() const; - + /*! - * Retrieves the timebound for the timebound property. + * Retrieves whether the non-determinism should be avoided by always taking the first possible dependency. * - * @return The timebound. + * @return True iff the option was set. */ - double getPropTimebound() const; + bool isTakeFirstDependency() const; /*! * Retrieves whether the DFT should be transformed into a GSPN. @@ -138,6 +159,20 @@ namespace storm { * @return True iff the option was set. */ bool isTransformToGspn() const; + + /*! + * Retrieves whether the export to Json file option was set. + * + * @return True if the export to json file option was set. + */ + bool isExportToJson() const; + + /*! + * Retrieves the name of the json file to export to. + * + * @return The name of the json file to export to. + */ + std::string getExportJsonFilename() const; #ifdef STORM_HAVE_Z3 /*! @@ -170,13 +205,16 @@ namespace storm { static const std::string propExpectedTimeOptionName; static const std::string propExpectedTimeOptionShortName; static const std::string propProbabilityOptionName; - static const std::string propTimeBoundOptionName; + static const std::string propTimeboundOptionName; + 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/storage/BucketPriorityQueue.h b/src/storm-dft/storage/BucketPriorityQueue.h index a332311a7..004469f9a 100644 --- a/src/storm-dft/storage/BucketPriorityQueue.h +++ b/src/storm-dft/storage/BucketPriorityQueue.h @@ -13,7 +13,7 @@ namespace storm { template class BucketPriorityQueue { - using HeuristicPointer = std::shared_ptr>; + using HeuristicPointer = std::shared_ptr>; public: explicit BucketPriorityQueue(size_t nrBuckets, double lowerValue, double ratio); diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index e38c40ce1..b21338c74 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -651,58 +651,70 @@ namespace storm { storm::utility::iota_n(std::back_inserter(vec), nrElements(), 0); BijectionCandidates completeCategories = colouring.colourSubdft(vec); std::map>> res; - + + // Find symmetries for gates for(auto const& colourClass : completeCategories.gateCandidates) { - if(colourClass.second.size() > 1) { - std::set foundEqClassFor; - for(auto it1 = colourClass.second.cbegin(); it1 != colourClass.second.cend(); ++it1) { - std::vector> symClass; - if(foundEqClassFor.count(*it1) > 0) { - // This item is already in a class. - continue; - } - if(!getGate(*it1)->hasOnlyStaticParents()) { - continue; - } - - std::pair, std::vector> influencedElem1Ids = getSortedParentAndOutDepIds(*it1); - auto it2 = it1; - for(++it2; it2 != colourClass.second.cend(); ++it2) { - if(!getGate(*it2)->hasOnlyStaticParents()) { - continue; - } - std::vector sortedParent2Ids = getGate(*it2)->parentIds(); - std::sort(sortedParent2Ids.begin(), sortedParent2Ids.end()); - - if(influencedElem1Ids == getSortedParentAndOutDepIds(*it2)) { - std::map bijection = findBijection(*it1, *it2, colouring, true); - if (!bijection.empty()) { - STORM_LOG_TRACE("Subdfts are symmetric"); - foundEqClassFor.insert(*it2); - if(symClass.empty()) { - for(auto const& i : bijection) { - symClass.push_back(std::vector({i.first})); - } - } - auto symClassIt = symClass.begin(); - for(auto const& i : bijection) { - symClassIt->emplace_back(i.second); - ++symClassIt; - - } + findSymmetriesHelper(colourClass.second, colouring, res); + } + + // Find symmetries for BEs + for(auto const& colourClass : completeCategories.beCandidates) { + findSymmetriesHelper(colourClass.second, colouring, res); + } + + return DFTIndependentSymmetries(res); + } + + template + void DFT::findSymmetriesHelper(std::vector const& candidates, DFTColouring const& colouring, std::map>>& result) const { + if(candidates.size() <= 0) { + return; + } + + std::set foundEqClassFor; + for(auto it1 = candidates.cbegin(); it1 != candidates.cend(); ++it1) { + std::vector> symClass; + if(foundEqClassFor.count(*it1) > 0) { + // This item is already in a class. + continue; + } + if(!getElement(*it1)->hasOnlyStaticParents()) { + continue; + } + + std::tuple, std::vector, std::vector> influencedElem1Ids = getSortedParentAndDependencyIds(*it1); + auto it2 = it1; + for(++it2; it2 != candidates.cend(); ++it2) { + if(!getElement(*it2)->hasOnlyStaticParents()) { + continue; + } + + if(influencedElem1Ids == getSortedParentAndDependencyIds(*it2)) { + std::map bijection = findBijection(*it1, *it2, colouring, true); + if (!bijection.empty()) { + STORM_LOG_TRACE("Subdfts are symmetric"); + foundEqClassFor.insert(*it2); + if(symClass.empty()) { + for(auto const& i : bijection) { + symClass.push_back(std::vector({i.first})); } } - } - if(!symClass.empty()) { - res.emplace(*it1, symClass); + auto symClassIt = symClass.begin(); + for(auto const& i : bijection) { + symClassIt->emplace_back(i.second); + ++symClassIt; + + } } } - + } + + if(!symClass.empty()) { + result.emplace(*it1, symClass); } } - return DFTIndependentSymmetries(res); } - + template std::vector DFT::findModularisationRewrite() const { for(auto const& e : mElements) { @@ -734,15 +746,25 @@ namespace storm { template - std::pair, std::vector> DFT::getSortedParentAndOutDepIds(size_t index) const { - std::pair, std::vector> res; - res.first = getElement(index)->parentIds(); - std::sort(res.first.begin(), res.first.end()); + std::tuple, std::vector, std::vector> DFT::getSortedParentAndDependencyIds(size_t index) const { + // Parents + std::vector parents = getElement(index)->parentIds(); + std::sort(parents.begin(), parents.end()); + // Ingoing dependencies + std::vector ingoingDeps; + if (isBasicElement(index)) { + for(auto const& dep : getBasicElement(index)->ingoingDependencies()) { + ingoingDeps.push_back(dep->id()); + } + std::sort(ingoingDeps.begin(), ingoingDeps.end()); + } + // Outgoing dependencies + std::vector outgoingDeps; for(auto const& dep : getElement(index)->outgoingDependencies()) { - res.second.push_back(dep->id()); + outgoingDeps.push_back(dep->id()); } - std::sort(res.second.begin(), res.second.end()); - return res; + std::sort(outgoingDeps.begin(), outgoingDeps.end()); + return std::make_tuple(parents, ingoingDeps, outgoingDeps); } // Explicitly instantiate the class. diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h index 1304bbfa9..304018d97 100644 --- a/src/storm-dft/storage/dft/DFT.h +++ b/src/storm-dft/storage/dft/DFT.h @@ -261,6 +261,8 @@ namespace storm { DFTIndependentSymmetries findSymmetries(DFTColouring const& colouring) const; + void findSymmetriesHelper(std::vector const& candidates, DFTColouring const& colouring, std::map>>& result) const; + std::vector immediateFailureCauses(size_t index) const; std::vector findModularisationRewrite() const; @@ -274,7 +276,7 @@ namespace storm { } private: - std::pair, std::vector> getSortedParentAndOutDepIds(size_t index) const; + std::tuple, std::vector, std::vector> getSortedParentAndDependencyIds(size_t index) const; bool elementIndicesCorrect() const { for(size_t i = 0; i < mElements.size(); ++i) { diff --git a/src/storm-dft/storage/dft/DFTBuilder.cpp b/src/storm-dft/storage/dft/DFTBuilder.cpp index 974ffac8a..88abc9665 100644 --- a/src/storm-dft/storage/dft/DFTBuilder.cpp +++ b/src/storm-dft/storage/dft/DFTBuilder.cpp @@ -46,7 +46,7 @@ namespace storm { auto itFind = mElements.find(childName); STORM_LOG_ASSERT(itFind != mElements.end(), "Child not found."); DFTElementPointer childElement = itFind->second; - STORM_LOG_ASSERT(!childElement->isDependency() && !childElement->isRestriction(), "Child has invalid type."); + STORM_LOG_ASSERT(!childElement->isDependency() && !childElement->isRestriction(), "Child '" << childElement->name() << "' has invalid type."); elem.first->pushBackChild(childElement); childElement->addRestriction(elem.first); } @@ -60,6 +60,7 @@ namespace storm { STORM_LOG_ASSERT(itFind != mElements.end(), "Child '" << childName << "' not found"); DFTElementPointer childElement = itFind->second; if (!first) { + STORM_LOG_ASSERT(childElement->isBasicElement(), "Child '" << childName << "' of dependency '" << elem.first->name() << "' must be BE."); dependencies.push_back(std::static_pointer_cast>(childElement)); } else { elem.first->setTriggerElement(std::static_pointer_cast>(childElement)); @@ -159,7 +160,7 @@ namespace storm { template bool DFTBuilder::addStandardGate(std::string const& name, std::vector const& children, DFTElementType tp) { - STORM_LOG_ASSERT(children.size() > 0, "No child."); + STORM_LOG_ASSERT(children.size() > 0, "No child for " << name); if(mElements.count(name) != 0) { // Element with that name already exists. return false; @@ -271,7 +272,7 @@ namespace storm { if (be->canFail()) { dormancyFactor = be->passiveFailureRate() / be->activeFailureRate(); } - addBasicElement(be->name(), be->activeFailureRate(), dormancyFactor); + addBasicElement(be->name(), be->activeFailureRate(), dormancyFactor, be->isTransient()); break; } case DFTElementType::CONSTF: diff --git a/src/storm-dft/storage/dft/DFTBuilder.h b/src/storm-dft/storage/dft/DFTBuilder.h index 636b5e5a1..42713e601 100644 --- a/src/storm-dft/storage/dft/DFTBuilder.h +++ b/src/storm-dft/storage/dft/DFTBuilder.h @@ -103,9 +103,9 @@ namespace storm { //TODO Matthias: collect constraints for SMT solving //0 <= probability <= 1 if (binaryDependencies && !storm::utility::isOne(probability) && children.size() > 2) { - // Introduce additional element for first capturing the proabilistic dependency + // Introduce additional element for first capturing the probabilistic dependency std::string nameAdditional = name + "_additional"; - addBasicElement(nameAdditional, storm::utility::zero(), storm::utility::zero()); + addBasicElement(nameAdditional, storm::utility::zero(), storm::utility::zero(), false); // First consider probabilistic dependency addDepElement(name + "_pdep", {children.front(), nameAdditional}, probability); // Then consider dependencies to the children if probabilistic dependency failed @@ -168,12 +168,12 @@ namespace storm { return true; } - bool addBasicElement(std::string const& name, ValueType failureRate, ValueType dormancyFactor) { + bool addBasicElement(std::string const& name, ValueType failureRate, ValueType dormancyFactor, bool transient = false) { //TODO Matthias: collect constraints for SMT solving //failureRate > 0 //0 <= dormancyFactor <= 1 - mElements[name] = std::make_shared>(mNextId++, name, failureRate, dormancyFactor); + mElements[name] = std::make_shared>(mNextId++, name, failureRate, dormancyFactor, transient); return true; } diff --git a/src/storm-dft/storage/dft/DFTElementType.h b/src/storm-dft/storage/dft/DFTElementType.h index 800da161f..1527efe25 100644 --- a/src/storm-dft/storage/dft/DFTElementType.h +++ b/src/storm-dft/storage/dft/DFTElementType.h @@ -75,7 +75,7 @@ namespace storm { } inline std::ostream& operator<<(std::ostream& os, DFTElementType const& tp) { - return os << toString(tp) << std::endl; + return os << toString(tp); } diff --git a/src/storm-dft/storage/dft/DFTIsomorphism.h b/src/storm-dft/storage/dft/DFTIsomorphism.h index 081b76f0b..869cbd065 100644 --- a/src/storm-dft/storage/dft/DFTIsomorphism.h +++ b/src/storm-dft/storage/dft/DFTIsomorphism.h @@ -249,7 +249,7 @@ namespace storage { protected: void colourize(std::shared_ptr> const& be) { - beColour[be->id()] = BEColourClass(be->activeFailureRate(), be->passiveFailureRate(), be->nrParents()); + beColour[be->id()] = BEColourClass(be->activeFailureRate(), be->passiveFailureRate(), be->nrParents()); } void colourize(std::shared_ptr> const& gate) { diff --git a/src/storm-dft/storage/dft/DFTState.cpp b/src/storm-dft/storage/dft/DFTState.cpp index ec6509944..29c1e525f 100644 --- a/src/storm-dft/storage/dft/DFTState.cpp +++ b/src/storm-dft/storage/dft/DFTState.cpp @@ -41,9 +41,9 @@ namespace storm { // Initialize currently failable BE if (mDft.isBasicElement(index) && isOperational(index)) { std::shared_ptr> be = mDft.getBasicElement(index); - if ((!be->isColdBasicElement() && be->canFail()) || !mDft.hasRepresentant(index) || isActive(mDft.getRepresentant(index))) { + if (be->canFail() && (!be->isColdBasicElement() || !mDft.hasRepresentant(index) || isActive(mDft.getRepresentant(index)))) { mCurrentlyFailableBE.push_back(index); - STORM_LOG_TRACE("Currently failable: " << mDft.getBasicElement(index)->toString()); + STORM_LOG_TRACE("Currently failable: " << be->toString()); } } else if (mDft.getElement(index)->isSpareGate()) { // Initialize used representants @@ -257,7 +257,7 @@ namespace storm { // Consider "normal" failure STORM_LOG_ASSERT(index < nrFailableBEs(), "Index invalid."); std::pair const>,bool> res(mDft.getBasicElement(mCurrentlyFailableBE[index]), false); - STORM_LOG_ASSERT(res.first->canFail(), "Element cannot fail."); + STORM_LOG_ASSERT(res.first->canFail(), "Element " << *(res.first) << " cannot fail."); mCurrentlyFailableBE.erase(mCurrentlyFailableBE.begin() + index); setFailed(res.first->id()); return res; diff --git a/src/storm-dft/storage/dft/DftJsonExporter.cpp b/src/storm-dft/storage/dft/DftJsonExporter.cpp new file mode 100644 index 000000000..bcafb35be --- /dev/null +++ b/src/storm-dft/storage/dft/DftJsonExporter.cpp @@ -0,0 +1,124 @@ +#include "DftJsonExporter.h" + +#include "storm/exceptions/NotImplementedException.h" +#include "storm/exceptions/FileIOException.h" + +#include +#include + +namespace storm { + namespace storage { + + template + size_t DftJsonExporter::currentId = 0; + + template + void DftJsonExporter::toFile(storm::storage::DFT const& dft, std::string const& filepath) { + std::ofstream ofs; + ofs.open(filepath, std::ofstream::out); + if(ofs.is_open()) { + toStream(dft, ofs); + ofs.close(); + } else { + STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Cannot open " << filepath); + } + } + + template + void DftJsonExporter::toStream(storm::storage::DFT const& dft, std::ostream& os) { + os << translate(dft).dump(4) << std::endl; + } + + template + modernjson::json DftJsonExporter::translate(storm::storage::DFT const& dft) { + modernjson::json jsonDft; + currentId = 0; + + // Nodes + modernjson::json jsonNodes; + for (size_t i = 0; i < dft.nrElements(); ++i) { + modernjson::json jsonNode = translateNode(dft.getElement(i)); + jsonDft.push_back(jsonNode); + } + + // Edges + modernjson::json jsonEdges; + for (size_t i = 0; i < dft.nrElements(); ++i) { + if (dft.isGate(i)) { + std::shared_ptr const> gate = dft.getGate(i); + for (size_t index = 0; index < gate->nrChildren(); ++index) { + DFTElementPointer child = gate->children()[index]; + modernjson::json jsonEdge = translateEdge(gate, child, index); + jsonDft.push_back(jsonEdge); + } + } + } + + return jsonDft; + } + + template + modernjson::json DftJsonExporter::translateNode(DFTElementCPointer const& element) { + modernjson::json nodeData; + nodeData["id"] = element->id(); + ++currentId; + STORM_LOG_ASSERT(element->id() == currentId-1, "Ids do not correspond"); + nodeData["name"] = element->name(); + + if (element->isGate()) { + // Set children for gate + std::shared_ptr const> gate = std::static_pointer_cast const>(element); + std::vector children; + for (DFTElementPointer const& child : gate->children()) { + children.push_back(child->id()); + } + nodeData["children"] = children; + } else if (element->isBasicElement()) { + // Set rates for BE + std::shared_ptr const> be = std::static_pointer_cast const>(element); + std::stringstream stream; + stream << be->activeFailureRate(); + nodeData["rate"] = stream.str(); + stream.clear(); + stream << (be->passiveFailureRate() / be->activeFailureRate()); + nodeData["dorm"] = stream.str(); + } + + modernjson::json jsonNode; + jsonNode["data"] = nodeData; + + jsonNode["group"] = "nodes"; + std::string type = storm::storage::toString(element->type()); + std::transform(type.begin(), type.end(), type.begin(), ::tolower); + jsonNode["classes"] = type; + return jsonNode; + } + + template + modernjson::json DftJsonExporter::translateEdge(std::shared_ptr const> const& gate, DFTElementCPointer const& child, size_t index) { + modernjson::json nodeData; + std::stringstream stream; + stream << gate->id() << "e" << child->id(); + nodeData["id"] = stream.str(); + ++currentId; + nodeData["source"] = gate->id(); + nodeData["target"] = child->id(); + nodeData["index"] = index; + + modernjson::json jsonNode; + jsonNode["data"] = nodeData; + + jsonNode["group"] = "edges"; + jsonNode["classes"] = ""; + return jsonNode; + } + + // Explicitly instantiate the class. + template class DftJsonExporter; + +#ifdef STORM_HAVE_CARL + template class DftJsonExporter; +#endif + + } +} diff --git a/src/storm-dft/storage/dft/DftJsonExporter.h b/src/storm-dft/storage/dft/DftJsonExporter.h new file mode 100644 index 000000000..ef04750ba --- /dev/null +++ b/src/storm-dft/storage/dft/DftJsonExporter.h @@ -0,0 +1,47 @@ +#pragma once + +#include "storm/utility/macros.h" + +#include "storm-dft/storage/dft/DFT.h" + +// JSON parser +#include "json.hpp" +namespace modernjson { + using json = nlohmann::basic_json; +} + +namespace storm { + namespace storage { + + /** + * Exports a DFT into the JSON format for visualizing it. + */ + template + class DftJsonExporter { + + using DFTElementPointer = std::shared_ptr>; + using DFTElementCPointer = std::shared_ptr const>; + using DFTGatePointer = std::shared_ptr>; + + public: + + static void toFile(storm::storage::DFT const& dft, std::string const& filepath); + + static void toStream(storm::storage::DFT const& dft, std::ostream& os); + + static modernjson::json translate(storm::storage::DFT const& dft); + + + private: + + static size_t currentId; + + static modernjson::json translateNode(DFTElementCPointer const& element); + + static modernjson::json translateEdge(std::shared_ptr const> const& gate, DFTElementCPointer const& child, size_t index); + + + }; + + } +} diff --git a/src/storm-dft/storage/dft/elements/DFTBE.h b/src/storm-dft/storage/dft/elements/DFTBE.h index 3be82d9f1..6bb234b4e 100644 --- a/src/storm-dft/storage/dft/elements/DFTBE.h +++ b/src/storm-dft/storage/dft/elements/DFTBE.h @@ -11,10 +11,11 @@ namespace storm { ValueType mActiveFailureRate; ValueType mPassiveFailureRate; DFTDependencyVector mIngoingDependencies; + bool mTransient; public: - DFTBE(size_t id, std::string const& name, ValueType failureRate, ValueType dormancyFactor) : - DFTElement(id, name), mActiveFailureRate(failureRate), mPassiveFailureRate(dormancyFactor * failureRate) + DFTBE(size_t id, std::string const& name, ValueType failureRate, ValueType dormancyFactor, bool transient = false) : + DFTElement(id, name), mActiveFailureRate(failureRate), mPassiveFailureRate(dormancyFactor * failureRate), mTransient(transient) {} DFTElementType type() const override { @@ -32,6 +33,10 @@ namespace storm { ValueType const& passiveFailureRate() const { return mPassiveFailureRate; } + + bool isTransient() const { + return mTransient; + } bool canFail() const { return !storm::utility::isZero(mActiveFailureRate); diff --git a/src/storm-gspn/CMakeLists.txt b/src/storm-gspn/CMakeLists.txt index 564b696bd..cf80ff6aa 100644 --- a/src/storm-gspn/CMakeLists.txt +++ b/src/storm-gspn/CMakeLists.txt @@ -10,7 +10,9 @@ file(GLOB_RECURSE STORM_GSPN_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-gspn/*/*.h) # Create storm-pgcl. add_library(storm-gspn SHARED ${STORM_GSPN_SOURCES} ${STORM_GSPN_HEADERS}) +list(APPEND STORM_TARGETS storm-gspn) +set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) target_link_libraries(storm-gspn storm ${STORM_GSPN_LINK_LIBRARIES}) # installation -install(TARGETS storm-gspn RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) \ No newline at end of file +install(TARGETS storm-gspn RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index 314afa700..dd8b9358b 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -294,7 +294,7 @@ namespace storm { } else { buildAndCheckSymbolicModel(model, properties, true); } - } else if (ioSettings.isExplicitSet()) { + } else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet()) { STORM_LOG_THROW(coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Only the sparse engine supports explicit model input."); // If the model is given in an explicit format, we parse the properties without allowing expressions @@ -303,9 +303,18 @@ namespace storm { if (ioSettings.isPropertySet()) { properties = storm::parsePropertiesForExplicit(ioSettings.getProperty(), propertyFilter); } - - buildAndCheckExplicitModel(properties, true); + + if (generalSettings.isParametricSet()) { +#ifdef STORM_HAVE_CARL + buildAndCheckExplicitModel(properties, true); +#else + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No parameters are supported in this build."); +#endif + } else { + buildAndCheckExplicitModel(properties, true); + } } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); } } diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h index 9d1052ca1..c4aa9895e 100644 --- a/src/storm/cli/entrypoints.h +++ b/src/storm/cli/entrypoints.h @@ -6,7 +6,7 @@ #include "storm/utility/storm.h" #include "storm/storage/SymbolicModelDescription.h" -#include "storm/utility/ExplicitExporter.h" +#include "storm/utility/DirectEncodingExporter.h" #include "storm/utility/Stopwatch.h" #include "storm/exceptions/NotImplementedException.h" @@ -401,10 +401,15 @@ namespace storm { void buildAndCheckExplicitModel(std::vector const& properties, bool onlyInitialStatesRelevant = false) { storm::settings::modules::IOSettings const& settings = storm::settings::getModule(); - STORM_LOG_THROW(settings.isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files."); + STORM_LOG_THROW(settings.isExplicitSet() || settings.isExplicitDRNSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files."); storm::utility::Stopwatch modelBuildingWatch(true); - std::shared_ptr model = buildExplicitModel(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? boost::optional(settings.getStateRewardsFilename()) : boost::none, settings.isTransitionRewardsSet() ? boost::optional(settings.getTransitionRewardsFilename()) : boost::none, settings.isChoiceLabelingSet() ? boost::optional(settings.getChoiceLabelingFilename()) : boost::none); + std::shared_ptr model; + if (settings.isExplicitSet()) { + model = buildExplicitModel(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? boost::optional(settings.getStateRewardsFilename()) : boost::none, settings.isTransitionRewardsSet() ? boost::optional(settings.getTransitionRewardsFilename()) : boost::none, settings.isChoiceLabelingSet() ? boost::optional(settings.getChoiceLabelingFilename()) : boost::none); + } else { + model = buildExplicitDRNModel(settings.getExplicitDRNFilename()); + } modelBuildingWatch.stop(); STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl); @@ -420,6 +425,35 @@ namespace storm { verifySparseModel(model->as>(), properties, onlyInitialStatesRelevant); } } + +#ifdef STORM_HAVE_CARL + template<> + void buildAndCheckExplicitModel(std::vector const& properties, bool onlyInitialStatesRelevant) { + storm::settings::modules::IOSettings const& settings = storm::settings::getModule(); + + STORM_LOG_THROW(settings.isExplicitSet() || settings.isExplicitDRNSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files."); + + storm::utility::Stopwatch modelBuildingWatch(true); + std::shared_ptr model; + STORM_LOG_THROW(!settings.isExplicitSet(), storm::exceptions::NotSupportedException, "Parametric explicit model files are not supported."); + model = buildExplicitDRNModel(settings.getExplicitDRNFilename()); + modelBuildingWatch.stop(); + STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl); + + // Preprocess the model if needed. + BRANCH_ON_MODELTYPE(model, model, storm::RationalFunction, storm::dd::DdType::CUDD, preprocessModel, extractFormulasFromProperties(properties)); + + // Print some information about the model. + model->printModelInformationToStream(std::cout); + + // Verify the model, if a formula was given. + if (!properties.empty()) { + STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidStateException, "Expected sparse model."); + verifySparseModel(model->as>(), properties, onlyInitialStatesRelevant); + } + } +#endif + } } diff --git a/src/storm/models/ModelType.cpp b/src/storm/models/ModelType.cpp index 5bb1a9b09..46bc06dc9 100644 --- a/src/storm/models/ModelType.cpp +++ b/src/storm/models/ModelType.cpp @@ -1,14 +1,46 @@ #include "storm/models/ModelType.h" +#include "storm/exceptions/InvalidTypeException.h" +#include "storm/utility/macros.h" + namespace storm { namespace models { + + ModelType getModelType(std::string const& type) { + if (type == "DTMC") { + return ModelType::Dtmc; + } else if (type == "CTMC") { + return ModelType::Ctmc; + }else if (type == "MDP") { + return ModelType::Mdp; + } else if (type == "Markov Automaton") { + return ModelType::MarkovAutomaton; + } else if (type == "S2PG") { + return ModelType::S2pg; + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Type " << type << "not known."); + } + } + std::ostream& operator<<(std::ostream& os, ModelType const& type) { switch (type) { - case ModelType::Dtmc: os << "DTMC"; break; - case ModelType::Ctmc: os << "CTMC"; break; - case ModelType::Mdp: os << "MDP"; break; - case ModelType::MarkovAutomaton: os << "Markov Automaton"; break; - case ModelType::S2pg: os << "S2PG"; break; + case ModelType::Dtmc: + os << "DTMC"; + break; + case ModelType::Ctmc: + os << "CTMC"; + break; + case ModelType::Mdp: + os << "MDP"; + break; + case ModelType::MarkovAutomaton: + os << "Markov Automaton"; + break; + case ModelType::S2pg: + os << "S2PG"; + break; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unknown model type."); } return os; } diff --git a/src/storm/models/ModelType.h b/src/storm/models/ModelType.h index 6fabee8a4..40d4da220 100644 --- a/src/storm/models/ModelType.h +++ b/src/storm/models/ModelType.h @@ -9,6 +9,8 @@ namespace storm { enum class ModelType { Dtmc, Ctmc, Mdp, MarkovAutomaton, S2pg }; + + ModelType getModelType(std::string const& type); std::ostream& operator<<(std::ostream& os, ModelType const& type); } diff --git a/src/storm/models/sparse/Ctmc.cpp b/src/storm/models/sparse/Ctmc.cpp index 884eb359d..a43aded44 100644 --- a/src/storm/models/sparse/Ctmc.cpp +++ b/src/storm/models/sparse/Ctmc.cpp @@ -35,7 +35,12 @@ namespace storm { std::vector const& Ctmc::getExitRateVector() const { return exitRates; } - + + template + std::vector& Ctmc::getExitRateVector() { + return exitRates; + } + template std::vector Ctmc::createExitRateVector(storm::storage::SparseMatrix const& rateMatrix) { std::vector exitRates(rateMatrix.getRowCount()); diff --git a/src/storm/models/sparse/Ctmc.h b/src/storm/models/sparse/Ctmc.h index 417a899a4..8bb1f37ed 100644 --- a/src/storm/models/sparse/Ctmc.h +++ b/src/storm/models/sparse/Ctmc.h @@ -65,7 +65,14 @@ namespace storm { * @return The exit rate vector. */ std::vector const& getExitRateVector() const; - + + /*! + * Retrieves the vector of exit rates of the model. + * + * @return The exit rate vector. + */ + std::vector& getExitRateVector(); + private: /*! * Computes the exit rate vector based on the given rate matrix. diff --git a/src/storm/models/sparse/StateLabeling.cpp b/src/storm/models/sparse/StateLabeling.cpp index df289d439..c88a5f07e 100644 --- a/src/storm/models/sparse/StateLabeling.cpp +++ b/src/storm/models/sparse/StateLabeling.cpp @@ -115,6 +115,23 @@ namespace storm { out << " * " << labelIndexPair.first << " -> " << this->labelings[labelIndexPair.second].getNumberOfSetBits() << " state(s)" << std::endl; } } + + void StateLabeling::printCompleteLabelingInformationToStream(std::ostream& out) const { + out << "Labels: \t" << this->getNumberOfLabels() << std::endl; + for (auto label : nameToLabelingIndexMap) { + out << "Label '" << label.first << "': "; + for (auto index : this->labelings[label.second]) { + out << index << " "; + } + out << std::endl; + } + } + + std::ostream& operator<<(std::ostream& out, StateLabeling const& labeling) { + labeling.printLabelingInformationToStream(out); + return out; + } + } } } diff --git a/src/storm/models/sparse/StateLabeling.h b/src/storm/models/sparse/StateLabeling.h index 330a4d8fe..f66ea86b4 100644 --- a/src/storm/models/sparse/StateLabeling.h +++ b/src/storm/models/sparse/StateLabeling.h @@ -152,7 +152,16 @@ namespace storm { * @param out The stream the information is to be printed to. */ void printLabelingInformationToStream(std::ostream& out) const; - + + /*! + * Prints the complete labeling to the specified stream. + * + * @param out The stream the information is to be printed to. + */ + void printCompleteLabelingInformationToStream(std::ostream& out) const; + + friend std::ostream& operator<<(std::ostream& out, StateLabeling const& labeling); + private: // The number of states for which this object can hold the labeling. uint_fast64_t stateCount; diff --git a/src/storm/parser/DirectEncodingParser.cpp b/src/storm/parser/DirectEncodingParser.cpp new file mode 100644 index 000000000..110c9ca32 --- /dev/null +++ b/src/storm/parser/DirectEncodingParser.cpp @@ -0,0 +1,229 @@ +#include "storm/parser/DirectEncodingParser.h" + +#include +#include + +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/models/sparse/Ctmc.h" + +#include "storm/exceptions/FileIoException.h" +#include "storm/exceptions/WrongFormatException.h" +#include "storm/exceptions/InvalidArgumentException.h" +#include "storm/exceptions/NotSupportedException.h" +#include "storm/settings/SettingsManager.h" + +#include "storm/adapters/CarlAdapter.h" +#include "storm/utility/constants.h" +#include "storm/utility/macros.h" +#include "storm/utility/file.h" + +namespace storm { + namespace parser { + + template + void ValueParser::addParameter(std::string const& parameter) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameters are not supported in this build."); + } + + template<> + void ValueParser::addParameter(std::string const& parameter) { + //STORM_LOG_THROW((std::is_same::value), storm::exceptions::NotSupportedException, "Parameters only allowed when using rational functions."); + storm::expressions::Variable var = manager->declareRationalVariable(parameter); + identifierMapping.emplace(var.getName(), var); + parser.setIdentifierMapping(identifierMapping); + STORM_LOG_TRACE("Added parameter: " << var.getName()); + } + + template<> + double ValueParser::parseValue(std::string const& value) const { + return boost::lexical_cast(value); + } + + template<> + storm::RationalFunction ValueParser::parseValue(std::string const& value) const { + storm::RationalFunction rationalFunction = evaluator.asRational(parser.parseFromString(value)); + STORM_LOG_TRACE("Parsed expression: " << rationalFunction); + return rationalFunction; + } + + template + std::shared_ptr> DirectEncodingParser::parseModel(std::string const& filename) { + + // Load file + STORM_LOG_INFO("Reading from file " << filename); + std::ifstream file; + storm::utility::openFile(filename, file); + std::string line; + + // Initialize + ValueParser valueParser; + + // Parse header + std::getline(file, line); + STORM_LOG_THROW(line == "// Exported by storm", storm::exceptions::WrongFormatException, "Expected header information."); + std::getline(file, line); + STORM_LOG_THROW(boost::starts_with(line, "// Original model type: "), storm::exceptions::WrongFormatException, "Expected header information."); + // Parse model type + std::getline(file, line); + STORM_LOG_THROW(boost::starts_with(line, "@type: "), storm::exceptions::WrongFormatException, "Expected model type."); + storm::models::ModelType type = storm::models::getModelType(line.substr(7)); + STORM_LOG_TRACE("Model type: " << type); + // Parse parameters + std::getline(file, line); + STORM_LOG_THROW(line == "@parameters", storm::exceptions::WrongFormatException, "Expected parameter declaration."); + std::getline(file, line); + if (line != "") { + std::vector parameters; + boost::split(parameters, line, boost::is_any_of(" ")); + for (std::string parameter : parameters) { + STORM_LOG_TRACE("New parameter: " << parameter); + valueParser.addParameter(parameter); + } + } + + // Parse no. states + std::getline(file, line); + STORM_LOG_THROW(line == "@nr_states", storm::exceptions::WrongFormatException, "Expected number of states."); + std::getline(file, line); + size_t nrStates = boost::lexical_cast(line); + STORM_LOG_TRACE("Model type: " << type); + + std::getline(file, line); + STORM_LOG_THROW(line == "@model", storm::exceptions::WrongFormatException, "Expected model declaration."); + + // Construct transition matrix + std::shared_ptr modelComponents = parseStates(file, type, nrStates, valueParser); + + // Done parsing + storm::utility::closeFile(file); + + // Build model + switch (type) { + case storm::models::ModelType::Dtmc: + { + STORM_LOG_THROW(false, storm::exceptions::FileIoException, "DTMC not supported."); + } + case storm::models::ModelType::Ctmc: + { + return std::make_shared>(std::move(modelComponents->transitionMatrix), std::move(modelComponents->stateLabeling), std::move(modelComponents->rewardModels), std::move(modelComponents->choiceLabeling)); + } + case storm::models::ModelType::Mdp: + { + STORM_LOG_THROW(false, storm::exceptions::FileIoException, "MDP not supported."); + } + case storm::models::ModelType::MarkovAutomaton: + { + return std::make_shared>(std::move(modelComponents->transitionMatrix), std::move(modelComponents->stateLabeling), std::move(modelComponents->markovianStates), std::move(modelComponents->exitRates)); + } + default: + STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Unknown/Unhandled model type " << type << " which cannot be parsed."); + } + } + + template + std::shared_ptr::ModelComponents> DirectEncodingParser::parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, ValueParser const& valueParser) { + // Initialize + std::shared_ptr modelComponents = std::make_shared(); + modelComponents->nonDeterministic = (type == storm::models::ModelType::Mdp || type == storm::models::ModelType::MarkovAutomaton); + storm::storage::SparseMatrixBuilder builder = storm::storage::SparseMatrixBuilder(0, 0, 0, false, modelComponents->nonDeterministic, 0); + modelComponents->stateLabeling = storm::models::sparse::StateLabeling(stateSize); + + // Iterate over all lines + std::string line; + size_t row = 0; + size_t state = 0; + bool first = true; + while (std::getline(file, line)) { + STORM_LOG_TRACE("Parsing: " << line); + if (boost::starts_with(line, "state ")) { + // New state + if (first) { + first = false; + } else { + ++state; + } + line = line.substr(6); + size_t parsedId; + size_t posId = line.find(" "); + if (posId != std::string::npos) { + parsedId = boost::lexical_cast(line.substr(0, posId)); + + // Parse rewards and labels + line = line.substr(posId+1); + // Check for rewards + if (boost::starts_with(line, "[")) { + // Rewards found + size_t posEndReward = line.find(']'); + STORM_LOG_THROW(posEndReward != std::string::npos, storm::exceptions::WrongFormatException, "] missing."); + std::string rewards = line.substr(1, posEndReward-1); + STORM_LOG_TRACE("State rewards: " << rewards); + // TODO import rewards + STORM_LOG_WARN("Rewards were not imported"); + line = line.substr(posEndReward+1); + } + // Check for labels + std::vector labels; + boost::split(labels, line, boost::is_any_of(" ")); + for (std::string label : labels) { + if (!modelComponents->stateLabeling.containsLabel(label)) { + modelComponents->stateLabeling.addLabel(label); + } + modelComponents->stateLabeling.addLabelToState(label, state); + STORM_LOG_TRACE("New label: " << label); + } + } else { + // Only state id given + parsedId = boost::lexical_cast(line); + } + STORM_LOG_TRACE("New state " << state); + STORM_LOG_ASSERT(state == parsedId, "State ids do not correspond."); + if (modelComponents->nonDeterministic) { + builder.newRowGroup(row); + } + } else if (boost::starts_with(line, "\taction ")) { + // New action + if (first) { + first = false; + } else { + ++row; + } + line = line.substr(8); + STORM_LOG_TRACE("New action: " << row); + // Check for rewards + if (boost::starts_with(line, "[")) { + // Rewards found + size_t posEndReward = line.find(']'); + STORM_LOG_THROW(posEndReward != std::string::npos, storm::exceptions::WrongFormatException, "] missing."); + std::string rewards = line.substr(1, posEndReward-1); + STORM_LOG_TRACE("Transition rewards: " << rewards); + // TODO save rewards + line = line.substr(posEndReward+1); + } + // TODO import choice labeling when the export works + + } else { + // New transition + size_t posColon = line.find(":"); + STORM_LOG_ASSERT(posColon != std::string::npos, "':' not found."); + size_t target = boost::lexical_cast(line.substr(2, posColon-3)); + std::string valueStr = line.substr(posColon+2); + ValueType value = valueParser.parseValue(valueStr); + STORM_LOG_TRACE("Transition " << state << " -> " << target << ": " << value); + builder.addNextValue(state, target, value); + } + } + + STORM_LOG_TRACE("Finished parsing"); + modelComponents->transitionMatrix = builder.build(stateSize, stateSize); + STORM_LOG_TRACE("Built matrix"); + return modelComponents; + } + + // Template instantiations. + template class DirectEncodingParser; + +#ifdef STORM_HAVE_CARL + template class DirectEncodingParser; +#endif + } // namespace parser +} // namespace storm diff --git a/src/storm/parser/DirectEncodingParser.h b/src/storm/parser/DirectEncodingParser.h new file mode 100644 index 000000000..ba1056401 --- /dev/null +++ b/src/storm/parser/DirectEncodingParser.h @@ -0,0 +1,109 @@ +#ifndef STORM_PARSER_DIRECTENCODINGPARSER_H_ +#define STORM_PARSER_DIRECTENCODINGPARSER_H_ + +#include "storm/models/sparse/Model.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/storage/expressions/ExpressionManager.h" +#include "storm/parser/ExpressionParser.h" +#include "storm/storage/expressions/ExpressionEvaluator.h" + + +namespace storm { + namespace parser { + + /*! + * Parser for values according to their ValueType. + */ + template + class ValueParser { + public: + + ValueParser() : manager(new storm::expressions::ExpressionManager()), parser(*manager), evaluator(*manager) { + } + + /*! + * Parse ValueType from string. + * + * @param value String containing the value. + * + * @return ValueType + */ + ValueType parseValue(std::string const& value) const; + + /*! + * Add declaration of parameter. + * + * @param parameter New parameter. + */ + void addParameter(std::string const& parameter); + + private: + + std::shared_ptr manager; + + storm::parser::ExpressionParser parser; + + storm::expressions::ExpressionEvaluator evaluator; + + std::unordered_map identifierMapping; + }; + + /*! + * Parser for models in the DRN format with explicit encoding. + */ + template> + class DirectEncodingParser { + public: + + /*! + * Load a model in DRN format from a file and create the model. + * + * @param file The DRN file to be parsed. + * + * @return A sparse model + */ + static std::shared_ptr> parseModel(std::string const& file); + + private: + + // A structure holding the individual components of a model. + struct ModelComponents { + + // The transition matrix. + storm::storage::SparseMatrix transitionMatrix; + + // The state labeling. + storm::models::sparse::StateLabeling stateLabeling; + + // The reward models. + std::unordered_map rewardModels; + + // A vector that stores a labeling for each choice. + boost::optional> choiceLabeling; + + // The exit rates for MAs. + std::vector exitRates; + + // The Markovian states for MA. + storm::storage::BitVector markovianStates; + + // A flag indicating if the model is non-deterministic. + bool nonDeterministic; + }; + + /*! + * Parse states and return transition matrix. + * + * @param file Input file stream. + * @param type Model type. + * @param stateSize No. of states + * + * @return Transition matrix. + */ + static std::shared_ptr parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, ValueParser const& valueParser); + }; + + } // namespace parser +} // namespace storm + +#endif /* STORM_PARSER_DIRECTENCODINGPARSER_H_ */ diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp index 9f07c0219..1ade861dd 100644 --- a/src/storm/settings/modules/IOSettings.cpp +++ b/src/storm/settings/modules/IOSettings.cpp @@ -21,6 +21,8 @@ namespace storm { const std::string IOSettings::exportExplicitOptionName = "exportexplicit"; const std::string IOSettings::explicitOptionName = "explicit"; const std::string IOSettings::explicitOptionShortName = "exp"; + const std::string IOSettings::explicitDrnOptionName = "explicit-drn"; + const std::string IOSettings::explicitDrnOptionShortName = "drn"; const std::string IOSettings::prismInputOptionName = "prism"; const std::string IOSettings::janiInputOptionName = "jani"; const std::string IOSettings::prismToJaniOptionName = "prism2jani"; @@ -53,6 +55,9 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, explicitOptionName, false, "Parses the model given in an explicit (sparse) representation.").setShortName(explicitOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("transition filename", "The name of the file from which to read the transitions.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("labeling filename", "The name of the file from which to read the state labeling.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, explicitDrnOptionName, false, "Parses the model given in the DRN format.").setShortName(explicitDrnOptionShortName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("drn filename", "The name of the DRN file containing the model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()) + .build()); this->addOption(storm::settings::OptionBuilder(moduleName, prismInputOptionName, false, "Parses the model given in the PRISM format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the PRISM input.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, janiInputOptionName, false, "Parses the model given in the JANI format.") @@ -109,7 +114,15 @@ namespace storm { std::string IOSettings::getLabelingFilename() const { return this->getOption(explicitOptionName).getArgumentByName("labeling filename").getValueAsString(); } - + + bool IOSettings::isExplicitDRNSet() const { + return this->getOption(explicitDrnOptionName).getHasOptionBeenSet(); + } + + std::string IOSettings::getExplicitDRNFilename() const { + return this->getOption(explicitDrnOptionName).getArgumentByName("drn filename").getValueAsString(); + } + bool IOSettings::isPrismInputSet() const { return this->getOption(prismInputOptionName).getHasOptionBeenSet(); } @@ -230,9 +243,12 @@ namespace storm { bool IOSettings::check() const { // Ensure that not two symbolic input models were given. STORM_LOG_THROW(!isJaniInputSet() || !isPrismInputSet(), storm::exceptions::InvalidSettingsException, "Symbolic model "); - + + // Ensure that not two explicit input models were given. + STORM_LOG_THROW(!isExplicitSet() || !isExplicitDRNSet(), storm::exceptions::InvalidSettingsException, "Explicit model "); + // Ensure that the model was given either symbolically or explicitly. - STORM_LOG_THROW(!isJaniInputSet() || !isPrismInputSet() || !isExplicitSet(), storm::exceptions::InvalidSettingsException, "The model may be either given in an explicit or a symbolic format (PRISM or JANI), but not both."); + STORM_LOG_THROW(!isJaniInputSet() || !isPrismInputSet() || !isExplicitSet() || !isExplicitDRNSet(), storm::exceptions::InvalidSettingsException, "The model may be either given in an explicit or a symbolic format (PRISM or JANI), but not both."); // Make sure PRISM-to-JANI conversion is only set if the actual input is in PRISM format. STORM_LOG_THROW(!isPrismToJaniSet() || isPrismInputSet(), storm::exceptions::InvalidSettingsException, "For the transformation from PRISM to JANI, the input model must be given in the prism format."); diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h index 711ec2d97..0e329b840 100644 --- a/src/storm/settings/modules/IOSettings.h +++ b/src/storm/settings/modules/IOSettings.h @@ -72,6 +72,20 @@ namespace storm { */ std::string getLabelingFilename() const; + /*! + * Retrieves whether the explicit option with DRN was set. + * + * @return True if the explicit option with DRN was set. + */ + bool isExplicitDRNSet() const; + + /*! + * Retrieves the name of the file that contains the model in the DRN format. + * + * @return The name of the DRN file that contains the model. + */ + std::string getExplicitDRNFilename() const; + /*! * Retrieves whether the PRISM language option was set. * @@ -275,6 +289,8 @@ namespace storm { static const std::string exportExplicitOptionName; static const std::string explicitOptionName; static const std::string explicitOptionShortName; + static const std::string explicitDrnOptionName; + static const std::string explicitDrnOptionShortName; static const std::string prismInputOptionName; static const std::string janiInputOptionName; static const std::string prismToJaniOptionName; diff --git a/src/storm/utility/DirectEncodingExporter.cpp b/src/storm/utility/DirectEncodingExporter.cpp new file mode 100644 index 000000000..b82957c9c --- /dev/null +++ b/src/storm/utility/DirectEncodingExporter.cpp @@ -0,0 +1,159 @@ +#include "DirectEncodingExporter.h" + +#include "storm/adapters/CarlAdapter.h" +#include "storm/utility/constants.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/NotImplementedException.h" +#include "storm/models/sparse/Dtmc.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/Ctmc.h" +#include "storm/models/sparse/MarkovAutomaton.h" + +#include "storm/models/sparse/StandardRewardModel.h" + + +namespace storm { + namespace exporter { + + template + void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters) { + + // Notice that for CTMCs we write the rate matrix instead of probabilities + + // Initialize + std::vector exitRates; // Only for CTMCs and MAs. + if(sparseModel->getType() == storm::models::ModelType::Ctmc) { + exitRates = sparseModel->template as>()->getExitRateVector(); + } else if(sparseModel->getType() == storm::models::ModelType::MarkovAutomaton) { + exitRates = sparseModel->template as>()->getExitRates(); + } + + // Write header + os << "// Exported by storm" << std::endl; + os << "// Original model type: " << sparseModel->getType() << std::endl; + os << "@type: " << sparseModel->getType() << std::endl; + os << "@parameters" << std::endl; + if (parameters.empty()) { + for (std::string const& parameter : getParameters(sparseModel)) { + os << parameter << " "; + } + } else { + for (std::string const& parameter : parameters) { + os << parameter << " "; + } + } + os << std::endl; + os << "@nr_states" << std::endl << sparseModel->getNumberOfStates() << std::endl; + os << "@model" << std::endl; + + storm::storage::SparseMatrix const& matrix = sparseModel->getTransitionMatrix(); + + for (typename storm::storage::SparseMatrix::index_type group = 0; group < matrix.getRowGroupCount(); ++group) { + os << "state " << group; + + // Write state rewards + bool first = true; + for (auto const& rewardModelEntry : sparseModel->getRewardModels()) { + if (first) { + os << " ["; + first = false; + } else { + os << ", "; + } + + if(rewardModelEntry.second.hasStateRewards()) { + os << rewardModelEntry.second.getStateRewardVector().at(group); + } else { + os << "0"; + } + } + + if (!first) { + os << "]"; + } + + // Write labels + for(auto const& label : sparseModel->getStateLabeling().getLabelsOfState(group)) { + os << " " << label; + } + os << std::endl; + + // Write probabilities + typename storm::storage::SparseMatrix::index_type start = matrix.hasTrivialRowGrouping() ? group : matrix.getRowGroupIndices()[group]; + typename storm::storage::SparseMatrix::index_type end = matrix.hasTrivialRowGrouping() ? group + 1 : matrix.getRowGroupIndices()[group + 1]; + + // Iterate over all actions + for (typename storm::storage::SparseMatrix::index_type row = start; row < end; ++row) { + // Print the actual row. + os << "\taction " << row - start; + bool first = true; + // Write transition rewards + for (auto const& rewardModelEntry : sparseModel->getRewardModels()) { + if (first) { + os << " ["; + first = false; + } else { + os << ", "; + } + + if(rewardModelEntry.second.hasStateActionRewards()) { + os << storm::utility::to_string(rewardModelEntry.second.getStateActionRewardVector().at(row)); + } else { + os << "0"; + } + + } + if (!first) { + os << "]"; + } + + // Write choice labeling + if(sparseModel->hasChoiceLabeling()) { + // TODO export choice labeling + STORM_LOG_WARN("Choice labeling was not exported."); + } + os << std::endl; + + // Write probabilities + for(auto it = matrix.begin(row); it != matrix.end(row); ++it) { + ValueType prob = it->getValue(); + os << "\t\t" << it->getColumn() << " : "; + os << storm::utility::to_string(prob) << std::endl; + } + + } + } // end matrix iteration + + } + + template + std::vector getParameters(std::shared_ptr> sparseModel) { + return {}; + } + + template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); + +#ifdef STORM_HAVE_CARL + template<> + std::vector getParameters(std::shared_ptr> sparseModel) { + std::vector parameters; + std::set parametersProb = storm::models::sparse::getProbabilityParameters(*sparseModel); + for (auto const& parameter : parametersProb) { + std::stringstream stream; + stream << parameter; + parameters.push_back(stream.str()); + } + std::set parametersReward = storm::models::sparse::getRewardParameters(*sparseModel); + for (auto const& parameter : parametersReward) { + std::stringstream stream; + stream << parameter; + parameters.push_back(stream.str()); + } + return parameters; + } + + template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); + template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); +#endif + } +} diff --git a/src/storm/utility/DirectEncodingExporter.h b/src/storm/utility/DirectEncodingExporter.h new file mode 100644 index 000000000..9728599a6 --- /dev/null +++ b/src/storm/utility/DirectEncodingExporter.h @@ -0,0 +1,30 @@ +#pragma once +#include +#include + +#include "storm/models/sparse/Model.h" + +namespace storm { + namespace exporter { + + /*! + * Exports a sparse model into the explicit DRN format. + * + * @param os Stream to export to + * @param sparseModel Model to export + * @param parameters List of parameters + */ + template + void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); + + /*! + * Accumalate parameters in the model. + * + * @param sparseModel Model. + * @return List of parameters in the model. + */ + template + std::vector getParameters(std::shared_ptr> sparseModel); + + } +} diff --git a/src/storm/utility/ExplicitExporter.cpp b/src/storm/utility/ExplicitExporter.cpp deleted file mode 100644 index 1f40ab538..000000000 --- a/src/storm/utility/ExplicitExporter.cpp +++ /dev/null @@ -1,138 +0,0 @@ -#include "ExplicitExporter.h" - -#include "storm/adapters/CarlAdapter.h" -#include "storm/utility/constants.h" -#include "storm/utility/macros.h" -#include "storm/exceptions/NotImplementedException.h" -#include "storm/models/sparse/Dtmc.h" -#include "storm/models/sparse/Mdp.h" -#include "storm/models/sparse/Ctmc.h" -#include "storm/models/sparse/MarkovAutomaton.h" - -#include "storm/models/sparse/StandardRewardModel.h" - - -namespace storm { - namespace exporter { - template - void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters) { - bool embedded = false; - if(sparseModel->getType() == storm::models::ModelType::Ctmc || sparseModel->getType() == storm::models::ModelType::MarkovAutomaton) { - STORM_LOG_WARN("This format only supports discrete time models"); - embedded = true; - } - - STORM_LOG_THROW(embedded || sparseModel->getType() == storm::models::ModelType::Mdp || sparseModel->getType() == storm::models::ModelType::Dtmc , storm::exceptions::NotImplementedException, "This functionality is not yet implemented." ); - - std::vector exitRates; // Only for CTMCs and MAs. - if(sparseModel->getType() == storm::models::ModelType::Ctmc) { - exitRates = sparseModel->template as>()->getExitRateVector(); - } else if(sparseModel->getType() == storm::models::ModelType::MarkovAutomaton) { - exitRates = sparseModel->template as>()->getExitRates(); - } - - os << "// Exported by storm" << std::endl; - os << "// Original model type: " << sparseModel->getType() << std::endl; - os << "@type: mdp" << std::endl; - os << "@parameters" << std::endl; - for (auto const& p : parameters) { - os << p << " "; - } - os << std::endl; - os << "@nr_states" << std::endl << sparseModel->getNumberOfStates() << std::endl; - os << "@model" << std::endl; - storm::storage::SparseMatrix const& matrix = sparseModel->getTransitionMatrix(); - - for (typename storm::storage::SparseMatrix::index_type group = 0; group < matrix.getRowGroupCount(); ++group) { - os << "state " << group; - - if (!embedded) { - bool first = true; - for (auto const& rewardModelEntry : sparseModel->getRewardModels()) { - if (first) { - os << " ["; - first = false; - } else { - os << ", "; - } - - if(rewardModelEntry.second.hasStateRewards()) { - os << rewardModelEntry.second.getStateRewardVector().at(group); - } else { - os << "0"; - } - } - - if (!first) { - os << "]"; - } - } else { - // We currently only support the expected time. - os << " [" << storm::utility::one()/exitRates.at(group) << "]"; - } - - for(auto const& label : sparseModel->getStateLabeling().getLabelsOfState(group)) { - os << " " << label; - } - os << std::endl; - typename storm::storage::SparseMatrix::index_type start = matrix.hasTrivialRowGrouping() ? group : matrix.getRowGroupIndices()[group]; - typename storm::storage::SparseMatrix::index_type end = matrix.hasTrivialRowGrouping() ? group + 1 : matrix.getRowGroupIndices()[group + 1]; - - - for (typename storm::storage::SparseMatrix::index_type i = start; i < end; ++i) { - // Print the actual row. - os << "\taction " << i - start; - if (!embedded) { - bool first = true; - for (auto const& rewardModelEntry : sparseModel->getRewardModels()) { - if (first) { - os << " ["; - first = false; - } else { - os << ", "; - } - - if(rewardModelEntry.second.hasStateActionRewards()) { - os << storm::utility::to_string(rewardModelEntry.second.getStateActionRewardVector().at(i)); - } else { - os << "0"; - } - - } - if (!first) { - os << "]"; - } - } else { - // We currently only support the expected time. - } - - - - if(sparseModel->hasChoiceLabeling()) { - //TODO - } - os << std::endl; - - - for(auto it = matrix.begin(i); it != matrix.end(i); ++it) { - ValueType prob = it->getValue(); - if(embedded) { - prob = prob / exitRates.at(group); - } - os << "\t\t" << it->getColumn() << " : "; - os << storm::utility::to_string(prob) << std::endl; - } - - } - } - - } - - - - template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); - - template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); - template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); - } -} diff --git a/src/storm/utility/ExplicitExporter.h b/src/storm/utility/ExplicitExporter.h deleted file mode 100644 index 964b1f10f..000000000 --- a/src/storm/utility/ExplicitExporter.h +++ /dev/null @@ -1,15 +0,0 @@ -#pragma once -#include -#include - -#include "storm/models/sparse/Model.h" - -namespace storm { - namespace exporter { - - template - void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); - - - } -} diff --git a/src/storm/utility/ModelInstantiator.h b/src/storm/utility/ModelInstantiator.h index 17de0ea21..ce5154a2b 100644 --- a/src/storm/utility/ModelInstantiator.h +++ b/src/storm/utility/ModelInstantiator.h @@ -67,15 +67,28 @@ namespace storm { template typename std::enable_if< std::is_same>::value || - std::is_same>::value || - std::is_same>::value + std::is_same>::value >::type initializeModelSpecificData(PMT const& parametricModel) { auto stateLabelingCopy = parametricModel.getStateLabeling(); auto choiceLabelingCopy = parametricModel.getOptionalChoiceLabeling(); this->instantiatedModel = std::make_shared(buildDummyMatrix(parametricModel.getTransitionMatrix()), std::move(stateLabelingCopy), buildDummyRewardModels(parametricModel.getRewardModels()), std::move(choiceLabelingCopy)); } - + + template + typename std::enable_if< + std::is_same>::value + >::type + initializeModelSpecificData(PMT const& parametricModel) { + auto stateLabelingCopy = parametricModel.getStateLabeling(); + auto choiceLabelingCopy = parametricModel.getOptionalChoiceLabeling(); + std::vector exitRates(parametricModel.getExitRateVector().size(), storm::utility::one()); + this->instantiatedModel = std::make_shared(buildDummyMatrix(parametricModel.getTransitionMatrix()), std::move(exitRates), std::move(stateLabelingCopy), buildDummyRewardModels(parametricModel.getRewardModels()), std::move(choiceLabelingCopy)); + + initializeVectorMapping(this->instantiatedModel->getExitRateVector(), this->functions, this->vectorMapping, parametricModel.getExitRateVector()); + } + + template typename std::enable_if< std::is_same>::value diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index 407c0b40c..0b43838f6 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -41,6 +41,7 @@ #include "storm/storage/dd/Bdd.h" #include "storm/parser/AutoParser.h" +#include "storm/parser/DirectEncodingParser.h" #include "storm/storage/jani/Model.h" #include "storm/storage/jani/Property.h" @@ -112,7 +113,12 @@ namespace storm { std::shared_ptr> buildExplicitModel(std::string const& transitionsFile, std::string const& labelingFile, boost::optional const& stateRewardsFile = boost::none, boost::optional const& transitionRewardsFile = boost::none, boost::optional const& choiceLabelingFile = boost::none) { return storm::parser::AutoParser<>::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "", choiceLabelingFile ? choiceLabelingFile.get() : "" ); } - + + template + std::shared_ptr> buildExplicitDRNModel(std::string const& drnFile) { + return storm::parser::DirectEncodingParser::parseModel(drnFile); + } + std::vector> extractFormulasFromProperties(std::vector const& properties); std::pair> parseJaniModel(std::string const& path); storm::prism::Program parseProgram(std::string const& path);