properties in storm-gspn

src/storm-gspn-cli/storm-gspn.cpp

@@ -14,6 +14,8 @@
 #include "utility/storm.h"
 #include "storm/cli/cli.h"
 
+#include "storm/parser/FormulaParser.h"
+
 #include "storm/storage/expressions/ExpressionManager.h"
 #include "storm/storage/jani/Model.h"
 #include "storm/storage/jani/JSONExporter.h"
@@ -33,6 +35,7 @@
 #include "storm/settings/modules/JaniExportSettings.h"
 #include "storm/settings/modules/ResourceSettings.h"
 
+
 /*!
  * Initialize the settings manager.
  */
@@ -88,6 +91,14 @@ int main(const int argc, const char **argv) {
         auto parser = storm::parser::GspnParser();
         auto gspn = parser.parse(storm::settings::getModule<storm::settings::modules::GSPNSettings>().getGspnFilename());
 
+        std::string formulaString = "";
+        if (!storm::settings::getModule<storm::settings::modules::GeneralSettings>().isPropertySet()) {
+            formulaString = storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty();
+        }
+        boost::optional<std::set<std::string>> propertyFilter;
+        storm::parser::FormulaParser formulaParser(gspn->getExpressionManager());
+        std::vector<storm::jani::Property> properties  = storm::parseProperties(formulaParser, formulaString, propertyFilter);
+
         if (!gspn->isValid()) {
             STORM_LOG_ERROR("The gspn is not valid.");
         }
@@ -101,7 +112,7 @@ int main(const int argc, const char **argv) {
         
         if(storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isJaniFileSet()) {
             storm::jani::Model* model = storm::buildJani(*gspn);
-            storm::exportJaniModel(*model, {}, storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename());
+            storm::exportJaniModel(*model, properties, storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename());
             delete model;
         }
 

src/storm-gspn/builder/JaniGSPNBuilder.cpp

@@ -19,10 +19,10 @@ namespace storm {
                 storm::jani::Variable* janiVar = nullptr;
                 if (!place.hasRestrictedCapacity()) {
                     // Effectively no capacity limit known
-                    janiVar = new storm::jani::UnboundedIntegerVariable(place.getName(), expressionManager->declareIntegerVariable(place.getName()), expressionManager->integer(place.getNumberOfInitialTokens()));
+                    janiVar = new storm::jani::UnboundedIntegerVariable(place.getName(), expressionManager->getVariable(place.getName()), expressionManager->integer(place.getNumberOfInitialTokens()));
                 } else {
                     assert(place.hasRestrictedCapacity());
-                    janiVar = new storm::jani::BoundedIntegerVariable(place.getName(), expressionManager->declareIntegerVariable(place.getName()), expressionManager->integer(place.getNumberOfInitialTokens()), expressionManager->integer(0), expressionManager->integer(place.getCapacity()));
+                    janiVar = new storm::jani::BoundedIntegerVariable(place.getName(), expressionManager->getVariable(place.getName()), expressionManager->integer(place.getNumberOfInitialTokens()), expressionManager->integer(0), expressionManager->integer(place.getCapacity()));
                 }
                 assert(janiVar != nullptr);
                 assert(vars.count(place.getID()) == 0);

src/storm-gspn/builder/JaniGSPNBuilder.h

@@ -2,14 +2,15 @@
 
 #include "storm-gspn/storage/gspn/GSPN.h"
 #include "storm/storage/jani/Model.h"
+#include "storm/storage/jani/Property.h"
 #include "storm/storage/expressions/ExpressionManager.h"
 
 namespace storm {
     namespace builder {
         class JaniGSPNBuilder {
         public:
-            JaniGSPNBuilder(storm::gspn::GSPN const& gspn, std::shared_ptr<storm::expressions::ExpressionManager> const& expManager)
-                    : gspn(gspn), expressionManager(expManager) {
+            JaniGSPNBuilder(storm::gspn::GSPN const& gspn)
+                    : gspn(gspn), expressionManager(gspn.getExpressionManager()) {
                 
             }
             
@@ -26,8 +27,6 @@ namespace storm {
 
             
         private:
-
-
             void addVariables(storm::jani::Model* model);
 
             uint64_t addLocation(storm::jani::Automaton& automaton);

src/storm-gspn/storage/gspn/GSPN.cpp

@@ -28,7 +28,7 @@ namespace storm {
         }
         
         GSPN::GSPN(std::string const& name, std::vector<Place> const& places, std::vector<ImmediateTransition<WeightType>> const& itransitions, std::vector<TimedTransition<RateType>> const& ttransitions, std::vector<TransitionPartition> const& partitions, std::shared_ptr<storm::expressions::ExpressionManager> const& exprManager)
-        : name(name), places(places), immediateTransitions(itransitions), timedTransitions(ttransitions), partitions(partitions), exprManager(exprManager);
+        : name(name), places(places), immediateTransitions(itransitions), timedTransitions(ttransitions), partitions(partitions), exprManager(exprManager)
         {
             
         }
@@ -136,7 +136,7 @@ namespace storm {
         }
 
 
-    std::shared_ptr<storm::expressions::ExpressionManager> const& GSPN::getExpressionManager() {
+    std::shared_ptr<storm::expressions::ExpressionManager> const& GSPN::getExpressionManager() const {
         return exprManager;
     }
 

src/storm-gspn/storage/gspn/GspnBuilder.cpp

@@ -4,7 +4,6 @@
 #include "storm/exceptions/IllegalFunctionCallException.h"
 
 #include "storm/utility/macros.h"
-#include "storm/exceptions/IllegalFunctionCallException.h"
 #include "storm/exceptions/InvalidArgumentException.h"
 #include "Place.h"
 
@@ -165,7 +164,6 @@ namespace storm {
 
         storm::gspn::GSPN* GspnBuilder::buildGspn() const {
             std::shared_ptr<storm::expressions::ExpressionManager> exprManager(new storm::expressions::ExpressionManager());
-            exprManager->
 
             std::vector<TransitionPartition> orderedPartitions;
             for(auto const& priorityPartitions : partitions) {
@@ -180,8 +178,11 @@ namespace storm {
                 
             }
             std::reverse(orderedPartitions.begin(), orderedPartitions.end());
-            
-            GSPN* result = new GSPN(gspnName, places, immediateTransitions, timedTransitions, orderedPartitions);
+            for(auto const& placeEntry : placeNames) {
+                exprManager->declareIntegerVariable(placeEntry.first, false);
+            }
+
+            GSPN* result = new GSPN(gspnName, places, immediateTransitions, timedTransitions, orderedPartitions, exprManager);
             result->setTransitionLayoutInfo(transitionLayout);
             result->setPlaceLayoutInfo(placeLayout);
             return result;

src/storm/utility/storm.cpp

@@ -41,7 +41,7 @@ namespace storm{
         }
     }
 
-    std::vector<storm::jani::Property> parseProperties(storm::parser::FormulaParser& formulaParser, std::string const& inputString, boost::optional<std::set<std::string>> const& propertyFilter = boost::none) {
+    std::vector<storm::jani::Property> parseProperties(storm::parser::FormulaParser& formulaParser, std::string const& inputString, boost::optional<std::set<std::string>> const& propertyFilter) {
         // If the given property looks like a file (containing a dot and there exists a file with that name),
         // we try to parse it as a file, otherwise we assume it's a property.
         std::vector<storm::jani::Property> properties;

src/storm/utility/storm.h

@@ -100,6 +100,10 @@
 
 namespace storm {
 
+    namespace parser {
+        class FormulaParser;
+    }
+
     template<typename ValueType>
     std::shared_ptr<storm::models::sparse::Model<ValueType>> buildExplicitModel(std::string const& transitionsFile, std::string const& labelingFile, boost::optional<std::string> const& stateRewardsFile = boost::none, boost::optional<std::string> const& transitionRewardsFile = boost::none, boost::optional<std::string> const& choiceLabelingFile = boost::none) {
         return storm::parser::AutoParser<>::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "", choiceLabelingFile ? choiceLabelingFile.get() : "" );
@@ -109,6 +113,7 @@ namespace storm {
     std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> parseJaniModel(std::string const& path);
     storm::prism::Program parseProgram(std::string const& path);
     std::vector<storm::jani::Property> substituteConstantsInProperties(std::vector<storm::jani::Property> const& properties, std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
+    std::vector<storm::jani::Property> parseProperties(storm::parser::FormulaParser& formulaParser, std::string const& inputString, boost::optional<std::set<std::string>> const& propertyFilter = boost::none);
     std::vector<storm::jani::Property> parsePropertiesForExplicit(std::string const& inputString, boost::optional<std::set<std::string>> const& propertyFilter = boost::none);
     std::vector<storm::jani::Property> parsePropertiesForPrismProgram(std::string const& inputString, storm::prism::Program const& program, boost::optional<std::set<std::string>> const& propertyFilter = boost::none);
     std::vector<storm::jani::Property> parsePropertiesForJaniModel(std::string const& inputString, storm::jani::Model const& model, boost::optional<std::set<std::string>> const& propertyFilter = boost::none);