Merge branch 'master' into nativepolytopes

src/storm-dft/modelchecker/dft/DFTASFChecker.cpp

@@ -1,5 +1,6 @@
 #include "DFTASFChecker.h"
 #include <string>
+#include "storm/utility/file.h"
 
 namespace storm {
     
@@ -394,24 +395,22 @@ namespace storm {
                 }
                 
                 void DFTASFChecker::toFile(std::string const& filename) {
-                    std::ofstream ofs;
-                    std::cout << "Writing to " << filename << std::endl;
-                    ofs.open(filename);
-                    ofs << "; time point variables" << std::endl;
+                    std::ofstream stream;
+                    storm::utility::openFile(filename, stream);
+                    stream << "; time point variables" << std::endl;
                     for (auto const& timeVarEntry : timePointVariables) {
-                        ofs << "(declare-fun " << varNames[timeVarEntry.second] << "()  Int)" << std::endl;
+                        stream << "(declare-fun " << varNames[timeVarEntry.second] << "()  Int)" << std::endl;
                     }
-                    ofs << "; claim variables" << std::endl;
+                    stream << "; claim variables" << std::endl;
                     for (auto const& claimVarEntry : claimVariables) {
-                        ofs << "(declare-fun " << varNames[claimVarEntry.second] << "() Int)" << std::endl;
+                        stream << "(declare-fun " << varNames[claimVarEntry.second] << "() Int)" << std::endl;
                     }
                     for (auto const& constraint : constraints) {
-                        ofs << "; " << constraint->description() << std::endl;
-                        ofs << "(assert " << constraint->toSmtlib2(varNames) << ")" << std::endl;
+                        stream << "; " << constraint->description() << std::endl;
+                        stream << "(assert " << constraint->toSmtlib2(varNames) << ")" << std::endl;
                     }
-                    ofs << "(check-sat)" << std::endl;
-                    ofs.close();
-                    
+                    stream << "(check-sat)" << std::endl;
+                    storm::utility::closeFile(stream);
                 }
     }
 }

src/storm-dft/parser/DFTGalileoParser.cpp

@@ -10,6 +10,7 @@
 #include "storm/exceptions/FileIoException.h"
 #include "storm/exceptions/NotSupportedException.h"
 #include "storm/utility/macros.h"
+#include "storm/utility/file.h"
 
 namespace storm {
     namespace parser {
@@ -49,18 +50,10 @@ namespace storm {
             std::string parametricToken = "param";
 
             std::ifstream file;
-            file.exceptions ( std::ifstream::failbit );
-            try {
-                file.open(filename);
-            }
-            catch (std::ifstream::failure e) {
-                STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Exception during file opening on " << filename << ".");
-                return;
-            }
-            file.exceptions( std::ifstream::goodbit );
-
+            storm::utility::openFile(filename, file);
             std::string line;
-            while(std::getline(file, line)) {
+
+            while (std::getline(file, line)) {
                 bool success = true;
                 STORM_LOG_TRACE("Parsing: " << line);
                 size_t commentstarts = line.find("//");
@@ -143,7 +136,7 @@ namespace storm {
             if(!builder.setTopLevel(toplevelId)) {
                 STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Top level id unknown.");
             }
-            file.close();
+            storm::utility::closeFile(file);
         }
 
         template<typename ValueType>

src/storm-dft/parser/DFTJsonParser.cpp

@@ -10,6 +10,7 @@
 #include "storm/exceptions/FileIoException.h"
 #include "storm/exceptions/NotSupportedException.h"
 #include "storm/utility/macros.h"
+#include "storm/utility/file.h"
 
 namespace storm {
     namespace parser {
@@ -52,19 +53,10 @@ namespace storm {
             STORM_LOG_DEBUG("Parsing from JSON");
 
             std::ifstream file;
-            file.exceptions ( std::ifstream::failbit );
-            try {
-                file.open(filename);
-            }
-            catch (std::ifstream::failure e) {
-                STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Exception during file opening on " << filename << ".");
-                return;
-            }
-            file.exceptions( std::ifstream::goodbit );
-
+            storm::utility::openFile(filename, file);
             json parsedJson;
             parsedJson << file;
-            file.close();
+            storm::utility::closeFile(file);
 
             // Start by building mapping from ids to names
             std::map<std::string, std::string> nameMapping;

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

@@ -56,19 +56,19 @@ void initializeSettings() {
 std::unordered_map<std::string, uint64_t> parseCapacitiesList(std::string const& filename) {
     std::unordered_map<std::string, uint64_t> map;
     
-    std::ifstream ifs;
-    ifs.open(filename);
+    std::ifstream stream;
+    storm::utility::openFile(filename, stream);
     
     std::string line;
-    while( std::getline(ifs, line) ) {
+    while ( std::getline(stream, line) ) {
         std::vector<std::string> strs;
         boost::split(strs, line, boost::is_any_of("\t "));
         STORM_LOG_THROW(strs.size() == 2, storm::exceptions::WrongFormatException, "Expect key value pairs");
         std::cout << std::stoll(strs[1]) << std::endl;
         map[strs[0]] = std::stoll(strs[1]);
     }
+    storm::utility::closeFile(stream);
     return map;
-    
 }
 
 

src/storm-gspn/storm-gspn.h

@@ -8,6 +8,8 @@
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/GSPNExportSettings.h"
 
+#include "storm/utility/file.h"
+
 namespace storm {
     /**
      *    Builds JANI model from GSPN.
@@ -21,23 +23,23 @@ namespace storm {
         storm::settings::modules::GSPNExportSettings const& exportSettings = storm::settings::getModule<storm::settings::modules::GSPNExportSettings>();
         if (exportSettings.isWriteToDotSet()) {
             std::ofstream fs;
-            fs.open(exportSettings.getWriteToDotFilename());
+            storm::utility::openFile(exportSettings.getWriteToDotFilename(), fs);
             gspn.writeDotToStream(fs);
-            fs.close();
+            storm::utility::closeFile(fs);
         }
         
         if (exportSettings.isWriteToPnproSet()) {
             std::ofstream fs;
-            fs.open(exportSettings.getWriteToPnproFilename());
+            storm::utility::openFile(exportSettings.getWriteToPnproFilename(), fs);
             gspn.toPnpro(fs);
-            fs.close();
+            storm::utility::closeFile(fs);
         }
         
         if (exportSettings.isWriteToPnmlSet()) {
             std::ofstream fs;
-            fs.open(exportSettings.getWriteToPnmlFilename());
+            storm::utility::openFile(exportSettings.getWriteToPnmlFilename(), fs);
             gspn.toPnml(fs);
-            fs.close();
+            storm::utility::closeFile(fs);
         }
         
         if (exportSettings.isDisplayStatsSet()) {
@@ -48,13 +50,13 @@ namespace storm {
         
         if (exportSettings.isWriteStatsToFileSet()) {
             std::ofstream fs;
-            fs.open(exportSettings.getWriteStatsFilename());
+            storm::utility::openFile(exportSettings.getWriteStatsFilename(), fs);
             gspn.writeStatsToStream(fs);
-            fs.close();
+            storm::utility::closeFile(fs);
         }
         
         
         
     }
     
-}
+}

src/storm-pgcl-cli/storm-pgcl.cpp

@@ -47,13 +47,10 @@ void handleJani(storm::jani::Model& model) {
 
 void programGraphToDotFile(storm::ppg::ProgramGraph const& prog) {
     std::string filepath = storm::settings::getModule<storm::settings::modules::PGCLSettings>().getProgramGraphDotOutputFilename();
-    std::ofstream ofs;
-    ofs.open(filepath, std::ofstream::out );
-    if (ofs.is_open()) {
-        prog.printDot(ofs);
-    } else {
-        STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Cannot open " << filepath);
-    }
+    std::ofstream stream;
+    storm::utility::openFile(filepath, stream);
+    prog.printDot(stream);
+    storm::utility::closeFile(stream);
 }
 
 int main(const int argc, const char** argv) {

src/storm-pgcl/parser/PgclParser.cpp

@@ -1,6 +1,7 @@
 #include "PgclParser.h"
 // If the parser fails due to ill-formed data, this exception is thrown.
 #include "storm/exceptions/WrongFormatException.h"
+#include "storm/utility/file.h"
 
 namespace storm {
     namespace parser {
@@ -9,8 +10,8 @@ namespace storm {
             storm::pgcl::PgclProgram result;
 
             // Open file and initialize result.
-            std::ifstream inputFileStream(filename, std::ios::in);
-            STORM_LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'.");
+            std::ifstream inputFileStream;
+            storm::utility::openFile(filename, inputFileStream);
             
             // Now try to parse the contents of the file.
             try {
@@ -18,12 +19,12 @@ namespace storm {
                 result = parseFromString(fileContent, filename);
             } catch(std::exception& e) {
                 // In case of an exception properly close the file before passing exception.
-                inputFileStream.close();
+                storm::utility::closeFile(inputFileStream);
                 throw e;
             }
             
             // Close the stream in case everything went smoothly and return result.
-            inputFileStream.close();
+            storm::utility::closeFile(inputFileStream);
             return result;
         }
         

src/storm/abstraction/MenuGameAbstractor.cpp

@@ -7,6 +7,7 @@
 #include "storm/storage/dd/Add.h"
 #include "storm/storage/dd/Bdd.h"
 #include "storm/utility/dd.h"
+#include "storm/utility/file.h"
 
 #include "storm-config.h"
 #include "storm/adapters/CarlAdapter.h"
@@ -47,7 +48,8 @@ namespace storm {
         template <storm::dd::DdType DdType, typename ValueType>
         void MenuGameAbstractor<DdType, ValueType>::exportToDot(storm::abstraction::MenuGame<DdType, ValueType> const& currentGame, std::string const& filename, storm::dd::Bdd<DdType> const& highlightStatesBdd, storm::dd::Bdd<DdType> const& filter) const {
 
-            std::ofstream out(filename);
+            std::ofstream out;
+            storm::utility::openFile(filename, out);
             AbstractionInformation<DdType> const& abstractionInformation = this->getAbstractionInformation();
             
             storm::dd::Add<DdType, ValueType> filteredTransitions = filter.template toAdd<ValueType>() * currentGame.getTransitionMatrix();
@@ -130,6 +132,7 @@ namespace storm {
             }
             
             out << "}" << std::endl;
+            storm::utility::closeFile(out);
         }
         
         template class MenuGameAbstractor<storm::dd::DdType::CUDD, double>;

src/storm/builder/DdJaniModelBuilder.cpp

@@ -518,7 +518,7 @@ namespace storm {
             result.setValue(metaVariableNameToValueMap, 1);
             return result;
         }
-                
+        
         template <storm::dd::DdType Type, typename ValueType>
         class CombinedEdgesSystemComposer : public SystemComposer<Type, ValueType> {
         public:
@@ -606,9 +606,53 @@ namespace storm {
                 bool inputEnabled;
             };
             
+            struct ActionIdentification {
+                ActionIdentification(uint64_t actionIndex) : actionIndex(actionIndex), synchronizationVectorIndex(boost::none) {
+                    // Intentionally left empty.
+                }
+                
+                ActionIdentification(uint64_t actionIndex, uint64_t synchronizationVectorIndex) : actionIndex(actionIndex), synchronizationVectorIndex(synchronizationVectorIndex) {
+                    // Intentionally left empty.
+                }
+                
+                ActionIdentification(uint64_t actionIndex, boost::optional<uint64_t> synchronizationVectorIndex) : actionIndex(actionIndex), synchronizationVectorIndex(synchronizationVectorIndex) {
+                    // Intentionally left empty.
+                }
+                
+                bool operator==(ActionIdentification const& other) const {
+                    bool result = actionIndex == other.actionIndex;
+                    if (synchronizationVectorIndex) {
+                        if (other.synchronizationVectorIndex) {
+                            result &= synchronizationVectorIndex.get() == other.synchronizationVectorIndex.get();
+                        } else {
+                            result = false;
+                        }
+                    } else {
+                        if (other.synchronizationVectorIndex) {
+                            result = false;
+                        }
+                    }
+                    return result;
+                }
+                
+                uint64_t actionIndex;
+                boost::optional<uint64_t> synchronizationVectorIndex;
+            };
+            
+            struct ActionIdentificationHash {
+                std::size_t operator()(ActionIdentification const& identification) const {
+                    std::size_t seed = 0;
+                    boost::hash_combine(seed, identification.actionIndex);
+                    if (identification.synchronizationVectorIndex) {
+                        boost::hash_combine(seed, identification.synchronizationVectorIndex.get());
+                    }
+                    return seed;
+                }
+            };
+            
             // This structure represents a subcomponent of a composition.
             struct AutomatonDd {
-                AutomatonDd(storm::dd::Add<Type, ValueType> const& identity, std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> const& transientLocationAssignments = {}) : actionIndexToAction(), transientLocationAssignments(transientLocationAssignments), identity(identity), localNondeterminismVariables(std::make_pair<uint64_t, uint64_t>(0, 0)) {
+                AutomatonDd(storm::dd::Add<Type, ValueType> const& identity, std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> const& transientLocationAssignments = {}) : actions(), transientLocationAssignments(transientLocationAssignments), identity(identity), localNondeterminismVariables(std::make_pair<uint64_t, uint64_t>(0, 0)) {
                     // Intentionally left empty.
                 }
                 
@@ -633,8 +677,8 @@ namespace storm {
                     setHighestLocalNondeterminismVariable(std::max(localNondeterminismVariables.second, getHighestLocalNondeterminismVariable()));
                 }
                 
-                // A mapping from action indices to the action DDs.
-                std::map<uint64_t, ActionDd> actionIndexToAction;
+                // A mapping from action identifications to the action DDs.
+                std::unordered_map<ActionIdentification, ActionDd, ActionIdentificationHash> actions;
                 
                 // A mapping from transient variables to their location-based transient assignment values.
                 std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> transientLocationAssignments;
@@ -644,7 +688,6 @@ namespace storm {
                 
                 // The local nondeterminism variables used by this action DD, given as the lowest and highest variable index.
                 std::pair<uint64_t, uint64_t> localNondeterminismVariables;
-
             };
             
             CombinedEdgesSystemComposer(storm::jani::Model const& model, storm::jani::CompositionInformation const& actionInformation, CompositionVariables<Type, ValueType> const& variables, std::vector<storm::expressions::Variable> const& transientVariables) : SystemComposer<Type, ValueType>(model, variables, transientVariables), actionInformation(actionInformation) {
@@ -654,208 +697,192 @@ namespace storm {
             storm::jani::CompositionInformation const& actionInformation;
 
             ComposerResult<Type, ValueType> compose() override {
-                std::map<uint64_t, uint64_t> actionIndexToLocalNondeterminismVariableOffset;
-                for (auto const& actionIndex : actionInformation.getNonSilentActionIndices()) {
-                    actionIndexToLocalNondeterminismVariableOffset[actionIndex] = 0;
-                }
-                actionIndexToLocalNondeterminismVariableOffset[storm::jani::Model::SILENT_ACTION_INDEX] = 0;
-
-                AutomatonDd globalAutomaton = boost::any_cast<AutomatonDd>(this->model.getSystemComposition().accept(*this, actionIndexToLocalNondeterminismVariableOffset));
+                STORM_LOG_THROW(this->model.hasStandardCompliantComposition(), storm::exceptions::WrongFormatException, "Model builder only supports non-nested parallel compositions.");
+                AutomatonDd globalAutomaton = boost::any_cast<AutomatonDd>(this->model.getSystemComposition().accept(*this, boost::any()));
                 return buildSystemFromAutomaton(globalAutomaton);
             }
             
+            struct ActionInstantiation {
+                ActionInstantiation(uint64_t actionIndex, uint64_t synchronizationVectorIndex, uint64_t localNondeterminismVariableOffset) : actionIndex(actionIndex), synchronizationVectorIndex(synchronizationVectorIndex), localNondeterminismVariableOffset(localNondeterminismVariableOffset) {
+                    // Intentionally left empty.
+                }
+
+                ActionInstantiation(uint64_t actionIndex, uint64_t localNondeterminismVariableOffset) : actionIndex(actionIndex), localNondeterminismVariableOffset(localNondeterminismVariableOffset) {
+                    // Intentionally left empty.
+                }
+
+                bool operator==(ActionInstantiation const& other) const {
+                    bool result = actionIndex == other.actionIndex;
+                    result &= localNondeterminismVariableOffset == other.localNondeterminismVariableOffset;
+                    if (synchronizationVectorIndex) {
+                        if (!other.synchronizationVectorIndex) {
+                            result = false;
+                        } else {
+                            result &= synchronizationVectorIndex.get() == other.synchronizationVectorIndex.get();
+                        }
+                    } else {
+                        if (other.synchronizationVectorIndex) {
+                            result = false;
+                        }
+                    }
+                    return result;
+                }
+                
+                uint64_t actionIndex;
+                boost::optional<uint64_t> synchronizationVectorIndex;
+                uint64_t localNondeterminismVariableOffset;
+            };
+            
+            struct ActionInstantiationHash {
+                std::size_t operator()(ActionInstantiation const& instantiation) const {
+                    std::size_t seed = 0;
+                    boost::hash_combine(seed, instantiation.actionIndex);
+                    boost::hash_combine(seed, instantiation.localNondeterminismVariableOffset);
+                    if (instantiation.synchronizationVectorIndex) {
+                        boost::hash_combine(seed, instantiation.synchronizationVectorIndex.get());
+                    }
+                    return seed;
+                }
+            };
+            
+            typedef std::map<uint64_t, std::vector<ActionInstantiation>> ActionInstantiations;
+            
             boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override {
-                std::map<uint64_t, uint64_t> const& actionIndexToLocalNondeterminismVariableOffset = boost::any_cast<std::map<uint_fast64_t, uint_fast64_t> const&>(data);
+                ActionInstantiations actionInstantiations;
+                if (data.empty()) {
+                    // If no data was provided, this is the top level element in which case we build the full automaton.
+                    for (auto const& actionIndex : actionInformation.getNonSilentActionIndices()) {
+                        actionInstantiations[actionIndex].emplace_back(actionIndex, 0);
+                    }
+                    actionInstantiations[storm::jani::Model::SILENT_ACTION_INDEX].emplace_back(storm::jani::Model::SILENT_ACTION_INDEX, 0);
+                }
                 
                 std::set<uint64_t> inputEnabledActionIndices;
                 for (auto const& actionName : composition.getInputEnabledActions()) {
                     inputEnabledActionIndices.insert(actionInformation.getActionIndex(actionName));
                 }
                 
-                return buildAutomatonDd(composition.getAutomatonName(), actionIndexToLocalNondeterminismVariableOffset, inputEnabledActionIndices);
+                return buildAutomatonDd(composition.getAutomatonName(), data.empty() ? actionInstantiations : boost::any_cast<ActionInstantiations const&>(data), inputEnabledActionIndices);
             }
             
             boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override {
-                std::map<uint64_t, uint64_t> const& actionIndexToLocalNondeterminismVariableOffset = boost::any_cast<std::map<uint64_t, uint64_t> const&>(data);
-                
+                STORM_LOG_ASSERT(data.empty(), "Expected parallel composition to be on topmost level to be JANI compliant.");
+
+                // Prepare storage for the subautomata of the composition.
                 std::vector<AutomatonDd> subautomata;
+
+                // The outer loop iterates over the indices of the subcomposition, because the first subcomposition needs
+                // to be built before the second and so on.
+                uint64_t silentActionIndex = actionInformation.getActionIndex(storm::jani::Model::SILENT_ACTION_NAME);
                 for (uint64_t subcompositionIndex = 0; subcompositionIndex < composition.getNumberOfSubcompositions(); ++subcompositionIndex) {
-                    // Prepare the new offset mapping.
-                    std::map<uint64_t, uint64_t> newSynchronizingActionToOffsetMap = actionIndexToLocalNondeterminismVariableOffset;
+                    // Now build a new set of action instantiations for the current subcomposition index.
+                    ActionInstantiations actionInstantiations;
+                    actionInstantiations[silentActionIndex].emplace_back(silentActionIndex, 0);
                     
-                    if (subcompositionIndex == 0) {
-                        for (auto const& synchVector : composition.getSynchronizationVectors()) {
-                            auto it = actionIndexToLocalNondeterminismVariableOffset.find(actionInformation.getActionIndex(synchVector.getOutput()));
-                            STORM_LOG_THROW(it != actionIndexToLocalNondeterminismVariableOffset.end(), storm::exceptions::InvalidArgumentException, "Invalid action " << synchVector.getOutput() << ".");
-                            if (synchVector.getInput(0) != storm::jani::SynchronizationVector::NO_ACTION_INPUT) {
-                                newSynchronizingActionToOffsetMap[actionInformation.getActionIndex(synchVector.getInput(0))] = it->second;
-                            }
-                        }
-                    } else {
-                        // Based on the previous results, we need to update the offsets.
-                        for (auto const& synchVector : composition.getSynchronizationVectors()) {
-                            if (synchVector.getInput(subcompositionIndex) != storm::jani::SynchronizationVector::NO_ACTION_INPUT) {
-                                boost::optional<uint64_t> previousActionPosition = synchVector.getPositionOfPrecedingParticipatingAction(subcompositionIndex);
-                                if (previousActionPosition) {
-                                    AutomatonDd const& previousAutomatonDd = subautomata[previousActionPosition.get()];
+                    for (uint64_t synchronizationVectorIndex = 0; synchronizationVectorIndex < composition.getNumberOfSynchronizationVectors(); ++synchronizationVectorIndex) {
+                        auto const& synchVector = composition.getSynchronizationVector(synchronizationVectorIndex);
+                        
+                        // Determine the first participating subcomposition, because we need to build the corresponding action
+                        // from all local nondeterminism variable offsets that the output action of the synchronization vector
+                        // is required to have.
+                        if (subcompositionIndex == synchVector.getPositionOfFirstParticipatingAction()) {
+                            uint64_t actionIndex = actionInformation.getActionIndex(synchVector.getInput(subcompositionIndex));
+                            actionInstantiations[actionIndex].emplace_back(actionIndex, synchronizationVectorIndex, 0);
+                        } else if (synchVector.getInput(subcompositionIndex) != storm::jani::SynchronizationVector::NO_ACTION_INPUT) {
+                            uint64_t actionIndex = actionInformation.getActionIndex(synchVector.getInput(subcompositionIndex));
 
-                                    std::string const& previousAction = synchVector.getInput(previousActionPosition.get());
-                                    auto it = previousAutomatonDd.actionIndexToAction.find(actionInformation.getActionIndex(previousAction));
-                                    if (it != previousAutomatonDd.actionIndexToAction.end()) {
-                                        newSynchronizingActionToOffsetMap[actionInformation.getActionIndex(synchVector.getInput(subcompositionIndex))] = it->second.getHighestLocalNondeterminismVariable();
-                                    } else {
-                                        STORM_LOG_ASSERT(false, "Subcomposition does not have action that is mentioned in parallel composition.");
-                                    }
-                                }
-                            }
+                            // If this subcomposition is participating in the synchronization vector, but it's not the first
+                            // such subcomposition, then we have to retrieve the offset we need for the participating action
+                            // by looking at the maximal offset used by the preceding participating action.
+                            boost::optional<uint64_t> previousActionPosition = synchVector.getPositionOfPrecedingParticipatingAction(subcompositionIndex);
+                            STORM_LOG_ASSERT(previousActionPosition, "Inconsistent information about synchronization vector.");
+                            AutomatonDd const& previousAutomatonDd = subautomata[previousActionPosition.get()];
+                            auto precedingActionIt = previousAutomatonDd.actions.find(ActionIdentification(actionInformation.getActionIndex(synchVector.getInput(previousActionPosition.get())), synchronizationVectorIndex));
+                            STORM_LOG_THROW(precedingActionIt != previousAutomatonDd.actions.end(), storm::exceptions::WrongFormatException, "Subcomposition does not have action that is mentioned in parallel composition.");
+                            actionInstantiations[actionIndex].emplace_back(actionIndex, synchronizationVectorIndex, precedingActionIt->second.getHighestLocalNondeterminismVariable());
                         }
                     }
                     
-                    // Build the DD for the next element of the composition wrt. to the current offset mapping.
-                    subautomata.push_back(boost::any_cast<AutomatonDd>(composition.getSubcomposition(subcompositionIndex).accept(*this, newSynchronizingActionToOffsetMap)));
+                    subautomata.push_back(boost::any_cast<AutomatonDd>(composition.getSubcomposition(subcompositionIndex).accept(*this, actionInstantiations)));
                 }
-                
+
                 return composeInParallel(subautomata, composition.getSynchronizationVectors());
             }
             
         private:
             AutomatonDd composeInParallel(std::vector<AutomatonDd> const& subautomata, std::vector<storm::jani::SynchronizationVector> const& synchronizationVectors) {
-                typedef storm::dd::Add<Type, ValueType> IdentityAdd;
-                typedef std::pair<ActionDd, IdentityAdd> ActionAndAutomatonIdentity;
-                typedef std::vector<ActionAndAutomatonIdentity> ActionAndAutomatonIdentities;
-                typedef std::vector<boost::optional<std::pair<ActionAndAutomatonIdentities, IdentityAdd>>> SynchronizationVectorActionsAndIdentities;
-                
                 AutomatonDd result(this->variables.manager->template getAddOne<ValueType>());
-                
-                std::map<uint64_t, std::vector<ActionDd>> nonSynchronizingActions;
-                SynchronizationVectorActionsAndIdentities synchronizationVectorActions(synchronizationVectors.size(), boost::none);
-                for (uint64_t automatonIndex = 0; automatonIndex < subautomata.size(); ++automatonIndex) {
-                    AutomatonDd const& subautomaton = subautomata[automatonIndex];
-                    
-                    // Add the transient assignments from the new subautomaton.
-                    addToTransientAssignmentMap(result.transientLocationAssignments, subautomaton.transientLocationAssignments);
-                    
-                    // Initilize the used local nondeterminism variables appropriately.
-                    if (automatonIndex == 0) {
-                        result.setLowestLocalNondeterminismVariable(subautomaton.getLowestLocalNondeterminismVariable());
-                        result.setHighestLocalNondeterminismVariable(subautomaton.getHighestLocalNondeterminismVariable());
-                    }
-
-                    // Compose the actions according to the synchronization vectors.
-                    std::set<uint64_t> actionsInSynch;
-                    for (uint64_t synchVectorIndex = 0; synchVectorIndex < synchronizationVectors.size(); ++synchVectorIndex) {
-                        auto const& synchVector = synchronizationVectors[synchVectorIndex];
-                        
-                        if (synchVector.isNoActionInput(synchVector.getInput(automatonIndex))) {
-                            if (automatonIndex == 0) {
-                                // Create a new action that is the identity over the first automaton.
-                                synchronizationVectorActions[synchVectorIndex] = std::make_pair(ActionAndAutomatonIdentities{std::make_pair(ActionDd(this->variables.manager->template getAddOne<ValueType>(), subautomaton.identity, {}, subautomaton.localNondeterminismVariables, {}, this->variables.manager->getBddZero()), subautomaton.identity)}, this->variables.manager->template getAddOne<ValueType>());
-                            } else {
-                                // If there is no action in the output spot, this means that some other subcomposition did
-                                // not provide the action necessary for the synchronization vector to resolve.
-                                if (synchronizationVectorActions[synchVectorIndex]) {
-                                    synchronizationVectorActions[synchVectorIndex].get().second *= subautomaton.identity;
-                                }
-                            }
-                        } else {
-                            // Determine the indices of input (at the current automaton position) and the output.
-                            uint64_t inputActionIndex = actionInformation.getActionIndex(synchVector.getInput(automatonIndex));
-                            actionsInSynch.insert(inputActionIndex);
-                            
-                            // Either set the action (if it's the first of the ones to compose) or compose the actions directly.
-                            if (automatonIndex == 0) {
-                                // If the action cannot be found, the particular spot in the output will be left empty.
-                                auto inputActionIt = subautomaton.actionIndexToAction.find(inputActionIndex);
-                                if (inputActionIt != subautomaton.actionIndexToAction.end()) {
-                                    synchronizationVectorActions[synchVectorIndex] = std::make_pair(ActionAndAutomatonIdentities{std::make_pair(inputActionIt->second, subautomaton.identity)}, this->variables.manager->template getAddOne<ValueType>());
-                                }
-                            } else {
-                                // If there is no action in the output spot, this means that some other subcomposition did
-                                // not provide the action necessary for the synchronization vector to resolve.
-                                if (synchronizationVectorActions[synchVectorIndex]) {
-                                    auto inputActionIt = subautomaton.actionIndexToAction.find(inputActionIndex);
-                                    if (inputActionIt != subautomaton.actionIndexToAction.end()) {
-                                        synchronizationVectorActions[synchVectorIndex].get().first.push_back(std::make_pair(inputActionIt->second, subautomaton.identity));
-                                    } else {
-                                        // If the current subcomposition does not provide the required action for the synchronization
-                                        // vector, we clear the action.
-                                        synchronizationVectorActions[synchVectorIndex] = boost::none;
-                                    }
-                                }
-                            }
-                        }
-                    }
 
-                    // Now treat all unsynchronizing actions.
-                    if (automatonIndex == 0) {
-                        // Since it's the first automaton, there is nothing to combine.
-                        for (auto const& action : subautomaton.actionIndexToAction) {
-                            if (actionsInSynch.find(action.first) == actionsInSynch.end()) {
-                                nonSynchronizingActions[action.first].push_back(action.second);
-                            }
-                        }
-                    } else {
-                        // Extend all other non-synchronizing actions with the identity of the current subautomaton.
-                        for (auto& actions : nonSynchronizingActions) {
-                            for (auto& action : actions.second) {
-                                STORM_LOG_TRACE("Extending action '" << actionInformation.getActionName(actions.first) << "' with identity of next composition.");
-                                action.transitions *= subautomaton.identity;
-                            }
-                        }
-                        
-                        // Extend the actions of the current subautomaton with the identity of the previous system and
-                        // add it to the overall non-synchronizing action result.
-                        for (auto const& action : subautomaton.actionIndexToAction) {
-                            if (actionsInSynch.find(action.first) == actionsInSynch.end()) {
-                                STORM_LOG_TRACE("Adding action " << actionInformation.getActionName(action.first) << " to non-synchronizing actions and multiply it with system identity.");
-                                nonSynchronizingActions[action.first].push_back(action.second.multiplyTransitions(result.identity));
-                            }
-                        }
-                    }
+                // Build the results of the synchronization vectors.
+                std::map<uint64_t, std::vector<ActionDd>> actions;
+                for (uint64_t synchronizationVectorIndex = 0; synchronizationVectorIndex < synchronizationVectors.size(); ++synchronizationVectorIndex) {
+                    auto const& synchVector = synchronizationVectors[synchronizationVectorIndex];
                     
-                    // Finally, construct combined identity.
-                    result.identity *= subautomaton.identity;
+                    boost::optional<ActionDd> synchronizingAction = combineSynchronizingActions(subautomata, synchVector, synchronizationVectorIndex);
+                    if (synchronizingAction) {
+                        actions[actionInformation.getActionIndex(synchVector.getOutput())].emplace_back(synchronizingAction.get());
+                    }
                 }
                 
-                // Add the results of the synchronization vectors to that of the non-synchronizing actions.
-                for (uint64_t synchVectorIndex = 0; synchVectorIndex < synchronizationVectors.size(); ++synchVectorIndex) {
-                    auto const& synchVector = synchronizationVectors[synchVectorIndex];
+                // Construct the silent action DDs.
+                std::vector<ActionDd> silentActionDds;
+                for (auto const& automaton : subautomata) {
+                    for (auto& actionDd : silentActionDds) {
+                        STORM_LOG_TRACE("Extending previous silent action by identity of current automaton.");
+                        actionDd = actionDd.multiplyTransitions(automaton.identity);
+                    }
                     
-                    // If there is an action resulting from this combination of actions, add it to the output action.
-                    if (synchronizationVectorActions[synchVectorIndex]) {
-                        uint64_t outputActionIndex = actionInformation.getActionIndex(synchVector.getOutput());
-                        nonSynchronizingActions[outputActionIndex].push_back(combineSynchronizingActions(synchronizationVectorActions[synchVectorIndex].get().first, synchronizationVectorActions[synchVectorIndex].get().second));
+                    ActionIdentification silentActionIdentification(storm::jani::Model::SILENT_ACTION_INDEX);
+                    auto silentActionIt = automaton.actions.find(silentActionIdentification);
+                    if (silentActionIt != automaton.actions.end()) {
+                        STORM_LOG_TRACE("Extending silent action by running identity.");
+                        silentActionDds.emplace_back(silentActionIt->second.multiplyTransitions(result.identity));
                     }
+
+                    result.identity *= automaton.identity;
                 }
                 
-                // Now that we have built the individual action DDs for all resulting actions, we need to combine them
-                // in an unsynchronizing way.
-                for (auto const& nonSynchronizingActionDds : nonSynchronizingActions) {
-                    std::vector<ActionDd> const& actionDds = nonSynchronizingActionDds.second;
-                    if (actionDds.size() > 1) {
-                        ActionDd combinedAction = combineUnsynchronizedActions(actionDds);
-                        result.actionIndexToAction[nonSynchronizingActionDds.first] = combinedAction;
-                        result.extendLocalNondeterminismVariables(combinedAction.getLocalNondeterminismVariables());
-                    } else {
-                        result.actionIndexToAction[nonSynchronizingActionDds.first] = actionDds.front();
-                        result.extendLocalNondeterminismVariables(actionDds.front().getLocalNondeterminismVariables());
-                    }
+                if (!silentActionDds.empty()) {
+                    auto& allSilentActionDds = actions[storm::jani::Model::SILENT_ACTION_INDEX];
+                    allSilentActionDds.insert(actions[storm::jani::Model::SILENT_ACTION_INDEX].end(), silentActionDds.begin(), silentActionDds.end());
                 }
                 
+                // Finally, combine (potential) multiple action DDs.
+                for (auto const& actionDds : actions) {
+                    ActionDd combinedAction = actionDds.second.size() > 1 ? combineUnsynchronizedActions(actionDds.second) : actionDds.second.front();
+                    result.actions[ActionIdentification(actionDds.first)] = combinedAction;
+                    result.extendLocalNondeterminismVariables(combinedAction.getLocalNondeterminismVariables());
+                }
+            
+                // Construct combined identity.
+                for (auto const& subautomaton : subautomata) {
+                    result.identity *= subautomaton.identity;
+                }
+
                 return result;
             }
             
-            ActionDd combineSynchronizingActions(std::vector<std::pair<ActionDd, storm::dd::Add<Type, ValueType>>> const& actionsAndIdentities, storm::dd::Add<Type, ValueType> const& nonSynchronizingAutomataIdentities) {
-                // If there is just one action, no need to combine anything.
-                if (actionsAndIdentities.size() == 1) {
-                    return actionsAndIdentities.front().first;
+            boost::optional<ActionDd> combineSynchronizingActions(std::vector<AutomatonDd> const& subautomata, storm::jani::SynchronizationVector const& synchronizationVector, uint64_t synchronizationVectorIndex) {
+                std::vector<std::pair<uint64_t, std::reference_wrapper<ActionDd const>>> actions;
+                storm::dd::Add<Type, ValueType> nonSynchronizingIdentity = this->variables.manager->template getAddOne<ValueType>();
+                for (uint64_t subautomatonIndex = 0; subautomatonIndex < subautomata.size(); ++subautomatonIndex) {
+                    auto const& subautomaton = subautomata[subautomatonIndex];
+                    if (synchronizationVector.getInput(subautomatonIndex) != storm::jani::SynchronizationVector::NO_ACTION_INPUT) {
+                        auto it = subautomaton.actions.find(ActionIdentification(actionInformation.getActionIndex(synchronizationVector.getInput(subautomatonIndex)), synchronizationVectorIndex));
+                        if (it != subautomaton.actions.end()) {
+                            actions.emplace_back(subautomatonIndex, it->second);
+                        } else {
+                            return boost::none;
+                        }
+                    } else {
+                        nonSynchronizingIdentity *= subautomaton.identity;
+                    }
                 }
                 
                 // If there are only input-enabled actions, we also need to build the disjunction of the guards.
                 bool allActionsInputEnabled = true;
-                for (auto const& actionIdentityPair : actionsAndIdentities) {
-                    auto const& action = actionIdentityPair.first;
-                    if (!action.isInputEnabled()) {
+                for (auto const& action : actions) {
+                    if (!action.second.get().isInputEnabled()) {
                         allActionsInputEnabled = false;
                     }
                 }
@@ -875,12 +902,13 @@ namespace storm {
                 storm::dd::Add<Type, ValueType> transitions = this->variables.manager->template getAddOne<ValueType>();
                 std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> transientEdgeAssignments;
                 
-                uint64_t lowestNondeterminismVariable = actionsAndIdentities.front().first.getLowestLocalNondeterminismVariable();
-                uint64_t highestNondeterminismVariable = actionsAndIdentities.front().first.getHighestLocalNondeterminismVariable();
+                uint64_t lowestNondeterminismVariable = actions.front().second.get().getLowestLocalNondeterminismVariable();
+                uint64_t highestNondeterminismVariable = actions.front().second.get().getHighestLocalNondeterminismVariable();
                 
                 storm::dd::Bdd<Type> newIllegalFragment = this->variables.manager->getBddZero();
-                for (auto const& actionIdentityPair : actionsAndIdentities) {
-                    auto const& action = actionIdentityPair.first;
+                for (auto const& actionIndexPair : actions) {
+                    auto componentIndex = actionIndexPair.first;
+                    auto const& action = actionIndexPair.second.get();
                     storm::dd::Bdd<Type> actionGuard = action.guard.toBdd();
                     if (guardDisjunction) {
                         guardDisjunction.get() |= actionGuard;
@@ -892,7 +920,7 @@ namespace storm {
                     
                     if (action.isInputEnabled()) {
                         // If the action is input-enabled, we add self-loops to all states.
-                        transitions *= actionGuard.ite(action.transitions, encodeIndex(0, action.getLowestLocalNondeterminismVariable(), action.getHighestLocalNondeterminismVariable() - action.getLowestLocalNondeterminismVariable(), this->variables) * actionIdentityPair.second);
+                        transitions *= actionGuard.ite(action.transitions, encodeIndex(0, action.getLowestLocalNondeterminismVariable(), action.getHighestLocalNondeterminismVariable() - action.getLowestLocalNondeterminismVariable(), this->variables) * subautomata[componentIndex].identity);
                     } else {
                         transitions *= action.transitions;
                     }
@@ -948,7 +976,7 @@ namespace storm {
                 // such a combined transition.
                 illegalFragment &= inputEnabledGuard;
                 
-                return ActionDd(inputEnabledGuard.template toAdd<ValueType>(), transitions * nonSynchronizingAutomataIdentities, transientEdgeAssignments, std::make_pair(lowestNondeterminismVariable, highestNondeterminismVariable), globalVariableToWritingFragment, illegalFragment);
+                return ActionDd(inputEnabledGuard.template toAdd<ValueType>(), transitions * nonSynchronizingIdentity, transientEdgeAssignments, std::make_pair(lowestNondeterminismVariable, highestNondeterminismVariable), globalVariableToWritingFragment, illegalFragment);
             }
             
             ActionDd combineUnsynchronizedActions(ActionDd action1, ActionDd action2, storm::dd::Add<Type, ValueType> const& identity1, storm::dd::Add<Type, ValueType> const& identity2) {
@@ -1141,7 +1169,7 @@ namespace storm {
 
                 bool overlappingGuards = false;
                 for (auto const& edge : edgeDds) {
-                    STORM_LOG_THROW(edge.isMarkovian, storm::exceptions::InvalidArgumentException, "Can only combine Markovian edges.");
+                    STORM_LOG_THROW(edge.isMarkovian, storm::exceptions::WrongFormatException, "Can only combine Markovian edges.");
                     
                     if (!overlappingGuards) {
                         overlappingGuards |= !(guard && edge.guard.toBdd()).isZero();
@@ -1197,7 +1225,7 @@ namespace storm {
                         }
                         return combineEdgesToActionNondeterministic(nonMarkovianEdges, markovianEdge, localNondeterminismVariableOffset);
                     } else {
-                        STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot translate model of this type.");
+                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Cannot translate model of this type.");
                     }
                 } else {
                     return ActionDd(this->variables.manager->template getAddZero<ValueType>(), this->variables.manager->template getAddZero<ValueType>(), {}, std::make_pair<uint64_t, uint64_t>(0, 0), {}, this->variables.manager->getBddZero());
@@ -1479,23 +1507,30 @@ namespace storm {
                 }
             }
             
-            AutomatonDd buildAutomatonDd(std::string const& automatonName, std::map<uint_fast64_t, uint_fast64_t> const& actionIndexToLocalNondeterminismVariableOffset, std::set<uint64_t> const& inputEnabledActionIndices) {
+            AutomatonDd buildAutomatonDd(std::string const& automatonName, ActionInstantiations const& actionInstantiations, std::set<uint64_t> const& inputEnabledActionIndices) {
+                STORM_LOG_TRACE("Building DD for automaton '" << automatonName << "'.");
                 AutomatonDd result(this->variables.automatonToIdentityMap.at(automatonName));
                 
                 storm::jani::Automaton const& automaton = this->model.getAutomaton(automatonName);
-                for (auto const& action : this->model.getActions()) {
-                    uint64_t actionIndex = this->model.getActionIndex(action.getName());
+                for (auto const& actionInstantiation : actionInstantiations) {
+                    uint64_t actionIndex = actionInstantiation.first;
                     if (!automaton.hasEdgeLabeledWithActionIndex(actionIndex)) {
                         continue;
                     }
-                    ActionDd actionDd = buildActionDdForActionIndex(automaton, actionIndex, actionIndexToLocalNondeterminismVariableOffset.at(actionIndex));
+                    bool inputEnabled = false;
                     if (inputEnabledActionIndices.find(actionIndex) != inputEnabledActionIndices.end()) {
-                        actionDd.setIsInputEnabled();
+                        inputEnabled = true;
+                    }
+                    for (auto const& instantiationOffset : actionInstantiation.second) {
+                        STORM_LOG_TRACE("Building " << (actionInformation.getActionName(actionIndex).empty() ? "silent " : "") << "action " << (actionInformation.getActionName(actionIndex).empty() ? "" : actionInformation.getActionName(actionIndex) + " ") << "from offset " << instantiationOffset.localNondeterminismVariableOffset << ".");
+                        ActionDd actionDd = buildActionDdForActionIndex(automaton, actionIndex, instantiationOffset.localNondeterminismVariableOffset);
+                        if (inputEnabled) {
+                            actionDd.setIsInputEnabled();
+                        }
+                        STORM_LOG_TRACE("Used local nondeterminism variables are " << actionDd.getLowestLocalNondeterminismVariable() << " to " << actionDd.getHighestLocalNondeterminismVariable() << ".");
+                        result.actions[ActionIdentification(actionIndex, instantiationOffset.synchronizationVectorIndex)] = actionDd;
+                        result.extendLocalNondeterminismVariables(actionDd.getLocalNondeterminismVariables());
                     }
-                    
-                    result.actionIndexToAction[actionIndex] = actionDd;
-                    result.setLowestLocalNondeterminismVariable(std::max(result.getLowestLocalNondeterminismVariable(), actionDd.getLowestLocalNondeterminismVariable()));
-                    result.setHighestLocalNondeterminismVariable(std::max(result.getHighestLocalNondeterminismVariable(), actionDd.getHighestLocalNondeterminismVariable()));
                 }
                 
                 for (uint64_t locationIndex = 0; locationIndex < automaton.getNumberOfLocations(); ++locationIndex) {
@@ -1513,7 +1548,7 @@ namespace storm {
                 
                 return result;
             }
-
+            
             void addMissingGlobalVariableIdentities(ActionDd& action) {
                 // Build a DD that we can multiply to the transitions and adds all missing global variable identities that way.
                 storm::dd::Add<Type, ValueType> missingIdentities = this->variables.manager->template getAddOne<ValueType>();
@@ -1539,13 +1574,18 @@ namespace storm {
                     // First, determine the highest number of nondeterminism variables that is used in any action and make
                     // all actions use the same amout of nondeterminism variables.
                     uint64_t numberOfUsedNondeterminismVariables = automaton.getHighestLocalNondeterminismVariable();
+                    STORM_LOG_TRACE("Building system from composed automaton; number of used nondeterminism variables is " << numberOfUsedNondeterminismVariables << ".");
                     
                     // Add missing global variable identities, action and nondeterminism encodings.
                     std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> transientEdgeAssignments;
-                    for (auto& action : automaton.actionIndexToAction) {
+                    std::unordered_set<uint64_t> actionIndices;
+                    for (auto& action : automaton.actions) {
+                        uint64_t actionIndex = action.first.actionIndex;
+                        STORM_LOG_THROW(actionIndices.find(actionIndex) == actionIndices.end(), storm::exceptions::WrongFormatException, "Duplication action " << actionInformation.getActionName(actionIndex));
+                        actionIndices.insert(action.first.actionIndex);
                         illegalFragment |= action.second.illegalFragment;
                         addMissingGlobalVariableIdentities(action.second);
-                        storm::dd::Add<Type, ValueType> actionEncoding = encodeAction(action.first != storm::jani::Model::SILENT_ACTION_INDEX ? boost::optional<uint64_t>(action.first) : boost::none, this->variables);
+                        storm::dd::Add<Type, ValueType> actionEncoding = encodeAction(actionIndex != storm::jani::Model::SILENT_ACTION_INDEX ? boost::optional<uint64_t>(actionIndex) : boost::none, this->variables);
                         storm::dd::Add<Type, ValueType> missingNondeterminismEncoding = encodeIndex(0, action.second.getHighestLocalNondeterminismVariable(), numberOfUsedNondeterminismVariables - action.second.getHighestLocalNondeterminismVariable(), this->variables);
                         storm::dd::Add<Type, ValueType> extendedTransitions = actionEncoding * missingNondeterminismEncoding * action.second.transitions;
                         for (auto const& transientAssignment : action.second.transientEdgeAssignments) {
@@ -1562,7 +1602,10 @@ namespace storm {
                     storm::dd::Add<Type, ValueType> result = this->variables.manager->template getAddZero<ValueType>();
                     storm::dd::Bdd<Type> illegalFragment = this->variables.manager->getBddZero();
                     std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> transientEdgeAssignments;
-                    for (auto& action : automaton.actionIndexToAction) {
+                    std::unordered_set<uint64_t> actionIndices;
+                    for (auto& action : automaton.actions) {
+                        STORM_LOG_THROW(actionIndices.find(action.first.actionIndex) == actionIndices.end(), storm::exceptions::WrongFormatException, "Duplication action " << actionInformation.getActionName(action.first.actionIndex));
+                        actionIndices.insert(action.first.actionIndex);
                         illegalFragment |= action.second.illegalFragment;
                         addMissingGlobalVariableIdentities(action.second);
                         addToTransientAssignmentMap(transientEdgeAssignments, action.second.transientEdgeAssignments);
@@ -1571,7 +1614,7 @@ namespace storm {
 
                     return ComposerResult<Type, ValueType>(result, automaton.transientLocationAssignments, transientEdgeAssignments, illegalFragment, 0);
                 } else {
-                    STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type.");
+                    STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Illegal model type.");
                 }
             }
         };
@@ -1596,7 +1639,7 @@ namespace storm {
             } else if (modelType == storm::jani::ModelType::MDP) {
                 return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Mdp<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, modelComponents.labelToExpressionMap, modelComponents.rewardModels));
             } else {
-                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid model type.");
+                STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Invalid model type.");
             }
         }
         
@@ -1718,7 +1761,7 @@ namespace storm {
                         transitionMatrix += deadlockStatesAdd * globalIdentity * action;
                     }
                 } else {
-                    STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The model contains " << deadlockStates.getNonZeroCount() << " deadlock states. Please unset the option to not fix deadlocks, if you want to fix them automatically.");
+                    STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "The model contains " << deadlockStates.getNonZeroCount() << " deadlock states. Please unset the option to not fix deadlocks, if you want to fix them automatically.");
                 }
             }
             return deadlockStates;
@@ -1813,8 +1856,7 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Model still contains these undefined constants: " << boost::join(strings, ", ") << ".");
             }
             
-            STORM_LOG_THROW(!model.usesAssignmentLevels(), storm::exceptions::InvalidSettingsException, "The symbolic JANI model builder currently does not support assignment levels.");
-            STORM_LOG_THROW(!model.reusesActionsInComposition(), storm::exceptions::InvalidSettingsException, "The symbolic JANI model builder currently does not support reusing actions in parallel composition");
+            STORM_LOG_THROW(!model.usesAssignmentLevels(), storm::exceptions::WrongFormatException, "The symbolic JANI model builder currently does not support assignment levels.");
 
             storm::jani::Model preparedModel = model;
             

src/storm/cli/entrypoints.h

@@ -324,10 +324,18 @@ namespace storm {
             
             // And export if required.
             if(storm::settings::getModule<storm::settings::modules::IOSettings>().isExportExplicitSet()) {
-                std::ofstream ofs;
-                ofs.open(storm::settings::getModule<storm::settings::modules::IOSettings>().getExportExplicitFilename(), std::ofstream::out);
-                storm::exporter::explicitExportSparseModel(ofs, sparseModel, model.getParameterNames());
-                ofs.close();
+                std::ofstream stream;
+                storm::utility::openFile(storm::settings::getModule<storm::settings::modules::IOSettings>().getExportExplicitFilename(), stream);
+                storm::exporter::explicitExportSparseModel(stream, sparseModel, model.getParameterNames());
+                storm::utility::closeFile(stream);
+            }
+
+            // And export DOT if required.
+            if(storm::settings::getModule<storm::settings::modules::IOSettings>().isExportDotSet()) {
+                std::ofstream stream;
+                storm::utility::openFile(storm::settings::getModule<storm::settings::modules::IOSettings>().getExportDotFilename(), stream);
+                sparseModel->writeDotToStream(stream);
+                storm::utility::closeFile(stream);
             }
         }
         

src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp

@@ -10,10 +10,15 @@
 
 #include "storm/logic/FragmentSpecification.h"
 
+#include "storm/modelchecker/multiobjective/pcaa.h"
+
 #include "storm/solver/MinMaxLinearEquationSolver.h"
 
 #include "storm/settings/modules/GeneralSettings.h"
 
+#include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/transformer/SymbolicToSparseTransformer.h"
+
 #include "storm/exceptions/InvalidStateException.h"
 #include "storm/exceptions/InvalidPropertyException.h"
 
@@ -32,7 +37,15 @@ namespace storm {
         template<typename ModelType>
         bool HybridMdpPrctlModelChecker<ModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
             storm::logic::Formula const& formula = checkTask.getFormula();
-            return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false));
+            if(formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false))) {
+                return true;
+            } else {
+                // Check whether we consider a multi-objective formula
+                // For multi-objective model checking, each state requires an individual scheduler (in contrast to single-objective model checking). Let's exclude that all states are considered.
+                if(!checkTask.isOnlyInitialStatesRelevantSet()) return false;
+                return formula.isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true));
+            }
+
         }
                 
         template<typename ModelType>
@@ -102,6 +115,11 @@ namespace storm {
             return storm::modelchecker::helper::HybridMdpPrctlHelper<DdType, ValueType>::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory);
         }
 
+        template<typename ModelType>
+        std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<ModelType>::checkMultiObjectiveFormula(CheckTask<storm::logic::MultiObjectiveFormula, ValueType> const& checkTask) {
+            auto sparseModel = storm::transformer::SymbolicMdpToSparseMdpTransformer<DdType, ValueType>::translate(this->getModel());
+			return multiobjective::performPcaa(*sparseModel, checkTask.getFormula());
+        }
 
         template class HybridMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>;
         template class HybridMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>>;

src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h

@@ -35,6 +35,7 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> checkMultiObjectiveFormula(CheckTask<storm::logic::MultiObjectiveFormula, ValueType> const& checkTask) override;
 
         private:
             // An object that is used for retrieving linear equation solvers.

src/storm/modelchecker/region/ParameterRegion.cpp

@@ -7,7 +7,8 @@
 #include "storm/settings/modules/RegionSettings.h"
 #include "storm/exceptions/InvalidSettingsException.h"
 #include "storm/exceptions/InvalidArgumentException.h"
-#include "utility/constants.h"
+#include "storm/utility/constants.h"
+#include "storm/utility/file.h"
 
 namespace storm {
     namespace modelchecker {
@@ -283,7 +284,7 @@ namespace storm {
                     }
                     else{
                         //if we reach this point we can assume that the region is given as a file.
-                        STORM_LOG_THROW(storm::parser::MappedFile::fileExistsAndIsReadable(storm::settings::getModule<storm::settings::modules::RegionSettings>().getRegionFilePath().c_str()), storm::exceptions::InvalidSettingsException, "The path to the file in which the regions are specified is not valid.");
+                        STORM_LOG_THROW(storm::utility::fileExistsAndIsReadable(storm::settings::getModule<storm::settings::modules::RegionSettings>().getRegionFilePath()), storm::exceptions::InvalidSettingsException, "The path to the file in which the regions are specified is not valid.");
                         storm::parser::MappedFile mf(storm::settings::getModule<storm::settings::modules::RegionSettings>().getRegionFilePath().c_str());
                         regionsString = std::string(mf.getData(),mf.getDataSize());
                     }

src/storm/models/symbolic/Model.cpp

@@ -71,6 +71,11 @@ namespace storm {
             storm::dd::Bdd<Type> const& Model<Type, ValueType>::getInitialStates() const {
                 return initialStates;
             }
+
+            template<storm::dd::DdType Type, typename ValueType>
+            storm::dd::Bdd<Type> const& Model<Type, ValueType>::getDeadlockStates() const {
+                return deadlockStates;
+            }
             
             template<storm::dd::DdType Type, typename ValueType>
             storm::dd::Bdd<Type> Model<Type, ValueType>::getStates(std::string const& label) const {
@@ -192,12 +197,26 @@ namespace storm {
             bool Model<Type, ValueType>::hasRewardModel() const {
                 return !this->rewardModels.empty();
             }
+
+            template<storm::dd::DdType Type, typename ValueType>
+            std::unordered_map<std::string, typename Model<Type, ValueType>::RewardModelType> const& Model<Type, ValueType>::getRewardModels() const {
+                return this->rewardModels;
+            }
             
             template<storm::dd::DdType Type, typename ValueType>
             void Model<Type, ValueType>::printModelInformationToStream(std::ostream& out) const {
                 this->printModelInformationHeaderToStream(out);
                 this->printModelInformationFooterToStream(out);
             }
+
+            template<storm::dd::DdType Type, typename ValueType>
+            std::vector<std::string> Model<Type, ValueType>::getLabels() const {
+                std::vector<std::string> labels;
+                for(auto const& entry : labelToExpressionMap) {
+                    labels.push_back(entry.first);
+                }
+                return labels;
+            }
             
             template<storm::dd::DdType Type, typename ValueType>
             void Model<Type, ValueType>::printModelInformationHeaderToStream(std::ostream& out) const {

src/storm/models/symbolic/Model.h

@@ -130,7 +130,12 @@ namespace storm {
                  * @return The initial states of the model.
                  */
                 storm::dd::Bdd<Type> const& getInitialStates() const;
-                
+
+                /*
+                 * Retrieves the deadlock states of the model.
+                 */
+                storm::dd::Bdd<Type> const& getDeadlockStates() const;
+
                 /*!
                  * Returns the sets of states labeled with the given label.
                  *
@@ -246,6 +251,8 @@ namespace storm {
                  * @return True iff the model has a reward model.
                  */
                 bool hasRewardModel() const;
+
+                std::unordered_map<std::string, RewardModelType> const& getRewardModels() const;
                 
                 /*!
                  * Retrieves the number of reward models associated with this model.
@@ -257,6 +264,8 @@ namespace storm {
                 virtual void printModelInformationToStream(std::ostream& out) const override;
                 
                 virtual bool isSymbolicModel() const override;
+
+                std::vector<std::string> getLabels() const;
                 
             protected:
                 

src/storm/parser/AtomicPropositionLabelingParser.cpp

@@ -24,11 +24,6 @@ namespace storm {
 		storm::models::sparse::StateLabeling AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(uint_fast64_t stateCount, std::string const & filename) {
 
 			// Open the given file.
-			if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) {
-				STORM_LOG_ERROR("Error while parsing " << filename << ": The supplied Labeling input file does not exist or is not readable by this process.");
-				throw storm::exceptions::FileIoException() << "Error while parsing " << filename << ": The supplied Labeling input file does not exist or is not readable by this process.";
-			}
-
 			MappedFile file(filename.c_str());
 			char const* buf = file.getData();
 

src/storm/parser/DeterministicSparseTransitionParser.cpp

@@ -41,11 +41,6 @@ namespace storm {
             // Enforce locale where decimal point is '.'.
             setlocale(LC_NUMERIC, "C");
 
-            if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) {
-                STORM_LOG_ERROR("Error while parsing " << filename << ": File does not exist or is not readable.");
-                throw storm::exceptions::FileIoException() << "The supplied Transition input file \"" << filename << "\" does not exist or is not readable by this process.";
-            }
-
             // Open file.
             MappedFile file(filename.c_str());
             char const* buf = file.getData();

src/storm/parser/FormulaParser.cpp

@@ -15,6 +15,7 @@
 #include "storm/storage/expressions/ExpressionEvaluator.h"
 #include "FormulaParserGrammar.h"
 #include "storm/storage/expressions/ExpressionManager.h"
+#include "storm/utility/file.h"
 
 namespace storm {
     namespace parser {
@@ -65,8 +66,8 @@ namespace storm {
         
         std::vector<storm::jani::Property> FormulaParser::parseFromFile(std::string const& filename) const {
             // Open file and initialize result.
-            std::ifstream inputFileStream(filename, std::ios::in);
-            STORM_LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'.");
+            std::ifstream inputFileStream;
+            storm::utility::openFile(filename, inputFileStream);
             
             std::vector<storm::jani::Property> properties;
             
@@ -76,12 +77,12 @@ namespace storm {
                 properties = parseFromString(fileContent);
             } catch(std::exception& e) {
                 // In case of an exception properly close the file before passing exception.
-                inputFileStream.close();
+                storm::utility::closeFile(inputFileStream);
                 throw e;
             }
             
             // Close the stream in case everything went smoothly and return result.
-            inputFileStream.close();
+            storm::utility::closeFile(inputFileStream);
             return properties;
         }
         

src/storm/parser/JaniParser.cpp

@@ -18,6 +18,7 @@
 #include <boost/lexical_cast.hpp>
 
 #include "storm/utility/macros.h"
+#include "storm/utility/file.h"
 
 namespace storm {
     namespace parser {
@@ -64,18 +65,9 @@ namespace storm {
 
         void JaniParser::readFile(std::string const &path) {
             std::ifstream file;
-            file.exceptions ( std::ifstream::failbit );
-            try {
-                file.open(path);
-            }
-            catch (std::ifstream::failure e) {
-                STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Exception during file opening on " << path << ".");
-                return;
-            }
-            file.exceptions( std::ifstream::goodbit );
-
+            storm::utility::openFile(path, file);
             parsedStructure << file;
-            file.close();
+            storm::utility::closeFile(file);
         }
 
         std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> JaniParser::parseModel(bool parseProperties) {

src/storm/parser/MappedFile.cpp

@@ -15,10 +15,14 @@
 
 #include "storm/exceptions/FileIoException.h"
 #include "storm/utility/macros.h"
+#include "storm/utility/file.h"
+
 namespace storm {
 	namespace parser {
 
 		MappedFile::MappedFile(const char* filename) {
+            STORM_LOG_THROW(storm::utility::fileExistsAndIsReadable(filename), storm::exceptions::FileIoException, "Error while reading " << filename << ": The file does not exist or is not readable.");
+
 		#if defined LINUX || defined MACOSX
 
 			// Do file mapping for reasonable systems.
@@ -29,15 +33,11 @@ namespace storm {
 		#else
 			if (stat64(filename, &(this->st)) != 0) {
 		#endif
-				STORM_LOG_ERROR("Error in stat(" << filename << "): Probably, this file does not exist.");
-				throw exceptions::FileIoException() << "MappedFile Error in stat(): Probably, this file does not exist.";
+				STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Error in stat(" << filename << "): Probably, this file does not exist.");
 			}
 			this->file = open(filename, O_RDONLY);
 
-			if (this->file < 0) {
-				STORM_LOG_ERROR("Error in open(" << filename << "): Probably, we may not read this file.");
-				throw exceptions::FileIoException() << "MappedFile Error in open(): Probably, we may not read this file.";
-			}
+            STORM_LOG_THROW(this->file >= 0, storm::exceptions::FileIoException, "Error in open(" << filename << "): Probably, we may not read this file.");
             
 			this->data = static_cast<char*>(mmap(NULL, this->st.st_size, PROT_READ, MAP_PRIVATE, this->file, 0));
 			if (this->data == MAP_FAILED) {
@@ -90,12 +90,6 @@ namespace storm {
 		#endif
 		}
 
-		bool MappedFile::fileExistsAndIsReadable(const char* filename) {
-			// Test by opening an input file stream and testing the stream flags.
-			std::ifstream fin(filename);
-			return fin.good();
-		}
-
 		char const* MappedFile::getData() const {
 			return data;
 		}

src/storm/parser/MappedFile.h

@@ -49,14 +49,6 @@ namespace storm {
 			 */
 			~MappedFile();
 
-			/*!
-			 * Tests whether the given file exists and is readable.
-			 *qi
-			 * @param filename Path and name of the file to be tested.
-			 * @return True iff the file exists and is readable.
-			 */
-			static bool fileExistsAndIsReadable(const char* filename);
-
 			/*!
 			 * Returns a pointer to the beginning of the mapped file data.
 			 *

src/storm/parser/MarkovAutomatonSparseTransitionParser.cpp

@@ -294,11 +294,6 @@ namespace storm {
             // Set the locale to correctly recognize floating point numbers.
             setlocale(LC_NUMERIC, "C");
 
-            if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) {
-                STORM_LOG_ERROR("Error while parsing " << filename << ": File does not exist or is not readable.");
-                throw storm::exceptions::FileIoException() << "Error while parsing " << filename << ": File does not exist or is not readable.";
-            }
-
             // Open file and prepare pointer to buffer.
             MappedFile file(filename.c_str());
             char const* buf = file.getData();

src/storm/parser/NondeterministicSparseTransitionParser.cpp

@@ -39,11 +39,6 @@ namespace storm {
             // Enforce locale where decimal point is '.'.
             setlocale(LC_NUMERIC, "C");
 
-            if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) {
-                STORM_LOG_ERROR("Error while parsing " << filename << ": File does not exist or is not readable.");
-                throw storm::exceptions::FileIoException() << "Error while parsing " << filename << ": File does not exist or is not readable.";
-            }
-
             // Open file.
             MappedFile file(filename.c_str());
             char const* buf = file.getData();

src/storm/parser/PrismParser.cpp

@@ -7,6 +7,7 @@
 #include "storm/exceptions/InvalidArgumentException.h"
 #include "storm/exceptions/InvalidTypeException.h"
 #include "storm/utility/macros.h"
+#include "storm/utility/file.h"
 #include "storm/exceptions/WrongFormatException.h"
 
 #include "storm/storage/expressions/ExpressionManager.h"
@@ -17,9 +18,8 @@ namespace storm {
     namespace parser {
         storm::prism::Program PrismParser::parse(std::string const& filename) {
             // Open file and initialize result.
-            std::ifstream inputFileStream(filename);
-            STORM_LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'.");
-            
+            std::ifstream inputFileStream;
+            storm::utility::openFile(filename, inputFileStream);
             storm::prism::Program result;
             
             // Now try to parse the contents of the file.
@@ -28,12 +28,12 @@ namespace storm {
                 result = parseFromString(fileContent, filename);
             } catch(std::exception& e) {
                 // In case of an exception properly close the file before passing exception.
-                inputFileStream.close();
+                storm::utility::closeFile(inputFileStream);
                 throw e;
             }
             
             // Close the stream in case everything went smoothly and return result.
-            inputFileStream.close();
+            storm::utility::closeFile(inputFileStream);
             return result;
         }
         

src/storm/parser/SparseChoiceLabelingParser.cpp

@@ -13,11 +13,6 @@ namespace storm {
 
         std::vector<storm::models::sparse::LabelSet> SparseChoiceLabelingParser::parseChoiceLabeling(std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, std::string const& filename) {
             // Open file.
-            if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) {
-                STORM_LOG_ERROR("Error while parsing " << filename << ": File does not exist or is not readable.");
-                throw storm::exceptions::FileIoException() << "Error while parsing " << filename << ": File does not exist or is not readable.";
-            }
-
             MappedFile file(filename.c_str());
             char const* buf = file.getData();
 

src/storm/parser/SparseStateRewardParser.cpp

@@ -17,11 +17,6 @@ namespace storm {
         template<typename ValueType>
         std::vector<ValueType> SparseStateRewardParser<ValueType>::parseSparseStateReward(uint_fast64_t stateCount, std::string const& filename) {
             // Open file.
-            if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) {
-                STORM_LOG_ERROR("Error while parsing " << filename << ": File does not exist or is not readable.");
-                throw storm::exceptions::FileIoException() << "Error while parsing " << filename << ": File does not exist or is not readable.";
-            }
-
             MappedFile file(filename.c_str());
             char const* buf = file.getData();
 

src/storm/settings/SettingsManager.cpp

@@ -39,6 +39,7 @@
 #include "storm/settings/modules/JitBuilderSettings.h"
 #include "storm/settings/modules/MultiObjectiveSettings.h"
 #include "storm/utility/macros.h"
+#include "storm/utility/file.h"
 #include "storm/settings/Option.h"
 
 namespace storm {
@@ -394,8 +395,8 @@ namespace storm {
         std::map<std::string, std::vector<std::string>> SettingsManager::parseConfigFile(std::string const& filename) const {
             std::map<std::string, std::vector<std::string>> result;
             
-            std::ifstream input(filename);
-            STORM_LOG_THROW(input.good(), storm::exceptions::OptionParserException, "Could not read from config file '" << filename << "'.");
+            std::ifstream input;
+            storm::utility::openFile(filename, input);
 
             bool globalScope = true;
             std::string activeModule = "";
@@ -480,7 +481,8 @@ namespace storm {
                     }
                 }
             }
-            
+
+            storm::utility::closeFile(input);
             return result;
         }
         

src/storm/solver/SmtlibSmtSolver.cpp

@@ -16,9 +16,10 @@
 #include "storm/exceptions/InvalidStateException.h"
 #include "storm/exceptions/IllegalArgumentException.h"
 #include "storm/exceptions/IllegalFunctionCallException.h"
-#include "utility/macros.h"
-#include "adapters/CarlAdapter.h"
-#include "exceptions/UnexpectedException.h"
+#include "storm/utility/macros.h"
+#include "storm/utility/file.h"
+#include "storm/adapters/CarlAdapter.h"
+#include "storm/exceptions/UnexpectedException.h"
 
 namespace storm {
     namespace solver {
@@ -245,9 +246,9 @@ namespace storm {
 
             if (storm::settings::getModule<storm::settings::modules::Smt2SmtSolverSettings>().isExportSmtLibScriptSet()){
                 STORM_LOG_DEBUG("The SMT-LIBv2 commands are exportet to the given file");
-                commandFile.open(storm::settings::getModule<storm::settings::modules::Smt2SmtSolverSettings>().getExportSmtLibScriptPath(), std::ios::trunc);
-                isCommandFileOpen=commandFile.is_open();
-                STORM_LOG_THROW(isCommandFileOpen, storm::exceptions::InvalidArgumentException, "The file where the smt2commands should be written to could not be opened");
+                storm::utility::openFile(storm::settings::getModule<storm::settings::modules::Smt2SmtSolverSettings>().getExportSmtLibScriptPath(), commandFile);
+                isCommandFileOpen = true;
+                // TODO also close file
             }
 
             //some initial commands

src/storm/storage/dd/Odd.cpp

@@ -6,6 +6,7 @@
 
 #include "storm/utility/macros.h"
 #include "storm/exceptions/InvalidArgumentException.h"
+#include "storm/utility/file.h"
 
 namespace storm {
     namespace dd {
@@ -86,7 +87,7 @@ namespace storm {
         
         void Odd::exportToDot(std::string const& filename) const {
             std::ofstream dotFile;
-            dotFile.open (filename);
+            storm::utility::openFile(filename, dotFile);
             
             // Print header.
             dotFile << "digraph \"ODD\" {" << std::endl << "center=true;" << std::endl << "edge [dir = none];" << std::endl;
@@ -129,8 +130,7 @@ namespace storm {
             }
             
             dotFile << "}" << std::endl;
-            
-            dotFile.close();
+            storm::utility::closeFile(dotFile);
         }
         
         void Odd::addToLevelToOddNodesMap(std::map<uint_fast64_t, std::vector<std::reference_wrapper<storm::dd::Odd const>>>& levelToOddNodesMap, uint_fast64_t level) const {

src/storm/storage/expressions/BinaryBooleanFunctionExpression.cpp

@@ -122,7 +122,11 @@ namespace storm {
         boost::any BinaryBooleanFunctionExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const {
             return visitor.visit(*this, data);
         }
-        
+
+        bool BinaryBooleanFunctionExpression::isBinaryBooleanFunctionExpression() const {
+            return true;
+        }
+
         void BinaryBooleanFunctionExpression::printToStream(std::ostream& stream) const {
             stream << "(" << *this->getFirstOperand();
             switch (this->getOperatorType()) {

src/storm/storage/expressions/BinaryBooleanFunctionExpression.h

@@ -38,6 +38,7 @@ namespace storm {
             virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override;
             virtual std::shared_ptr<BaseExpression const> simplify() const override;
             virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override;
+            virtual bool isBinaryBooleanFunctionExpression() const override;
 
             /*!
              * Retrieves the operator associated with the expression.

src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp

@@ -122,7 +122,11 @@ namespace storm {
         boost::any BinaryNumericalFunctionExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const {
             return visitor.visit(*this, data);
         }
-        
+
+        bool BinaryNumericalFunctionExpression::isBinaryNumericalFunctionExpression() const {
+            return true;
+        }
+
         void BinaryNumericalFunctionExpression::printToStream(std::ostream& stream) const {
             stream << "(";
             switch (this->getOperatorType()) {

src/storm/storage/expressions/BinaryNumericalFunctionExpression.h

@@ -39,6 +39,7 @@ namespace storm {
             virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override;
             virtual std::shared_ptr<BaseExpression const> simplify() const override;
             virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override;
+            virtual bool isBinaryNumericalFunctionExpression() const override;
 
             /*!
              * Retrieves the operator associated with the expression.

src/storm/storage/expressions/BinaryRelationExpression.cpp

@@ -85,7 +85,11 @@ namespace storm {
         boost::any BinaryRelationExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const {
             return visitor.visit(*this, data);
         }
-        
+
+        bool BinaryRelationExpression::isBinaryRelationExpression() const {
+            return true;
+        }
+
         BinaryRelationExpression::RelationType BinaryRelationExpression::getRelationType() const {
             return this->relationType;
         }

src/storm/storage/expressions/BinaryRelationExpression.h

@@ -38,6 +38,7 @@ namespace storm {
             virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override;
             virtual std::shared_ptr<BaseExpression const> simplify() const override;
             virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override;
+            virtual bool isBinaryRelationExpression() const override;
 
             /*!
              * Retrieves the relation associated with the expression.

src/storm/storage/expressions/BooleanLiteralExpression.cpp

@@ -35,7 +35,11 @@ namespace storm {
         boost::any BooleanLiteralExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const {
             return visitor.visit(*this, data);
         }
-        
+
+        bool BooleanLiteralExpression::isBooleanLiteralExpression() const {
+            return true;
+        }
+
         bool BooleanLiteralExpression::getValue() const {
             return this->value;
         }

src/storm/storage/expressions/BooleanLiteralExpression.h

@@ -33,7 +33,7 @@ namespace storm {
             virtual void gatherVariables(std::set<storm::expressions::Variable>& variables) const override;
             virtual std::shared_ptr<BaseExpression const> simplify() const override;
             virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override;
-            
+            virtual bool isBooleanLiteralExpression() const override;
             /*!
              * Retrieves the value of the boolean literal.
              *

src/storm/storage/expressions/IfThenElseExpression.cpp

@@ -91,6 +91,10 @@ namespace storm {
         boost::any IfThenElseExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const {
             return visitor.visit(*this, data);
         }
+
+        bool IfThenElseExpression::isIfThenElseExpression() const {
+            return true;
+        }
         
         std::shared_ptr<BaseExpression const> IfThenElseExpression::getCondition() const {
             return this->condition;

src/storm/storage/expressions/IfThenElseExpression.h

@@ -39,7 +39,8 @@ namespace storm {
             virtual void gatherVariables(std::set<storm::expressions::Variable>& variables) const override;
             virtual std::shared_ptr<BaseExpression const> simplify() const override;
             virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override;
-            
+            virtual bool isIfThenElseExpression() const override;
+
             /*!
              * Retrieves the condition expression of the if-then-else expression.
              *

src/storm/storage/expressions/IntegerLiteralExpression.cpp

@@ -32,7 +32,12 @@ namespace storm {
         boost::any IntegerLiteralExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const {
             return visitor.visit(*this, data);
         }
-        
+
+        bool IntegerLiteralExpression::isIntegerLiteralExpression() const {
+            return true;
+        }
+
+
         int_fast64_t IntegerLiteralExpression::getValue() const {
             return this->value;
         }

src/storm/storage/expressions/IntegerLiteralExpression.h

@@ -32,7 +32,8 @@ namespace storm {
             virtual void gatherVariables(std::set<storm::expressions::Variable>& variables) const override;
             virtual std::shared_ptr<BaseExpression const> simplify() const override;
             virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override;
-            
+            virtual bool isIntegerLiteralExpression() const override;
+
             /*!
              * Retrieves the value of the integer literal.
              *

src/storm/storage/expressions/RationalLiteralExpression.cpp

@@ -37,6 +37,10 @@ namespace storm {
         boost::any RationalLiteralExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const {
             return visitor.visit(*this, data);
         }
+
+        bool RationalLiteralExpression::isRationalLiteralExpression() const {
+            return true;
+        }
         
         double RationalLiteralExpression::getValueAsDouble() const {
             return storm::utility::convertNumber<double>(this->value);

src/storm/storage/expressions/RationalLiteralExpression.h

@@ -49,6 +49,7 @@ namespace storm {
             virtual void gatherVariables(std::set<storm::expressions::Variable>& variables) const override;
             virtual std::shared_ptr<BaseExpression const> simplify() const override;
             virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override;
+            virtual bool isRationalLiteralExpression() const override;
 
             /*!
              * Retrieves the value of the double literal.

src/storm/storage/expressions/UnaryBooleanFunctionExpression.cpp

@@ -52,7 +52,11 @@ namespace storm {
         boost::any UnaryBooleanFunctionExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const {
             return visitor.visit(*this, data);
         }
-        
+
+        bool UnaryBooleanFunctionExpression::isUnaryBooleanFunctionExpression() const {
+            return true;
+        }
+
         void UnaryBooleanFunctionExpression::printToStream(std::ostream& stream) const {
             stream << "!(" << *this->getOperand() << ")";
         }

src/storm/storage/expressions/UnaryBooleanFunctionExpression.h

@@ -37,6 +37,7 @@ namespace storm {
             virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override;
             virtual std::shared_ptr<BaseExpression const> simplify() const override;
             virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override;
+            virtual bool isUnaryBooleanFunctionExpression() const override;
 
             /*!
              * Retrieves the operator associated with this expression.

src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp

@@ -103,7 +103,11 @@ namespace storm {
         boost::any UnaryNumericalFunctionExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const {
             return visitor.visit(*this, data);
         }
-        
+
+        bool UnaryNumericalFunctionExpression::isUnaryNumericalFunctionExpression() const {
+            return true;
+        }
+
         void UnaryNumericalFunctionExpression::printToStream(std::ostream& stream) const {
             switch (this->getOperatorType()) {
                 case OperatorType::Minus: stream << "-("; break;

src/storm/storage/expressions/UnaryNumericalFunctionExpression.h

@@ -38,7 +38,8 @@ namespace storm {
             virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override;
             virtual std::shared_ptr<BaseExpression const> simplify() const override;
             virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override;
-     
+            virtual bool isUnaryNumericalFunctionExpression() const override;
+
             /*!
              * Retrieves the operator associated with this expression.
              *

src/storm/storage/expressions/VariableExpression.cpp

@@ -66,7 +66,11 @@ namespace storm {
         boost::any VariableExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const {
             return visitor.visit(*this, data);
         }
-        
+
+        bool VariableExpression::isVariableExpression() const {
+            return true;
+        }
+
         void VariableExpression::printToStream(std::ostream& stream) const {
             stream << this->getVariableName();
         }

src/storm/storage/expressions/VariableExpression.h

@@ -36,6 +36,7 @@ namespace storm {
             virtual void gatherVariables(std::set<storm::expressions::Variable>& variables) const override;
             virtual std::shared_ptr<BaseExpression const> simplify() const override;
             virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override;
+            virtual bool isVariableExpression() const override;
 
             /*!
              * Retrieves the name of the variable associated with this expression.

src/storm/storage/jani/JSONExporter.cpp

@@ -5,6 +5,7 @@
 #include <vector>
 
 #include "storm/utility/macros.h"
+#include "storm/utility/file.h"
 #include "storm/exceptions/FileIoException.h"
 #include "storm/exceptions/NotSupportedException.h"
 
@@ -510,20 +511,11 @@ namespace storm {
             return modernjson::json(expression.getValueAsDouble());
         }
         
-        
-        
-        
-        
-        
-        
         void JsonExporter::toFile(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::string const& filepath, bool checkValid) {
-            std::ofstream ofs;
-            ofs.open (filepath, std::ofstream::out );
-            if(ofs.is_open()) {
-                toStream(janiModel, formulas, ofs, checkValid);
-            } else {
-                STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Cannot open " << filepath);
-            }
+            std::ofstream stream;
+            storm::utility::openFile(filepath, stream);
+            toStream(janiModel, formulas, stream, checkValid);
+            storm::utility::closeFile(stream);
         }
         
         void JsonExporter::toStream(storm::jani::Model const& janiModel,  std::vector<storm::jani::Property> const& formulas, std::ostream& os, bool checkValid) {

src/storm/storage/jani/Model.cpp

@@ -758,10 +758,7 @@ namespace storm {
                     ++i;
                 }
                 
-                // Only add the synchronization vector if there is more than one participating automaton.
-                if (numberOfParticipatingAutomata > 1) {
-                    synchVectors.push_back(storm::jani::SynchronizationVector(synchVectorInputs, actionName));
-                }
+                synchVectors.push_back(storm::jani::SynchronizationVector(synchVectorInputs, actionName));
             }
             
             return std::make_shared<ParallelComposition>(subcompositions, synchVectors);

src/storm/transformer/SymbolicToSparseTransformer.cpp

@@ -0,0 +1,50 @@
+#include "SymbolicToSparseTransformer.h"
+
+#include "storm/storage/dd/DdManager.h"
+#include "storm/storage/dd/Add.h"
+#include "storm/storage/dd/Bdd.h"
+#include "storm/models/symbolic/StandardRewardModel.h"
+
+
+#include "storm/models/sparse/StandardRewardModel.h"
+
+namespace storm {
+    namespace transformer {
+
+        template<storm::dd::DdType Type, typename ValueType>
+        std::shared_ptr<storm::models::sparse::Mdp<ValueType>> SymbolicMdpToSparseMdpTransformer<Type, ValueType>::translate(
+                storm::models::symbolic::Mdp<Type, ValueType> const& symbolicMdp) {
+            storm::dd::Odd odd = symbolicMdp.getReachableStates().createOdd();
+            storm::storage::SparseMatrix<ValueType> transitionMatrix = symbolicMdp.getTransitionMatrix().toMatrix(symbolicMdp.getNondeterminismVariables(), odd, odd);
+            std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> rewardModels;
+            for (auto const& rewardModelNameAndModel : symbolicMdp.getRewardModels()) {
+                boost::optional<std::vector<ValueType>> stateRewards;
+                boost::optional<std::vector<ValueType>> stateActionRewards;
+                boost::optional<storm::storage::SparseMatrix<ValueType>> transitionRewards;
+                if (rewardModelNameAndModel.second.hasStateRewards()) {
+                    stateRewards = rewardModelNameAndModel.second.getStateRewardVector().toVector(odd);
+                }
+                if (rewardModelNameAndModel.second.hasStateActionRewards()) {
+                    stateActionRewards = rewardModelNameAndModel.second.getStateActionRewardVector().toVector(odd);
+                }
+                if (rewardModelNameAndModel.second.hasTransitionRewards()) {
+                    transitionRewards = rewardModelNameAndModel.second.getTransitionRewardMatrix().toMatrix(symbolicMdp.getNondeterminismVariables(), odd, odd);
+                }
+                rewardModels.emplace(rewardModelNameAndModel.first,storm::models::sparse::StandardRewardModel<ValueType>(stateRewards, stateActionRewards, transitionRewards));
+            }
+            storm::models::sparse::StateLabeling labelling;
+
+            labelling.addLabel("init", symbolicMdp.getInitialStates().toVector(odd));
+            labelling.addLabel("deadlock", symbolicMdp.getDeadlockStates().toVector(odd));
+            for(auto const& label : symbolicMdp.getLabels()) {
+                labelling.addLabel(label, symbolicMdp.getStates(label).toVector(odd));
+            }
+            return std::make_shared<storm::models::sparse::Mdp<ValueType>>(transitionMatrix, labelling, rewardModels);
+
+
+        }
+
+        template class SymbolicMdpToSparseMdpTransformer<storm::dd::DdType::CUDD, double>;
+        template class SymbolicMdpToSparseMdpTransformer<storm::dd::DdType::Sylvan, double>;
+    }
+}

src/storm/transformer/SymbolicToSparseTransformer.h

@@ -0,0 +1,15 @@
+#pragma once
+
+#include "storm/models/sparse/Mdp.h"
+#include "storm/models/symbolic/Mdp.h"
+
+namespace storm {
+    namespace transformer {
+
+        template<storm::dd::DdType Type, typename ValueType>
+        class SymbolicMdpToSparseMdpTransformer {
+        public:
+            static std::shared_ptr<storm::models::sparse::Mdp<ValueType>> translate(storm::models::symbolic::Mdp<Type, ValueType> const& symbolicMdp);
+        };
+    }
+}

src/storm/utility/export.h

@@ -12,7 +12,7 @@
 #include <boost/optional.hpp>
 
 #include "storm/utility/macros.h"
-#include "storm/exceptions/FileIoException.h"
+#include "storm/utility/file.h"
 
 //#include "storm/storage/parameters.h"
 //#include "storm/settings/modules/ParametricSettings.h"
@@ -40,19 +40,11 @@ namespace storm {
             filestream.close();
         }
         */
-            
-        inline void exportStringToFile(std::string const& str, std::string filepath) {
-            std::ofstream filestream;
-            filestream.open(filepath);
-            STORM_LOG_THROW(filestream.is_open(), storm::exceptions::FileIoException , "Could not open file " << filepath << ".");
-            filestream << str;
-        }
         
         template <typename ValueType>
         inline void exportDataToCSVFile(std::string filepath, std::vector<std::vector<ValueType>> const& data, boost::optional<std::vector<std::string>> const& columnHeaders) {
             std::ofstream filestream;
-            filestream.open(filepath);
-            STORM_LOG_THROW(filestream.is_open(), storm::exceptions::FileIoException , "Could not open file " << filepath << ".");
+            storm::utility::openFile(filepath, filestream);
             
             if(columnHeaders) {
                 for(auto columnIt = columnHeaders->begin(); columnIt != columnHeaders->end(); ++columnIt) {
@@ -73,10 +65,9 @@ namespace storm {
                 }
                 filestream << std::endl;
             }
+            storm::utility::closeFile(filestream);
         }
     }
 }
 
-
-
 #endif

src/storm/utility/file.h

@@ -0,0 +1,81 @@
+/** 
+ * @file:   file.h
+ * @author: Sebastian Junges
+ *
+ * @since October 7, 2014
+ */
+
+#ifndef STORM_UTILITY_FILE_H_
+#define STORM_UTILITY_FILE_H_
+
+#include <iostream>
+
+#include "storm/utility/macros.h"
+#include "storm/exceptions/FileIoException.h"
+
+namespace storm {
+    namespace utility {
+
+        /*!
+         * Open the given file for writing.
+         *
+         * @param filename Path and name of the file to be tested.
+         * @param filestream Contains the file handler afterwards.
+         * @param append If true, the new content is appended instead of clearing the existing content.
+         */
+        inline void openFile(std::string const& filepath, std::ofstream& filestream, bool append = false) {
+            if (append) {
+                filestream.open(filepath, std::ios::app);
+            } else {
+                filestream.open(filepath);
+            }
+            STORM_LOG_THROW(filestream, storm::exceptions::FileIoException , "Could not open file " << filepath << ".");
+            STORM_PRINT_AND_LOG("Write to file " << filepath << "." << std::endl);
+        }
+
+        /*!
+         * Open the given file for reading.
+         *
+         * @param filename Path and name of the file to be tested.
+         * @param filestream Contains the file handler afterwards.
+         */
+        inline void openFile(std::string const& filepath, std::ifstream& filestream) {
+            filestream.open(filepath);
+            STORM_LOG_THROW(filestream, storm::exceptions::FileIoException , "Could not open file " << filepath << ".");
+        }
+
+        /*!
+         * Close the given file after writing.
+         *
+         * @param filestream Contains the file handler to close.
+         */
+        inline void closeFile(std::ofstream& stream) {
+            stream.close();
+        }
+
+        /*!
+         * Close the given file after reading.
+         *
+         * @param filestream Contains the file handler to close.
+         */
+        inline void closeFile(std::ifstream& stream) {
+            stream.close();
+        }
+
+        /*!
+         * Tests whether the given file exists and is readable.
+         *
+         * @param filename Path and name of the file to be tested.
+         * @return True iff the file exists and is readable.
+         */
+        inline bool fileExistsAndIsReadable(std::string const& filename) {
+            // Test by opening an input file stream and testing the stream flags.
+            std::ifstream filestream;
+            filestream.open(filename);
+            return filestream.good();
+        }
+
+    }
+}
+
+#endif

src/storm/utility/storm.h

@@ -97,6 +97,7 @@
 #include "storm/exceptions/NotSupportedException.h"
 
 #include "storm/utility/Stopwatch.h"
+#include "storm/utility/file.h"
 
 namespace storm {
 
@@ -434,7 +435,7 @@ namespace storm {
 
     inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::models::sparse::Dtmc<storm::RationalFunction>::ConstraintCollector const& constraintCollector, std::string const& path) {
         std::ofstream filestream;
-        filestream.open(path);
+        storm::utility::openFile(path, filestream);
         // TODO: add checks.
         filestream << "!Parameters: ";
         std::set<storm::RationalFunctionVariable> vars = result.gatherVariables();
@@ -445,7 +446,7 @@ namespace storm {
         std::copy(constraintCollector.getWellformedConstraints().begin(), constraintCollector.getWellformedConstraints().end(), std::ostream_iterator<storm::ArithConstraint<storm::RationalFunction>>(filestream, "\n"));
         filestream << "!Graph-preserving Constraints: " << std::endl;
         std::copy(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::ostream_iterator<storm::ArithConstraint<storm::RationalFunction>>(filestream, "\n"));
-        filestream.close();
+        storm::utility::closeFile(filestream);
     }
 
     template<>
@@ -623,10 +624,10 @@ namespace storm {
     template<typename ValueType>
     void exportMatrixToFile(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::string const& filepath) {
         STORM_LOG_THROW(model->getType() != storm::models::ModelType::Ctmc, storm::exceptions::NotImplementedException, "This functionality is not yet implemented." );
-        std::ofstream ofs;
-        ofs.open (filepath, std::ofstream::out);
-        model->getTransitionMatrix().printAsMatlabMatrix(ofs);
-        ofs.close();
+        std::ofstream stream;
+        storm::utility::openFile(filepath, stream);
+        model->getTransitionMatrix().printAsMatlabMatrix(stream);
+        storm::utility::closeFile(stream);
     }
         
 }

src/test/builder/DdJaniModelBuilderTest.cpp

@@ -328,9 +328,42 @@ TEST(DdJaniModelBuilderTest_Cudd, SynchronizationVectors) {
     automataCompositions.push_back(std::make_shared<storm::jani::AutomatonComposition>("one"));
     automataCompositions.push_back(std::make_shared<storm::jani::AutomatonComposition>("two"));
     automataCompositions.push_back(std::make_shared<storm::jani::AutomatonComposition>("three"));
-    
+
     // First, make all actions non-synchronizing.
     std::vector<storm::jani::SynchronizationVector> synchronizationVectors;
+
+    std::vector<std::string> inputVector;
+    inputVector.push_back("a");
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    synchronizationVectors.emplace_back(inputVector);
+    inputVector.clear();
+    inputVector.push_back("c");
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    synchronizationVectors.emplace_back(inputVector);
+    inputVector.clear();
+    inputVector.push_back("d");
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    synchronizationVectors.emplace_back(inputVector);
+    inputVector.clear();
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    inputVector.push_back("b");
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    synchronizationVectors.emplace_back(inputVector);
+    inputVector.clear();
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    inputVector.push_back("c");
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    synchronizationVectors.emplace_back(inputVector);
+    inputVector.clear();
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    inputVector.push_back("c");
+    synchronizationVectors.emplace_back(inputVector);
+    inputVector.clear();
+    
     std::shared_ptr<storm::jani::Composition> newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors);
     janiModel.setSystemComposition(newComposition);
     model = builder.build(janiModel);
@@ -338,22 +371,50 @@ TEST(DdJaniModelBuilderTest_Cudd, SynchronizationVectors) {
     EXPECT_EQ(48ul, model->getNumberOfTransitions());
     
     // Then, make only a, b and c synchronize.
-    std::vector<std::string> inputVector;
+    synchronizationVectors.clear();
+    inputVector.clear();
     inputVector.push_back("a");
     inputVector.push_back("b");
     inputVector.push_back("c");
-    synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d"));
+    synchronizationVectors.emplace_back(inputVector, "d");
+    inputVector.clear();
+    inputVector.push_back("c");
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    synchronizationVectors.emplace_back(inputVector);
+    inputVector.clear();
+    inputVector.push_back("d");
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    synchronizationVectors.emplace_back(inputVector);
+    inputVector.clear();
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    inputVector.push_back("c");
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    synchronizationVectors.emplace_back(inputVector);
+    
     newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors);
     janiModel.setSystemComposition(newComposition);
     model = builder.build(janiModel);
     EXPECT_EQ(7ul, model->getNumberOfStates());
     EXPECT_EQ(10ul, model->getNumberOfTransitions());
 
+    synchronizationVectors.clear();
+    inputVector.clear();
+    inputVector.push_back("a");
+    inputVector.push_back("b");
+    inputVector.push_back("c");
+    synchronizationVectors.emplace_back(inputVector, "d");
     inputVector.clear();
     inputVector.push_back("c");
     inputVector.push_back("c");
     inputVector.push_back("a");
-    synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d"));
+    synchronizationVectors.emplace_back(inputVector, "d");
+    inputVector.clear();
+    inputVector.push_back("d");
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    synchronizationVectors.emplace_back(inputVector);
     newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors);
     janiModel.setSystemComposition(newComposition);
     model = builder.build(janiModel);
@@ -367,7 +428,7 @@ TEST(DdJaniModelBuilderTest_Cudd, SynchronizationVectors) {
     synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "e"));
     newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors);
     janiModel.setSystemComposition(newComposition);
-    EXPECT_THROW(model = builder.build(janiModel), storm::exceptions::InvalidSettingsException);
+    EXPECT_THROW(model = builder.build(janiModel), storm::exceptions::WrongFormatException);
 }
 
 TEST(DdJaniModelBuilderTest_Sylvan, SynchronizationVectors) {
@@ -389,6 +450,39 @@ TEST(DdJaniModelBuilderTest_Sylvan, SynchronizationVectors) {
     
     // First, make all actions non-synchronizing.
     std::vector<storm::jani::SynchronizationVector> synchronizationVectors;
+    
+    std::vector<std::string> inputVector;
+    inputVector.push_back("a");
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    synchronizationVectors.emplace_back(inputVector);
+    inputVector.clear();
+    inputVector.push_back("c");
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    synchronizationVectors.emplace_back(inputVector);
+    inputVector.clear();
+    inputVector.push_back("d");
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    synchronizationVectors.emplace_back(inputVector);
+    inputVector.clear();
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    inputVector.push_back("b");
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    synchronizationVectors.emplace_back(inputVector);
+    inputVector.clear();
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    inputVector.push_back("c");
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    synchronizationVectors.emplace_back(inputVector);
+    inputVector.clear();
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    inputVector.push_back("c");
+    synchronizationVectors.emplace_back(inputVector);
+    inputVector.clear();
+    
     std::shared_ptr<storm::jani::Composition> newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors);
     janiModel.setSystemComposition(newComposition);
     model = builder.build(janiModel);
@@ -396,22 +490,50 @@ TEST(DdJaniModelBuilderTest_Sylvan, SynchronizationVectors) {
     EXPECT_EQ(48ul, model->getNumberOfTransitions());
     
     // Then, make only a, b and c synchronize.
-    std::vector<std::string> inputVector;
+    synchronizationVectors.clear();
+    inputVector.clear();
     inputVector.push_back("a");
     inputVector.push_back("b");
     inputVector.push_back("c");
-    synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d"));
+    synchronizationVectors.emplace_back(inputVector, "d");
+    inputVector.clear();
+    inputVector.push_back("c");
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    synchronizationVectors.emplace_back(inputVector);
+    inputVector.clear();
+    inputVector.push_back("d");
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    synchronizationVectors.emplace_back(inputVector);
+    inputVector.clear();
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    inputVector.push_back("c");
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    synchronizationVectors.emplace_back(inputVector);
+    
     newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors);
     janiModel.setSystemComposition(newComposition);
     model = builder.build(janiModel);
     EXPECT_EQ(7ul, model->getNumberOfStates());
     EXPECT_EQ(10ul, model->getNumberOfTransitions());
     
+    synchronizationVectors.clear();
+    inputVector.clear();
+    inputVector.push_back("a");
+    inputVector.push_back("b");
+    inputVector.push_back("c");
+    synchronizationVectors.emplace_back(inputVector, "d");
     inputVector.clear();
     inputVector.push_back("c");
     inputVector.push_back("c");
     inputVector.push_back("a");
-    synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d"));
+    synchronizationVectors.emplace_back(inputVector, "d");
+    inputVector.clear();
+    inputVector.push_back("d");
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    synchronizationVectors.emplace_back(inputVector);
     newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors);
     janiModel.setSystemComposition(newComposition);
     model = builder.build(janiModel);
@@ -425,7 +547,7 @@ TEST(DdJaniModelBuilderTest_Sylvan, SynchronizationVectors) {
     synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "e"));
     newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors);
     janiModel.setSystemComposition(newComposition);
-    EXPECT_THROW(model = builder.build(janiModel), storm::exceptions::InvalidSettingsException);
+    EXPECT_THROW(model = builder.build(janiModel), storm::exceptions::WrongFormatException);
 }
 
 TEST(DdJaniModelBuilderTest_Sylvan, Composition) {
@@ -433,24 +555,11 @@ TEST(DdJaniModelBuilderTest_Sylvan, Composition) {
     storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
     
     storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double> builder;
-    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.build(janiModel);
-    
-    EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
-    std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
-    
-    EXPECT_EQ(21ul, mdp->getNumberOfStates());
-    EXPECT_EQ(61ul, mdp->getNumberOfTransitions());
-    EXPECT_EQ(61ul, mdp->getNumberOfChoices());
-    
+    EXPECT_THROW(std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.build(janiModel), storm::exceptions::WrongFormatException);
+
     modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/system_composition2.nm");
     janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
-    model = builder.build(janiModel);
-    EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
-    mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
-    
-    EXPECT_EQ(8ul, mdp->getNumberOfStates());
-    EXPECT_EQ(21ul, mdp->getNumberOfTransitions());
-    EXPECT_EQ(21ul, mdp->getNumberOfChoices());
+    EXPECT_THROW(std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.build(janiModel), storm::exceptions::WrongFormatException);
 }
 
 TEST(DdJaniModelBuilderTest_Cudd, Composition) {
@@ -458,24 +567,11 @@ TEST(DdJaniModelBuilderTest_Cudd, Composition) {
     storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
     
     storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder;
-    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.build(janiModel);
-    
-    EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
-    std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
-    
-    EXPECT_EQ(21ul, mdp->getNumberOfStates());
-    EXPECT_EQ(61ul, mdp->getNumberOfTransitions());
-    EXPECT_EQ(61ul, mdp->getNumberOfChoices());
-    
+    EXPECT_THROW(std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.build(janiModel), storm::exceptions::WrongFormatException);
+
     modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/system_composition2.nm");
     janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
-    model = builder.build(janiModel);
-    EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
-    mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
-    
-    EXPECT_EQ(8ul, mdp->getNumberOfStates());
-    EXPECT_EQ(21ul, mdp->getNumberOfTransitions());
-    EXPECT_EQ(21ul, mdp->getNumberOfChoices());
+    EXPECT_THROW(std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.build(janiModel), storm::exceptions::WrongFormatException);
 }
 
 TEST(DdJaniModelBuilderTest_Cudd, InputEnabling) {
@@ -496,12 +592,17 @@ TEST(DdJaniModelBuilderTest_Cudd, InputEnabling) {
     inputVector.push_back("a");
     inputVector.push_back("b");
     inputVector.push_back("c");
-    synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d"));
+    synchronizationVectors.emplace_back(inputVector, "d");
     inputVector.clear();
     inputVector.push_back("c");
     inputVector.push_back("c");
     inputVector.push_back("a");
-    synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d"));
+    synchronizationVectors.emplace_back(inputVector, "d");
+    inputVector.clear();
+    inputVector.push_back("d");
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    synchronizationVectors.emplace_back(inputVector);
     
     std::shared_ptr<storm::jani::Composition> newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors);
     janiModel.setSystemComposition(newComposition);
@@ -528,12 +629,17 @@ TEST(DdJaniModelBuilderTest_Sylvan, InputEnabling) {
     inputVector.push_back("a");
     inputVector.push_back("b");
     inputVector.push_back("c");
-    synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d"));
+    synchronizationVectors.emplace_back(inputVector, "d");
     inputVector.clear();
     inputVector.push_back("c");
     inputVector.push_back("c");
     inputVector.push_back("a");
-    synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d"));
+    synchronizationVectors.emplace_back(inputVector, "d");
+    inputVector.clear();
+    inputVector.push_back("d");
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT);
+    synchronizationVectors.emplace_back(inputVector);
     
     std::shared_ptr<storm::jani::Composition> newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors);
     janiModel.setSystemComposition(newComposition);

src/test/parser/MappedFileTest.cpp

@@ -11,6 +11,7 @@
 #include <string>
 #include "storm/parser/MappedFile.h"
 #include "storm/utility/cstring.h"
+#include "storm/utility/file.h"
 #include "storm/exceptions/FileIoException.h"
 
 TEST(MappedFileTest, NonExistingFile) {
@@ -41,12 +42,12 @@ TEST(MappedFileTest, ExistsAndReadble) {
 	// Test the fileExistsAndIsReadable() method under various circumstances.
 
 	// File exists and is readable.
-	ASSERT_TRUE(storm::parser::MappedFile::fileExistsAndIsReadable(STORM_TEST_RESOURCES_DIR "/txt/testStringFile.txt"));
+	ASSERT_TRUE(storm::utility::fileExistsAndIsReadable(STORM_TEST_RESOURCES_DIR "/txt/testStringFile.txt"));
 
 	// File does not exist.
-	ASSERT_FALSE(storm::parser::MappedFile::fileExistsAndIsReadable(STORM_TEST_RESOURCES_DIR "/nonExistingFile.not"));
+	ASSERT_FALSE(storm::utility::fileExistsAndIsReadable(STORM_TEST_RESOURCES_DIR "/nonExistingFile.not"));
 
 	// File exists but is not readable.
 	// TODO: Find portable solution to providing a situation in which a file exists but is not readable.
-	//ASSERT_FALSE(storm::parser::MappedFile::fileExistsAndIsReadable(STORM_TEST_RESOURCES_DIR "/parser/unreadableFile.txt"));
+	//ASSERT_FALSE(storm::utility::fileExistsAndIsReadable(STORM_TEST_RESOURCES_DIR "/parser/unreadableFile.txt"));
 }