Merge branch 'master' into smt-based-multi-objective

resources/3rdparty/CMakeLists.txt

@@ -213,7 +213,7 @@ if(USE_CARL)
 		message("START CARL CONFIG PROCESS")
 		file(MAKE_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download) 
 		execute_process(
-		COMMAND ${CMAKE_COMMAND} ${STORM_3RDPARTY_SOURCE_DIR}/carl "-DSTORM_3RDPARTY_BINARY_DIR=${STORM_3RDPARTY_BINARY_DIR}" "-DBoost_LIBRARY_DIRS=${Boost_LIBRARY_DIRS}" "-DBoost_INCLUDE_DIRS=${Boost_INCLUDE_DIRS}" "-DTHREAD_SAFE=ON"
+		COMMAND ${CMAKE_COMMAND} ${STORM_3RDPARTY_SOURCE_DIR}/carl "-DSTORM_3RDPARTY_BINARY_DIR=${STORM_3RDPARTY_BINARY_DIR}" "-DCARL_USE_CLN_NUMBERS=ON" "-DBoost_LIBRARY_DIRS=${Boost_LIBRARY_DIRS}" "-DBoost_INCLUDE_DIRS=${Boost_INCLUDE_DIRS}" "-DTHREAD_SAFE=ON"
 		WORKING_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download
 		OUTPUT_VARIABLE carlconfig_out
 		RESULT_VARIABLE carlconfig_result)

src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp

@@ -32,6 +32,9 @@
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/JitBuilderSettings.h"
 
+#include "storm/settings/modules/CoreSettings.h"
+
+
 #include "storm/utility/OsDetection.h"
 #include "storm-config.h"
 
@@ -535,6 +538,8 @@ namespace storm {
                 }
                 modelData["double"] = cpptempl::make_data(list);
 
+                modelData["dontFixDeadlocks"] = storm::settings::getModule<storm::settings::modules::CoreSettings>().isDontFixDeadlocksSet();
+
                 // If we are building a possibly parametric model, we need to create the parameters.
                 if (std::is_same<storm::RationalFunction, ValueType>::value) {
                     generateParameters(modelData);
@@ -1657,7 +1662,6 @@ namespace storm {
 #include "storm/builder/RewardModelInformation.h"
                 
 #include "storm/utility/constants.h"
-                
 #include "storm/exceptions/WrongFormatException.h"
                 
                 namespace storm {
@@ -2278,7 +2282,14 @@ namespace storm {
                                             // Explore all edges that participate in synchronization vectors.
                                             exploreSynchronizingEdges(currentState, behaviour, statesToExplore);
                                         }
-                                        
+
+                                        {% if dontFixDeadlocks %}
+                                        if (behaviour.empty() && behaviour.isExpanded() ) {
+                                            std::cout << currentState << std::endl;
+                                            throw storm::exceptions::WrongFormatException("Error while creating sparse matrix from JANI model: found deadlock state  and fixing deadlocks was explicitly disabled.");
+                                        }
+                                        {% endif %}
+
                                         this->addStateBehaviour(currentIndex, behaviour);
                                         behaviour.clear();
                                     }

src/storm/builder/jit/ModelComponentsBuilder.cpp

@@ -81,7 +81,8 @@ namespace storm {
                     }
                 } else {
                     if (behaviour.isExpanded() && dontFixDeadlocks) {
-                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating sparse matrix from JANI model: found deadlock state and fixing deadlocks was explicitly disabled.");
+                        // Skip on purpose; Error is produced in the generated code to provide better diagnostics.
+                        //STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating sparse matrix from JANI model: found deadlock state and fixing deadlocks was explicitly disabled.");
                     } else {
                         // Add the self-loop in the transition matrix.
                         transitionMatrixBuilder->addNextValue(currentRow, currentRowGroup, storm::utility::one<ValueType>());

src/storm/cli/cli.cpp

@@ -15,6 +15,7 @@
 #include "storm/settings/modules/JaniExportSettings.h"
 
 #include "storm/utility/resources.h"
+#include "storm/utility/file.h"
 #include "storm/utility/storm-version.h"
 
 
@@ -241,6 +242,13 @@ namespace storm {
                             properties.push_back(input.second.at(propName));
                         }
                     }
+
+                    if(ioSettings.isExportJaniDotSet()) {
+                        std::ofstream out;
+                        storm::utility::openFile(ioSettings.getExportJaniDotFilename(), out);
+                        model.asJaniModel().writeDotToStream(out);
+                        storm::utility::closeFile(out);
+                    }
                     
                 }
                 

src/storm/models/sparse/Ctmc.h

@@ -54,11 +54,9 @@ namespace storm {
                 
                 Ctmc(Ctmc<ValueType, RewardModelType> const& ctmc) = default;
                 Ctmc& operator=(Ctmc<ValueType, RewardModelType> const& ctmc) = default;
-                
-#ifndef WINDOWS
                 Ctmc(Ctmc<ValueType, RewardModelType>&& ctmc) = default;
                 Ctmc& operator=(Ctmc<ValueType, RewardModelType>&& ctmc) = default;
-#endif
+
                 /*!
                  * Retrieves the vector of exit rates of the model.
                  *

src/storm/models/sparse/DeterministicModel.h

@@ -47,11 +47,10 @@ namespace storm {
                 DeterministicModel(DeterministicModel<ValueType, RewardModelType> const& other) = default;
                 DeterministicModel& operator=(DeterministicModel<ValueType, RewardModelType> const& other) = default;
                 
-#ifndef WINDOWS
+
                 DeterministicModel(DeterministicModel<ValueType, RewardModelType>&& other) = default;
                 DeterministicModel<ValueType, RewardModelType>& operator=(DeterministicModel<ValueType, RewardModelType>&& model) = default;
-#endif
-                
+
                 virtual void reduceToStateBasedRewards() override;
                 
                 virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector<ValueType> const* firstValue = nullptr, std::vector<ValueType> const* secondValue = nullptr, std::vector<uint_fast64_t> const* stateColoring = nullptr, std::vector<std::string> const* colors = nullptr, std::vector<uint_fast64_t>* scheduler = nullptr, bool finalizeOutput = true) const override;

src/storm/models/sparse/Dtmc.h

@@ -44,11 +44,9 @@ namespace storm {
                 Dtmc(Dtmc<ValueType, RewardModelType> const& dtmc) = default;
                 Dtmc& operator=(Dtmc<ValueType, RewardModelType> const& dtmc) = default;
                 
-#ifndef WINDOWS
                 Dtmc(Dtmc<ValueType, RewardModelType>&& dtmc) = default;
                 Dtmc& operator=(Dtmc<ValueType, RewardModelType>&& dtmc) = default;
-#endif
-                
+
                 
 #ifdef STORM_HAVE_CARL
                 class ConstraintCollector {

src/storm/models/sparse/MarkovAutomaton.h

@@ -107,11 +107,9 @@ namespace storm {
                 MarkovAutomaton(MarkovAutomaton<ValueType, RewardModelType> const& other) = default;
                 MarkovAutomaton& operator=(MarkovAutomaton<ValueType, RewardModelType> const& other) = default;
                 
-#ifndef WINDOWS
                 MarkovAutomaton(MarkovAutomaton<ValueType, RewardModelType>&& other) = default;
                 MarkovAutomaton& operator=(MarkovAutomaton<ValueType, RewardModelType>&& other) = default;
-#endif
-                
+
                 /*!
                  * Retrieves whether the Markov automaton is closed.
                  *

src/storm/models/sparse/Mdp.h

@@ -44,11 +44,9 @@ namespace storm {
                 Mdp(Mdp<ValueType, RewardModelType> const& other) = default;
                 Mdp& operator=(Mdp<ValueType, RewardModelType> const& other) = default;
                 
-#ifndef WINDOWS
                 Mdp(Mdp<ValueType, RewardModelType>&& other) = default;
                 Mdp& operator=(Mdp<ValueType, RewardModelType>&& other) = default;
-#endif
-                
+
                 /*!
                  * Constructs an MDP by copying the current MDP and restricting the choices of each state to the ones
                  * whose label set is contained in the given label set. Note that is is only valid to call this method

src/storm/models/sparse/Model.h

@@ -46,11 +46,7 @@ namespace storm {
                 Model(Model<ValueType, RewardModelType> const& other) = default;
                 Model& operator=(Model<ValueType, RewardModelType> const& other) = default;
                 
-#ifndef WINDOWS
-                Model(Model<ValueType, RewardModelType>&& other) = default;
-                Model& operator=(Model<ValueType, RewardModelType>&& other) = default;
-#endif
-                
+
                 /*!
                  * Constructs a model from the given data.
                  *

src/storm/models/sparse/NondeterministicModel.h

@@ -47,11 +47,9 @@ namespace storm {
                 NondeterministicModel(NondeterministicModel<ValueType, RewardModelType> const& other) = default;
                 NondeterministicModel& operator=(NondeterministicModel<ValueType, RewardModelType> const& other) = default;
                 
-#ifndef WINDOWS
                 NondeterministicModel(NondeterministicModel<ValueType, RewardModelType>&& other) = default;
                 NondeterministicModel& operator=(NondeterministicModel<ValueType, RewardModelType>&& other) = default;
-#endif
-                
+
                 /*!
                  * Retrieves the number of (nondeterministic) choices in the model.
                  *

src/storm/models/sparse/StandardRewardModel.h

@@ -40,11 +40,9 @@ namespace storm {
                 StandardRewardModel(StandardRewardModel<ValueType> const& dtmc) = default;
                 StandardRewardModel& operator=(StandardRewardModel<ValueType> const& dtmc) = default;
                 
-#ifndef WINDOWS
                 StandardRewardModel(StandardRewardModel<ValueType>&& dtmc) = default;
                 StandardRewardModel& operator=(StandardRewardModel<ValueType>&& dtmc) = default;
-#endif
-                
+
                 /*!
                  * Retrieves whether the reward model has state rewards.
                  *

src/storm/models/sparse/StochasticTwoPlayerGame.h

@@ -52,11 +52,9 @@ namespace storm {
                 StochasticTwoPlayerGame(StochasticTwoPlayerGame const& other) = default;
                 StochasticTwoPlayerGame& operator=(StochasticTwoPlayerGame const& other) = default;
                 
-#ifndef WINDOWS
                 StochasticTwoPlayerGame(StochasticTwoPlayerGame&& other) = default;
                 StochasticTwoPlayerGame& operator=(StochasticTwoPlayerGame&& other) = default;
-#endif
-                
+
                 /*!
                  * Retrieves the matrix representing the choices in player 1 states.
                  *

src/storm/settings/Argument.cpp

@@ -68,9 +68,9 @@ namespace storm {
         
         template<typename T>
         void Argument<T>::setFromDefaultValue()  {
-            STORM_LOG_THROW(this->hasDefaultValue, storm::exceptions::IllegalFunctionCallException, "Unable to set value from default value, because the argument has none.");
+            STORM_LOG_THROW(this->hasDefaultValue, storm::exceptions::IllegalFunctionCallException, "Unable to set value from default value, because the argument " << name << " has none.");
             bool result = this->setFromTypeValue(this->defaultValue, false);
-            STORM_LOG_THROW(result, storm::exceptions::IllegalArgumentValueException, "Unable to assign default value to argument, because it was rejected.");
+            STORM_LOG_THROW(result, storm::exceptions::IllegalArgumentValueException, "Unable to assign default value to argument " << name << ", because it was rejected.");
         }
         
         template<typename T>
@@ -95,7 +95,7 @@ namespace storm {
             switch (this->argumentType) {
                 case ArgumentType::Integer:
                     return inferToInteger(ArgumentType::Integer, this->getArgumentValue());
-                default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as integer."); break;
+                default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value for " << name << " as integer."); break;
             }
         }
         
@@ -105,7 +105,7 @@ namespace storm {
             switch (this->argumentType) {
                 case ArgumentType::UnsignedInteger:
                     return inferToUnsignedInteger(ArgumentType::UnsignedInteger, this->getArgumentValue());
-                default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as unsigned integer."); break;
+                default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value for " << name << " as unsigned integer."); break;
             }
         }
         
@@ -115,7 +115,7 @@ namespace storm {
             switch (this->argumentType) {
                 case ArgumentType::Double:
                     return inferToDouble(ArgumentType::Double, this->getArgumentValue());
-                default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as double."); break;
+                default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value for " << name << " as double."); break;
             }
         }
         
@@ -124,7 +124,7 @@ namespace storm {
             switch (this->argumentType) {
                 case ArgumentType::Boolean:
                     return inferToBoolean(ArgumentType::Boolean, this->getArgumentValue());
-                default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as boolean."); break;
+                default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value for " << name << " as Boolean."); break;
             }
         }
         

src/storm/settings/modules/IOSettings.cpp

@@ -19,6 +19,7 @@ namespace storm {
             const std::string IOSettings::moduleName = "io";
             const std::string IOSettings::exportDotOptionName = "exportdot";
             const std::string IOSettings::exportExplicitOptionName = "exportexplicit";
+            const std::string IOSettings::exportJaniDotOptionName = "exportjanidot";
             const std::string IOSettings::explicitOptionName = "explicit";
             const std::string IOSettings::explicitOptionShortName = "exp";
             const std::string IOSettings::explicitDrnOptionName = "explicit-drn";
@@ -40,6 +41,7 @@ namespace storm {
             const std::string IOSettings::prismCompatibilityOptionShortName = "pc";
             const std::string IOSettings::noBuildOptionName = "nobuild";
             const std::string IOSettings::fullModelBuildOptionName = "buildfull";
+            const std::string IOSettings::buildChoiceLabelOptionName = "buildchoicelab";
             const std::string IOSettings::janiPropertyOptionName = "janiproperty";
             const std::string IOSettings::janiPropertyOptionShortName = "jprop";
             const std::string IOSettings::propertyOptionName = "prop";
@@ -50,6 +52,8 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, prismCompatibilityOptionName, false, "Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportDotOptionName, "", "If given, the loaded model will be written to the specified file in the dot format.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, exportJaniDotOptionName, "", "If given, the loaded jani model will be written to the specified file in the dot format.")
+                                        .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportExplicitOptionName, "", "If given, the loaded model will be written to the specified file in the drn format.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "the name of the file to which the model is to be writen.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, explicitOptionName, false, "Parses the model given in an explicit (sparse) representation.").setShortName(explicitOptionShortName)
@@ -65,6 +69,7 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, prismToJaniOptionName, false, "If set, the input PRISM model is transformed to JANI.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, jitOptionName, false, "If set, the model is built using the JIT model builder.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, fullModelBuildOptionName, false, "If set, include all rewards and labels.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, buildChoiceLabelOptionName, false, "If set, include choice labels").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, noBuildOptionName, false, "If set, do not build the model.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, propertyOptionName, false, "Specifies the properties to be checked on the model.").setShortName(propertyOptionShortName)
                                         .addArgument(storm::settings::ArgumentBuilder::createStringArgument("property or filename", "The formula or the file containing the formulas.").build())
@@ -94,6 +99,14 @@ namespace storm {
             std::string IOSettings::getExportDotFilename() const {
                 return this->getOption(exportDotOptionName).getArgumentByName("filename").getValueAsString();
             }
+
+            bool IOSettings::isExportJaniDotSet() const {
+                return this->getOption(exportJaniDotOptionName).getHasOptionBeenSet();
+            }
+
+            std::string IOSettings::getExportJaniDotFilename() const {
+                return this->getOption(exportJaniDotOptionName).getArgumentByName("filename").getValueAsString();
+            }
             
             bool IOSettings::isExportExplicitSet() const {
                 return this->getOption(exportExplicitOptionName).getHasOptionBeenSet();
@@ -225,6 +238,10 @@ namespace storm {
                 return this->getOption(noBuildOptionName).getHasOptionBeenSet();
             }
 
+            bool IOSettings::isBuildChoiceLabelsSet() const {
+                return this->getOption(buildChoiceLabelOptionName).getHasOptionBeenSet();
+            }
+
             bool IOSettings::isPropertySet() const {
                 return this->getOption(propertyOptionName).getHasOptionBeenSet();
             }
@@ -247,6 +264,8 @@ namespace storm {
                 // Ensure that not two explicit input models were given.
                 STORM_LOG_THROW(!isExplicitSet() || !isExplicitDRNSet(), storm::exceptions::InvalidSettingsException, "Explicit model ");
 
+                STORM_LOG_THROW(!isExportJaniDotSet() || isJaniInputSet(), storm::exceptions::InvalidSettingsException, "Jani-to-dot export is only available for jani models" );
+
                 // Ensure that the model was given either symbolically or explicitly.
                 STORM_LOG_THROW(!isJaniInputSet() || !isPrismInputSet() || !isExplicitSet() || !isExplicitDRNSet(), storm::exceptions::InvalidSettingsException, "The model may be either given in an explicit or a symbolic format (PRISM or JANI), but not both.");
                 

src/storm/settings/modules/IOSettings.h

@@ -35,6 +35,20 @@ namespace storm {
                  */
                 std::string getExportDotFilename() const;
 
+                /*!
+                 * Retrieves whether the export-to-dot option for jani was set.
+                 *
+                 * @return True if the export-to-jani-dot option was set.
+                 */
+                bool isExportJaniDotSet() const;
+
+                /*!
+                 * Retrieves the name in which to write the jani model in dot format, if the export-to-jani-dot option was set.
+                 *
+                 * @return The name of the file in which to write the exported model.
+                 */
+                std::string getExportJaniDotFilename() const;
+
                 /*!
                  * Retrieves whether the export-to-explicit option was set
                  *
@@ -277,6 +291,12 @@ namespace storm {
                  */
                 bool isBuildFullModelSet() const;
 
+                /*!
+                 * Retrieves whether the choice labels should be build
+                 * @return
+                 */
+                bool isBuildChoiceLabelsSet() const;
+
                 bool check() const override;
                 void finalize() override;
 
@@ -286,6 +306,7 @@ namespace storm {
             private:
                 // Define the string names of the options as constants.
                 static const std::string exportDotOptionName;
+                static const std::string exportJaniDotOptionName;
                 static const std::string exportExplicitOptionName;
                 static const std::string explicitOptionName;
                 static const std::string explicitOptionShortName;
@@ -308,6 +329,7 @@ namespace storm {
                 static const std::string prismCompatibilityOptionShortName;
                 static const std::string fullModelBuildOptionName;
                 static const std::string noBuildOptionName;
+                static const std::string buildChoiceLabelOptionName;
                 static const std::string janiPropertyOptionName;
                 static const std::string janiPropertyOptionShortName;
                 static const std::string propertyOptionName;

src/storm/storage/expressions/BaseExpression.h

@@ -48,11 +48,9 @@ namespace storm {
             // Create default versions of constructors and assignments.
             BaseExpression(BaseExpression const&) = default;
             BaseExpression& operator=(BaseExpression const&) = delete;
-#ifndef WINDOWS
             BaseExpression(BaseExpression&&) = default;
             BaseExpression& operator=(BaseExpression&&) = delete;
-#endif
-            
+
             // Make the destructor virtual (to allow destruction via base class pointer) and default it.
             virtual ~BaseExpression() = default;
 

src/storm/storage/expressions/BinaryBooleanFunctionExpression.h

@@ -27,10 +27,9 @@ namespace storm {
             // Instantiate constructors and assignments with their default implementations.
             BinaryBooleanFunctionExpression(BinaryBooleanFunctionExpression const& other) = default;
             BinaryBooleanFunctionExpression& operator=(BinaryBooleanFunctionExpression const& other) = delete;
-#ifndef WINDOWS
             BinaryBooleanFunctionExpression(BinaryBooleanFunctionExpression&&) = default;
             BinaryBooleanFunctionExpression& operator=(BinaryBooleanFunctionExpression&&) = delete;
-#endif
+
             virtual ~BinaryBooleanFunctionExpression() = default;
             
             // Override base class methods.

src/storm/storage/expressions/BinaryExpression.h

@@ -24,10 +24,9 @@ namespace storm {
             // Instantiate constructors and assignments with their default implementations.
             BinaryExpression(BinaryExpression const& other) = default;
             BinaryExpression& operator=(BinaryExpression const& other) = delete;
-#ifndef WINDOWS
             BinaryExpression(BinaryExpression&&) = default;
             BinaryExpression& operator=(BinaryExpression&&) = delete;
-#endif
+
             virtual ~BinaryExpression() = default;
 
             // Override base class methods.

src/storm/storage/expressions/BinaryNumericalFunctionExpression.h

@@ -27,10 +27,9 @@ namespace storm {
             // Instantiate constructors and assignments with their default implementations.
             BinaryNumericalFunctionExpression(BinaryNumericalFunctionExpression const& other) = default;
             BinaryNumericalFunctionExpression& operator=(BinaryNumericalFunctionExpression const& other) = delete;
-#ifndef WINDOWS
             BinaryNumericalFunctionExpression(BinaryNumericalFunctionExpression&&) = default;
             BinaryNumericalFunctionExpression& operator=(BinaryNumericalFunctionExpression&&) = delete;
-#endif
+
             virtual ~BinaryNumericalFunctionExpression() = default;
             
             // Override base class methods.

src/storm/storage/expressions/BinaryRelationExpression.h

@@ -27,10 +27,9 @@ namespace storm {
             // Instantiate constructors and assignments with their default implementations.
             BinaryRelationExpression(BinaryRelationExpression const& other) = default;
             BinaryRelationExpression& operator=(BinaryRelationExpression const& other) = default;
-#ifndef WINDOWS
             BinaryRelationExpression(BinaryRelationExpression&&) = default;
             BinaryRelationExpression& operator=(BinaryRelationExpression&&) = default;
-#endif
+
             virtual ~BinaryRelationExpression() = default;
             
             // Override base class methods.

src/storm/storage/expressions/BooleanLiteralExpression.h

@@ -19,10 +19,9 @@ namespace storm {
             // Instantiate constructors and assignments with their default implementations.
             BooleanLiteralExpression(BooleanLiteralExpression const& other) = default;
             BooleanLiteralExpression& operator=(BooleanLiteralExpression const& other) = delete;
-#ifndef WINDOWS
             BooleanLiteralExpression(BooleanLiteralExpression&&) = default;
             BooleanLiteralExpression& operator=(BooleanLiteralExpression&&) = delete;
-#endif
+
             virtual ~BooleanLiteralExpression() = default;
 
             // Override base class methods.

src/storm/storage/expressions/Expression.h

@@ -76,11 +76,9 @@ namespace storm {
             // Instantiate constructors and assignments with their default implementations.
             Expression(Expression const& other) = default;
             Expression& operator=(Expression const& other) = default;
-#ifndef WINDOWS
             Expression(Expression&&) = default;
             Expression& operator=(Expression&&) = default;
-#endif
-            
+
             /*!
              * Converts the expression to an expression over the variables of the provided expression manager.
              */

src/storm/storage/expressions/IfThenElseExpression.h

@@ -21,10 +21,9 @@ namespace storm {
             // Instantiate constructors and assignments with their default implementations.
             IfThenElseExpression(IfThenElseExpression const& other) = default;
             IfThenElseExpression& operator=(IfThenElseExpression const& other) = delete;
-#ifndef WINDOWS
             IfThenElseExpression(IfThenElseExpression&&) = default;
             IfThenElseExpression& operator=(IfThenElseExpression&&) = delete;
-#endif
+
             virtual ~IfThenElseExpression() = default;
             
             // Override base class methods.

src/storm/storage/expressions/IntegerLiteralExpression.h

@@ -19,10 +19,9 @@ namespace storm {
             // Instantiate constructors and assignments with their default implementations.
             IntegerLiteralExpression(IntegerLiteralExpression const& other) = default;
             IntegerLiteralExpression& operator=(IntegerLiteralExpression const& other) = delete;
-#ifndef WINDOWS
             IntegerLiteralExpression(IntegerLiteralExpression&&) = default;
             IntegerLiteralExpression& operator=(IntegerLiteralExpression&&) = delete;
-#endif
+
             virtual ~IntegerLiteralExpression() = default;
             
             // Override base class methods.

src/storm/storage/expressions/LinearCoefficientVisitor.h

@@ -18,11 +18,9 @@ namespace storm {
 
                 VariableCoefficients(VariableCoefficients const& other) = default;
                 VariableCoefficients& operator=(VariableCoefficients const& other) = default;
-#ifndef WINDOWS
                 VariableCoefficients(VariableCoefficients&& other) = default;
                 VariableCoefficients& operator=(VariableCoefficients&& other) = default;
-#endif
-                
+
                 VariableCoefficients& operator+=(VariableCoefficients&& other);
                 VariableCoefficients& operator-=(VariableCoefficients&& other);
                 VariableCoefficients& operator*=(VariableCoefficients&& other);

src/storm/storage/expressions/RationalLiteralExpression.h

@@ -37,10 +37,9 @@ namespace storm {
             // Instantiate constructors and assignments with their default implementations.
             RationalLiteralExpression(RationalLiteralExpression const& other) = default;
             RationalLiteralExpression& operator=(RationalLiteralExpression const& other) = delete;
-#ifndef WINDOWS
             RationalLiteralExpression(RationalLiteralExpression&&) = default;
             RationalLiteralExpression& operator=(RationalLiteralExpression&&) = delete;
-#endif
+
             virtual ~RationalLiteralExpression() = default;
             
             // Override base class methods.

src/storm/storage/expressions/UnaryBooleanFunctionExpression.h

@@ -26,10 +26,8 @@ namespace storm {
             // Instantiate constructors and assignments with their default implementations.
             UnaryBooleanFunctionExpression(UnaryBooleanFunctionExpression const& other) = default;
             UnaryBooleanFunctionExpression& operator=(UnaryBooleanFunctionExpression const& other) = delete;
-#ifndef WINDOWS
             UnaryBooleanFunctionExpression(UnaryBooleanFunctionExpression&&) = default;
             UnaryBooleanFunctionExpression& operator=(UnaryBooleanFunctionExpression&&) = delete;
-#endif
             virtual ~UnaryBooleanFunctionExpression() = default;
             
             // Override base class methods.

src/storm/storage/expressions/UnaryExpression.h

@@ -20,10 +20,8 @@ namespace storm {
             // Instantiate constructors and assignments with their default implementations.
             UnaryExpression(UnaryExpression const& other) = default;
             UnaryExpression& operator=(UnaryExpression const& other) = delete;
-#ifndef WINDOWS
             UnaryExpression(UnaryExpression&&) = default;
             UnaryExpression& operator=(UnaryExpression&&) = delete;
-#endif
             virtual ~UnaryExpression() = default;
             
             // Override base class methods.

src/storm/storage/expressions/UnaryNumericalFunctionExpression.h

@@ -26,10 +26,9 @@ namespace storm {
             // Instantiate constructors and assignments with their default implementations.
             UnaryNumericalFunctionExpression(UnaryNumericalFunctionExpression const& other) = default;
             UnaryNumericalFunctionExpression& operator=(UnaryNumericalFunctionExpression const& other) = delete;
-#ifndef WINDOWS
             UnaryNumericalFunctionExpression(UnaryNumericalFunctionExpression&&) = default;
             UnaryNumericalFunctionExpression& operator=(UnaryNumericalFunctionExpression&&) = delete;
-#endif
+
             virtual ~UnaryNumericalFunctionExpression() = default;
             
             // Override base class methods.

src/storm/storage/expressions/Variable.h

@@ -31,10 +31,9 @@ namespace storm {
             // Default-instantiate some copy/move construction/assignment.
             Variable(Variable const& other) = default;
             Variable& operator=(Variable const& other) = default;
-#ifndef WINDOWS
             Variable(Variable&& other) = default;
             Variable& operator=(Variable&& other) = default;
-#endif
+
             
             /*!
              * Checks the two variables for equality.

src/storm/storage/expressions/VariableExpression.h

@@ -20,10 +20,9 @@ namespace storm {
             // Instantiate constructors and assignments with their default implementations.
             VariableExpression(VariableExpression const&) = default;
             VariableExpression& operator=(VariableExpression const&) = delete;
-#ifndef WINDOWS
             VariableExpression(VariableExpression&&) = default;
             VariableExpression& operator=(VariableExpression&&) = delete;
-#endif
+
             virtual ~VariableExpression() = default;
 
             // Override base class methods.

src/storm/storage/jani/Automaton.cpp

@@ -528,5 +528,36 @@ namespace storm {
             
             return result;
         }
+
+        void Automaton::writeDotToStream(std::ostream& outStream, std::vector<std::string> const& actionNames) const {
+            outStream << "\tsubgraph " << name << " {" << std::endl;
+
+            // Write all locations to the stream.
+            uint64_t locIndex = 0;
+            for (auto const& loc : locations) {
+                outStream << "\t" << name << "_s" << locIndex  << "[ label=\"" << loc.getName() << "\"];" << std::endl;
+                ++locIndex;
+            }
+            // Write for each edge an node to the stream;
+            uint64_t edgeIndex = 0;
+            for (auto const& edge : edges) {
+                outStream << "\t" << name << "_e" << edgeIndex << "[ label=\"\" , shape=circle, width=.2, style=filled, fillcolor=\"black\"];" << std::endl;
+                ++edgeIndex;
+            }
+
+            // Connect edges
+            edgeIndex = 0;
+            for (auto const& edge : edges) {
+                outStream << "\t" << name << "_s" << edge.getSourceLocationIndex() << " -> " << name << "_e" << edgeIndex << " [label=\"" << actionNames.at(edge.getActionIndex()) << "\"];" << std::endl;
+                for (auto const& edgeDest : edge.getDestinations()) {
+                    outStream << "\t" << name << "_e" << edgeIndex << " -> " << name << "_s" << edgeDest.getLocationIndex() << ";" << std::endl;
+                }
+                ++edgeIndex;
+            }
+
+
+            outStream << "\t}" << std::endl;
+
+        }
     }
 }

src/storm/storage/jani/Automaton.h

@@ -371,6 +371,8 @@ namespace storm {
              * Checks the automaton for linearity.
              */
             bool isLinear() const;
+
+            void writeDotToStream(std::ostream& outStream, std::vector<std::string> const& actionNames) const;
             
         private:
             /// The name of the automaton.

src/storm/storage/jani/JSONExporter.cpp

@@ -525,6 +525,7 @@ namespace storm {
                 }
             }
             STORM_LOG_ASSERT(false, "Expression variable '" << expression.getVariableName() << "' not known in Jani data structures.");
+            return modernjson::json(); // should not reach this point.
         }
         boost::any ExpressionToJson::visit(storm::expressions::UnaryBooleanFunctionExpression const& expression, boost::any const& data) {
             modernjson::json opDecl;

src/storm/storage/jani/Model.cpp

@@ -1,5 +1,7 @@
 #include "storm/storage/jani/Model.h"
 
+#include <algorithm>
+
 #include "storm/storage/expressions/ExpressionManager.h"
 
 
@@ -1165,5 +1167,32 @@ namespace storm {
             
             return newModel;
         }
+
+
+        // Helper for writeDotToStream:
+
+        std::string filterName(std::string const& text)  {
+            std::string result = text;
+            std::replace_if(result.begin() , result.end() ,
+                            [] (const char& c) { return std::ispunct(c) ;},'_');
+            return result;
+        }
+
+
+        void Model::writeDotToStream(std::ostream& outStream) const {
+            outStream << "digraph " << filterName(name) << " {" << std::endl;
+
+            std::vector<std::string> actionNames;
+            for (auto const& act : actions) {
+                actionNames.push_back(act.getName());
+            }
+
+            for (auto const& automaton : automata) {
+                automaton.writeDotToStream(outStream, actionNames);
+                outStream << std::endl;
+            }
+
+            outStream << "}";
+        }
     }
 }

src/storm/storage/jani/Model.h

@@ -448,6 +448,8 @@ namespace storm {
              * @return
              */
             bool reusesActionsInComposition() const;
+
+            void writeDotToStream(std::ostream& outStream = std::cout) const;
             
             /// The name of the silent action.
             static const std::string SILENT_ACTION_NAME;

src/storm/storage/prism/Assignment.h

@@ -26,11 +26,9 @@ namespace storm {
             Assignment() = default;
             Assignment(Assignment const& other) = default;
             Assignment& operator=(Assignment const& other)= default;
-#ifndef WINDOWS
             Assignment(Assignment&& other) = default;
             Assignment& operator=(Assignment&& other) = default;
-#endif
-            
+
             /*!
              * Retrieves the name of the variable that this assignment targets.
              *

src/storm/storage/prism/BooleanVariable.h

@@ -14,10 +14,8 @@ namespace storm {
             BooleanVariable() = default;
             BooleanVariable(BooleanVariable const& other) = default;
             BooleanVariable& operator=(BooleanVariable const& other)= default;
-#ifndef WINDOWS
             BooleanVariable(BooleanVariable&& other) = default;
             BooleanVariable& operator=(BooleanVariable&& other) = default;
-#endif
 
             /*!
              * Creates a boolean variable with the given constant initial value expression.

src/storm/storage/prism/Command.h

@@ -32,11 +32,9 @@ namespace storm {
             Command() = default;
             Command(Command const& other) = default;
             Command& operator=(Command const& other) = default;
-#ifndef WINDOWS
             Command(Command&& other) = default;
             Command& operator=(Command&& other) = default;
-#endif
-            
+
             /*!
              * Retrieves the action name of this command.
              *

src/storm/storage/prism/Constant.h

@@ -35,11 +35,9 @@ namespace storm {
             Constant() = default;
             Constant(Constant const& other) = default;
             Constant& operator=(Constant const& other)= default;
-#ifndef WINDOWS
             Constant(Constant&& other) = default;
             Constant& operator=(Constant&& other) = default;
-#endif
-            
+
             /*!
              * Retrieves the name of the constant.
              *

src/storm/storage/prism/Formula.h

@@ -26,11 +26,9 @@ namespace storm {
             Formula() = default;
             Formula(Formula const& other) = default;
             Formula& operator=(Formula const& other)= default;
-#ifndef WINDOWS
             Formula(Formula&& other) = default;
             Formula& operator=(Formula&& other) = default;
-#endif
-            
+
             /*!
              * Retrieves the name that is associated with this formula.
              *

src/storm/storage/prism/InitialConstruct.h

@@ -32,11 +32,9 @@ namespace storm {
             InitialConstruct() = default;
             InitialConstruct(InitialConstruct const& other) = default;
             InitialConstruct& operator=(InitialConstruct const& other)= default;
-#ifndef WINDOWS
             InitialConstruct(InitialConstruct&& other) = default;
             InitialConstruct& operator=(InitialConstruct&& other) = default;
-#endif
-            
+
             /*!
              * Retrieves the expression characterizing the initial states.
              *

src/storm/storage/prism/IntegerVariable.h

@@ -14,10 +14,8 @@ namespace storm {
             IntegerVariable() = default;
             IntegerVariable(IntegerVariable const& other) = default;
             IntegerVariable& operator=(IntegerVariable const& other)= default;
-#ifndef WINDOWS
             IntegerVariable(IntegerVariable&& other) = default;
             IntegerVariable& operator=(IntegerVariable&& other) = default;
-#endif
 
             /*!
              * Creates an integer variable with the given initial value expression.

src/storm/storage/prism/Label.h

@@ -34,11 +34,9 @@ namespace storm {
             Label() = default;
             Label(Label const& other) = default;
             Label& operator=(Label const& other)= default;
-#ifndef WINDOWS
             Label(Label&& other) = default;
             Label& operator=(Label&& other) = default;
-#endif
-            
+
             /*!
              * Retrieves the name that is associated with this label.
              *

src/storm/storage/prism/LocatedInformation.h

@@ -22,11 +22,9 @@ namespace storm {
             LocatedInformation() = default;
             LocatedInformation(LocatedInformation const& other) = default;
             LocatedInformation& operator=(LocatedInformation const& other)= default;
-#ifndef WINDOWS
             LocatedInformation(LocatedInformation&& other) = default;
             LocatedInformation& operator=(LocatedInformation&& other) = default;
-#endif
-            
+
             /*!
              * Retrieves the name of the file in which the information was found.
              *

src/storm/storage/prism/Module.h

@@ -48,11 +48,9 @@ namespace storm {
             Module() = default;
             Module(Module const& other) = default;
             Module& operator=(Module const& other)= default;
-#ifndef WINDOWS
             Module(Module&& other) = default;
             Module& operator=(Module&& other) = default;
-#endif
-            
+
             /*!
              * Retrieves the number of boolean variables in the module.
              *

src/storm/storage/prism/Program.h

@@ -63,11 +63,9 @@ namespace storm {
             Program() = default;
             Program(Program const& other) = default;
             Program& operator=(Program const& other) = default;
-#ifndef WINDOWS
             Program(Program&& other) = default;
             Program& operator=(Program&& other) = default;
-#endif
-            
+
             /*!
              * Retrieves the model type of the model.
              *

src/storm/storage/prism/RewardModel.h

@@ -31,11 +31,9 @@ namespace storm {
             RewardModel() = default;
             RewardModel(RewardModel const& other) = default;
             RewardModel& operator=(RewardModel const& other)= default;
-#ifndef WINDOWS
             RewardModel(RewardModel&& other) = default;
             RewardModel& operator=(RewardModel&& other) = default;
-#endif
-            
+
             /*!
              * Retrieves the name of the reward model.
              *

src/storm/storage/prism/StateActionReward.h

@@ -38,11 +38,9 @@ namespace storm {
             StateActionReward() = default;
             StateActionReward(StateActionReward const& other) = default;
             StateActionReward& operator=(StateActionReward const& other)= default;
-#ifndef WINDOWS
             StateActionReward(StateActionReward&& other) = default;
             StateActionReward& operator=(StateActionReward&& other) = default;
-#endif
-            
+
             /*!
              * Retrieves the action name that is associated with this transition reward.
              *

src/storm/storage/prism/StateReward.h

@@ -35,11 +35,9 @@ namespace storm {
             StateReward() = default;
             StateReward(StateReward const& other) = default;
             StateReward& operator=(StateReward const& other)= default;
-#ifndef WINDOWS
             StateReward(StateReward&& other) = default;
             StateReward& operator=(StateReward&& other) = default;
-#endif
-            
+
             /*!
              * Retrieves the state predicate that is associated with this state reward.
              *

src/storm/storage/prism/SystemCompositionConstruct.h

@@ -26,11 +26,9 @@ namespace storm {
             SystemCompositionConstruct() = default;
             SystemCompositionConstruct(SystemCompositionConstruct const& other) = default;
             SystemCompositionConstruct& operator=(SystemCompositionConstruct const& other)= default;
-#ifndef WINDOWS
             SystemCompositionConstruct(SystemCompositionConstruct&& other) = default;
             SystemCompositionConstruct& operator=(SystemCompositionConstruct&& other) = default;
-#endif
-            
+
             Composition const& getSystemComposition() const;
             
             friend std::ostream& operator<<(std::ostream& stream, SystemCompositionConstruct const& systemCompositionConstruct);

src/storm/storage/prism/TransitionReward.h

@@ -41,11 +41,9 @@ namespace storm {
             TransitionReward() = default;
             TransitionReward(TransitionReward const& other) = default;
             TransitionReward& operator=(TransitionReward const& other)= default;
-#ifndef WINDOWS
             TransitionReward(TransitionReward&& other) = default;
             TransitionReward& operator=(TransitionReward&& other) = default;
-#endif
-            
+
             /*!
              * Retrieves the action name that is associated with this transition reward.
              *

src/storm/storage/prism/Update.h

@@ -26,11 +26,9 @@ namespace storm {
             Update() = default;
             Update(Update const& other) = default;
             Update& operator=(Update const& other)= default;
-#ifndef WINDOWS
             Update(Update&& other) = default;
             Update& operator=(Update&& other) = default;
-#endif
-            
+
             /*!
              * Retrieves the expression for the likelihood of this update.
              *

src/storm/storage/prism/Variable.h

@@ -15,11 +15,9 @@ namespace storm {
             // Create default implementations of constructors/assignment.
             Variable(Variable const& otherVariable) = default;
             Variable& operator=(Variable const& otherVariable)= default;
-#ifndef WINDOWS
             Variable(Variable&& otherVariable) = default;
             Variable& operator=(Variable&& otherVariable) = default;
-#endif
-            
+
             /*!
              * Retrieves the name of the variable.
              *