diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c index 8cf8a5b88..a890e28a9 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c @@ -542,7 +542,7 @@ TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_and_exists, MTBDD, a, MTBDD, b return result; } -TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_threshold, MTBDD, a, size_t, svalue) { +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_threshold, MTBDD, a, size_t*, svalue) { storm_rational_function_ptr value = (storm_rational_function_ptr)svalue; if (mtbdd_isleaf(a)) { @@ -553,7 +553,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_threshold, MTBDD, a, size_t return mtbdd_invalid; } -TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_strict_threshold, MTBDD, a, size_t, svalue) { +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_strict_threshold, MTBDD, a, size_t*, svalue) { storm_rational_function_ptr value = (storm_rational_function_ptr)svalue; if (mtbdd_isleaf(a)) { @@ -567,12 +567,12 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_strict_threshold, MTBDD, a, TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_threshold, MTBDD, dd, storm_rational_function_ptr, value) { - return mtbdd_uapply(dd, TASK(sylvan_storm_rational_function_op_threshold), *(size_t*)value); + return mtbdd_uapply(dd, TASK(sylvan_storm_rational_function_op_threshold), (size_t*)value); } TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_strict_threshold, MTBDD, dd, storm_rational_function_ptr, value) { - return mtbdd_uapply(dd, TASK(sylvan_storm_rational_function_op_strict_threshold), *(size_t*)value); + return mtbdd_uapply(dd, TASK(sylvan_storm_rational_function_op_strict_threshold), (size_t*)value); } TASK_IMPL_1(MTBDD, sylvan_storm_rational_function_minimum, MTBDD, a) { diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h index a47def0a1..888a80d51 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h @@ -76,8 +76,8 @@ TASK_DECL_3(MTBDD, sylvan_storm_rational_function_and_exists, MTBDD, MTBDD, MTBD TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_to_double, MTBDD, size_t) #define sylvan_storm_rational_function_to_double(a) mtbdd_uapply_nocache(a, TASK(sylvan_storm_rational_function_op_to_double), 0) -TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_threshold, MTBDD, size_t) -TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_strict_threshold, MTBDD, size_t) +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_threshold, MTBDD, size_t*) +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_strict_threshold, MTBDD, size_t*) TASK_DECL_2(MTBDD, sylvan_storm_rational_function_threshold, MTBDD, storm_rational_function_ptr); #define sylvan_storm_rational_function_threshold(dd, value) CALL(sylvan_storm_rational_function_strict_threshold, dd, value) diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c b/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c index 692a6f607..076e75442 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c @@ -576,7 +576,7 @@ TASK_IMPL_3(MTBDD, sylvan_storm_rational_number_and_exists, MTBDD, a, MTBDD, b, return result; } -TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_threshold, MTBDD, a, size_t, svalue) { +TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_threshold, MTBDD, a, size_t*, svalue) { storm_rational_number_ptr value = (storm_rational_number_ptr)svalue; if (mtbdd_isleaf(a)) { @@ -587,7 +587,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_threshold, MTBDD, a, size_t, return mtbdd_invalid; } -TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_strict_threshold, MTBDD, a, size_t, svalue) { +TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_strict_threshold, MTBDD, a, size_t*, svalue) { storm_rational_number_ptr value = (storm_rational_number_ptr)svalue; if (mtbdd_isleaf(a)) { @@ -601,12 +601,12 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_strict_threshold, MTBDD, a, s TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_threshold, MTBDD, dd, storm_rational_number_ptr, value) { - return mtbdd_uapply(dd, TASK(sylvan_storm_rational_number_op_threshold), *(size_t*)value); + return mtbdd_uapply(dd, TASK(sylvan_storm_rational_number_op_threshold), (size_t*)value); } TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_strict_threshold, MTBDD, dd, storm_rational_number_ptr, value) { - return mtbdd_uapply(dd, TASK(sylvan_storm_rational_number_op_strict_threshold), *(size_t*)value); + return mtbdd_uapply(dd, TASK(sylvan_storm_rational_number_op_strict_threshold), (size_t*)value); } TASK_IMPL_1(MTBDD, sylvan_storm_rational_number_minimum, MTBDD, a) { diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.h b/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.h index d7accd375..227a9831d 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.h +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.h @@ -76,8 +76,8 @@ TASK_DECL_3(MTBDD, sylvan_storm_rational_number_and_exists, MTBDD, MTBDD, MTBDD) TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_to_double, MTBDD, size_t) #define sylvan_storm_rational_number_to_double(a) mtbdd_uapply_nocache(a, TASK(sylvan_storm_rational_number_op_to_double), 0) -TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_threshold, MTBDD, size_t) -TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_strict_threshold, MTBDD, size_t) +TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_threshold, MTBDD, size_t*) +TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_strict_threshold, MTBDD, size_t*) TASK_DECL_2(MTBDD, sylvan_storm_rational_number_threshold, MTBDD, storm_rational_number_ptr); #define sylvan_storm_rational_number_threshold(dd, value) CALL(sylvan_storm_rational_number_strict_threshold, dd, value) 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..30e0d2eec --- /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/modelchecker/multiobjective/pcaa.cpp b/src/storm/modelchecker/multiobjective/pcaa.cpp index ff9e84966..6019c19cd 100644 --- a/src/storm/modelchecker/multiobjective/pcaa.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa.cpp @@ -9,8 +9,10 @@ #include "storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h" #include "storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h" #include "storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h" -#include "storm/settings//SettingsManager.h" +#include "storm/settings/SettingsManager.h" #include "storm/settings/modules/MultiObjectiveSettings.h" +#include "storm/settings/modules/CoreSettings.h" +#include "storm/utility/Stopwatch.h" #include "storm/exceptions/InvalidArgumentException.h" @@ -21,6 +23,8 @@ namespace storm { template std::unique_ptr performPcaa(SparseModelType const& model, storm::logic::MultiObjectiveFormula const& formula) { + storm::utility::Stopwatch swTotal(true); + storm::utility::Stopwatch swPreprocessing(true); STORM_LOG_ASSERT(model.getInitialStates().getNumberOfSetBits() == 1, "Multi-objective Model checking on model with multiple initial states is not supported."); #ifdef STORM_HAVE_CARL @@ -31,8 +35,13 @@ namespace storm { } auto preprocessorResult = SparsePcaaPreprocessor::preprocess(model, formula); - STORM_LOG_INFO("Preprocessing done. Result: " << preprocessorResult); - + swPreprocessing.stop(); + if (storm::settings::getModule().isShowStatisticsSet()) { + STORM_PRINT_AND_LOG("Preprocessing done in " << swPreprocessing << " seconds." << std::endl << " Result: " << preprocessorResult << std::endl); + } else { + STORM_LOG_INFO("Preprocessing done in " << swPreprocessing << " seconds." << std::endl << " Result: " << preprocessorResult << std::endl); + } + storm::utility::Stopwatch swValueIterations(true); std::unique_ptr> query; switch (preprocessorResult.queryType) { case SparsePcaaPreprocessorReturnType::QueryType::Achievability: @@ -50,8 +59,14 @@ namespace storm { } auto result = query->check(); + swValueIterations.stop(); + swTotal.stop(); + if (storm::settings::getModule().isShowStatisticsSet()) { + STORM_PRINT_AND_LOG("Solving multi-objective query took " << swTotal << " seconds (consisting of " << swPreprocessing << " seconds for preprocessing and " << swValueIterations << " seconds for value iteration-based exploration of achievable points)." << std::endl); + } + - if(settings::getModule().isExportPlotSet()) { + if(storm::settings::getModule().isExportPlotSet()) { query->exportPlotOfCurrentApproximation(storm::settings::getModule().getExportPlotDirectory()); } return result; diff --git a/src/storm/modelchecker/multiobjective/pcaa/PcaaObjective.h b/src/storm/modelchecker/multiobjective/pcaa/PcaaObjective.h index 84f04ec62..ac0043fae 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/PcaaObjective.h +++ b/src/storm/modelchecker/multiobjective/pcaa/PcaaObjective.h @@ -32,8 +32,10 @@ namespace storm { bool thresholdIsStrict = false; // The time bound(s) for the formula (if given by the originalFormula) - boost::optional lowerTimeBound; - boost::optional upperTimeBound; + boost::optional lowerTimeBound; + boost::optional upperTimeBound; + bool lowerTimeBoundStrict = false; + bool upperTimeBoundStrict = false; void printToStream(std::ostream& out) const { out << std::setw(30) << originalFormula->toString(); @@ -51,12 +53,12 @@ namespace storm { out << "time bounds:"; if(lowerTimeBound) { if(upperTimeBound) { - out << "[" << *lowerTimeBound << ", " << *upperTimeBound << "]"; + out << (lowerTimeBoundStrict ? "(" : "[") << *lowerTimeBound << ", " << *upperTimeBound << (upperTimeBoundStrict ? ")" : "]"); } else { - out << ">=" << std::setw(5) << *lowerTimeBound; + out << (lowerTimeBoundStrict ? " >" : ">=") << std::setw(5) << *lowerTimeBound; } } else if (upperTimeBound) { - out << "<=" << std::setw(5) << *upperTimeBound; + out << (upperTimeBoundStrict ? " <" : "<=") << std::setw(5) << *upperTimeBound; } else { out << " none"; } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp index df2864b34..8ae1c8498 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp @@ -9,6 +9,7 @@ #include "storm/utility/vector.h" #include "storm/exceptions/InvalidOperationException.h" +#include "storm/exceptions/InvalidPropertyException.h" namespace storm { namespace modelchecker { @@ -48,9 +49,8 @@ namespace storm { digitize(MS, digitizationConstant); // Get for each occurring (digitized) timeBound the indices of the objectives with that bound. - TimeBoundMap lowerTimeBounds; TimeBoundMap upperTimeBounds; - digitizeTimeBounds(lowerTimeBounds, upperTimeBounds, digitizationConstant); + digitizeTimeBounds(upperTimeBounds, digitizationConstant); // Initialize a minMaxSolver to compute an optimal scheduler (w.r.t. PS) for each epoch // No EC elimination is necessary as we assume non-zenoness @@ -66,12 +66,11 @@ namespace storm { // Stores the objectives for which we need to compute values in the current time epoch. storm::storage::BitVector consideredObjectives = this->objectivesWithNoUpperTimeBound; - auto lowerTimeBoundIt = lowerTimeBounds.begin(); auto upperTimeBoundIt = upperTimeBounds.begin(); - uint_fast64_t currentEpoch = std::max(lowerTimeBounds.empty() ? 0 : lowerTimeBoundIt->first, upperTimeBounds.empty() ? 0 : upperTimeBoundIt->first); - while(true) { + uint_fast64_t currentEpoch = upperTimeBounds.empty() ? 0 : upperTimeBoundIt->first; + while (true) { // Update the objectives that are considered at the current time epoch as well as the (weighted) reward vectors. - updateDataToCurrentEpoch(MS, PS, *minMax, consideredObjectives, currentEpoch, weightVector, lowerTimeBoundIt, lowerTimeBounds, upperTimeBoundIt, upperTimeBounds); + updateDataToCurrentEpoch(MS, PS, *minMax, consideredObjectives, currentEpoch, weightVector, upperTimeBoundIt, upperTimeBounds); // Compute the values that can be obtained at probabilistic states in the current time epoch performPSStep(PS, MS, *minMax, *linEq, optimalChoicesAtCurrentEpoch, consideredObjectives, weightVector); @@ -156,20 +155,19 @@ namespace storm { // Initialize some data for fast and easy access VT const maxRate = this->model.getMaximalExitRate(); - std::vector> eToPowerOfMinusMaxRateTimesBound; + std::vector timeBounds; + std::vector eToPowerOfMinusMaxRateTimesBound; VT smallestNonZeroBound = storm::utility::zero(); for(auto const& obj : this->objectives) { - eToPowerOfMinusMaxRateTimesBound.emplace_back(); - if(obj.lowerTimeBound){ - STORM_LOG_ASSERT(!storm::utility::isZero(*obj.lowerTimeBound), "Got zero-valued lower bound."); // should have been handled in preprocessing - STORM_LOG_ASSERT(!obj.upperTimeBound || *obj.lowerTimeBound < *obj.upperTimeBound, "Got point intervall or empty intervall on time bounded property which is not supported"); // should also have been handled in preprocessing - eToPowerOfMinusMaxRateTimesBound.back().first = std::exp(-maxRate * (*obj.lowerTimeBound)); - smallestNonZeroBound = storm::utility::isZero(smallestNonZeroBound) ? *obj.lowerTimeBound : std::min(smallestNonZeroBound, *obj.lowerTimeBound); - } if(obj.upperTimeBound){ - STORM_LOG_ASSERT(!storm::utility::isZero(*obj.upperTimeBound), "Got zero-valued upper bound."); // should have been handled in preprocessing - eToPowerOfMinusMaxRateTimesBound.back().second = std::exp(-maxRate * (*obj.upperTimeBound)); - smallestNonZeroBound = storm::utility::isZero(smallestNonZeroBound) ? *obj.upperTimeBound : std::min(smallestNonZeroBound, *obj.upperTimeBound); + STORM_LOG_THROW(!obj.upperTimeBound->containsVariables(), storm::exceptions::InvalidOperationException, "The time bound '" << *obj.upperTimeBound << " contains undefined variables"); + timeBounds.push_back(storm::utility::convertNumber(obj.upperTimeBound->evaluateAsRational())); + STORM_LOG_ASSERT(!storm::utility::isZero(timeBounds.back()), "Got zero-valued upper time bound."); + eToPowerOfMinusMaxRateTimesBound.push_back(std::exp(-maxRate * timeBounds.back())); + smallestNonZeroBound = storm::utility::isZero(smallestNonZeroBound) ? timeBounds.back() : std::min(smallestNonZeroBound, timeBounds.back()); + } else { + timeBounds.push_back(storm::utility::zero()); + eToPowerOfMinusMaxRateTimesBound.push_back(storm::utility::zero()); } } if(storm::utility::isZero(smallestNonZeroBound)) { @@ -181,13 +179,14 @@ namespace storm { // We brute-force a delta, since a direct computation is apparently not easy. // Also note that the number of times this loop runs is a lower bound for the number of minMaxSolver invocations. // Hence, this brute-force approach will most likely not be a bottleneck. + storm::storage::BitVector objectivesWithTimeBound = ~this->objectivesWithNoUpperTimeBound; uint_fast64_t smallestStepBound = 1; VT delta = smallestNonZeroBound / smallestStepBound; while(true) { bool deltaValid = true; - for(auto const& obj : this->objectives) { - if((obj.lowerTimeBound && *obj.lowerTimeBound/delta != std::floor(*obj.lowerTimeBound/delta)) || - (obj.upperTimeBound && *obj.upperTimeBound/delta != std::floor(*obj.upperTimeBound/delta))) { + for(auto const& objIndex : objectivesWithTimeBound) { + auto const& timeBound = timeBounds[objIndex]; + if(timeBound/delta != std::floor(timeBound/delta)) { deltaValid = false; break; } @@ -195,14 +194,9 @@ namespace storm { if(deltaValid) { VT weightedPrecisionForCurrentDelta = storm::utility::zero(); for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { - auto const& obj = this->objectives[objIndex]; VT precisionOfObj = storm::utility::zero(); - if(obj.lowerTimeBound) { - precisionOfObj += storm::utility::one() - (eToPowerOfMinusMaxRateTimesBound[objIndex].first * storm::utility::pow(storm::utility::one() + maxRate * delta, *obj.lowerTimeBound / delta) ) - + storm::utility::one() - std::exp(-maxRate * delta); - } - if(obj.upperTimeBound) { - precisionOfObj += storm::utility::one() - (eToPowerOfMinusMaxRateTimesBound[objIndex].second * storm::utility::pow(storm::utility::one() + maxRate * delta, *obj.upperTimeBound / delta) ); + if (objectivesWithTimeBound.get(objIndex)) { + precisionOfObj += storm::utility::one() - (eToPowerOfMinusMaxRateTimesBound[objIndex] * storm::utility::pow(storm::utility::one() + maxRate * delta, timeBounds[objIndex] / delta) ); } weightedPrecisionForCurrentDelta += weightVector[objIndex] * precisionOfObj; } @@ -256,31 +250,21 @@ namespace storm { template template ::SupportsExponential, int>::type> - void SparseMaPcaaWeightVectorChecker::digitizeTimeBounds(TimeBoundMap& lowerTimeBounds, TimeBoundMap& upperTimeBounds, VT const& digitizationConstant) { + void SparseMaPcaaWeightVectorChecker::digitizeTimeBounds(TimeBoundMap& upperTimeBounds, VT const& digitizationConstant) { VT const maxRate = this->model.getMaximalExitRate(); for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { auto const& obj = this->objectives[objIndex]; - VT errorTowardsZero; - VT errorAwayFromZero; - if(obj.lowerTimeBound) { - uint_fast64_t digitizedBound = storm::utility::convertNumber((*obj.lowerTimeBound)/digitizationConstant); - auto timeBoundIt = lowerTimeBounds.insert(std::make_pair(digitizedBound, storm::storage::BitVector(this->objectives.size(), false))).first; - timeBoundIt->second.set(objIndex); - VT digitizationError = storm::utility::one(); - digitizationError -= std::exp(-maxRate * (*obj.lowerTimeBound)) * storm::utility::pow(storm::utility::one() + maxRate * digitizationConstant, digitizedBound); - errorTowardsZero = -digitizationError; - errorAwayFromZero = storm::utility::one() - std::exp(-maxRate * digitizationConstant);; - } else { - errorTowardsZero = storm::utility::zero(); - errorAwayFromZero = storm::utility::zero(); - } + STORM_LOG_THROW(!obj.lowerTimeBound, storm::exceptions::InvalidPropertyException, "Lower time bounds are not supported by this model checker"); + VT errorTowardsZero = storm::utility::zero(); + VT errorAwayFromZero = storm::utility::zero(); if(obj.upperTimeBound) { - uint_fast64_t digitizedBound = storm::utility::convertNumber((*obj.upperTimeBound)/digitizationConstant); + VT timeBound = storm::utility::convertNumber(obj.upperTimeBound->evaluateAsRational()); + uint_fast64_t digitizedBound = storm::utility::convertNumber(timeBound/digitizationConstant); auto timeBoundIt = upperTimeBounds.insert(std::make_pair(digitizedBound, storm::storage::BitVector(this->objectives.size(), false))).first; timeBoundIt->second.set(objIndex); VT digitizationError = storm::utility::one(); - digitizationError -= std::exp(-maxRate * (*obj.upperTimeBound)) * storm::utility::pow(storm::utility::one() + maxRate * digitizationConstant, digitizedBound); + digitizationError -= std::exp(-maxRate * timeBound) * storm::utility::pow(storm::utility::one() + maxRate * digitizationConstant, digitizedBound); errorAwayFromZero += digitizationError; } if (obj.rewardsArePositive) { @@ -295,7 +279,7 @@ namespace storm { template template ::SupportsExponential, int>::type> - void SparseMaPcaaWeightVectorChecker::digitizeTimeBounds(TimeBoundMap& lowerTimeBounds, TimeBoundMap& upperTimeBounds, VT const& digitizationConstant) { + void SparseMaPcaaWeightVectorChecker::digitizeTimeBounds(TimeBoundMap& upperTimeBounds, VT const& digitizationConstant) { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded probabilities of MAs is unsupported for this value type."); } @@ -324,19 +308,7 @@ namespace storm { } template - void SparseMaPcaaWeightVectorChecker::updateDataToCurrentEpoch(SubModel& MS, SubModel& PS, MinMaxSolverData& minMax, storm::storage::BitVector& consideredObjectives, uint_fast64_t const& currentEpoch, std::vector const& weightVector, TimeBoundMap::iterator& lowerTimeBoundIt, TimeBoundMap const& lowerTimeBounds, TimeBoundMap::iterator& upperTimeBoundIt, TimeBoundMap const& upperTimeBounds) { - - //Note that lower time bounds are always strict. Hence, we need to react when the current epoch equals the stored bound. - if(lowerTimeBoundIt != lowerTimeBounds.end() && currentEpoch == lowerTimeBoundIt->first) { - for(auto objIndex : lowerTimeBoundIt->second) { - // No more reward is earned for this objective. - storm::utility::vector::addScaledVector(MS.weightedRewardVector, MS.objectiveRewardVectors[objIndex], -weightVector[objIndex]); - storm::utility::vector::addScaledVector(PS.weightedRewardVector, PS.objectiveRewardVectors[objIndex], -weightVector[objIndex]); - MS.objectiveRewardVectors[objIndex] = std::vector(MS.objectiveRewardVectors[objIndex].size(), storm::utility::zero()); - PS.objectiveRewardVectors[objIndex] = std::vector(PS.objectiveRewardVectors[objIndex].size(), storm::utility::zero()); - } - ++lowerTimeBoundIt; - } + void SparseMaPcaaWeightVectorChecker::updateDataToCurrentEpoch(SubModel& MS, SubModel& PS, MinMaxSolverData& minMax, storm::storage::BitVector& consideredObjectives, uint_fast64_t const& currentEpoch, std::vector const& weightVector, TimeBoundMap::iterator& upperTimeBoundIt, TimeBoundMap const& upperTimeBounds) { if(upperTimeBoundIt != upperTimeBounds.end() && currentEpoch == upperTimeBoundIt->first) { consideredObjectives |= upperTimeBoundIt->second; @@ -420,12 +392,12 @@ namespace storm { template class SparseMaPcaaWeightVectorChecker>; template double SparseMaPcaaWeightVectorChecker>::getDigitizationConstant(std::vector const& direction) const; template void SparseMaPcaaWeightVectorChecker>::digitize(SparseMaPcaaWeightVectorChecker>::SubModel& subModel, double const& digitizationConstant) const; - template void SparseMaPcaaWeightVectorChecker>::digitizeTimeBounds(SparseMaPcaaWeightVectorChecker>::TimeBoundMap& lowerTimeBounds, SparseMaPcaaWeightVectorChecker>::TimeBoundMap& upperTimeBounds, double const& digitizationConstant); + template void SparseMaPcaaWeightVectorChecker>::digitizeTimeBounds( SparseMaPcaaWeightVectorChecker>::TimeBoundMap& upperTimeBounds, double const& digitizationConstant); #ifdef STORM_HAVE_CARL // template class SparseMaPcaaWeightVectorChecker>; // template storm::RationalNumber SparseMaPcaaWeightVectorChecker>::getDigitizationConstant(std::vector const& direction) const; // template void SparseMaPcaaWeightVectorChecker>::digitize(SparseMaPcaaWeightVectorChecker>::SubModel& subModel, storm::RationalNumber const& digitizationConstant) const; -// template void SparseMaPcaaWeightVectorChecker>::digitizeTimeBounds(SparseMaPcaaWeightVectorChecker>::TimeBoundMap& lowerTimeBounds, SparseMaPcaaWeightVectorChecker>::TimeBoundMap& upperTimeBounds, storm::RationalNumber const& digitizationConstant); +// template void SparseMaPcaaWeightVectorChecker>::digitizeTimeBounds(SparseMaPcaaWeightVectorChecker>::TimeBoundMap& upperTimeBounds, storm::RationalNumber const& digitizationConstant); #endif } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h index a757ccf0a..1ac363c4d 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h @@ -105,13 +105,13 @@ namespace storm { void digitize(SubModel& subModel, VT const& digitizationConstant) const; /* - * Fills the given maps with the digitized time bounds. Also sets the offsetsToLowerBound / offsetsToUpperBound values + * Fills the given map with the digitized time bounds. Also sets the offsetsToLowerBound / offsetsToUpperBound values * according to the digitization error */ template ::SupportsExponential, int>::type = 0> - void digitizeTimeBounds(TimeBoundMap& lowerTimeBounds, TimeBoundMap& upperTimeBounds, VT const& digitizationConstant); + void digitizeTimeBounds(TimeBoundMap& upperTimeBounds, VT const& digitizationConstant); template ::SupportsExponential, int>::type = 0> - void digitizeTimeBounds(TimeBoundMap& lowerTimeBounds, TimeBoundMap& upperTimeBounds, VT const& digitizationConstant); + void digitizeTimeBounds(TimeBoundMap& upperTimeBounds, VT const& digitizationConstant); /*! @@ -129,7 +129,7 @@ namespace storm { * the reward vector of the reduced PStoPS model, and * objectives that are considered at the current time epoch. */ - void updateDataToCurrentEpoch(SubModel& MS, SubModel& PS, MinMaxSolverData& minMax, storm::storage::BitVector& consideredObjectives, uint_fast64_t const& currentEpoch, std::vector const& weightVector, TimeBoundMap::iterator& lowerTimeBoundIt, TimeBoundMap const& lowerTimeBounds, TimeBoundMap::iterator& upperTimeBoundIt, TimeBoundMap const& upperTimeBounds); + void updateDataToCurrentEpoch(SubModel& MS, SubModel& PS, MinMaxSolverData& minMax, storm::storage::BitVector& consideredObjectives, uint_fast64_t const& currentEpoch, std::vector const& weightVector, TimeBoundMap::iterator& upperTimeBoundIt, TimeBoundMap const& upperTimeBounds); /* * Performs a step for the probabilistic states, that is diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp index cb5c92e34..a6dc7a3b4 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp @@ -5,6 +5,7 @@ #include "storm/models/sparse/StandardRewardModel.h" #include "storm/utility/macros.h" #include "storm/utility/vector.h" +#include "storm/exceptions/InvalidPropertyException.h" namespace storm { @@ -19,7 +20,7 @@ namespace storm { storm::storage::BitVector const& possiblyRecurrentStates) : SparsePcaaWeightVectorChecker(model, objectives, actionsWithNegativeReward, ecActions, possiblyRecurrentStates) { // set the state action rewards - for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { + for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { typename SparseMdpModelType::RewardModelType const& rewModel = this->model.getRewardModel(this->objectives[objIndex].rewardModelName); STORM_LOG_ASSERT(!rewModel.hasTransitionRewards(), "Reward model has transition rewards which is not expected."); this->discreteActionRewards[objIndex] = rewModel.getTotalRewardVector(this->model.getTransitionMatrix()); @@ -34,19 +35,18 @@ namespace storm { std::vector temporaryResult(this->model.getNumberOfStates()); std::vector zeroReward(weightedRewardVector.size(), storm::utility::zero()); // Get for each occurring timeBound the indices of the objectives with that bound. - std::map> lowerTimeBounds; - std::map> upperTimeBounds; - for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { + std::map> stepBounds; + for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { auto const& obj = this->objectives[objIndex]; - if(obj.lowerTimeBound) { - auto timeBoundIt = lowerTimeBounds.insert(std::make_pair(storm::utility::convertNumber(*obj.lowerTimeBound), storm::storage::BitVector(this->objectives.size(), false))).first; - STORM_LOG_WARN_COND(storm::utility::convertNumber(timeBoundIt->first) == (*obj.lowerTimeBound), "Rounded non-integral bound " << *obj.lowerTimeBound << " to " << timeBoundIt->first << "."); - timeBoundIt->second.set(objIndex); - } - if(obj.upperTimeBound) { - auto timeBoundIt = upperTimeBounds.insert(std::make_pair(storm::utility::convertNumber(*obj.upperTimeBound), storm::storage::BitVector(this->objectives.size(), false))).first; - STORM_LOG_WARN_COND(storm::utility::convertNumber(timeBoundIt->first) == (*obj.upperTimeBound), "Rounded non-integral bound " << *obj.upperTimeBound << " to " << timeBoundIt->first << "."); - timeBoundIt->second.set(objIndex); + STORM_LOG_THROW(!obj.lowerTimeBound, storm::exceptions::InvalidPropertyException, "Lower step bounds are not supported by this model checker"); + if (obj.upperTimeBound) { + STORM_LOG_THROW(!obj.upperTimeBound->containsVariables(), storm::exceptions::InvalidPropertyException, "The step bound '" << * obj.upperTimeBound << " contains undefined variables"); + uint_fast64_t stepBound = (uint_fast64_t) obj.upperTimeBound->evaluateAsInt(); + if (obj.upperTimeBoundStrict) { + --stepBound; + } + auto stepBoundIt = stepBounds.insert(std::make_pair(stepBound, storm::storage::BitVector(this->objectives.size(), false))).first; + stepBoundIt->second.set(objIndex); // There is no error for the values of these objectives. this->offsetsToLowerBound[objIndex] = storm::utility::zero(); @@ -60,29 +60,18 @@ namespace storm { // Stores objectives for which the current epoch passed their lower bound storm::storage::BitVector lowerBoundViolatedObjectives(consideredObjectives.size(), false); - auto lowerTimeBoundIt = lowerTimeBounds.begin(); - auto upperTimeBoundIt = upperTimeBounds.begin(); - uint_fast64_t currentEpoch = std::max(lowerTimeBounds.empty() ? 0 : lowerTimeBoundIt->first - 1, upperTimeBounds.empty() ? 0 : upperTimeBoundIt->first); // consider lowerBound - 1 since we are interested in the first epoch that passes the bound + auto stepBoundIt = stepBounds.begin(); + uint_fast64_t currentEpoch = stepBounds.empty() ? 0 : stepBoundIt->first; - while(currentEpoch > 0) { - //For lower time bounds we need to react when the currentEpoch passed the bound - // Hence, we substract 1 from the lower time bounds. - if(lowerTimeBoundIt != lowerTimeBounds.end() && currentEpoch == lowerTimeBoundIt->first - 1) { - lowerBoundViolatedObjectives |= lowerTimeBoundIt->second; - for(auto objIndex : lowerTimeBoundIt->second) { - // No more reward is earned for this objective. - storm::utility::vector::addScaledVector(weightedRewardVector, this->discreteActionRewards[objIndex], -weightVector[objIndex]); - } - ++lowerTimeBoundIt; - } + while (currentEpoch > 0) { - if(upperTimeBoundIt != upperTimeBounds.end() && currentEpoch == upperTimeBoundIt->first) { - consideredObjectives |= upperTimeBoundIt->second; - for(auto objIndex : upperTimeBoundIt->second) { + if (stepBoundIt != stepBounds.end() && currentEpoch == stepBoundIt->first) { + consideredObjectives |= stepBoundIt->second; + for(auto objIndex : stepBoundIt->second) { // This objective now plays a role in the weighted sum storm::utility::vector::addScaledVector(weightedRewardVector, this->discreteActionRewards[objIndex], weightVector[objIndex]); } - ++upperTimeBoundIt; + ++stepBoundIt; } // Get values and scheduler for weighted sum of objectives @@ -92,7 +81,7 @@ namespace storm { // get values for individual objectives // TODO we could compute the result for one of the objectives from the weighted result, the given weight vector, and the remaining objective results. - for(auto objIndex : consideredObjectives) { + for (auto objIndex : consideredObjectives) { std::vector& objectiveResult = this->objectiveResults[objIndex]; std::vector const& objectiveRewards = lowerBoundViolatedObjectives.get(objIndex) ? zeroReward : this->discreteActionRewards[objIndex]; auto rowGroupIndexIt = this->model.getTransitionMatrix().getRowGroupIndices().begin(); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp index 36f4a961b..9e5474362 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp @@ -228,30 +228,16 @@ namespace storm { template void SparsePcaaPreprocessor::preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { - STORM_LOG_THROW(!result.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) || !formula.isStepBounded(), storm::exceptions::InvalidPropertyException, "Multi-objective model checking currently does not support step-bounded properties for Markov automata."); + STORM_LOG_THROW(!result.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) || !formula.isStepBounded(), storm::exceptions::InvalidPropertyException, "Multi-objective model checking currently does not support STEP-bounded properties for Markov automata."); if (formula.hasLowerBound()) { - STORM_LOG_THROW(!result.originalModel.isOfType(storm::models::ModelType::Mdp) || formula.hasIntegerLowerBound(), storm::exceptions::InvalidPropertyException, "Expected discrete lower time-bound in formula."); - // FIXME: really convert formula bound to value type? - if (formula.hasIntegerLowerBound()) { - currentObjective.lowerTimeBound = storm::utility::convertNumber(formula.getLowerBound()); - } else { - currentObjective.lowerTimeBound = storm::utility::convertNumber(formula.getLowerBound()); - } + currentObjective.lowerTimeBound = formula.getLowerBound(); + currentObjective.lowerTimeBoundStrict = formula.isLowerBoundStrict(); } if (formula.hasUpperBound()) { - STORM_LOG_THROW(!result.originalModel.isOfType(storm::models::ModelType::Mdp) || formula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Expected discrete lower time-bound in formula."); - // FIXME: really convert formula bound to value type? - if (formula.hasIntegerUpperBound()) { - currentObjective.upperTimeBound = storm::utility::convertNumber(formula.getUpperBound()); - } else { - currentObjective.upperTimeBound = storm::utility::convertNumber(formula.getUpperBound()); - } - } else { - currentObjective.upperTimeBound = storm::utility::infinity(); + currentObjective.upperTimeBound = formula.getUpperBound(); + currentObjective.upperTimeBoundStrict = formula.isUpperBoundStrict(); } - STORM_LOG_THROW(currentObjective.lowerTimeBound < currentObjective.upperTimeBound, storm::exceptions::InvalidPropertyException, "Empty or point time intervals are currently not supported by multi-objective model checking."); - preprocessUntilFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), result, currentObjective); } @@ -318,9 +304,8 @@ namespace storm { template void SparsePcaaPreprocessor::preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, ReturnType& result, PcaaObjective& currentObjective, boost::optional const& optionalRewardModelName) { STORM_LOG_THROW(result.originalModel.isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidPropertyException, "Cumulative reward formulas are not supported for the given model type."); - STORM_LOG_THROW(formula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Expected a cumulativeRewardFormula with a discrete time bound but got " << formula << "."); - // FIXME: really convert to value type? - currentObjective.upperTimeBound = storm::utility::convertNumber(formula.getBound()); + currentObjective.upperTimeBound = formula.getBound(); + currentObjective.upperTimeBoundStrict = formula.isBoundStrict(); RewardModelType objectiveRewards = result.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : ""); objectiveRewards.reduceToStateBasedRewards(result.preprocessedModel.getTransitionMatrix(), false); diff --git a/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp index 324d8d1d6..ea6320bda 100644 --- a/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp @@ -21,17 +21,17 @@ namespace storm { template std::unique_ptr HybridQuantitativeCheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const { - storm::dd::Bdd symbolicResult; - + storm::dd::Bdd symbolicResult = symbolicStates; + // First compute the symbolic part of the result. if (comparisonType == storm::logic::ComparisonType::Less) { - symbolicResult = symbolicValues.less(bound); + symbolicResult &= symbolicValues.less(bound); } else if (comparisonType == storm::logic::ComparisonType::LessEqual) { - symbolicResult = symbolicValues.lessOrEqual(bound); + symbolicResult &= symbolicValues.lessOrEqual(bound); } else if (comparisonType == storm::logic::ComparisonType::Greater) { - symbolicResult = symbolicValues.greater(bound); + symbolicResult &= symbolicValues.greater(bound); } else if (comparisonType == storm::logic::ComparisonType::GreaterEqual) { - symbolicResult = symbolicValues.greaterOrEqual(bound); + symbolicResult &= symbolicValues.greaterOrEqual(bound); } // Then translate the explicit part to a symbolic format and simultaneously to a qualitative result. 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);