modularisation on and and or

Former-commit-id: 50950ba497

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 <chrono>
+
+template<typename ValueType>
+class DFTAnalyser {
+    
+    std::chrono::duration<double> buildingTime = std::chrono::duration<double>::zero();
+    std::chrono::duration<double> explorationTime = std::chrono::duration<double>::zero();
+    std::chrono::duration<double> bisimulationTime = std::chrono::duration<double>::zero();
+    std::chrono::duration<double> modelCheckingTime = std::chrono::duration<double>::zero();
+    std::chrono::duration<double> totalTime = std::chrono::duration<double>::zero();
+    ValueType checkResult = storm::utility::zero<ValueType>();
+public:
+    void check(storm::storage::DFT<ValueType> dft , std::shared_ptr<const storm::logic::Formula> 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<storm::storage::DFT<ValueType>> dfts;
+        checkResult = checkHelper(dft, formula, symred, allowModularisation);
+        totalTime = std::chrono::high_resolution_clock::now() - totalStart;
+            
+        
+            
+    }
+    
+private:
+    ValueType checkHelper(storm::storage::DFT<ValueType> const& dft , std::shared_ptr<const storm::logic::Formula> const& formula, bool symred = true, bool allowModularisation = true)  {
+        std::cout << "check helper called" << std::endl;
+        bool invResults = false;
+        std::vector<storm::storage::DFT<ValueType>> dfts = {dft};
+        std::vector<ValueType> 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<storm::modelchecker::CheckResult> 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<ValueType>().getValueMap().begin()->second);
+            }
+        }
+        
+        ValueType result = storm::utility::one<ValueType>();
+        for(auto const& r : res) {
+            if(invResults) {
+                result *= storm::utility::one<ValueType>() - r;
+            } else {
+                result *= r;
+            }
+        }
+        if(invResults) {
+            return storm::utility::one<ValueType>() - result;
+        }
+        return result;
+    }
+    
+    
+    std::vector<std::shared_ptr<storm::models::sparse::Model<ValueType>>> buildMarkovModels(std::vector<storm::storage::DFT<ValueType>> const&  dfts,   std::shared_ptr<const storm::logic::Formula> const& formula, bool symred) {
+        std::vector<std::shared_ptr<storm::models::sparse::Model<ValueType>>> models;
+        for(auto& dft : dfts) {
+            std::chrono::high_resolution_clock::time_point buildingStart = std::chrono::high_resolution_clock::now();
+
+            std::map<size_t, std::vector<std::vector<size_t>>> 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<ValueType> builder(dft, symmetries);
+            typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
+            std::shared_ptr<storm::models::sparse::Model<ValueType>> 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<storm::models::sparse::Ctmc<ValueType>>(model->template as<storm::models::sparse::Ctmc<ValueType>>(), {formula}, storm::storage::BisimulationType::Weak)->template as<storm::models::sparse::Ctmc<ValueType>>();
+                //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;
+    }
+    
+};

src/storage/dft/DFT.cpp

@@ -247,6 +247,46 @@ namespace storm {
             return stateIndex;
         }
         
+        template<typename ValueType>
+        std::vector<DFT<ValueType>>  DFT<ValueType>::topModularisation() const {
+            assert(isGate(mTopLevelIndex));
+            auto const& children = getGate(mTopLevelIndex)->children();
+            std::map<size_t, std::vector<size_t>> subdfts;
+            for(auto const& child : children) {
+                std::vector<size_t> 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<DFT<ValueType>> res;
+            for(auto const& subdft : subdfts) {
+                DFTBuilder<ValueType> 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<typename ValueType>
         DFT<ValueType> DFT<ValueType>::optimize() const {
             std::vector<size_t> modIdea = findModularisationRewrite();

src/storage/dft/DFT.h

@@ -6,6 +6,7 @@
 #include <unordered_map>
 #include <list>
 #include <map>
+#include <vector>
 
 #include <boost/iterator/counting_iterator.hpp>
 
@@ -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<DFT<ValueType>> topModularisation() const;
+            
             bool isRepresentative(size_t id) const {
                 for (auto const& parent : getElement(id)->parents()) {
                     if (parent->isSpareGate()) {

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 <boost/lexical_cast.hpp>
 
 /*!
@@ -15,71 +11,20 @@
  * @param property PCTC formula capturing the property to check.
  */
 template <typename ValueType>
-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<ValueType> parser;
     storm::storage::DFT<ValueType> dft = parser.parseDFT(filename);
     std::vector<std::shared_ptr<storm::logic::Formula>> parsedFormulas = storm::parseFormulasForExplicit(property);
     std::vector<std::shared_ptr<const storm::logic::Formula>> formulas(parsedFormulas.begin(), parsedFormulas.end());
     assert(formulas.size() == 1);
     
-    // Optimizing DFT
-    dft = dft.optimize();
-    std::map<size_t, std::vector<std::vector<size_t>>> 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<ValueType> builder(dft, symmetries);
-    typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
-    std::shared_ptr<storm::models::sparse::Model<ValueType>> 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<storm::models::sparse::Ctmc<ValueType>>(model->template as<storm::models::sparse::Ctmc<ValueType>>(), formulas, storm::storage::BisimulationType::Weak)->template as<storm::models::sparse::Ctmc<ValueType>>();
-        //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<storm::modelchecker::CheckResult> 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<double> buildingTime = buildingEnd - buildingStart;
-    std::chrono::duration<double> explorationTime = explorationEnd - buildingEnd;
-    std::chrono::duration<double> bisimulationTime = bisimulationEnd - explorationEnd;
-    std::chrono::duration<double> modelCheckingTime = modelCheckingEnd - bisimulationEnd;
-    std::chrono::duration<double> 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<ValueType> 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<storm::RationalFunction>(filename, pctlFormula, symred);
+        analyzeDFT<storm::RationalFunction>(filename, pctlFormula, symred, allowModular && enableModularisation );
     } else {
-        analyzeDFT<double>(filename, pctlFormula, symred);
+        analyzeDFT<double>(filename, pctlFormula, symred, allowModular && enableModularisation);
     }
 }