From 9ae9700d5c9f4dbb5e1073b27f9bc1f712c60a04 Mon Sep 17 00:00:00 2001 From: sjunges Date: Sat, 12 Mar 2016 20:43:37 +0100 Subject: [PATCH] modularisation on and and or Former-commit-id: 50950ba49767282d35ac4b7dba78dc9c98af5f2b --- src/modelchecker/DFTAnalyser.h | 158 +++++++++++++++++++++++++++++++++ src/storage/dft/DFT.cpp | 40 +++++++++ src/storage/dft/DFT.h | 7 ++ src/storm-dyftee.cpp | 76 +++------------- 4 files changed, 218 insertions(+), 63 deletions(-) create mode 100644 src/modelchecker/DFTAnalyser.h diff --git a/src/modelchecker/DFTAnalyser.h b/src/modelchecker/DFTAnalyser.h new file mode 100644 index 000000000..93bc7c7b1 --- /dev/null +++ b/src/modelchecker/DFTAnalyser.h @@ -0,0 +1,158 @@ +#pragma once + +#include "logic/Formula.h" +#include "parser/DFTGalileoParser.h" +#include "builder/ExplicitDFTModelBuilder.h" +#include "modelchecker/results/CheckResult.h" +#include "utility/storm.h" +#include "storage/dft/DFTIsomorphism.h" + + +#include + +template +class DFTAnalyser { + + std::chrono::duration buildingTime = std::chrono::duration::zero(); + std::chrono::duration explorationTime = std::chrono::duration::zero(); + std::chrono::duration bisimulationTime = std::chrono::duration::zero(); + std::chrono::duration modelCheckingTime = std::chrono::duration::zero(); + std::chrono::duration totalTime = std::chrono::duration::zero(); + ValueType checkResult = storm::utility::zero(); +public: + void check(storm::storage::DFT dft , std::shared_ptr const& formula, bool symred = true, bool allowModularisation = true) { + + // Building DFT + std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now(); + + + // Optimizing DFT + dft = dft.optimize(); + std::vector> dfts; + checkResult = checkHelper(dft, formula, symred, allowModularisation); + totalTime = std::chrono::high_resolution_clock::now() - totalStart; + + + + } + +private: + ValueType checkHelper(storm::storage::DFT const& dft , std::shared_ptr const& formula, bool symred = true, bool allowModularisation = true) { + std::cout << "check helper called" << std::endl; + bool invResults = false; + std::vector> dfts = {dft}; + std::vector res; + + if(allowModularisation) { + std::cout << dft.topLevelType() << std::endl; + if(dft.topLevelType() == storm::storage::DFTElementType::AND) { + std::cout << "top modularisation called AND" << std::endl; + dfts = dft.topModularisation(); + if(dfts.size() > 1) { + for(auto const ft : dfts) { + res.push_back(checkHelper(ft, formula, symred, allowModularisation)); + } + } + } + if(dft.topLevelType() == storm::storage::DFTElementType::OR) { + std::cout << "top modularisation called OR" << std::endl; + dfts = dft.topModularisation(); + if(dfts.size() > 1) { + for(auto const ft : dfts) { + res.push_back(checkHelper(ft, formula, symred, allowModularisation)); + } + } + invResults = true; + } + } + if(res.empty()) { + // Model based modularisation. + auto const& models = buildMarkovModels(dfts, formula, symred); + + + for (auto const& model : models) { + // Model checking + std::cout << "Model checking..." << std::endl; + std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now(); + std::unique_ptr result(storm::verifySparseModel(model, formula)); + std::cout << "done." << std::endl; + assert(result); + result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); + modelCheckingTime += std::chrono::high_resolution_clock::now() - modelCheckingStart; + res.push_back(result->asExplicitQuantitativeCheckResult().getValueMap().begin()->second); + } + } + + ValueType result = storm::utility::one(); + for(auto const& r : res) { + if(invResults) { + result *= storm::utility::one() - r; + } else { + result *= r; + } + } + if(invResults) { + return storm::utility::one() - result; + } + return result; + } + + + std::vector>> buildMarkovModels(std::vector> const& dfts, std::shared_ptr const& formula, bool symred) { + std::vector>> models; + for(auto& dft : dfts) { + std::chrono::high_resolution_clock::time_point buildingStart = std::chrono::high_resolution_clock::now(); + + std::map>> emptySymmetry; + storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); + if(symred) { + auto colouring = dft.colourDFT(); + symmetries = dft.findSymmetries(colouring); + std::cout << "Found " << symmetries.groups.size() << " symmetries." << std::endl; + STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries); + } + std::chrono::high_resolution_clock::time_point buildingEnd = std::chrono::high_resolution_clock::now(); + buildingTime += buildingEnd - buildingStart; + + // Building Markov Automaton + std::cout << "Building Model..." << std::endl; + storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries); + typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions; // TODO initialize this with the formula + std::shared_ptr> model = builder.buildModel(labeloptions); + //model->printModelInformationToStream(std::cout); + std::cout << "No. states (Explored): " << model->getNumberOfStates() << std::endl; + std::cout << "No. transitions (Explored): " << model->getNumberOfTransitions() << std::endl; + std::chrono::high_resolution_clock::time_point explorationEnd = std::chrono::high_resolution_clock::now(); + explorationTime += explorationEnd -buildingEnd; + + // Bisimulation + if (model->isOfType(storm::models::ModelType::Ctmc)) { + std::cout << "Bisimulation..." << std::endl; + model = storm::performDeterministicSparseBisimulationMinimization>(model->template as>(), {formula}, storm::storage::BisimulationType::Weak)->template as>(); + //model->printModelInformationToStream(std::cout); + } + std::cout << "No. states (Bisimulation): " << model->getNumberOfStates() << std::endl; + std::cout << "No. transitions (Bisimulation): " << model->getNumberOfTransitions() << std::endl; + bisimulationTime += std::chrono::high_resolution_clock::now() - explorationEnd; + models.push_back(model); + } + return models; + } + +public: + void printTimings(std::ostream& os = std::cout) { + os << "Times:" << std::endl; + os << "Building:\t" << buildingTime.count() << std::endl; + os << "Exploration:\t" << explorationTime.count() << std::endl; + os << "Bisimulation:\t" << bisimulationTime.count() << std::endl; + os << "Modelchecking:\t" << modelCheckingTime.count() << std::endl; + os << "Total:\t\t" << totalTime.count() << std::endl; + } + + void printResult(std::ostream& os = std::cout) { + + os << "Result: ["; + os << checkResult << "]" << std::endl; + } + +}; diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index dd771f230..482e8203c 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -247,6 +247,46 @@ namespace storm { return stateIndex; } + template + std::vector> DFT::topModularisation() const { + assert(isGate(mTopLevelIndex)); + auto const& children = getGate(mTopLevelIndex)->children(); + std::map> subdfts; + for(auto const& child : children) { + std::vector isubdft; + if(child->nrParents() > 1 || child->hasOutgoingDependencies()) { + return {*this}; + } + if (isGate(child->id())) { + isubdft = getGate(child->id())->independentSubDft(false); + } else { + assert(isBasicElement(child->id())); + if(!getBasicElement(child->id())->hasIngoingDependencies()) { + isubdft = {child->id()}; + } + + } + if(isubdft.empty()) { + return {*this}; + } else { + subdfts[child->id()] = isubdft; + } + } + + std::vector> res; + for(auto const& subdft : subdfts) { + DFTBuilder builder; + + for(size_t id : subdft.second) { + builder.copyElement(mElements[id]); + } + builder.setTopLevel(mElements[subdft.first]->name()); + res.push_back(builder.build()); + } + return res; + + } + template DFT DFT::optimize() const { std::vector modIdea = findModularisationRewrite(); diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h index f28d244f0..0f4832fb5 100644 --- a/src/storage/dft/DFT.h +++ b/src/storage/dft/DFT.h @@ -6,6 +6,7 @@ #include #include #include +#include #include @@ -95,6 +96,10 @@ namespace storm { return mTopLevelIndex; } + DFTElementType topLevelType() const { + return mElements[getTopLevelIndex()]->type(); + } + size_t getMaxSpareChildCount() const { return mMaxSpareChildCount; } @@ -187,6 +192,8 @@ namespace storm { return elements; } + std::vector> topModularisation() const; + bool isRepresentative(size_t id) const { for (auto const& parent : getElement(id)->parents()) { if (parent->isSpareGate()) { diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index 1f170072b..f280bbebf 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -1,11 +1,7 @@ #include "logic/Formula.h" -#include "parser/DFTGalileoParser.h" #include "utility/initialize.h" -#include "builder/ExplicitDFTModelBuilder.h" -#include "modelchecker/results/CheckResult.h" #include "utility/storm.h" -#include "storage/dft/DFTIsomorphism.h" - +#include "modelchecker/DFTAnalyser.h" #include /*! @@ -15,71 +11,20 @@ * @param property PCTC formula capturing the property to check. */ template -void analyzeDFT(std::string filename, std::string property, bool symred = false) { +void analyzeDFT(std::string filename, std::string property, bool symred = false, bool allowModularisation = false) { storm::settings::SettingsManager& manager = storm::settings::mutableManager(); manager.setFromString(""); - // Building DFT - std::chrono::high_resolution_clock::time_point buildingStart = std::chrono::high_resolution_clock::now(); storm::parser::DFTGalileoParser parser; storm::storage::DFT dft = parser.parseDFT(filename); std::vector> parsedFormulas = storm::parseFormulasForExplicit(property); std::vector> formulas(parsedFormulas.begin(), parsedFormulas.end()); assert(formulas.size() == 1); - // Optimizing DFT - dft = dft.optimize(); - std::map>> emptySymmetry; - storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); - if(symred) { - auto colouring = dft.colourDFT(); - symmetries = dft.findSymmetries(colouring); - std::cout << "Found " << symmetries.groups.size() << " symmetries." << std::endl; - STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries); - } - std::chrono::high_resolution_clock::time_point buildingEnd = std::chrono::high_resolution_clock::now(); - - // Building Markov Automaton - std::cout << "Building Model..." << std::endl; - storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries); - typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions; // TODO initialize this with the formula - std::shared_ptr> model = builder.buildModel(labeloptions); - //model->printModelInformationToStream(std::cout); - std::cout << "No. states (Explored): " << model->getNumberOfStates() << std::endl; - std::cout << "No. transitions (Explored): " << model->getNumberOfTransitions() << std::endl; - std::chrono::high_resolution_clock::time_point explorationEnd = std::chrono::high_resolution_clock::now(); - - // Bisimulation - if (model->isOfType(storm::models::ModelType::Ctmc)) { - std::cout << "Bisimulation..." << std::endl; - model = storm::performDeterministicSparseBisimulationMinimization>(model->template as>(), formulas, storm::storage::BisimulationType::Weak)->template as>(); - //model->printModelInformationToStream(std::cout); - } - std::cout << "No. states (Bisimulation): " << model->getNumberOfStates() << std::endl; - std::cout << "No. transitions (Bisimulation): " << model->getNumberOfTransitions() << std::endl; - std::chrono::high_resolution_clock::time_point bisimulationEnd = std::chrono::high_resolution_clock::now(); - - // Model checking - std::cout << "Model checking..." << std::endl; - std::unique_ptr result(storm::verifySparseModel(model, formulas[0])); - assert(result); - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); - - // Times - std::chrono::high_resolution_clock::time_point modelCheckingEnd = std::chrono::high_resolution_clock::now(); - std::chrono::duration buildingTime = buildingEnd - buildingStart; - std::chrono::duration explorationTime = explorationEnd - buildingEnd; - std::chrono::duration bisimulationTime = bisimulationEnd - explorationEnd; - std::chrono::duration modelCheckingTime = modelCheckingEnd - bisimulationEnd; - std::chrono::duration totalTime = modelCheckingEnd - buildingStart; - std::cout << "Times:" << std::endl; - std::cout << "Building:\t" << buildingTime.count() << std::endl; - std::cout << "Exploration:\t" << explorationTime.count() << std::endl; - std::cout << "Bisimulation:\t" << bisimulationTime.count() << std::endl; - std::cout << "Modelchecking:\t" << modelCheckingTime.count() << std::endl; - std::cout << "Total:\t\t" << totalTime.count() << std::endl; - std::cout << "Result: "; - std::cout << *result << std::endl; + DFTAnalyser analyser; + analyser.check(dft, formulas[0], symred, allowModularisation); + analyser.printTimings(); + analyser.printResult(); } /*! @@ -100,6 +45,8 @@ int main(int argc, char** argv) { bool parametric = false; bool symred = false; bool minimal = true; + bool allowModular = true; + bool enableModularisation = false; std::string filename = argv[1]; std::string operatorType = ""; std::string targetFormula = ""; @@ -112,6 +59,7 @@ int main(int argc, char** argv) { assert(targetFormula.empty()); operatorType = "ET"; targetFormula = "F \"failed\""; + allowModular = false; } else if (option == "--probability") { assert(targetFormula.empty()); operatorType = "P";; @@ -142,6 +90,8 @@ int main(int argc, char** argv) { pctlFormula = argv[i]; } else if (option == "--symred") { symred = true; + } else if (option == "--modularisation") { + enableModularisation = true; } else if (option == "--min") { minimal = true; } else if (option == "--max") { @@ -164,8 +114,8 @@ int main(int argc, char** argv) { std::cout << "Running " << (parametric ? "parametric " : "") << "DFT analysis on file " << filename << " with property " << pctlFormula << std::endl; if (parametric) { - analyzeDFT(filename, pctlFormula, symred); + analyzeDFT(filename, pctlFormula, symred, allowModular && enableModularisation ); } else { - analyzeDFT(filename, pctlFormula, symred); + analyzeDFT(filename, pctlFormula, symred, allowModular && enableModularisation); } }