diff --git a/CHANGELOG.md b/CHANGELOG.md index b05097073..88296152d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,26 +8,35 @@ Version 1.3.x ------------- ### Version 1.3.1 (under development) -- Added support for multi-dimensional quantile queries -- Allow to quickly check a benchmark from the [Quantitative Verification Benchmark Set](http://qcomp.org/benchmarks/) using the --qvbs option. -- Added script resources/examples/download_qvbs.sh to download the QVBS. +- Added support for multi-dimensional quantile queries. +- Allow to quickly check a benchmark from the [Quantitative Verification Benchmark Set](http://qcomp.org/benchmarks/) using the `--qvbs` option. +- Added script `resources/examples/download_qvbs.sh` to download the QVBS. - If an option is unknown, Storm now suggests similar option names. - Flagged several options as 'advanced' to clean up the `--help`-message. Use `--help all` to display a complete list of options. -- Support for the new `round` operator in the PRISM language -- Support for parsing of exact time bounds for properties, e.g., `P=? [F=27 "goal"]` -- Export of optimal schedulers when checking MDPs with the sparse engine (experimental). Use `--exportscheduler ` -- JANI: Allow bounded types for constants +- Support for the new `round` operator in the PRISM language. +- Support for parsing of exact time bounds for properties, e.g., `P=? [F=27 "goal"]`. +- Export of optimal schedulers when checking MDPs with the sparse engine (experimental). Use `--exportscheduler `. +- JANI: Allow bounded types for constants. - JANI: Support for non-trivial reward accumulations. - JANI: Fixed support for reward expressions over non-transient variables. -- DRN: Added support for exact parsing and action-based rewards -- storm-conv can now apply transformations on a prism file -- Fixed sparse bisimulation of MDPs (which failed if all non-absorbing states in the quotient are initial) -- Fixed linking with Mathsat on macOS -- Fixed compilation for macOS mojave -- Support for export of MTBDDs from storm -- Support for monotonicity checking of pMCs using the `--monotonicity-analysis` option. Use `--help monotonicity` for all options. - -### Version 1.3.0 (2018/12) +- DRN: Added support for exact parsing and action-based rewards. +- DRN: Support for placeholder variables which allows to parse recurring rational functions only once. +- Fixed sparse bisimulation of MDPs (which failed if all non-absorbing states in the quotient are initial). +- Support for export of MTBDDs from Storm. +- Support for k-shortest path counterexamples (arguments `-cex --cextype shortestpath`) +- New settings module `transformation` for Markov chain transformations. Use `--help transformation` to get a list of available transformations. +- Support for eliminating chains of Non-Markovian states in MAs via `--eliminate-chains`. +- Export to dot format allows for maximal line width in states (argument `--dot-maxwidth `) +- `storm-conv` can now apply transformations on a prism file. +- `storm-dft`: Support partial-order for state space generation. +- `storm-dft`: Compute lower and upper bounds for number of BE failures via SMT. +- `storm-dft`: Support for constant failed BEs. Use flag `--uniquefailedbe` to create a unique constant failed BE. +- `storm-dft`: Support for probabilistic BEs via PDEPs. +- Fixed linking with Mathsat on macOS. +- Fixed compilation for macOS Mojave. +- Several bug fixes. + +## Version 1.3.0 (2018/12) - Slightly improved scheduler extraction - Environments are now part of the c++ API - Heavily extended JANI support, in particular: diff --git a/resources/doxygen/CMakeLists.txt b/resources/doxygen/CMakeLists.txt index 6105db27f..4be483a24 100644 --- a/resources/doxygen/CMakeLists.txt +++ b/resources/doxygen/CMakeLists.txt @@ -7,30 +7,34 @@ find_package(Doxygen) # Add a target to generate API documentation with Doxygen if(DOXYGEN_FOUND) - # We use the doxygen command of CMake instead of using the separate config file - set(DOXYGEN_PROJECT_NAME "Storm") - set(DOXYGEN_PROJECT_BRIEF "A Modern Probabilistic Model Checker") - set(DOXYGEN_BRIEF_MEMBER_DESC YES) - set(DOXYGEN_REPEAT_BRIEF YES) - set(DOXYGEN_JAVADOC_AUTOBRIEF YES) - set(DOXYGEN_QT_AUTOBRIEF YES) - set(DOXYGEN_EXTRACT_ALL YES) - set(DOXYGEN_EXTRACT_STATIC YES) - set(DOXYGEN_SOURCE_BROWSER YES) - set(DOXYGEN_GENERATE_TREEVIEW YES) - set(DOXYGEN_CASE_SENSE_NAMES NO) - set(DOXYGEN_HTML_TIMESTAMP YES) - set(DOXYGEN_CREATE_SUBDIRS YES) - set(DOXYGEN_OUTPUT_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/doc") - doxygen_add_docs( - doc - "${PROJECT_SOURCE_DIR}/src" - COMMENT "Generating API documentation with Doxygen" - ) + if(${CMAKE_VERSION} VERSION_LESS "3.9.0") + # Use old commands if CMake does not support the command doxygen_add_docs + set(CMAKE_DOXYGEN_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/doc") + string(REGEX REPLACE ";" " " CMAKE_DOXYGEN_INPUT_LIST "${PROJECT_SOURCE_DIR}/src") + configure_file("${CMAKE_CURRENT_SOURCE_DIR}/resources/doxygen/Doxyfile.in" "${CMAKE_CURRENT_BINARY_DIR}/Doxyfile" @ONLY) + add_custom_target(doc ${DOXYGEN_EXECUTABLE} "${CMAKE_CURRENT_BINARY_DIR}/Doxyfile" DEPENDS "${CMAKE_CURRENT_BINARY_DIR}/Doxyfile" COMMENT "Generating API documentation with Doxygen" VERBATIM) + else() + + # We use the doxygen command of CMake instead of using the separate config file + set(DOXYGEN_PROJECT_NAME "Storm") + set(DOXYGEN_PROJECT_BRIEF "A Modern Probabilistic Model Checker") + set(DOXYGEN_BRIEF_MEMBER_DESC YES) + set(DOXYGEN_REPEAT_BRIEF YES) + set(DOXYGEN_JAVADOC_AUTOBRIEF YES) + set(DOXYGEN_QT_AUTOBRIEF YES) + set(DOXYGEN_EXTRACT_ALL YES) + set(DOXYGEN_EXTRACT_STATIC YES) + set(DOXYGEN_SOURCE_BROWSER YES) + set(DOXYGEN_GENERATE_TREEVIEW YES) + set(DOXYGEN_CASE_SENSE_NAMES NO) + set(DOXYGEN_HTML_TIMESTAMP YES) + set(DOXYGEN_CREATE_SUBDIRS YES) + set(DOXYGEN_OUTPUT_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/doc") + doxygen_add_docs( + doc + "${PROJECT_SOURCE_DIR}/src" + COMMENT "Generating API documentation with Doxygen" + ) + endif() - # These commands can be used if the separate config files should be used - #set(CMAKE_DOXYGEN_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/doc") - #string(REGEX REPLACE ";" " " CMAKE_DOXYGEN_INPUT_LIST "${PROJECT_SOURCE_DIR}/src") - #configure_file("${CMAKE_CURRENT_SOURCE_DIR}/resources/doxygen/Doxyfile.in.new" "${CMAKE_CURRENT_BINARY_DIR}/Doxyfile" @ONLY) - #add_custom_target(doc ${DOXYGEN_EXECUTABLE} "${CMAKE_CURRENT_BINARY_DIR}/Doxyfile" DEPENDS "${CMAKE_CURRENT_BINARY_DIR}/Doxyfile" COMMENT "Generating API documentation with Doxygen" VERBATIM) endif(DOXYGEN_FOUND) diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 6613030a2..1dc8a2370 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -268,12 +268,14 @@ namespace storm { storm::builder::BuilderOptions options(createFormulasToRespect(input.properties), input.model.get()); options.setBuildChoiceLabels(buildSettings.isBuildChoiceLabelsSet()); options.setBuildStateValuations(buildSettings.isBuildStateValuationsSet()); + bool buildChoiceOrigins = false; if (storm::settings::manager().hasModule(storm::settings::modules::CounterexampleGeneratorSettings::moduleName)) { auto counterexampleGeneratorSettings = storm::settings::getModule(); - options.setBuildChoiceOrigins(counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet()); - } else { - options.setBuildChoiceOrigins(false); + if (counterexampleGeneratorSettings.isCounterexampleSet()) { + buildChoiceOrigins = counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet(); + } } + options.setBuildChoiceOrigins(buildChoiceOrigins); options.setAddOutOfBoundsState(buildSettings.isBuildOutOfBoundsStateSet()); if (buildSettings.isBuildFullModelSet()) { options.clearTerminalStates(); @@ -326,12 +328,20 @@ namespace storm { template std::shared_ptr> preprocessSparseMarkovAutomaton(std::shared_ptr> const& model) { + auto transformationSettings = storm::settings::getModule(); + std::shared_ptr> result = model; model->close(); if (model->isConvertibleToCtmc()) { STORM_LOG_WARN_COND(false, "MA is convertible to a CTMC, consider using a CTMC instead."); result = model->convertToCtmc(); } + + if (transformationSettings.isChainEliminationSet() && result->isOfType(storm::models::ModelType::MarkovAutomaton)) { + result = storm::transformer::NonMarkovianChainTransformer::eliminateNonmarkovianStates( + result->template as>(), !transformationSettings.isIgnoreLabelingSet()); + } + return result; } @@ -352,17 +362,11 @@ namespace storm { auto bisimulationSettings = storm::settings::getModule(); auto ioSettings = storm::settings::getModule(); auto transformationSettings = storm::settings::getModule(); - + std::pair>, bool> result = std::make_pair(model, false); if (result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) { result.first = preprocessSparseMarkovAutomaton(result.first->template as>()); - if (transformationSettings.isChainEliminationSet() && - result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) { - result.first = storm::transformer::NonMarkovianChainTransformer::eliminateNonmarkovianStates( - result.first->template as>(), - !transformationSettings.isIgnoreLabelingSet()); - } result.second = true; } @@ -395,7 +399,7 @@ namespace storm { } if (ioSettings.isExportDotSet()) { - storm::api::exportSparseModelAsDot(model, ioSettings.getExportDotFilename()); + storm::api::exportSparseModelAsDot(model, ioSettings.getExportDotFilename(), ioSettings.getExportDotMaxWidth()); } } @@ -536,27 +540,41 @@ namespace storm { auto counterexampleSettings = storm::settings::getModule(); if (counterexampleSettings.isMinimalCommandSetGenerationSet()) { - bool useMilp = counterexampleSettings.isUseMilpBasedMinimalCommandSetGenerationSet(); for (auto const& property : input.properties) { std::shared_ptr counterexample; printComputingCounterexample(property); storm::utility::Stopwatch watch(true); if (useMilp) { - STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "Counterexample generation using MILP is currently only supported for MDPs."); - counterexample = storm::api::computeHighLevelCounterexampleMilp(input.model.get(), sparseModel->template as>(), property.getRawFormula()); + STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, + "Counterexample generation using MILP is currently only supported for MDPs."); + counterexample = storm::api::computeHighLevelCounterexampleMilp(input.model.get(), sparseModel->template as>(), + property.getRawFormula()); } else { - STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Dtmc) || sparseModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "Counterexample generation using MaxSAT is currently only supported for discrete-time models."); + STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Dtmc) || sparseModel->isOfType(storm::models::ModelType::Mdp), + storm::exceptions::NotSupportedException, "Counterexample generation using MaxSAT is currently only supported for discrete-time models."); if (sparseModel->isOfType(storm::models::ModelType::Dtmc)) { - counterexample = storm::api::computeHighLevelCounterexampleMaxSmt(input.model.get(), sparseModel->template as>(), property.getRawFormula()); + counterexample = storm::api::computeHighLevelCounterexampleMaxSmt(input.model.get(), sparseModel->template as>(), + property.getRawFormula()); } else { - counterexample = storm::api::computeHighLevelCounterexampleMaxSmt(input.model.get(), sparseModel->template as>(), property.getRawFormula()); + counterexample = storm::api::computeHighLevelCounterexampleMaxSmt(input.model.get(), sparseModel->template as>(), + property.getRawFormula()); } } watch.stop(); printCounterexample(counterexample, &watch); } + } else if (counterexampleSettings.isShortestPathGenerationSet()) { + for (auto const& property : input.properties) { + std::shared_ptr counterexample; + printComputingCounterexample(property); + storm::utility::Stopwatch watch(true); + STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Dtmc), storm::exceptions::NotSupportedException, "Counterexample generation using shortest paths is currently only supported for DTMCs."); + counterexample = storm::api::computeKShortestPathCounterexample(sparseModel->template as>(), property.getRawFormula(), counterexampleSettings.getShortestPathMaxK()); + watch.stop(); + printCounterexample(counterexample, &watch); + } } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The selected counterexample formalism is unsupported."); } @@ -927,6 +945,7 @@ namespace storm { void processInputWithValueTypeAndDdlib(SymbolicInput const& input) { auto coreSettings = storm::settings::getModule(); auto abstractionSettings = storm::settings::getModule(); + auto counterexampleSettings = storm::settings::getModule(); // For several engines, no model building step is performed, but the verification is started right away. storm::settings::modules::CoreSettings::Engine engine = coreSettings.getEngine(); @@ -939,11 +958,9 @@ namespace storm { std::shared_ptr model = buildPreprocessExportModelWithValueTypeAndDdlib(input, engine); if (model) { - if (coreSettings.isCounterexampleSet()) { - auto ioSettings = storm::settings::getModule(); + if (counterexampleSettings.isCounterexampleSet()) { generateCounterexamples(model, input); } else { - auto ioSettings = storm::settings::getModule(); verifyModel(model, input, coreSettings); } } diff --git a/src/storm-counterexamples/api/counterexamples.cpp b/src/storm-counterexamples/api/counterexamples.cpp index 5652beba6..f0927c869 100644 --- a/src/storm-counterexamples/api/counterexamples.cpp +++ b/src/storm-counterexamples/api/counterexamples.cpp @@ -1,19 +1,65 @@ #include "storm-counterexamples/api/counterexamples.h" #include "storm/environment/Environment.h" +#include "storm/utility/shortestPaths.h" namespace storm { namespace api { - - std::shared_ptr computeHighLevelCounterexampleMilp(storm::storage::SymbolicModelDescription const& symbolicModel, std::shared_ptr> mdp, std::shared_ptr const& formula) { + + std::shared_ptr + computeHighLevelCounterexampleMilp(storm::storage::SymbolicModelDescription const& symbolicModel, std::shared_ptr> mdp, + std::shared_ptr const& formula) { Environment env; return storm::counterexamples::MILPMinimalLabelSetGenerator::computeCounterexample(env, symbolicModel, *mdp, formula); } - - std::shared_ptr computeHighLevelCounterexampleMaxSmt(storm::storage::SymbolicModelDescription const& symbolicModel, std::shared_ptr> model, std::shared_ptr const& formula) { + + std::shared_ptr + computeHighLevelCounterexampleMaxSmt(storm::storage::SymbolicModelDescription const& symbolicModel, std::shared_ptr> model, + std::shared_ptr const& formula) { Environment env; return storm::counterexamples::SMTMinimalLabelSetGenerator::computeCounterexample(env, symbolicModel, *model, formula); } - + + std::shared_ptr + computeKShortestPathCounterexample(std::shared_ptr> model, std::shared_ptr const& formula, size_t maxK) { + // Only accept formulas of the form "P isProbabilityOperatorFormula(), storm::exceptions::InvalidPropertyException, + "Counterexample generation does not support this kind of formula. Expecting a probability operator as the outermost formula element."); + storm::logic::ProbabilityOperatorFormula const& probabilityOperator = formula->asProbabilityOperatorFormula(); + STORM_LOG_THROW(probabilityOperator.hasBound(), storm::exceptions::InvalidPropertyException, "Counterexample generation only supports bounded formulas."); + STORM_LOG_THROW(!storm::logic::isLowerBound(probabilityOperator.getComparisonType()), storm::exceptions::InvalidPropertyException, + "Counterexample generation only supports upper bounds."); + double threshold = probabilityOperator.getThresholdAs(); + storm::logic::Formula const& subformula = formula->asOperatorFormula().getSubformula(); + STORM_LOG_THROW(subformula.isEventuallyFormula(), storm::exceptions::InvalidPropertyException, + "Path formula is required to be of the form 'F psi' for counterexample generation."); + bool strictBound = (probabilityOperator.getComparisonType() == storm::logic::ComparisonType::Greater); + + // Perform model checking to get target states + Environment env; + storm::modelchecker::SparsePropositionalModelChecker> modelchecker(*model); + + storm::logic::EventuallyFormula const& eventuallyFormula = subformula.asEventuallyFormula(); + std::unique_ptr subResult = modelchecker.check(env, eventuallyFormula.getSubformula()); + storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult->asExplicitQualitativeCheckResult(); + + auto generator = storm::utility::ksp::ShortestPathsGenerator(*model, subQualitativeResult.getTruthValuesVector()); + storm::counterexamples::PathCounterexample cex(model); + double probability = 0; + bool thresholdExceeded = false; + for (size_t k = 1; k <= maxK; ++k) { + cex.addPath(generator.getPathAsList(k), k); + probability += generator.getDistance(k); + // Check if accumulated probability mass is already enough + if ((probability >= threshold && !strictBound) || (probability > threshold)) { + thresholdExceeded = true; + break; + } + } + STORM_LOG_WARN_COND(thresholdExceeded, "Aborted computation because maximal number of paths was reached. Probability threshold is not yet exceeded."); + + return std::make_shared>(cex); + } + } } diff --git a/src/storm-counterexamples/api/counterexamples.h b/src/storm-counterexamples/api/counterexamples.h index 6a5984991..4e0a9f931 100644 --- a/src/storm-counterexamples/api/counterexamples.h +++ b/src/storm-counterexamples/api/counterexamples.h @@ -2,6 +2,7 @@ #include "storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h" #include "storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h" +#include "storm-counterexamples/counterexamples/PathCounterexample.h" namespace storm { namespace api { @@ -9,6 +10,8 @@ namespace storm { std::shared_ptr computeHighLevelCounterexampleMilp(storm::storage::SymbolicModelDescription const& symbolicModel, std::shared_ptr> mdp, std::shared_ptr const& formula); std::shared_ptr computeHighLevelCounterexampleMaxSmt(storm::storage::SymbolicModelDescription const& symbolicModel, std::shared_ptr> model, std::shared_ptr const& formula); - + + std::shared_ptr computeKShortestPathCounterexample(std::shared_ptr> model, std::shared_ptr const& formula, size_t maxK); + } } diff --git a/src/storm-counterexamples/counterexamples/GuaranteedLabelSet.h b/src/storm-counterexamples/counterexamples/GuaranteedLabelSet.h new file mode 100644 index 000000000..da1696517 --- /dev/null +++ b/src/storm-counterexamples/counterexamples/GuaranteedLabelSet.h @@ -0,0 +1,125 @@ +#pragma once + +#include +#include + +#include "storm/exceptions/InvalidArgumentException.h" +#include "storm/models/sparse/Model.h" +#include "storm/storage/sparse/PrismChoiceOrigins.h" + +namespace storm { + namespace counterexamples { + + /*! + * Computes a set of labels that is executed along all paths from any state to a target state. + * + * @param labelSet the considered label sets (a label set is assigned to each choice) + * + * @return The set of labels that is visited on all paths from any state to a target state. + */ + template + std::vector> getGuaranteedLabelSets(storm::models::sparse::Model const& model, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, storm::storage::FlatSet const& relevantLabels) { + STORM_LOG_THROW(model.getNumberOfChoices() == labelSets.size(), storm::exceptions::InvalidArgumentException, "The given number of labels does not match the number of choices."); + + // Get some data from the model for convenient access. + storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); + std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); + + // Now we compute the set of labels that is present on all paths from the initial to the target states. + std::vector> analysisInformation(model.getNumberOfStates(), relevantLabels); + + std::queue worklist; + storm::storage::BitVector statesInWorkList(model.getNumberOfStates()); + storm::storage::BitVector markedStates(model.getNumberOfStates()); + + // Initially, put all predecessors of target states in the worklist and empty the analysis information them. + for (auto state : psiStates) { + analysisInformation[state] = storm::storage::FlatSet(); + for (auto const& predecessorEntry : backwardTransitions.getRow(state)) { + if (predecessorEntry.getColumn() != state && !statesInWorkList.get(predecessorEntry.getColumn()) && !psiStates.get(predecessorEntry.getColumn())) { + worklist.push(predecessorEntry.getColumn()); + statesInWorkList.set(predecessorEntry.getColumn()); + markedStates.set(state); + } + } + } + + uint_fast64_t iters = 0; + while (!worklist.empty()) { + ++iters; + uint_fast64_t const& currentState = worklist.front(); + + size_t analysisInformationSizeBefore = analysisInformation[currentState].size(); + + // Iterate over the successor states for all choices and compute new analysis information. + for (uint_fast64_t currentChoice = nondeterministicChoiceIndices[currentState]; currentChoice < nondeterministicChoiceIndices[currentState + 1]; ++currentChoice) { + bool modifiedChoice = false; + + for (auto const& entry : transitionMatrix.getRow(currentChoice)) { + if (markedStates.get(entry.getColumn())) { + modifiedChoice = true; + break; + } + } + + // If we can reach the target state with this choice, we need to intersect the current + // analysis information with the union of the new analysis information of the target state + // and the choice labels. + if (modifiedChoice) { + for (auto const& entry : transitionMatrix.getRow(currentChoice)) { + if (markedStates.get(entry.getColumn())) { + storm::storage::FlatSet tmpIntersection; + std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), analysisInformation[entry.getColumn()].begin(), analysisInformation[entry.getColumn()].end(), std::inserter(tmpIntersection, tmpIntersection.begin())); + std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), labelSets[currentChoice].begin(), labelSets[currentChoice].end(), std::inserter(tmpIntersection, tmpIntersection.begin())); + analysisInformation[currentState] = std::move(tmpIntersection); + } + } + } + } + + // If the analysis information changed, we need to update it and put all the predecessors of this + // state in the worklist. + if (analysisInformation[currentState].size() != analysisInformationSizeBefore) { + for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) { + // Only put the predecessor in the worklist if it's not already a target state. + if (!psiStates.get(predecessorEntry.getColumn()) && !statesInWorkList.get(predecessorEntry.getColumn())) { + worklist.push(predecessorEntry.getColumn()); + statesInWorkList.set(predecessorEntry.getColumn()); + } + } + markedStates.set(currentState, true); + } else { + markedStates.set(currentState, false); + } + + worklist.pop(); + statesInWorkList.set(currentState, false); + } + + return analysisInformation; + } + + /*! + * Computes a set of labels that is executed along all paths from an initial state to a target state. + * + * @param labelSet the considered label sets (a label set is assigned to each choice) + * + * @return The set of labels that is executed on all paths from an initial state to a target state. + */ + template + storm::storage::FlatSet getGuaranteedLabelSet(storm::models::sparse::Model const& model, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, storm::storage::FlatSet const& relevantLabels) { + std::vector> guaranteedLabels = getGuaranteedLabelSets(model, labelSets, psiStates, relevantLabels); + + storm::storage::FlatSet knownLabels(relevantLabels); + storm::storage::FlatSet tempIntersection; + for (auto initialState : model.getInitialStates()) { + std::set_intersection(knownLabels.begin(), knownLabels.end(), guaranteedLabels[initialState].begin(), guaranteedLabels[initialState].end(), std::inserter(tempIntersection, tempIntersection.end())); + std::swap(knownLabels, tempIntersection); + } + + return knownLabels; + } + + } // namespace counterexample +} // namespace storm diff --git a/src/storm-counterexamples/counterexamples/HighLevelCounterexample.h b/src/storm-counterexamples/counterexamples/HighLevelCounterexample.h index 27fe981c0..4ce432a8f 100644 --- a/src/storm-counterexamples/counterexamples/HighLevelCounterexample.h +++ b/src/storm-counterexamples/counterexamples/HighLevelCounterexample.h @@ -1,7 +1,6 @@ #pragma once -#include "Counterexample.h" - +#include "storm-counterexamples/counterexamples/Counterexample.h" #include "storm/storage/SymbolicModelDescription.h" namespace storm { diff --git a/src/storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h b/src/storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h index a2e6de197..d7186c95c 100644 --- a/src/storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h @@ -2,9 +2,16 @@ #include +#include "storm-counterexamples/counterexamples/GuaranteedLabelSet.h" +#include "storm-counterexamples/counterexamples/HighLevelCounterexample.h" +#include "storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h" + #include "storm/models/sparse/Mdp.h" #include "storm/logic/Formulas.h" #include "storm/storage/prism/Program.h" +#include "storm/storage/sparse/PrismChoiceOrigins.h" +#include "storm/storage/sparse/JaniChoiceOrigins.h" +#include "storm/storage/BoostTypes.h" #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" @@ -13,23 +20,12 @@ #include "storm/exceptions/InvalidPropertyException.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/InvalidStateException.h" - #include "storm/solver/MinMaxLinearEquationSolver.h" - -#include "storm-counterexamples/counterexamples/HighLevelCounterexample.h" - +#include "storm/solver/LpSolver.h" #include "storm/utility/graph.h" -#include "storm/utility/counterexamples.h" #include "storm/utility/solver.h" -#include "storm/solver/LpSolver.h" - -#include "storm/storage/sparse/PrismChoiceOrigins.h" -#include "storm/storage/sparse/JaniChoiceOrigins.h" -#include "storm/storage/BoostTypes.h" - #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GeneralSettings.h" -#include "storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h" namespace storm { @@ -167,7 +163,7 @@ namespace storm { } // Finally, determine the set of labels that are known to be taken. - result.knownLabels = storm::utility::counterexamples::getGuaranteedLabelSet(mdp, labelSets, psiStates, result.allRelevantLabels); + result.knownLabels = storm::counterexamples::getGuaranteedLabelSet(mdp, labelSets, psiStates, result.allRelevantLabels); STORM_LOG_DEBUG("Found " << result.allRelevantLabels.size() << " relevant labels and " << result.knownLabels.size() << " known labels."); return result; diff --git a/src/storm-counterexamples/counterexamples/PathCounterexample.cpp b/src/storm-counterexamples/counterexamples/PathCounterexample.cpp new file mode 100644 index 000000000..5d8f18762 --- /dev/null +++ b/src/storm-counterexamples/counterexamples/PathCounterexample.cpp @@ -0,0 +1,40 @@ +#include "storm-counterexamples/counterexamples/PathCounterexample.h" + +#include "storm/utility/export.h" + +namespace storm { + namespace counterexamples { + + template + PathCounterexample::PathCounterexample(std::shared_ptr> model) : model(model) { + // Intentionally left empty. + } + + template + void PathCounterexample::addPath(std::vector path, size_t k) { + if (k >= shortestPaths.size()) { + shortestPaths.resize(k); + } + shortestPaths[k-1] = path; + } + + template + void PathCounterexample::writeToStream(std::ostream& out) const { + out << "Shortest path counterexample with k = " << shortestPaths.size() << " paths: " << std::endl; + for (size_t i = 0; i < shortestPaths.size(); ++i) { + out << i+1 << "-shortest path: " << std::endl; + for (auto it = shortestPaths[i].rbegin(); it != shortestPaths[i].rend(); ++it) { + out << "\tstate " << *it; + if (model->hasStateValuations()) { + out << ": "<< model->getStateValuations().getStateInfo(*it); + } + out << ": {"; + storm::utility::outputFixedWidth(out, model->getLabelsOfState(*it), 0); + out << "}" << std::endl; + } + } + } + + template class PathCounterexample; + } +} diff --git a/src/storm-counterexamples/counterexamples/PathCounterexample.h b/src/storm-counterexamples/counterexamples/PathCounterexample.h new file mode 100644 index 000000000..41543687d --- /dev/null +++ b/src/storm-counterexamples/counterexamples/PathCounterexample.h @@ -0,0 +1,25 @@ +#pragma once + +#include "storm-counterexamples/counterexamples/Counterexample.h" + +#include "storm/models/sparse/Model.h" + +namespace storm { + namespace counterexamples { + + template + class PathCounterexample : public Counterexample { + public: + PathCounterexample(std::shared_ptr> model); + + void addPath(std::vector path, size_t k); + + void writeToStream(std::ostream& out) const override; + + private: + std::shared_ptr> model; + std::vector> shortestPaths; + }; + + } +} diff --git a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h index 9a66982b0..66e27fa78 100644 --- a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h @@ -3,10 +3,11 @@ #include #include -#include "storm/solver/Z3SmtSolver.h" - +#include "storm-counterexamples/counterexamples/GuaranteedLabelSet.h" #include "storm-counterexamples/counterexamples/HighLevelCounterexample.h" +#include "storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h" +#include "storm/solver/Z3SmtSolver.h" #include "storm/storage/prism/Program.h" #include "storm/storage/expressions/Expression.h" #include "storm/storage/sparse/PrismChoiceOrigins.h" @@ -17,13 +18,10 @@ #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/CoreSettings.h" -#include "storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h" - +#include "storm/utility/cli.h" #include "storm/utility/macros.h" #include "storm/exceptions/NotSupportedException.h" -#include "storm/utility/counterexamples.h" -#include "storm/utility/cli.h" namespace storm { @@ -165,7 +163,7 @@ namespace storm { } // Compute the set of labels that are known to be taken in any case. - relevancyInformation.knownLabels = storm::utility::counterexamples::getGuaranteedLabelSet(model, labelSets, psiStates, relevancyInformation.relevantLabels); + relevancyInformation.knownLabels = storm::counterexamples::getGuaranteedLabelSet(model, labelSets, psiStates, relevancyInformation.relevantLabels); if (!relevancyInformation.knownLabels.empty()) { storm::storage::FlatSet remainingLabels; std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(remainingLabels, remainingLabels.end())); @@ -1349,7 +1347,7 @@ namespace storm { storm::storage::FlatSet locallyRelevantLabels; std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), commandSet.begin(), commandSet.end(), std::inserter(locallyRelevantLabels, locallyRelevantLabels.begin())); - std::vector> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalModel, originalLabelSets, statesThatCanReachTargetStates, locallyRelevantLabels); + std::vector> guaranteedLabelSets = storm::counterexamples::getGuaranteedLabelSets(originalModel, originalLabelSets, statesThatCanReachTargetStates, locallyRelevantLabels); STORM_LOG_DEBUG("Found " << reachableLabels.size() << " reachable labels and " << reachableStates.getNumberOfSetBits() << " reachable states."); // Search for states on the border of the reachable state space, i.e. states that are still reachable @@ -1466,7 +1464,7 @@ namespace storm { storm::storage::FlatSet locallyRelevantLabels; std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), commandSet.begin(), commandSet.end(), std::inserter(locallyRelevantLabels, locallyRelevantLabels.begin())); - std::vector> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalModel, originalLabelSets, statesThatCanReachTargetStates, locallyRelevantLabels); + std::vector> guaranteedLabelSets = storm::counterexamples::getGuaranteedLabelSets(originalModel, originalLabelSets, statesThatCanReachTargetStates, locallyRelevantLabels); // Search for states for which we could enable another option and possibly improve the reachability probability. std::set> cutLabels; diff --git a/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp b/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp index 27a2c1120..752da88be 100644 --- a/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp +++ b/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp @@ -13,30 +13,56 @@ namespace storm { namespace modules { const std::string CounterexampleGeneratorSettings::moduleName = "counterexample"; - const std::string CounterexampleGeneratorSettings::minimalCommandSetOptionName = "mincmd"; + const std::string CounterexampleGeneratorSettings::counterexampleOptionName = "counterexample"; + const std::string CounterexampleGeneratorSettings::counterexampleOptionShortName = "cex"; + const std::string CounterexampleGeneratorSettings::counterexampleTypeOptionName = "cextype"; + const std::string CounterexampleGeneratorSettings::shortestPathMaxKOptionName = "shortestpath-maxk"; + const std::string CounterexampleGeneratorSettings::minimalCommandMethodOptionName = "mincmdmethod"; const std::string CounterexampleGeneratorSettings::encodeReachabilityOptionName = "encreach"; const std::string CounterexampleGeneratorSettings::schedulerCutsOptionName = "schedcuts"; const std::string CounterexampleGeneratorSettings::noDynamicConstraintsOptionName = "nodyn"; CounterexampleGeneratorSettings::CounterexampleGeneratorSettings() : ModuleSettings(moduleName) { - std::vector techniques = {"maxsat", "milp"}; - this->addOption(storm::settings::OptionBuilder(moduleName, minimalCommandSetOptionName, true, "Computes a counterexample for the given model in terms of a minimal command/edge set. Note that this requires the model to be given in a symbolic format.").setIsAdvanced() - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used to derive the counterexample.").setDefaultValueString("maxsat").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(techniques)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, counterexampleOptionName, false, "Generates a counterexample for the given PRCTL formulas if not satisfied by the model.").setShortName(counterexampleOptionShortName).build()); + std::vector cextype = {"mincmd", "shortestpath"}; + this->addOption(storm::settings::OptionBuilder(moduleName, counterexampleTypeOptionName, false, "Generates a counterexample of the given type if the given PRCTL formula is not satisfied by the model.").setIsAdvanced() + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("type", "The type of the counterexample to compute.").setDefaultValueString("mincmd").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(cextype)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, shortestPathMaxKOptionName, false, "Maximal number K of shortest paths to generate.").setIsAdvanced() + .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("maxk", "Upper bound on number of generated paths. Default value is 10.").setDefaultValueUnsignedInteger(10).build()).build()); + std::vector method = {"maxsat", "milp"}; + this->addOption(storm::settings::OptionBuilder(moduleName, minimalCommandMethodOptionName, true, "Sets which method is used to derive the counterexample in terms of a minimal command/edge set.").setIsAdvanced() + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "The name of the method to use.").setDefaultValueString("maxsat").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(method)).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, encodeReachabilityOptionName, true, "Sets whether to encode reachability for MAXSAT-based counterexample generation.").setIsAdvanced().build()); this->addOption(storm::settings::OptionBuilder(moduleName, schedulerCutsOptionName, true, "Sets whether to add the scheduler cuts for MILP-based counterexample generation.").setIsAdvanced().build()); this->addOption(storm::settings::OptionBuilder(moduleName, noDynamicConstraintsOptionName, true, "Disables the generation of dynamic constraints in the MAXSAT-based counterexample generation.").setIsAdvanced().build()); } - + + bool CounterexampleGeneratorSettings::isCounterexampleSet() const { + return this->getOption(counterexampleOptionName).getHasOptionBeenSet(); + } + + bool CounterexampleGeneratorSettings::isCounterexampleTypeSet() const { + return this->getOption(counterexampleTypeOptionName).getHasOptionBeenSet(); + } + bool CounterexampleGeneratorSettings::isMinimalCommandSetGenerationSet() const { - return this->getOption(minimalCommandSetOptionName).getHasOptionBeenSet(); + return this->getOption(counterexampleTypeOptionName).getArgumentByName("type").getValueAsString() == "mincmd"; + } + + bool CounterexampleGeneratorSettings::isShortestPathGenerationSet() const { + return this->getOption(counterexampleTypeOptionName).getArgumentByName("type").getValueAsString() == "shortestpath"; + } + + size_t CounterexampleGeneratorSettings::getShortestPathMaxK() const { + return this->getOption(shortestPathMaxKOptionName).getArgumentByName("maxk").getValueAsUnsignedInteger(); } bool CounterexampleGeneratorSettings::isUseMilpBasedMinimalCommandSetGenerationSet() const { - return this->getOption(minimalCommandSetOptionName).getArgumentByName("method").getValueAsString() == "milp"; + return this->getOption(minimalCommandMethodOptionName).getArgumentByName("method").getValueAsString() == "milp"; } bool CounterexampleGeneratorSettings::isUseMaxSatBasedMinimalCommandSetGenerationSet() const { - return this->getOption(minimalCommandSetOptionName).getArgumentByName("method").getValueAsString() == "maxsat"; + return this->getOption(minimalCommandMethodOptionName).getArgumentByName("method").getValueAsString() == "maxsat"; } bool CounterexampleGeneratorSettings::isEncodeReachabilitySet() const { @@ -52,8 +78,9 @@ namespace storm { } bool CounterexampleGeneratorSettings::check() const { + STORM_LOG_THROW(isCounterexampleSet() || !isCounterexampleTypeSet(), storm::exceptions::InvalidSettingsException, "Counterexample type was set but counterexample flag '-cex' is missing."); // Ensure that the model was given either symbolically or explicitly. - STORM_LOG_THROW(!isMinimalCommandSetGenerationSet() || storm::settings::getModule().isPrismInputSet() || storm::settings::getModule().isJaniInputSet(), storm::exceptions::InvalidSettingsException, "For the generation of a minimal command set, the model has to be specified in the PRISM/JANI format."); + STORM_LOG_THROW(!isCounterexampleSet() || !isMinimalCommandSetGenerationSet() || storm::settings::getModule().isPrismInputSet() || storm::settings::getModule().isJaniInputSet(), storm::exceptions::InvalidSettingsException, "For the generation of a minimal command set, the model has to be specified in the PRISM/JANI format."); if (isMinimalCommandSetGenerationSet()) { STORM_LOG_WARN_COND(isUseMaxSatBasedMinimalCommandSetGenerationSet() || !isEncodeReachabilitySet(), "Encoding reachability is only available for the MaxSat-based minimal command set generation, so selecting it has no effect."); diff --git a/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h b/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h index bdb0813a6..4fa9e77e0 100644 --- a/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h +++ b/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h @@ -16,14 +16,42 @@ namespace storm { * Creates a new set of counterexample settings. */ CounterexampleGeneratorSettings(); - + + /*! + * Retrieves whether the counterexample option was set. + * + * @return True if the counterexample option was set. + */ + bool isCounterexampleSet() const; + + /*! + * Retrieves whether the type of counterexample was set. + * + * @return True if the type of the counterexample was set. + */ + bool isCounterexampleTypeSet() const; + /*! - * Retrieves whether the option to generate a minimal command set was set. + * Retrieves whether the option to generate a minimal command set counterexample was set. * * @return True iff a minimal command set counterexample is to be generated. */ bool isMinimalCommandSetGenerationSet() const; - + + /*! + * Retrieves whether the option to generate a shortest path counterexample was set. + * + * @return True iff a shortest path counterexample is to be generated. + */ + bool isShortestPathGenerationSet() const; + + /*! + * Retrieves the maximal number K of shortest paths which should be generated. + * + * @return The upper bound on the number of shortest paths. + */ + size_t getShortestPathMaxK() const; + /*! * Retrieves whether the MILP-based technique is to be used to generate a minimal command set * counterexample. @@ -70,7 +98,11 @@ namespace storm { private: // Define the string names of the options as constants. - static const std::string minimalCommandSetOptionName; + static const std::string counterexampleOptionName; + static const std::string counterexampleOptionShortName; + static const std::string counterexampleTypeOptionName; + static const std::string shortestPathMaxKOptionName; + static const std::string minimalCommandMethodOptionName; static const std::string encodeReachabilityOptionName; static const std::string schedulerCutsOptionName; static const std::string noDynamicConstraintsOptionName; diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index f14d3e6ca..3f9d302b3 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -5,7 +5,7 @@ #include "storm-dft/settings/modules/DftGspnSettings.h" #include "storm-dft/settings/modules/DftIOSettings.h" #include "storm-dft/settings/modules/FaultTreeSettings.h" -#include +#include "storm/exceptions/UnmetRequirementException.h" #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/DebugSettings.h" #include "storm/settings/modules/IOSettings.h" @@ -14,7 +14,6 @@ #include "storm/utility/initialize.h" #include "storm-cli-utilities/cli.h" #include "storm-parsers/api/storm-parsers.h" -#include "storm-dft/transformations/DftTransformator.h" /*! @@ -25,54 +24,40 @@ void processOptions() { // Start by setting some urgent options (log levels, resources, etc.) storm::cli::setUrgentOptions(); - storm::settings::modules::DftIOSettings const& dftIOSettings = storm::settings::getModule(); - storm::settings::modules::FaultTreeSettings const& faultTreeSettings = storm::settings::getModule(); - storm::settings::modules::IOSettings const& ioSettings = storm::settings::getModule(); - storm::settings::modules::DftGspnSettings const& dftGspnSettings = storm::settings::getModule(); - storm::settings::modules::TransformationSettings const &transformationSettings = storm::settings::getModule(); - - auto dftTransformator = storm::transformations::dft::DftTransformator(); - - if (!dftIOSettings.isDftFileSet() && !dftIOSettings.isDftJsonFileSet()) { - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model given."); - } + auto const& dftIOSettings = storm::settings::getModule(); + auto const& faultTreeSettings = storm::settings::getModule(); + auto const& ioSettings = storm::settings::getModule(); + auto const& dftGspnSettings = storm::settings::getModule(); + auto const& transformationSettings = storm::settings::getModule(); // Build DFT from given file std::shared_ptr> dft; - if (dftIOSettings.isDftJsonFileSet()) { - STORM_LOG_DEBUG("Loading DFT from file " << dftIOSettings.getDftJsonFilename()); + if (dftIOSettings.isDftFileSet()) { + STORM_LOG_DEBUG("Loading DFT from Galileo file " << dftIOSettings.getDftFilename()); + dft = storm::api::loadDFTGalileoFile(dftIOSettings.getDftFilename()); + } else if (dftIOSettings.isDftJsonFileSet()) { + STORM_LOG_DEBUG("Loading DFT from Json file " << dftIOSettings.getDftJsonFilename()); dft = storm::api::loadDFTJsonFile(dftIOSettings.getDftJsonFilename()); } else { - STORM_LOG_DEBUG("Loading DFT from file " << dftIOSettings.getDftFilename()); - dft = storm::api::loadDFTGalileoFile(dftIOSettings.getDftFilename()); + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model given."); } + // DFT statistics if (dftIOSettings.isDisplayStatsSet()) { dft->writeStatsToStream(std::cout); } + // Export to json if (dftIOSettings.isExportToJson()) { - // Export to json storm::api::exportDFTToJsonFile(*dft, dftIOSettings.getExportJsonFilename()); } - // Limit to one constantly failed BE - if (faultTreeSettings.isUniqueFailedBE()) { - dft = dftTransformator.transformUniqueFailedBe(*dft); - } - - // Eliminate non-binary dependencies - if (!dft->getDependencies().empty()) { - dft = dftTransformator.transformBinaryFDEPs(*dft); - } // Check well-formedness of DFT - std::stringstream stream; - if (!dft->checkWellFormedness(stream)) { - STORM_LOG_THROW(false, storm::exceptions::UnmetRequirementException, "DFT is not well-formed: " << stream.str()); - } + auto wellFormedResult = storm::api::isWellFormed(*dft, false); + STORM_LOG_THROW(wellFormedResult.first, storm::exceptions::UnmetRequirementException, "DFT is not well-formed: " << wellFormedResult.second); + // Transformation to GSPN if (dftGspnSettings.isTransformToGspn()) { - // Transform to GSPN std::pair, uint64_t> pair = storm::api::transformToGSPN(*dft); std::shared_ptr gspn = pair.first; uint64_t toplevelFailedPlace = pair.second; @@ -81,13 +66,13 @@ void processOptions() { storm::api::handleGSPNExportSettings(*gspn); // Transform to Jani + // TODO analyse Jani model std::shared_ptr model = storm::api::transformToJani(*gspn, toplevelFailedPlace); return; } - // SMT + // Export to SMT if (dftIOSettings.isExportToSmt()) { - // Export to smtlib2 storm::api::exportDFTToSMT(*dft, dftIOSettings.getExportSmtFilename()); return; } @@ -97,35 +82,35 @@ void processOptions() { #ifdef STORM_HAVE_Z3 if (faultTreeSettings.solveWithSMT()) { useSMT = true; - STORM_PRINT("Use SMT for preprocessing" << std::endl) + STORM_LOG_DEBUG("Use SMT for preprocessing"); } #endif + // Apply transformations + // TODO transform later before actual analysis + dft = storm::api::applyTransformations(*dft, faultTreeSettings.isUniqueFailedBE(), true); + + dft->setDynamicBehaviorInfo(); storm::api::PreprocessingResult preResults; - preResults.lowerBEBound = storm::dft::utility::FailureBoundFinder::getLeastFailureBound(*dft, useSMT, - solverTimeout); - preResults.upperBEBound = storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(*dft, useSMT, - solverTimeout); - STORM_LOG_DEBUG("BE FAILURE BOUNDS" << std::endl << "========================================" << std::endl << + // TODO: always needed? + preResults.lowerBEBound = storm::dft::utility::FailureBoundFinder::getLeastFailureBound(*dft, useSMT, solverTimeout); + preResults.upperBEBound = storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(*dft, useSMT, solverTimeout); + STORM_LOG_DEBUG("BE failure bounds" << std::endl << "========================================" << std::endl << "Lower bound: " << std::to_string(preResults.lowerBEBound) << std::endl << - "Upper bound: " << std::to_string(preResults.upperBEBound) << std::endl); + "Upper bound: " << std::to_string(preResults.upperBEBound)); - preResults.fdepConflicts = storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, useSMT, - solverTimeout); + // TODO: move into API call? + preResults.fdepConflicts = storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, useSMT, solverTimeout); if (preResults.fdepConflicts.empty()) { - STORM_LOG_DEBUG("No FDEP conflicts found" << std::endl); + STORM_LOG_DEBUG("No FDEP conflicts found"); } else { - STORM_LOG_DEBUG("========================================" << std::endl << - "FDEP CONFLICTS" << std::endl << - "========================================" - << std::endl); + STORM_LOG_DEBUG("========================================" << std::endl << "FDEP CONFLICTS" << std::endl << "========================================"); } for (auto pair: preResults.fdepConflicts) { - STORM_LOG_DEBUG("Conflict between " << dft->getElement(pair.first)->name() << " and " - << dft->getElement(pair.second)->name() << std::endl); + STORM_LOG_DEBUG("Conflict between " << dft->getElement(pair.first)->name() << " and " << dft->getElement(pair.second)->name()); } // Set the conflict map of the dft @@ -142,16 +127,16 @@ void processOptions() { #ifdef STORM_HAVE_Z3 - if (faultTreeSettings.solveWithSMT()) { + if (useSMT) { // Solve with SMT - STORM_LOG_DEBUG("Running DFT analysis with use of SMT" << std::endl); + STORM_LOG_DEBUG("Running DFT analysis with use of SMT"); // Set dynamic behavior vector storm::api::analyzeDFTSMT(*dft, true); } #endif - // From now on we analyse DFT via model checking + // From now on we analyse the DFT via model checking // Set min or max std::string optimizationDirection = "min"; @@ -258,10 +243,8 @@ void processOptions() { approximationError = faultTreeSettings.getApproximationError(); } storm::api::analyzeDFT(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), relevantEvents, - faultTreeSettings.isAllowDCForRelevantEvents(), approximationError, - faultTreeSettings.getApproximationHeuristic(), - transformationSettings.isChainEliminationSet(), - transformationSettings.isIgnoreLabelingSet(), true); + faultTreeSettings.isAllowDCForRelevantEvents(), approximationError, faultTreeSettings.getApproximationHeuristic(), + transformationSettings.isChainEliminationSet(), transformationSettings.isIgnoreLabelingSet(), true); } } diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index 1d053dc87..5912a3c73 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -1,6 +1,7 @@ #pragma once #include +#include #include "storm-dft/parser/DFTGalileoParser.h" #include "storm-dft/parser/DFTJsonParser.h" @@ -8,6 +9,7 @@ #include "storm-dft/modelchecker/dft/DFTModelChecker.h" #include "storm-dft/modelchecker/dft/DFTASFChecker.h" #include "storm-dft/transformations/DftToGspnTransformator.h" +#include "storm-dft/transformations/DftTransformator.h" #include "storm-dft/utility/FDEPConflictFinder.h" #include "storm-dft/utility/FailureBoundFinder.h" @@ -59,12 +61,60 @@ namespace storm { * Check whether the DFT is well-formed. * * @param dft DFT. - * @return True iff the DFT is well-formed. + * @param validForAnalysis If true, additional (more restrictive) checks are performed to check whether the DFT is valid for analysis. + * @return Pair where the first entry is true iff the DFT is well-formed. The second entry contains the error messages for illformed parts. */ template - bool isWellFormed(storm::storage::DFT const& dft) { + std::pair isWellFormed(storm::storage::DFT const& dft, bool validForAnalysis = true) { std::stringstream stream; - return dft.checkWellFormedness(stream); + bool wellFormed = dft.checkWellFormedness(validForAnalysis, stream); + return std::pair(wellFormed, stream.str()); + } + + /*! + * Apply transformations for DFT. + * + * @param dft DFT. + * @param uniqueBE Flag whether a unique constant failed BE is created. + * @param binaryFDEP Flag whether all dependencies should be binary (only one dependent child). + * @return Transformed DFT. + */ + template + std::shared_ptr> applyTransformations(storm::storage::DFT const& dft, bool uniqueBE, bool binaryFDEP) { + std::shared_ptr> transformedDFT = std::make_shared>(dft); + auto dftTransformator = storm::transformations::dft::DftTransformator(); + if (uniqueBE) { + transformedDFT = dftTransformator.transformUniqueFailedBe(*transformedDFT); + } + if (binaryFDEP && !dft.getDependencies().empty()) { + transformedDFT = dftTransformator.transformBinaryFDEPs(*transformedDFT); + } + return transformedDFT; + } + + template + bool computeDependencyConflicts(storm::storage::DFT const& dft, bool useSMT, double solverTimeout) { + std::vector> fdepConflicts = storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, useSMT, solverTimeout); + + if (fdepConflicts.empty()) { + return false; + } + for (auto pair: fdepConflicts) { + STORM_LOG_DEBUG("Conflict between " << dft.getElement(pair.first)->name() << " and " << dft.getElement(pair.second)->name()); + } + + // Set the conflict map of the dft + std::set conflict_set; + for (auto conflict : fdepConflicts) { + conflict_set.insert(size_t(conflict.first)); + conflict_set.insert(size_t(conflict.second)); + } + for (size_t depId : dft->getDependencies()) { + if (!conflict_set.count(depId)) { + dft->setDependencyNotInConflict(depId); + } + } + return true; } /*! @@ -79,8 +129,8 @@ namespace storm { * @param allowDCForRelevantEvents If true, Don't Care propagation is allowed even for relevant events. * @param approximationError Allowed approximation error. Value 0 indicates no approximation. * @param approximationHeuristic Heuristic used for state space exploration. - * @param eliminateChains If true, chains of non-Markovian states are elimianted from the resulting MA - * @param ignoreLabeling If true, the labeling of states is ignored during state elimination + * @param eliminateChains If true, chains of non-Markovian states are eliminated from the resulting MA. + * @param ignoreLabeling If true, the labeling of states is ignored during state elimination. * @param printOutput If true, model information, timings, results, etc. are printed. * @return Results. */ @@ -88,14 +138,12 @@ namespace storm { typename storm::modelchecker::DFTModelChecker::dft_results analyzeDFT(storm::storage::DFT const& dft, std::vector> const& properties, bool symred = true, bool allowModularisation = true, std::set const& relevantEvents = {}, bool allowDCForRelevantEvents = true, double approximationError = 0.0, - storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, - bool eliminateChains = false, bool ignoreLabeling = false, bool printOutput = false) { + storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, bool eliminateChains = false, + bool ignoreLabeling = false, bool printOutput = false) { storm::modelchecker::DFTModelChecker modelChecker(printOutput); typename storm::modelchecker::DFTModelChecker::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, relevantEvents, - allowDCForRelevantEvents, approximationError, - approximationHeuristic, - eliminateChains, - ignoreLabeling); + allowDCForRelevantEvents, approximationError, approximationHeuristic, + eliminateChains, ignoreLabeling); if (printOutput) { modelChecker.printTimings(); modelChecker.printResults(results); @@ -111,8 +159,7 @@ namespace storm { * @return Result result vector */ template - void - analyzeDFTSMT(storm::storage::DFT const &dft, bool printOutput); + void analyzeDFTSMT(storm::storage::DFT const& dft, bool printOutput); /*! * Export DFT to JSON file. @@ -139,7 +186,7 @@ namespace storm { * @param file File. */ template - void exportDFTToSMT(storm::storage::DFT const &dft, std::string const &file); + void exportDFTToSMT(storm::storage::DFT const& dft, std::string const& file); /*! * Transform DFT to GSPN. diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index ca62ea406..5bc4b0f4c 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -3,12 +3,14 @@ #include "storm/settings/modules/IOSettings.h" #include "storm/settings/modules/GeneralSettings.h" #include "storm/builder/ParallelCompositionBuilder.h" +#include "storm/exceptions/UnmetRequirementException.h" #include "storm/utility/bitoperations.h" #include "storm/utility/DirectEncodingExporter.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/models/ModelType.h" +#include "storm-dft/api/storm-dft.h" #include "storm-dft/builder/ExplicitDFTModelBuilder.h" #include "storm-dft/storage/dft/DFTIsomorphism.h" #include "storm-dft/settings/modules/FaultTreeSettings.h" @@ -18,16 +20,19 @@ namespace storm { namespace modelchecker { template - typename DFTModelChecker::dft_results - DFTModelChecker::check(storm::storage::DFT const &origDft, - std::vector> const &properties, - bool symred, bool allowModularisation, std::set const &relevantEvents, - bool allowDCForRelevantEvents, double approximationError, - storm::builder::ApproximationHeuristic approximationHeuristic, - bool eliminateChains, bool ignoreLabeling) { + typename DFTModelChecker::dft_results DFTModelChecker::check(storm::storage::DFT const& origDft, + std::vector> const& properties, bool symred, + bool allowModularisation, std::set const& relevantEvents, + bool allowDCForRelevantEvents, double approximationError, + storm::builder::ApproximationHeuristic approximationHeuristic, bool eliminateChains, + bool ignoreLabeling) { totalTimer.start(); dft_results results; + // Check well-formedness of DFT + auto wellFormedResult = storm::api::isWellFormed(origDft, true); + STORM_LOG_THROW(wellFormedResult.first, storm::exceptions::UnmetRequirementException, "DFT is not well-formed for analysis: " << wellFormedResult.second); + // Optimizing DFT storm::storage::DFT dft = origDft.optimize(); @@ -37,18 +42,14 @@ namespace storm { // TODO: distinguish for all properties, not only for first one if (properties[0]->isTimeOperatorFormula() && allowModularisation) { // Use parallel composition as modularisation approach for expected time - std::shared_ptr> model = buildModelViaComposition(dft, - properties, - symred, true, - relevantEvents); + std::shared_ptr> model = buildModelViaComposition(dft, properties, symred, true, relevantEvents); // Model checking std::vector resultsValue = checkModel(model, properties); for (ValueType result : resultsValue) { results.push_back(result); } } else { - results = checkHelper(dft, properties, symred, allowModularisation, relevantEvents, - allowDCForRelevantEvents, approximationError, approximationHeuristic, + results = checkHelper(dft, properties, symred, allowModularisation, relevantEvents, allowDCForRelevantEvents, approximationError, approximationHeuristic, eliminateChains, ignoreLabeling); } totalTimer.stop(); @@ -56,13 +57,11 @@ namespace storm { } template - typename DFTModelChecker::dft_results - DFTModelChecker::checkHelper(storm::storage::DFT const &dft, - property_vector const &properties, bool symred, - bool allowModularisation, std::set const &relevantEvents, - bool allowDCForRelevantEvents, double approximationError, - storm::builder::ApproximationHeuristic approximationHeuristic, - bool eliminateChains, bool ignoreLabeling) { + typename DFTModelChecker::dft_results DFTModelChecker::checkHelper(storm::storage::DFT const& dft, property_vector const& properties, + bool symred, bool allowModularisation, std::set const& relevantEvents, + bool allowDCForRelevantEvents, double approximationError, + storm::builder::ApproximationHeuristic approximationHeuristic, + bool eliminateChains, bool ignoreLabeling) { STORM_LOG_TRACE("Check helper called"); std::vector> dfts; bool invResults = false; @@ -425,10 +424,7 @@ namespace storm { storm::api::exportSparseModelAsDrn(model, ioSettings.getExportExplicitFilename(), parameterNames); } if (ioSettings.isExportDotSet()) { - std::ofstream stream; - storm::utility::openFile(ioSettings.getExportDotFilename(), stream); - model->writeDotToStream(stream, true, true); - storm::utility::closeFile(stream); + storm::api::exportSparseModelAsDot(model, ioSettings.getExportDotFilename(), ioSettings.getExportDotMaxWidth()); } // Model checking diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 6c3324bf2..daa6c33f2 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -760,7 +760,7 @@ namespace storm { } template - bool DFT::checkWellFormedness(std::ostream& stream) const { + bool DFT::checkWellFormedness(bool validForAnalysis, std::ostream& stream) const { bool wellformed = true; // Check independence of spare modules // TODO: comparing one element of each spare module sufficient? @@ -776,6 +776,21 @@ namespace storm { } } } + + if (validForAnalysis) { + // Check that each dependency is binary + for (size_t idDependency : this->getDependencies()) { + std::shared_ptr const> dependency = this->getDependency(idDependency); + if (dependency->dependentEvents().size() != 1) { + if (!wellformed) { + stream << std::endl; + } + stream << "Dependency '" << dependency->name() << "' is not binary."; + wellformed = false; + } + + } + } // TODO check VOT gates // TODO check only one constant failed event return wellformed; diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h index 6a00be126..c7c790350 100644 --- a/src/storm-dft/storage/dft/DFT.h +++ b/src/storm-dft/storage/dft/DFT.h @@ -243,10 +243,12 @@ namespace storm { /*! * Check if the DFT is well-formed. + * + * @param validForAnalysis If true, additional (more restrictive) checks are performed to check whether the DFT is valid for analysis. * @param stream Output stream where warnings about non-well-formed parts are written. * @return True iff the DFT is well-formed. */ - bool checkWellFormedness(std::ostream& stream) const; + bool checkWellFormedness(bool validForAnalysis, std::ostream& stream) const; uint64_t maxRank() const; diff --git a/src/storm-dft/transformations/DftTransformator.cpp b/src/storm-dft/transformations/DftTransformator.cpp index 473f4249b..6dcbdf17c 100644 --- a/src/storm-dft/transformations/DftTransformator.cpp +++ b/src/storm-dft/transformations/DftTransformator.cpp @@ -4,6 +4,7 @@ namespace storm { namespace transformations { namespace dft { + template DftTransformator::DftTransformator() { } diff --git a/src/storm-dft/transformations/DftTransformator.h b/src/storm-dft/transformations/DftTransformator.h index c8e832f1b..5e1c48f13 100644 --- a/src/storm-dft/transformations/DftTransformator.h +++ b/src/storm-dft/transformations/DftTransformator.h @@ -1,3 +1,5 @@ +#pragma once + #include "storm-dft/storage/dft/DFT.h" #include "storm-dft/builder/DFTBuilder.h" #include "storm/utility/macros.h" diff --git a/src/storm-dft/utility/FDEPConflictFinder.cpp b/src/storm-dft/utility/FDEPConflictFinder.cpp index 53f63ae4b..eb4447ffb 100644 --- a/src/storm-dft/utility/FDEPConflictFinder.cpp +++ b/src/storm-dft/utility/FDEPConflictFinder.cpp @@ -4,10 +4,9 @@ namespace storm { namespace dft { namespace utility { - std::vector> - FDEPConflictFinder::getDependencyConflicts(storm::storage::DFT const &dft, - bool useSMT, - uint_fast64_t timeout) { + template<> + std::vector> FDEPConflictFinder::getDependencyConflicts(storm::storage::DFT const& dft, bool useSMT, + uint_fast64_t timeout) { std::shared_ptr smtChecker = nullptr; if (useSMT) { @@ -25,46 +24,30 @@ namespace storm { dep2Index = dft.getDependencies().at(j); if (dft.getDynamicBehavior()[dep1Index] && dft.getDynamicBehavior()[dep2Index]) { if (useSMT) { // if an SMT solver is to be used - if (dft.getDependency(dep1Index)->triggerEvent() == - dft.getDependency(dep2Index)->triggerEvent()) { - STORM_LOG_DEBUG("Conflict between " << dft.getElement(dep1Index)->name() << " and " - << dft.getElement(dep2Index)->name() - << ": Same trigger"); + if (dft.getDependency(dep1Index)->triggerEvent() == dft.getDependency(dep2Index)->triggerEvent()) { + STORM_LOG_DEBUG("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name() << ": Same trigger"); res.emplace_back(std::pair(dep1Index, dep2Index)); } else { switch (smtChecker->checkDependencyConflict(dep1Index, dep2Index, timeout)) { case storm::solver::SmtSolver::CheckResult::Sat: - STORM_LOG_DEBUG( - "Conflict between " << dft.getElement(dep1Index)->name() << " and " - << dft.getElement(dep2Index)->name()); + STORM_LOG_DEBUG("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); res.emplace_back(std::pair(dep1Index, dep2Index)); break; case storm::solver::SmtSolver::CheckResult::Unknown: - STORM_LOG_DEBUG( - "Unknown: Conflict between " << dft.getElement(dep1Index)->name() - << " and " - << dft.getElement(dep2Index)->name()); + STORM_LOG_DEBUG("Unknown: Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); res.emplace_back(std::pair(dep1Index, dep2Index)); break; default: - STORM_LOG_DEBUG( - "No conflict between " << dft.getElement(dep1Index)->name() - << " and " - << dft.getElement(dep2Index)->name()); + STORM_LOG_DEBUG("No conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); break; } } } else { - STORM_LOG_DEBUG( - "Conflict between " << dft.getElement(dep1Index)->name() << " and " - << dft.getElement(dep2Index)->name()); + STORM_LOG_DEBUG("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); res.emplace_back(std::pair(dep1Index, dep2Index)); } } else { - STORM_LOG_DEBUG( - "Static behavior: No conflict between " << dft.getElement(dep1Index)->name() - << " and " - << dft.getElement(dep2Index)->name()); + STORM_LOG_DEBUG("Static behavior: No conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); break; } } @@ -72,10 +55,9 @@ namespace storm { return res; } - std::vector> - FDEPConflictFinder::getDependencyConflicts(storm::storage::DFT const &dft, - bool useSMT, - uint_fast64_t timeout) { + template<> + std::vector> FDEPConflictFinder::getDependencyConflicts(storm::storage::DFT const& dft, + bool useSMT, uint_fast64_t timeout) { if (useSMT) { STORM_LOG_WARN("SMT encoding for rational functions is not supported"); } @@ -88,15 +70,10 @@ namespace storm { for (size_t j = i + 1; j < dft.getDependencies().size(); ++j) { dep2Index = dft.getDependencies().at(j); if (dft.getDynamicBehavior()[dep1Index] && dft.getDynamicBehavior()[dep2Index]) { - STORM_LOG_DEBUG( - "Conflict between " << dft.getElement(dep1Index)->name() << " and " - << dft.getElement(dep2Index)->name()); + STORM_LOG_DEBUG("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); res.emplace_back(std::pair(dep1Index, dep2Index)); } else { - STORM_LOG_DEBUG( - "Static behavior: No conflict between " << dft.getElement(dep1Index)->name() - << " and " - << dft.getElement(dep2Index)->name()); + STORM_LOG_DEBUG("Static behavior: No conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); break; } } @@ -104,8 +81,11 @@ namespace storm { return res; } - class FDEPConflictFinder; + template + class FDEPConflictFinder; + template + class FDEPConflictFinder; } } } \ No newline at end of file diff --git a/src/storm-dft/utility/FDEPConflictFinder.h b/src/storm-dft/utility/FDEPConflictFinder.h index 831bfd248..e783f9000 100644 --- a/src/storm-dft/utility/FDEPConflictFinder.h +++ b/src/storm-dft/utility/FDEPConflictFinder.h @@ -5,24 +5,22 @@ namespace storm { namespace dft { namespace utility { + + template class FDEPConflictFinder { public: - /** + + /*! * Get a vector of index pairs of FDEPs in the DFT which are conflicting. Two FDEPs are conflicting if * their simultaneous triggering may cause unresolvable non-deterministic behavior. * - * @param dft the DFT - * @param useSMT if set, an SMT solver is used to refine the conflict set - * @param timeout timeout for each query in seconds, defaults to 10 seconds - * @return a vector of pairs of indices. The indices in a pair refer to FDEPs which are conflicting + * @param dft The DFT. + * @param useSMT If set, an SMT solver is used to refine the conflict set. + * @param timeout Timeout for each SMT query in seconds, defaults to 10 seconds. + * @return A vector of pairs of indices. The indices in a pair refer to FDEPs which are conflicting. */ - static std::vector> - getDependencyConflicts(storm::storage::DFT const &dft, - bool useSMT = false, uint_fast64_t timeout = 10); - - static std::vector> - getDependencyConflicts(storm::storage::DFT const &dft, - bool useSMT = false, uint_fast64_t timeout = 10); + static std::vector> getDependencyConflicts(storm::storage::DFT const& dft, bool useSMT = false, + uint_fast64_t timeout = 10); }; } } diff --git a/src/storm-parsers/parser/DeterministicSparseTransitionParser.cpp b/src/storm-parsers/parser/DeterministicSparseTransitionParser.cpp index 229cc3c2e..6c063d49c 100644 --- a/src/storm-parsers/parser/DeterministicSparseTransitionParser.cpp +++ b/src/storm-parsers/parser/DeterministicSparseTransitionParser.cpp @@ -14,7 +14,7 @@ #include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/CoreSettings.h" +#include "storm/settings/modules/BuildSettings.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/macros.h" @@ -82,7 +82,7 @@ namespace storm { uint_fast64_t row, col, lastRow = 0; double val; - bool dontFixDeadlocks = storm::settings::getModule().isDontFixDeadlocksSet(); + bool dontFixDeadlocks = storm::settings::getModule().isDontFixDeadlocksSet(); bool hadDeadlocks = false; // Read all transitions from file. Note that we assume that the diff --git a/src/storm-parsers/parser/ImcaMarkovAutomatonParser.cpp b/src/storm-parsers/parser/ImcaMarkovAutomatonParser.cpp index 0cbf917f1..a10e3864b 100644 --- a/src/storm-parsers/parser/ImcaMarkovAutomatonParser.cpp +++ b/src/storm-parsers/parser/ImcaMarkovAutomatonParser.cpp @@ -2,7 +2,6 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/BuildSettings.h" -#include "storm/settings/modules/CoreSettings.h" #include "storm/utility/file.h" #include "storm/utility/builder.h" @@ -127,7 +126,7 @@ namespace storm { // Fix deadlocks (if required) assert(stateBehaviors.size() == numStates); - if (!storm::settings::getModule().isDontFixDeadlocksSet()) { + if (!storm::settings::getModule().isDontFixDeadlocksSet()) { StateType state = 0; for (auto& behavior : stateBehaviors) { if (!behavior.wasExpanded()) { diff --git a/src/storm-parsers/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/storm-parsers/parser/MarkovAutomatonSparseTransitionParser.cpp index 9acd151b0..6d25e7f15 100644 --- a/src/storm-parsers/parser/MarkovAutomatonSparseTransitionParser.cpp +++ b/src/storm-parsers/parser/MarkovAutomatonSparseTransitionParser.cpp @@ -1,7 +1,7 @@ #include "MarkovAutomatonSparseTransitionParser.h" #include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/CoreSettings.h" +#include "storm/settings/modules/BuildSettings.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/FileIoException.h" #include "storm-parsers/parser/MappedFile.h" @@ -18,7 +18,7 @@ namespace storm { typename MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTransitionParser::firstPass(char const* buf) { MarkovAutomatonSparseTransitionParser::FirstPassResult result; - bool dontFixDeadlocks = storm::settings::getModule().isDontFixDeadlocksSet(); + bool dontFixDeadlocks = storm::settings::getModule().isDontFixDeadlocksSet(); // Skip the format hint if it is there. buf = trimWhitespaces(buf); @@ -171,7 +171,7 @@ namespace storm { typename MarkovAutomatonSparseTransitionParser::Result MarkovAutomatonSparseTransitionParser::secondPass(char const* buf, FirstPassResult const& firstPassResult) { Result result(firstPassResult); - bool dontFixDeadlocks = storm::settings::getModule().isDontFixDeadlocksSet(); + bool dontFixDeadlocks = storm::settings::getModule().isDontFixDeadlocksSet(); // Skip the format hint if it is there. buf = trimWhitespaces(buf); diff --git a/src/storm-parsers/parser/NondeterministicSparseTransitionParser.cpp b/src/storm-parsers/parser/NondeterministicSparseTransitionParser.cpp index 56b00070c..1f3b4c896 100644 --- a/src/storm-parsers/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/storm-parsers/parser/NondeterministicSparseTransitionParser.cpp @@ -4,7 +4,7 @@ #include "storm-parsers/parser/MappedFile.h" #include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/CoreSettings.h" +#include "storm/settings/modules/BuildSettings.h" #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/OutOfRangeException.h" @@ -91,7 +91,7 @@ namespace storm { // Initialize variables for the parsing run. uint_fast64_t source = 0, target = 0, lastSource = 0, choice = 0, lastChoice = 0, curRow = 0; double val = 0.0; - bool dontFixDeadlocks = storm::settings::getModule().isDontFixDeadlocksSet(); + bool dontFixDeadlocks = storm::settings::getModule().isDontFixDeadlocksSet(); bool hadDeadlocks = false; // The first state already starts a new row group of the matrix. diff --git a/src/storm/api/export.h b/src/storm/api/export.h index f3064b538..ca05b7a47 100644 --- a/src/storm/api/export.h +++ b/src/storm/api/export.h @@ -32,10 +32,10 @@ namespace storm { } template - void exportSparseModelAsDot(std::shared_ptr> const& model, std::string const& filename) { + void exportSparseModelAsDot(std::shared_ptr> const& model, std::string const& filename, size_t maxWidth = 30) { std::ofstream stream; storm::utility::openFile(filename, stream); - model->writeDotToStream(stream); + model->writeDotToStream(stream, maxWidth); storm::utility::closeFile(stream); } diff --git a/src/storm/api/transformation.h b/src/storm/api/transformation.h index 521aecb75..3ffbab033 100644 --- a/src/storm/api/transformation.h +++ b/src/storm/api/transformation.h @@ -16,21 +16,11 @@ namespace storm { * Eliminates chains of non-Markovian states from a given Markov Automaton */ template - std::pair>, std::vector>> - eliminateNonMarkovianChains(std::shared_ptr> const &ma, - std::vector> const &formulas, - bool ignoreLabeling) { - - auto newFormulas = storm::transformer::NonMarkovianChainTransformer::checkAndTransformFormulas( - formulas); - STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(), - "The state elimination does not preserve all properties."); - STORM_LOG_WARN_COND(!ignoreLabeling, - "Labels are ignored for the state elimination. This may cause incorrect results."); - return std::make_pair( - storm::transformer::NonMarkovianChainTransformer::eliminateNonmarkovianStates(ma, - !ignoreLabeling), - newFormulas); + std::pair>, std::vector>> eliminateNonMarkovianChains(std::shared_ptr> const& ma, std::vector> const& formulas,bool ignoreLabeling) { + auto newFormulas = storm::transformer::NonMarkovianChainTransformer::checkAndTransformFormulas(formulas); + STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(), "The state elimination does not preserve all properties."); + STORM_LOG_WARN_COND(!ignoreLabeling, "Labels are ignored for the state elimination. This may cause incorrect results."); + return std::make_pair(storm::transformer::NonMarkovianChainTransformer::eliminateNonmarkovianStates(ma, !ignoreLabeling), newFormulas); } @@ -40,17 +30,17 @@ namespace storm { * If such a transformation does not preserve one of the given formulas, a warning is issued. */ template - std::pair>, std::vector>> transformContinuousToDiscreteTimeSparseModel(std::shared_ptr> const& model, std::vector> const& formulas) { - + std::pair>, std::vector>> transformContinuousToDiscreteTimeSparseModel(std::shared_ptr> const& model, std::vector> const& formulas) { + storm::transformer::ContinuousToDiscreteTimeModelTransformer transformer; - + std::string timeRewardName = "_time"; while(model->hasRewardModel(timeRewardName)) { timeRewardName += "_"; } auto newFormulas = transformer.checkAndTransformFormulas(formulas, timeRewardName); STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(), "Transformation of a " << model->getType() << " to a discrete time model does not preserve all properties."); - + if (model->isOfType(storm::models::ModelType::Ctmc)) { return std::make_pair(transformer.transform(*model->template as>(), timeRewardName), newFormulas); } else if (model->isOfType(storm::models::ModelType::MarkovAutomaton)) { @@ -68,16 +58,16 @@ namespace storm { */ template std::pair>, std::vector>> transformContinuousToDiscreteTimeSparseModel(storm::models::sparse::Model&& model, std::vector> const& formulas) { - + storm::transformer::ContinuousToDiscreteTimeModelTransformer transformer; - + std::string timeRewardName = "_time"; while(model.hasRewardModel(timeRewardName)) { timeRewardName += "_"; } auto newFormulas = transformer.checkAndTransformFormulas(formulas, timeRewardName); STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(), "Transformation of a " << model.getType() << " to a discrete time model does not preserve all properties."); - + if (model.isOfType(storm::models::ModelType::Ctmc)) { return std::make_pair(transformer.transform(std::move(*model.template as>()), timeRewardName), newFormulas); } else if (model.isOfType(storm::models::ModelType::MarkovAutomaton)) { @@ -86,9 +76,9 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation of a " << model.getType() << " to a discrete time model is not supported."); } return std::make_pair(nullptr, newFormulas);; - + } - + template std::shared_ptr checkAndTransformContinuousToDiscreteTimeFormula(storm::logic::Formula const& formula, std::string const& timeRewardName = "_time") { storm::transformer::ContinuousToDiscreteTimeModelTransformer transformer; @@ -99,8 +89,7 @@ namespace storm { } return nullptr; } - - + /*! * Transforms the given symbolic model to a sparse model. */ @@ -118,7 +107,7 @@ namespace storm { } return nullptr; } - + template std::shared_ptr> transformToNondeterministicModel(storm::models::sparse::Model&& model) { storm::storage::sparse::ModelComponents components(std::move(model.getTransitionMatrix()), std::move(model.getStateLabeling()), std::move(model.getRewardModels())); @@ -135,6 +124,6 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot transform model of type " << model.getType() << " to a nondeterministic model."); } } - + } } diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp index 3e0250ac8..64a74a258 100644 --- a/src/storm/builder/DdJaniModelBuilder.cpp +++ b/src/storm/builder/DdJaniModelBuilder.cpp @@ -28,7 +28,7 @@ #include "storm/models/symbolic/StandardRewardModel.h" #include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/CoreSettings.h" +#include "storm/settings/modules/BuildSettings.h" #include "storm/utility/macros.h" #include "storm/utility/jani.h" @@ -1932,7 +1932,7 @@ namespace storm { if (!deadlockStates.isZero()) { // If we need to fix deadlocks, we do so now. - if (!storm::settings::getModule().isDontFixDeadlocksSet()) { + if (!storm::settings::getModule().isDontFixDeadlocksSet()) { STORM_LOG_INFO("Fixing deadlocks in " << deadlockStates.getNonZeroCount() << " states. The first three of these states are: "); storm::dd::Add deadlockStatesAdd = deadlockStates.template toAdd(); diff --git a/src/storm/builder/DdPrismModelBuilder.cpp b/src/storm/builder/DdPrismModelBuilder.cpp index 83905937c..1a25bdaa2 100644 --- a/src/storm/builder/DdPrismModelBuilder.cpp +++ b/src/storm/builder/DdPrismModelBuilder.cpp @@ -24,7 +24,7 @@ #include "storm/storage/dd/cudd/CuddAddIterator.h" #include "storm/storage/dd/Bdd.h" -#include "storm/settings/modules/CoreSettings.h" +#include "storm/settings/modules/BuildSettings.h" #include "storm/adapters/RationalFunctionAdapter.h" @@ -1422,7 +1422,7 @@ namespace storm { // If there are deadlocks, either fix them or raise an error. if (!deadlockStates.isZero()) { // If we need to fix deadlocks, we do so now. - if (!storm::settings::getModule().isDontFixDeadlocksSet()) { + if (!storm::settings::getModule().isDontFixDeadlocksSet()) { STORM_LOG_INFO("Fixing deadlocks in " << deadlockStates.getNonZeroCount() << " states. The first three of these states are: "); storm::dd::Add deadlockStatesAdd = deadlockStates.template toAdd(); diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index cd87af9a6..63ebee7c9 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -10,7 +10,6 @@ #include "storm/storage/expressions/ExpressionManager.h" -#include "storm/settings/modules/CoreSettings.h" #include "storm/settings/modules/BuildSettings.h" #include "storm/builder/RewardModelBuilder.h" @@ -163,7 +162,7 @@ namespace storm { // If there is no behavior, we might have to introduce a self-loop. if (behavior.empty()) { - if (!storm::settings::getModule().isDontFixDeadlocksSet() || !behavior.wasExpanded()) { + if (!storm::settings::getModule().isDontFixDeadlocksSet() || !behavior.wasExpanded()) { // If the behavior was actually expanded and yet there are no transitions, then we have a deadlock state. if (behavior.wasExpanded()) { this->stateStorage.deadlockStateIndices.push_back(currentIndex); diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp index 43fdfccc7..eb1b397dc 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp @@ -33,7 +33,7 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/JitBuilderSettings.h" -#include "storm/settings/modules/CoreSettings.h" +#include "storm/settings/modules/BuildSettings.h" #include "storm/utility/OsDetection.h" #include "storm-config.h" @@ -574,7 +574,7 @@ namespace storm { modelData["double"] = cpptempl::make_data(list); list = cpptempl::data_list(); - if (storm::settings::getModule().isDontFixDeadlocksSet()) { + if (storm::settings::getModule().isDontFixDeadlocksSet()) { list.push_back(cpptempl::data_map()); } modelData["dontFixDeadlocks"] = cpptempl::make_data(list); diff --git a/src/storm/builder/jit/ModelComponentsBuilder.cpp b/src/storm/builder/jit/ModelComponentsBuilder.cpp index 34cdf8af3..287b05f04 100644 --- a/src/storm/builder/jit/ModelComponentsBuilder.cpp +++ b/src/storm/builder/jit/ModelComponentsBuilder.cpp @@ -10,7 +10,7 @@ #include "storm/builder/RewardModelBuilder.h" #include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/CoreSettings.h" +#include "storm/settings/modules/BuildSettings.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/utility/macros.h" @@ -27,7 +27,7 @@ namespace storm { markovianStates = std::make_unique(10); } - dontFixDeadlocks = storm::settings::getModule().isDontFixDeadlocksSet(); + dontFixDeadlocks = storm::settings::getModule().isDontFixDeadlocksSet(); } template diff --git a/src/storm/models/sparse/DeterministicModel.cpp b/src/storm/models/sparse/DeterministicModel.cpp index 9073e35f9..06419a6c0 100644 --- a/src/storm/models/sparse/DeterministicModel.cpp +++ b/src/storm/models/sparse/DeterministicModel.cpp @@ -1,7 +1,9 @@ #include "storm/models/sparse/DeterministicModel.h" + +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/utility/constants.h" -#include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/utility/export.h" namespace storm { namespace models { @@ -20,8 +22,8 @@ namespace storm { } template - void DeterministicModel::writeDotToStream(std::ostream& outStream, bool includeLabeling, bool linebreakLabel, storm::storage::BitVector const* subsystem, std::vector const* firstValue, std::vector const* secondValue, std::vector const* stateColoring, std::vector const* colors, std::vector* scheduler, bool finalizeOutput) const { - Model::writeDotToStream(outStream, includeLabeling, linebreakLabel, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); + void DeterministicModel::writeDotToStream(std::ostream& outStream, size_t maxWidthLabel, bool includeLabeling, storm::storage::BitVector const* subsystem, std::vector const* firstValue, std::vector const* secondValue, std::vector const* stateColoring, std::vector const* colors, std::vector* scheduler, bool finalizeOutput) const { + Model::writeDotToStream(outStream, maxWidthLabel, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); // iterate over all transitions and draw the arrows with probability information attached. auto rowIt = this->getTransitionMatrix().begin(); @@ -33,14 +35,7 @@ namespace storm { arrowOrigin = "\"" + arrowOrigin + "c\""; outStream << "\t" << arrowOrigin << " [shape = \"point\"]" << std::endl; outStream << "\t" << i << " -> " << arrowOrigin << " [label= \"{"; - bool firstLabel = true; - for (auto const& label : this->getChoiceLabeling().getLabelsOfChoice(i)) { - if (!firstLabel) { - outStream << ", "; - } - firstLabel = false; - outStream << label; - } + storm::utility::outputFixedWidth(outStream, this->getChoiceLabeling().getLabelsOfChoice(i), maxWidthLabel); outStream << "}\"];" << std::endl; } diff --git a/src/storm/models/sparse/DeterministicModel.h b/src/storm/models/sparse/DeterministicModel.h index 01c2f3247..09a8d7ce7 100644 --- a/src/storm/models/sparse/DeterministicModel.h +++ b/src/storm/models/sparse/DeterministicModel.h @@ -30,7 +30,7 @@ namespace storm { DeterministicModel(DeterministicModel&& other) = default; DeterministicModel& operator=(DeterministicModel&& model) = default; - virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, bool linebreakLabeling = false, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const override; + virtual void writeDotToStream(std::ostream& outStream, size_t maxWidthLabel = 30, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const override; }; } // namespace sparse diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp index a5b0e6002..1fe875ab9 100644 --- a/src/storm/models/sparse/Model.cpp +++ b/src/storm/models/sparse/Model.cpp @@ -2,16 +2,16 @@ #include -#include "storm/models/sparse/StandardRewardModel.h" - -#include "storm/utility/vector.h" #include "storm/adapters/RationalFunctionAdapter.h" -#include "storm/utility/NumberTraits.h" - #include "storm/exceptions/IllegalArgumentException.h" #include "storm/exceptions/IllegalFunctionCallException.h" #include "storm/models/sparse/Ctmc.h" #include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/utility/vector.h" +#include "storm/utility/export.h" +#include "storm/utility/NumberTraits.h" + namespace storm { namespace models { @@ -336,7 +336,7 @@ namespace storm { } template - void Model::writeDotToStream(std::ostream& outStream, bool includeLabeling, bool linebreakLabel, storm::storage::BitVector const* subsystem, std::vector const* firstValue, std::vector const* secondValue, std::vector const* stateColoring, std::vector const* colors, std::vector*, bool finalizeOutput) const { + void Model::writeDotToStream(std::ostream& outStream, size_t maxWidthLabel, bool includeLabeling, storm::storage::BitVector const* subsystem, std::vector const* firstValue, std::vector const* secondValue, std::vector const* stateColoring, std::vector const* colors, std::vector*, bool finalizeOutput) const { outStream << "digraph model {" << std::endl; // Write all states to the stream. @@ -350,26 +350,16 @@ namespace storm { if (includeLabeling || firstValue != nullptr || secondValue != nullptr || hasStateValuations()) { outStream << "label = \"" << state; if (hasStateValuations()) { - outStream << " " << getStateValuations().getStateInfo(state); + std::vector results; + boost::split(results, getStateValuations().getStateInfo(state), [](char c) { return c == ',';}); + storm::utility::outputFixedWidth(outStream, results, maxWidthLabel); } outStream << ": "; // Now print the state labeling to the stream if requested. if (includeLabeling) { outStream << "{"; - bool includeComma = false; - for (std::string const& label : this->getLabelsOfState(state)) { - if (includeComma) { - if (linebreakLabel) { - outStream << ",\n"; - } else { - outStream << ", "; - } - } else { - includeComma = true; - } - outStream << label; - } + storm::utility::outputFixedWidth(outStream, this->getLabelsOfState(state), maxWidthLabel); outStream << "}"; } diff --git a/src/storm/models/sparse/Model.h b/src/storm/models/sparse/Model.h index 885374ab6..d1ef45bc1 100644 --- a/src/storm/models/sparse/Model.h +++ b/src/storm/models/sparse/Model.h @@ -323,8 +323,8 @@ namespace storm { * Exports the model to the dot-format and prints the result to the given stream. * * @param outStream The stream to which the model is to be written. + * @param maxWidthLabel Maximal width of the labeling before a linebreak is inserted. Value 0 represents no linebreaks. * @param includeLabling If set to true, the states will be exported with their labels. - * @param linebreakLabel If set to true, a linebreak is introduced after each label. * @param subsystem If not null, this represents the subsystem that is to be exported. * @param firstValue If not null, the values in this vector are attached to the states. * @param secondValue If not null, the values in this vector are attached to the states. @@ -333,7 +333,7 @@ namespace storm { * @param finalizeOutput A flag that sets whether or not the dot stream is closed with a curly brace. * @return A string containing the exported model in dot-format. */ - virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, bool linebreakLabel = false, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const; + virtual void writeDotToStream(std::ostream& outStream, size_t maxWidthLabel = 30, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const; /*! * Retrieves the set of labels attached to the given state. diff --git a/src/storm/models/sparse/NondeterministicModel.cpp b/src/storm/models/sparse/NondeterministicModel.cpp index 1a5cfd7b1..635cfee7b 100644 --- a/src/storm/models/sparse/NondeterministicModel.cpp +++ b/src/storm/models/sparse/NondeterministicModel.cpp @@ -1,15 +1,14 @@ #include "storm/models/sparse/NondeterministicModel.h" +#include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/exceptions/InvalidOperationException.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/storage/Scheduler.h" #include "storm/storage/memorystructure/MemoryStructureBuilder.h" #include "storm/storage/memorystructure/SparseModelMemoryProduct.h" #include "storm/transformer/SubsystemBuilder.h" - -#include "storm/adapters/RationalFunctionAdapter.h" - -#include "storm/exceptions/InvalidOperationException.h" +#include "storm/utility/export.h" namespace storm { namespace models { @@ -72,8 +71,8 @@ namespace storm { } template - void NondeterministicModel::writeDotToStream(std::ostream& outStream, bool includeLabeling, bool linebreakLabel, storm::storage::BitVector const* subsystem, std::vector const* firstValue, std::vector const* secondValue, std::vector const* stateColoring, std::vector const* colors, std::vector* scheduler, bool finalizeOutput) const { - Model::writeDotToStream(outStream, includeLabeling, linebreakLabel, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); + void NondeterministicModel::writeDotToStream(std::ostream& outStream, size_t maxWidthLabel, bool includeLabeling, storm::storage::BitVector const* subsystem, std::vector const* firstValue, std::vector const* secondValue, std::vector const* stateColoring, std::vector const* colors, std::vector* scheduler, bool finalizeOutput) const { + Model::writeDotToStream(outStream, maxWidthLabel, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); // Write the probability distributions for all the states. for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) { @@ -125,14 +124,7 @@ namespace storm { outStream << " [ label = \"{"; } arrowHasLabel = true; - bool firstLabel = true; - for (auto const& label : this->getChoiceLabeling().getLabelsOfChoice(rowIndex)) { - if (!firstLabel) { - outStream << ", "; - } - firstLabel = false; - outStream << label; - } + storm::utility::outputFixedWidth(outStream, this->getChoiceLabeling().getLabelsOfChoice(rowIndex), maxWidthLabel); outStream << "}"; } if (arrowHasLabel) { @@ -157,7 +149,7 @@ namespace storm { } outStream << ";" << std::endl; - // Now draw all probabilitic arcs that belong to this nondeterminstic choice. + // Now draw all probabilistic arcs that belong to this non-deterministic choice. for (auto const& transition : row) { if (subsystem == nullptr || subsystem->get(transition.getColumn())) { outStream << "\t\"" << state << "c" << choice << "\" -> " << transition.getColumn() << " [ label= \"" << transition.getValue() << "\" ]"; diff --git a/src/storm/models/sparse/NondeterministicModel.h b/src/storm/models/sparse/NondeterministicModel.h index 8210ec13f..2a76c1ee0 100644 --- a/src/storm/models/sparse/NondeterministicModel.h +++ b/src/storm/models/sparse/NondeterministicModel.h @@ -61,7 +61,7 @@ namespace storm { virtual void printModelInformationToStream(std::ostream& out) const override; - virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, bool linebreakLabel = false, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const override; + virtual void writeDotToStream(std::ostream& outStream, size_t maxWidthLabel = 30, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const override; }; } // namespace sparse diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp index cc68677e3..74bb4d0a7 100644 --- a/src/storm/settings/SettingsManager.cpp +++ b/src/storm/settings/SettingsManager.cpp @@ -630,12 +630,8 @@ namespace storm { return SettingsManager::manager(); } - storm::settings::modules::CoreSettings& mutableCoreSettings() { - return dynamic_cast(mutableManager().getModule(storm::settings::modules::CoreSettings::moduleName)); - } - - storm::settings::modules::IOSettings& mutableIOSettings() { - return dynamic_cast(mutableManager().getModule(storm::settings::modules::IOSettings::moduleName)); + storm::settings::modules::BuildSettings& mutableBuildSettings() { + return dynamic_cast(mutableManager().getModule(storm::settings::modules::BuildSettings::moduleName)); } storm::settings::modules::AbstractionSettings& mutableAbstractionSettings() { diff --git a/src/storm/settings/SettingsManager.h b/src/storm/settings/SettingsManager.h index 96637153b..9239496e9 100644 --- a/src/storm/settings/SettingsManager.h +++ b/src/storm/settings/SettingsManager.h @@ -12,8 +12,7 @@ namespace storm { namespace settings { namespace modules { - class CoreSettings; - class IOSettings; + class BuildSettings; class ModuleSettings; class AbstractionSettings; } @@ -27,7 +26,7 @@ namespace storm { class SettingsManager { public: - // Explicitely delete copy constructor + // Explicitly delete copy constructor SettingsManager(SettingsManager const&) = delete; void operator=(SettingsManager const&) = delete; @@ -305,20 +304,12 @@ namespace storm { } /*! - * Retrieves the core settings in a mutable form. This is only meant to be used for debug purposes or very + * Retrieves the build settings in a mutable form. This is only meant to be used for debug purposes or very * rare cases where it is necessary. * - * @return An object that allows accessing and modifying the core settings. + * @return An object that allows accessing and modifying the build settings. */ - storm::settings::modules::CoreSettings& mutableCoreSettings(); - - /*! - * Retrieves the IO settings in a mutable form. This is only meant to be used for debug purposes or very - * rare cases where it is necessary. - * - * @return An object that allows accessing and modifying the IO settings. - */ - storm::settings::modules::IOSettings& mutableIOSettings(); + storm::settings::modules::BuildSettings& mutableBuildSettings(); /*! * Retrieves the abstraction settings in a mutable form. This is only meant to be used for debug purposes or very diff --git a/src/storm/settings/modules/BuildSettings.cpp b/src/storm/settings/modules/BuildSettings.cpp index 56dbb3e45..3ebc6d109 100644 --- a/src/storm/settings/modules/BuildSettings.cpp +++ b/src/storm/settings/modules/BuildSettings.cpp @@ -25,15 +25,19 @@ namespace storm { const std::string explorationChecksOptionShortName = "ec"; const std::string prismCompatibilityOptionName = "prismcompat"; const std::string prismCompatibilityOptionShortName = "pc"; + const std::string dontFixDeadlockOptionName = "nofixdl"; + const std::string dontFixDeadlockOptionShortName = "ndl"; const std::string noBuildOptionName = "nobuild"; const std::string fullModelBuildOptionName = "buildfull"; const std::string buildChoiceLabelOptionName = "buildchoicelab"; const std::string buildStateValuationsOptionName = "buildstateval"; const std::string buildOutOfBoundsStateOptionName = "buildoutofboundsstate"; const std::string bitsForUnboundedVariablesOptionName = "int-bits"; + BuildSettings::BuildSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, prismCompatibilityOptionName, false, "Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, dontFixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(dontFixDeadlockOptionShortName).setIsAdvanced().build()); this->addOption(storm::settings::OptionBuilder(moduleName, jitOptionName, false, "If set, the model is built using the JIT model builder.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, fullModelBuildOptionName, false, "If set, include all rewards and labels.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, buildChoiceLabelOptionName, false, "If set, also build the choice labels").setIsAdvanced().build()); @@ -61,6 +65,14 @@ namespace storm { return this->getOption(prismCompatibilityOptionName).getHasOptionBeenSet(); } + bool BuildSettings::isDontFixDeadlocksSet() const { + return this->getOption(dontFixDeadlockOptionName).getHasOptionBeenSet(); + } + + std::unique_ptr BuildSettings::overrideDontFixDeadlocksSet(bool stateToSet) { + return this->overrideOption(dontFixDeadlockOptionName, stateToSet); + } + bool BuildSettings::isBuildFullModelSet() const { return this->getOption(fullModelBuildOptionName).getHasOptionBeenSet(); } diff --git a/src/storm/settings/modules/BuildSettings.h b/src/storm/settings/modules/BuildSettings.h index 29575e2a3..b80424c7f 100644 --- a/src/storm/settings/modules/BuildSettings.h +++ b/src/storm/settings/modules/BuildSettings.h @@ -51,6 +51,22 @@ namespace storm { */ bool isPrismCompatibilityEnabled() const; + /*! + * Retrieves whether the dont-fix-deadlocks option was set. + * + * @return True if the dont-fix-deadlocks option was set. + */ + bool isDontFixDeadlocksSet() const; + + /*! + * Overrides the option to not fix deadlocks by setting it to the specified value. As soon as the + * returned memento goes out of scope, the original value is restored. + * + * @param stateToSet The value that is to be set for the fix-deadlocks option. + * @return The memento that will eventually restore the original value. + */ + std::unique_ptr overrideDontFixDeadlocksSet(bool stateToSet); + /** * Retrieves whether no model should be build at all, in case one just want to translate models or parse a file. */ diff --git a/src/storm/settings/modules/CoreSettings.cpp b/src/storm/settings/modules/CoreSettings.cpp index 9f50da725..bc9ea87fb 100644 --- a/src/storm/settings/modules/CoreSettings.cpp +++ b/src/storm/settings/modules/CoreSettings.cpp @@ -20,10 +20,6 @@ namespace storm { namespace modules { const std::string CoreSettings::moduleName = "core"; - const std::string CoreSettings::counterexampleOptionName = "counterexample"; - const std::string CoreSettings::counterexampleOptionShortName = "cex"; - const std::string CoreSettings::dontFixDeadlockOptionName = "nofixdl"; - const std::string CoreSettings::dontFixDeadlockOptionShortName = "ndl"; const std::string CoreSettings::eqSolverOptionName = "eqsolver"; const std::string CoreSettings::lpSolverOptionName = "lpsolver"; const std::string CoreSettings::smtSolverOptionName = "smtsolver"; @@ -37,9 +33,6 @@ namespace storm { const std::string CoreSettings::intelTbbOptionShortName = "tbb"; CoreSettings::CoreSettings() : ModuleSettings(moduleName), engine(CoreSettings::Engine::Sparse) { - this->addOption(storm::settings::OptionBuilder(moduleName, counterexampleOptionName, false, "Generates a counterexample for the given PRCTL formulas if not satisfied by the model.").setShortName(counterexampleOptionShortName).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, dontFixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(dontFixDeadlockOptionShortName).setIsAdvanced().build()); - std::vector engines = {"sparse", "hybrid", "dd", "dd-to-sparse", "expl", "abs"}; this->addOption(storm::settings::OptionBuilder(moduleName, engineOptionName, false, "Sets which engine is used for model building and model checking.").setShortName(engineOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(engines)).setDefaultValueString("sparse").build()).build()); @@ -65,18 +58,6 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, intelTbbOptionName, false, "Sets whether to use Intel TBB (if Storm was built with support for TBB).").setShortName(intelTbbOptionShortName).build()); } - bool CoreSettings::isCounterexampleSet() const { - return this->getOption(counterexampleOptionName).getHasOptionBeenSet(); - } - - bool CoreSettings::isDontFixDeadlocksSet() const { - return this->getOption(dontFixDeadlockOptionName).getHasOptionBeenSet(); - } - - std::unique_ptr CoreSettings::overrideDontFixDeadlocksSet(bool stateToSet) { - return this->overrideOption(dontFixDeadlockOptionName, stateToSet); - } - storm::solver::EquationSolverType CoreSettings::getEquationSolver() const { std::string equationSolverName = this->getOption(eqSolverOptionName).getArgumentByName("name").getValueAsString(); if (equationSolverName == "gmm++") { diff --git a/src/storm/settings/modules/CoreSettings.h b/src/storm/settings/modules/CoreSettings.h index 483e61df3..405fad91f 100644 --- a/src/storm/settings/modules/CoreSettings.h +++ b/src/storm/settings/modules/CoreSettings.h @@ -36,37 +36,6 @@ namespace storm { */ CoreSettings(); - /*! - * Retrieves whether the counterexample option was set. - * - * @return True if the counterexample option was set. - */ - bool isCounterexampleSet() const; - - /*! - * Retrieves the name of the file to which the counterexample is to be written if the counterexample - * option was set. - * - * @return The name of the file to which the counterexample is to be written. - */ - std::string getCounterexampleFilename() const; - - /*! - * Retrieves whether the dont-fix-deadlocks option was set. - * - * @return True if the dont-fix-deadlocks option was set. - */ - bool isDontFixDeadlocksSet() const; - - /*! - * Overrides the option to not fix deadlocks by setting it to the specified value. As soon as the - * returned memento goes out of scope, the original value is restored. - * - * @param stateToSet The value that is to be set for the fix-deadlocks option. - * @return The memento that will eventually restore the original value. - */ - std::unique_ptr overrideDontFixDeadlocksSet(bool stateToSet); - /*! * Retrieves the selected equation solver. * @@ -166,10 +135,6 @@ namespace storm { Engine engine; // Define the string names of the options as constants. - static const std::string counterexampleOptionName; - static const std::string counterexampleOptionShortName; - static const std::string dontFixDeadlockOptionName; - static const std::string dontFixDeadlockOptionShortName; static const std::string eqSolverOptionName; static const std::string lpSolverOptionName; static const std::string smtSolverOptionName; diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp index 583f37c7f..98219969e 100644 --- a/src/storm/settings/modules/IOSettings.cpp +++ b/src/storm/settings/modules/IOSettings.cpp @@ -18,6 +18,7 @@ namespace storm { const std::string IOSettings::moduleName = "io"; const std::string IOSettings::exportDotOptionName = "exportdot"; + const std::string IOSettings::exportDotMaxWidthOptionName = "dot-maxwidth"; const std::string IOSettings::exportExplicitOptionName = "exportexplicit"; const std::string IOSettings::exportDdOptionName = "exportdd"; const std::string IOSettings::exportJaniDotOptionName = "exportjanidot"; @@ -50,9 +51,11 @@ namespace storm { const std::string IOSettings::qvbsRootOptionName = "qvbsroot"; IOSettings::IOSettings() : ModuleSettings(moduleName) { - this->addOption(storm::settings::OptionBuilder(moduleName, exportDotOptionName, "", "If given, the loaded model will be written to the specified file in the dot format.").setIsAdvanced() + this->addOption(storm::settings::OptionBuilder(moduleName, exportDotOptionName, false, "If given, the loaded model will be written to the specified file in the dot format.").setIsAdvanced() .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, exportJaniDotOptionName, "", "If given, the loaded jani model will be written to the specified file in the dot format.").setIsAdvanced() + this->addOption(storm::settings::OptionBuilder(moduleName, exportDotMaxWidthOptionName, false, "The maximal width for labels in the dot format. For longer lines a linebreak is inserted. Value 0 represents no linebreaks.").setIsAdvanced() + .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("width", "The maximal line width for the dot format. Default is 0 meaning no linebreaks.").setDefaultValueUnsignedInteger(0).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, exportJaniDotOptionName, false, "If given, the loaded jani model will be written to the specified file in the dot format.").setIsAdvanced() .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportCdfOptionName, false, "Exports the cumulative density function for reward bounded properties into a .csv file.").setIsAdvanced().setShortName(exportCdfOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("directory", "A path to an existing directory where the cdf files will be stored.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportSchedulerOptionName, false, "Exports the choices of an optimal scheduler to the given file (if supported by engine).").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The output file.").build()).build()); @@ -112,6 +115,10 @@ namespace storm { return this->getOption(exportDotOptionName).getArgumentByName("filename").getValueAsString(); } + size_t IOSettings::getExportDotMaxWidth() const { + return this->getOption(exportDotMaxWidthOptionName).getArgumentByName("width").getValueAsUnsignedInteger(); + } + bool IOSettings::isExportJaniDotSet() const { return this->getOption(exportJaniDotOptionName).getHasOptionBeenSet(); } diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h index 9731a272c..91cc3b765 100644 --- a/src/storm/settings/modules/IOSettings.h +++ b/src/storm/settings/modules/IOSettings.h @@ -37,6 +37,13 @@ namespace storm { */ std::string getExportDotFilename() const; + /*! + * Retrieves the maximal width for labels in the dot format. + * + * @return The maximal width. + */ + size_t getExportDotMaxWidth() const; + /*! * Retrieves whether the export-to-dot option for jani was set. * @@ -325,6 +332,7 @@ namespace storm { private: // Define the string names of the options as constants. static const std::string exportDotOptionName; + static const std::string exportDotMaxWidthOptionName; static const std::string exportJaniDotOptionName; static const std::string exportExplicitOptionName; static const std::string exportDdOptionName; diff --git a/src/storm/transformer/NonMarkovianChainTransformer.h b/src/storm/transformer/NonMarkovianChainTransformer.h index 317be4b2d..8382f7419 100644 --- a/src/storm/transformer/NonMarkovianChainTransformer.h +++ b/src/storm/transformer/NonMarkovianChainTransformer.h @@ -4,7 +4,7 @@ namespace storm { namespace transformer { /** - * Transformer for eliminating chains of non-Markovian states (instantaneous path fragment leading to the same outcome) from Markov Automata + * Transformer for eliminating chains of non-Markovian states (instantaneous path fragment leading to the same outcome) from Markov automata. */ template> class NonMarkovianChainTransformer { @@ -14,32 +14,29 @@ namespace storm { * Generates a model with the same basic behavior as the input, but eliminates non-Markovian chains. * If no non-determinism occurs, a CTMC is generated. * - * @param ma the input Markov Automaton - * @param preserveLabels if set, the procedure considers the labels of non-Markovian states when eliminating states - * @return a reference to the new Mmodel after eliminating non-Markovian states + * @param ma The input Markov Automaton. + * @param preserveLabels If set, the procedure considers the labels of non-Markovian states when eliminating states. + * @return A reference to the new model after eliminating non-Markovian states. */ - static std::shared_ptr< - models::sparse::Model < ValueType, RewardModelType>> eliminateNonmarkovianStates(std::shared_ptr< - models::sparse::MarkovAutomaton < ValueType, RewardModelType>> ma, - bool preserveLabels = true + static std::shared_ptr> eliminateNonmarkovianStates( + std::shared_ptr> ma, bool preserveLabels = true ); /** * Check if the property specified by the given formula is preserved by the transformation. * - * @param formula the formula to check - * @return true, if the property is preserved + * @param formula The formula to check. + * @return True, if the property is preserved. */ - static bool preservesFormula(storm::logic::Formula const &formula); + static bool preservesFormula(storm::logic::Formula const& formula); /** * Checks for the given formulae if the specified properties are preserved and removes formulae of properties which are not preserved. * - * @param formulas - * @return vector containing all fomulae which are valid for the transformed model + * @param formulas Formulae. + * @return Vector containing all fomulae which are valid for the transformed model. */ - static std::vector> - checkAndTransformFormulas(std::vector> const &formulas); + static std::vector> checkAndTransformFormulas(std::vector> const& formulas); }; } } diff --git a/src/storm/utility/counterexamples.h b/src/storm/utility/counterexamples.h deleted file mode 100644 index 6705e40f7..000000000 --- a/src/storm/utility/counterexamples.h +++ /dev/null @@ -1,128 +0,0 @@ -#ifndef STORM_UTILITY_COUNTEREXAMPLE_H_ -#define STORM_UTILITY_COUNTEREXAMPLE_H_ - -#include -#include - -#include "storm/storage/sparse/PrismChoiceOrigins.h" - -namespace storm { - namespace utility { - namespace counterexamples { - - /*! - * Computes a set of labels that is executed along all paths from any state to a target state. - * - * @param labelSet the considered label sets (a label set is assigned to each choice) - * - * @return The set of labels that is visited on all paths from any state to a target state. - */ - template - std::vector> getGuaranteedLabelSets(storm::models::sparse::Model const& model, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, storm::storage::FlatSet const& relevantLabels) { - STORM_LOG_THROW(model.getNumberOfChoices() == labelSets.size(), storm::exceptions::InvalidArgumentException, "The given number of labels does not match the number of choices."); - - // Get some data from the model for convenient access. - storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); - std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); - storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - - // Now we compute the set of labels that is present on all paths from the initial to the target states. - std::vector> analysisInformation(model.getNumberOfStates(), relevantLabels); - - std::queue worklist; - storm::storage::BitVector statesInWorkList(model.getNumberOfStates()); - storm::storage::BitVector markedStates(model.getNumberOfStates()); - - // Initially, put all predecessors of target states in the worklist and empty the analysis information them. - for (auto state : psiStates) { - analysisInformation[state] = storm::storage::FlatSet(); - for (auto const& predecessorEntry : backwardTransitions.getRow(state)) { - if (predecessorEntry.getColumn() != state && !statesInWorkList.get(predecessorEntry.getColumn()) && !psiStates.get(predecessorEntry.getColumn())) { - worklist.push(predecessorEntry.getColumn()); - statesInWorkList.set(predecessorEntry.getColumn()); - markedStates.set(state); - } - } - } - - uint_fast64_t iters = 0; - while (!worklist.empty()) { - ++iters; - uint_fast64_t const& currentState = worklist.front(); - - size_t analysisInformationSizeBefore = analysisInformation[currentState].size(); - - // Iterate over the successor states for all choices and compute new analysis information. - for (uint_fast64_t currentChoice = nondeterministicChoiceIndices[currentState]; currentChoice < nondeterministicChoiceIndices[currentState + 1]; ++currentChoice) { - bool modifiedChoice = false; - - for (auto const& entry : transitionMatrix.getRow(currentChoice)) { - if (markedStates.get(entry.getColumn())) { - modifiedChoice = true; - break; - } - } - - // If we can reach the target state with this choice, we need to intersect the current - // analysis information with the union of the new analysis information of the target state - // and the choice labels. - if (modifiedChoice) { - for (auto const& entry : transitionMatrix.getRow(currentChoice)) { - if (markedStates.get(entry.getColumn())) { - storm::storage::FlatSet tmpIntersection; - std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), analysisInformation[entry.getColumn()].begin(), analysisInformation[entry.getColumn()].end(), std::inserter(tmpIntersection, tmpIntersection.begin())); - std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), labelSets[currentChoice].begin(), labelSets[currentChoice].end(), std::inserter(tmpIntersection, tmpIntersection.begin())); - analysisInformation[currentState] = std::move(tmpIntersection); - } - } - } - } - - // If the analysis information changed, we need to update it and put all the predecessors of this - // state in the worklist. - if (analysisInformation[currentState].size() != analysisInformationSizeBefore) { - for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) { - // Only put the predecessor in the worklist if it's not already a target state. - if (!psiStates.get(predecessorEntry.getColumn()) && !statesInWorkList.get(predecessorEntry.getColumn())) { - worklist.push(predecessorEntry.getColumn()); - statesInWorkList.set(predecessorEntry.getColumn()); - } - } - markedStates.set(currentState, true); - } else { - markedStates.set(currentState, false); - } - - worklist.pop(); - statesInWorkList.set(currentState, false); - } - - return analysisInformation; - } - - /*! - * Computes a set of labels that is executed along all paths from an initial state to a target state. - * - * @param labelSet the considered label sets (a label set is assigned to each choice) - * - * @return The set of labels that is executed on all paths from an initial state to a target state. - */ - template - storm::storage::FlatSet getGuaranteedLabelSet(storm::models::sparse::Model const& model, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, storm::storage::FlatSet const& relevantLabels) { - std::vector> guaranteedLabels = getGuaranteedLabelSets(model, labelSets, psiStates, relevantLabels); - - storm::storage::FlatSet knownLabels(relevantLabels); - storm::storage::FlatSet tempIntersection; - for (auto initialState : model.getInitialStates()) { - std::set_intersection(knownLabels.begin(), knownLabels.end(), guaranteedLabels[initialState].begin(), guaranteedLabels[initialState].end(), std::inserter(tempIntersection, tempIntersection.end())); - std::swap(knownLabels, tempIntersection); - } - - return knownLabels; - } - - } // namespace counterexample - } // namespace utility -} // namespace storm - -#endif /* STORM_UTILITY_COUNTEREXAMPLE_H_ */ diff --git a/src/storm/utility/export.h b/src/storm/utility/export.h index babf90d63..f067f88b3 100644 --- a/src/storm/utility/export.h +++ b/src/storm/utility/export.h @@ -8,40 +8,37 @@ #include "storm/utility/file.h" - namespace storm { namespace utility { - - - template + template inline void exportDataToCSVFile(std::string filepath, std::vector> const& data, boost::optional> const& header1 = boost::none, boost::optional> const& header2 = boost::none) { std::ofstream filestream; storm::utility::openFile(filepath, filestream); - + if (header1) { - for(auto columnIt = header1->begin(); columnIt != header1->end(); ++columnIt) { - if(columnIt != header1->begin()) { + for (auto columnIt = header1->begin(); columnIt != header1->end(); ++columnIt) { + if (columnIt != header1->begin()) { filestream << ","; } filestream << *columnIt; } filestream << std::endl; } - + if (header2) { - for(auto columnIt = header2->begin(); columnIt != header2->end(); ++columnIt) { - if(columnIt != header2->begin()) { + for (auto columnIt = header2->begin(); columnIt != header2->end(); ++columnIt) { + if (columnIt != header2->begin()) { filestream << ","; } filestream << *columnIt; } filestream << std::endl; } - + for (auto const& row : data) { - for(auto columnIt = row.begin(); columnIt != row.end(); ++columnIt) { - if(columnIt != row.begin()) { + for (auto columnIt = row.begin(); columnIt != row.end(); ++columnIt) { + if (columnIt != row.begin()) { filestream << ","; } filestream << *columnIt; @@ -50,6 +47,31 @@ namespace storm { } storm::utility::closeFile(filestream); } + + /*! + * Output list of strings with linebreaks according to fixed width. + * Strings are printed with comma separator. + * If the length of the current line is greater than maxWidth, a linebreak is inserted. + * @param stream Output stream. + * @param output List of strings to output. + * @param maxWidth Maximal width after which a linebreak is inserted. Value 0 represents no linebreaks. + */ + template + inline void outputFixedWidth(std::ostream& stream, Container const& output, size_t maxWidth = 30) { + size_t curLength = 0; + for (auto s : output) { + if (curLength > 0) { + stream << ", "; + curLength += 2; + } + stream << s; + curLength += s.length(); + if (maxWidth > 0 && curLength >= maxWidth) { + stream << std::endl; + curLength = 0; + } + } + } } } diff --git a/src/test/storm-dft/api/DftApproximationTest.cpp b/src/test/storm-dft/api/DftApproximationTest.cpp index e17fa200c..40c3eb6ff 100644 --- a/src/test/storm-dft/api/DftApproximationTest.cpp +++ b/src/test/storm-dft/api/DftApproximationTest.cpp @@ -54,7 +54,7 @@ namespace { std::pair analyzeMTTF(std::string const& file, double errorBound) { std::shared_ptr> dft = storm::api::loadDFTGalileoFile(file); - EXPECT_TRUE(storm::api::isWellFormed(*dft)); + EXPECT_TRUE(storm::api::isWellFormed(*dft).first); std::string property = "T=? [F \"failed\"]"; std::vector> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, config.useSR, false, {}, true, errorBound, @@ -64,7 +64,7 @@ namespace { std::pair analyzeTimebound(std::string const& file, double timeBound, double errorBound) { std::shared_ptr> dft = storm::api::loadDFTGalileoFile(file); - EXPECT_TRUE(storm::api::isWellFormed(*dft)); + EXPECT_TRUE(storm::api::isWellFormed(*dft).first); std::stringstream propertyStream; propertyStream << "P=? [F<=" << timeBound << " \"failed\"]"; std::vector > properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(propertyStream.str())); diff --git a/src/test/storm-dft/api/DftModelBuildingTest.cpp b/src/test/storm-dft/api/DftModelBuildingTest.cpp index a934ea1e2..8e4a6262a 100644 --- a/src/test/storm-dft/api/DftModelBuildingTest.cpp +++ b/src/test/storm-dft/api/DftModelBuildingTest.cpp @@ -11,7 +11,7 @@ namespace { // Initialize std::string file = STORM_TEST_RESOURCES_DIR "/dft/dont_care.dft"; std::shared_ptr> dft = storm::api::loadDFTGalileoFile(file); - EXPECT_TRUE(storm::api::isWellFormed(*dft)); + EXPECT_TRUE(storm::api::isWellFormed(*dft).first); std::string property = "Tmin=? [F \"failed\"]"; std::vector> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); std::map>> emptySymmetry; diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp index 14d640e1f..1d4501132 100644 --- a/src/test/storm-dft/api/DftModelCheckerTest.cpp +++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp @@ -77,7 +77,7 @@ namespace { storm::transformations::dft::DftTransformator dftTransformator = storm::transformations::dft::DftTransformator(); std::shared_ptr> dft = dftTransformator.transformBinaryFDEPs( *(storm::api::loadDFTGalileoFile(file))); - EXPECT_TRUE(storm::api::isWellFormed(*dft)); + EXPECT_TRUE(storm::api::isWellFormed(*dft).first); std::string property = "Tmin=? [F \"failed\"]"; std::vector> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); std::set relevantEvents; @@ -92,7 +92,7 @@ namespace { double analyzeReliability(std::string const &file, double bound) { storm::transformations::dft::DftTransformator dftTransformator = storm::transformations::dft::DftTransformator(); std::shared_ptr> dft = dftTransformator.transformBinaryFDEPs(*(storm::api::loadDFTGalileoFile(file))); - EXPECT_TRUE(storm::api::isWellFormed(*dft)); + EXPECT_TRUE(storm::api::isWellFormed(*dft).first); std::string property = "Pmin=? [F<=" + std::to_string(bound) + " \"failed\"]"; std::vector> properties = storm::api::extractFormulasFromProperties( storm::api::parseProperties(property)); diff --git a/src/test/storm-dft/api/DftParserTest.cpp b/src/test/storm-dft/api/DftParserTest.cpp index dfa7ad769..e57502889 100644 --- a/src/test/storm-dft/api/DftParserTest.cpp +++ b/src/test/storm-dft/api/DftParserTest.cpp @@ -10,7 +10,7 @@ namespace { std::shared_ptr> dft = storm::api::loadDFTGalileoFile(file); EXPECT_EQ(3ul, dft->nrElements()); EXPECT_EQ(2ul, dft->nrBasicElements()); - EXPECT_TRUE(storm::api::isWellFormed(*dft)); + EXPECT_TRUE(storm::api::isWellFormed(*dft).first); } TEST(DftParserTest, LoadFromJsonFile) { @@ -18,7 +18,7 @@ namespace { std::shared_ptr> dft = storm::api::loadDFTJsonFile(file); EXPECT_EQ(3ul, dft->nrElements()); EXPECT_EQ(2ul, dft->nrBasicElements()); - EXPECT_TRUE(storm::api::isWellFormed(*dft)); + EXPECT_TRUE(storm::api::isWellFormed(*dft).first); } TEST(DftParserTest, CatchCycles) { diff --git a/src/test/storm-dft/api/DftSmtTest.cpp b/src/test/storm-dft/api/DftSmtTest.cpp index f23a433c9..fb6ab15de 100644 --- a/src/test/storm-dft/api/DftSmtTest.cpp +++ b/src/test/storm-dft/api/DftSmtTest.cpp @@ -7,7 +7,7 @@ namespace { TEST(DftSmtTest, AndTest) { std::shared_ptr> dft = storm::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/and.dft"); - EXPECT_TRUE(storm::api::isWellFormed(*dft)); + EXPECT_TRUE(storm::api::isWellFormed(*dft).first); storm::modelchecker::DFTASFChecker smtChecker(*dft); smtChecker.convert(); smtChecker.toSolver(); @@ -17,7 +17,7 @@ namespace { TEST(DftSmtTest, PandTest) { std::shared_ptr> dft = storm::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/pand.dft"); - EXPECT_TRUE(storm::api::isWellFormed(*dft)); + EXPECT_TRUE(storm::api::isWellFormed(*dft).first); storm::modelchecker::DFTASFChecker smtChecker(*dft); smtChecker.convert(); smtChecker.toSolver(); @@ -27,7 +27,7 @@ namespace { TEST(DftSmtTest, SpareTest) { std::shared_ptr> dft = storm::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/spare_two_modules.dft"); - EXPECT_TRUE(storm::api::isWellFormed(*dft)); + EXPECT_TRUE(storm::api::isWellFormed(*dft).first); storm::modelchecker::DFTASFChecker smtChecker(*dft); smtChecker.convert(); smtChecker.toSolver(); @@ -38,7 +38,7 @@ namespace { TEST(DftSmtTest, BoundTest) { std::shared_ptr> dft = storm::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/spare5.dft"); - EXPECT_TRUE(storm::api::isWellFormed(*dft)); + EXPECT_TRUE(storm::api::isWellFormed(*dft).first); storm::modelchecker::DFTASFChecker smtChecker(*dft); smtChecker.convert(); smtChecker.toSolver(); @@ -49,7 +49,7 @@ namespace { TEST(DftSmtTest, FDEPBoundTest) { std::shared_ptr> dft = storm::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/fdep_bound.dft"); - EXPECT_TRUE(storm::api::isWellFormed(*dft)); + EXPECT_TRUE(storm::api::isWellFormed(*dft, false).first); storm::modelchecker::DFTASFChecker smtChecker(*dft); smtChecker.convert(); smtChecker.toSolver(); @@ -60,37 +60,37 @@ namespace { TEST(DftSmtTest, FDEPConflictTest) { std::shared_ptr> dft = storm::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/spare_conflict_test.dft"); - EXPECT_TRUE(storm::api::isWellFormed(*dft)); + EXPECT_TRUE(storm::api::isWellFormed(*dft).first); std::vector true_vector(10, true); dft->setDynamicBehaviorInfo(); EXPECT_EQ(dft->getDynamicBehavior(), true_vector); - EXPECT_TRUE(storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, true).empty()); + EXPECT_TRUE(storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, true).empty()); } TEST(DftSmtTest, FDEPConflictSPARETest) { std::shared_ptr> dft = storm::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/spare_conflict_test.dft"); - EXPECT_TRUE(storm::api::isWellFormed(*dft)); + EXPECT_TRUE(storm::api::isWellFormed(*dft).first); std::vector true_vector(10, true); dft->setDynamicBehaviorInfo(); EXPECT_EQ(dft->getDynamicBehavior(), true_vector); - EXPECT_TRUE(storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, true).empty()); + EXPECT_TRUE(storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, true).empty()); } TEST(DftSmtTest, FDEPConflictSEQTest) { std::shared_ptr> dft = storm::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/seq_conflict_test.dft"); - EXPECT_TRUE(storm::api::isWellFormed(*dft)); + EXPECT_TRUE(storm::api::isWellFormed(*dft).first); std::vector expected_dynamic_vector(dft->nrElements(), true); expected_dynamic_vector.at(dft->getTopLevelIndex()) = false; dft->setDynamicBehaviorInfo(); EXPECT_EQ(dft->getDynamicBehavior(), expected_dynamic_vector); - EXPECT_EQ(storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, true).size(), uint64_t(3)); + EXPECT_EQ(storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, true).size(), uint64_t(3)); } } \ No newline at end of file diff --git a/src/test/storm-pars/analysis/AssumptionMakerTest.cpp b/src/test/storm-pars/analysis/AssumptionMakerTest.cpp index 7ede1cc08..ea5a838b0 100644 --- a/src/test/storm-pars/analysis/AssumptionMakerTest.cpp +++ b/src/test/storm-pars/analysis/AssumptionMakerTest.cpp @@ -53,14 +53,14 @@ TEST(AssumptionMakerTest, Brp_without_bisimulation) { auto *extender = new storm::analysis::OrderExtender(dtmc); auto criticalTuple = extender->toOrder(formulas); - ASSERT_EQ(183, std::get<1>(criticalTuple)); - ASSERT_EQ(186, std::get<2>(criticalTuple)); + ASSERT_EQ(183ul, std::get<1>(criticalTuple)); + ASSERT_EQ(186ul, std::get<2>(criticalTuple)); auto assumptionChecker = storm::analysis::AssumptionChecker(formulas[0], dtmc, region, 3); auto assumptionMaker = storm::analysis::AssumptionMaker(&assumptionChecker, dtmc->getNumberOfStates(), true); auto result = assumptionMaker.createAndCheckAssumption(std::get<1>(criticalTuple), std::get<2>(criticalTuple), std::get<0>(criticalTuple)); - EXPECT_EQ(3, result.size()); + EXPECT_EQ(3ul, result.size()); bool foundFirst = false; bool foundSecond = false; @@ -123,15 +123,15 @@ TEST(AssumptionMakerTest, Brp_without_bisimulation_no_validation) { auto *extender = new storm::analysis::OrderExtender(dtmc); auto criticalTuple = extender->toOrder(formulas); - ASSERT_EQ(183, std::get<1>(criticalTuple)); - ASSERT_EQ(186, std::get<2>(criticalTuple)); + ASSERT_EQ(183ul, std::get<1>(criticalTuple)); + ASSERT_EQ(186ul, std::get<2>(criticalTuple)); auto assumptionChecker = storm::analysis::AssumptionChecker(formulas[0], dtmc, region, 3); // This one does not validate the assumptions! auto assumptionMaker = storm::analysis::AssumptionMaker(&assumptionChecker, dtmc->getNumberOfStates(), false); auto result = assumptionMaker.createAndCheckAssumption(std::get<1>(criticalTuple), std::get<2>(criticalTuple), std::get<0>(criticalTuple)); - EXPECT_EQ(3, result.size()); + EXPECT_EQ(3ul, result.size()); bool foundFirst = false; bool foundSecond = false; @@ -188,8 +188,8 @@ TEST(AssumptionMakerTest, Simple1) { auto vars = storm::models::sparse::getProbabilityParameters(*dtmc); auto region = storm::api::parseRegion("0.00001 <= p <= 0.999999", vars); - ASSERT_EQ(dtmc->getNumberOfStates(), 5); - ASSERT_EQ(dtmc->getNumberOfTransitions(), 8); + ASSERT_EQ(dtmc->getNumberOfStates(), 5ul); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 8ul); storm::storage::BitVector above(5); above.set(3); @@ -204,7 +204,7 @@ TEST(AssumptionMakerTest, Simple1) { auto assumptionMaker = storm::analysis::AssumptionMaker(&assumptionChecker, dtmc->getNumberOfStates(), true); auto result = assumptionMaker.createAndCheckAssumption(1, 2, order); - EXPECT_EQ(3, result.size()); + EXPECT_EQ(3ul, result.size()); bool foundFirst = false; bool foundSecond = false; @@ -260,8 +260,8 @@ TEST(AssumptionMakerTest, Simple2) { auto vars = storm::models::sparse::getProbabilityParameters(*dtmc); auto region = storm::api::parseRegion("0.00001 <= p <= 0.999999", vars); - ASSERT_EQ(dtmc->getNumberOfStates(), 5); - ASSERT_EQ(dtmc->getNumberOfTransitions(), 8); + ASSERT_EQ(dtmc->getNumberOfStates(), 5ul); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 8ul); storm::storage::BitVector above(5); above.set(3); @@ -277,9 +277,7 @@ TEST(AssumptionMakerTest, Simple2) { auto assumptionMaker = storm::analysis::AssumptionMaker(&assumptionChecker, dtmc->getNumberOfStates(), true); auto result = assumptionMaker.createAndCheckAssumption(1, 2, order); - auto itr = result.begin(); - - EXPECT_EQ(3, result.size()); + EXPECT_EQ(3ul, result.size()); bool foundFirst = false; bool foundSecond = false; diff --git a/src/test/storm/parser/DeterministicSparseTransitionParserTest.cpp b/src/test/storm/parser/DeterministicSparseTransitionParserTest.cpp index 737d8ff04..c71699233 100644 --- a/src/test/storm/parser/DeterministicSparseTransitionParserTest.cpp +++ b/src/test/storm/parser/DeterministicSparseTransitionParserTest.cpp @@ -11,7 +11,7 @@ #include "storm-parsers/parser/DeterministicSparseTransitionParser.h" #include "storm/storage/SparseMatrix.h" #include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/CoreSettings.h" +#include "storm/settings/modules/BuildSettings.h" #include "storm/settings/SettingMemento.h" #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/WrongFormatException.h" @@ -179,7 +179,7 @@ TEST(DeterministicSparseTransitionParserTest, MixedTransitionOrder) { TEST(DeterministicSparseTransitionParserTest, FixDeadlocks) { // Set the fixDeadlocks flag temporarily. It is set to its old value once the deadlockOption object is destructed. - std::unique_ptr fixDeadlocks = storm::settings::mutableCoreSettings().overrideDontFixDeadlocksSet(false); + std::unique_ptr fixDeadlocks = storm::settings::mutableBuildSettings().overrideDontFixDeadlocksSet(false); // Parse a transitions file with the fixDeadlocks Flag set and test if it works. storm::storage::SparseMatrix transitionMatrix = storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_TEST_RESOURCES_DIR "/tra/dtmc_deadlock.tra"); @@ -200,7 +200,7 @@ TEST(DeterministicSparseTransitionParserTest, FixDeadlocks) { TEST(DeterministicSparseTransitionParserTest, DontFixDeadlocks) { // Try to parse a transitions file containing a deadlock state with the fixDeadlocksFlag unset. This should throw an exception. - std::unique_ptr dontFixDeadlocks = storm::settings::mutableCoreSettings().overrideDontFixDeadlocksSet(true); + std::unique_ptr dontFixDeadlocks = storm::settings::mutableBuildSettings().overrideDontFixDeadlocksSet(true); ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_TEST_RESOURCES_DIR "/tra/dtmc_deadlock.tra"), storm::exceptions::WrongFormatException); } diff --git a/src/test/storm/parser/MarkovAutomatonSparseTransitionParserTest.cpp b/src/test/storm/parser/MarkovAutomatonSparseTransitionParserTest.cpp index f29a5689d..f09c2144f 100644 --- a/src/test/storm/parser/MarkovAutomatonSparseTransitionParserTest.cpp +++ b/src/test/storm/parser/MarkovAutomatonSparseTransitionParserTest.cpp @@ -8,7 +8,7 @@ #include "gtest/gtest.h" #include "storm-config.h" #include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/CoreSettings.h" +#include "storm/settings/modules/BuildSettings.h" #include @@ -187,7 +187,7 @@ TEST(MarkovAutomatonSparseTransitionParserTest, Whitespaces) { TEST(MarkovAutomatonSparseTransitionParserTest, FixDeadlocks) { // Set the fixDeadlocks flag temporarily. It is set to its old value once the deadlockOption object is destructed. - std::unique_ptr fixDeadlocks = storm::settings::mutableCoreSettings().overrideDontFixDeadlocksSet(false); + std::unique_ptr fixDeadlocks = storm::settings::mutableBuildSettings().overrideDontFixDeadlocksSet(false); // Parse a Markov Automaton transition file with the fixDeadlocks Flag set and test if it works. typename storm::parser::MarkovAutomatonSparseTransitionParser<>::Result result = storm::parser::MarkovAutomatonSparseTransitionParser<>::parseMarkovAutomatonTransitions(STORM_TEST_RESOURCES_DIR "/tra/ma_deadlock.tra"); @@ -206,7 +206,7 @@ TEST(MarkovAutomatonSparseTransitionParserTest, FixDeadlocks) { TEST(MarkovAutomatonSparseTransitionParserTest, DontFixDeadlocks) { // Try to parse a Markov Automaton transition file containing a deadlock state with the fixDeadlocksFlag unset. This should throw an exception. - std::unique_ptr dontFixDeadlocks = storm::settings::mutableCoreSettings().overrideDontFixDeadlocksSet(true); + std::unique_ptr dontFixDeadlocks = storm::settings::mutableBuildSettings().overrideDontFixDeadlocksSet(true); ASSERT_THROW(storm::parser::MarkovAutomatonSparseTransitionParser<>::parseMarkovAutomatonTransitions(STORM_TEST_RESOURCES_DIR "/tra/ma_deadlock.tra"), storm::exceptions::WrongFormatException); } diff --git a/src/test/storm/parser/NondeterministicSparseTransitionParserTest.cpp b/src/test/storm/parser/NondeterministicSparseTransitionParserTest.cpp index 9c740144f..26f70612b 100644 --- a/src/test/storm/parser/NondeterministicSparseTransitionParserTest.cpp +++ b/src/test/storm/parser/NondeterministicSparseTransitionParserTest.cpp @@ -13,7 +13,7 @@ #include "storm/settings/SettingMemento.h" #include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/CoreSettings.h" +#include "storm/settings/modules/BuildSettings.h" #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/WrongFormatException.h" @@ -210,7 +210,7 @@ TEST(NondeterministicSparseTransitionParserTest, MixedTransitionOrder) { TEST(NondeterministicSparseTransitionParserTest, FixDeadlocks) { // Set the fixDeadlocks flag temporarily. It is set to its old value once the deadlockOption object is destructed. - std::unique_ptr fixDeadlocks = storm::settings::mutableCoreSettings().overrideDontFixDeadlocksSet(false); + std::unique_ptr fixDeadlocks = storm::settings::mutableBuildSettings().overrideDontFixDeadlocksSet(false); // Parse a transitions file with the fixDeadlocks Flag set and test if it works. storm::storage::SparseMatrix result(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_TEST_RESOURCES_DIR "/tra/mdp_deadlock.tra")); @@ -251,7 +251,7 @@ TEST(NondeterministicSparseTransitionParserTest, FixDeadlocks) { TEST(NondeterministicSparseTransitionParserTest, DontFixDeadlocks) { // Try to parse a transitions file containing a deadlock state with the fixDeadlocksFlag unset. This should throw an exception. - std::unique_ptr dontFixDeadlocks = storm::settings::mutableCoreSettings().overrideDontFixDeadlocksSet(true); + std::unique_ptr dontFixDeadlocks = storm::settings::mutableBuildSettings().overrideDontFixDeadlocksSet(true); ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_TEST_RESOURCES_DIR "/tra/mdp_deadlock.tra"), storm::exceptions::WrongFormatException); }