Further step towards Markov automata parser.

Former-commit-id: 33e4634743

src/models/AbstractModel.cpp

@@ -19,6 +19,7 @@ std::ostream& storm::models::operator<<(std::ostream& os, storm::models::ModelTy
 		case storm::models::CTMC: os << "CTMC"; break;
 		case storm::models::MDP: os << "MDP"; break;
 		case storm::models::CTMDP: os << "CTMDP"; break;
+        case storm::models::MA: os << "MA"; break;
 		default: os << "Invalid ModelType"; break;
 	}
 	return os;

src/models/AtomicPropositionsLabeling.h

@@ -12,7 +12,6 @@
 #include "src/exceptions/OutOfRangeException.h"
 #include <ostream>
 #include <stdexcept>
-#include <unordered_map>
 #include <set>
 
 #include "src/utility/Hash.h"
@@ -146,8 +145,8 @@ public:
 			apCountMax++;
 			singleLabelings.reserve(apCountMax);
 		}
-		nameToLabelingMap[ap] = apsCurrent;
-        singleLabelings.push_back(storm::storage::BitVector(stateCount));
+		nameToLabelingMap.emplace(ap, apsCurrent);
+        singleLabelings.emplace_back(stateCount);
 
 		uint_fast64_t returnValue = apsCurrent++;
 		return returnValue;
@@ -279,10 +278,6 @@ public:
 		}
 	}
 
-	std::unordered_map<std::string, uint_fast64_t> const& getNameToLabelingMap() const {
-		return this->nameToLabelingMap;
-	}
-
 	/*!
 	 * Adds a state to the labeling.
 	 * Since this operation is quite expensive (resizing of all BitVectors containing the labeling), it should
@@ -342,7 +337,7 @@ private:
 	 * by mapping the name to a specific index in the array of all
 	 * individual labelings.
 	 */
-	std::unordered_map<std::string, uint_fast64_t> nameToLabelingMap;
+	std::map<std::string, uint_fast64_t> nameToLabelingMap;
 
 	/*!
 	 * Stores all individual labelings. To find the labeling associated with

src/models/MarkovAutomaton.h

@@ -23,12 +23,12 @@ namespace storm {
 
 		public:
 			MarkovAutomaton(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling,
-							std::vector<uint_fast64_t>&& nondeterministicChoiceIndices,
+							std::vector<uint_fast64_t>&& nondeterministicChoiceIndices, storm::storage::BitVector const& markovianStates,
 							storm::storage::BitVector const& markovianChoices, std::vector<T> const& exitRates,
 							boost::optional<std::vector<T>> const& optionalStateRewardVector, boost::optional<storm::storage::SparseMatrix<T>> const& optionalTransitionRewardMatrix,
 							boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>> const& optionalChoiceLabeling)
 							: AbstractNondeterministicModel<T>(transitionMatrix, stateLabeling, nondeterministicChoiceIndices, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling),
-							  markovianChoices(markovianChoices), exitRates(exitRates) {
+							  markovianStates(markovianStates), markovianChoices(markovianChoices), exitRates(exitRates) {
 				if (this->hasTransitionRewards()) {
 					if (!this->getTransitionRewardMatrix().isSubmatrixOf(this->getTransitionMatrix())) {
 						LOG4CPLUS_ERROR(logger, "Transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist.");
@@ -40,13 +40,13 @@ namespace storm {
 			MarkovAutomaton(storm::storage::SparseMatrix<T>&& transitionMatrix,
 							storm::models::AtomicPropositionsLabeling&& stateLabeling,
 							std::vector<uint_fast64_t>&& nondeterministicChoiceIndices,
+                            storm::storage::BitVector const& markovianStates,
 							storm::storage::BitVector const& markovianChoices, std::vector<T> const& exitRates,
 							boost::optional<std::vector<T>>&& optionalStateRewardVector,
 							boost::optional<storm::storage::SparseMatrix<T>>&& optionalTransitionRewardMatrix,
 							boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>>&& optionalChoiceLabeling)
-							// The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class
 							: AbstractNondeterministicModel<T>(std::move(transitionMatrix), std::move(stateLabeling), std::move(nondeterministicChoiceIndices), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix),
-																std::move(optionalChoiceLabeling)), markovianChoices(std::move(markovianChoices)), exitRates(std::move(exitRates)) {
+																std::move(optionalChoiceLabeling)), markovianStates(markovianStates), markovianChoices(std::move(markovianChoices)), exitRates(std::move(exitRates)) {
 		        if (this->hasTransitionRewards()) {
 		            if (!this->getTransitionRewardMatrix().isSubmatrixOf(this->getTransitionMatrix())) {
 		                LOG4CPLUS_ERROR(logger, "Transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist.");
@@ -55,11 +55,11 @@ namespace storm {
 		        }
 			}
 
-			MarkovAutomaton(MarkovAutomaton<T> const & markovAutomaton) : AbstractNondeterministicModel<T>(markovAutomaton) {
+			MarkovAutomaton(MarkovAutomaton<T> const& markovAutomaton) : AbstractNondeterministicModel<T>(markovAutomaton), exitRates(markovAutomaton.exitRates), markovianStates(markovAutomaton.markovianStates), markovianChoices(markovAutomaton.markovianChoices) {
 				// Intentionally left empty.
 			}
 
-			MarkovAutomaton(MarkovAutomaton<T>&& markovAutomaton) : AbstractNondeterministicModel<T>(std::move(markovAutomaton)) {
+			MarkovAutomaton(MarkovAutomaton<T>&& markovAutomaton) : AbstractNondeterministicModel<T>(std::move(markovAutomaton)), markovianStates(std::move(markovAutomaton.markovianStates)), markovianChoices(std::move(markovAutomaton.markovianChoices)), exitRates(std::move(markovAutomaton.exitRates)) {
 				// Intentionally left empty.
 			}
 
@@ -71,10 +71,88 @@ namespace storm {
 				return MA;
 			}
 
+            virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector<T> const* firstValue = nullptr, std::vector<T> const* secondValue = nullptr, std::vector<uint_fast64_t> const* stateColoring = nullptr, std::vector<std::string> const* colors = nullptr, std::vector<uint_fast64_t>* scheduler = nullptr, bool finalizeOutput = true) const override {
+                AbstractModel<T>::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false);
+
+                // Write the probability distributions for all the states.
+                auto rowIt = this->transitionMatrix.begin();
+                for (uint_fast64_t state = 0, highestStateIndex = this->getNumberOfStates() - 1; state <= highestStateIndex; ++state) {
+                    uint_fast64_t rowCount = this->getNondeterministicChoiceIndices()[state + 1] - this->getNondeterministicChoiceIndices()[state];
+                    bool highlightChoice = true;
+                
+                    // For this, we need to iterate over all available nondeterministic choices in the current state.
+                    for (uint_fast64_t row = 0; row < rowCount; ++row, ++rowIt) {
+                        if (scheduler != nullptr) {
+                            // If the scheduler picked the current choice, we will not make it dotted, but highlight it.
+                            if ((*scheduler)[state] == row) {
+                                highlightChoice = true;
+                            } else {
+                                highlightChoice = false;
+                            }
+                        }
+                        
+                        if (!markovianChoices.get(this->getNondeterministicChoiceIndices()[state] + row)) {
+                            // For each nondeterministic choice, we draw an arrow to an intermediate node to better display
+                            // the grouping of transitions.
+                            outStream << "\t\"" << state << "c" << row << "\" [shape = \"point\"";
+                            
+                            // If we were given a scheduler to highlight, we do so now.
+                            if (scheduler != nullptr) {
+                                if (highlightChoice) {
+                                    outStream << ", fillcolor=\"red\"";
+                                }
+                            }
+                            outStream << "];" << std::endl;
+                            
+                            outStream << "\t" << state << " -> \"" << state << "c" << row << "\"";
+                            
+                            // If we were given a scheduler to highlight, we do so now.
+                            if (scheduler != nullptr) {
+                                if (highlightChoice) {
+                                    outStream << " [color=\"red\", penwidth = 2]";
+                                } else {
+                                    outStream << " [style = \"dotted\"]";
+                                }
+                            }
+                            outStream << ";" << std::endl;
+                            
+                            // Now draw all probabilitic arcs that belong to this nondeterminstic choice.
+                            for (auto transitionIt = rowIt.begin(), transitionIte = rowIt.end(); transitionIt != transitionIte; ++transitionIt) {
+                                if (subsystem == nullptr || subsystem->get(transitionIt.column())) {
+                                    outStream << "\t\"" << state << "c" << row << "\" -> " << transitionIt.column() << " [ label= \"" << transitionIt.value() << "\" ]";
+                                    
+                                    // If we were given a scheduler to highlight, we do so now.
+                                    if (scheduler != nullptr) {
+                                        if (highlightChoice) {
+                                            outStream << " [color=\"red\", penwidth = 2]";
+                                        } else {
+                                            outStream << " [style = \"dotted\"]";
+                                        }
+                                    }
+                                    outStream << ";" << std::endl;
+                                }
+                            }
+                        } else {
+                            // In this case we are emitting a Markovian choice, so draw the arrows directly to the target states.
+                            for (auto transitionIt = rowIt.begin(), transitionIte = rowIt.end(); transitionIt != transitionIte; ++transitionIt) {
+                                if (subsystem == nullptr || subsystem->get(transitionIt.column())) {
+                                    outStream << "\t\"" << state << "\" -> " << transitionIt.column() << " [ label= \"" << transitionIt.value() << "\" ]";
+                                }
+                            }
+                        }
+                    }
+                }
+                        
+                if (finalizeOutput) {
+                    outStream << "}" << std::endl;
+                }
+            }
+            
 		private:
 
-			std::vector<T> exitRates;
+            storm::storage::BitVector markovianStates;
 			storm::storage::BitVector markovianChoices;
+			std::vector<T> exitRates;
 
 		};
 	}

src/parser/AtomicPropositionLabelingParser.cpp

@@ -190,6 +190,7 @@ storm::models::AtomicPropositionsLabeling AtomicPropositionLabelingParser(uint_f
 			buf = storm::parser::trimWhitespaces(buf);
 		}
 	}
+    
 	return labeling;
 }
 

src/parser/AutoParser.h

@@ -8,7 +8,7 @@
 #include "src/models/AbstractModel.h"
 #include "src/parser/DeterministicModelParser.h"
 #include "src/parser/NondeterministicModelParser.h"
-#include "src/parser/MarkovAutomataSparseTransitionParser.h"
+#include "src/parser/MarkovAutomatonParser.h"
 
 #include <memory>
 #include <iostream>
@@ -63,6 +63,10 @@ class AutoParser {
 					this->model.reset(new storm::models::Ctmdp<double>(std::move(NondeterministicModelParserAsCtmdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))));
 					break;
 				}
+                case storm::models::MA: {
+                    this->model.reset(new storm::models::MarkovAutomaton<double>(storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)));
+					break;
+                }
 				default: ;  // Unknown
 			}
 

src/parser/MarkovAutomataSparseTransitionParser.h

@@ -1,47 +0,0 @@
-#ifndef STORM_PARSER_MARKOVAUTOMATASPARSETRANSITIONPARSER_H_
-#define STORM_PARSER_MARKOVAUTOMATASPARSETRANSITIONPARSER_H_
-
-#include "src/storage/SparseMatrix.h"
-#include "src/storage/BitVector.h"
-#include "Parser.h"
-
-namespace storm {
-    namespace parser {
-        
-        class MarkovAutomataSparseTransitionParser {
-        public:
-            struct FirstPassResult {
-                
-                FirstPassResult() : numberOfNonzeroEntries(0), highestStateIndex(0), numberOfChoices(0) {
-                    // Intentionally left empty.
-                }
-                
-                uint_fast64_t numberOfNonzeroEntries;
-                uint_fast64_t highestStateIndex;
-                uint_fast64_t numberOfChoices;
-            };
-            
-            struct ResultType {
-                
-                ResultType(FirstPassResult const& firstPassResult) : transitionMatrix(firstPassResult.numberOfChoices, firstPassResult.highestStateIndex + 1), nondeterministicChoiceIndices(firstPassResult.highestStateIndex + 2), markovianChoices(firstPassResult.numberOfChoices), exitRates(firstPassResult.numberOfChoices) {
-                    transitionMatrix.initialize(firstPassResult.numberOfNonzeroEntries);
-                    // Intentionally left empty.
-                }
-                
-                storm::storage::SparseMatrix<double> transitionMatrix;
-                std::vector<uint_fast64_t> nondeterministicChoiceIndices;
-                storm::storage::BitVector markovianChoices;
-                std::vector<double> exitRates;
-            };
-            
-            static ResultType parseMarkovAutomataTransitions(std::string const& filename, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr);
-            
-        private:
-            static FirstPassResult firstPass(char* buf, SupportedLineEndingsEnum lineEndings, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr);
-            static ResultType secondPass(char* buf, SupportedLineEndingsEnum lineEndings, FirstPassResult const& firstPassResult, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr);
-        };
-        
-    } // namespace parser
-} // namespace storm
-
-#endif /* STORM_PARSER_MARKOVAUTOMATASPARSETRANSITIONPARSER_H_ */

src/parser/MarkovAutomatonParser.cpp

@@ -0,0 +1,28 @@
+#include "MarkovAutomatonParser.h"
+#include "AtomicPropositionLabelingParser.h"
+#include "SparseStateRewardParser.h"
+
+namespace storm {
+    namespace parser {
+        
+        storm::models::MarkovAutomaton<double> MarkovAutomatonParser::parseMarkovAutomaton(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename, std::string const& transitionRewardFilename) {
+            storm::parser::MarkovAutomatonSparseTransitionParser::ResultType transitionResult(storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(transitionsFilename));
+            storm::models::AtomicPropositionsLabeling resultLabeling(storm::parser::AtomicPropositionLabelingParser(transitionResult.transitionMatrix.getColumnCount(), labelingFilename));
+
+            boost::optional<std::vector<double>> stateRewards;
+            if (stateRewardFilename != "") {
+                stateRewards.reset(storm::parser::SparseStateRewardParser(transitionResult.transitionMatrix.getColumnCount(), stateRewardFilename));
+            }
+            
+            if (transitionRewardFilename != "") {
+                LOG4CPLUS_ERROR(logger, "Transition rewards are unsupported for Markov automata.");
+                throw storm::exceptions::WrongFormatException() << "Transition rewards are unsupported for Markov automata.";
+            }
+            
+            storm::models::MarkovAutomaton<double> resultingAutomaton(std::move(transitionResult.transitionMatrix), std::move(resultLabeling), std::move(transitionResult.nondeterministicChoiceIndices), std::move(transitionResult.markovianStates), std::move(transitionResult.markovianChoices), std::move(transitionResult.exitRates), std::move(stateRewards), boost::optional<storm::storage::SparseMatrix<double>>(), boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>>());
+            
+            return resultingAutomaton;
+        }
+        
+    } // namespace parser
+} // namespace storm

src/parser/MarkovAutomatonParser.h

@@ -0,0 +1,29 @@
+#ifndef STORM_PARSER_MARKOVAUTOMATONPARSER_H_
+#define STORM_PARSER_MARKOVAUTOMATONPARSER_H_
+
+#include "src/models/MarkovAutomaton.h"
+#include "src/parser/MarkovAutomatonSparseTransitionParser.h"
+
+namespace storm {
+    namespace parser {
+        
+        /*!
+         * A class providing the functionality to parse a labeled Markov automaton.
+         */
+        class MarkovAutomatonParser {
+        public:
+            
+            /*!
+             * Parses the given Markov automaton and returns an object representing the automaton.
+             *
+             * @param transitionsFilename The name of the file containing the transitions of the Markov automaton.
+             * @param labelingFilename The name of the file containing the labels for the states of the Markov automaton.
+             * @param stateRewardFilename The name of the file that contains the state reward of the Markov automaton.
+             * @param transitionRewardFilename The name of the file that contains the transition rewards of the Markov automaton.
+             */
+            static storm::models::MarkovAutomaton<double> parseMarkovAutomaton(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename, std::string const& transitionRewardFilename);
+        };
+    } // namespace parser
+} // namespace storm
+
+#endif /* STORM_PARSER_MARKOVAUTOMATONPARSER_H_ */

src/parser/MarkovAutomataSparseTransitionParser.cpp → src/parser/MarkovAutomatonSparseTransitionParser.cpp

@@ -1,14 +1,12 @@
-#include "MarkovAutomataSparseTransitionParser.h"
+#include "MarkovAutomatonSparseTransitionParser.h"
 
 #include "src/settings/Settings.h"
 
 namespace storm {
     namespace parser {
  
-        MarkovAutomataSparseTransitionParser::FirstPassResult MarkovAutomataSparseTransitionParser::firstPass(char* buf, SupportedLineEndingsEnum lineEndings, RewardMatrixInformationStruct* rewardMatrixInformation) {
-            bool isRewardFile = rewardMatrixInformation != nullptr;
-            
-            MarkovAutomataSparseTransitionParser::FirstPassResult result;
+        MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTransitionParser::firstPass(char* buf, SupportedLineEndingsEnum lineEndings) {
+            MarkovAutomatonSparseTransitionParser::FirstPassResult result;
 
             // Skip the format hint.
             buf = storm::parser::forwardToNextLine(buf, lineEndings);
@@ -136,7 +134,7 @@ namespace storm {
             return result;
         }
         
-        MarkovAutomataSparseTransitionParser::ResultType MarkovAutomataSparseTransitionParser::secondPass(char* buf, SupportedLineEndingsEnum lineEndings, FirstPassResult const& firstPassResult, RewardMatrixInformationStruct* rewardMatrixInformation) {
+        MarkovAutomatonSparseTransitionParser::ResultType MarkovAutomatonSparseTransitionParser::secondPass(char* buf, SupportedLineEndingsEnum lineEndings, FirstPassResult const& firstPassResult) {
             ResultType result(firstPassResult);
             
             bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks");
@@ -196,8 +194,9 @@ namespace storm {
                 if (strcmp(actionNameBuffer, "!") == 0) {
                     isMarkovianChoice = true;
                     
-                    // Mark the current choice as a Markovian one.
+                    // Mark the current choice and state as a Markovian one.
                     result.markovianChoices.set(currentChoice, true);
+                    result.markovianStates.set(source, true);
                 } else {
                     isMarkovianChoice = false;
                 }
@@ -270,7 +269,7 @@ namespace storm {
             return result;
         }
         
-        MarkovAutomataSparseTransitionParser::ResultType MarkovAutomataSparseTransitionParser::parseMarkovAutomataTransitions(std::string const& filename, RewardMatrixInformationStruct* rewardMatrixInformation) {
+        MarkovAutomatonSparseTransitionParser::ResultType MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(std::string const& filename) {
             // Set the locale to correctly recognize floating point numbers.
             setlocale(LC_NUMERIC, "C");
             
@@ -279,8 +278,6 @@ namespace storm {
                 throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": File does not exist or is not readable.";
             }
             
-            bool isRewardFile = rewardMatrixInformation != nullptr;
-            
             // Determine used line endings.
             SupportedLineEndingsEnum lineEndings = findUsedLineEndings(filename, true);
             
@@ -288,8 +285,8 @@ namespace storm {
             MappedFile file(filename.c_str());
             char* buf = file.data;
             
-            return secondPass(buf, lineEndings, firstPass(buf, lineEndings, rewardMatrixInformation), rewardMatrixInformation);
+            return secondPass(buf, lineEndings, firstPass(buf, lineEndings));
         }
         
-    }
-}
+    } // namespace parser
+} // namespace storm

src/parser/MarkovAutomatonSparseTransitionParser.h

@@ -0,0 +1,95 @@
+#ifndef STORM_PARSER_MARKOVAUTOMATONSPARSETRANSITIONPARSER_H_
+#define STORM_PARSER_MARKOVAUTOMATONSPARSETRANSITIONPARSER_H_
+
+#include "src/storage/SparseMatrix.h"
+#include "src/storage/BitVector.h"
+#include "Parser.h"
+
+namespace storm {
+    namespace parser {
+        
+        /*
+         * A class providing the functionality to parse the transitions of a Markov automaton.
+         */
+        class MarkovAutomatonSparseTransitionParser {
+        public:
+            /*
+             * A structure representing the result of the first pass of this parser. It contains the number of non-zero entries in the model, the highest state index
+             * and the total number of choices.
+             */
+            struct FirstPassResult {
+                
+                FirstPassResult() : numberOfNonzeroEntries(0), highestStateIndex(0), numberOfChoices(0) {
+                    // Intentionally left empty.
+                }
+
+                // The total number of non-zero entries of the model.
+                uint_fast64_t numberOfNonzeroEntries;
+                
+                // The highest state index that appears in the model.
+                uint_fast64_t highestStateIndex;
+                
+                // The total number of choices in the model.
+                uint_fast64_t numberOfChoices;
+            };
+            
+            /*
+             * A structure representing the result of the parser. It contains the sparse matrix that represents the transitions (along with a vector indicating
+             * at which index the choices of a given state begin) as well as the exit rates for all Markovian choices.
+             */
+            struct ResultType {
+                
+                ResultType(FirstPassResult const& firstPassResult) : transitionMatrix(firstPassResult.numberOfChoices, firstPassResult.highestStateIndex + 1), nondeterministicChoiceIndices(firstPassResult.highestStateIndex + 2), markovianChoices(firstPassResult.numberOfChoices), markovianStates(firstPassResult.highestStateIndex + 1), exitRates(firstPassResult.highestStateIndex + 1) {
+                    transitionMatrix.initialize(firstPassResult.numberOfNonzeroEntries);
+                    // Intentionally left empty.
+                }
+                
+                // A matrix representing the transitions of the model.
+                storm::storage::SparseMatrix<double> transitionMatrix;
+                
+                // A vector indicating which rows of the matrix represent the choices of a given state.
+                std::vector<uint_fast64_t> nondeterministicChoiceIndices;
+                
+                // A bit vector indicating which choices are Markovian. By duality, all other choices are probabilitic.
+                storm::storage::BitVector markovianChoices;
+                
+                // A bit vector indicating which states possess a Markovian choice.
+                storm::storage::BitVector markovianStates;
+                
+                // A vector that stores the exit rates for each
+                std::vector<double> exitRates;
+            };
+            
+            /*!
+             * Parses the given file under the assumption that it contains a Markov automaton specified in the appropriate format.
+             *
+             * @param filename The name of the file to parse.
+             * @return A structure representing the result of the parser.
+             */
+            static ResultType parseMarkovAutomatonTransitions(std::string const& filename);
+            
+        private:
+            /*
+             * Performs the first pass on the input pointed to by the given buffer.
+             *
+             * @param buffer The buffer that cointains the input.
+             * @param lineEndings The line endings that are to be used while parsing.
+             * @return A structure representing the result of the first pass.
+             */
+            static FirstPassResult firstPass(char* buffer, SupportedLineEndingsEnum lineEndings);
+            
+            /*
+             * Performs the second pass on the input pointed to by the given buffer with the information of the first pass.
+             *
+             * @param buffer The buffer that cointains the input.
+             * @param lineEndings The line endings that are to be used while parsing.
+             * @param firstPassResult The result of the first pass performed on the same input.
+             * @return A structure representing the result of the second pass.
+             */
+            static ResultType secondPass(char* buffer, SupportedLineEndingsEnum lineEndings, FirstPassResult const& firstPassResult);
+        };
+        
+    } // namespace parser
+} // namespace storm
+
+#endif /* STORM_PARSER_MARKOVAUTOMATONSPARSETRANSITIONPARSER_H_ */

src/storm.cpp

@@ -15,6 +15,7 @@
 
 #include "src/utility/OsDetection.h"
 #include <iostream>
+#include <fstream>
 #include <cstdio>
 #include <sstream>
 #include <vector>
@@ -32,7 +33,7 @@
 #include "src/counterexamples/SMTMinimalCommandSetGenerator.h"
 #include "src/counterexamples/PathBasedSubsystemGenerator.h"
 #include "src/parser/AutoParser.h"
-#include "src/parser/MarkovAutomataSparseTransitionParser.h"
+#include "src/parser/MarkovAutomatonParser.h"
 #include "src/parser/PrctlParser.h"
 #include "src/utility/ErrorHandling.h"
 #include "src/formula/Prctl.h"
@@ -407,7 +408,7 @@ int main(const int argc, const char* argv[]) {
 			// If parsing failed or the option to see the usage was set, program execution stops here.
 			return 0;
 		}
-
+        
 		// Now, the settings are received and the specified model is parsed. The actual actions taken depend on whether
         // the model was provided in explicit or symbolic format.
 		storm::settings::Settings* s = storm::settings::Settings::getInstance();
@@ -426,6 +427,33 @@ int main(const int argc, const char* argv[]) {
 
 			storm::parser::AutoParser<double> parser(chosenTransitionSystemFile, chosenLabelingFile, chosenStateRewardsFile, chosenTransitionRewardsFile);
 
+            if (s->isSet("exportdot")) {
+                std::ofstream outputFileStream;
+                outputFileStream.open(s->getOptionByLongName("exportdot").getArgument(0).getValueAsString(), std::ofstream::out);
+                switch (parser.getType()) {
+                    case storm::models::DTMC:
+                        parser.getModel<storm::models::Dtmc<double>>()->writeDotToStream(outputFileStream);
+                        break;
+                    case storm::models::CTMC:
+                        parser.getModel<storm::models::Ctmc<double>>()->writeDotToStream(outputFileStream);
+                        break;
+                    case storm::models::MDP:
+                        parser.getModel<storm::models::Mdp<double>>()->writeDotToStream(outputFileStream);
+                        break;
+                    case storm::models::CTMDP:
+                        parser.getModel<storm::models::Ctmdp<double>>()->writeDotToStream(outputFileStream);
+                        break;
+                    case storm::models::MA:
+                        parser.getModel<storm::models::MarkovAutomaton<double>>()->writeDotToStream(outputFileStream);
+                        break;
+                    default:
+                        LOG4CPLUS_ERROR(logger, "Illegal model type.");
+                        break;
+                }
+                
+                outputFileStream.close();
+            }
+            
 			//Should there be a counterexample generated in case the formula is not satisfied?
 			if(s->isSet("counterExample")) {
 
@@ -438,6 +466,7 @@ int main(const int argc, const char* argv[]) {
 				// Depending on the model type, the appropriate model checking procedure is chosen.
 				storm::modelchecker::prctl::AbstractModelChecker<double>* modelchecker = nullptr;
 				parser.getModel<storm::models::AbstractModel<double>>()->printModelInformationToStream(std::cout);
+                
 				switch (parser.getType()) {
 				case storm::models::DTMC:
 					LOG4CPLUS_INFO(logger, "Model is a DTMC.");
@@ -457,6 +486,9 @@ int main(const int argc, const char* argv[]) {
 					LOG4CPLUS_INFO(logger, "Model is a CTMDP.");
 					LOG4CPLUS_ERROR(logger, "The selected model type is not supported.");
 					break;
+                case storm::models::MA:
+                    LOG4CPLUS_INFO(logger, "Model is a Markov automaton.");
+                    break;
 				case storm::models::Unknown:
 				default:
 					LOG4CPLUS_ERROR(logger, "The model type could not be determined correctly.");
@@ -503,7 +535,7 @@ int main(const int argc, const char* argv[]) {
                 }
             }
         }
-
+        
         // Perform clean-up and terminate.
 		cleanUp();
 		LOG4CPLUS_INFO(logger, "StoRM terminating.");

src/utility/StormOptions.cpp

@@ -12,6 +12,8 @@ bool storm::utility::StormOptions::optionsRegistered = storm::settings::Settings
     
 	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "logfile", "l", "If specified, the log output will also be written to this file.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("logFileName", "The path and name of the file to write to.").build()).build());
     
+    settings->addOption(storm::settings::OptionBuilder("StoRM Main", "exportdot", "", "If specified, the loaded model will be written to the specified file in the dot format.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("dotFileName", "The file to export the model to.").build()).build());
+    
 	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "configfile", "c", "If specified, this file will be read and parsed for additional configuration settings.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("configFileName", "The path and name of the file from which to read.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
     
 	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "explicit", "", "Explicit parsing from transition- and labeling files.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("transitionFileName", "The path and name of the file from which to read the transitions.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).addArgument(storm::settings::ArgumentBuilder::createStringArgument("labelingFileName", "The path and name of the file from which to read the labeling.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());