From 743ce2b023079a6dd678b46660a9b858a960f7bf Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 22 Dec 2016 12:21:00 +0100 Subject: [PATCH 01/37] Export DFT to Cytoscape JSON format --- src/storm-dft-cli/storm-dyftee.cpp | 12 +- .../settings/modules/DFTSettings.cpp | 12 +- src/storm-dft/settings/modules/DFTSettings.h | 15 +++ src/storm-dft/storage/dft/DFTElementType.h | 2 +- src/storm-dft/storage/dft/DftJsonExporter.cpp | 122 ++++++++++++++++++ src/storm-dft/storage/dft/DftJsonExporter.h | 47 +++++++ 6 files changed, 207 insertions(+), 3 deletions(-) create mode 100644 src/storm-dft/storage/dft/DftJsonExporter.cpp create mode 100644 src/storm-dft/storage/dft/DftJsonExporter.h diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp index f246438fe..78e411df8 100644 --- a/src/storm-dft-cli/storm-dyftee.cpp +++ b/src/storm-dft-cli/storm-dyftee.cpp @@ -19,7 +19,7 @@ #include "storm-dft/modelchecker/dft/DFTModelChecker.h" #include "storm-dft/modelchecker/dft/DFTASFChecker.h" #include "storm-dft/transformations/DftToGspnTransformator.h" - +#include "storm-dft/storage/dft/DftJsonExporter.h" #include "storm-dft/settings/modules/DFTSettings.h" @@ -129,6 +129,16 @@ int main(const int argc, const char** argv) { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); } + if (dftSettings.isExportToJson()) { + STORM_LOG_THROW(dftSettings.isDftFileSet(), storm::exceptions::InvalidSettingsException, "No input model in Galileo format given."); + storm::parser::DFTGalileoParser parser; + storm::storage::DFT dft = parser.parseDFT(dftSettings.getDftFilename()); + // Export to json + storm::storage::DftJsonExporter::toFile(dft, dftSettings.getExportJsonFilename()); + storm::utility::cleanUp(); + return 0; + } + if (dftSettings.isTransformToGspn()) { std::shared_ptr> dft; diff --git a/src/storm-dft/settings/modules/DFTSettings.cpp b/src/storm-dft/settings/modules/DFTSettings.cpp index 898360c4b..6af1d9678 100644 --- a/src/storm-dft/settings/modules/DFTSettings.cpp +++ b/src/storm-dft/settings/modules/DFTSettings.cpp @@ -32,6 +32,7 @@ namespace storm { const std::string DFTSettings::minValueOptionName = "min"; const std::string DFTSettings::maxValueOptionName = "max"; const std::string DFTSettings::transformToGspnOptionName = "gspn"; + const std::string DFTSettings::exportToJsonOptionName = "export-json"; #ifdef STORM_HAVE_Z3 const std::string DFTSettings::solveWithSmtOptionName = "smt"; #endif @@ -55,8 +56,9 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, solveWithSmtOptionName, true, "Solve the DFT with SMT.").build()); #endif this->addOption(storm::settings::OptionBuilder(moduleName, transformToGspnOptionName, false, "Transform DFT to GSPN.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, exportToJsonOptionName, false, "Export the model to the Cytoscape JSON format.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file to export to.").build()).build()); } - + bool DFTSettings::isDftFileSet() const { return this->getOption(dftFileOptionName).getHasOptionBeenSet(); } @@ -141,6 +143,14 @@ namespace storm { return this->getOption(transformToGspnOptionName).getHasOptionBeenSet(); } + bool DFTSettings::isExportToJson() const { + return this->getOption(exportToJsonOptionName).getHasOptionBeenSet(); + } + + std::string DFTSettings::getExportJsonFilename() const { + return this->getOption(exportToJsonOptionName).getArgumentByName("filename").getValueAsString(); + } + void DFTSettings::finalize() { } diff --git a/src/storm-dft/settings/modules/DFTSettings.h b/src/storm-dft/settings/modules/DFTSettings.h index c1a9df7e5..0d8695e2a 100644 --- a/src/storm-dft/settings/modules/DFTSettings.h +++ b/src/storm-dft/settings/modules/DFTSettings.h @@ -138,6 +138,20 @@ namespace storm { * @return True iff the option was set. */ bool isTransformToGspn() const; + + /*! + * Retrieves whether the export to Json file option was set. + * + * @return True if the export to json file option was set. + */ + bool isExportToJson() const; + + /*! + * Retrieves the name of the json file to export to. + * + * @return The name of the json file to export to. + */ + std::string getExportJsonFilename() const; #ifdef STORM_HAVE_Z3 /*! @@ -177,6 +191,7 @@ namespace storm { static const std::string solveWithSmtOptionName; #endif static const std::string transformToGspnOptionName; + static const std::string exportToJsonOptionName; }; diff --git a/src/storm-dft/storage/dft/DFTElementType.h b/src/storm-dft/storage/dft/DFTElementType.h index 800da161f..1527efe25 100644 --- a/src/storm-dft/storage/dft/DFTElementType.h +++ b/src/storm-dft/storage/dft/DFTElementType.h @@ -75,7 +75,7 @@ namespace storm { } inline std::ostream& operator<<(std::ostream& os, DFTElementType const& tp) { - return os << toString(tp) << std::endl; + return os << toString(tp); } diff --git a/src/storm-dft/storage/dft/DftJsonExporter.cpp b/src/storm-dft/storage/dft/DftJsonExporter.cpp new file mode 100644 index 000000000..89cb07287 --- /dev/null +++ b/src/storm-dft/storage/dft/DftJsonExporter.cpp @@ -0,0 +1,122 @@ +#include "DftJsonExporter.h" + +#include "storm/exceptions/NotImplementedException.h" +#include "storm/exceptions/FileIOException.h" + +#include +#include + +namespace storm { + namespace storage { + + template + size_t DftJsonExporter::currentId = 0; + + template + void DftJsonExporter::toFile(storm::storage::DFT const& dft, std::string const& filepath) { + std::ofstream ofs; + ofs.open(filepath, std::ofstream::out); + if(ofs.is_open()) { + toStream(dft, ofs); + ofs.close(); + } else { + STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Cannot open " << filepath); + } + } + + template + void DftJsonExporter::toStream(storm::storage::DFT const& dft, std::ostream& os) { + os << translate(dft).dump(4) << std::endl; + } + + template + modernjson::json DftJsonExporter::translate(storm::storage::DFT const& dft) { + modernjson::json jsonDft; + currentId = 0; + + // Nodes + modernjson::json jsonNodes; + for (size_t i = 0; i < dft.nrElements(); ++i) { + modernjson::json jsonNode = translateNode(dft.getElement(i)); + jsonDft.push_back(jsonNode); + } + + // Edges + modernjson::json jsonEdges; + for (size_t i = 0; i < dft.nrElements(); ++i) { + if (dft.isGate(i)) { + std::shared_ptr const> gate = dft.getGate(i); + for (size_t index = 0; index < gate->nrChildren(); ++index) { + DFTElementPointer child = gate->children()[index]; + modernjson::json jsonEdge = translateEdge(gate, child, index); + jsonDft.push_back(jsonEdge); + } + } + } + + return jsonDft; + } + + template + modernjson::json DftJsonExporter::translateNode(DFTElementCPointer const& element) { + modernjson::json nodeData; + nodeData["id"] = element->id(); + ++currentId; + STORM_LOG_ASSERT(element->id() == currentId-1, "Ids do not correspond"); + nodeData["name"] = element->name(); + + if (element->isGate()) { + // Set children for gate + std::shared_ptr const> gate = std::static_pointer_cast const>(element); + std::vector children; + for (DFTElementPointer const& child : gate->children()) { + children.push_back(child->id()); + } + nodeData["children"] = children; + } else if (element->isBasicElement()) { + // Set rates for BE + std::shared_ptr const> be = std::static_pointer_cast const>(element); + std::stringstream stream; + stream << be->activeFailureRate(); + nodeData["rate"] = stream.str(); + stream.clear(); + stream << (be->passiveFailureRate() / be->activeFailureRate()); + nodeData["dorm"] = stream.str(); + } + + modernjson::json jsonNode; + jsonNode["data"] = nodeData; + + jsonNode["group"] = "nodes"; + std::string type = storm::storage::toString(element->type()); + std::transform(type.begin(), type.end(), type.begin(), ::tolower); + jsonNode["classes"] = type; + return jsonNode; + } + + template + modernjson::json DftJsonExporter::translateEdge(std::shared_ptr const> const& gate, DFTElementCPointer const& child, size_t index) { + modernjson::json nodeData; + nodeData["id"] = currentId; + ++currentId; + nodeData["source"] = gate->id(); + nodeData["target"] = child->id(); + nodeData["index"] = index; + + modernjson::json jsonNode; + jsonNode["data"] = nodeData; + + jsonNode["group"] = "edges"; + jsonNode["classes"] = ""; + return jsonNode; + } + + // Explicitly instantiate the class. + template class DftJsonExporter; + +#ifdef STORM_HAVE_CARL + template class DftJsonExporter; +#endif + + } +} diff --git a/src/storm-dft/storage/dft/DftJsonExporter.h b/src/storm-dft/storage/dft/DftJsonExporter.h new file mode 100644 index 000000000..ef04750ba --- /dev/null +++ b/src/storm-dft/storage/dft/DftJsonExporter.h @@ -0,0 +1,47 @@ +#pragma once + +#include "storm/utility/macros.h" + +#include "storm-dft/storage/dft/DFT.h" + +// JSON parser +#include "json.hpp" +namespace modernjson { + using json = nlohmann::basic_json; +} + +namespace storm { + namespace storage { + + /** + * Exports a DFT into the JSON format for visualizing it. + */ + template + class DftJsonExporter { + + using DFTElementPointer = std::shared_ptr>; + using DFTElementCPointer = std::shared_ptr const>; + using DFTGatePointer = std::shared_ptr>; + + public: + + static void toFile(storm::storage::DFT const& dft, std::string const& filepath); + + static void toStream(storm::storage::DFT const& dft, std::ostream& os); + + static modernjson::json translate(storm::storage::DFT const& dft); + + + private: + + static size_t currentId; + + static modernjson::json translateNode(DFTElementCPointer const& element); + + static modernjson::json translateEdge(std::shared_ptr const> const& gate, DFTElementCPointer const& child, size_t index); + + + }; + + } +} From ade2b96903aaaa81b1726546f35004dcb2b82d5b Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 23 Dec 2016 11:10:33 +0100 Subject: [PATCH 02/37] Set correct edge id for JSON export --- src/storm-dft/storage/dft/DftJsonExporter.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/storm-dft/storage/dft/DftJsonExporter.cpp b/src/storm-dft/storage/dft/DftJsonExporter.cpp index 89cb07287..bcafb35be 100644 --- a/src/storm-dft/storage/dft/DftJsonExporter.cpp +++ b/src/storm-dft/storage/dft/DftJsonExporter.cpp @@ -97,7 +97,9 @@ namespace storm { template modernjson::json DftJsonExporter::translateEdge(std::shared_ptr const> const& gate, DFTElementCPointer const& child, size_t index) { modernjson::json nodeData; - nodeData["id"] = currentId; + std::stringstream stream; + stream << gate->id() << "e" << child->id(); + nodeData["id"] = stream.str(); ++currentId; nodeData["source"] = gate->id(); nodeData["target"] = child->id(); From 0d1923524c319f75db7507b65acad2f244c88bf8 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 7 Feb 2017 13:58:40 +0100 Subject: [PATCH 03/37] Json file can be used as dft input from now on as well --- src/storm-dft-cli/storm-dyftee.cpp | 24 ++++++++++++++++-------- 1 file changed, 16 insertions(+), 8 deletions(-) diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp index 3ec3b0ac0..9a8cd033b 100644 --- a/src/storm-dft-cli/storm-dyftee.cpp +++ b/src/storm-dft-cli/storm-dyftee.cpp @@ -36,23 +36,31 @@ /*! * Load DFT from filename, build corresponding Model and check against given property. * - * @param filename Path to DFT file in Galileo format. * @param property PCTC formula capturing the property to check. * @param symred Flag whether symmetry reduction should be used. * @param allowModularisation Flag whether modularisation should be applied if possible. * @param enableDC Flag whether Don't Care propagation should be used. */ template -void analyzeDFT(std::string filename, std::string property, bool symred, bool allowModularisation, bool enableDC, double approximationError) { - std::cout << "Running DFT analysis on file " << filename << " with property " << property << std::endl; +void analyzeDFT(std::string property, bool symred, bool allowModularisation, bool enableDC, double approximationError) { + storm::settings::modules::DFTSettings const& dftSettings = storm::settings::getModule(); + + std::shared_ptr> dft; + if (dftSettings.isDftJsonFileSet()) { + storm::parser::DFTJsonParser parser; + std::cout << "Running DFT analysis on file " << dftSettings.getDftJsonFilename() << " with property " << property << std::endl; + dft = std::make_shared>(parser.parseJson(dftSettings.getDftJsonFilename())); + } else { + storm::parser::DFTGalileoParser parser; + std::cout << "Running DFT analysis on file " << dftSettings.getDftFilename() << " with property " << property << std::endl; + dft = std::make_shared>(parser.parseDFT(dftSettings.getDftFilename())); + } - storm::parser::DFTGalileoParser parser; - storm::storage::DFT dft = parser.parseDFT(filename); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForExplicit(property)); STORM_LOG_ASSERT(formulas.size() == 1, "Wrong number of formulas."); storm::modelchecker::DFTModelChecker modelChecker; - modelChecker.check(dft, formulas[0], symred, allowModularisation, enableDC, approximationError); + modelChecker.check(*dft, formulas[0], symred, allowModularisation, enableDC, approximationError); modelChecker.printTimings(); modelChecker.printResult(); } @@ -247,12 +255,12 @@ int main(const int argc, const char** argv) { // From this point on we are ready to carry out the actual computations. if (parametric) { #ifdef STORM_HAVE_CARL - analyzeDFT(dftSettings.getDftFilename(), pctlFormula, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError); + analyzeDFT(pctlFormula, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError); #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameters are not supported in this build."); #endif } else { - analyzeDFT(dftSettings.getDftFilename(), pctlFormula, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError); + analyzeDFT(pctlFormula, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError); } // All operations have now been performed, so we clean up everything and terminate. From b571d176c0e6bc6308df39eaf6151ce517d4f8f1 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 7 Feb 2017 13:59:13 +0100 Subject: [PATCH 04/37] Parse toplevel element from json --- src/storm-dft/parser/DFTJsonParser.cpp | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp index 9a5c5d047..2d0ddfe39 100644 --- a/src/storm-dft/parser/DFTJsonParser.cpp +++ b/src/storm-dft/parser/DFTJsonParser.cpp @@ -66,6 +66,8 @@ namespace storm { parsedJson << file; file.close(); + std::string toplevelName = ""; + // Start by building mapping from ids to names std::map nameMapping; for (auto& element: parsedJson) { @@ -74,11 +76,13 @@ namespace storm { std::string id = data.at("id"); std::string name = data.at("name"); nameMapping[id] = name; + if (data.count("toplevel") > 0) { + STORM_LOG_ASSERT(toplevelName.empty(), "Toplevel element already defined."); + toplevelName = name; + } } } - - // TODO: avoid hack - std::string toplevelId = nameMapping["1"]; + std::cout << toplevelName << std::endl; for (auto& element : parsedJson) { bool success = true; @@ -130,7 +134,7 @@ namespace storm { STORM_LOG_THROW(success, storm::exceptions::FileIoException, "Error while adding element '" << element << "'."); } - if(!builder.setTopLevel(toplevelId)) { + if(!builder.setTopLevel(toplevelName)) { STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Top level id unknown."); } } From f9114bb54db32fe21d0fa50a294ec3dbbe3e0025 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 7 Feb 2017 18:59:39 +0100 Subject: [PATCH 05/37] Use name + id for getting unique json element --- src/storm-dft/parser/DFTJsonParser.cpp | 37 +++++++++++++++--------- src/storm-dft/storage/dft/DFTBuilder.cpp | 2 +- src/storm-dft/storage/dft/DFTBuilder.h | 2 +- 3 files changed, 26 insertions(+), 15 deletions(-) diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp index 2d0ddfe39..774f2cef8 100644 --- a/src/storm-dft/parser/DFTJsonParser.cpp +++ b/src/storm-dft/parser/DFTJsonParser.cpp @@ -74,27 +74,33 @@ namespace storm { if (element.at("classes") != "") { json data = element.at("data"); std::string id = data.at("id"); - std::string name = data.at("name"); + // Append to id to distinguish elements with the same name + std::stringstream stream; + stream << data.at("name").get() << "-" << id; + std::string name = stream.str(); nameMapping[id] = name; - if (data.count("toplevel") > 0) { - STORM_LOG_ASSERT(toplevelName.empty(), "Toplevel element already defined."); - toplevelName = name; - } } } std::cout << toplevelName << std::endl; for (auto& element : parsedJson) { + STORM_LOG_TRACE("Parsing: " << element); bool success = true; if (element.at("classes") == "") { continue; } json data = element.at("data"); - std::string name = data.at("name"); + std::stringstream stream; + stream << data.at("name").get() << "-" << data.at("id").get(); + std::string name = stream.str(); + if (data.count("toplevel") > 0) { + STORM_LOG_ASSERT(toplevelName.empty(), "Toplevel element already defined."); + toplevelName = name; + } std::vector childNames; if (data.count("children") > 0) { - for (auto& child : data.at("children")) { - childNames.push_back(nameMapping[child]); + for (json& child : data.at("children")) { + childNames.push_back(nameMapping[child.get()]); } } @@ -126,11 +132,16 @@ namespace storm { success = false; } - // Set layout positions - json position = element.at("position"); - double x = position.at("x"); - double y = position.at("y"); - builder.addLayoutInfo(name, x / 7, y / 7); + // Do not set layout for dependencies + // This does not work because dependencies might be splitted + // TODO: do splitting later in rewriting step + if (type != "fdep" && type != "pdep") { + // Set layout positions + json position = element.at("position"); + double x = position.at("x"); + double y = position.at("y"); + builder.addLayoutInfo(name, x / 7, y / 7); + } STORM_LOG_THROW(success, storm::exceptions::FileIoException, "Error while adding element '" << element << "'."); } diff --git a/src/storm-dft/storage/dft/DFTBuilder.cpp b/src/storm-dft/storage/dft/DFTBuilder.cpp index 974ffac8a..db779e3d9 100644 --- a/src/storm-dft/storage/dft/DFTBuilder.cpp +++ b/src/storm-dft/storage/dft/DFTBuilder.cpp @@ -159,7 +159,7 @@ namespace storm { template bool DFTBuilder::addStandardGate(std::string const& name, std::vector const& children, DFTElementType tp) { - STORM_LOG_ASSERT(children.size() > 0, "No child."); + STORM_LOG_ASSERT(children.size() > 0, "No child for " << name); if(mElements.count(name) != 0) { // Element with that name already exists. return false; diff --git a/src/storm-dft/storage/dft/DFTBuilder.h b/src/storm-dft/storage/dft/DFTBuilder.h index 636b5e5a1..598c1d765 100644 --- a/src/storm-dft/storage/dft/DFTBuilder.h +++ b/src/storm-dft/storage/dft/DFTBuilder.h @@ -103,7 +103,7 @@ namespace storm { //TODO Matthias: collect constraints for SMT solving //0 <= probability <= 1 if (binaryDependencies && !storm::utility::isOne(probability) && children.size() > 2) { - // Introduce additional element for first capturing the proabilistic dependency + // Introduce additional element for first capturing the probabilistic dependency std::string nameAdditional = name + "_additional"; addBasicElement(nameAdditional, storm::utility::zero(), storm::utility::zero()); // First consider probabilistic dependency From 69e2aac5c948e1b05b5cabcf11a8be1f02133e6d Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 7 Feb 2017 19:00:10 +0100 Subject: [PATCH 06/37] Fixed labeling when using multiple failed states --- src/storm-dft/builder/ExplicitDFTModelBuilder.h | 2 +- .../builder/ExplicitDFTModelBuilderApprox.cpp | 7 ++++--- .../builder/ExplicitDFTModelBuilderApprox.h | 14 +++++++++++++- 3 files changed, 18 insertions(+), 5 deletions(-) diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.h b/src/storm-dft/builder/ExplicitDFTModelBuilder.h index d3d191a8a..d61043368 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.h +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.h @@ -60,7 +60,7 @@ namespace storm { storm::storage::BitVectorHashMap mStates; std::vector> mPseudoStatesMapping; // vector of (id to concrete state, bitvector) size_t newIndex = 0; - bool mergeFailedStates = true; + bool mergeFailedStates = false; bool enableDC = true; size_t failedIndex = 0; size_t initialStateIndex = 0; diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp index 194372a30..48e564af0 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp @@ -169,7 +169,7 @@ namespace storm { modelComponents.deterministicModel = generator.isDeterministicModel(); // Fix the entries in the transition matrix according to the mapping of ids to row group indices - STORM_LOG_ASSERT(matrixBuilder.stateRemapping[initialStateIndex] == initialStateIndex, "Initial state should not be remapped."); + STORM_LOG_ASSERT(matrixBuilder.getRemapping(initialStateIndex) == initialStateIndex, "Initial state should not be remapped."); // TODO Matthias: do not consider all rows? STORM_LOG_TRACE("Remap matrix: " << matrixBuilder.stateRemapping << ", offset: " << matrixBuilder.mappingOffset); matrixBuilder.remap(); @@ -230,7 +230,7 @@ namespace storm { StateType skippedIndex = nrExpandedStates; std::map> skippedStatesNew; for (size_t id = 0; id < matrixBuilder.stateRemapping.size(); ++id) { - StateType index = matrixBuilder.stateRemapping[id]; + StateType index = matrixBuilder.getRemapping(id); auto itFind = skippedStates.find(index); if (itFind != skippedStates.end()) { // Set new mapping for skipped state @@ -405,6 +405,7 @@ namespace storm { modelComponents.stateLabeling = storm::models::sparse::StateLabeling(modelComponents.transitionMatrix.getRowGroupCount()); // Initial state modelComponents.stateLabeling.addLabel("init"); + STORM_LOG_ASSERT(matrixBuilder.getRemapping(initialStateIndex) == initialStateIndex, "Initial state should not be remapped."); modelComponents.stateLabeling.addLabelToState("init", initialStateIndex); // Label all states corresponding to their status (failed, failsafe, failed BE) if(labelOpts.buildFailLabel) { @@ -428,7 +429,7 @@ namespace storm { } for (auto const& stateIdPair : stateStorage.stateToId) { storm::storage::BitVector state = stateIdPair.first; - size_t stateId = stateIdPair.second; + size_t stateId = matrixBuilder.getRemapping(stateIdPair.second); if (!mergeFailedStates && labelOpts.buildFailLabel && dft.hasFailed(state, *stateGenerationInfo)) { modelComponents.stateLabeling.addLabelToState("failed", stateId); } diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h index 52bcbf2c9..6cf765d40 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h +++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h @@ -116,6 +116,18 @@ namespace storm { return currentRowGroup; } + /*! + * Get the remapped state for the given id. + * + * @param id State. + * + * @return Remapped index. + */ + StateType getRemapping(StateType id) { + STORM_LOG_ASSERT(id < stateRemapping.size(), "Invalid index for remapping."); + return stateRemapping[id]; + } + // Matrix builder. storm::storage::SparseMatrixBuilder builder; @@ -287,7 +299,7 @@ namespace storm { bool enableDC = true; //TODO Matthias: make changeable - const bool mergeFailedStates = true; + const bool mergeFailedStates = false; // Heuristic used for approximation storm::builder::ApproximationHeuristic usedHeuristic; From c7e7722af6963df204d19c4b74fe473c43a9d065 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 7 Feb 2017 19:17:01 +0100 Subject: [PATCH 07/37] Avoid whitespace in element names --- src/storm-dft/parser/DFTJsonParser.cpp | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp index 774f2cef8..7d4a64a64 100644 --- a/src/storm-dft/parser/DFTJsonParser.cpp +++ b/src/storm-dft/parser/DFTJsonParser.cpp @@ -75,9 +75,12 @@ namespace storm { json data = element.at("data"); std::string id = data.at("id"); // Append to id to distinguish elements with the same name + std::string name = data.at("name"); + std::replace(name.begin(), name.end(), ' ', '_'); std::stringstream stream; - stream << data.at("name").get() << "-" << id; - std::string name = stream.str(); + stream << name << "_" << data.at("id").get(); + name = stream.str(); + nameMapping[id] = name; } } @@ -90,9 +93,11 @@ namespace storm { continue; } json data = element.at("data"); + std::string name = data.at("name"); + std::replace(name.begin(), name.end(), ' ', '_'); std::stringstream stream; - stream << data.at("name").get() << "-" << data.at("id").get(); - std::string name = stream.str(); + stream << name << "_" << data.at("id").get(); + name = stream.str(); if (data.count("toplevel") > 0) { STORM_LOG_ASSERT(toplevelName.empty(), "Toplevel element already defined."); toplevelName = name; From 036d9c55d50f6f3a41cfe75147acd2ce3f8e30b7 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 8 Feb 2017 14:32:44 +0100 Subject: [PATCH 08/37] Small fixes --- .../builder/ExplicitDFTModelBuilderApprox.cpp | 4 ++++ src/storm-dft/modelchecker/dft/DFTModelChecker.cpp | 11 +++++------ src/storm-dft/parser/DFTJsonParser.cpp | 2 ++ 3 files changed, 11 insertions(+), 6 deletions(-) diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp index 48e564af0..9bb318cc1 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp @@ -563,6 +563,10 @@ namespace storm { if (storm::utility::isZero(rate)) { // Get active failure rate for cold BE rate = dft.getBasicElement(id)->activeFailureRate(); + if (storm::utility::isZero(rate)) { + // Ignore BE which cannot fail + continue; + } // Mark BE as cold coldBEs.set(i, true); } diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 8ca775432..fadd6d6fe 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -224,7 +224,6 @@ namespace storm { // Apply bisimulation bisimulationTimer.start(); composedModel = storm::performDeterministicSparseBisimulationMinimization>(composedModel, {formula}, storm::storage::BisimulationType::Weak)->template as>(); - std::chrono::high_resolution_clock::time_point bisimulationEnd = std::chrono::high_resolution_clock::now(); bisimulationTimer.stop(); STORM_LOG_INFO("No. states (Composed): " << composedModel->getNumberOfStates()); @@ -412,11 +411,11 @@ namespace storm { template void DFTModelChecker::printTimings(std::ostream& os) { os << "Times:" << std::endl; - os << "Exploration:\t" << explorationTimer.getTimeInSeconds() << "s" << std::endl; - os << "Building:\t" << buildingTimer.getTimeInSeconds() << "s" << std::endl; - os << "Bisimulation:\t" << bisimulationTimer.getTimeInSeconds() << "s" << std::endl; - os << "Modelchecking:\t" << modelCheckingTimer.getTimeInSeconds() << "s" << std::endl; - os << "Total:\t\t" << totalTimer.getTimeInSeconds() << "s" << std::endl; + os << "Exploration:\t" << explorationTimer.getTimeInMilliseconds() / 1000.0 << "s" << std::endl; + os << "Building:\t" << buildingTimer.getTimeInMilliseconds() / 1000.0 << "s" << std::endl; + os << "Bisimulation:\t" << bisimulationTimer.getTimeInMilliseconds() / 1000.0 << "s" << std::endl; + os << "Modelchecking:\t" << modelCheckingTimer.getTimeInMilliseconds() / 1000.0 << "s" << std::endl; + os << "Total:\t\t" << totalTimer.getTimeInMilliseconds() / 1000.0 << "s" << std::endl; } template diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp index 7d4a64a64..80ccdec45 100644 --- a/src/storm-dft/parser/DFTJsonParser.cpp +++ b/src/storm-dft/parser/DFTJsonParser.cpp @@ -77,6 +77,7 @@ namespace storm { // Append to id to distinguish elements with the same name std::string name = data.at("name"); std::replace(name.begin(), name.end(), ' ', '_'); + std::replace(name.begin(), name.end(), '-', '_'); std::stringstream stream; stream << name << "_" << data.at("id").get(); name = stream.str(); @@ -95,6 +96,7 @@ namespace storm { json data = element.at("data"); std::string name = data.at("name"); std::replace(name.begin(), name.end(), ' ', '_'); + std::replace(name.begin(), name.end(), '-', '_'); std::stringstream stream; stream << name << "_" << data.at("id").get(); name = stream.str(); From d1b86c8f355826176c94a34c9584e6f0e2ed6982 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 9 Feb 2017 00:24:35 +0100 Subject: [PATCH 09/37] Failed states are Markovian --- src/storm-dft/generator/DftNextStateGenerator.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index 3f1361f93..c89368099 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -52,10 +52,10 @@ namespace storm { bool hasDependencies = state->nrFailableDependencies() > 0; size_t failableCount = hasDependencies ? state->nrFailableDependencies() : state->nrFailableBEs(); size_t currentFailable = 0; - Choice choice(0, !hasDependencies); // Check for absorbing state if (mDft.hasFailed(state) || mDft.isFailsafe(state) || failableCount == 0) { + Choice choice(0, true); // Add self loop choice.addProbability(state->getId(), storm::utility::one()); STORM_LOG_TRACE("Added self loop for " << state->getId()); @@ -65,6 +65,8 @@ namespace storm { return result; } + Choice choice(0, !hasDependencies); + // Let BE fail while (currentFailable < failableCount) { STORM_LOG_ASSERT(!mDft.hasFailed(state), "Dft has failed."); From cd1bd6b538650bcf912b6fea196d03d7923c32f1 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 13 Feb 2017 15:05:05 +0100 Subject: [PATCH 10/37] Support for checking multiple dft properties at once --- src/storm-dft-cli/storm-dyftee.cpp | 86 +++-- .../modelchecker/dft/DFTModelChecker.cpp | 358 ++++++++++-------- .../modelchecker/dft/DFTModelChecker.h | 38 +- 3 files changed, 258 insertions(+), 224 deletions(-) diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp index 9a8cd033b..1dfe445e2 100644 --- a/src/storm-dft-cli/storm-dyftee.cpp +++ b/src/storm-dft-cli/storm-dyftee.cpp @@ -34,35 +34,44 @@ #include /*! - * Load DFT from filename, build corresponding Model and check against given property. + * Analyse the given DFT according to the given properties. + * We first load the DFT from the given file, then build the corresponding model and last check against the given properties. * - * @param property PCTC formula capturing the property to check. + * @param properties PCTL formulas capturing the properties to check. * @param symred Flag whether symmetry reduction should be used. * @param allowModularisation Flag whether modularisation should be applied if possible. * @param enableDC Flag whether Don't Care propagation should be used. + * @param approximationError Allowed approximation error. */ template -void analyzeDFT(std::string property, bool symred, bool allowModularisation, bool enableDC, double approximationError) { +void analyzeDFT(std::vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) { storm::settings::modules::DFTSettings const& dftSettings = storm::settings::getModule(); - std::shared_ptr> dft; + + // Build DFT from given file. if (dftSettings.isDftJsonFileSet()) { storm::parser::DFTJsonParser parser; - std::cout << "Running DFT analysis on file " << dftSettings.getDftJsonFilename() << " with property " << property << std::endl; + std::cout << "Loading DFT from file " << dftSettings.getDftJsonFilename() << std::endl; dft = std::make_shared>(parser.parseJson(dftSettings.getDftJsonFilename())); } else { storm::parser::DFTGalileoParser parser; - std::cout << "Running DFT analysis on file " << dftSettings.getDftFilename() << " with property " << property << std::endl; + std::cout << "Loading DFT from file " << dftSettings.getDftFilename() << std::endl; dft = std::make_shared>(parser.parseDFT(dftSettings.getDftFilename())); } - std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForExplicit(property)); - STORM_LOG_ASSERT(formulas.size() == 1, "Wrong number of formulas."); + // Build properties + std::string propString = properties[0]; + for (size_t i = 1; i < properties.size(); ++i) { + propString += ";" + properties[i]; + } + std::vector> props = storm::extractFormulasFromProperties(storm::parsePropertiesForExplicit(propString)); + STORM_LOG_ASSERT(props.size() > 0, "No properties found."); + // Check model storm::modelchecker::DFTModelChecker modelChecker; - modelChecker.check(*dft, formulas[0], symred, allowModularisation, enableDC, approximationError); + modelChecker.check(*dft, props, symred, allowModularisation, enableDC, approximationError); modelChecker.printTimings(); - modelChecker.printResult(); + modelChecker.printResults(); } /*! @@ -210,43 +219,42 @@ int main(const int argc, const char** argv) { #endif // Set min or max - bool minimal = true; + std::string optimizationDirection = "min"; if (dftSettings.isComputeMaximalValue()) { STORM_LOG_THROW(!dftSettings.isComputeMinimalValue(), storm::exceptions::InvalidSettingsException, "Cannot compute minimal and maximal values at the same time."); - minimal = false; + optimizationDirection = "max"; } - // Construct pctlFormula - std::string pctlFormula = ""; - std::string operatorType = ""; - std::string targetFormula = ""; + // Construct properties to check for + std::vector properties; if (generalSettings.isPropertySet()) { - STORM_LOG_THROW(!dftSettings.usePropExpectedTime() && !dftSettings.usePropProbability() && !dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given."); - pctlFormula = generalSettings.getProperty(); - } else if (dftSettings.usePropExpectedTime()) { - STORM_LOG_THROW(!dftSettings.usePropProbability() && !dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given."); - operatorType = "T"; - targetFormula = "F \"failed\""; - } else if (dftSettings.usePropProbability()) { - STORM_LOG_THROW(!dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given."); - operatorType = "P";; - targetFormula = "F \"failed\""; - } else { - STORM_LOG_THROW(dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "No property given."); + properties.push_back(generalSettings.getProperty()); + } + if (dftSettings.usePropExpectedTime()) { + properties.push_back("T" + optimizationDirection + "=? [F \"failed\"]"); + } + if (dftSettings.usePropProbability()) { + properties.push_back("P" + optimizationDirection + "=? [F \"failed\"]"); + } + if (dftSettings.usePropTimebound()) { std::stringstream stream; - stream << "F<=" << dftSettings.getPropTimebound() << " \"failed\""; - operatorType = "P"; - targetFormula = stream.str(); + stream << "P" << optimizationDirection << "=? [F<=" << dftSettings.getPropTimebound() << " \"failed\"]"; + properties.push_back(stream.str()); } - - if (!targetFormula.empty()) { - STORM_LOG_ASSERT(pctlFormula.empty(), "Pctl formula not empty."); - pctlFormula = operatorType + (minimal ? "min" : "max") + "=?[" + targetFormula + "]"; + if (dftSettings.usePropTimepoints()) { + for (double timepoint : dftSettings.getPropTimepoints()) { + std::stringstream stream; + stream << "P" << optimizationDirection << "=? [F<=" << timepoint << " \"failed\"]"; + properties.push_back(stream.str()); + } + } + + if (properties.empty()) { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No property given."); } - - STORM_LOG_ASSERT(!pctlFormula.empty(), "Pctl formula empty."); + // Set possible approximation error double approximationError = 0.0; if (dftSettings.isApproximationErrorSet()) { approximationError = dftSettings.getApproximationError(); @@ -255,12 +263,12 @@ int main(const int argc, const char** argv) { // From this point on we are ready to carry out the actual computations. if (parametric) { #ifdef STORM_HAVE_CARL - analyzeDFT(pctlFormula, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError); + analyzeDFT(properties, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError); #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameters are not supported in this build."); #endif } else { - analyzeDFT(pctlFormula, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError); + analyzeDFT(properties, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError); } // All operations have now been performed, so we clean up everything and terminate. diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index fadd6d6fe..362c49445 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -13,12 +13,7 @@ namespace storm { namespace modelchecker { template - DFTModelChecker::DFTModelChecker() { - checkResult = storm::utility::zero(); - } - - template - void DFTModelChecker::check(storm::storage::DFT const& origDft, std::shared_ptr const& formula, bool symred, bool allowModularisation, bool enableDC, double approximationError) { + void DFTModelChecker::check(storm::storage::DFT const& origDft, std::vector> const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) { // Initialize this->approximationError = approximationError; totalTimer.start(); @@ -29,31 +24,31 @@ namespace storm { // TODO Matthias: check that all paths reach the target state for approximation // Checking DFT - if (formula->isProbabilityOperatorFormula() || !allowModularisation) { - checkResult = checkHelper(dft, formula, symred, allowModularisation, enableDC, approximationError); - } else { - std::shared_ptr> model = buildModelComposition(dft, formula, symred, allowModularisation, enableDC); + if (properties[0]->isTimeOperatorFormula() && allowModularisation) { + // Use parallel composition as modularisation approach for expected time + std::shared_ptr> model = buildModelViaComposition(dft, properties, symred, true, enableDC, approximationError); // Model checking - std::unique_ptr result = checkModel(model, formula); - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); - checkResult = result->asExplicitQuantitativeCheckResult().getValueMap().begin()->second; + std::vector resultsValue = checkModel(model, properties); + for (ValueType result : resultsValue) { + checkResults.push_back(result); + } + } else { + checkResults = checkHelper(dft, properties, symred, allowModularisation, enableDC, approximationError); } totalTimer.stop(); } template - typename DFTModelChecker::dft_result DFTModelChecker::checkHelper(storm::storage::DFT const& dft, std::shared_ptr const& formula, bool symred, bool allowModularisation, bool enableDC, double approximationError) { + typename DFTModelChecker::dft_results DFTModelChecker::checkHelper(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) { STORM_LOG_TRACE("Check helper called"); - bool modularisationPossible = allowModularisation; + std::vector> dfts; + bool invResults = false; + size_t nrK = 0; // K out of M + size_t nrM = 0; // K out of M // Try modularisation - if(modularisationPossible) { - bool invResults = false; - std::vector> dfts; - size_t nrK = 0; // K out of M - size_t nrM = 0; // K out of M - + if(allowModularisation) { switch (dft.topLevelType()) { case storm::storage::DFTElementType::AND: STORM_LOG_TRACE("top modularisation called AND"); @@ -61,7 +56,6 @@ namespace storm { STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules."); nrK = dfts.size(); nrM = dfts.size(); - modularisationPossible = dfts.size() > 1; break; case storm::storage::DFTElementType::OR: STORM_LOG_TRACE("top modularisation called OR"); @@ -70,7 +64,6 @@ namespace storm { nrK = 0; nrM = dfts.size(); invResults = true; - modularisationPossible = dfts.size() > 1; break; case storm::storage::DFTElementType::VOT: STORM_LOG_TRACE("top modularisation called VOT"); @@ -82,22 +75,29 @@ namespace storm { nrK -= 1; invResults = true; } - modularisationPossible = dfts.size() > 1; break; default: // No static gate -> no modularisation applicable - modularisationPossible = false; break; } + } - if(modularisationPossible) { - STORM_LOG_TRACE("Recursive CHECK Call"); - if (formula->isProbabilityOperatorFormula()) { + // Perform modularisation + if(dfts.size() > 1) { + STORM_LOG_TRACE("Recursive CHECK Call"); + // TODO Matthias: compute simultaneously + dft_results results; + for (auto property : properties) { + if (!property->isProbabilityOperatorFormula()) { + STORM_LOG_WARN("Could not check property: " << *property); + } else { // Recursively call model checking std::vector res; for(auto const ft : dfts) { - dft_result ftResult = checkHelper(ft, formula, symred, true, enableDC, 0.0); - res.push_back(boost::get(ftResult)); + // TODO Matthias: allow approximation in modularisation + dft_results ftResults = checkHelper(ft, {property}, symred, true, enableDC, 0.0); + STORM_LOG_ASSERT(ftResults.size() == 1, "Wrong number of results"); + res.push_back(boost::get(ftResults[0])); } // Combine modularisation results @@ -128,148 +128,138 @@ namespace storm { if(invResults) { result = storm::utility::one() - result; } - return result; + results.push_back(result); } } + return results; + } else { + // No modularisation was possible + return checkDFT(dft, properties, symred, enableDC, approximationError); } - - // If we are here, no modularisation was possible - STORM_LOG_ASSERT(!modularisationPossible, "Modularisation should not be possible."); - return checkDFT(dft, formula, symred, enableDC, approximationError); } template - std::shared_ptr> DFTModelChecker::buildModelComposition(storm::storage::DFT const& dft, std::shared_ptr const& formula, bool symred, bool allowModularisation, bool enableDC) { + std::shared_ptr> DFTModelChecker::buildModelViaComposition(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) { + // TODO Matthias: use approximation? STORM_LOG_TRACE("Build model via composition"); - // Use parallel composition for CTMCs for expected time - STORM_LOG_ASSERT(formula->isTimeOperatorFormula(), "Formula is not a time operator formula"); - bool modularisationPossible = allowModularisation; + std::vector> dfts; + bool isAnd = true; // Try modularisation - if(modularisationPossible) { - std::vector> dfts; - bool isAnd = true; - + if(allowModularisation) { switch (dft.topLevelType()) { case storm::storage::DFTElementType::AND: STORM_LOG_TRACE("top modularisation called AND"); dfts = dft.topModularisation(); STORM_LOG_TRACE("Modularisation into " << dfts.size() << " submodules."); - modularisationPossible = dfts.size() > 1; isAnd = true; break; case storm::storage::DFTElementType::OR: STORM_LOG_TRACE("top modularisation called OR"); dfts = dft.topModularisation(); STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules."); - modularisationPossible = dfts.size() > 1; isAnd = false; break; case storm::storage::DFTElementType::VOT: - /*STORM_LOG_TRACE("top modularisation called VOT"); - dfts = dft.topModularisation(); - STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules."); - std::static_pointer_cast const>(dft.getTopLevelGate())->threshold(); - */ // TODO enable modularisation for voting gate - modularisationPossible = false; break; default: // No static gate -> no modularisation applicable - modularisationPossible = false; break; } + } - if(modularisationPossible) { - STORM_LOG_TRACE("Recursive CHECK Call"); - bool firstTime = true; - std::shared_ptr> composedModel; - for (auto const ft : dfts) { - STORM_LOG_INFO("Building Model via parallel composition..."); - explorationTimer.start(); + // Perform modularisation via parallel composition + if(dfts.size() > 1) { + STORM_LOG_TRACE("Recursive CHECK Call"); + bool firstTime = true; + std::shared_ptr> composedModel; + for (auto const ft : dfts) { + STORM_LOG_INFO("Building Model via parallel composition..."); + explorationTimer.start(); + + // Find symmetries + std::map>> emptySymmetry; + storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); + if(symred) { + auto colouring = ft.colourDFT(); + symmetries = ft.findSymmetries(colouring); + STORM_LOG_INFO("Found " << symmetries.groups.size() << " symmetries."); + STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries); + } - // Find symmetries - std::map>> emptySymmetry; - storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); - if(symred) { - auto colouring = ft.colourDFT(); - symmetries = ft.findSymmetries(colouring); - STORM_LOG_INFO("Found " << symmetries.groups.size() << " symmetries."); - STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries); - } + // Build a single CTMC + STORM_LOG_INFO("Building Model..."); + storm::builder::ExplicitDFTModelBuilderApprox builder(ft, symmetries, enableDC); + typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions; // TODO initialize this with the formula + builder.buildModel(labeloptions, 0, 0.0); + std::shared_ptr> model = builder.getModel(); + //model->printModelInformationToStream(std::cout); + STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates()); + STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions()); + explorationTimer.stop(); - // Build a single CTMC - STORM_LOG_INFO("Building Model..."); - storm::builder::ExplicitDFTModelBuilderApprox builder(ft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions; // TODO initialize this with the formula - builder.buildModel(labeloptions, 0, 0.0); - std::shared_ptr> model = builder.getModel(); - //model->printModelInformationToStream(std::cout); - STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates()); - STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions()); - explorationTimer.stop(); - - STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs"); - std::shared_ptr> ctmc = model->template as>(); - - ctmc = storm::performDeterministicSparseBisimulationMinimization>(ctmc, {formula}, storm::storage::BisimulationType::Weak)->template as>(); - - if (firstTime) { - composedModel = ctmc; - firstTime = false; - } else { - composedModel = storm::builder::ParallelCompositionBuilder::compose(composedModel, ctmc, isAnd); - } + STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs"); + std::shared_ptr> ctmc = model->template as>(); - // Apply bisimulation - bisimulationTimer.start(); - composedModel = storm::performDeterministicSparseBisimulationMinimization>(composedModel, {formula}, storm::storage::BisimulationType::Weak)->template as>(); - bisimulationTimer.stop(); - - STORM_LOG_INFO("No. states (Composed): " << composedModel->getNumberOfStates()); - STORM_LOG_INFO("No. transitions (Composed): " << composedModel->getNumberOfTransitions()); - if (composedModel->getNumberOfStates() <= 15) { - STORM_LOG_TRACE("Transition matrix: " << std::endl << composedModel->getTransitionMatrix()); - } else { - STORM_LOG_TRACE("Transition matrix: too big to print"); - } + // Apply bisimulation to new CTMC + bisimulationTimer.start(); + ctmc = storm::performDeterministicSparseBisimulationMinimization>(ctmc, properties, storm::storage::BisimulationType::Weak)->template as>(); + bisimulationTimer.stop(); + if (firstTime) { + composedModel = ctmc; + firstTime = false; + } else { + composedModel = storm::builder::ParallelCompositionBuilder::compose(composedModel, ctmc, isAnd); } - return composedModel; - } - } - // If we are here, no composition was possible - STORM_LOG_ASSERT(!modularisationPossible, "Modularisation should not be possible."); - explorationTimer.start(); - // Find symmetries - std::map>> emptySymmetry; - storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); - if(symred) { - auto colouring = dft.colourDFT(); - symmetries = dft.findSymmetries(colouring); - STORM_LOG_INFO("Found " << symmetries.groups.size() << " symmetries."); - STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries); - } - // Build a single CTMC - STORM_LOG_INFO("Building Model..."); + // Apply bisimulation to parallel composition + bisimulationTimer.start(); + composedModel = storm::performDeterministicSparseBisimulationMinimization>(composedModel, properties, storm::storage::BisimulationType::Weak)->template as>(); + bisimulationTimer.stop(); + + STORM_LOG_INFO("No. states (Composed): " << composedModel->getNumberOfStates()); + STORM_LOG_INFO("No. transitions (Composed): " << composedModel->getNumberOfTransitions()); + if (composedModel->getNumberOfStates() <= 15) { + STORM_LOG_TRACE("Transition matrix: " << std::endl << composedModel->getTransitionMatrix()); + } else { + STORM_LOG_TRACE("Transition matrix: too big to print"); + } + } + return composedModel; + } else { + // No composition was possible + explorationTimer.start(); + // Find symmetries + std::map>> emptySymmetry; + storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); + if(symred) { + auto colouring = dft.colourDFT(); + symmetries = dft.findSymmetries(colouring); + STORM_LOG_INFO("Found " << symmetries.groups.size() << " symmetries."); + STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries); + } + // Build a single CTMC + STORM_LOG_INFO("Building Model..."); - storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions; // TODO initialize this with the formula - builder.buildModel(labeloptions, 0, 0.0); - std::shared_ptr> model = builder.getModel(); - //model->printModelInformationToStream(std::cout); - STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates()); - STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions()); - explorationTimer.stop(); - STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs"); - return model->template as>(); + storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); + typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions; // TODO initialize this with the formula + builder.buildModel(labeloptions, 0, 0.0); + std::shared_ptr> model = builder.getModel(); + //model->printModelInformationToStream(std::cout); + STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates()); + STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions()); + explorationTimer.stop(); + STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs"); + return model->template as>(); + } } template - typename DFTModelChecker::dft_result DFTModelChecker::checkDFT(storm::storage::DFT const& dft, std::shared_ptr const& formula, bool symred, bool enableDC, double approximationError) { + typename DFTModelChecker::dft_results DFTModelChecker::checkDFT(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool enableDC, double approximationError) { explorationTimer.start(); // Find symmetries @@ -288,11 +278,18 @@ namespace storm { // Build approximate Markov Automata for lower and upper bound approximation_result approxResult = std::make_pair(storm::utility::zero(), storm::utility::zero()); std::shared_ptr> model; + std::vector newResult; storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions; // TODO initialize this with the formula - bool probabilityFormula = formula->isProbabilityOperatorFormula(); - STORM_LOG_ASSERT((formula->isTimeOperatorFormula() && !probabilityFormula) || (!formula->isTimeOperatorFormula() && probabilityFormula), "Probability formula not initialized correctly"); + // TODO Matthias: compute approximation for all properties simultaneously? + std::shared_ptr property = properties[0]; + if (properties.size() > 1) { + STORM_LOG_WARN("Computing approximation only for first property: " << *property); + } + + bool probabilityFormula = property->isProbabilityOperatorFormula(); + STORM_LOG_ASSERT((property->isTimeOperatorFormula() && !probabilityFormula) || (!property->isTimeOperatorFormula() && probabilityFormula), "Probability formula not initialized correctly"); size_t iteration = 0; do { // Iteratively build finer models @@ -315,12 +312,11 @@ namespace storm { STORM_LOG_INFO("No. transitions: " << model->getNumberOfTransitions()); buildingTimer.stop(); - // Check lower bound - std::unique_ptr result = checkModel(model, formula); - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); - ValueType newResult = result->asExplicitQuantitativeCheckResult().getValueMap().begin()->second; - STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(newResult, approxResult.first), "New under-approximation " << newResult << " is smaller than old result " << approxResult.first); - approxResult.first = newResult; + // Check lower bounds + newResult = checkModel(model, {property}); + STORM_LOG_ASSERT(newResult.size() == 1, "Wrong size for result vector."); + STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(newResult[0], approxResult.first), "New under-approximation " << newResult[0] << " is smaller than old result " << approxResult.first); + approxResult.first = newResult[0]; // Build model for upper bound STORM_LOG_INFO("Getting model for upper bound..."); @@ -328,11 +324,10 @@ namespace storm { model = builder.getModelApproximation(probabilityFormula ? true : false); buildingTimer.stop(); // Check upper bound - result = checkModel(model, formula); - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); - newResult = result->asExplicitQuantitativeCheckResult().getValueMap().begin()->second; - STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(approxResult.second, newResult), "New over-approximation " << newResult << " is greater than old result " << approxResult.second); - approxResult.second = newResult; + newResult = checkModel(model, {properties}); + STORM_LOG_ASSERT(newResult.size() == 1, "Wrong size for result vector."); + STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(approxResult.second, newResult[0]), "New over-approximation " << newResult[0] << " is greater than old result " << approxResult.second); + approxResult.second = newResult[0]; ++iteration; STORM_LOG_INFO("Result after iteration " << iteration << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")"); @@ -343,7 +338,9 @@ namespace storm { } while (!isApproximationSufficient(approxResult.first, approxResult.second, approximationError, probabilityFormula)); STORM_LOG_INFO("Finished approximation after " << iteration << " iteration" << (iteration > 1 ? "s." : ".")); - return approxResult; + dft_results results; + results.push_back(approxResult); + return results; } else { // Build a single Markov Automaton STORM_LOG_INFO("Building Model..."); @@ -365,32 +362,50 @@ namespace storm { explorationTimer.stop(); // Model checking - std::unique_ptr result = checkModel(model, formula); - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); - return result->asExplicitQuantitativeCheckResult().getValueMap().begin()->second; + std::vector resultsValue = checkModel(model, properties); + dft_results results; + for (ValueType result : resultsValue) { + results.push_back(result); + } + return results; } } template - std::unique_ptr DFTModelChecker::checkModel(std::shared_ptr>& model, std::shared_ptr const& formula) { + std::vector DFTModelChecker::checkModel(std::shared_ptr>& model, property_vector const& properties) { // Bisimulation - bisimulationTimer.start(); if (model->isOfType(storm::models::ModelType::Ctmc) && storm::settings::getModule().isBisimulationSet()) { + bisimulationTimer.start(); STORM_LOG_INFO("Bisimulation..."); - model = storm::performDeterministicSparseBisimulationMinimization>(model->template as>(), {formula}, storm::storage::BisimulationType::Weak)->template as>(); + model = storm::performDeterministicSparseBisimulationMinimization>(model->template as>(), properties, storm::storage::BisimulationType::Weak)->template as>(); STORM_LOG_INFO("No. states (Bisimulation): " << model->getNumberOfStates()); STORM_LOG_INFO("No. transitions (Bisimulation): " << model->getNumberOfTransitions()); + bisimulationTimer.stop(); } - bisimulationTimer.stop(); - modelCheckingTimer.start(); // Check the model STORM_LOG_INFO("Model checking..."); - std::unique_ptr result(storm::verifySparseModel(model, formula)); - STORM_LOG_INFO("Model checking done."); - STORM_LOG_ASSERT(result, "Result does not exist."); + modelCheckingTimer.start(); + std::vector results; + + // Check each property + storm::utility::Stopwatch singleModelCheckingTimer; + for (auto property : properties) { + singleModelCheckingTimer.reset(); + singleModelCheckingTimer.start(); + STORM_PRINT_AND_LOG("Model checking property " << *property << " ..." << std::endl); + std::unique_ptr result(storm::verifySparseModel(model, property, true)); + STORM_LOG_ASSERT(result, "Result does not exist."); + result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); + ValueType resultValue = result->asExplicitQuantitativeCheckResult().getValueMap().begin()->second; + STORM_PRINT_AND_LOG("Result (initial states): " << resultValue << std::endl); + results.push_back(resultValue); + singleModelCheckingTimer.stop(); + STORM_PRINT_AND_LOG("Time for model checking: " << singleModelCheckingTimer << "." << std::endl); + } modelCheckingTimer.stop(); - return result; + STORM_LOG_INFO("Model checking done."); + return results; } template @@ -411,21 +426,30 @@ namespace storm { template void DFTModelChecker::printTimings(std::ostream& os) { os << "Times:" << std::endl; - os << "Exploration:\t" << explorationTimer.getTimeInMilliseconds() / 1000.0 << "s" << std::endl; - os << "Building:\t" << buildingTimer.getTimeInMilliseconds() / 1000.0 << "s" << std::endl; - os << "Bisimulation:\t" << bisimulationTimer.getTimeInMilliseconds() / 1000.0 << "s" << std::endl; - os << "Modelchecking:\t" << modelCheckingTimer.getTimeInMilliseconds() / 1000.0 << "s" << std::endl; - os << "Total:\t\t" << totalTimer.getTimeInMilliseconds() / 1000.0 << "s" << std::endl; + os << "Exploration:\t" << explorationTimer << "s" << std::endl; + os << "Building:\t" << buildingTimer << "s" << std::endl; + os << "Bisimulation:\t" << bisimulationTimer<< "s" << std::endl; + os << "Modelchecking:\t" << modelCheckingTimer << "s" << std::endl; + os << "Total:\t\t" << totalTimer << "s" << std::endl; } template - void DFTModelChecker::printResult(std::ostream& os) { + void DFTModelChecker::printResults(std::ostream& os) { + bool first = true; os << "Result: ["; - if (this->approximationError > 0.0) { - approximation_result result = boost::get(checkResult); - os << "(" << result.first << ", " << result.second << ")"; - } else { - os << boost::get(checkResult); + for (auto result : checkResults) { + if (!first) { + os << ", "; + } + if (this->approximationError > 0.0) { + approximation_result resultApprox = boost::get(result); + os << "(" << resultApprox.first << ", " << resultApprox.second << ")"; + } else { + os << boost::get(result); + } + if (first) { + first = false; + } } os << "]" << std::endl; } diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.h b/src/storm-dft/modelchecker/dft/DFTModelChecker.h index c714999a8..6991ac888 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.h @@ -18,26 +18,28 @@ namespace storm { class DFTModelChecker { typedef std::pair approximation_result; - typedef boost::variant dft_result; + typedef std::vector> dft_results; + typedef std::vector> property_vector; public: /*! * Constructor. */ - DFTModelChecker(); + DFTModelChecker() { + } /*! * Main method for checking DFTs. * * @param origDft Original DFT - * @param formula Formula to check for + * @param properties Properties to check for * @param symred Flag indicating if symmetry reduction should be used * @param allowModularisation Flag indication if modularisation is allowed * @param enableDC Flag indicating if dont care propagation should be used * @param approximationError Error allowed for approximation. Value 0 indicates no approximation */ - void check(storm::storage::DFT const& origDft, std::shared_ptr const& formula, bool symred = true, bool allowModularisation = true, bool enableDC = true, double approximationError = 0.0); + void check(storm::storage::DFT const& origDft, property_vector const& properties, bool symred = true, bool allowModularisation = true, bool enableDC = true, double approximationError = 0.0); /*! * Print timings of all operations to stream. @@ -51,7 +53,7 @@ namespace storm { * * @param os Output stream to write to. */ - void printResult(std::ostream& os = std::cout); + void printResults(std::ostream& os = std::cout); private: @@ -62,8 +64,8 @@ namespace storm { storm::utility::Stopwatch modelCheckingTimer; storm::utility::Stopwatch totalTimer; - // Model checking result - dft_result checkResult; + // Model checking results + dft_results checkResults; // Allowed error bound for approximation double approximationError; @@ -72,21 +74,21 @@ namespace storm { * Internal helper for model checking a DFT. * * @param dft DFT - * @param formula Formula to check for + * @param properties Properties to check for * @param symred Flag indicating if symmetry reduction should be used * @param allowModularisation Flag indication if modularisation is allowed * @param enableDC Flag indicating if dont care propagation should be used * @param approximationError Error allowed for approximation. Value 0 indicates no approximation * - * @return Model checking result (or in case of approximation two results for lower and upper bound) + * @return Model checking results (or in case of approximation two results for lower and upper bound) */ - dft_result checkHelper(storm::storage::DFT const& dft, std::shared_ptr const& formula, bool symred, bool allowModularisation, bool enableDC, double approximationError); + dft_results checkHelper(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError); /*! * Internal helper for building a CTMC from a DFT via parallel composition. * * @param dft DFT - * @param formula Formula to check for + * @param properties Properties to check for * @param symred Flag indicating if symmetry reduction should be used * @param allowModularisation Flag indication if modularisation is allowed * @param enableDC Flag indicating if dont care propagation should be used @@ -94,30 +96,30 @@ namespace storm { * * @return CTMC representing the DFT */ - std::shared_ptr> buildModelComposition(storm::storage::DFT const& dft, std::shared_ptr const& formula, bool symred, bool allowModularisation, bool enableDC); + std::shared_ptr> buildModelViaComposition(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError); /*! * Check model generated from DFT. * * @param dft The DFT - * @param formula Formula to check for + * @param properties Properties to check for * @param symred Flag indicating if symmetry reduction should be used * @param enableDC Flag indicating if dont care propagation should be used * @param approximationError Error allowed for approximation. Value 0 indicates no approximation * * @return Model checking result */ - dft_result checkDFT(storm::storage::DFT const& dft, std::shared_ptr const& formula, bool symred, bool enableDC, double approximationError = 0.0); + dft_results checkDFT(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool enableDC, double approximationError = 0.0); /*! - * Check the given markov model for the given property. + * Check the given markov model for the given properties. * - * @param model Model to check - * @param formula Formula to check for + * @param model Model to check + * @param properties Properties to check for * * @return Model checking result */ - std::unique_ptr checkModel(std::shared_ptr>& model, std::shared_ptr const& formula); + std::vector checkModel(std::shared_ptr>& model, property_vector const& properties); /*! * Checks if the computed approximation is sufficient, i.e. From b178703a884709bd2aa8340f2ae143b750ee9f61 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 13 Feb 2017 15:33:39 +0100 Subject: [PATCH 11/37] Check for set of timepoints --- .../settings/modules/DFTSettings.cpp | 36 ++++++++++++------- src/storm-dft/settings/modules/DFTSettings.h | 33 ++++++++++++----- 2 files changed, 47 insertions(+), 22 deletions(-) diff --git a/src/storm-dft/settings/modules/DFTSettings.cpp b/src/storm-dft/settings/modules/DFTSettings.cpp index 8b62833a1..e20df83ec 100644 --- a/src/storm-dft/settings/modules/DFTSettings.cpp +++ b/src/storm-dft/settings/modules/DFTSettings.cpp @@ -29,7 +29,8 @@ namespace storm { const std::string DFTSettings::propExpectedTimeOptionName = "expectedtime"; const std::string DFTSettings::propExpectedTimeOptionShortName = "mttf"; const std::string DFTSettings::propProbabilityOptionName = "probability"; - const std::string DFTSettings::propTimeBoundOptionName = "timebound"; + const std::string DFTSettings::propTimeboundOptionName = "timebound"; + const std::string DFTSettings::propTimepointsOptionName = "timepoints"; const std::string DFTSettings::minValueOptionName = "min"; const std::string DFTSettings::maxValueOptionName = "max"; const std::string DFTSettings::transformToGspnOptionName = "gspn"; @@ -50,7 +51,8 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, approximationHeuristicOptionName, false, "Set the heuristic used for approximation.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "Sets which heuristic is used for approximation. Must be in {depth, probability}. Default is").setDefaultValueString("depth").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"depth", "rateratio"})).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, propExpectedTimeOptionName, false, "Compute expected time of system failure.").setShortName(propExpectedTimeOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, propProbabilityOptionName, false, "Compute probability of system failure.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, propTimeBoundOptionName, false, "Compute probability of system failure up to given timebound.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time", "The timebound to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, propTimeboundOptionName, false, "Compute probability of system failure up to given timebound.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time", "The timebound to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, propTimepointsOptionName, false, "Compute probability of system failure up to given timebound for a set of given timepoints [starttime, starttime+inc, starttime+2inc, ... ,endtime]").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("starttime", "The timebound to start from.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("endtime", "The timebound to end with.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("inc", "The value to increment with to get the next timepoint.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, minValueOptionName, false, "Compute minimal value in case of non-determinism.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, maxValueOptionName, false, "Compute maximal value in case of non-determinism.").build()); #ifdef STORM_HAVE_Z3 @@ -119,13 +121,28 @@ namespace storm { } bool DFTSettings::usePropTimebound() const { - return this->getOption(propTimeBoundOptionName).getHasOptionBeenSet(); + return this->getOption(propTimeboundOptionName).getHasOptionBeenSet(); } - + double DFTSettings::getPropTimebound() const { - return this->getOption(propTimeBoundOptionName).getArgumentByName("time").getValueAsDouble(); + return this->getOption(propTimeboundOptionName).getArgumentByName("time").getValueAsDouble(); } - + + bool DFTSettings::usePropTimepoints() const { + return this->getOption(propTimepointsOptionName).getHasOptionBeenSet(); + } + + std::vector DFTSettings::getPropTimepoints() const { + double starttime = this->getOption(propTimepointsOptionName).getArgumentByName("starttime").getValueAsDouble(); + double endtime = this->getOption(propTimepointsOptionName).getArgumentByName("endtime").getValueAsDouble(); + double inc = this->getOption(propTimepointsOptionName).getArgumentByName("inc").getValueAsDouble(); + std::vector timepoints; + for (double time = starttime; time <= endtime; time += inc) { + timepoints.push_back(time); + } + return timepoints; + } + bool DFTSettings::isComputeMinimalValue() const { return this->getOption(minValueOptionName).getHasOptionBeenSet(); } @@ -156,13 +173,6 @@ namespace storm { } bool DFTSettings::check() const { - // Ensure that only one property is given. - if (usePropExpectedTime()) { - STORM_LOG_THROW(!usePropProbability() && !usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given."); - } else if (usePropProbability()) { - STORM_LOG_THROW(!usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given."); - } - // Ensure that at most one of min or max is set STORM_LOG_THROW(!isComputeMinimalValue() || !isComputeMaximalValue(), storm::exceptions::InvalidSettingsException, "Min and max can not both be set."); return true; diff --git a/src/storm-dft/settings/modules/DFTSettings.h b/src/storm-dft/settings/modules/DFTSettings.h index 0d8695e2a..662039e0f 100644 --- a/src/storm-dft/settings/modules/DFTSettings.h +++ b/src/storm-dft/settings/modules/DFTSettings.h @@ -110,7 +110,28 @@ namespace storm { * @return True iff the option was set. */ bool usePropTimebound() const; - + + /*! + * Retrieves the timebound for the timebound property. + * + * @return The timebound. + */ + double getPropTimebound() const; + + /*! + * Retrieves whether the property timepoints should be used. + * + * @return True iff the option was set. + */ + bool usePropTimepoints() const; + + /*! + * Retrieves the settings for the timepoints property. + * + * @return The timepoints. + */ + std::vector getPropTimepoints() const; + /*! * Retrieves whether the minimal value should be computed for non-determinism. * @@ -124,13 +145,6 @@ namespace storm { * @return True iff the option was set. */ bool isComputeMaximalValue() const; - - /*! - * Retrieves the timebound for the timebound property. - * - * @return The timebound. - */ - double getPropTimebound() const; /*! * Retrieves whether the DFT should be transformed into a GSPN. @@ -184,7 +198,8 @@ namespace storm { static const std::string propExpectedTimeOptionName; static const std::string propExpectedTimeOptionShortName; static const std::string propProbabilityOptionName; - static const std::string propTimeBoundOptionName; + static const std::string propTimeboundOptionName; + static const std::string propTimepointsOptionName; static const std::string minValueOptionName; static const std::string maxValueOptionName; #ifdef STORM_HAVE_Z3 From 7d3fee88f8e2c062728bc13be28897a7a60843bf Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 13 Feb 2017 18:18:02 +0100 Subject: [PATCH 12/37] Use fail labels according to given properties --- .../builder/ExplicitDFTModelBuilderApprox.cpp | 50 ++++++++++++++----- .../builder/ExplicitDFTModelBuilderApprox.h | 14 ++++-- .../modelchecker/dft/DFTModelChecker.cpp | 10 ++-- .../modelchecker/dft/DFTModelChecker.h | 2 +- src/storm/models/sparse/StateLabeling.cpp | 17 +++++++ src/storm/models/sparse/StateLabeling.h | 11 +++- 6 files changed, 82 insertions(+), 22 deletions(-) diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp index 9bb318cc1..b6ed86c1e 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp @@ -9,7 +9,7 @@ #include "storm/utility/bitoperations.h" #include "storm/exceptions/UnexpectedException.h" #include "storm/settings/SettingsManager.h" - +#include "storm/logic/AtomicLabelFormula.h" #include "storm-dft/settings/modules/DFTSettings.h" @@ -27,6 +27,29 @@ namespace storm { builder = storm::storage::SparseMatrixBuilder(0, 0, 0, false, canHaveNondeterminism, 0); } + template + ExplicitDFTModelBuilderApprox::LabelOptions::LabelOptions(std::vector> properties) : buildFailLabel(true), buildFailSafeLabel(false) { + // Get necessary labels from properties + std::vector> atomicLabels; + for (auto property : properties) { + property->gatherAtomicLabelFormulas(atomicLabels); + } + // Set usage of necessary labels + for (auto atomic : atomicLabels) { + std::string label = atomic->getLabel(); + std::size_t foundIndex = label.find("_fail"); + if (foundIndex != std::string::npos) { + elementLabels.insert(label.substr(0, foundIndex)); + } else if (label.compare("failed") == 0) { + buildFailLabel = true; + } else if (label.compare("failsafe") == 0) { + buildFailSafeLabel = true; + } else { + STORM_LOG_WARN("Label '" << label << "' not known."); + } + } + } + template ExplicitDFTModelBuilderApprox::ExplicitDFTModelBuilderApprox(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) : dft(dft), @@ -415,16 +438,16 @@ namespace storm { modelComponents.stateLabeling.addLabel("failsafe"); } - // Collect labels for all BE - std::vector>> basicElements = dft.getBasicElements(); - for (std::shared_ptr> elem : basicElements) { - if(labelOpts.beLabels.count(elem->name()) > 0) { - modelComponents.stateLabeling.addLabel(elem->name() + "_fail"); + // Collect labels for all necessary elements + for (size_t id = 0; id < dft.nrElements(); ++id) { + std::shared_ptr const> element = dft.getElement(id); + if (labelOpts.elementLabels.count(element->name()) > 0) { + modelComponents.stateLabeling.addLabel(element->name() + "_fail"); } } // Set labels to states - if(mergeFailedStates) { + if (mergeFailedStates) { modelComponents.stateLabeling.addLabelToState("failed", failedStateId); } for (auto const& stateIdPair : stateStorage.stateToId) { @@ -435,14 +458,17 @@ namespace storm { } if (labelOpts.buildFailSafeLabel && dft.isFailsafe(state, *stateGenerationInfo)) { modelComponents.stateLabeling.addLabelToState("failsafe", stateId); - }; - // Set fail status for each BE - for (std::shared_ptr> elem : basicElements) { - if (labelOpts.beLabels.count(elem->name()) > 0 && storm::storage::DFTState::hasFailed(state, stateGenerationInfo->getStateIndex(elem->id())) ) { - modelComponents.stateLabeling.addLabelToState(elem->name() + "_fail", stateId); + } + // Set fail status for each necessary element + for (size_t id = 0; id < dft.nrElements(); ++id) { + std::shared_ptr const> element = dft.getElement(id); + if (labelOpts.elementLabels.count(element->name()) > 0 && storm::storage::DFTState::hasFailed(state, stateGenerationInfo->getStateIndex(element->id()))) { + modelComponents.stateLabeling.addLabelToState(element->name() + "_fail", stateId); } } } + + STORM_LOG_TRACE(modelComponents.stateLabeling); } template diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h index 6cf765d40..ce86fc759 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h +++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h @@ -153,9 +153,17 @@ namespace storm { public: // A structure holding the labeling options. struct LabelOptions { - bool buildFailLabel = true; - bool buildFailSafeLabel = false; - std::set beLabels = {}; + // Constructor + LabelOptions(std::vector> properties); + + // Flag indicating if the general fail label should be included. + bool buildFailLabel; + + // Flag indicating if the general failsafe label should be included. + bool buildFailSafeLabel; + + // Set of element names whose fail label to include. + std::set elementLabels; }; /*! diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 362c49445..805d54b6b 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -191,7 +191,7 @@ namespace storm { // Build a single CTMC STORM_LOG_INFO("Building Model..."); storm::builder::ExplicitDFTModelBuilderApprox builder(ft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions; // TODO initialize this with the formula + typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions(properties); builder.buildModel(labeloptions, 0, 0.0); std::shared_ptr> model = builder.getModel(); //model->printModelInformationToStream(std::cout); @@ -246,7 +246,7 @@ namespace storm { storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions; // TODO initialize this with the formula + typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions(properties); builder.buildModel(labeloptions, 0, 0.0); std::shared_ptr> model = builder.getModel(); //model->printModelInformationToStream(std::cout); @@ -280,7 +280,7 @@ namespace storm { std::shared_ptr> model; std::vector newResult; storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions; // TODO initialize this with the formula + typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions(properties); // TODO Matthias: compute approximation for all properties simultaneously? std::shared_ptr property = properties[0]; @@ -348,12 +348,12 @@ namespace storm { // TODO Matthias: use only one builder if everything works again if (storm::settings::getModule().isApproximationErrorSet()) { storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions; // TODO initialize this with the formula + typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions(properties); builder.buildModel(labeloptions, 0, 0.0); model = builder.getModel(); } else { storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions; // TODO initialize this with the formula + typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions; model = builder.buildModel(labeloptions); } //model->printModelInformationToStream(std::cout); diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.h b/src/storm-dft/modelchecker/dft/DFTModelChecker.h index 6991ac888..f67fe125e 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.h @@ -19,7 +19,7 @@ namespace storm { typedef std::pair approximation_result; typedef std::vector> dft_results; - typedef std::vector> property_vector; + typedef std::vector> property_vector; public: diff --git a/src/storm/models/sparse/StateLabeling.cpp b/src/storm/models/sparse/StateLabeling.cpp index 55eaa76d5..f3629829f 100644 --- a/src/storm/models/sparse/StateLabeling.cpp +++ b/src/storm/models/sparse/StateLabeling.cpp @@ -115,6 +115,23 @@ namespace storm { out << " * " << labelIndexPair.first << " -> " << this->labelings[labelIndexPair.second].getNumberOfSetBits() << " state(s)" << std::endl; } } + + void StateLabeling::printCompleteLabelingInformationToStream(std::ostream& out) const { + out << "Labels: \t" << this->getNumberOfLabels() << std::endl; + for (auto label : nameToLabelingIndexMap) { + out << "Label '" << label.first << "': "; + for (auto index : this->labelings[label.second]) { + out << index << " "; + } + out << std::endl; + } + } + + std::ostream& operator<<(std::ostream& out, StateLabeling const& labeling) { + labeling.printLabelingInformationToStream(out); + return out; + } + } } } diff --git a/src/storm/models/sparse/StateLabeling.h b/src/storm/models/sparse/StateLabeling.h index 330a4d8fe..f66ea86b4 100644 --- a/src/storm/models/sparse/StateLabeling.h +++ b/src/storm/models/sparse/StateLabeling.h @@ -152,7 +152,16 @@ namespace storm { * @param out The stream the information is to be printed to. */ void printLabelingInformationToStream(std::ostream& out) const; - + + /*! + * Prints the complete labeling to the specified stream. + * + * @param out The stream the information is to be printed to. + */ + void printCompleteLabelingInformationToStream(std::ostream& out) const; + + friend std::ostream& operator<<(std::ostream& out, StateLabeling const& labeling); + private: // The number of states for which this object can hold the labeling. uint_fast64_t stateCount; From a4777840699c03fdb2a9965e00f8d5d8da3d3045 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 13 Feb 2017 18:18:43 +0100 Subject: [PATCH 13/37] Small fix when computing upper bound in failed states --- src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp index b6ed86c1e..c21ce6ef7 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp @@ -572,6 +572,9 @@ namespace storm { template ValueType ExplicitDFTModelBuilderApprox::getUpperBound(DFTStatePointer const& state) const { + if (state->hasFailed(dft.getTopLevelIndex())) { + return storm::utility::zero(); + } // Get the upper bound by considering the failure of all BEs ValueType upperBound = storm::utility::one(); ValueType rateSum = storm::utility::zero(); From 831d86a2e0693bf4708a13fb2c3c22dad402ee2b Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 17 Feb 2017 19:58:01 +0100 Subject: [PATCH 14/37] Updated parser to read new JSON format --- src/storm-dft/parser/DFTJsonParser.cpp | 76 +++++++------------------- src/storm-dft/parser/DFTJsonParser.h | 4 +- 2 files changed, 22 insertions(+), 58 deletions(-) diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp index 80ccdec45..4c4dc0a3c 100644 --- a/src/storm-dft/parser/DFTJsonParser.cpp +++ b/src/storm-dft/parser/DFTJsonParser.cpp @@ -24,27 +24,11 @@ namespace storm { } template - std::string DFTJsonParser::stripQuotsFromName(std::string const& name) { - size_t firstQuots = name.find("\""); - size_t secondQuots = name.find("\"", firstQuots+1); - - if(firstQuots == std::string::npos) { - return name; - } else { - STORM_LOG_THROW(secondQuots != std::string::npos, storm::exceptions::FileIoException, "No ending quotation mark found in " << name); - return name.substr(firstQuots+1,secondQuots-1); - } - } - - template - std::string DFTJsonParser::getString(json const& structure, std::string const& errorInfo) { - STORM_LOG_THROW(structure.is_string(), storm::exceptions::FileIoException, "Expected a string in " << errorInfo << ", got '" << structure.dump() << "'"); - return structure.front(); - } - - template - std::string DFTJsonParser::parseNodeIdentifier(std::string const& name) { - return boost::replace_all_copy(name, "'", "__prime__"); + std::string DFTJsonParser::generateUniqueName(std::string const& id, std::string const& name) { + std::string newId = name; + std::replace(newId.begin(), newId.end(), ' ', '_'); + std::replace(newId.begin(), newId.end(), '-', '_'); + return newId + "_" + id; } template @@ -66,52 +50,33 @@ namespace storm { parsedJson << file; file.close(); - std::string toplevelName = ""; + storm::expressions::Variable var = manager->declareRationalVariable("x"); + identifierMapping.emplace(var.getName(), var); + parser.setIdentifierMapping(identifierMapping); + + json nodes = parsedJson.at("nodes"); - // Start by building mapping from ids to names + // Start by building mapping from ids to their unique names std::map nameMapping; - for (auto& element: parsedJson) { - if (element.at("classes") != "") { - json data = element.at("data"); - std::string id = data.at("id"); - // Append to id to distinguish elements with the same name - std::string name = data.at("name"); - std::replace(name.begin(), name.end(), ' ', '_'); - std::replace(name.begin(), name.end(), '-', '_'); - std::stringstream stream; - stream << name << "_" << data.at("id").get(); - name = stream.str(); - - nameMapping[id] = name; - } + for (auto& element: nodes) { + json data = element.at("data"); + std::string id = data.at("id"); + nameMapping[id] = generateUniqueName(id, data.at("name")); } - std::cout << toplevelName << std::endl; - for (auto& element : parsedJson) { + for (auto& element : nodes) { STORM_LOG_TRACE("Parsing: " << element); bool success = true; - if (element.at("classes") == "") { - continue; - } json data = element.at("data"); - std::string name = data.at("name"); - std::replace(name.begin(), name.end(), ' ', '_'); - std::replace(name.begin(), name.end(), '-', '_'); - std::stringstream stream; - stream << name << "_" << data.at("id").get(); - name = stream.str(); - if (data.count("toplevel") > 0) { - STORM_LOG_ASSERT(toplevelName.empty(), "Toplevel element already defined."); - toplevelName = name; - } + std::string name = generateUniqueName(data.at("id"), data.at("name")); std::vector childNames; if (data.count("children") > 0) { - for (json& child : data.at("children")) { - childNames.push_back(nameMapping[child.get()]); + for (std::string const& child : data.at("children")) { + childNames.push_back(nameMapping[child]); } } - std::string type = getString(element.at("classes"), "classes"); + std::string type = data.at("type"); if(type == "and") { success = builder.addAndElement(name, childNames); @@ -152,6 +117,7 @@ namespace storm { STORM_LOG_THROW(success, storm::exceptions::FileIoException, "Error while adding element '" << element << "'."); } + std::string toplevelName = nameMapping[parsedJson.at("toplevel")]; if(!builder.setTopLevel(toplevelName)) { STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Top level id unknown."); } diff --git a/src/storm-dft/parser/DFTJsonParser.h b/src/storm-dft/parser/DFTJsonParser.h index cf2e83826..d23baf58e 100644 --- a/src/storm-dft/parser/DFTJsonParser.h +++ b/src/storm-dft/parser/DFTJsonParser.h @@ -38,9 +38,7 @@ namespace storm { private: void readFile(std::string const& filename); - std::string stripQuotsFromName(std::string const& name); - std::string parseNodeIdentifier(std::string const& name); - std::string getString(json const& structure, std::string const& errorInfo); + std::string generateUniqueName(std::string const& id, std::string const& name); ValueType parseRationalExpression(std::string const& expr); }; From 40212bb7e6ad3de6e6c6dee4f28ca19dc988afd2 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 17 Feb 2017 20:22:44 +0100 Subject: [PATCH 15/37] Added possibility to avoid non-determinism by only taking the first dependency --- src/storm-dft/generator/DftNextStateGenerator.cpp | 6 ++++++ src/storm-dft/settings/modules/DFTSettings.cpp | 6 ++++++ src/storm-dft/settings/modules/DFTSettings.h | 8 ++++++++ 3 files changed, 20 insertions(+) diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index c89368099..9e9aa7056 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -3,6 +3,8 @@ #include "storm/utility/constants.h" #include "storm/utility/macros.h" #include "storm/exceptions/NotImplementedException.h" +#include "storm/settings/SettingsManager.h" +#include "storm-dft/settings/modules/DFTSettings.h" namespace storm { namespace generator { @@ -69,6 +71,10 @@ namespace storm { // Let BE fail while (currentFailable < failableCount) { + if (storm::settings::getModule().isTakeFirstDependency() && hasDependencies && currentFailable > 0) { + // We discard further exploration as we already chose one dependent event + break; + } STORM_LOG_ASSERT(!mDft.hasFailed(state), "Dft has failed."); // Construct new state as copy from original one diff --git a/src/storm-dft/settings/modules/DFTSettings.cpp b/src/storm-dft/settings/modules/DFTSettings.cpp index e20df83ec..1a8d59d70 100644 --- a/src/storm-dft/settings/modules/DFTSettings.cpp +++ b/src/storm-dft/settings/modules/DFTSettings.cpp @@ -33,6 +33,7 @@ namespace storm { const std::string DFTSettings::propTimepointsOptionName = "timepoints"; const std::string DFTSettings::minValueOptionName = "min"; const std::string DFTSettings::maxValueOptionName = "max"; + const std::string DFTSettings::firstDependencyOptionName = "firstdep"; const std::string DFTSettings::transformToGspnOptionName = "gspn"; const std::string DFTSettings::exportToJsonOptionName = "export-json"; #ifdef STORM_HAVE_Z3 @@ -47,6 +48,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, symmetryReductionOptionName, false, "Exploit symmetric structure of model.").setShortName(symmetryReductionOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, modularisationOptionName, false, "Use modularisation (not applicable for expected time).").build()); this->addOption(storm::settings::OptionBuilder(moduleName, disableDCOptionName, false, "Disable Dont Care propagation.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, firstDependencyOptionName, false, "Avoid non-determinism by always taking the first possible dependency.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, approximationErrorOptionName, false, "Approximation error allowed.").setShortName(approximationErrorOptionShortName).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("error", "The relative approximation error to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, approximationHeuristicOptionName, false, "Set the heuristic used for approximation.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "Sets which heuristic is used for approximation. Must be in {depth, probability}. Default is").setDefaultValueString("depth").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"depth", "rateratio"})).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, propExpectedTimeOptionName, false, "Compute expected time of system failure.").setShortName(propExpectedTimeOptionShortName).build()); @@ -151,6 +153,10 @@ namespace storm { return this->getOption(maxValueOptionName).getHasOptionBeenSet(); } + bool DFTSettings::isTakeFirstDependency() const { + return this->getOption(firstDependencyOptionName).getHasOptionBeenSet(); + } + #ifdef STORM_HAVE_Z3 bool DFTSettings::solveWithSMT() const { return this->getOption(solveWithSmtOptionName).getHasOptionBeenSet(); diff --git a/src/storm-dft/settings/modules/DFTSettings.h b/src/storm-dft/settings/modules/DFTSettings.h index 662039e0f..c04ef1a23 100644 --- a/src/storm-dft/settings/modules/DFTSettings.h +++ b/src/storm-dft/settings/modules/DFTSettings.h @@ -146,6 +146,13 @@ namespace storm { */ bool isComputeMaximalValue() const; + /*! + * Retrieves whether the non-determinism should be avoided by always taking the first possible dependency. + * + * @return True iff the option was set. + */ + bool isTakeFirstDependency() const; + /*! * Retrieves whether the DFT should be transformed into a GSPN. * @@ -202,6 +209,7 @@ namespace storm { static const std::string propTimepointsOptionName; static const std::string minValueOptionName; static const std::string maxValueOptionName; + static const std::string firstDependencyOptionName; #ifdef STORM_HAVE_Z3 static const std::string solveWithSmtOptionName; #endif From 21e16a9222ed87e5c1e67675e53d00e8a3f50739 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 22 Feb 2017 14:27:31 +0100 Subject: [PATCH 16/37] Assert that dependent events are BEs --- src/storm-dft/storage/dft/DFTBuilder.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/storm-dft/storage/dft/DFTBuilder.cpp b/src/storm-dft/storage/dft/DFTBuilder.cpp index db779e3d9..66beaa387 100644 --- a/src/storm-dft/storage/dft/DFTBuilder.cpp +++ b/src/storm-dft/storage/dft/DFTBuilder.cpp @@ -46,7 +46,7 @@ namespace storm { auto itFind = mElements.find(childName); STORM_LOG_ASSERT(itFind != mElements.end(), "Child not found."); DFTElementPointer childElement = itFind->second; - STORM_LOG_ASSERT(!childElement->isDependency() && !childElement->isRestriction(), "Child has invalid type."); + STORM_LOG_ASSERT(!childElement->isDependency() && !childElement->isRestriction(), "Child '" << childElement->name() << "' has invalid type."); elem.first->pushBackChild(childElement); childElement->addRestriction(elem.first); } @@ -60,6 +60,7 @@ namespace storm { STORM_LOG_ASSERT(itFind != mElements.end(), "Child '" << childName << "' not found"); DFTElementPointer childElement = itFind->second; if (!first) { + STORM_LOG_ASSERT(childElement->isBasicElement(), "Child '" << childName << "' of dependency '" << elem.first->name() << "' must be BE."); dependencies.push_back(std::static_pointer_cast>(childElement)); } else { elem.first->setTriggerElement(std::static_pointer_cast>(childElement)); From 1c2426b0f4656855c9d175de125510cf72502abe Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 24 Feb 2017 09:24:40 +0100 Subject: [PATCH 17/37] Print model information --- .../builder/ExplicitDFTModelBuilderApprox.cpp | 2 -- .../generator/DftNextStateGenerator.cpp | 2 +- .../modelchecker/dft/DFTModelChecker.cpp | 19 ++++++------------- src/storm/utility/storm.h | 8 ++++++++ 4 files changed, 15 insertions(+), 16 deletions(-) diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp index c21ce6ef7..d3e92fd1b 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp @@ -525,8 +525,6 @@ namespace storm { } } - STORM_LOG_DEBUG("No. states: " << model->getNumberOfStates()); - STORM_LOG_DEBUG("No. transitions: " << model->getNumberOfTransitions()); if (model->getNumberOfStates() <= 15) { STORM_LOG_TRACE("Transition matrix: " << std::endl << model->getTransitionMatrix()); } else { diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index 9e9aa7056..245a448ef 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -45,7 +45,7 @@ namespace storm { template StateBehavior DftNextStateGenerator::expand(StateToIdCallback const& stateToIdCallback) { - STORM_LOG_TRACE("Explore state: " << mDft.getStateString(state)); + STORM_LOG_DEBUG("Explore state: " << mDft.getStateString(state)); // Prepare the result, in case we return early. StateBehavior result; diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 805d54b6b..7f11d1caa 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -194,9 +194,6 @@ namespace storm { typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions(properties); builder.buildModel(labeloptions, 0, 0.0); std::shared_ptr> model = builder.getModel(); - //model->printModelInformationToStream(std::cout); - STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates()); - STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions()); explorationTimer.stop(); STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs"); @@ -219,8 +216,8 @@ namespace storm { composedModel = storm::performDeterministicSparseBisimulationMinimization>(composedModel, properties, storm::storage::BisimulationType::Weak)->template as>(); bisimulationTimer.stop(); - STORM_LOG_INFO("No. states (Composed): " << composedModel->getNumberOfStates()); - STORM_LOG_INFO("No. transitions (Composed): " << composedModel->getNumberOfTransitions()); + STORM_LOG_DEBUG("No. states (Composed): " << composedModel->getNumberOfStates()); + STORM_LOG_DEBUG("No. transitions (Composed): " << composedModel->getNumberOfTransitions()); if (composedModel->getNumberOfStates() <= 15) { STORM_LOG_TRACE("Transition matrix: " << std::endl << composedModel->getTransitionMatrix()); } else { @@ -228,6 +225,7 @@ namespace storm { } } + composedModel->printModelInformationToStream(std::cout); return composedModel; } else { // No composition was possible @@ -249,9 +247,7 @@ namespace storm { typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions(properties); builder.buildModel(labeloptions, 0, 0.0); std::shared_ptr> model = builder.getModel(); - //model->printModelInformationToStream(std::cout); - STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates()); - STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions()); + model->printModelInformationToStream(std::cout); explorationTimer.stop(); STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs"); return model->template as>(); @@ -308,8 +304,7 @@ namespace storm { STORM_LOG_INFO("Getting model for lower bound..."); model = builder.getModelApproximation(probabilityFormula ? false : true); // We only output the info from the lower bound as the info for the upper bound is the same - STORM_LOG_INFO("No. states: " << model->getNumberOfStates()); - STORM_LOG_INFO("No. transitions: " << model->getNumberOfTransitions()); + model->printModelInformationToStream(std::cout); buildingTimer.stop(); // Check lower bounds @@ -356,9 +351,7 @@ namespace storm { typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions; model = builder.buildModel(labeloptions); } - //model->printModelInformationToStream(std::cout); - STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates()); - STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions()); + model->printModelInformationToStream(std::cout); explorationTimer.stop(); // Model checking diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index 3aca0dbe2..ada4ea0d1 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -192,6 +192,10 @@ namespace storm { storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*model, options); bisimulationDecomposition.computeBisimulationDecomposition(); model = bisimulationDecomposition.getQuotient(); + + // Print some information about the model after the bisimulation + model->printModelInformationToStream(std::cout); + STORM_LOG_INFO("Bisimulation done. "); return model; } @@ -208,6 +212,10 @@ namespace storm { storm::storage::NondeterministicModelBisimulationDecomposition bisimulationDecomposition(*model, options); bisimulationDecomposition.computeBisimulationDecomposition(); model = bisimulationDecomposition.getQuotient(); + + // Print some information about the model after the bisimulation + model->printModelInformationToStream(std::cout); + STORM_LOG_INFO("Bisimulation done."); return model; } From d85a9499853fe679a868c04ce7f2837a6950036a Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 24 Feb 2017 09:25:05 +0100 Subject: [PATCH 18/37] Parse voting gate in JSON --- src/storm-dft/parser/DFTJsonParser.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp index 296b89f56..07454416f 100644 --- a/src/storm-dft/parser/DFTJsonParser.cpp +++ b/src/storm-dft/parser/DFTJsonParser.cpp @@ -74,6 +74,9 @@ namespace storm { success = builder.addAndElement(name, childNames); } else if (type == "or") { success = builder.addOrElement(name, childNames); + } else if (type == "vot") { + std::string votThreshold = data.at("voting"); + success = builder.addVotElement(name, boost::lexical_cast(votThreshold), childNames); } else if (type == "pand") { success = builder.addPandElement(name, childNames); } else if (type == "por") { From 97d09408d15e28c6a2adb2f631cf84f9a7cc4d02 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 27 Feb 2017 16:51:51 +0100 Subject: [PATCH 19/37] Export generated model from DFT --- .../modelchecker/dft/DFTModelChecker.cpp | 11 ++ src/storm/cli/entrypoints.h | 2 +- ...xporter.cpp => DirectEncodingExporter.cpp} | 129 +++++++++--------- ...citExporter.h => DirectEncodingExporter.h} | 10 +- 4 files changed, 81 insertions(+), 71 deletions(-) rename src/storm/utility/{ExplicitExporter.cpp => DirectEncodingExporter.cpp} (56%) rename src/storm/utility/{ExplicitExporter.h => DirectEncodingExporter.h} (59%) diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 7f11d1caa..8d655764e 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -2,6 +2,7 @@ #include "storm/builder/ParallelCompositionBuilder.h" #include "storm/utility/bitoperations.h" +#include "storm/utility/DirectEncodingExporter.h" #include "storm-dft/builder/ExplicitDFTModelBuilder.h" #include "storm-dft/builder/ExplicitDFTModelBuilderApprox.h" @@ -354,6 +355,16 @@ namespace storm { model->printModelInformationToStream(std::cout); explorationTimer.stop(); + // Export the model if required + if (storm::settings::getModule().isExportExplicitSet()) { + std::ofstream stream; + storm::utility::openFile(storm::settings::getModule().getExportExplicitFilename(), stream); + std::vector parameterNames; + // TODO fill parameter names + storm::exporter::explicitExportSparseModel(stream, model, parameterNames); + storm::utility::closeFile(stream); + } + // Model checking std::vector resultsValue = checkModel(model, properties); dft_results results; diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h index 8b968e756..a3883512f 100644 --- a/src/storm/cli/entrypoints.h +++ b/src/storm/cli/entrypoints.h @@ -6,7 +6,7 @@ #include "storm/utility/storm.h" #include "storm/storage/SymbolicModelDescription.h" -#include "storm/utility/ExplicitExporter.h" +#include "storm/utility/DirectEncodingExporter.h" #include "storm/utility/Stopwatch.h" #include "storm/exceptions/NotImplementedException.h" diff --git a/src/storm/utility/ExplicitExporter.cpp b/src/storm/utility/DirectEncodingExporter.cpp similarity index 56% rename from src/storm/utility/ExplicitExporter.cpp rename to src/storm/utility/DirectEncodingExporter.cpp index 1f40ab538..194ba7763 100644 --- a/src/storm/utility/ExplicitExporter.cpp +++ b/src/storm/utility/DirectEncodingExporter.cpp @@ -1,4 +1,4 @@ -#include "ExplicitExporter.h" +#include "DirectEncodingExporter.h" #include "storm/adapters/CarlAdapter.h" #include "storm/utility/constants.h" @@ -14,26 +14,24 @@ namespace storm { namespace exporter { + template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters) { - bool embedded = false; - if(sparseModel->getType() == storm::models::ModelType::Ctmc || sparseModel->getType() == storm::models::ModelType::MarkovAutomaton) { - STORM_LOG_WARN("This format only supports discrete time models"); - embedded = true; - } - - STORM_LOG_THROW(embedded || sparseModel->getType() == storm::models::ModelType::Mdp || sparseModel->getType() == storm::models::ModelType::Dtmc , storm::exceptions::NotImplementedException, "This functionality is not yet implemented." ); - + + // Notice that for CTMCs we write the rate matrix instead of probabilities + + // Initialize std::vector exitRates; // Only for CTMCs and MAs. if(sparseModel->getType() == storm::models::ModelType::Ctmc) { exitRates = sparseModel->template as>()->getExitRateVector(); } else if(sparseModel->getType() == storm::models::ModelType::MarkovAutomaton) { exitRates = sparseModel->template as>()->getExitRates(); } - + + // Write header os << "// Exported by storm" << std::endl; os << "// Original model type: " << sparseModel->getType() << std::endl; - os << "@type: mdp" << std::endl; + os << "@type: " << sparseModel->getType() << std::endl; os << "@parameters" << std::endl; for (auto const& p : parameters) { os << p << " "; @@ -41,98 +39,93 @@ namespace storm { os << std::endl; os << "@nr_states" << std::endl << sparseModel->getNumberOfStates() << std::endl; os << "@model" << std::endl; + storm::storage::SparseMatrix const& matrix = sparseModel->getTransitionMatrix(); for (typename storm::storage::SparseMatrix::index_type group = 0; group < matrix.getRowGroupCount(); ++group) { os << "state " << group; - - if (!embedded) { - bool first = true; - for (auto const& rewardModelEntry : sparseModel->getRewardModels()) { - if (first) { - os << " ["; - first = false; - } else { - os << ", "; - } - - if(rewardModelEntry.second.hasStateRewards()) { - os << rewardModelEntry.second.getStateRewardVector().at(group); - } else { - os << "0"; - } + + // Write state rewards + bool first = true; + for (auto const& rewardModelEntry : sparseModel->getRewardModels()) { + if (first) { + os << " ["; + first = false; + } else { + os << ", "; } - - if (!first) { - os << "]"; + + if(rewardModelEntry.second.hasStateRewards()) { + os << rewardModelEntry.second.getStateRewardVector().at(group); + } else { + os << "0"; } - } else { - // We currently only support the expected time. - os << " [" << storm::utility::one()/exitRates.at(group) << "]"; } - + + if (!first) { + os << "]"; + } + + // Write labels for(auto const& label : sparseModel->getStateLabeling().getLabelsOfState(group)) { os << " " << label; } os << std::endl; + + // Write probabilities typename storm::storage::SparseMatrix::index_type start = matrix.hasTrivialRowGrouping() ? group : matrix.getRowGroupIndices()[group]; typename storm::storage::SparseMatrix::index_type end = matrix.hasTrivialRowGrouping() ? group + 1 : matrix.getRowGroupIndices()[group + 1]; - - - for (typename storm::storage::SparseMatrix::index_type i = start; i < end; ++i) { + + // Iterate over all actions + for (typename storm::storage::SparseMatrix::index_type row = start; row < end; ++row) { // Print the actual row. - os << "\taction " << i - start; - if (!embedded) { - bool first = true; - for (auto const& rewardModelEntry : sparseModel->getRewardModels()) { - if (first) { - os << " ["; - first = false; - } else { - os << ", "; - } - - if(rewardModelEntry.second.hasStateActionRewards()) { - os << storm::utility::to_string(rewardModelEntry.second.getStateActionRewardVector().at(i)); - } else { - os << "0"; - } - + os << "\taction " << row - start; + bool first = true; + // Write transition rewards + for (auto const& rewardModelEntry : sparseModel->getRewardModels()) { + if (first) { + os << " ["; + first = false; + } else { + os << ", "; } - if (!first) { - os << "]"; + + if(rewardModelEntry.second.hasStateActionRewards()) { + os << storm::utility::to_string(rewardModelEntry.second.getStateActionRewardVector().at(row)); + } else { + os << "0"; } - } else { - // We currently only support the expected time. + + } + if (!first) { + os << "]"; } - - + // Write choice labeling if(sparseModel->hasChoiceLabeling()) { - //TODO + // TODO export choice labeling } os << std::endl; - - for(auto it = matrix.begin(i); it != matrix.end(i); ++it) { + // Write probabilities + for(auto it = matrix.begin(row); it != matrix.end(row); ++it) { ValueType prob = it->getValue(); - if(embedded) { - prob = prob / exitRates.at(group); - } os << "\t\t" << it->getColumn() << " : "; os << storm::utility::to_string(prob) << std::endl; } } - } + } // end matrix iteration } template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); - + +#ifdef STORM_HAVE_CARL template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); +#endif } } diff --git a/src/storm/utility/ExplicitExporter.h b/src/storm/utility/DirectEncodingExporter.h similarity index 59% rename from src/storm/utility/ExplicitExporter.h rename to src/storm/utility/DirectEncodingExporter.h index 964b1f10f..2ebee0092 100644 --- a/src/storm/utility/ExplicitExporter.h +++ b/src/storm/utility/DirectEncodingExporter.h @@ -6,10 +6,16 @@ namespace storm { namespace exporter { - + + /*! + * Exports a sparse model into the explicit DRN format. + * + * @param os Stream to export to + * @param sparseModel Model to export + * @param parameters List of parameters + */ template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); - } } From 36854d4636701af6becd5d22a1c92cc897dacc85 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 27 Feb 2017 17:54:36 +0100 Subject: [PATCH 20/37] Framework for DRN parser --- src/storm/cli/cli.cpp | 2 +- src/storm/cli/entrypoints.h | 9 ++- src/storm/parser/DirectEncodingParser.cpp | 72 +++++++++++++++++++++++ src/storm/parser/DirectEncodingParser.h | 33 +++++++++++ src/storm/settings/modules/IOSettings.cpp | 22 ++++++- src/storm/settings/modules/IOSettings.h | 16 +++++ src/storm/utility/storm.h | 6 ++ 7 files changed, 154 insertions(+), 6 deletions(-) create mode 100644 src/storm/parser/DirectEncodingParser.cpp create mode 100644 src/storm/parser/DirectEncodingParser.h diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index efdb54d42..a524de567 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -294,7 +294,7 @@ namespace storm { } else { buildAndCheckSymbolicModel(model, properties, true); } - } else if (ioSettings.isExplicitSet()) { + } else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet()) { STORM_LOG_THROW(coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Only the sparse engine supports explicit model input."); // If the model is given in an explicit format, we parse the properties without allowing expressions diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h index a3883512f..38ed1f551 100644 --- a/src/storm/cli/entrypoints.h +++ b/src/storm/cli/entrypoints.h @@ -385,10 +385,15 @@ namespace storm { void buildAndCheckExplicitModel(std::vector const& properties, bool onlyInitialStatesRelevant = false) { storm::settings::modules::IOSettings const& settings = storm::settings::getModule(); - STORM_LOG_THROW(settings.isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files."); + STORM_LOG_THROW(settings.isExplicitSet() || settings.isExplicitDRNSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files."); storm::utility::Stopwatch modelBuildingWatch(true); - std::shared_ptr model = buildExplicitModel(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? boost::optional(settings.getStateRewardsFilename()) : boost::none, settings.isTransitionRewardsSet() ? boost::optional(settings.getTransitionRewardsFilename()) : boost::none, settings.isChoiceLabelingSet() ? boost::optional(settings.getChoiceLabelingFilename()) : boost::none); + std::shared_ptr model; + if (settings.isExplicitSet()) { + model = buildExplicitModel(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? boost::optional(settings.getStateRewardsFilename()) : boost::none, settings.isTransitionRewardsSet() ? boost::optional(settings.getTransitionRewardsFilename()) : boost::none, settings.isChoiceLabelingSet() ? boost::optional(settings.getChoiceLabelingFilename()) : boost::none); + } else { + model = buildExplicitDRNModel(settings.getExplicitDRNFilename()); + } modelBuildingWatch.stop(); STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl); diff --git a/src/storm/parser/DirectEncodingParser.cpp b/src/storm/parser/DirectEncodingParser.cpp new file mode 100644 index 000000000..d343e4b6c --- /dev/null +++ b/src/storm/parser/DirectEncodingParser.cpp @@ -0,0 +1,72 @@ +#include "storm/parser/DirectEncodingParser.h" + +#include +#include +#include +#include +#include +#include + +#include "storm/exceptions/FileIoException.h" +#include "storm/exceptions/WrongFormatException.h" +#include "storm/exceptions/InvalidArgumentException.h" +#include "storm/settings/SettingsManager.h" + +#include "storm/adapters/CarlAdapter.h" +#include "storm/utility/macros.h" +#include "storm/utility/file.h" + +namespace storm { + namespace parser { + + template + std::shared_ptr> DirectEncodingParser::parseModel(std::string const& filename) { + + // Load file + STORM_LOG_INFO("Reading from file " << filename); + std::ifstream file; + storm::utility::openFile(filename, file); + std::string line; + + // Initialize + storm::models::ModelType type; + + // Iterate over all lines + while (std::getline(file, line)) { + STORM_LOG_TRACE("Parsing: " << line); + } + + // Done parsing + storm::utility::closeFile(file); + + + // Build model + switch (type) { + case storm::models::ModelType::Dtmc: + { + STORM_LOG_THROW(false, storm::exceptions::FileIoException, "DTMC not supported."); + } + case storm::models::ModelType::Ctmc: + { + STORM_LOG_THROW(false, storm::exceptions::FileIoException, "CTMC not supported."); + } + case storm::models::ModelType::Mdp: + { + STORM_LOG_THROW(false, storm::exceptions::FileIoException, "MDP not supported."); + } + case storm::models::ModelType::MarkovAutomaton: + { + STORM_LOG_THROW(false, storm::exceptions::FileIoException, "MA not supported."); + } + default: + STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Unknown/Unhandled model type " << type << " which cannot be parsed."); + } + } + + template class DirectEncodingParser; + +#ifdef STORM_HAVE_CARL + template class DirectEncodingParser; +#endif + } // namespace parser +} // namespace storm diff --git a/src/storm/parser/DirectEncodingParser.h b/src/storm/parser/DirectEncodingParser.h new file mode 100644 index 000000000..536f1b209 --- /dev/null +++ b/src/storm/parser/DirectEncodingParser.h @@ -0,0 +1,33 @@ +#ifndef STORM_PARSER_DIRECTENCODINGPARSER_H_ +#define STORM_PARSER_DIRECTENCODINGPARSER_H_ + +#include "storm/models/sparse/Model.h" + + +namespace storm { + namespace parser { + + /*! + * Parser for models in the DRN format with explicit encoding. + */ + template> + class DirectEncodingParser { + public: + + /*! + * Load a model in DRN format from a file and create the model. + * + * @param file The DRN file to be parsed. + * + * @return A sparse model + */ + static std::shared_ptr> parseModel(std::string const& file); + + private: + + }; + + } // namespace parser +} // namespace storm + +#endif /* STORM_PARSER_DIRECTENCODINGPARSER_H_ */ diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp index 9f07c0219..1ade861dd 100644 --- a/src/storm/settings/modules/IOSettings.cpp +++ b/src/storm/settings/modules/IOSettings.cpp @@ -21,6 +21,8 @@ namespace storm { const std::string IOSettings::exportExplicitOptionName = "exportexplicit"; const std::string IOSettings::explicitOptionName = "explicit"; const std::string IOSettings::explicitOptionShortName = "exp"; + const std::string IOSettings::explicitDrnOptionName = "explicit-drn"; + const std::string IOSettings::explicitDrnOptionShortName = "drn"; const std::string IOSettings::prismInputOptionName = "prism"; const std::string IOSettings::janiInputOptionName = "jani"; const std::string IOSettings::prismToJaniOptionName = "prism2jani"; @@ -53,6 +55,9 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, explicitOptionName, false, "Parses the model given in an explicit (sparse) representation.").setShortName(explicitOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("transition filename", "The name of the file from which to read the transitions.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("labeling filename", "The name of the file from which to read the state labeling.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, explicitDrnOptionName, false, "Parses the model given in the DRN format.").setShortName(explicitDrnOptionShortName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("drn filename", "The name of the DRN file containing the model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()) + .build()); this->addOption(storm::settings::OptionBuilder(moduleName, prismInputOptionName, false, "Parses the model given in the PRISM format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the PRISM input.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, janiInputOptionName, false, "Parses the model given in the JANI format.") @@ -109,7 +114,15 @@ namespace storm { std::string IOSettings::getLabelingFilename() const { return this->getOption(explicitOptionName).getArgumentByName("labeling filename").getValueAsString(); } - + + bool IOSettings::isExplicitDRNSet() const { + return this->getOption(explicitDrnOptionName).getHasOptionBeenSet(); + } + + std::string IOSettings::getExplicitDRNFilename() const { + return this->getOption(explicitDrnOptionName).getArgumentByName("drn filename").getValueAsString(); + } + bool IOSettings::isPrismInputSet() const { return this->getOption(prismInputOptionName).getHasOptionBeenSet(); } @@ -230,9 +243,12 @@ namespace storm { bool IOSettings::check() const { // Ensure that not two symbolic input models were given. STORM_LOG_THROW(!isJaniInputSet() || !isPrismInputSet(), storm::exceptions::InvalidSettingsException, "Symbolic model "); - + + // Ensure that not two explicit input models were given. + STORM_LOG_THROW(!isExplicitSet() || !isExplicitDRNSet(), storm::exceptions::InvalidSettingsException, "Explicit model "); + // Ensure that the model was given either symbolically or explicitly. - STORM_LOG_THROW(!isJaniInputSet() || !isPrismInputSet() || !isExplicitSet(), storm::exceptions::InvalidSettingsException, "The model may be either given in an explicit or a symbolic format (PRISM or JANI), but not both."); + STORM_LOG_THROW(!isJaniInputSet() || !isPrismInputSet() || !isExplicitSet() || !isExplicitDRNSet(), storm::exceptions::InvalidSettingsException, "The model may be either given in an explicit or a symbolic format (PRISM or JANI), but not both."); // Make sure PRISM-to-JANI conversion is only set if the actual input is in PRISM format. STORM_LOG_THROW(!isPrismToJaniSet() || isPrismInputSet(), storm::exceptions::InvalidSettingsException, "For the transformation from PRISM to JANI, the input model must be given in the prism format."); diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h index 711ec2d97..0e329b840 100644 --- a/src/storm/settings/modules/IOSettings.h +++ b/src/storm/settings/modules/IOSettings.h @@ -72,6 +72,20 @@ namespace storm { */ std::string getLabelingFilename() const; + /*! + * Retrieves whether the explicit option with DRN was set. + * + * @return True if the explicit option with DRN was set. + */ + bool isExplicitDRNSet() const; + + /*! + * Retrieves the name of the file that contains the model in the DRN format. + * + * @return The name of the DRN file that contains the model. + */ + std::string getExplicitDRNFilename() const; + /*! * Retrieves whether the PRISM language option was set. * @@ -275,6 +289,8 @@ namespace storm { static const std::string exportExplicitOptionName; static const std::string explicitOptionName; static const std::string explicitOptionShortName; + static const std::string explicitDrnOptionName; + static const std::string explicitDrnOptionShortName; static const std::string prismInputOptionName; static const std::string janiInputOptionName; static const std::string prismToJaniOptionName; diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index ada4ea0d1..75c52d80d 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -41,6 +41,7 @@ #include "storm/storage/dd/Bdd.h" #include "storm/parser/AutoParser.h" +#include "storm/parser/DirectEncodingParser.h" #include "storm/storage/jani/Model.h" #include "storm/storage/jani/Property.h" @@ -110,6 +111,11 @@ namespace storm { return storm::parser::AutoParser<>::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "", choiceLabelingFile ? choiceLabelingFile.get() : "" ); } + template + std::shared_ptr> buildExplicitDRNModel(std::string const& drnFile) { + return storm::parser::DirectEncodingParser::parseModel(drnFile); + } + std::vector> extractFormulasFromProperties(std::vector const& properties); std::pair> parseJaniModel(std::string const& path); storm::prism::Program parseProgram(std::string const& path); From 069908d7c99e8f6a25cc5b8e7286872cbba38303 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 28 Feb 2017 22:36:29 +0100 Subject: [PATCH 21/37] Working on DNR parser --- src/storm/models/ModelType.cpp | 42 +++++- src/storm/models/ModelType.h | 2 + src/storm/parser/DirectEncodingParser.cpp | 169 ++++++++++++++++++++-- src/storm/parser/DirectEncodingParser.h | 76 ++++++++++ 4 files changed, 273 insertions(+), 16 deletions(-) diff --git a/src/storm/models/ModelType.cpp b/src/storm/models/ModelType.cpp index 5bb1a9b09..46bc06dc9 100644 --- a/src/storm/models/ModelType.cpp +++ b/src/storm/models/ModelType.cpp @@ -1,14 +1,46 @@ #include "storm/models/ModelType.h" +#include "storm/exceptions/InvalidTypeException.h" +#include "storm/utility/macros.h" + namespace storm { namespace models { + + ModelType getModelType(std::string const& type) { + if (type == "DTMC") { + return ModelType::Dtmc; + } else if (type == "CTMC") { + return ModelType::Ctmc; + }else if (type == "MDP") { + return ModelType::Mdp; + } else if (type == "Markov Automaton") { + return ModelType::MarkovAutomaton; + } else if (type == "S2PG") { + return ModelType::S2pg; + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Type " << type << "not known."); + } + } + std::ostream& operator<<(std::ostream& os, ModelType const& type) { switch (type) { - case ModelType::Dtmc: os << "DTMC"; break; - case ModelType::Ctmc: os << "CTMC"; break; - case ModelType::Mdp: os << "MDP"; break; - case ModelType::MarkovAutomaton: os << "Markov Automaton"; break; - case ModelType::S2pg: os << "S2PG"; break; + case ModelType::Dtmc: + os << "DTMC"; + break; + case ModelType::Ctmc: + os << "CTMC"; + break; + case ModelType::Mdp: + os << "MDP"; + break; + case ModelType::MarkovAutomaton: + os << "Markov Automaton"; + break; + case ModelType::S2pg: + os << "S2PG"; + break; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unknown model type."); } return os; } diff --git a/src/storm/models/ModelType.h b/src/storm/models/ModelType.h index 6fabee8a4..40d4da220 100644 --- a/src/storm/models/ModelType.h +++ b/src/storm/models/ModelType.h @@ -9,6 +9,8 @@ namespace storm { enum class ModelType { Dtmc, Ctmc, Mdp, MarkovAutomaton, S2pg }; + + ModelType getModelType(std::string const& type); std::ostream& operator<<(std::ostream& os, ModelType const& type); } diff --git a/src/storm/parser/DirectEncodingParser.cpp b/src/storm/parser/DirectEncodingParser.cpp index d343e4b6c..1be94ca4c 100644 --- a/src/storm/parser/DirectEncodingParser.cpp +++ b/src/storm/parser/DirectEncodingParser.cpp @@ -1,24 +1,51 @@ #include "storm/parser/DirectEncodingParser.h" -#include -#include -#include -#include #include #include +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/models/sparse/Ctmc.h" + #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/InvalidArgumentException.h" +#include "storm/exceptions/NotSupportedException.h" #include "storm/settings/SettingsManager.h" #include "storm/adapters/CarlAdapter.h" +#include "storm/utility/constants.h" #include "storm/utility/macros.h" #include "storm/utility/file.h" namespace storm { namespace parser { + template<> + void ValueParser::addParameter(std::string const& parameter) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameters are not supported in this build."); + } + + template<> + void ValueParser::addParameter(std::string const& parameter) { + //STORM_LOG_THROW((std::is_same::value), storm::exceptions::NotSupportedException, "Parameters only allowed when using rational functions."); + storm::expressions::Variable var = manager->declareRationalVariable(parameter); + identifierMapping.emplace(var.getName(), var); + parser.setIdentifierMapping(identifierMapping); + STORM_LOG_TRACE("Added parameter: " << var.getName()); + } + + template<> + double ValueParser::parseValue(std::string const& value) const { + return boost::lexical_cast(value); + } + + template<> + storm::RationalFunction ValueParser::parseValue(std::string const& value) const { + storm::RationalFunction rationalFunction = evaluator.asRational(parser.parseFromString(value)); + STORM_LOG_TRACE("Parsed expression: " << rationalFunction); + return rationalFunction; + } + template std::shared_ptr> DirectEncodingParser::parseModel(std::string const& filename) { @@ -29,17 +56,47 @@ namespace storm { std::string line; // Initialize - storm::models::ModelType type; + ValueParser valueParser; - // Iterate over all lines - while (std::getline(file, line)) { - STORM_LOG_TRACE("Parsing: " << line); + // Parse header + std::getline(file, line); + STORM_LOG_THROW(line == "// Exported by storm", storm::exceptions::WrongFormatException, "Expected header information."); + std::getline(file, line); + STORM_LOG_THROW(boost::starts_with(line, "// Original model type: "), storm::exceptions::WrongFormatException, "Expected header information."); + // Parse model type + std::getline(file, line); + STORM_LOG_THROW(boost::starts_with(line, "@type: "), storm::exceptions::WrongFormatException, "Expected model type."); + storm::models::ModelType type = storm::models::getModelType(line.substr(7)); + STORM_LOG_TRACE("Model type: " << type); + // Parse parameters + std::getline(file, line); + STORM_LOG_THROW(line == "@parameters", storm::exceptions::WrongFormatException, "Expected parameter declaration."); + std::getline(file, line); + if (line != "") { + std::vector parameters; + boost::split(parameters, line, boost::is_any_of(" ")); + for (std::string parameter : parameters) { + STORM_LOG_TRACE("New parameter: " << parameter); + valueParser.addParameter(parameter); + } } + // Parse no. states + std::getline(file, line); + STORM_LOG_THROW(line == "@nr_states", storm::exceptions::WrongFormatException, "Expected number of states."); + std::getline(file, line); + size_t nrStates = boost::lexical_cast(line); + STORM_LOG_TRACE("Model type: " << type); + + std::getline(file, line); + STORM_LOG_THROW(line == "@model", storm::exceptions::WrongFormatException, "Expected model declaration."); + + // Construct transition matrix + std::shared_ptr modelComponents = parseStates(file, type, nrStates, valueParser); + // Done parsing storm::utility::closeFile(file); - // Build model switch (type) { case storm::models::ModelType::Dtmc: @@ -48,7 +105,7 @@ namespace storm { } case storm::models::ModelType::Ctmc: { - STORM_LOG_THROW(false, storm::exceptions::FileIoException, "CTMC not supported."); + return std::make_shared>(std::move(modelComponents->transitionMatrix), std::move(modelComponents->stateLabeling), std::move(modelComponents->rewardModels), std::move(modelComponents->choiceLabeling)); } case storm::models::ModelType::Mdp: { @@ -56,13 +113,103 @@ namespace storm { } case storm::models::ModelType::MarkovAutomaton: { - STORM_LOG_THROW(false, storm::exceptions::FileIoException, "MA not supported."); + return std::make_shared>(std::move(modelComponents->transitionMatrix), std::move(modelComponents->stateLabeling), std::move(modelComponents->markovianStates), std::move(modelComponents->exitRates)); } default: STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Unknown/Unhandled model type " << type << " which cannot be parsed."); } } + template + std::shared_ptr::ModelComponents> DirectEncodingParser::parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, ValueParser const& valueParser) { + // Initialize + std::shared_ptr modelComponents = std::make_shared(); + modelComponents->nonDeterministic = (type == storm::models::ModelType::Mdp || type == storm::models::ModelType::MarkovAutomaton); + storm::storage::SparseMatrixBuilder builder = storm::storage::SparseMatrixBuilder(0, 0, 0, false, modelComponents->nonDeterministic, 0); + + // Iterate over all lines + std::string line; + size_t row = 0; + size_t state = 0; + bool first = true; + while (std::getline(file, line)) { + STORM_LOG_TRACE("Parsing: " << line); + if (boost::starts_with(line, "state ")) { + // New state + line = line.substr(6); + size_t parsedId; + size_t posId = line.find(" "); + if (posId != std::string::npos) { + parsedId = boost::lexical_cast(line.substr(0, posId)); + + // Parse rewards and labels + line = line.substr(posId+1); + // Check for rewards + if (boost::starts_with(line, "[")) { + // Rewards found + size_t posEndReward = line.find(']'); + STORM_LOG_THROW(posEndReward != std::string::npos, storm::exceptions::WrongFormatException, "] missing."); + std::string rewards = line.substr(1, posEndReward-1); + STORM_LOG_TRACE("State rewards: " << rewards); + // TODO save rewards + line = line.substr(posEndReward+1); + } + // Check for labels + std::vector labels; + boost::split(labels, line, boost::is_any_of(" ")); + if (!labels.empty()) { + STORM_LOG_TRACE("Labels: " << labels); + } + } else { + // Only state id given + parsedId = boost::lexical_cast(line); + } + STORM_LOG_TRACE("New state " << state << " " << parsedId); + STORM_LOG_ASSERT(state == parsedId, "State ids do not correspond."); + if (modelComponents->nonDeterministic) { + builder.newRowGroup(row); + } + ++state; + } else if (boost::starts_with(line, "\taction ")) { + // New action + line = line.substr(8); + STORM_LOG_TRACE("New action: " << row); + // Check for rewards + if (boost::starts_with(line, "[")) { + // Rewards found + size_t posEndReward = line.find(']'); + STORM_LOG_THROW(posEndReward != std::string::npos, storm::exceptions::WrongFormatException, "] missing."); + std::string rewards = line.substr(1, posEndReward-1); + STORM_LOG_TRACE("Transition rewards: " << rewards); + // TODO save rewards + line = line.substr(posEndReward+1); + } + // TODO import choice labeling when the export works + + if (first) { + first = false; + } else { + ++row; + } + } else { + // New transition + size_t posColon = line.find(":"); + STORM_LOG_ASSERT(posColon != std::string::npos, "':' not found."); + size_t target = boost::lexical_cast(line.substr(2, posColon-3)); + std::string valueStr = line.substr(posColon+2); + ValueType value = valueParser.parseValue(valueStr); + STORM_LOG_TRACE("Transition " << state << " -> " << target << ": " << value); + builder.addNextValue(state, target, value); + } + } + + STORM_LOG_TRACE("Finished parsing"); + modelComponents->transitionMatrix = builder.build(stateSize, stateSize); + STORM_LOG_TRACE("Built matrix"); + return modelComponents; + } + + // Template instantiations. template class DirectEncodingParser; #ifdef STORM_HAVE_CARL diff --git a/src/storm/parser/DirectEncodingParser.h b/src/storm/parser/DirectEncodingParser.h index 536f1b209..1bbbf6a37 100644 --- a/src/storm/parser/DirectEncodingParser.h +++ b/src/storm/parser/DirectEncodingParser.h @@ -2,11 +2,52 @@ #define STORM_PARSER_DIRECTENCODINGPARSER_H_ #include "storm/models/sparse/Model.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/storage/expressions/ExpressionManager.h" +#include "storm/parser/ExpressionParser.h" +#include "storm/storage/expressions/ExpressionEvaluator.h" namespace storm { namespace parser { + /*! + * Parser for values according to their ValueType. + */ + template + class ValueParser { + public: + + ValueParser() : manager(new storm::expressions::ExpressionManager()), parser(*manager), evaluator(*manager) { + } + + /*! + * Parse ValueType from string. + * + * @param value String containing the value. + * + * @return ValueType + */ + ValueType parseValue(std::string const& value) const; + + /*! + * Add declaration of parameter. + * + * @param parameter New parameter. + */ + void addParameter(std::string const& parameter); + + private: + + std::shared_ptr manager; + + storm::parser::ExpressionParser parser; + + storm::expressions::ExpressionEvaluator evaluator; + + std::unordered_map identifierMapping; + }; + /*! * Parser for models in the DRN format with explicit encoding. */ @@ -25,6 +66,41 @@ namespace storm { private: + // A structure holding the individual components of a model. + struct ModelComponents { + + // The transition matrix. + storm::storage::SparseMatrix transitionMatrix; + + // The state labeling. + storm::models::sparse::StateLabeling stateLabeling; + + // The reward models. + std::unordered_map rewardModels; + + // A vector that stores a labeling for each choice. + boost::optional> choiceLabeling; + + // The exit rates for CTMCs and MAs. + std::vector exitRates; + + // The Markovian states for MA. + storm::storage::BitVector markovianStates; + + // A flag indicating if the model is non-deterministic. + bool nonDeterministic; + }; + + /*! + * Parse states and return transition matrix. + * + * @param file Input file stream. + * @param type Model type. + * @param stateSize No. of states + * + * @return Transition matrix. + */ + static std::shared_ptr parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, ValueParser const& valueParser); }; } // namespace parser From 9ad582dafca70cc9c63136fb47455e2869f9c063 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 1 Mar 2017 10:20:44 +0100 Subject: [PATCH 22/37] Import state labeling --- src/storm/parser/DirectEncodingParser.cpp | 30 +++++++++++++------- src/storm/parser/DirectEncodingParser.h | 2 +- src/storm/utility/DirectEncodingExporter.cpp | 1 + 3 files changed, 22 insertions(+), 11 deletions(-) diff --git a/src/storm/parser/DirectEncodingParser.cpp b/src/storm/parser/DirectEncodingParser.cpp index 1be94ca4c..8c1288ce1 100644 --- a/src/storm/parser/DirectEncodingParser.cpp +++ b/src/storm/parser/DirectEncodingParser.cpp @@ -126,6 +126,7 @@ namespace storm { std::shared_ptr modelComponents = std::make_shared(); modelComponents->nonDeterministic = (type == storm::models::ModelType::Mdp || type == storm::models::ModelType::MarkovAutomaton); storm::storage::SparseMatrixBuilder builder = storm::storage::SparseMatrixBuilder(0, 0, 0, false, modelComponents->nonDeterministic, 0); + modelComponents->stateLabeling = storm::models::sparse::StateLabeling(stateSize); // Iterate over all lines std::string line; @@ -136,6 +137,11 @@ namespace storm { STORM_LOG_TRACE("Parsing: " << line); if (boost::starts_with(line, "state ")) { // New state + if (first) { + first = false; + } else { + ++state; + } line = line.substr(6); size_t parsedId; size_t posId = line.find(" "); @@ -151,27 +157,36 @@ namespace storm { STORM_LOG_THROW(posEndReward != std::string::npos, storm::exceptions::WrongFormatException, "] missing."); std::string rewards = line.substr(1, posEndReward-1); STORM_LOG_TRACE("State rewards: " << rewards); - // TODO save rewards + // TODO import rewards + STORM_LOG_WARN("Rewards were not imported"); line = line.substr(posEndReward+1); } // Check for labels std::vector labels; boost::split(labels, line, boost::is_any_of(" ")); - if (!labels.empty()) { - STORM_LOG_TRACE("Labels: " << labels); + for (std::string label : labels) { + if (!modelComponents->stateLabeling.containsLabel(label)) { + modelComponents->stateLabeling.addLabel(label); + } + modelComponents->stateLabeling.addLabelToState(label, state); + STORM_LOG_TRACE("New label: " << label); } } else { // Only state id given parsedId = boost::lexical_cast(line); } - STORM_LOG_TRACE("New state " << state << " " << parsedId); + STORM_LOG_TRACE("New state " << state); STORM_LOG_ASSERT(state == parsedId, "State ids do not correspond."); if (modelComponents->nonDeterministic) { builder.newRowGroup(row); } - ++state; } else if (boost::starts_with(line, "\taction ")) { // New action + if (first) { + first = false; + } else { + ++row; + } line = line.substr(8); STORM_LOG_TRACE("New action: " << row); // Check for rewards @@ -186,11 +201,6 @@ namespace storm { } // TODO import choice labeling when the export works - if (first) { - first = false; - } else { - ++row; - } } else { // New transition size_t posColon = line.find(":"); diff --git a/src/storm/parser/DirectEncodingParser.h b/src/storm/parser/DirectEncodingParser.h index 1bbbf6a37..ba1056401 100644 --- a/src/storm/parser/DirectEncodingParser.h +++ b/src/storm/parser/DirectEncodingParser.h @@ -81,7 +81,7 @@ namespace storm { // A vector that stores a labeling for each choice. boost::optional> choiceLabeling; - // The exit rates for CTMCs and MAs. + // The exit rates for MAs. std::vector exitRates; // The Markovian states for MA. diff --git a/src/storm/utility/DirectEncodingExporter.cpp b/src/storm/utility/DirectEncodingExporter.cpp index 194ba7763..f08d979d6 100644 --- a/src/storm/utility/DirectEncodingExporter.cpp +++ b/src/storm/utility/DirectEncodingExporter.cpp @@ -104,6 +104,7 @@ namespace storm { // Write choice labeling if(sparseModel->hasChoiceLabeling()) { // TODO export choice labeling + STORM_LOG_WARN("Choice labeling was not exported."); } os << std::endl; From 40e125fb85c99929341c6c45331b53f9a473bcad Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 1 Mar 2017 17:19:32 +0100 Subject: [PATCH 23/37] Enable parsing of parametric DRN --- src/storm/cli/cli.cpp | 13 ++++++- src/storm/cli/entrypoints.h | 29 +++++++++++++++ src/storm/parser/DirectEncodingParser.cpp | 4 +- src/storm/utility/DirectEncodingExporter.cpp | 39 +++++++++++++++++--- src/storm/utility/DirectEncodingExporter.h | 9 +++++ 5 files changed, 84 insertions(+), 10 deletions(-) diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index a524de567..4eafad0f7 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -303,9 +303,18 @@ namespace storm { if (ioSettings.isPropertySet()) { properties = storm::parsePropertiesForExplicit(ioSettings.getProperty(), propertyFilter); } - - buildAndCheckExplicitModel(properties, true); + + if (generalSettings.isParametricSet()) { +#ifdef STORM_HAVE_CARL + buildAndCheckExplicitModel(properties, true); +#else + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No parameters are supported in this build."); +#endif + } else { + buildAndCheckExplicitModel(properties, true); + } } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); } } diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h index 38ed1f551..fcf743b14 100644 --- a/src/storm/cli/entrypoints.h +++ b/src/storm/cli/entrypoints.h @@ -409,6 +409,35 @@ namespace storm { verifySparseModel(model->as>(), properties, onlyInitialStatesRelevant); } } + +#ifdef STORM_HAVE_CARL + template<> + void buildAndCheckExplicitModel(std::vector const& properties, bool onlyInitialStatesRelevant) { + storm::settings::modules::IOSettings const& settings = storm::settings::getModule(); + + STORM_LOG_THROW(settings.isExplicitSet() || settings.isExplicitDRNSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files."); + + storm::utility::Stopwatch modelBuildingWatch(true); + std::shared_ptr model; + STORM_LOG_THROW(!settings.isExplicitSet(), storm::exceptions::NotSupportedException, "Parametric explicit model files are not supported."); + model = buildExplicitDRNModel(settings.getExplicitDRNFilename()); + modelBuildingWatch.stop(); + STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl); + + // Preprocess the model if needed. + BRANCH_ON_MODELTYPE(model, model, storm::RationalFunction, storm::dd::DdType::CUDD, preprocessModel, extractFormulasFromProperties(properties)); + + // Print some information about the model. + model->printModelInformationToStream(std::cout); + + // Verify the model, if a formula was given. + if (!properties.empty()) { + STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidStateException, "Expected sparse model."); + verifySparseModel(model->as>(), properties, onlyInitialStatesRelevant); + } + } +#endif + } } diff --git a/src/storm/parser/DirectEncodingParser.cpp b/src/storm/parser/DirectEncodingParser.cpp index 8c1288ce1..110c9ca32 100644 --- a/src/storm/parser/DirectEncodingParser.cpp +++ b/src/storm/parser/DirectEncodingParser.cpp @@ -20,8 +20,8 @@ namespace storm { namespace parser { - template<> - void ValueParser::addParameter(std::string const& parameter) { + template + void ValueParser::addParameter(std::string const& parameter) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameters are not supported in this build."); } diff --git a/src/storm/utility/DirectEncodingExporter.cpp b/src/storm/utility/DirectEncodingExporter.cpp index f08d979d6..b82957c9c 100644 --- a/src/storm/utility/DirectEncodingExporter.cpp +++ b/src/storm/utility/DirectEncodingExporter.cpp @@ -16,7 +16,7 @@ namespace storm { namespace exporter { template - void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters) { + void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters) { // Notice that for CTMCs we write the rate matrix instead of probabilities @@ -33,8 +33,14 @@ namespace storm { os << "// Original model type: " << sparseModel->getType() << std::endl; os << "@type: " << sparseModel->getType() << std::endl; os << "@parameters" << std::endl; - for (auto const& p : parameters) { - os << p << " "; + if (parameters.empty()) { + for (std::string const& parameter : getParameters(sparseModel)) { + os << parameter << " "; + } + } else { + for (std::string const& parameter : parameters) { + os << parameter << " "; + } } os << std::endl; os << "@nr_states" << std::endl << sparseModel->getNumberOfStates() << std::endl; @@ -119,12 +125,33 @@ namespace storm { } // end matrix iteration } - - - + + template + std::vector getParameters(std::shared_ptr> sparseModel) { + return {}; + } + template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); #ifdef STORM_HAVE_CARL + template<> + std::vector getParameters(std::shared_ptr> sparseModel) { + std::vector parameters; + std::set parametersProb = storm::models::sparse::getProbabilityParameters(*sparseModel); + for (auto const& parameter : parametersProb) { + std::stringstream stream; + stream << parameter; + parameters.push_back(stream.str()); + } + std::set parametersReward = storm::models::sparse::getRewardParameters(*sparseModel); + for (auto const& parameter : parametersReward) { + std::stringstream stream; + stream << parameter; + parameters.push_back(stream.str()); + } + return parameters; + } + template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); #endif diff --git a/src/storm/utility/DirectEncodingExporter.h b/src/storm/utility/DirectEncodingExporter.h index 2ebee0092..9728599a6 100644 --- a/src/storm/utility/DirectEncodingExporter.h +++ b/src/storm/utility/DirectEncodingExporter.h @@ -16,6 +16,15 @@ namespace storm { */ template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); + + /*! + * Accumalate parameters in the model. + * + * @param sparseModel Model. + * @return List of parameters in the model. + */ + template + std::vector getParameters(std::shared_ptr> sparseModel); } } From a18161b6e307d0795d77636c6e8d99fa39a93878 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 2 Mar 2017 17:03:35 +0100 Subject: [PATCH 24/37] Quick fix for CTMC instantiation --- src/storm/models/sparse/Ctmc.cpp | 7 ++++++- src/storm/models/sparse/Ctmc.h | 9 ++++++++- src/storm/utility/ModelInstantiator.h | 19 ++++++++++++++++--- 3 files changed, 30 insertions(+), 5 deletions(-) diff --git a/src/storm/models/sparse/Ctmc.cpp b/src/storm/models/sparse/Ctmc.cpp index 884eb359d..a43aded44 100644 --- a/src/storm/models/sparse/Ctmc.cpp +++ b/src/storm/models/sparse/Ctmc.cpp @@ -35,7 +35,12 @@ namespace storm { std::vector const& Ctmc::getExitRateVector() const { return exitRates; } - + + template + std::vector& Ctmc::getExitRateVector() { + return exitRates; + } + template std::vector Ctmc::createExitRateVector(storm::storage::SparseMatrix const& rateMatrix) { std::vector exitRates(rateMatrix.getRowCount()); diff --git a/src/storm/models/sparse/Ctmc.h b/src/storm/models/sparse/Ctmc.h index 417a899a4..8bb1f37ed 100644 --- a/src/storm/models/sparse/Ctmc.h +++ b/src/storm/models/sparse/Ctmc.h @@ -65,7 +65,14 @@ namespace storm { * @return The exit rate vector. */ std::vector const& getExitRateVector() const; - + + /*! + * Retrieves the vector of exit rates of the model. + * + * @return The exit rate vector. + */ + std::vector& getExitRateVector(); + private: /*! * Computes the exit rate vector based on the given rate matrix. diff --git a/src/storm/utility/ModelInstantiator.h b/src/storm/utility/ModelInstantiator.h index 17de0ea21..ce5154a2b 100644 --- a/src/storm/utility/ModelInstantiator.h +++ b/src/storm/utility/ModelInstantiator.h @@ -67,15 +67,28 @@ namespace storm { template typename std::enable_if< std::is_same>::value || - std::is_same>::value || - std::is_same>::value + std::is_same>::value >::type initializeModelSpecificData(PMT const& parametricModel) { auto stateLabelingCopy = parametricModel.getStateLabeling(); auto choiceLabelingCopy = parametricModel.getOptionalChoiceLabeling(); this->instantiatedModel = std::make_shared(buildDummyMatrix(parametricModel.getTransitionMatrix()), std::move(stateLabelingCopy), buildDummyRewardModels(parametricModel.getRewardModels()), std::move(choiceLabelingCopy)); } - + + template + typename std::enable_if< + std::is_same>::value + >::type + initializeModelSpecificData(PMT const& parametricModel) { + auto stateLabelingCopy = parametricModel.getStateLabeling(); + auto choiceLabelingCopy = parametricModel.getOptionalChoiceLabeling(); + std::vector exitRates(parametricModel.getExitRateVector().size(), storm::utility::one()); + this->instantiatedModel = std::make_shared(buildDummyMatrix(parametricModel.getTransitionMatrix()), std::move(exitRates), std::move(stateLabelingCopy), buildDummyRewardModels(parametricModel.getRewardModels()), std::move(choiceLabelingCopy)); + + initializeVectorMapping(this->instantiatedModel->getExitRateVector(), this->functions, this->vectorMapping, parametricModel.getExitRateVector()); + } + + template typename std::enable_if< std::is_same>::value From 02c7ace5e6fbc8bf0a9534199a1af547e4aea5ef Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 2 Mar 2017 17:55:58 +0100 Subject: [PATCH 25/37] Use heuristic NONE --- src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp | 2 +- src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h | 3 +-- src/storm-dft/storage/BucketPriorityQueue.h | 2 +- 3 files changed, 3 insertions(+), 4 deletions(-) diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp index d3e92fd1b..febccc0e6 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp @@ -65,7 +65,7 @@ namespace storm { { // Intentionally left empty. // TODO Matthias: remove again - usedHeuristic = storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE; + usedHeuristic = storm::builder::ApproximationHeuristic::NONE; // Compute independent subtrees if (dft.topLevelType() == storm::storage::DFTElementType::OR) { diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h index ce86fc759..6facce687 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h +++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h @@ -29,7 +29,7 @@ namespace storm { using DFTStatePointer = std::shared_ptr>; // TODO Matthias: make choosable - using ExplorationHeuristic = DFTExplorationHeuristicBoundDifference; + using ExplorationHeuristic = DFTExplorationHeuristicNone; using ExplorationHeuristicPointer = std::shared_ptr; @@ -335,7 +335,6 @@ namespace storm { // A priority queue of states that still need to be explored. storm::storage::BucketPriorityQueue explorationQueue; - //storm::storage::DynamicPriorityQueue, std::function> explorationQueue; // A mapping of not yet explored states from the id to the tuple (state object, heuristic values). std::map> statesNotExplored; diff --git a/src/storm-dft/storage/BucketPriorityQueue.h b/src/storm-dft/storage/BucketPriorityQueue.h index a332311a7..5acd178d6 100644 --- a/src/storm-dft/storage/BucketPriorityQueue.h +++ b/src/storm-dft/storage/BucketPriorityQueue.h @@ -13,7 +13,7 @@ namespace storm { template class BucketPriorityQueue { - using HeuristicPointer = std::shared_ptr>; + using HeuristicPointer = std::shared_ptr>; public: explicit BucketPriorityQueue(size_t nrBuckets, double lowerValue, double ratio); From 5c0e515adeb8105742b5ba5db24c9dd1fc3fd321 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 2 Mar 2017 18:05:36 +0100 Subject: [PATCH 26/37] Build all labels when exporting DFT --- src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp | 6 +++--- src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h | 5 ++++- src/storm-dft/modelchecker/dft/DFTModelChecker.cpp | 2 +- 3 files changed, 8 insertions(+), 5 deletions(-) diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp index febccc0e6..65d9f838b 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp @@ -28,7 +28,7 @@ namespace storm { } template - ExplicitDFTModelBuilderApprox::LabelOptions::LabelOptions(std::vector> properties) : buildFailLabel(true), buildFailSafeLabel(false) { + ExplicitDFTModelBuilderApprox::LabelOptions::LabelOptions(std::vector> properties, bool buildAllLabels) : buildFailLabel(true), buildFailSafeLabel(false), buildAllLabels(buildAllLabels) { // Get necessary labels from properties std::vector> atomicLabels; for (auto property : properties) { @@ -441,7 +441,7 @@ namespace storm { // Collect labels for all necessary elements for (size_t id = 0; id < dft.nrElements(); ++id) { std::shared_ptr const> element = dft.getElement(id); - if (labelOpts.elementLabels.count(element->name()) > 0) { + if (labelOpts.buildAllLabels || labelOpts.elementLabels.count(element->name()) > 0) { modelComponents.stateLabeling.addLabel(element->name() + "_fail"); } } @@ -462,7 +462,7 @@ namespace storm { // Set fail status for each necessary element for (size_t id = 0; id < dft.nrElements(); ++id) { std::shared_ptr const> element = dft.getElement(id); - if (labelOpts.elementLabels.count(element->name()) > 0 && storm::storage::DFTState::hasFailed(state, stateGenerationInfo->getStateIndex(element->id()))) { + if ((labelOpts.buildAllLabels || labelOpts.elementLabels.count(element->name()) > 0) && storm::storage::DFTState::hasFailed(state, stateGenerationInfo->getStateIndex(element->id()))) { modelComponents.stateLabeling.addLabelToState(element->name() + "_fail", stateId); } } diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h index 6facce687..d7ee37de5 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h +++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h @@ -154,7 +154,7 @@ namespace storm { // A structure holding the labeling options. struct LabelOptions { // Constructor - LabelOptions(std::vector> properties); + LabelOptions(std::vector> properties, bool buildAllLabels = false); // Flag indicating if the general fail label should be included. bool buildFailLabel; @@ -162,6 +162,9 @@ namespace storm { // Flag indicating if the general failsafe label should be included. bool buildFailSafeLabel; + // Flag indicating if all possible labels should be included. + bool buildAllLabels; + // Set of element names whose fail label to include. std::set elementLabels; }; diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 8d655764e..73c107de6 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -344,7 +344,7 @@ namespace storm { // TODO Matthias: use only one builder if everything works again if (storm::settings::getModule().isApproximationErrorSet()) { storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions(properties); + typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions(properties, storm::settings::getModule().isExportExplicitSet()); builder.buildModel(labeloptions, 0, 0.0); model = builder.getModel(); } else { From 9a5e47151ba8ee64f4b126517b1634ce13dd2b6b Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 3 Mar 2017 12:05:16 +0100 Subject: [PATCH 27/37] Fixed double s in times --- src/storm-dft/modelchecker/dft/DFTModelChecker.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 73c107de6..0ecf2718f 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -430,11 +430,11 @@ namespace storm { template void DFTModelChecker::printTimings(std::ostream& os) { os << "Times:" << std::endl; - os << "Exploration:\t" << explorationTimer << "s" << std::endl; - os << "Building:\t" << buildingTimer << "s" << std::endl; - os << "Bisimulation:\t" << bisimulationTimer<< "s" << std::endl; - os << "Modelchecking:\t" << modelCheckingTimer << "s" << std::endl; - os << "Total:\t\t" << totalTimer << "s" << std::endl; + os << "Exploration:\t" << explorationTimer << std::endl; + os << "Building:\t" << buildingTimer << std::endl; + os << "Bisimulation:\t" << bisimulationTimer<< std::endl; + os << "Modelchecking:\t" << modelCheckingTimer << std::endl; + os << "Total:\t\t" << totalTimer << std::endl; } template From 0b6273cad63543cab6c0526e7477c85b94d431d1 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Sun, 5 Mar 2017 19:58:59 +0100 Subject: [PATCH 28/37] Implemented parsing for UnaryNumericalFunctionExpression --- .../storage/expressions/ToRationalFunctionVisitor.cpp | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp b/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp index 6fa620157..870014f60 100644 --- a/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp +++ b/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp @@ -94,8 +94,15 @@ namespace storm { } template - boost::any ToRationalFunctionVisitor::visit(UnaryNumericalFunctionExpression const&, boost::any const&) { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function."); + boost::any ToRationalFunctionVisitor::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) { + RationalFunctionType operandAsRationalFunction = boost::any_cast(expression.getOperand()->accept(*this, data)); + switch (expression.getOperatorType()) { + case UnaryNumericalFunctionExpression::OperatorType::Minus: + return -operandAsRationalFunction; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function."); + } + return boost::any(); } template From 3483e794127c4a7ff9f1dee53b0b13a320889f02 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Sun, 5 Mar 2017 19:59:35 +0100 Subject: [PATCH 29/37] Parse parameters in JSON --- src/storm-dft/parser/DFTGalileoParser.cpp | 1 - src/storm-dft/parser/DFTJsonParser.cpp | 15 +++++++++++---- 2 files changed, 11 insertions(+), 5 deletions(-) diff --git a/src/storm-dft/parser/DFTGalileoParser.cpp b/src/storm-dft/parser/DFTGalileoParser.cpp index c5a88716c..38dec9bf0 100644 --- a/src/storm-dft/parser/DFTGalileoParser.cpp +++ b/src/storm-dft/parser/DFTGalileoParser.cpp @@ -5,7 +5,6 @@ #include #include #include -#include "storm/storage/expressions/ExpressionManager.h" #include "storm/exceptions/NotImplementedException.h" #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/NotSupportedException.h" diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp index 07454416f..83710b482 100644 --- a/src/storm-dft/parser/DFTJsonParser.cpp +++ b/src/storm-dft/parser/DFTJsonParser.cpp @@ -5,7 +5,6 @@ #include #include #include -#include "storm/storage/expressions/ExpressionManager.h" #include "storm/exceptions/NotImplementedException.h" #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/NotSupportedException.h" @@ -42,9 +41,17 @@ namespace storm { parsedJson << file; storm::utility::closeFile(file); - storm::expressions::Variable var = manager->declareRationalVariable("x"); - identifierMapping.emplace(var.getName(), var); - parser.setIdentifierMapping(identifierMapping); + json parameters = parsedJson.at("parameters"); +#ifdef STORM_HAVE_CARL + STORM_LOG_THROW((std::is_same::value), storm::exceptions::NotSupportedException, "Parameters only allowed when using rational functions."); + for (auto it = parameters.begin(); it != parameters.end(); ++it) { + std::string parameter = it.key(); + storm::expressions::Variable var = manager->declareRationalVariable(parameter); + identifierMapping.emplace(var.getName(), var); + parser.setIdentifierMapping(identifierMapping); + STORM_LOG_TRACE("Added parameter: " << var.getName()); + } +#endif json nodes = parsedJson.at("nodes"); From d813851897616defc19d92d702268ca896b24906 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 8 Mar 2017 13:13:25 +0100 Subject: [PATCH 30/37] Small fix --- src/storm-dft/parser/DFTJsonParser.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp index 83710b482..ac4e094ff 100644 --- a/src/storm-dft/parser/DFTJsonParser.cpp +++ b/src/storm-dft/parser/DFTJsonParser.cpp @@ -43,8 +43,8 @@ namespace storm { json parameters = parsedJson.at("parameters"); #ifdef STORM_HAVE_CARL - STORM_LOG_THROW((std::is_same::value), storm::exceptions::NotSupportedException, "Parameters only allowed when using rational functions."); for (auto it = parameters.begin(); it != parameters.end(); ++it) { + STORM_LOG_THROW((std::is_same::value), storm::exceptions::NotSupportedException, "Parameters only allowed when using rational functions."); std::string parameter = it.key(); storm::expressions::Variable var = manager->declareRationalVariable(parameter); identifierMapping.emplace(var.getName(), var); From c26237c16f75193161784ac476473b71e5f30926 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 8 Mar 2017 13:14:08 +0100 Subject: [PATCH 31/37] Export Dft headers for stormpy --- src/storm-dft/CMakeLists.txt | 26 +++++++++++++++++++++++++- src/storm-gspn/CMakeLists.txt | 4 +++- 2 files changed, 28 insertions(+), 2 deletions(-) diff --git a/src/storm-dft/CMakeLists.txt b/src/storm-dft/CMakeLists.txt index 16fa40e48..3951551ae 100644 --- a/src/storm-dft/CMakeLists.txt +++ b/src/storm-dft/CMakeLists.txt @@ -10,7 +10,31 @@ file(GLOB_RECURSE STORM_DFT_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-dft/*/*.h) # Create storm-pgcl. add_library(storm-dft SHARED ${STORM_DFT_SOURCES} ${STORM_DFT_HEADERS}) -target_link_libraries(storm-dft storm storm-gspn ${STORM_DFT_LINK_LIBRARIES}) + +# Remove define symbol for shared libstorm. +set_target_properties(storm-dft PROPERTIES DEFINE_SYMBOL "") +#add_dependencies(storm resources) +list(APPEND STORM_TARGETS storm-dft) +set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) + +target_link_libraries(storm-dft PUBLIC storm storm-gspn ${STORM_DFT_LINK_LIBRARIES}) + +# Install storm headers to include directory. +foreach(HEADER ${STORM_DFT_HEADERS}) + string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER}) + string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH}) + string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH}) + add_custom_command( + OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} + COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY} + COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} + DEPENDS ${HEADER} + ) + list(APPEND STORM_DFT_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}") +endforeach() +add_custom_target(copy_storm_dft_headers DEPENDS ${STORM_DFT_OUTPUT_HEADERS} ${STORM_DFT_HEADERS}) +add_dependencies(storm-dft copy_storm_dft_headers) # installation install(TARGETS storm-dft RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) + diff --git a/src/storm-gspn/CMakeLists.txt b/src/storm-gspn/CMakeLists.txt index 564b696bd..cf80ff6aa 100644 --- a/src/storm-gspn/CMakeLists.txt +++ b/src/storm-gspn/CMakeLists.txt @@ -10,7 +10,9 @@ file(GLOB_RECURSE STORM_GSPN_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-gspn/*/*.h) # Create storm-pgcl. add_library(storm-gspn SHARED ${STORM_GSPN_SOURCES} ${STORM_GSPN_HEADERS}) +list(APPEND STORM_TARGETS storm-gspn) +set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) target_link_libraries(storm-gspn storm ${STORM_GSPN_LINK_LIBRARIES}) # installation -install(TARGETS storm-gspn RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) \ No newline at end of file +install(TARGETS storm-gspn RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) From ac8cea1e53bdfbf9cb188da0529fc92c2d69956b Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 10 Mar 2017 16:23:26 +0100 Subject: [PATCH 32/37] Added transient BEs --- src/storm-dft/generator/DftNextStateGenerator.cpp | 2 +- src/storm-dft/parser/DFTGalileoParser.cpp | 2 +- src/storm-dft/parser/DFTJsonParser.cpp | 6 +++++- src/storm-dft/storage/dft/DFTBuilder.cpp | 2 +- src/storm-dft/storage/dft/DFTBuilder.h | 6 +++--- src/storm-dft/storage/dft/elements/DFTBE.h | 9 +++++++-- 6 files changed, 18 insertions(+), 9 deletions(-) diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index 245a448ef..7b86d1faa 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -112,7 +112,7 @@ namespace storm { newState->updateFailableDependencies(next->id()); } - if(newState->isInvalid()) { + if(newState->isInvalid() || (nextBE->isTransient() && !newState->hasFailed(mDft.getTopLevelIndex()))) { // Continue with next possible state ++currentFailable; continue; diff --git a/src/storm-dft/parser/DFTGalileoParser.cpp b/src/storm-dft/parser/DFTGalileoParser.cpp index 38dec9bf0..c81c2767a 100644 --- a/src/storm-dft/parser/DFTGalileoParser.cpp +++ b/src/storm-dft/parser/DFTGalileoParser.cpp @@ -124,7 +124,7 @@ namespace storm { } else if (boost::starts_with(tokens[1], "lambda=")) { ValueType failureRate = parseRationalExpression(tokens[1].substr(7)); ValueType dormancyFactor = parseRationalExpression(tokens[2].substr(5)); - success = builder.addBasicElement(name, failureRate, dormancyFactor); + success = builder.addBasicElement(name, failureRate, dormancyFactor, false); // TODO set transient BEs } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Type name: " << tokens[1] << " not recognized."); success = false; diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp index ac4e094ff..0d6f312f2 100644 --- a/src/storm-dft/parser/DFTJsonParser.cpp +++ b/src/storm-dft/parser/DFTJsonParser.cpp @@ -100,7 +100,11 @@ namespace storm { } else if (type == "be") { ValueType failureRate = parseRationalExpression(data.at("rate")); ValueType dormancyFactor = parseRationalExpression(data.at("dorm")); - success = builder.addBasicElement(name, failureRate, dormancyFactor); + bool transient = false; + if (data.count("transient") > 0) { + transient = data.at("transient"); + } + success = builder.addBasicElement(name, failureRate, dormancyFactor, transient); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Type name: " << type << " not recognized."); success = false; diff --git a/src/storm-dft/storage/dft/DFTBuilder.cpp b/src/storm-dft/storage/dft/DFTBuilder.cpp index 66beaa387..88abc9665 100644 --- a/src/storm-dft/storage/dft/DFTBuilder.cpp +++ b/src/storm-dft/storage/dft/DFTBuilder.cpp @@ -272,7 +272,7 @@ namespace storm { if (be->canFail()) { dormancyFactor = be->passiveFailureRate() / be->activeFailureRate(); } - addBasicElement(be->name(), be->activeFailureRate(), dormancyFactor); + addBasicElement(be->name(), be->activeFailureRate(), dormancyFactor, be->isTransient()); break; } case DFTElementType::CONSTF: diff --git a/src/storm-dft/storage/dft/DFTBuilder.h b/src/storm-dft/storage/dft/DFTBuilder.h index 598c1d765..42713e601 100644 --- a/src/storm-dft/storage/dft/DFTBuilder.h +++ b/src/storm-dft/storage/dft/DFTBuilder.h @@ -105,7 +105,7 @@ namespace storm { if (binaryDependencies && !storm::utility::isOne(probability) && children.size() > 2) { // Introduce additional element for first capturing the probabilistic dependency std::string nameAdditional = name + "_additional"; - addBasicElement(nameAdditional, storm::utility::zero(), storm::utility::zero()); + addBasicElement(nameAdditional, storm::utility::zero(), storm::utility::zero(), false); // First consider probabilistic dependency addDepElement(name + "_pdep", {children.front(), nameAdditional}, probability); // Then consider dependencies to the children if probabilistic dependency failed @@ -168,12 +168,12 @@ namespace storm { return true; } - bool addBasicElement(std::string const& name, ValueType failureRate, ValueType dormancyFactor) { + bool addBasicElement(std::string const& name, ValueType failureRate, ValueType dormancyFactor, bool transient = false) { //TODO Matthias: collect constraints for SMT solving //failureRate > 0 //0 <= dormancyFactor <= 1 - mElements[name] = std::make_shared>(mNextId++, name, failureRate, dormancyFactor); + mElements[name] = std::make_shared>(mNextId++, name, failureRate, dormancyFactor, transient); return true; } diff --git a/src/storm-dft/storage/dft/elements/DFTBE.h b/src/storm-dft/storage/dft/elements/DFTBE.h index 3be82d9f1..6bb234b4e 100644 --- a/src/storm-dft/storage/dft/elements/DFTBE.h +++ b/src/storm-dft/storage/dft/elements/DFTBE.h @@ -11,10 +11,11 @@ namespace storm { ValueType mActiveFailureRate; ValueType mPassiveFailureRate; DFTDependencyVector mIngoingDependencies; + bool mTransient; public: - DFTBE(size_t id, std::string const& name, ValueType failureRate, ValueType dormancyFactor) : - DFTElement(id, name), mActiveFailureRate(failureRate), mPassiveFailureRate(dormancyFactor * failureRate) + DFTBE(size_t id, std::string const& name, ValueType failureRate, ValueType dormancyFactor, bool transient = false) : + DFTElement(id, name), mActiveFailureRate(failureRate), mPassiveFailureRate(dormancyFactor * failureRate), mTransient(transient) {} DFTElementType type() const override { @@ -32,6 +33,10 @@ namespace storm { ValueType const& passiveFailureRate() const { return mPassiveFailureRate; } + + bool isTransient() const { + return mTransient; + } bool canFail() const { return !storm::utility::isZero(mActiveFailureRate); From 8cbfccba225ef5d00c16aa4e1cc578333db69ebe Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 10 Mar 2017 23:03:25 +0100 Subject: [PATCH 33/37] Hacked approximation for probabilities --- .../builder/DftExplorationHeuristic.h | 4 +- .../builder/ExplicitDFTModelBuilderApprox.cpp | 76 +++++++++++++++++-- .../builder/ExplicitDFTModelBuilderApprox.h | 17 +++-- .../modelchecker/dft/DFTModelChecker.cpp | 7 +- src/storm-dft/storage/BucketPriorityQueue.h | 2 +- 5 files changed, 87 insertions(+), 19 deletions(-) diff --git a/src/storm-dft/builder/DftExplorationHeuristic.h b/src/storm-dft/builder/DftExplorationHeuristic.h index 874cfb586..f4cc3c1ce 100644 --- a/src/storm-dft/builder/DftExplorationHeuristic.h +++ b/src/storm-dft/builder/DftExplorationHeuristic.h @@ -107,8 +107,8 @@ namespace storm { } bool updateHeuristicValues(DFTExplorationHeuristic const& predecessor, ValueType, ValueType) override { - if (predecessor.getDepth() < this->depth) { - this->depth = predecessor.getDepth(); + if (predecessor.getDepth() + 1 < this->depth) { + this->depth = predecessor.getDepth() + 1; return true; } return false; diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp index 65d9f838b..8483aa3fd 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp @@ -65,7 +65,7 @@ namespace storm { { // Intentionally left empty. // TODO Matthias: remove again - usedHeuristic = storm::builder::ApproximationHeuristic::NONE; + usedHeuristic = storm::builder::ApproximationHeuristic::DEPTH; // Compute independent subtrees if (dft.topLevelType() == storm::storage::DFTElementType::OR) { @@ -349,8 +349,8 @@ namespace storm { // Try to explore the next state generator.load(currentState); - if (approximationThreshold > 0.0 && nrExpandedStates > approximationThreshold && !currentExplorationHeuristic->isExpand()) { - //if (currentExplorationHeuristic->isSkip(approximationThreshold)) { + //if (approximationThreshold > 0.0 && nrExpandedStates > approximationThreshold && !currentExplorationHeuristic->isExpand()) { + if (approximationThreshold > 0.0 && currentExplorationHeuristic->isSkip(approximationThreshold)) { // Skip the current state ++nrSkippedStates; STORM_LOG_TRACE("Skip expansion of state: " << dft.getStateString(currentState)); @@ -397,6 +397,7 @@ namespace storm { STORM_LOG_ASSERT(!currentState->isPseudoState(), "State is pseudo state."); // Initialize bounds + // TODO Mathias: avoid hack ValueType lowerBound = getLowerBound(state); ValueType upperBound = getUpperBound(state); heuristic->setBounds(lowerBound, upperBound); @@ -478,10 +479,70 @@ namespace storm { } template - std::shared_ptr> ExplicitDFTModelBuilderApprox::getModelApproximation(bool lowerBound) { - // TODO Matthias: handle case with no skipped states - changeMatrixBound(modelComponents.transitionMatrix, lowerBound); - return createModel(true); + std::shared_ptr> ExplicitDFTModelBuilderApprox::getModelApproximation(bool lowerBound, bool expectedTime) { + if (expectedTime) { + // TODO Matthias: handle case with no skipped states + changeMatrixBound(modelComponents.transitionMatrix, lowerBound); + return createModel(true); + } else { + // Change model for probabilities + // TODO Matthias: make nicer + storm::storage::SparseMatrix matrix = modelComponents.transitionMatrix; + storm::models::sparse::StateLabeling labeling = modelComponents.stateLabeling; + if (lowerBound) { + // Set self loop for lower bound + for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) { + auto matrixEntry = matrix.getRow(it->first, 0).begin(); + STORM_LOG_ASSERT(matrixEntry->getColumn() == failedStateId, "Transition has wrong target state."); + STORM_LOG_ASSERT(!it->second.first->isPseudoState(), "State is still pseudo state."); + matrixEntry->setValue(storm::utility::one()); + matrixEntry->setColumn(it->first); + } + } else { + // Make skipped states failed states for upper bound + storm::storage::BitVector failedStates = modelComponents.stateLabeling.getStates("failed"); + for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) { + failedStates.set(it->first); + } + labeling.setStates("failed", failedStates); + } + + std::shared_ptr> model; + if (modelComponents.deterministicModel) { + model = std::make_shared>(std::move(matrix), std::move(labeling)); + } else { + // Build MA + // Compute exit rates + // TODO Matthias: avoid computing multiple times + modelComponents.exitRates = std::vector(modelComponents.markovianStates.size()); + std::vector::index_type> indices = matrix.getRowGroupIndices(); + for (StateType stateIndex = 0; stateIndex < modelComponents.markovianStates.size(); ++stateIndex) { + if (modelComponents.markovianStates[stateIndex]) { + modelComponents.exitRates[stateIndex] = matrix.getRowSum(indices[stateIndex]); + } else { + modelComponents.exitRates[stateIndex] = storm::utility::zero(); + } + } + STORM_LOG_TRACE("Exit rates: " << modelComponents.exitRates); + + std::shared_ptr> ma = std::make_shared>(std::move(matrix), std::move(labeling), modelComponents.markovianStates, modelComponents.exitRates); + if (ma->hasOnlyTrivialNondeterminism()) { + // Markov automaton can be converted into CTMC + // TODO Matthias: change components which were not moved accordingly + model = ma->convertToCTMC(); + } else { + model = ma; + } + + } + + if (model->getNumberOfStates() <= 15) { + STORM_LOG_TRACE("Transition matrix: " << std::endl << model->getTransitionMatrix()); + } else { + STORM_LOG_TRACE("Transition matrix: too big to print"); + } + return model; + } } template @@ -573,6 +634,7 @@ namespace storm { if (state->hasFailed(dft.getTopLevelIndex())) { return storm::utility::zero(); } + // Get the upper bound by considering the failure of all BEs ValueType upperBound = storm::utility::one(); ValueType rateSum = storm::utility::zero(); diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h index d7ee37de5..97439f47a 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h +++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h @@ -29,7 +29,7 @@ namespace storm { using DFTStatePointer = std::shared_ptr>; // TODO Matthias: make choosable - using ExplorationHeuristic = DFTExplorationHeuristicNone; + using ExplorationHeuristic = DFTExplorationHeuristicDepth; using ExplorationHeuristicPointer = std::shared_ptr; @@ -197,11 +197,12 @@ namespace storm { /*! * Get the built approximation model for either the lower or upper bound. * - * @param lowerBound If true, the lower bound model is returned, else the upper bound model + * @param lowerBound If true, the lower bound model is returned, else the upper bound model + * @param expectedTime If true, the bounds for expected time are computed, else the bounds for probabilities. * * @return The model built from the DFT. */ - std::shared_ptr> getModelApproximation(bool lowerBound = true); + std::shared_ptr> getModelApproximation(bool lowerBound, bool expectedTime); private: @@ -243,14 +244,16 @@ namespace storm { /** * Change matrix to reflect the lower or upper approximation bound. * - * @param matrix Matrix to change. The change are reflected here. - * @param lowerBound Flag indicating if the lower bound should be used. Otherwise the upper bound is used. + * @param matrix Matrix to change. The change are reflected here. + * @param lowerBound Flag indicating if the lower bound should be used. Otherwise the upper bound is used. */ void changeMatrixBound(storm::storage::SparseMatrix & matrix, bool lowerBound) const; /*! * Get lower bound approximation for state. * + * @param state The state. + * * @return Lower bound approximation. */ ValueType getLowerBound(DFTStatePointer const& state) const; @@ -258,6 +261,8 @@ namespace storm { /*! * Get upper bound approximation for state. * + * @param state The state. + * * @return Upper bound approximation. */ ValueType getUpperBound(DFTStatePointer const& state) const; @@ -310,7 +315,7 @@ namespace storm { bool enableDC = true; //TODO Matthias: make changeable - const bool mergeFailedStates = false; + const bool mergeFailedStates = true; // Heuristic used for approximation storm::builder::ApproximationHeuristic usedHeuristic; diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 0ecf2718f..79ed0ef95 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -303,7 +303,7 @@ namespace storm { // Build model for lower bound STORM_LOG_INFO("Getting model for lower bound..."); - model = builder.getModelApproximation(probabilityFormula ? false : true); + model = builder.getModelApproximation(true, !probabilityFormula); // We only output the info from the lower bound as the info for the upper bound is the same model->printModelInformationToStream(std::cout); buildingTimer.stop(); @@ -317,15 +317,16 @@ namespace storm { // Build model for upper bound STORM_LOG_INFO("Getting model for upper bound..."); buildingTimer.start(); - model = builder.getModelApproximation(probabilityFormula ? true : false); + model = builder.getModelApproximation(false, !probabilityFormula); buildingTimer.stop(); // Check upper bound - newResult = checkModel(model, {properties}); + newResult = checkModel(model, {property}); STORM_LOG_ASSERT(newResult.size() == 1, "Wrong size for result vector."); STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(approxResult.second, newResult[0]), "New over-approximation " << newResult[0] << " is greater than old result " << approxResult.second); approxResult.second = newResult[0]; ++iteration; + STORM_LOG_ASSERT(comparator.isLess(approxResult.first, approxResult.second) || comparator.isEqual(approxResult.first, approxResult.second), "Under-approximation " << approxResult.first << " is greater than over-approximation " << approxResult.second); STORM_LOG_INFO("Result after iteration " << iteration << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")"); totalTimer.stop(); printTimings(); diff --git a/src/storm-dft/storage/BucketPriorityQueue.h b/src/storm-dft/storage/BucketPriorityQueue.h index 5acd178d6..004469f9a 100644 --- a/src/storm-dft/storage/BucketPriorityQueue.h +++ b/src/storm-dft/storage/BucketPriorityQueue.h @@ -13,7 +13,7 @@ namespace storm { template class BucketPriorityQueue { - using HeuristicPointer = std::shared_ptr>; + using HeuristicPointer = std::shared_ptr>; public: explicit BucketPriorityQueue(size_t nrBuckets, double lowerValue, double ratio); From affa7db555fe6bf2b06003f7cfdf70d74dd0e8be Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Sat, 11 Mar 2017 14:26:29 +0100 Subject: [PATCH 34/37] Depth heuristic did not skip --- src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp index 8483aa3fd..84eaa21a7 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp @@ -177,7 +177,7 @@ namespace storm { approximationThreshold = dft.nrElements()+10; break; case storm::builder::ApproximationHeuristic::DEPTH: - approximationThreshold = iteration; + approximationThreshold = iteration + 1; break; case storm::builder::ApproximationHeuristic::PROBABILITY: case storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE: From 9b567608f3f7e38038bc453148d724c266b3aec3 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Sun, 12 Mar 2017 19:10:51 +0100 Subject: [PATCH 35/37] Find symmetries for BEs as well --- src/storm-dft/storage/dft/DFT.cpp | 102 ++++++++++++--------- src/storm-dft/storage/dft/DFT.h | 2 + src/storm-dft/storage/dft/DFTIsomorphism.h | 2 +- 3 files changed, 61 insertions(+), 45 deletions(-) diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index e38c40ce1..a5f2f6444 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -651,58 +651,72 @@ namespace storm { storm::utility::iota_n(std::back_inserter(vec), nrElements(), 0); BijectionCandidates completeCategories = colouring.colourSubdft(vec); std::map>> res; - + + // Find symmetries for gates for(auto const& colourClass : completeCategories.gateCandidates) { - if(colourClass.second.size() > 1) { - std::set foundEqClassFor; - for(auto it1 = colourClass.second.cbegin(); it1 != colourClass.second.cend(); ++it1) { - std::vector> symClass; - if(foundEqClassFor.count(*it1) > 0) { - // This item is already in a class. - continue; - } - if(!getGate(*it1)->hasOnlyStaticParents()) { - continue; - } - - std::pair, std::vector> influencedElem1Ids = getSortedParentAndOutDepIds(*it1); - auto it2 = it1; - for(++it2; it2 != colourClass.second.cend(); ++it2) { - if(!getGate(*it2)->hasOnlyStaticParents()) { - continue; - } - std::vector sortedParent2Ids = getGate(*it2)->parentIds(); - std::sort(sortedParent2Ids.begin(), sortedParent2Ids.end()); - - if(influencedElem1Ids == getSortedParentAndOutDepIds(*it2)) { - std::map bijection = findBijection(*it1, *it2, colouring, true); - if (!bijection.empty()) { - STORM_LOG_TRACE("Subdfts are symmetric"); - foundEqClassFor.insert(*it2); - if(symClass.empty()) { - for(auto const& i : bijection) { - symClass.push_back(std::vector({i.first})); - } - } - auto symClassIt = symClass.begin(); - for(auto const& i : bijection) { - symClassIt->emplace_back(i.second); - ++symClassIt; - - } + findSymmetriesHelper(colourClass.second, colouring, res); + } + + // Find symmetries for BEs + for(auto const& colourClass : completeCategories.beCandidates) { + findSymmetriesHelper(colourClass.second, colouring, res); + } + + return DFTIndependentSymmetries(res); + } + + template + void DFT::findSymmetriesHelper(std::vector const& candidates, DFTColouring const& colouring, std::map>>& result) const { + if(candidates.size() <= 0) { + return; + } + + std::set foundEqClassFor; + for(auto it1 = candidates.cbegin(); it1 != candidates.cend(); ++it1) { + std::vector> symClass; + if(foundEqClassFor.count(*it1) > 0) { + // This item is already in a class. + continue; + } + if(!getElement(*it1)->hasOnlyStaticParents()) { + continue; + } + + std::pair, std::vector> influencedElem1Ids = getSortedParentAndOutDepIds(*it1); + auto it2 = it1; + for(++it2; it2 != candidates.cend(); ++it2) { + if(!getElement(*it2)->hasOnlyStaticParents()) { + continue; + } + std::vector sortedParent2Ids = getElement(*it2)->parentIds(); + std::sort(sortedParent2Ids.begin(), sortedParent2Ids.end()); + + if(influencedElem1Ids == getSortedParentAndOutDepIds(*it2)) { + std::map bijection = findBijection(*it1, *it2, colouring, true); + if (!bijection.empty()) { + STORM_LOG_TRACE("Subdfts are symmetric"); + foundEqClassFor.insert(*it2); + if(symClass.empty()) { + for(auto const& i : bijection) { + symClass.push_back(std::vector({i.first})); } } - } - if(!symClass.empty()) { - res.emplace(*it1, symClass); + auto symClassIt = symClass.begin(); + for(auto const& i : bijection) { + symClassIt->emplace_back(i.second); + ++symClassIt; + + } } } - + } + + if(!symClass.empty()) { + result.emplace(*it1, symClass); } } - return DFTIndependentSymmetries(res); } - + template std::vector DFT::findModularisationRewrite() const { for(auto const& e : mElements) { diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h index 1304bbfa9..815bb0df5 100644 --- a/src/storm-dft/storage/dft/DFT.h +++ b/src/storm-dft/storage/dft/DFT.h @@ -261,6 +261,8 @@ namespace storm { DFTIndependentSymmetries findSymmetries(DFTColouring const& colouring) const; + void findSymmetriesHelper(std::vector const& candidates, DFTColouring const& colouring, std::map>>& result) const; + std::vector immediateFailureCauses(size_t index) const; std::vector findModularisationRewrite() const; diff --git a/src/storm-dft/storage/dft/DFTIsomorphism.h b/src/storm-dft/storage/dft/DFTIsomorphism.h index 081b76f0b..869cbd065 100644 --- a/src/storm-dft/storage/dft/DFTIsomorphism.h +++ b/src/storm-dft/storage/dft/DFTIsomorphism.h @@ -249,7 +249,7 @@ namespace storage { protected: void colourize(std::shared_ptr> const& be) { - beColour[be->id()] = BEColourClass(be->activeFailureRate(), be->passiveFailureRate(), be->nrParents()); + beColour[be->id()] = BEColourClass(be->activeFailureRate(), be->passiveFailureRate(), be->nrParents()); } void colourize(std::shared_ptr> const& gate) { From fd2f83fe6de4189c3206f970f40eadaac79c16c1 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Sun, 12 Mar 2017 20:29:39 +0100 Subject: [PATCH 36/37] Consider ingoing dependencies for symmetry --- src/storm-dft/storage/dft/DFT.cpp | 30 +++++++++++++++++++----------- src/storm-dft/storage/dft/DFT.h | 2 +- 2 files changed, 20 insertions(+), 12 deletions(-) diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index a5f2f6444..b21338c74 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -682,16 +682,14 @@ namespace storm { continue; } - std::pair, std::vector> influencedElem1Ids = getSortedParentAndOutDepIds(*it1); + std::tuple, std::vector, std::vector> influencedElem1Ids = getSortedParentAndDependencyIds(*it1); auto it2 = it1; for(++it2; it2 != candidates.cend(); ++it2) { if(!getElement(*it2)->hasOnlyStaticParents()) { continue; } - std::vector sortedParent2Ids = getElement(*it2)->parentIds(); - std::sort(sortedParent2Ids.begin(), sortedParent2Ids.end()); - if(influencedElem1Ids == getSortedParentAndOutDepIds(*it2)) { + if(influencedElem1Ids == getSortedParentAndDependencyIds(*it2)) { std::map bijection = findBijection(*it1, *it2, colouring, true); if (!bijection.empty()) { STORM_LOG_TRACE("Subdfts are symmetric"); @@ -748,15 +746,25 @@ namespace storm { template - std::pair, std::vector> DFT::getSortedParentAndOutDepIds(size_t index) const { - std::pair, std::vector> res; - res.first = getElement(index)->parentIds(); - std::sort(res.first.begin(), res.first.end()); + std::tuple, std::vector, std::vector> DFT::getSortedParentAndDependencyIds(size_t index) const { + // Parents + std::vector parents = getElement(index)->parentIds(); + std::sort(parents.begin(), parents.end()); + // Ingoing dependencies + std::vector ingoingDeps; + if (isBasicElement(index)) { + for(auto const& dep : getBasicElement(index)->ingoingDependencies()) { + ingoingDeps.push_back(dep->id()); + } + std::sort(ingoingDeps.begin(), ingoingDeps.end()); + } + // Outgoing dependencies + std::vector outgoingDeps; for(auto const& dep : getElement(index)->outgoingDependencies()) { - res.second.push_back(dep->id()); + outgoingDeps.push_back(dep->id()); } - std::sort(res.second.begin(), res.second.end()); - return res; + std::sort(outgoingDeps.begin(), outgoingDeps.end()); + return std::make_tuple(parents, ingoingDeps, outgoingDeps); } // Explicitly instantiate the class. diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h index 815bb0df5..304018d97 100644 --- a/src/storm-dft/storage/dft/DFT.h +++ b/src/storm-dft/storage/dft/DFT.h @@ -276,7 +276,7 @@ namespace storm { } private: - std::pair, std::vector> getSortedParentAndOutDepIds(size_t index) const; + std::tuple, std::vector, std::vector> getSortedParentAndDependencyIds(size_t index) const; bool elementIndicesCorrect() const { for(size_t i = 0; i < mElements.size(); ++i) { From 0a06a2b33e28a3d05f3fd06b32c6b5a897a351c7 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Sun, 12 Mar 2017 20:32:52 +0100 Subject: [PATCH 37/37] Fix in constructing pseudo state --- src/storm-dft/storage/dft/DFTState.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/storm-dft/storage/dft/DFTState.cpp b/src/storm-dft/storage/dft/DFTState.cpp index ec6509944..29c1e525f 100644 --- a/src/storm-dft/storage/dft/DFTState.cpp +++ b/src/storm-dft/storage/dft/DFTState.cpp @@ -41,9 +41,9 @@ namespace storm { // Initialize currently failable BE if (mDft.isBasicElement(index) && isOperational(index)) { std::shared_ptr> be = mDft.getBasicElement(index); - if ((!be->isColdBasicElement() && be->canFail()) || !mDft.hasRepresentant(index) || isActive(mDft.getRepresentant(index))) { + if (be->canFail() && (!be->isColdBasicElement() || !mDft.hasRepresentant(index) || isActive(mDft.getRepresentant(index)))) { mCurrentlyFailableBE.push_back(index); - STORM_LOG_TRACE("Currently failable: " << mDft.getBasicElement(index)->toString()); + STORM_LOG_TRACE("Currently failable: " << be->toString()); } } else if (mDft.getElement(index)->isSpareGate()) { // Initialize used representants @@ -257,7 +257,7 @@ namespace storm { // Consider "normal" failure STORM_LOG_ASSERT(index < nrFailableBEs(), "Index invalid."); std::pair const>,bool> res(mDft.getBasicElement(mCurrentlyFailableBE[index]), false); - STORM_LOG_ASSERT(res.first->canFail(), "Element cannot fail."); + STORM_LOG_ASSERT(res.first->canFail(), "Element " << *(res.first) << " cannot fail."); mCurrentlyFailableBE.erase(mCurrentlyFailableBE.begin() + index); setFailed(res.first->id()); return res;