From 28910462ec7b8861424137d220d2509eca4088c3 Mon Sep 17 00:00:00 2001 From: masawei Date: Wed, 12 Mar 2014 22:47:16 +0100 Subject: [PATCH] Necessary changes to the nondeterministic parses to compensate for the change in the way the mapping between states of the model and the rows of the transition matrix are handled. - All tests are green. - Some comments are now a bit wrong. Next up: Correct comments. Former-commit-id: 610c0282b26e11cbe02804fe3daa9b241ed352b1 --- .../AtomicPropositionLabelingParser.cpp | 4 +- src/parser/MarkovAutomatonParser.cpp | 8 +- .../MarkovAutomatonSparseTransitionParser.cpp | 10 ++- .../MarkovAutomatonSparseTransitionParser.h | 5 +- src/parser/NondeterministicModelParser.cpp | 12 +-- src/parser/NondeterministicModelParser.h | 12 +-- ...NondeterministicSparseTransitionParser.cpp | 73 +++++++++++-------- .../NondeterministicSparseTransitionParser.h | 44 +---------- src/parser/SparseStateRewardParser.cpp | 4 +- ...kovAutomatonSparseTransitionParserTest.cpp | 37 +++++----- ...eterministicSparseTransitionParserTest.cpp | 71 +++++++++--------- 11 files changed, 129 insertions(+), 151 deletions(-) diff --git a/src/parser/AtomicPropositionLabelingParser.cpp b/src/parser/AtomicPropositionLabelingParser.cpp index 43c5d308a..0dac9a8c9 100644 --- a/src/parser/AtomicPropositionLabelingParser.cpp +++ b/src/parser/AtomicPropositionLabelingParser.cpp @@ -126,7 +126,7 @@ namespace storm { buf = trimWhitespaces(buf); uint_fast64_t state = 0; - uint_fast64_t lastState = -1; + uint_fast64_t lastState = (uint_fast64_t)-1; cnt = 0; // Now parse the assignments of labels to nodes. @@ -137,7 +137,7 @@ namespace storm { 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 != -1) { + if(state <= lastState && lastState != (uint_fast64_t)-1) { LOG4CPLUS_ERROR(logger, "Wrong file format in (" << filename << "). State " << state << " was found but has already been read or skipped previously."); throw storm::exceptions::WrongFormatException() << "State " << state << " was found but has already been read or skipped previously."; } diff --git a/src/parser/MarkovAutomatonParser.cpp b/src/parser/MarkovAutomatonParser.cpp index 91a01c286..707436dab 100644 --- a/src/parser/MarkovAutomatonParser.cpp +++ b/src/parser/MarkovAutomatonParser.cpp @@ -3,6 +3,10 @@ #include "SparseStateRewardParser.h" #include "src/exceptions/WrongFormatException.h" +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" +extern log4cplus::Logger logger; + namespace storm { namespace parser { @@ -12,7 +16,7 @@ namespace storm { storm::parser::MarkovAutomatonSparseTransitionParser::Result transitionResult(storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(transitionsFilename)); // Build the actual transition matrix using the MatrixBuilder provided by the transitionResult. - storm::storage::SparseMatrix transitionMatrix(transitionResult.transitionMatrixBuilder.build(0,0)); + storm::storage::SparseMatrix transitionMatrix(transitionResult.transitionMatrixBuilder.build()); // Parse the state labeling. storm::models::AtomicPropositionsLabeling resultLabeling(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(transitionMatrix.getColumnCount(), labelingFilename)); @@ -30,7 +34,7 @@ namespace storm { } // Put the pieces together to generate the Markov Automaton. - storm::models::MarkovAutomaton resultingAutomaton(std::move(transitionMatrix), std::move(resultLabeling), std::move(transitionResult.nondeterministicChoiceIndices), std::move(transitionResult.markovianStates), std::move(transitionResult.exitRates), std::move(stateRewards), boost::optional>(), boost::optional>>()); + storm::models::MarkovAutomaton resultingAutomaton(std::move(transitionMatrix), std::move(resultLabeling), std::move(transitionResult.markovianStates), std::move(transitionResult.exitRates), std::move(stateRewards), boost::optional>(), boost::optional>>()); return resultingAutomaton; } diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/parser/MarkovAutomatonSparseTransitionParser.cpp index 10682dc04..0fac2eb18 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.cpp +++ b/src/parser/MarkovAutomatonSparseTransitionParser.cpp @@ -170,6 +170,10 @@ namespace storm { uint_fast64_t lastsource = 0; bool encounteredEOF = false; uint_fast64_t currentChoice = 0; + + // The first choice of the first state already starts a new row group of the matrix. + result.transitionMatrixBuilder.newRowGroup(0); + while (buf[0] != '\0' && !encounteredEOF) { // At the current point, the next thing to read is the source state of the next choice to come. source = checked_strtol(buf, &buf); @@ -178,7 +182,7 @@ namespace storm { if (source > lastsource + 1) { if (fixDeadlocks) { for (uint_fast64_t index = lastsource + 1; index < source; ++index) { - result.nondeterministicChoiceIndices[index] = currentChoice; + result.transitionMatrixBuilder.newRowGroup(currentChoice); result.transitionMatrixBuilder.addNextValue(currentChoice, index, 1); ++currentChoice; } @@ -190,7 +194,7 @@ namespace storm { if (source != lastsource) { // If we skipped to a new state we need to record the beginning of the choices in the nondeterministic choice indices. - result.nondeterministicChoiceIndices[source] = currentChoice; + result.transitionMatrixBuilder.newRowGroup(currentChoice); } // Record that the current source was the last source. @@ -253,7 +257,7 @@ namespace storm { } // Put a sentinel element at the end. - result.nondeterministicChoiceIndices[firstPassResult.highestStateIndex + 1] = currentChoice; + result.transitionMatrixBuilder.newRowGroup(currentChoice); return result; } diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.h b/src/parser/MarkovAutomatonSparseTransitionParser.h index c6019d934..de82c28b8 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.h +++ b/src/parser/MarkovAutomatonSparseTransitionParser.h @@ -52,16 +52,13 @@ namespace storm { * * @param firstPassResult A reference to the result of the first pass. */ - Result(FirstPassResult const& firstPassResult) : transitionMatrixBuilder(firstPassResult.numberOfChoices, firstPassResult.highestStateIndex + 1, firstPassResult.numberOfNonzeroEntries), nondeterministicChoiceIndices(firstPassResult.highestStateIndex + 2), markovianChoices(firstPassResult.numberOfChoices), markovianStates(firstPassResult.highestStateIndex + 1), exitRates(firstPassResult.highestStateIndex + 1) { + Result(FirstPassResult const& firstPassResult) : transitionMatrixBuilder(firstPassResult.numberOfChoices, firstPassResult.highestStateIndex + 1, firstPassResult.numberOfNonzeroEntries, true, firstPassResult.highestStateIndex + 1), markovianChoices(firstPassResult.numberOfChoices), markovianStates(firstPassResult.highestStateIndex + 1), exitRates(firstPassResult.highestStateIndex + 1) { // Intentionally left empty. } //! A matrix representing the transitions of the model. storm::storage::SparseMatrixBuilder transitionMatrixBuilder; - //! A vector indicating which rows of the matrix represent the choices of a given state. - std::vector nondeterministicChoiceIndices; - //! A bit vector indicating which choices are Markovian. By duality, all other choices are probabilitic. storm::storage::BitVector markovianChoices; diff --git a/src/parser/NondeterministicModelParser.cpp b/src/parser/NondeterministicModelParser.cpp index d150b8c84..fc66dacfb 100644 --- a/src/parser/NondeterministicModelParser.cpp +++ b/src/parser/NondeterministicModelParser.cpp @@ -20,9 +20,9 @@ namespace storm { NondeterministicModelParser::Result NondeterministicModelParser::parseNondeterministicModel(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename, std::string const & transitionRewardFilename) { // Parse the transitions. - NondeterministicSparseTransitionParser::Result transitions(std::move(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(transitionsFilename))); + storm::storage::SparseMatrix transitions(std::move(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(transitionsFilename))); - uint_fast64_t stateCount = transitions.transitionMatrix.getColumnCount(); + uint_fast64_t stateCount = transitions.getColumnCount(); // Parse the state labeling. storm::models::AtomicPropositionsLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFilename))); @@ -36,11 +36,11 @@ namespace storm { // Only parse transition rewards if a file is given. boost::optional> transitionRewards; if (transitionRewardFilename != "") { - transitionRewards = storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(transitionRewardFilename, transitions).transitionMatrix; + transitionRewards = storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(transitionRewardFilename, transitions); } // Construct the result. - Result result(std::move(transitions.transitionMatrix), std::move(transitions.rowMapping), std::move(labeling)); + Result result(std::move(transitions), std::move(labeling)); result.stateRewards = stateRewards; result.transitionRewards = transitionRewards; @@ -50,13 +50,13 @@ namespace storm { storm::models::Mdp NondeterministicModelParser::parseMdp(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename, std::string const & transitionRewardFilename) { Result parserResult = parseNondeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename); - return storm::models::Mdp(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); + return storm::models::Mdp(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); } storm::models::Ctmdp NondeterministicModelParser::parseCtmdp(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename, std::string const & transitionRewardFilename) { Result parserResult = parseNondeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename); - return storm::models::Ctmdp(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); + return storm::models::Ctmdp(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); } } /* namespace parser */ diff --git a/src/parser/NondeterministicModelParser.h b/src/parser/NondeterministicModelParser.h index 376c3e8c6..5de438fde 100644 --- a/src/parser/NondeterministicModelParser.h +++ b/src/parser/NondeterministicModelParser.h @@ -33,10 +33,9 @@ namespace storm { * The copy constructor. * * @param transitionSystem The transition system to be contained in the Result. - * @param rowMapping The mapping between matrix rows and model states to be contained in the Result. * @param labeling The the labeling of the transition system to be contained in the Result. */ - Result(storm::storage::SparseMatrix& transitionSystem, std::vector& rowMapping, storm::models::AtomicPropositionsLabeling& labeling) : transitionSystem(transitionSystem), labeling(labeling), rowMapping(rowMapping) { + Result(storm::storage::SparseMatrix& transitionSystem, storm::models::AtomicPropositionsLabeling& labeling) : transitionSystem(transitionSystem), labeling(labeling) { // Intentionally left empty. } @@ -44,10 +43,9 @@ namespace storm { * The move constructor. * * @param transitionSystem The transition system to be contained in the Result. - * @param rowMapping The mapping between matrix rows and model states to be contained in the Result. * @param labeling The the labeling of the transition system to be contained in the Result. */ - Result(storm::storage::SparseMatrix&& transitionSystem, std::vector&& rowMapping, storm::models::AtomicPropositionsLabeling&& labeling) : transitionSystem(std::move(transitionSystem)), labeling(std::move(labeling)), rowMapping(std::move(rowMapping)) { + Result(storm::storage::SparseMatrix&& transitionSystem, storm::models::AtomicPropositionsLabeling&& labeling) : transitionSystem(std::move(transitionSystem)), labeling(std::move(labeling)) { // Intentionally left empty. } @@ -61,12 +59,6 @@ namespace storm { */ storm::models::AtomicPropositionsLabeling labeling; - /*! - * A mapping from rows of the matrix to states of the model. - * This resolves the nondeterministic choices inside the transition system. - */ - std::vector rowMapping; - /*! * Optional rewards for each state. */ diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp index 6e16b2f43..3d8a0826c 100644 --- a/src/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/parser/NondeterministicSparseTransitionParser.cpp @@ -26,19 +26,19 @@ namespace storm { using namespace storm::utility::cstring; - NondeterministicSparseTransitionParser::Result NondeterministicSparseTransitionParser::parseNondeterministicTransitions(std::string const& filename) { + storm::storage::SparseMatrix NondeterministicSparseTransitionParser::parseNondeterministicTransitions(std::string const& filename) { - Result emptyResult; + storm::storage::SparseMatrix emptyMatrix; - return NondeterministicSparseTransitionParser::parse(filename, false, emptyResult); + return NondeterministicSparseTransitionParser::parse(filename, false, emptyMatrix); } - NondeterministicSparseTransitionParser::Result NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(std::string const& filename, Result const & modelInformation) { + storm::storage::SparseMatrix NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(std::string const& filename, storm::storage::SparseMatrix const & modelInformation) { return NondeterministicSparseTransitionParser::parse(filename, true, modelInformation); } - NondeterministicSparseTransitionParser::Result NondeterministicSparseTransitionParser::parse(std::string const &filename, bool isRewardFile, Result const & modelInformation) { + storm::storage::SparseMatrix NondeterministicSparseTransitionParser::parse(std::string const &filename, bool isRewardFile, storm::storage::SparseMatrix const & modelInformation) { // Enforce locale where decimal point is '.'. setlocale(LC_NUMERIC, "C"); @@ -72,17 +72,17 @@ namespace storm { if (isRewardFile) { // The reward matrix should match the size of the transition matrix. - if (firstPass.choices > modelInformation.transitionMatrix.getRowCount() || (uint_fast64_t)(firstPass.highestStateIndex + 1) > modelInformation.transitionMatrix.getColumnCount()) { + if (firstPass.choices > modelInformation.getRowCount() || (uint_fast64_t)(firstPass.highestStateIndex + 1) > modelInformation.getColumnCount()) { LOG4CPLUS_ERROR(logger, "Reward matrix size exceeds transition matrix size."); throw storm::exceptions::OutOfRangeException() << "Reward matrix size exceeds transition matrix size."; - } else if (firstPass.choices != modelInformation.transitionMatrix.getRowCount()) { + } else if (firstPass.choices != modelInformation.getRowCount()) { LOG4CPLUS_ERROR(logger, "Reward matrix row count does not match transition matrix row count."); throw storm::exceptions::OutOfRangeException() << "Reward matrix row count does not match transition matrix row count."; - } else if(firstPass.numberOfNonzeroEntries > modelInformation.transitionMatrix.getEntryCount()) { + } else if(firstPass.numberOfNonzeroEntries > modelInformation.getEntryCount()) { LOG4CPLUS_ERROR(logger, "The reward matrix has more entries than the transition matrix. There must be a reward for a non existent transition"); throw storm::exceptions::OutOfRangeException() << "The reward matrix has more entries than the transition matrix."; } else { - firstPass.highestStateIndex = modelInformation.transitionMatrix.getColumnCount() - 1; + firstPass.highestStateIndex = modelInformation.getColumnCount() - 1; } } @@ -90,10 +90,12 @@ namespace storm { // The matrix to be build should have as many columns as we have nodes and as many rows as we have choices. // Those two values, as well as the number of nonzero elements, was been calculated in the first run. LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << firstPass.choices << " x " << (firstPass.highestStateIndex+1) << " with " << firstPass.numberOfNonzeroEntries << " entries."); - storm::storage::SparseMatrixBuilder matrixBuilder(firstPass.choices, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries); - - // Create row mapping. - std::vector rowMapping(firstPass.highestStateIndex + 2, 0); + storm::storage::SparseMatrixBuilder matrixBuilder; + if(!isRewardFile) { + matrixBuilder = storm::storage::SparseMatrixBuilder(firstPass.choices, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries, true, firstPass.highestStateIndex + 1); + } else { + matrixBuilder = storm::storage::SparseMatrixBuilder(firstPass.choices, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries, true, modelInformation.getRowGroupCount()); + } // Initialize variables for the parsing run. uint_fast64_t source = 0, target = 0, lastSource = 0, choice = 0, lastChoice = 0, curRow = 0; @@ -101,6 +103,9 @@ namespace storm { bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks"); bool hadDeadlocks = false; + // The first state already starts a new row group of the matrix. + matrixBuilder.newRowGroup(0); + // Read all transitions from file. while (buf[0] != '\0') { @@ -112,13 +117,13 @@ namespace storm { // If we have switched the source state, we possibly need to insert the rows of the last // source state. if (source != lastSource) { - curRow += ((modelInformation.rowMapping)[lastSource + 1] - (modelInformation.rowMapping)[lastSource]) -(lastChoice + 1); + curRow += ((modelInformation.getRowGroupIndices())[lastSource + 1] - (modelInformation.getRowGroupIndices())[lastSource]) -(lastChoice + 1); } // If we skipped some states, we need to reserve empty rows for all their nondeterministic // choices. for (uint_fast64_t i = lastSource + 1; i < source; ++i) { - curRow += ((modelInformation.rowMapping)[i + 1] - (modelInformation.rowMapping)[i]); + curRow += ((modelInformation.getRowGroupIndices())[i + 1] - (modelInformation.getRowGroupIndices())[i]); } // If we advanced to the next state, but skipped some choices, we have to reserve rows @@ -140,7 +145,7 @@ namespace storm { for (uint_fast64_t node = lastSource + 1; node < source; node++) { hadDeadlocks = true; if (fixDeadlocks) { - rowMapping.at(node) = curRow; + matrixBuilder.newRowGroup(curRow); matrixBuilder.addNextValue(curRow, node, 1); ++curRow; LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted."); @@ -150,7 +155,7 @@ namespace storm { } if (source != lastSource) { // Add this source to rowMapping, if this is the first choice we encounter for this state. - rowMapping.at(source) = curRow; + matrixBuilder.newRowGroup(curRow); } } @@ -168,25 +173,33 @@ namespace storm { buf = trimWhitespaces(buf); } - for (uint_fast64_t node = lastSource + 1; node <= firstPass.highestStateIndex + 1; node++) { - rowMapping.at(node) = curRow + 1; - } - if (!fixDeadlocks && hadDeadlocks && !isRewardFile) throw storm::exceptions::WrongFormatException() << "Some of the nodes had deadlocks. You can use --fixDeadlocks to insert self-loops on the fly."; - // Finally, build the actual matrix, test and return it together with the rowMapping. + // Since we assume the transition rewards are for the transitions of the model, we copy the rowGroupIndices. + if(isRewardFile) { + // We already have rowGroup 0. + for(uint_fast64_t index = 1; index < modelInformation.getRowGroupIndices().size(); index++) { + matrixBuilder.newRowGroup(modelInformation.getRowGroupIndices()[index]); + } + } else { + for (uint_fast64_t node = lastSource + 1; node <= firstPass.highestStateIndex; node++) { + matrixBuilder.newRowGroup(curRow + 1); + } + } + + // Finally, build the actual matrix, test and return. storm::storage::SparseMatrix resultMatrix = matrixBuilder.build(); // Since we cannot do the testing if each transition for which there is a reward in the reward file also exists in the transition matrix during parsing, we have to do it afterwards. - if(isRewardFile && !resultMatrix.isSubmatrixOf(modelInformation.transitionMatrix)) { + if(isRewardFile && !resultMatrix.isSubmatrixOf(modelInformation)) { LOG4CPLUS_ERROR(logger, "There are rewards for non existent transitions given in the reward file."); throw storm::exceptions::WrongFormatException() << "There are rewards for non existent transitions given in the reward file."; } - return NondeterministicSparseTransitionParser::Result(resultMatrix, rowMapping); + return resultMatrix; } - NondeterministicSparseTransitionParser::FirstPassResult NondeterministicSparseTransitionParser::firstPass(char* buf, bool isRewardFile, Result const & modelInformation) { + NondeterministicSparseTransitionParser::FirstPassResult NondeterministicSparseTransitionParser::firstPass(char* buf, bool isRewardFile, storm::storage::SparseMatrix const & modelInformation) { // Check file header and extract number of transitions. @@ -228,13 +241,13 @@ namespace storm { // source state. if (source != lastSource) { // number of choices skipped = number of choices of last state - number of choices read - result.choices += ((modelInformation.rowMapping)[lastSource + 1] - (modelInformation.rowMapping)[lastSource]) - (lastChoice + 1); + result.choices += ((modelInformation.getRowGroupIndices())[lastSource + 1] - (modelInformation.getRowGroupIndices())[lastSource]) - (lastChoice + 1); } // If we skipped some states, we need to reserve empty rows for all their nondeterministic // choices. for (uint_fast64_t i = lastSource + 1; i < source; ++i) { - result.choices += ((modelInformation.rowMapping)[i + 1] - (modelInformation.rowMapping)[i]); + result.choices += ((modelInformation.getRowGroupIndices())[i + 1] - (modelInformation.getRowGroupIndices())[i]); } // If we advanced to the next state, but skipped some choices, we have to reserve rows @@ -302,12 +315,12 @@ namespace storm { if (isRewardFile) { // If not all rows were filled for the last state, we need to insert them. - result.choices += ((modelInformation.rowMapping)[lastSource + 1] - (modelInformation.rowMapping)[lastSource] ) - (lastChoice + 1); + result.choices += ((modelInformation.getRowGroupIndices())[lastSource + 1] - (modelInformation.getRowGroupIndices())[lastSource] ) - (lastChoice + 1); // If we skipped some states, we need to reserve empty rows for all their nondeterministic // choices. - for (uint_fast64_t i = lastSource + 1; i < modelInformation.rowMapping.size() - 1; ++i) { - result.choices += ((modelInformation.rowMapping)[i + 1] - (modelInformation.rowMapping)[i]); + for (uint_fast64_t i = lastSource + 1; i < modelInformation.getRowGroupIndices().size() - 1; ++i) { + result.choices += ((modelInformation.getRowGroupIndices())[i + 1] - (modelInformation.getRowGroupIndices())[i]); } } diff --git a/src/parser/NondeterministicSparseTransitionParser.h b/src/parser/NondeterministicSparseTransitionParser.h index aea0f8fcc..f75babbb7 100644 --- a/src/parser/NondeterministicSparseTransitionParser.h +++ b/src/parser/NondeterministicSparseTransitionParser.h @@ -43,48 +43,12 @@ namespace storm { uint_fast64_t choices; }; - /*! - * A structure representing the result of the parser. - * It contains the resulting matrix as well as the row mapping. - */ - struct Result { - - /*! - * The default constructor. - * Constructs an empty Result. - */ - Result() : transitionMatrix(), rowMapping() { - // Intentionally left empty. - } - - /*! - * Constructs a Result, initializing its members with the given values. - * - * @param transitionMatrix The matrix containing the parsed transition system. - * @param rowMapping A mapping from rows of the matrix to states of the model. - */ - Result(storm::storage::SparseMatrix transitionMatrix, std::vector rowMapping) : transitionMatrix(transitionMatrix), rowMapping(rowMapping) { - // Intentionally left empty. - } - - /*! - * The matrix containing the parsed transition system. - */ - storm::storage::SparseMatrix transitionMatrix; - - /*! - * A mapping from rows of the matrix to states of the model. - * This resolves the nondeterministic choices inside the transition system. - */ - std::vector rowMapping; - }; - /*! * Load a nondeterministic transition system from file and create a sparse adjacency matrix whose entries represent the weights of the edges * * @param filename The path and name of file to be parsed. */ - static Result parseNondeterministicTransitions(std::string const & filename); + static storm::storage::SparseMatrix parseNondeterministicTransitions(std::string const & filename); /*! * Load a nondeterministic transition system from file and create a sparse adjacency matrix whose entries represent the weights of the edges @@ -93,7 +57,7 @@ namespace storm { * @param modelInformation The information about the transition structure of nondeterministic model in which the transition rewards shall be used. * @return A struct containing the parsed file contents, i.e. the transition reward matrix and the mapping between its rows and the states of the model. */ - static Result parseNondeterministicTransitionRewards(std::string const & filename, Result const & modelInformation); + static storm::storage::SparseMatrix parseNondeterministicTransitionRewards(std::string const & filename, storm::storage::SparseMatrix const & modelInformation); private: @@ -110,7 +74,7 @@ namespace storm { * @param insertDiagonalEntriesIfMissing A flag set iff entries on the primary diagonal of the matrix should be added in case they are missing in the parsed file. * @return A structure representing the result of the first pass. */ - static FirstPassResult firstPass(char* buffer, bool isRewardFile, Result const & modelInformation); + static FirstPassResult firstPass(char* buffer, bool isRewardFile, storm::storage::SparseMatrix const & modelInformation); /*! * The main parsing routine. @@ -122,7 +86,7 @@ namespace storm { * @param modelInformation A struct containing information that is used to check if the transition reward matrix fits to the rest of the model. * @return A SparseMatrix containing the parsed file contents. */ - static Result parse(std::string const& filename, bool isRewardFile, Result const & modelInformation); + static storm::storage::SparseMatrix parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix const & modelInformation); }; diff --git a/src/parser/SparseStateRewardParser.cpp b/src/parser/SparseStateRewardParser.cpp index a71d741ad..679bb5e7e 100644 --- a/src/parser/SparseStateRewardParser.cpp +++ b/src/parser/SparseStateRewardParser.cpp @@ -36,7 +36,7 @@ namespace storm { // Now parse state reward assignments. uint_fast64_t state = 0; - uint_fast64_t lastState = -1; + uint_fast64_t lastState = (uint_fast64_t)-1; double reward; // Iterate over states. @@ -47,7 +47,7 @@ namespace storm { // 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 != -1) { + if(state <= lastState && lastState != (uint_fast64_t)-1) { LOG4CPLUS_ERROR(logger, "State " << state << " was found but has already been read or skipped previously."); throw storm::exceptions::WrongFormatException() << "State " << state << " was found but has already been read or skipped previously."; } diff --git a/test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp b/test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp index f5dcbc1d2..0af549586 100644 --- a/test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp +++ b/test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp @@ -42,22 +42,23 @@ TEST(MarkovAutomatonSparseTransitionParserTest, BasicParsing) { ASSERT_EQ(transitionMatrix.getColumnCount(), STATE_COUNT); ASSERT_EQ(transitionMatrix.getRowCount(), CHOICE_COUNT); ASSERT_EQ(transitionMatrix.getEntryCount(), 12); + ASSERT_EQ(transitionMatrix.getRowGroupCount(), 6); + ASSERT_EQ(transitionMatrix.getRowGroupIndices().size(), 7); ASSERT_EQ(result.markovianChoices.size(), CHOICE_COUNT); ASSERT_EQ(result.markovianStates.size(), STATE_COUNT); ASSERT_EQ(result.markovianStates.getNumberOfSetBits(), 2); ASSERT_EQ(result.exitRates.size(), STATE_COUNT); - ASSERT_EQ(result.nondeterministicChoiceIndices.size(), 7); // Test the general structure of the transition system (that will be an Markov automaton). // Test the mapping between states and transition matrix rows. - ASSERT_EQ(result.nondeterministicChoiceIndices[0], 0); - ASSERT_EQ(result.nondeterministicChoiceIndices[1], 1); - ASSERT_EQ(result.nondeterministicChoiceIndices[2], 2); - ASSERT_EQ(result.nondeterministicChoiceIndices[3], 3); - ASSERT_EQ(result.nondeterministicChoiceIndices[4], 4); - ASSERT_EQ(result.nondeterministicChoiceIndices[5], 6); - ASSERT_EQ(result.nondeterministicChoiceIndices[6], 7); + ASSERT_EQ(transitionMatrix.getRowGroupIndices()[0], 0); + ASSERT_EQ(transitionMatrix.getRowGroupIndices()[1], 1); + ASSERT_EQ(transitionMatrix.getRowGroupIndices()[2], 2); + ASSERT_EQ(transitionMatrix.getRowGroupIndices()[3], 3); + ASSERT_EQ(transitionMatrix.getRowGroupIndices()[4], 4); + ASSERT_EQ(transitionMatrix.getRowGroupIndices()[5], 6); + ASSERT_EQ(transitionMatrix.getRowGroupIndices()[6], 7); // Test the Markovian states. ASSERT_TRUE(result.markovianStates.get(0)); @@ -119,22 +120,23 @@ TEST(MarkovAutomatonSparseTransitionParserTest, Whitespaces) { ASSERT_EQ(transitionMatrix.getColumnCount(), STATE_COUNT); ASSERT_EQ(transitionMatrix.getRowCount(), CHOICE_COUNT); ASSERT_EQ(transitionMatrix.getEntryCount(), 12); + ASSERT_EQ(transitionMatrix.getRowGroupCount(), 6); + ASSERT_EQ(transitionMatrix.getRowGroupIndices().size(), 7); ASSERT_EQ(result.markovianChoices.size(), CHOICE_COUNT); ASSERT_EQ(result.markovianStates.size(), STATE_COUNT); ASSERT_EQ(result.markovianStates.getNumberOfSetBits(), 2); ASSERT_EQ(result.exitRates.size(), STATE_COUNT); - ASSERT_EQ(result.nondeterministicChoiceIndices.size(), 7); // Test the general structure of the transition system (that will be an Markov automaton). // Test the mapping between states and transition matrix rows. - ASSERT_EQ(result.nondeterministicChoiceIndices[0], 0); - ASSERT_EQ(result.nondeterministicChoiceIndices[1], 1); - ASSERT_EQ(result.nondeterministicChoiceIndices[2], 2); - ASSERT_EQ(result.nondeterministicChoiceIndices[3], 3); - ASSERT_EQ(result.nondeterministicChoiceIndices[4], 4); - ASSERT_EQ(result.nondeterministicChoiceIndices[5], 6); - ASSERT_EQ(result.nondeterministicChoiceIndices[6], 7); + ASSERT_EQ(transitionMatrix.getRowGroupIndices()[0], 0); + ASSERT_EQ(transitionMatrix.getRowGroupIndices()[1], 1); + ASSERT_EQ(transitionMatrix.getRowGroupIndices()[2], 2); + ASSERT_EQ(transitionMatrix.getRowGroupIndices()[3], 3); + ASSERT_EQ(transitionMatrix.getRowGroupIndices()[4], 4); + ASSERT_EQ(transitionMatrix.getRowGroupIndices()[5], 6); + ASSERT_EQ(transitionMatrix.getRowGroupIndices()[6], 7); // Test the Markovian states. ASSERT_TRUE(result.markovianStates.get(0)); @@ -193,11 +195,12 @@ TEST(MarkovAutomatonSparseTransitionParserTest, FixDeadlocks) { storm::storage::SparseMatrix resultMatrix(result.transitionMatrixBuilder.build(0,0)); ASSERT_EQ(resultMatrix.getColumnCount(), STATE_COUNT + 1); ASSERT_EQ(resultMatrix.getEntryCount(), 13); + ASSERT_EQ(resultMatrix.getRowGroupCount(), 7); + ASSERT_EQ(resultMatrix.getRowGroupIndices().size(), 8); ASSERT_EQ(result.markovianChoices.size(), CHOICE_COUNT +1); ASSERT_EQ(result.markovianStates.size(), STATE_COUNT +1); ASSERT_EQ(result.markovianStates.getNumberOfSetBits(), 2); ASSERT_EQ(result.exitRates.size(), STATE_COUNT + 1); - ASSERT_EQ(result.nondeterministicChoiceIndices.size(), 8); } TEST(MarkovAutomatonSparseTransitionParserTest, DontFixDeadlocks) { diff --git a/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp b/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp index 8fc55cf1c..554d689ea 100644 --- a/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp +++ b/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp @@ -19,7 +19,7 @@ TEST(NondeterministicSparseTransitionParserTest, NonExistingFile) { // No matter what happens, please do NOT create a file with the name "nonExistingFile.not"! ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException); - storm::parser::NondeterministicSparseTransitionParser::Result nullInformation; + storm::storage::SparseMatrix nullInformation; ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not", nullInformation), storm::exceptions::FileIoException); } @@ -27,25 +27,26 @@ TEST(NondeterministicSparseTransitionParserTest, NonExistingFile) { TEST(NondeterministicSparseTransitionParserTest, BasicTransitionsParsing) { // Parse a nondeterministic transitions file and test the result. - storm::parser::NondeterministicSparseTransitionParser::Result result(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general.tra")); + storm::storage::SparseMatrix result(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general.tra")); // Test the row mapping, i.e. at which row which state starts. - ASSERT_EQ(result.rowMapping.size(), 7); - ASSERT_EQ(result.rowMapping[0], 0); - ASSERT_EQ(result.rowMapping[1], 4); - ASSERT_EQ(result.rowMapping[2], 5); - ASSERT_EQ(result.rowMapping[3], 7); - ASSERT_EQ(result.rowMapping[4], 8); - ASSERT_EQ(result.rowMapping[5], 9); - ASSERT_EQ(result.rowMapping[6], 11); + ASSERT_EQ(6, result.getRowGroupCount()); + ASSERT_EQ(7, result.getRowGroupIndices().size()); + ASSERT_EQ(result.getRowGroupIndices()[0], 0); + ASSERT_EQ(result.getRowGroupIndices()[1], 4); + ASSERT_EQ(result.getRowGroupIndices()[2], 5); + ASSERT_EQ(result.getRowGroupIndices()[3], 7); + ASSERT_EQ(result.getRowGroupIndices()[4], 8); + ASSERT_EQ(result.getRowGroupIndices()[5], 9); + ASSERT_EQ(result.getRowGroupIndices()[6], 11); // Test the transition matrix. - ASSERT_EQ(result.transitionMatrix.getColumnCount(), 6); - ASSERT_EQ(result.transitionMatrix.getRowCount(), 11); - ASSERT_EQ(result.transitionMatrix.getEntryCount(), 22); + ASSERT_EQ(result.getColumnCount(), 6); + ASSERT_EQ(result.getRowCount(), 11); + ASSERT_EQ(result.getEntryCount(), 22); // Test every entry of the matrix. - storm::storage::SparseMatrix::const_iterator cIter = result.transitionMatrix.begin(0); + storm::storage::SparseMatrix::const_iterator cIter = result.begin(0); ASSERT_EQ(cIter->first, 0); ASSERT_EQ(cIter->second, 0.9); @@ -116,8 +117,8 @@ TEST(NondeterministicSparseTransitionParserTest, BasicTransitionsParsing) { TEST(NondeterministicSparseTransitionParserTest, BasicTransitionsRewardsParsing) { // Parse a nondeterministic transitions file and test the result. - storm::parser::NondeterministicSparseTransitionParser::Result modelInformation(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general.tra")); - storm::storage::SparseMatrix result(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_general.trans.rew", modelInformation).transitionMatrix); + storm::storage::SparseMatrix modelInformation(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general.tra")); + storm::storage::SparseMatrix result(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_general.trans.rew", modelInformation)); // Test the transition matrix. ASSERT_EQ(result.getColumnCount(), 6); @@ -182,17 +183,17 @@ TEST(NondeterministicSparseTransitionParserTest, BasicTransitionsRewardsParsing) TEST(NondeterministicSparseTransitionParserTest, Whitespaces) { // Test the resilience of the parser against whitespaces. // Do so by comparing the hashes of the transition matices and the rowMapping vectors element by element. - storm::parser::NondeterministicSparseTransitionParser::Result correctResult(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general.tra")); - storm::parser::NondeterministicSparseTransitionParser::Result whitespaceResult = storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_whitespaces.tra"); - ASSERT_EQ(correctResult.transitionMatrix.hash(), whitespaceResult.transitionMatrix.hash()); - ASSERT_EQ(correctResult.rowMapping.size(), whitespaceResult.rowMapping.size()); - for(uint_fast64_t i = 0; i < correctResult.rowMapping.size(); i++) { - ASSERT_EQ(correctResult.rowMapping[i], whitespaceResult.rowMapping[i]); + storm::storage::SparseMatrix correctResult(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general.tra")); + storm::storage::SparseMatrix whitespaceResult = storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_whitespaces.tra"); + ASSERT_EQ(correctResult.hash(), whitespaceResult.hash()); + ASSERT_EQ(correctResult.getRowGroupIndices().size(), whitespaceResult.getRowGroupIndices().size()); + for(uint_fast64_t i = 0; i < correctResult.getRowGroupIndices().size(); i++) { + ASSERT_EQ(correctResult.getRowGroupIndices()[i], whitespaceResult.getRowGroupIndices()[i]); } // Do the same (minus the unused rowMapping) for the corresponding transition rewards file (with and without whitespaces) - uint_fast64_t correctHash = storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_general.trans.rew", correctResult).transitionMatrix.hash(); - ASSERT_EQ(correctHash, storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_whitespaces.trans.rew", whitespaceResult).transitionMatrix.hash()); + uint_fast64_t correctHash = storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_general.trans.rew", correctResult).hash(); + ASSERT_EQ(correctHash, storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_whitespaces.trans.rew", whitespaceResult).hash()); } TEST(NondeterministicSparseTransitionParserTest, MixedTransitionOrder) { @@ -200,7 +201,7 @@ TEST(NondeterministicSparseTransitionParserTest, MixedTransitionOrder) { ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_mixedTransitionOrder.tra"), storm::exceptions::InvalidArgumentException); ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_mixedStateOrder.tra"), storm::exceptions::InvalidArgumentException); - storm::parser::NondeterministicSparseTransitionParser::Result modelInformation = storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general.tra"); + storm::storage::SparseMatrix modelInformation = storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general.tra"); ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_mixedTransitionOrder.trans.rew", modelInformation), storm::exceptions::InvalidArgumentException); ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_mixedStateOrder.trans.rew", modelInformation), storm::exceptions::InvalidArgumentException); } @@ -210,18 +211,18 @@ TEST(NondeterministicSparseTransitionParserTest, FixDeadlocks) { storm::settings::InternalOptionMemento setDeadlockOption("fixDeadlocks", true); // Parse a transitions file with the fixDeadlocks Flag set and test if it works. - storm::parser::NondeterministicSparseTransitionParser::Result result(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_deadlock.tra")); + storm::storage::SparseMatrix result(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_deadlock.tra")); - ASSERT_EQ(result.rowMapping.size(), 8); - ASSERT_EQ(result.rowMapping[5], 9); - ASSERT_EQ(result.rowMapping[6], 10); - ASSERT_EQ(result.rowMapping[7], 12); + ASSERT_EQ(result.getRowGroupIndices().size(), 8); + ASSERT_EQ(result.getRowGroupIndices()[5], 9); + ASSERT_EQ(result.getRowGroupIndices()[6], 10); + ASSERT_EQ(result.getRowGroupIndices()[7], 12); - ASSERT_EQ(result.transitionMatrix.getColumnCount(), 7); - ASSERT_EQ(result.transitionMatrix.getRowCount(), 12); - ASSERT_EQ(result.transitionMatrix.getEntryCount(), 23); + ASSERT_EQ(result.getColumnCount(), 7); + ASSERT_EQ(result.getRowCount(), 12); + ASSERT_EQ(result.getEntryCount(), 23); - storm::storage::SparseMatrix::const_iterator cIter = result.transitionMatrix.begin(8); + storm::storage::SparseMatrix::const_iterator cIter = result.begin(8); ASSERT_EQ(cIter->first, 1); ASSERT_EQ(cIter->second, 0.7); @@ -261,7 +262,7 @@ TEST(NondeterministicSparseTransitionParserTest, DoubledLines) { TEST(NondeterministicSparseTransitionParserTest, RewardForNonExistentTransition) { // First parse a transition file. Then parse a transition reward file for the resulting transition matrix. - storm::parser::NondeterministicSparseTransitionParser::Result transitionResult = storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general.tra"); + storm::storage::SparseMatrix transitionResult = storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general.tra"); // There is a reward for a transition that does not exist in the transition matrix. ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_rewardForNonExTrans.trans.rew", transitionResult), storm::exceptions::WrongFormatException);