1st try on CTMC model checking

Former-commit-id: 5520801c2d

src/builder/ExplicitDFTModelBuilder.cpp

@@ -1,10 +1,16 @@
 #include "src/builder/ExplicitDFTModelBuilder.h"
+#include <src/models/sparse/Ctmc.h>
 
 namespace storm {
     namespace builder {
 
+        template <typename ValueType, typename RewardModelType, typename IndexType>
+        ExplicitDFTModelBuilder<ValueType, RewardModelType, IndexType>::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), rewardModels(), choiceLabeling() {
+            // Intentionally left empty.
+        }
+
         template<typename ValueType, typename RewardModelType, typename IndexType>
-        void ExplicitDFTModelBuilder<ValueType, RewardModelType, IndexType>::buildCTMC() {
+        std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> ExplicitDFTModelBuilder<ValueType, RewardModelType, IndexType>::buildCTMC() {
             // Initialize
             storm::storage::DFTState state(mDft, newIndex++);
             mStates.insert(state);
@@ -20,9 +26,29 @@ namespace storm {
             STORM_LOG_DEBUG("Generated " << mStates.size() << " states");
 
             // Build CTMC
-            transitionMatrix = transitionMatrixBuilder.build();
-            STORM_LOG_DEBUG("TransitionMatrix: " << std::endl << transitionMatrix);
-            // TODO Matthias: build CTMC
+            ModelComponents modelComponents;
+            // Build transition matrix
+            modelComponents.transitionMatrix = transitionMatrixBuilder.build();
+            STORM_LOG_DEBUG("TransitionMatrix: " << std::endl << modelComponents.transitionMatrix);
+
+            // Build state labeling
+            modelComponents.stateLabeling = storm::models::sparse::StateLabeling(mStates.size());
+            // Also label the initial state with the special label "init".
+            modelComponents.stateLabeling.addLabel("init");
+            modelComponents.stateLabeling.addLabelToState("init", 0);
+            // TODO Matthias: not fixed
+            modelComponents.stateLabeling.addLabel("failed");
+            modelComponents.stateLabeling.addLabelToState("failed", 7);
+
+            // 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);
+            return model;
         }
 
         template<typename ValueType, typename RewardModelType, typename IndexType>

src/builder/ExplicitDFTModelBuilder.h

@@ -5,6 +5,7 @@
 
 #include <src/models/sparse/StateLabeling.h>
 #include <src/models/sparse/StandardRewardModel.h>
+#include <src/models/sparse/Model.h>
 #include <src/storage/SparseMatrix.h>
 #include <boost/container/flat_set.hpp>
 #include <boost/optional/optional.hpp>
@@ -16,25 +17,34 @@ namespace storm {
 
         template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename IndexType = uint32_t>
         class ExplicitDFTModelBuilder {
-            storm::storage::DFT const &mDft;
-            std::unordered_set<storm::storage::DFTState> mStates;
-            size_t newIndex = 0;
 
-            // The transition matrix.
-            storm::storage::SparseMatrix<ValueType> transitionMatrix;
+            // A structure holding the individual components of a model.
+            struct ModelComponents {
+                ModelComponents();
+
+                // The transition matrix.
+                storm::storage::SparseMatrix<ValueType> transitionMatrix;
+
+                // The state labeling.
+                storm::models::sparse::StateLabeling stateLabeling;
 
-            // The state labeling.
-            storm::models::sparse::StateLabeling stateLabeling;
+                // The reward models associated with the model.
+                std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<typename RewardModelType::ValueType>> rewardModels;
 
-            // A vector that stores a labeling for each choice.
-            boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> choiceLabeling;
+                // A vector that stores a labeling for each choice.
+                boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> choiceLabeling;
+            };
+
+            storm::storage::DFT const &mDft;
+            std::unordered_set<storm::storage::DFTState> mStates;
+            size_t newIndex = 0;
 
         public:
             ExplicitDFTModelBuilder(storm::storage::DFT const &dft) : mDft(dft) {
 
             }
 
-            void buildCTMC();
+            std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> buildCTMC();
 
         private:
             void exploreStates(std::queue<storm::storage::DFTState>& stateQueue, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder);

src/storm-dyftee.cpp

@@ -1,7 +1,9 @@
+#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"
 
 /*
  * Entry point for the DyFTeE backend.
@@ -24,10 +26,19 @@ int main(int argc, char** argv) {
 
     std::cout << "Building CTMC..." << std::endl;
     storm::builder::ExplicitDFTModelBuilder<double> builder(dft);
-    builder.buildCTMC();
+    std::shared_ptr<storm::models::sparse::Model<double>> model = builder.buildCTMC();
     std::cout << "Built CTMC" << std::endl;
 
     std::cout << "Model checking..." << std::endl;
-    //TODO Matthias: check CTMC
+    //TODO Matthias: Construct formula, do not fix
+    std::vector<std::shared_ptr<storm::logic::Formula>> formulas = storm::parseFormulasForExplicit("Pmax=?[true U \"failed\"]");
+    assert(formulas.size() == 1);
+    // Verify the model, if a formula was given.
+    std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, formulas[0]));
+    assert(result);
+    std::cout << "Result (initial states): ";
+    result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
+    std::cout << *result << std::endl;
+
     std::cout << "Checked model" << std::endl;
 }