tempest/src/storm-parsers/parser/SparseItemLabelingParser.cpp

#include "storm-parsers/parser/SparseItemLabelingParser.h"

#include <cstring>
#include <string>
#include <iostream>

#include "storm-parsers/util/cstring.h"
#include "storm-parsers/parser/MappedFile.h"

#include "storm/utility/macros.h"
#include "storm/exceptions/WrongFormatException.h"
#include "storm/exceptions/FileIoException.h"

namespace storm {
	namespace parser {

		using namespace storm::utility::cstring;

		storm::models::sparse::StateLabeling SparseItemLabelingParser::parseAtomicPropositionLabeling(uint_fast64_t stateCount, std::string const & filename) {
			MappedFile file(filename.c_str());
			checkSyntax(filename, file);
			
			// Create labeling object with given node and label count.
			storm::models::sparse::StateLabeling labeling(stateCount);

			// initialize the buffer
			char const* buf = file.getData();
			
			// add the labels to the labeling
			parseLabelNames(filename, labeling, buf);
			
			// Now parse the assignments of labels to states.
			parseDeterministicLabelAssignments(filename, labeling, buf);

			return labeling;
		}
		
		storm::models::sparse::ChoiceLabeling SparseItemLabelingParser::parseChoiceLabeling(uint_fast64_t choiceCount, std::string const& filename, boost::optional<std::vector<uint_fast64_t>> const& nondeterministicChoiceIndices) {
			MappedFile file(filename.c_str());
			checkSyntax(filename, file);
			
			// Create labeling object with given node and label count.
			storm::models::sparse::ChoiceLabeling labeling(choiceCount);

			// initialize the buffer
			char const* buf = file.getData();
			
			// add the labels to the labeling
			parseLabelNames(filename, labeling, buf);
			
			// Now parse the assignments of labels to states.
			if (nondeterministicChoiceIndices) {
				parseNonDeterministicLabelAssignments(filename, labeling, nondeterministicChoiceIndices.get(), buf);
			} else {
				parseDeterministicLabelAssignments(filename, labeling, buf);
			}

			return labeling;
		}

		
		void SparseItemLabelingParser::checkSyntax(std::string const & filename, storm::parser::MappedFile const& file) {
			char const* buf = file.getData();

			// First pass: Count the number of propositions.
			bool foundDecl = false, foundEnd = false;
			size_t cnt = 0;

			// Iterate over tokens until we hit #END or the end of the file.
			while(buf[0] != '\0') {

				//Move the buffer to the beginning of the next word.
				buf += cnt;
				buf = trimWhitespaces(buf);

				// Get the number of characters until the next separator.
				cnt = skipWord(buf) - buf;
				if (cnt > 0) {

					// If the next token is #DECLARATION: Just skip it.
					// If the next token is #END: Stop the search.
					// Otherwise increase proposition_count.
					if (strncmp(buf, "#DECLARATION", cnt) == 0) {
						foundDecl = true;
						continue;
					} else if (strncmp(buf, "#END", cnt) == 0) {
						foundEnd = true;
						break;
					}
				}
			}

			// If #DECLARATION or #END have not been found, the file format is wrong.
			STORM_LOG_THROW(foundDecl, storm::exceptions::WrongFormatException, "Error while parsing " << filename << ": File header is corrupted (Token #DECLARATION missing - case sensitive).");
			STORM_LOG_THROW(foundEnd, storm::exceptions::WrongFormatException, "Error while parsing " << filename << ": File header is corrupted (Token #END missing - case sensitive).");
		}

		
		void SparseItemLabelingParser::parseLabelNames(std::string const & filename, storm::models::sparse::ItemLabeling& labeling, char const*& buf) {
			// Prepare a buffer for proposition names.
			char proposition[128];
			size_t cnt = 0;

			// Parse proposition names.
			// As we already checked the file header, we know that #DECLARATION and #END are tokens in the character stream.
			while(buf[0] != '\0') {

				//Move the buffer to the beginning of the next word.
				buf += cnt;
				buf = trimWhitespaces(buf);

				// Get the number of characters until the next separator.
				cnt = skipWord(buf) - buf;

				if (cnt >= sizeof(proposition)) {

					// if token is longer than our buffer, the following strncpy code might get risky...
					STORM_LOG_ERROR("Error while parsing " << filename << ": Atomic proposition with length > " << (sizeof(proposition) - 1) << " was found.");
					throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": Atomic proposition with length > " << (sizeof(proposition) - 1) << " was found.";

				} else if (cnt > 0) {

					// If the next token is #DECLARATION: Just skip it.
					if (strncmp(buf, "#DECLARATION", cnt) == 0) continue;

					// If the next token is #END: Stop the search.
					if (strncmp(buf, "#END", cnt) == 0) break;

					// Otherwise copy the token to the buffer, append a trailing null byte and hand it to labeling.
					strncpy(proposition, buf, cnt);
					proposition[cnt] = '\0';
					labeling.addLabel(proposition);
				}
			}

			// At this point, the pointer buf is still pointing to our last token, i.e. to #END.
			// We want to skip it.
			buf += 4;

			// Now eliminate remaining whitespaces such as empty lines and start parsing.
			buf = trimWhitespaces(buf);
		}

		void SparseItemLabelingParser::parseDeterministicLabelAssignments(std::string const & filename, storm::models::sparse::ItemLabeling& labeling, char const*& buf) {
			uint_fast64_t state = 0;
			uint_fast64_t lastState = (uint_fast64_t)-1;
			uint_fast64_t const startIndexComparison = lastState;
			size_t cnt = 0;
			char proposition[128];

			while (buf[0] != '\0') {

				// Parse the state number and iterate over its labels (atomic propositions).
				// Stop at the end of the line.
				state = 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).
				if (state <= lastState && lastState != startIndexComparison) {
					STORM_LOG_ERROR("Error while parsing " << filename << ": State " << state << " was found but has already been read or skipped previously.");
					throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": State " << state << " was found but has already been read or skipped previously.";
				}

				while ((buf[0] != '\r') && (buf[0] != '\n') && (buf[0] != '\0')) {
					cnt = skipWord(buf) - buf;
					if (cnt == 0) {

						// The next character is a separator.
						// If it is a line separator, we continue with next node.
						// Otherwise, we skip it and try again.
						if (buf[0] == '\n' || buf[0] == '\r') break;
						buf++;
					} else {

						// Copy the label to the buffer, null terminate it and add it to labeling.
						strncpy(proposition, buf, cnt);
						proposition[cnt] = '\0';

						// Has the label been declared in the header?
						if(!labeling.containsLabel(proposition)) {
							STORM_LOG_ERROR("Error while parsing " << filename << ": Atomic proposition" << proposition << " was found but not declared.");
							throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": Atomic proposition" << proposition << " was found but not declared.";
						}
                        if (labeling.isStateLabeling()) {
						    labeling.asStateLabeling().addLabelToState(proposition, state);
                        } else {
                            STORM_LOG_ASSERT(labeling.isChoiceLabeling(), "Unexpected labeling type");
                            labeling.asChoiceLabeling().addLabelToChoice(proposition, state);
                        }
						buf += cnt;
					}
				}
				buf = trimWhitespaces(buf);
				lastState = state;
			}
		}

		void SparseItemLabelingParser::parseNonDeterministicLabelAssignments(std::string const & filename, storm::models::sparse::ChoiceLabeling& labeling, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, char const*& buf) {
			uint_fast64_t const startIndexComparison = (uint_fast64_t)-1;
			uint_fast64_t state = 0;
			uint_fast64_t lastState = startIndexComparison;
			uint_fast64_t localChoice = 0;
			uint_fast64_t lastLocalChoice = startIndexComparison;
			size_t cnt = 0;
			char proposition[128];

			while (buf[0] != '\0') {

				// Parse the state and choice number and iterate over its labels (atomic propositions).
				// Stop at the end of the line.
				state = checked_strtol(buf, &buf);
				localChoice = checked_strtol(buf, &buf);
				
				// If we see this state for the first time, reset the last choice
				if (state != lastState) {
					lastLocalChoice = startIndexComparison;
				}

				// If the state-choice pair has already been read or skipped once there might be a problem with the file (doubled lines, or blocks).
                STORM_LOG_THROW(state >= lastState || lastState == startIndexComparison, storm::exceptions::WrongFormatException, "Error while parsing " << filename << ": State " << state << " and Choice " << localChoice << " were found but the state has already been read or skipped previously.");
                STORM_LOG_THROW(state != lastState || localChoice > lastLocalChoice || lastLocalChoice == startIndexComparison, storm::exceptions::WrongFormatException, "Error while parsing " << filename << ": State " << state << " and Choice " << localChoice << " were found but the choice has already been read or skipped previously.");
                
                uint_fast64_t const globalChoice = nondeterministicChoiceIndices[state] + localChoice;
                STORM_LOG_THROW(globalChoice < nondeterministicChoiceIndices[state + 1], storm::exceptions::WrongFormatException, "Error while parsing " << filename << ": Invalid choice index " << localChoice << " at state " << state << ".");

				while ((buf[0] != '\r') && (buf[0] != '\n') && (buf[0] != '\0')) {
					cnt = skipWord(buf) - buf;
					if (cnt == 0) {

						// The next character is a separator.
						// If it is a line separator, we continue with next node.
						// Otherwise, we skip it and try again.
						if (buf[0] == '\n' || buf[0] == '\r') break;
						buf++;
					} else {

						// Copy the label to the buffer, null terminate it and add it to labeling.
						strncpy(proposition, buf, cnt);
						proposition[cnt] = '\0';

						// Has the label been declared in the header?
                        STORM_LOG_THROW(labeling.containsLabel(proposition), storm::exceptions::WrongFormatException, "Error while parsing " << filename << ": Atomic proposition" << proposition << " was found but not declared.");
                        
						labeling.addLabelToChoice(proposition, globalChoice);
						buf += cnt;
					}
				}
				buf = trimWhitespaces(buf);
				lastState = state;
                lastLocalChoice = localChoice;
			}
		}
		
	}  // namespace parser
}  // namespace storm