From 3f23d7b322029f350a89b471fa70f16c11d7e468 Mon Sep 17 00:00:00 2001
From: ThomasH <thomas.henn@rwth-aachen.de>
Date: Thu, 16 Jun 2016 17:54:04 +0200
Subject: [PATCH] add advanced state labeling (wrt a given formula)

Former-commit-id: 84e0ede9a06afb1399f3eed861c2469102656756
---
 src/builder/ExplicitGspnModelBuilder.cpp | 44 ++++++++++++++++++++++--
 src/builder/ExplicitGspnModelBuilder.h   |  4 ++-
 src/storm-gspn.cpp                       | 24 +++++++++++--
 3 files changed, 67 insertions(+), 5 deletions(-)

diff --git a/src/builder/ExplicitGspnModelBuilder.cpp b/src/builder/ExplicitGspnModelBuilder.cpp
index ddf7bf616..c3e5e15f9 100644
--- a/src/builder/ExplicitGspnModelBuilder.cpp
+++ b/src/builder/ExplicitGspnModelBuilder.cpp
@@ -4,12 +4,15 @@
 
 #include "src/utility/macros.h"
 #include "src/exceptions/NotImplementedException.h"
+#include "src/storage/expressions/ExpressionManager.h"
+#include "src/parser/FormulaParser.h"
+#include "src/storage/expressions/ExpressionEvaluator.h"
 
 namespace storm {
     namespace builder {
 
         template<typename ValueType>
-        storm::models::sparse::MarkovAutomaton<ValueType> ExplicitGspnModelBuilder<ValueType>::translateGspn(storm::gspn::GSPN const& gspn) {
+        storm::models::sparse::MarkovAutomaton<ValueType> ExplicitGspnModelBuilder<ValueType>::translateGspn(storm::gspn::GSPN const& gspn, std::string const& formula) {
             // set the given gspn and compute the limits of the net
             this->gspn = gspn;
             computeCapacities(gspn);
@@ -70,7 +73,44 @@ namespace storm {
             }
 
             auto matrix = builder.build();
-            auto labeling = getStateLabeling();
+
+            // create expression manager and add variables from the gspn
+            auto expressionManager = std::make_shared<storm::expressions::ExpressionManager>();
+            for (auto& place : gspn.getPlaces()) {
+                expressionManager->declareIntegerVariable(place.getName());
+            }
+
+            // parse formula
+            storm::parser::FormulaParser formulaParser(expressionManager);
+            auto formulaPtr = formulaParser.parseSingleFormulaFromString(formula);
+            auto atomicFormulas = formulaPtr->getAtomicExpressionFormulas();
+
+            // create empty state labeling
+            storm::models::sparse::StateLabeling labeling(markings.size());
+            storm::expressions::ExpressionEvaluator<double> expressionEvaluator(*expressionManager);
+
+            std::cout << std::endl;
+            std::cout << "build labeling:" << std::endl;
+            for (auto& atomicFormula : atomicFormulas) {
+                std::cout << atomicFormula;
+                auto label = atomicFormula->toString();
+                labeling.addLabel(label);
+
+                for (auto statePair : markings) {
+                    auto marking = storm::gspn::Marking(gspn.getNumberOfPlaces(), numberOfBits, statePair.first);
+                    for (auto& place : gspn.getPlaces()) {
+                        auto variable = expressionManager->getVariable(place.getName());
+                        expressionEvaluator.setIntegerValue(variable, marking.getNumberOfTokensAt(place.getID()));
+                    }
+                    bool hold = expressionEvaluator.asBool(atomicFormula->getExpression());
+                    if (hold) {
+                        labeling.addLabelToState(label, statePair.second);
+                    }
+                }
+
+            }
+
+            //auto labeling = getStateLabeling();
 
             return storm::models::sparse::MarkovAutomaton<double>(matrix, labeling, markovianStates, exitRates);
         }
diff --git a/src/builder/ExplicitGspnModelBuilder.h b/src/builder/ExplicitGspnModelBuilder.h
index fa8ed75be..05c95e087 100644
--- a/src/builder/ExplicitGspnModelBuilder.h
+++ b/src/builder/ExplicitGspnModelBuilder.h
@@ -1,6 +1,8 @@
 #ifndef STORM_BUILDER_EXPLICITGSPNMODELBUILDER_H_
 #define STORM_BUILDER_EXPLICITGSPNMODELBUILDER_H_
 
+#include <String>
+
 #include "src/models/sparse/MarkovAutomaton.h"
 #include "src/models/sparse/StandardRewardModel.h"
 #include "src/storage/Bitvector.h"
@@ -25,7 +27,7 @@ namespace storm {
              * @param gspn The gspn whose semantic is covered by the MarkovAutomaton
              * @return The resulting MarkovAutomaton
              */
-            storm::models::sparse::MarkovAutomaton<ValueType> translateGspn(storm::gspn::GSPN const& gspn);
+            storm::models::sparse::MarkovAutomaton<ValueType> translateGspn(storm::gspn::GSPN const& gspn, std::string const& formula);
         private:
 
             /*!
diff --git a/src/storm-gspn.cpp b/src/storm-gspn.cpp
index cc68438f9..706b9ce42 100644
--- a/src/storm-gspn.cpp
+++ b/src/storm-gspn.cpp
@@ -1,15 +1,18 @@
 #include <iostream>
+#include <src/builder/ExplicitGspnModelBuilder.h>
 #include "src/exceptions/BaseException.h"
 #include "src/parser/GspnParser.h"
 #include "src/storage/gspn/GSPN.h"
 #include "src/utility/macros.h"
 #include "src/utility/initialize.h"
+#include <fstream>
 
 int main(const int argc, const char** argv) {
-    if (argc != 2) {
+    if (argc != 3) {
         std::cout << "Error: incorrect number of parameters!" << std::endl << std::endl;
         std::cout << "Usage:" << std::endl;
-        std::cout << "storm-gspn <path to pnml file>" << std::endl;
+        std::cout << "storm-gspn <path to pnml file> <formular>" << std::endl;
+        return 1;
     }
 
     try {
@@ -18,9 +21,26 @@ int main(const int argc, const char** argv) {
         // Parse GSPN from xml
         auto parser = storm::parser::GspnParser();
         auto gspn = parser.parse(argv[1]);
+
+        //
+        //std::ofstream file;
+        //file.open("/Users/thomas/Desktop/storm.dot");
+        //gspn.writeDotToStream(file);
+        //file.close();
+
         std::cout << "Parsing complete!" << std::endl;
 
+
         // Construct MA
+        auto builder = storm::builder::ExplicitGspnModelBuilder<>();
+        auto ma = builder.translateGspn(gspn, argv[2]);
+        std::cout << "Markov Automaton: " << std::endl;
+        std::cout << "number of states: " << ma.getNumberOfStates() << std::endl;
+        std::cout << "number of transitions: " << ma.getNumberOfTransitions() << std::endl << std::endl;
+
+
+
+
 
         // All operations have now been performed, so we clean up everything and terminate.
         storm::utility::cleanUp();