From 18383f5220dfb77bd615fd0cd6b3d2133ab9c1bc Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 14 Dec 2016 15:46:13 +0100 Subject: [PATCH] several fixes in dft->gspn->jani code path: Most notably, mas are closed, successor nodes failed places keep intact and tb property is added --- src/storm-dft-cli/storm-dyftee.cpp | 36 ++++++++++--------- .../DftToGspnTransformator.cpp | 14 +++++++- .../transformations/DftToGspnTransformator.h | 3 ++ src/storm-gspn-cli/storm-gspn.cpp | 4 +-- src/storm-gspn/builder/JaniGSPNBuilder.h | 16 ++++----- src/storm/utility/storm.h | 1 + 6 files changed, 45 insertions(+), 29 deletions(-) diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp index 8ccdc12be..6c54dc226 100644 --- a/src/storm-dft-cli/storm-dyftee.cpp +++ b/src/storm-dft-cli/storm-dyftee.cpp @@ -4,6 +4,7 @@ #include "storm/cli/cli.h" #include "storm/exceptions/BaseException.h" +#include "storm/logic/Formula.h" #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/CoreSettings.h" @@ -71,20 +72,6 @@ void analyzeWithSMT(std::string filename) { //std::cout << "SMT result: " << sat << std::endl; } -/*! - * Load DFT from filename and transform into a GSPN. - * - * @param filename Path to DFT file in Galileo format. - * - */ -template -storm::gspn::GSPN* transformDFT(std::string filename) { - storm::parser::DFTGalileoParser parser; - storm::storage::DFT dft = parser.parseDFT(filename); - storm::transformations::dft::DftToGspnTransformator gspnTransformator(dft); - gspnTransformator.transform(); - return gspnTransformator.obtainGSPN(); -} /*! * Initialize the settings manager. @@ -140,15 +127,30 @@ int main(const int argc, const char** argv) { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); } + if (dftSettings.isTransformToGspn()) { - storm::gspn::GSPN* gspn = transformDFT(dftSettings.getDftFilename()); + + storm::parser::DFTGalileoParser parser; + storm::storage::DFT dft = parser.parseDFT(dftSettings.getDftFilename()); + storm::transformations::dft::DftToGspnTransformator gspnTransformator(dft); + gspnTransformator.transform(); + storm::gspn::GSPN* gspn = gspnTransformator.obtainGSPN(); + uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId(); storm::handleGSPNExportSettings(*gspn); - storm::jani::Model* model = storm::buildJani(*gspn); + std::shared_ptr exprManager(new storm::expressions::ExpressionManager()); + storm::builder::JaniGSPNBuilder builder(*gspn, exprManager); + storm::jani::Model* model = builder.build(); + storm::jani::Variable const& topfailedVar = builder.getPlaceVariable(toplevelFailedPlace); + + + auto evtlFormula = std::make_shared(exprManager->integer(1) == topfailedVar.getExpressionVariable().getExpression()); + auto tbFormula = std::make_shared(std::make_shared(true), evtlFormula, 0.0, 10.0); + auto tbUntil = std::make_shared(tbFormula); storm::settings::modules::JaniExportSettings const& janiSettings = storm::settings::getModule(); if (janiSettings.isJaniFileSet()) { - storm::exportJaniModel(*model, {}, janiSettings.getJaniFilename()); + storm::exportJaniModel(*model, {storm::jani::Property("time-bounded", tbUntil)}, janiSettings.getJaniFilename()); } delete model; diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp index 5649754cd..355c6f440 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.cpp +++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp @@ -8,7 +8,7 @@ namespace storm { // Prevent some magic constants static constexpr const uint64_t defaultPriority = 0; - static constexpr const uint64_t defaultCapacity = 0; + static constexpr const uint64_t defaultCapacity = 1; template DftToGspnTransformator::DftToGspnTransformator(storm::storage::DFT const& dft) : mDft(dft) { @@ -27,6 +27,12 @@ namespace storm { //drawGSPNRestrictions(); } + template + uint64_t DftToGspnTransformator::toplevelFailedPlaceId() { + assert(failedNodes.size() > mDft.getTopLevelIndex()); + return failedNodes[mDft.getTopLevelIndex()]; + } + template void DftToGspnTransformator::drawGSPNElements() { @@ -133,6 +139,7 @@ namespace storm { for(auto const& child : dftAnd->children()) { assert(failedNodes.size() > child->id()); builder.addInputArc(failedNodes[child->id()], tAndFailed); + builder.addOutputArc(tAndFailed, failedNodes[child->id()]); } } @@ -157,6 +164,7 @@ namespace storm { } assert(failedNodes.size() > child->id()); builder.addInputArc(failedNodes[child->id()], tNodeFailed); + builder.addOutputArc(tNodeFailed, failedNodes[child->id()]); ++i; } } @@ -188,6 +196,7 @@ namespace storm { builder.addOutputArc(tCollect, childInhibPlace); builder.addInhibitionArc(childInhibPlace, tCollect); builder.addInputArc(failedNodes[child->id()], tCollect); + builder.addOutputArc(tCollect, failedNodes[child->id()]); ++i; } } @@ -212,12 +221,15 @@ namespace storm { } for(auto const& child : dftPand->children()) { builder.addInputArc(failedNodes[child->id()], tNodeFailed); + builder.addOutputArc(tNodeFailed, failedNodes[child->id()]); } for (uint64_t j = 1; j < dftPand->nrChildren(); ++j) { uint64_t tfs = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILSAVING + std::to_string(j)); builder.addInputArc(failedNodes[dftPand->children().at(j)->id()], tfs); + builder.addOutputArc(tfs, failedNodes[dftPand->children().at(j)->id()]); builder.addInhibitionArc(failedNodes[dftPand->children().at(j-1)->id()], tfs); builder.addOutputArc(tfs, nodeFS); + builder.addInhibitionArc(nodeFS, tfs); } } diff --git a/src/storm-dft/transformations/DftToGspnTransformator.h b/src/storm-dft/transformations/DftToGspnTransformator.h index e2812f738..2d763452d 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.h +++ b/src/storm-dft/transformations/DftToGspnTransformator.h @@ -33,6 +33,9 @@ namespace storm { */ gspn::GSPN* obtainGSPN(); + + uint64_t toplevelFailedPlaceId(); + private: /* * Draw all elements of the GSPN. diff --git a/src/storm-gspn-cli/storm-gspn.cpp b/src/storm-gspn-cli/storm-gspn.cpp index b973d046d..17b45222d 100644 --- a/src/storm-gspn-cli/storm-gspn.cpp +++ b/src/storm-gspn-cli/storm-gspn.cpp @@ -66,9 +66,7 @@ std::unordered_map parseCapacitiesList(std::string const& } void handleJani(storm::gspn::GSPN const& gspn) { - std::shared_ptr exprManager(new storm::expressions::ExpressionManager()); - storm::builder::JaniGSPNBuilder builder(gspn, exprManager); - storm::jani::Model* model = builder.build(); + storm::jani::JsonExporter::toFile(*model, {}, storm::settings::getModule().getJaniFilename()); delete model; } diff --git a/src/storm-gspn/builder/JaniGSPNBuilder.h b/src/storm-gspn/builder/JaniGSPNBuilder.h index 305fa0129..196d29562 100644 --- a/src/storm-gspn/builder/JaniGSPNBuilder.h +++ b/src/storm-gspn/builder/JaniGSPNBuilder.h @@ -16,10 +16,6 @@ namespace storm { } - void setIgnoreWeights(bool ignore = true) { - //ignoreWeights = ignore; - } - storm::jani::Model* build() { storm::jani::Model* model = new storm::jani::Model(gspn.getName(), storm::jani::ModelType::MA, janiVersion, expressionManager); @@ -32,6 +28,10 @@ namespace storm { return model; } + storm::jani::Variable const& getPlaceVariable(uint64_t placeId) { + return *vars.at(placeId); + } + void addVariables(storm::jani::Model* model) { for (auto const& place : gspn.getPlaces()) { storm::jani::Variable* janiVar = nullptr; @@ -86,7 +86,7 @@ namespace storm { destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() >= inPlaceEntry.second); } for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) { - destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() >= inhibPlaceEntry.second); + destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() < inhibPlaceEntry.second); } totalWeight = totalWeight + storm::expressions::ite(destguard, expressionManager->rational(trans.getWeight()), expressionManager->rational(0.0)); @@ -103,13 +103,13 @@ namespace storm { storm::expressions::Expression destguard = expressionManager->boolean(true); std::vector assignments; for (auto const& inPlaceEntry : trans.getInputPlaces()) { - destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() > inPlaceEntry.second); + destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() >= inPlaceEntry.second); if (trans.getOutputPlaces().count(inPlaceEntry.first) == 0) { assignments.emplace_back( *vars[inPlaceEntry.first], (vars[inPlaceEntry.first])->getExpressionVariable() - inPlaceEntry.second); } } for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) { - destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() > inhibPlaceEntry.second); + destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() < inhibPlaceEntry.second); } for (auto const& outputPlaceEntry : trans.getOutputPlaces()) { if (trans.getInputPlaces().count(outputPlaceEntry.first) == 0) { @@ -140,7 +140,7 @@ namespace storm { } } for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) { - guard = guard && (vars[inhibPlaceEntry.first]->getExpressionVariable() >= inhibPlaceEntry.second); + guard = guard && (vars[inhibPlaceEntry.first]->getExpressionVariable() < inhibPlaceEntry.second); } for (auto const& outputPlaceEntry : trans.getOutputPlaces()) { if (trans.getInputPlaces().count(outputPlaceEntry.first) == 0) { diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index 6657a7d6d..343832e00 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -227,6 +227,7 @@ namespace storm { std::shared_ptr preprocessModel(std::shared_ptr model, std::vector> const& formulas) { if (model->getType() == storm::models::ModelType::MarkovAutomaton && model->isSparseModel()) { std::shared_ptr> ma = model->template as>(); + ma->close(); if (ma->hasOnlyTrivialNondeterminism()) { // Markov automaton can be converted into CTMC. model = ma->convertToCTMC();