added ltl2da option

src/storm/automata/LTL2DeterministicAutomaton.cpp

@@ -22,12 +22,10 @@
 namespace storm {
     namespace automata {
 
-        bool LTL2DeterministicAutomaton::isExternalDaToolSet() {
-            return std::getenv("LTL2DA");
-        }
 
-        std::shared_ptr<DeterministicAutomaton> LTL2DeterministicAutomaton::ltl2daInternalTool(std::string const& prefixLtl, bool dnf) {
+        std::shared_ptr<DeterministicAutomaton> LTL2DeterministicAutomaton::ltl2daSpot(storm::logic::Formula const& f, bool dnf) {
 #ifdef STORM_HAVE_SPOT
+            std::string prefixLtl = f.toPrefixString();
 
             spot::parsed_formula spotPrefixLtl = spot::parse_prefix_ltl(prefixLtl);
             if(!spotPrefixLtl.errors.empty()){
@@ -68,12 +66,10 @@ namespace storm {
         }
 
         // TODO: this is quite hacky, improve robustness
-        std::shared_ptr<DeterministicAutomaton> LTL2DeterministicAutomaton::ltl2daExternalTool(std::string const& prefixLtl) {
-
-
-            std::string ltl2da_tool = std::getenv("LTL2DA");
+        std::shared_ptr<DeterministicAutomaton> LTL2DeterministicAutomaton::ltl2daExternalTool(storm::logic::Formula const& f, std::string ltl2daTool) {
+            std::string prefixLtl = f.toPrefixString();
 
-            STORM_LOG_INFO("Calling external LTL->DA tool:   " << ltl2da_tool << " '" << prefixLtl << "' da.hoa");
+            STORM_LOG_INFO("Calling external LTL->DA tool:   " << ltl2daTool << " '" << prefixLtl << "' da.hoa");
 
             pid_t pid;
 
@@ -82,7 +78,7 @@ namespace storm {
 
             if (pid == 0) {
                 // we are in the child process
-                if (execlp(ltl2da_tool.c_str(), ltl2da_tool.c_str(), prefixLtl.c_str(), "da.hoa", NULL) < 0) {
+                if (execlp(ltl2daTool.c_str(), ltl2daTool.c_str(), prefixLtl.c_str(), "da.hoa", NULL) < 0) {
                     std::cerr << "ERROR: exec failed: " << strerror(errno) << std::endl;
                     std::exit(1);
                 }
@@ -110,17 +106,6 @@ namespace storm {
             }
         }
 
-        std::shared_ptr<DeterministicAutomaton> LTL2DeterministicAutomaton::ltl2da(storm::logic::Formula const& f, bool dnf) {
-            std::string prefixLtl = f.toPrefixString();
-
-            storm::automata::DeterministicAutomaton::ptr da;
-            if(isExternalDaToolSet()){
-                da = ltl2daExternalTool(prefixLtl);
-            } else {
-                da = ltl2daInternalTool(prefixLtl, dnf);
-            }
-            return da;
     }
 
-    }
 }

src/storm/automata/LTL2DeterministicAutomaton.h

@@ -15,13 +15,23 @@ namespace storm {
 
         class LTL2DeterministicAutomaton {
         public:
-            static std::shared_ptr<DeterministicAutomaton> ltl2da(storm::logic::Formula const&, bool dnf);
 
-        private:
-            static bool isExternalDaToolSet();
+            /*!
+             * TODO
+             * @param f
+             * @param dnf
+             * @return
+             */
+            static std::shared_ptr<DeterministicAutomaton> ltl2daSpot(storm::logic::Formula const& f, bool dnf);
+
+            /*!
+             * TODO
+             * @param f
+             * @param ltl2daTool
+             * @return
+             */
+            static std::shared_ptr<DeterministicAutomaton> ltl2daExternalTool(storm::logic::Formula const& f, std::string ltl2daTool);
 
-            static std::shared_ptr<DeterministicAutomaton> ltl2daInternalTool(std::string const& prefixLtl, bool dnf);
-            static std::shared_ptr<DeterministicAutomaton> ltl2daExternalTool(std::string const& prefixLtl);
         };
 
     }

src/storm/environment/modelchecker/ModelCheckerEnvironment.cpp

@@ -3,6 +3,7 @@
 #include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h"
 
 #include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/ModelCheckerSettings.h"
 #include "storm/utility/macros.h"
 
 #include "storm/exceptions/InvalidEnvironmentException.h"
@@ -12,7 +13,10 @@
 namespace storm {
     
     ModelCheckerEnvironment::ModelCheckerEnvironment() {
-        // Intentionally left empty
+        auto const& mcSettings = storm::settings::getModule<storm::settings::modules::ModelCheckerSettings>();
+        if (mcSettings.isLtl2daSet()) {
+            ltl2da = mcSettings.getLtl2da();
+        }
     }
     
     ModelCheckerEnvironment::~ModelCheckerEnvironment() {
@@ -26,6 +30,25 @@ namespace storm {
     MultiObjectiveModelCheckerEnvironment const& ModelCheckerEnvironment::multi() const {
         return multiObjectiveModelCheckerEnvironment.get();
     }
+
+    bool ModelCheckerEnvironment::isLtl2daSet() const {
+        return ltl2da.is_initialized();
+    }
+
+    boost::optional<std::string> const& ModelCheckerEnvironment::getLtl2da() const {
+        return ltl2da;
+    }
+
+    void ModelCheckerEnvironment::setLtl2da(std::string const& value) {
+        ltl2da = value;
+    }
+
+    void ModelCheckerEnvironment::unsetLtl2da() {
+        ltl2da = boost::none;
+    }
+
+
+
 }
     
 

src/storm/environment/modelchecker/ModelCheckerEnvironment.h

@@ -20,9 +20,15 @@ namespace storm {
         MultiObjectiveModelCheckerEnvironment& multi();
         MultiObjectiveModelCheckerEnvironment const& multi() const;
 
+        bool isLtl2daSet() const;
+        boost::optional<std::string> const& getLtl2da() const;
+        void setLtl2da(std::string const& value);
+        void unsetLtl2da();
+
 
     private:
         SubEnvironment<MultiObjectiveModelCheckerEnvironment> multiObjectiveModelCheckerEnvironment;
+        boost::optional<std::string> ltl2da;
     };
 }
 

src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp

@@ -15,6 +15,8 @@
 #include "storm/settings/modules/DebugSettings.h"
 #include "storm/exceptions/InvalidPropertyException.h"
 
+#include "storm/environment/modelchecker/ModelCheckerEnvironment.h"
+
 namespace storm {
     namespace modelchecker {
         namespace helper {
@@ -272,11 +274,21 @@ namespace storm {
                     ltlFormula = formula.asSharedPointer();
                 }
 
-
                 STORM_LOG_INFO("Resulting LTL path formula: " << ltlFormula->toString());
                 STORM_LOG_INFO(" in prefix format: " << ltlFormula->toPrefixString());
 
-                std::shared_ptr<storm::automata::DeterministicAutomaton> da = storm::automata::LTL2DeterministicAutomaton::ltl2da(*ltlFormula, Nondeterministic);
+                // Convert LTL formula to a deterministic automaton
+                std::shared_ptr<storm::automata::DeterministicAutomaton> da;
+                if (env.modelchecker().isLtl2daSet()) {
+                    // Use the external tool given via ltl2da
+                    std::string ltl2da = env.modelchecker().getLtl2da().get();
+                    da = storm::automata::LTL2DeterministicAutomaton::ltl2daExternalTool(*ltlFormula, ltl2da);
+                }
+                else {
+                    // Use the internal tool (Spot)
+                    // For nondeterministic models the acceptance condition is transformed into DNF
+                    da = storm::automata::LTL2DeterministicAutomaton::ltl2daSpot(*ltlFormula, Nondeterministic);
+                }
 
                 STORM_LOG_INFO("Deterministic automaton for LTL formula has "
                                        << da->getNumberOfStates() << " states, "

src/storm/settings/modules/ModelCheckerSettings.cpp

@@ -14,15 +14,25 @@ namespace storm {
             
             const std::string ModelCheckerSettings::moduleName = "modelchecker";
             const std::string ModelCheckerSettings::filterRewZeroOptionName = "filterrewzero";
+            const std::string ModelCheckerSettings::ltl2daName = "ltl2da";
 
             ModelCheckerSettings::ModelCheckerSettings() : ModuleSettings(moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, filterRewZeroOptionName, false, "If set, states with reward zero are filtered out, potentially reducing the size of the equation system").setIsAdvanced().build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, ltl2daName, false, "If set, use an external tool to convert LTL formulas to state-based deterministic automata in HOA format").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "A script that can be called with a prefix formula and a name for the output automaton.").build()).build());
             }
             
             bool ModelCheckerSettings::isFilterRewZeroSet() const {
                 return this->getOption(filterRewZeroOptionName).getHasOptionBeenSet();
             }
 
+            bool ModelCheckerSettings::isLtl2daSet() const {
+                return this->getOption(ltl2daName).getHasOptionBeenSet();
+            }
+
+            std::string ModelCheckerSettings::getLtl2da() const {
+                return this->getOption(ltl2daName).getArgumentByName("filename").getValueAsString();
+            }
+            
         } // namespace modules
     } // namespace settings
 } // namespace storm

src/storm/settings/modules/ModelCheckerSettings.h

@@ -22,12 +22,27 @@ namespace storm {
 
                 bool isFilterRewZeroSet() const;
 
+                /*!
+                 * Retrieves whether the external ltl2da tool has been set.
+                 *
+                 * @return True iff the external ltl2da has been set.
+                 */
+                bool isLtl2daSet() const;
+
+                /*!
+                 * Retrieves the external ltl2da tool that is used for converting LTL formulas to deterministic automata.
+                 *
+                 * @return The executable to use for converting LTL formulas to deterministic automata.
+                 */
+                std::string getLtl2da() const;
+
                 // The name of the module.
                 static const std::string moduleName;
 
             private:
                 // Define the string names of the options as constants.
                 static const std::string filterRewZeroOptionName;
+                static const std::string ltl2daName;
             };
 
         } // namespace modules