#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; } } }