From d5474722c0ed470dad3b5121c5339eb553d0dcad Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Thu, 17 Dec 2015 11:35:28 +0100
Subject: [PATCH] Label generation from FT

Former-commit-id: 111a02a1437345bffd42806fdf6be4d3e252b949
---
 src/builder/ExplicitDFTModelBuilder.cpp | 27 +++++++++++++++++++++----
 src/storage/dft/DFT.h                   | 13 +++++++++++-
 src/storage/dft/DFTState.h              | 11 ++++------
 src/storm-dyftee.cpp                    | 17 ++++++++++++----
 4 files changed, 52 insertions(+), 16 deletions(-)

diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp
index 6e938f289..bb4204918 100644
--- a/src/builder/ExplicitDFTModelBuilder.cpp
+++ b/src/builder/ExplicitDFTModelBuilder.cpp
@@ -33,18 +33,37 @@ namespace storm {
 
             // Build state labeling
             modelComponents.stateLabeling = storm::models::sparse::StateLabeling(mStates.size());
-            // Also label the initial state with the special label "init".
+            // Initial state is always first state without any failure
             modelComponents.stateLabeling.addLabel("init");
             modelComponents.stateLabeling.addLabelToState("init", 0);
-            // TODO Matthias: not fixed
+            // Label all states corresponding to their status (failed, failsafe, failed BE)
             modelComponents.stateLabeling.addLabel("failed");
-            modelComponents.stateLabeling.addLabelToState("failed", 7);
+            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) {
+                modelComponents.stateLabeling.addLabel(elem->name() + "_fail");
+            }
+
+            for (storm::storage::DFTState state : mStates) {
+                if (mDft.hasFailed(state)) {
+                    modelComponents.stateLabeling.addLabelToState("failed", state.getId());
+                }
+                if (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())) {
+                        modelComponents.stateLabeling.addLabelToState(elem->name() + "_fail", state.getId());
+                    }
+                }
+            }
 
             // TODO Matthias: initialize
             modelComponents.rewardModels;
             modelComponents.choiceLabeling;
 
-
             std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> model;
             model = std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>(new storm::models::sparse::Ctmc<ValueType, RewardModelType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling)));
             model->printModelInformationToStream(std::cout);
diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h
index df97df476..69a407461 100644
--- a/src/storage/dft/DFT.h
+++ b/src/storage/dft/DFT.h
@@ -136,7 +136,18 @@ namespace storm {
                 assert(mElements[index]->isBasicElement());
                 return std::static_pointer_cast<DFTBE<double>>(mElements[index]);
             }
-            
+
+            std::vector<std::shared_ptr<DFTBE<double>>> getBasicElements() const {
+                std::vector<std::shared_ptr<DFTBE<double>>> elements;
+                for (std::shared_ptr<storm::storage::DFTElement> elem : mElements) {
+                    if (elem->isBasicElement()) {
+                        elements.push_back(std::static_pointer_cast<DFTBE<double>>(elem));
+                    }
+                }
+                return elements;
+            }
+
+
             bool hasFailed(DFTState const& state) const {
                 return state.hasFailed(mTopLevelIndex);
             }
diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h
index 2085ba010..788162ce3 100644
--- a/src/storage/dft/DFTState.h
+++ b/src/storage/dft/DFTState.h
@@ -9,12 +9,11 @@
 namespace storm {
     namespace storage {
        
-        class DFT; 
-        template<typename T>
+        class DFT;
+        template<typename ValueType>
         class DFTBE;
-        
-        
-        
+
+
         class DFTState {
             friend struct std::hash<DFTState>;
         private:
@@ -97,8 +96,6 @@ namespace storm {
              */
             void setUsesAtPosition(size_t usageIndex, size_t child);
             
-            
-            
             bool claimNew(size_t spareId, size_t usageIndex, size_t currentlyUses, std::vector<size_t> const& childIds);
             
             bool hasOutgoingEdges() const {
diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp
index a5a4feb98..d24d2ad08 100644
--- a/src/storm-dyftee.cpp
+++ b/src/storm-dyftee.cpp
@@ -9,7 +9,7 @@
  * Entry point for the DyFTeE backend.
  */
 int main(int argc, char** argv) {
-    if(argc != 2) {
+    if(argc < 2) {
         std::cout <<  "Storm-DyFTeE should be called with a filename as argument." << std::endl;
     }
 
@@ -30,10 +30,19 @@ int main(int argc, char** argv) {
     std::cout << "Built CTMC" << std::endl;
 
     std::cout << "Model checking..." << std::endl;
-    //TODO Matthias: Construct formula, do not fix
-    std::vector<std::shared_ptr<storm::logic::Formula>> formulas = storm::parseFormulasForExplicit("Pmax=?[true U \"failed\"]");
+    // Construct PCTL forumla
+    std::string inputFormula;
+    if (argc < 3) {
+        // Set explicit reachability formula
+        inputFormula = "Pmax=?[true U \"failed\"]";
+    } else {
+        // Read formula from input
+        inputFormula = argv[2];
+    }
+    std::vector<std::shared_ptr<storm::logic::Formula>> formulas = storm::parseFormulasForExplicit(inputFormula);
     assert(formulas.size() == 1);
-    // Verify the model, if a formula was given.
+
+    // Verify the model
     std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, formulas[0]));
     assert(result);
     std::cout << "Result (initial states): ";