some refactoring

Former-commit-id: 90be99f04d

src/builder/ExplicitDFTModelBuilder.cpp

@@ -56,7 +56,7 @@ namespace storm {
 
 
         template <typename ValueType>
-        std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilder<ValueType>::buildModel() {
+        std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilder<ValueType>::buildModel(LabelOptions const& labelOpts) {
             // Initialize
             DFTStatePointer state = std::make_shared<storm::storage::DFTState<ValueType>>(mDft, *mStateGenerationInfo, newIndex++);
             mStates.findOrAdd(state->status(), state);
@@ -89,25 +89,32 @@ namespace storm {
             modelComponents.stateLabeling.addLabel("init");
             modelComponents.stateLabeling.addLabelToState("init", 0);
             // Label all states corresponding to their status (failed, failsafe, failed BE)
+            if(labelOpts.buildFailLabel) {
                 modelComponents.stateLabeling.addLabel("failed");
+            } 
+            if(labelOpts.buildFailSafeLabel) {
                 modelComponents.stateLabeling.addLabel("failsafe");
+            }
+            
             // Collect labels for all BE
             std::vector<std::shared_ptr<storage::DFTBE<ValueType>>> basicElements = mDft.getBasicElements();
             for (std::shared_ptr<storage::DFTBE<ValueType>> elem : basicElements) {
+                if(labelOpts.beLabels.count(elem->name()) > 0) {
                     modelComponents.stateLabeling.addLabel(elem->name() + "_fail");
                 }
+            }
 
             for (auto const& stateVectorPair : mStates) {
                 DFTStatePointer state = stateVectorPair.second;
-                if (mDft.hasFailed(state)) {
+                if (labelOpts.buildFailLabel && mDft.hasFailed(state)) {
                     modelComponents.stateLabeling.addLabelToState("failed", state->getId());
                 }
-                if (mDft.isFailsafe(state)) {
+                if (labelOpts.buildFailSafeLabel && mDft.isFailsafe(state)) {
                     modelComponents.stateLabeling.addLabelToState("failsafe", state->getId());
                 };
                 // Set fail status for each BE
                 for (std::shared_ptr<storage::DFTBE<ValueType>> elem : basicElements) {
-                    if (state->hasFailed(elem->id())) {
+                    if (labelOpts.beLabels.count(elem->name()) > 0 && state->hasFailed(elem->id()) ) {
                         modelComponents.stateLabeling.addLabelToState(elem->name() + "_fail", state->getId());
                     }
                 }
@@ -129,7 +136,13 @@ namespace storm {
                 }
                 model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(std::move(rateMatrix), std::move(modelComponents.stateLabeling));
             } else {
-                model = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates), true);
+                std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates), true);
+                if (ma->hasOnlyTrivialNondeterminism()) {
+                 // Markov automaton can be converted into CTMC
+                    model = ma->convertToCTMC();
+                } else {
+                    model = ma;
+                }
             }
             
             model->printModelInformationToStream(std::cout);

src/builder/ExplicitDFTModelBuilder.h

@@ -44,15 +44,23 @@ namespace storm {
                 boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> choiceLabeling;
             };
 
+          
+            
             storm::storage::DFT<ValueType> const& mDft;
             std::shared_ptr<storm::storage::DFTStateGenerationInfo> mStateGenerationInfo;
             storm::storage::BitVectorHashMap<DFTStatePointer> mStates;
             size_t newIndex = 0;
 
         public:
+              struct LabelOptions {
+                bool buildFailLabel = true;
+                bool buildFailSafeLabel = false;
+                std::set<std::string> beLabels = {};
+            };
+            
             ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft);
 
-            std::shared_ptr<storm::models::sparse::Model<ValueType>> buildModel();
+            std::shared_ptr<storm::models::sparse::Model<ValueType>> buildModel(LabelOptions const& labelOpts);
 
         private:
             bool exploreStates(std::queue<DFTStatePointer>& stateQueue, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<uint_fast64_t>& markovianStates, std::vector<ValueType>& exitRates);

src/storm-dyftee.cpp

@@ -32,7 +32,8 @@ void analyzeDFT(std::string filename, std::string property, bool symred = false)
     // Building Markov Automaton
     std::cout << "Building Model..." << std::endl;
     storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft);
-    std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.buildModel();
+    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);
     std::cout << "Built Model" << std::endl;
 
     // Model checking

src/utility/storm.h

@@ -196,6 +196,15 @@ namespace storm {
     
     template<typename ModelType>
     std::shared_ptr<storm::models::ModelBase> preprocessModel(std::shared_ptr<storm::models::ModelBase> model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) {
+        if(model->getType() == storm::models::ModelType::MarkovAutomaton && model->isSparseModel()) {
+            std::shared_ptr<storm::models::sparse::MarkovAutomaton<typename ModelType::ValueType>> ma = model->template as<storm::models::sparse::MarkovAutomaton<typename ModelType::ValueType>>();
+            if (ma->hasOnlyTrivialNondeterminism()) {
+                // Markov automaton can be converted into CTMC
+                model = ma->convertToCTMC();
+                
+            } 
+        }
+        
         if (model->isSparseModel() && storm::settings::generalSettings().isBisimulationSet()) {
             storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong;
             if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) {
@@ -205,6 +214,7 @@ namespace storm {
             STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for sparse models.");
             return performBisimulationMinimization<ModelType>(model->template as<storm::models::sparse::Model<typename ModelType::ValueType>>(), formulas, bisimType);
         }
+        
         return model;
     }
     
@@ -302,15 +312,8 @@ namespace storm {
             result = modelchecker.check(task);
         } else if (model->getType() == storm::models::ModelType::MarkovAutomaton) {
             std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = model->template as<storm::models::sparse::MarkovAutomaton<ValueType>>();
-            if (ma->hasOnlyTrivialNondeterminism()) {
-                // Markov automaton can be converted into CTMC
-                std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> ctmc = ma->convertToCTMC();
-                storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<ValueType>> modelchecker(*ctmc);
-                result = modelchecker.check(task);
-            } else {
             storm::modelchecker::SparseMarkovAutomatonCslModelChecker<storm::models::sparse::MarkovAutomaton<ValueType>> modelchecker(*ma);
             result = modelchecker.check(task);
-            }
         } else {
             STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type " << model->getType() << " is not supported.");
         }