From 22f1d99a157be529ef78017d297d131cd58769f2 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 4 Sep 2015 10:15:32 +0200
Subject: [PATCH] missing files finally added

Former-commit-id: 3ab8472b258eb5fe62d89d805699075a083d510a
---
 src/parser/SparseChoiceLabelingParser.cpp | 73 +++++++++++++++++++++++
 src/parser/SparseChoiceLabelingParser.h   | 27 +++++++++
 2 files changed, 100 insertions(+)
 create mode 100644 src/parser/SparseChoiceLabelingParser.cpp
 create mode 100644 src/parser/SparseChoiceLabelingParser.h

diff --git a/src/parser/SparseChoiceLabelingParser.cpp b/src/parser/SparseChoiceLabelingParser.cpp
new file mode 100644
index 000000000..7bfeeb459
--- /dev/null
+++ b/src/parser/SparseChoiceLabelingParser.cpp
@@ -0,0 +1,73 @@
+#include "src/parser/SparseChoiceLabelingParser.h"
+
+#include "src/exceptions/WrongFormatException.h"
+#include "src/exceptions/OutOfRangeException.h"
+#include "src/exceptions/FileIoException.h"
+#include "src/parser/MappedFile.h"
+#include "src/utility/cstring.h"
+
+namespace storm {
+    namespace parser {
+
+        using namespace storm::utility::cstring;
+
+        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())) {
+                LOG4CPLUS_ERROR(logger, "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();
+
+            uint_fast64_t totalNumberOfChoices = nondeterministicChoiceIndices.back();
+            
+            // Create choice labeling vector with given choice count.
+            std::vector<storm::models::sparse::LabelSet> result(totalNumberOfChoices);
+
+            // Now parse state reward assignments.
+            uint_fast64_t state = 0;
+            uint_fast64_t lastState = (uint_fast64_t) - 1;
+            uint_fast64_t lastChoice = (uint_fast64_t) - 1;
+            uint_fast64_t const startIndexComparison = lastState;
+            uint_fast64_t const startChoiceIndexComparison = lastChoice;
+            uint_fast64_t choice = 0;
+            uint_fast64_t label = 0;
+
+            // Iterate over states.
+            while (buf[0] != '\0') {
+
+                // Parse state number and choice.
+                state = checked_strtol(buf, &buf);
+                choice = checked_strtol(buf, &buf);
+
+                // If the state has already been read or skipped once there might be a problem with the file (doubled lines, or blocks).
+                // Note: The value -1 shows that lastState has not yet been set, i.e. this is the first run of the loop (state index (2^64)-1 is a really bad starting index).
+                if (state < lastState && lastState != startIndexComparison) {
+                    STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while parsing " << filename << ": State " << state << " was found but has already been read or skipped previously.");
+                }
+                if (state == lastState && choice < lastChoice && lastChoice != startChoiceIndexComparison) {
+                    STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while parsing " << filename << ": Choice " << choice << " was found but has already been read or skipped previously.");
+                }
+                if (state >= nondeterministicChoiceIndices.size()) {
+                    STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while parsing " << filename << ": Illegal state " << state << ".");
+                }
+                uint_fast64_t numberOfChoicesForState = nondeterministicChoiceIndices[state + 1] - nondeterministicChoiceIndices[state];
+                if (choice >= numberOfChoicesForState) {
+                    STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while parsing " << filename << ": Choice " << choice << " is illegal for state " << state << ", because this state has fewer choices.");
+                }
+
+                label = checked_strtol(buf, &buf);
+
+                result[nondeterministicChoiceIndices[state] + choice].insert(label);
+
+                buf = trimWhitespaces(buf);
+                lastState = state;
+                lastChoice = choice;
+            }
+
+            return result;
+        }
+    }
+}
\ No newline at end of file
diff --git a/src/parser/SparseChoiceLabelingParser.h b/src/parser/SparseChoiceLabelingParser.h
new file mode 100644
index 000000000..44bc9aedb
--- /dev/null
+++ b/src/parser/SparseChoiceLabelingParser.h
@@ -0,0 +1,27 @@
+#ifndef STORM_PARSER_SPARSECHOICELABELINGPARSER_H_
+#define	STORM_PARSER_SPARSECHOICELABELINGPARSER_H_
+
+#include "src/models/sparse/Model.h"
+
+namespace storm {
+    namespace parser {
+        /*!
+         * A class providing the functionality to parse a choice labeling.
+         */
+        class SparseChoiceLabelingParser {
+        public:
+            /*!
+             * Parses the given file and returns the resulting choice labeling.
+             * 
+             * @param nondeterministicChoiceIndices The indices at which the choices
+             * of the states begin.
+             * @param filename The name of the file to parse.
+             * @return The resulting choice labeling.
+             */
+            static std::vector<storm::models::sparse::LabelSet> parseChoiceLabeling(std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, std::string const& filename);
+        };
+    }
+}
+
+#endif	/* STORM_PARSER_SPARSECHOICELABELINGPARSER_H_ */
+