sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

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: 610c0282b2
main
masawei 11 years ago
parent
08168f5511
commit
28910462ec
11 changed files with 129 additions and 151 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      src/parser/AtomicPropositionLabelingParser.cpp
  2. 8
      src/parser/MarkovAutomatonParser.cpp
  3. 10
      src/parser/MarkovAutomatonSparseTransitionParser.cpp
  4. 5
      src/parser/MarkovAutomatonSparseTransitionParser.h
  5. 12
      src/parser/NondeterministicModelParser.cpp
  6. 12
      src/parser/NondeterministicModelParser.h
  7. 73
      src/parser/NondeterministicSparseTransitionParser.cpp
  8. 44
      src/parser/NondeterministicSparseTransitionParser.h
  9. 4
      src/parser/SparseStateRewardParser.cpp
  10. 37
      test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp
  11. 71
      test/functional/parser/NondeterministicSparseTransitionParserTest.cpp

4
src/parser/AtomicPropositionLabelingParser.cpp
View File

@ -126,7 +126,7 @@ namespace storm {
buf = trimWhitespaces(buf); buf = trimWhitespaces(buf);
uint_fast64_t state = 0; uint_fast64_t state = 0;
uint_fast64_t lastState = -1;
uint_fast64_t lastState = (uint_fast64_t)-1;
cnt = 0; cnt = 0;
// Now parse the assignments of labels to nodes. // Now parse the assignments of labels to nodes.
@ -137,7 +137,7 @@ namespace storm {
state = checked_strtol(buf, &buf); 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 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."); 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."; throw storm::exceptions::WrongFormatException() << "State " << state << " was found but has already been read or skipped previously.";
} }

8
src/parser/MarkovAutomatonParser.cpp
View File

@ -3,6 +3,10 @@
#include "SparseStateRewardParser.h" #include "SparseStateRewardParser.h"
#include "src/exceptions/WrongFormatException.h" #include "src/exceptions/WrongFormatException.h"
#include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h"
extern log4cplus::Logger logger;
namespace storm { namespace storm {
namespace parser { namespace parser {
@ -12,7 +16,7 @@ namespace storm {
storm::parser::MarkovAutomatonSparseTransitionParser::Result transitionResult(storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(transitionsFilename)); storm::parser::MarkovAutomatonSparseTransitionParser::Result transitionResult(storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(transitionsFilename));
// Build the actual transition matrix using the MatrixBuilder provided by the transitionResult. // Build the actual transition matrix using the MatrixBuilder provided by the transitionResult.
storm::storage::SparseMatrix<double> transitionMatrix(transitionResult.transitionMatrixBuilder.build(0,0));
storm::storage::SparseMatrix<double> transitionMatrix(transitionResult.transitionMatrixBuilder.build());
// Parse the state labeling. // Parse the state labeling.
storm::models::AtomicPropositionsLabeling resultLabeling(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(transitionMatrix.getColumnCount(), labelingFilename)); 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. // Put the pieces together to generate the Markov Automaton.
storm::models::MarkovAutomaton<double> resultingAutomaton(std::move(transitionMatrix), std::move(resultLabeling), std::move(transitionResult.nondeterministicChoiceIndices), std::move(transitionResult.markovianStates), std::move(transitionResult.exitRates), std::move(stateRewards), boost::optional<storm::storage::SparseMatrix<double>>(), boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
storm::models::MarkovAutomaton<double> resultingAutomaton(std::move(transitionMatrix), std::move(resultLabeling), std::move(transitionResult.markovianStates), std::move(transitionResult.exitRates), std::move(stateRewards), boost::optional<storm::storage::SparseMatrix<double>>(), boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
return resultingAutomaton; return resultingAutomaton;
} }

10
src/parser/MarkovAutomatonSparseTransitionParser.cpp
View File

@ -170,6 +170,10 @@ namespace storm {
uint_fast64_t lastsource = 0; uint_fast64_t lastsource = 0;
bool encounteredEOF = false; bool encounteredEOF = false;
uint_fast64_t currentChoice = 0; 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) { while (buf[0] != '\0' && !encounteredEOF) {
// At the current point, the next thing to read is the source state of the next choice to come. // At the current point, the next thing to read is the source state of the next choice to come.
source = checked_strtol(buf, &buf); source = checked_strtol(buf, &buf);
@ -178,7 +182,7 @@ namespace storm {
if (source > lastsource + 1) { if (source > lastsource + 1) {
if (fixDeadlocks) { if (fixDeadlocks) {
for (uint_fast64_t index = lastsource + 1; index < source; ++index) { for (uint_fast64_t index = lastsource + 1; index < source; ++index) {
result.nondeterministicChoiceIndices[index] = currentChoice;
result.transitionMatrixBuilder.newRowGroup(currentChoice);
result.transitionMatrixBuilder.addNextValue(currentChoice, index, 1); result.transitionMatrixBuilder.addNextValue(currentChoice, index, 1);
++currentChoice; ++currentChoice;
} }
@ -190,7 +194,7 @@ namespace storm {
if (source != lastsource) { if (source != lastsource) {
// If we skipped to a new state we need to record the beginning of the choices in the nondeterministic choice indices. // 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. // Record that the current source was the last source.
@ -253,7 +257,7 @@ namespace storm {
} }
// Put a sentinel element at the end. // Put a sentinel element at the end.
result.nondeterministicChoiceIndices[firstPassResult.highestStateIndex + 1] = currentChoice;
result.transitionMatrixBuilder.newRowGroup(currentChoice);
return result; return result;
} }

5
src/parser/MarkovAutomatonSparseTransitionParser.h
View File

@ -52,16 +52,13 @@ namespace storm {
* *
* @param firstPassResult A reference to the result of the first pass. * @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. // Intentionally left empty.
} }
//! A matrix representing the transitions of the model. //! A matrix representing the transitions of the model.
storm::storage::SparseMatrixBuilder<double> transitionMatrixBuilder; storm::storage::SparseMatrixBuilder<double> transitionMatrixBuilder;
//! 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. //! A bit vector indicating which choices are Markovian. By duality, all other choices are probabilitic.
storm::storage::BitVector markovianChoices; storm::storage::BitVector markovianChoices;

12
src/parser/NondeterministicModelParser.cpp
View File

@ -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) { NondeterministicModelParser::Result NondeterministicModelParser::parseNondeterministicModel(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename, std::string const & transitionRewardFilename) {
// Parse the transitions. // Parse the transitions.
NondeterministicSparseTransitionParser::Result transitions(std::move(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(transitionsFilename)));
storm::storage::SparseMatrix<double> 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. // Parse the state labeling.
storm::models::AtomicPropositionsLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFilename))); 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. // Only parse transition rewards if a file is given.
boost::optional<storm::storage::SparseMatrix<double>> transitionRewards; boost::optional<storm::storage::SparseMatrix<double>> transitionRewards;
if (transitionRewardFilename != "") { if (transitionRewardFilename != "") {
transitionRewards = storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(transitionRewardFilename, transitions).transitionMatrix;
transitionRewards = storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(transitionRewardFilename, transitions);
} }
// Construct the result. // 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.stateRewards = stateRewards;
result.transitionRewards = transitionRewards; result.transitionRewards = transitionRewards;
@ -50,13 +50,13 @@ namespace storm {
storm::models::Mdp<double> NondeterministicModelParser::parseMdp(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename, std::string const & transitionRewardFilename) { storm::models::Mdp<double> 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); Result parserResult = parseNondeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename);
return storm::models::Mdp<double>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
return storm::models::Mdp<double>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
} }
storm::models::Ctmdp<double> NondeterministicModelParser::parseCtmdp(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename, std::string const & transitionRewardFilename) { storm::models::Ctmdp<double> 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); Result parserResult = parseNondeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename);
return storm::models::Ctmdp<double>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
return storm::models::Ctmdp<double>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
} }
} /* namespace parser */ } /* namespace parser */

12
src/parser/NondeterministicModelParser.h
View File

@ -33,10 +33,9 @@ namespace storm {
* The copy constructor. * The copy constructor.
* *
* @param transitionSystem The transition system to be contained in the Result. * @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. * @param labeling The the labeling of the transition system to be contained in the Result.
*/ */
Result(storm::storage::SparseMatrix<double>& transitionSystem, std::vector<uint_fast64_t>& rowMapping, storm::models::AtomicPropositionsLabeling& labeling) : transitionSystem(transitionSystem), labeling(labeling), rowMapping(rowMapping) {
Result(storm::storage::SparseMatrix<double>& transitionSystem, storm::models::AtomicPropositionsLabeling& labeling) : transitionSystem(transitionSystem), labeling(labeling) {
// Intentionally left empty. // Intentionally left empty.
} }
@ -44,10 +43,9 @@ namespace storm {
* The move constructor. * The move constructor.
* *
* @param transitionSystem The transition system to be contained in the Result. * @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. * @param labeling The the labeling of the transition system to be contained in the Result.
*/ */
Result(storm::storage::SparseMatrix<double>&& transitionSystem, std::vector<uint_fast64_t>&& rowMapping, storm::models::AtomicPropositionsLabeling&& labeling) : transitionSystem(std::move(transitionSystem)), labeling(std::move(labeling)), rowMapping(std::move(rowMapping)) {
Result(storm::storage::SparseMatrix<double>&& transitionSystem, storm::models::AtomicPropositionsLabeling&& labeling) : transitionSystem(std::move(transitionSystem)), labeling(std::move(labeling)) {
// Intentionally left empty. // Intentionally left empty.
} }
@ -61,12 +59,6 @@ namespace storm {
*/ */
storm::models::AtomicPropositionsLabeling labeling; 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<uint_fast64_t> rowMapping;
/*! /*!
* Optional rewards for each state. * Optional rewards for each state.
*/ */

73
src/parser/NondeterministicSparseTransitionParser.cpp
View File

@ -26,19 +26,19 @@ namespace storm {
using namespace storm::utility::cstring; using namespace storm::utility::cstring;
NondeterministicSparseTransitionParser::Result NondeterministicSparseTransitionParser::parseNondeterministicTransitions(std::string const& filename) {
storm::storage::SparseMatrix<double> NondeterministicSparseTransitionParser::parseNondeterministicTransitions(std::string const& filename) {
Result emptyResult;
storm::storage::SparseMatrix<double> 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<double> NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(std::string const& filename, storm::storage::SparseMatrix<double> const & modelInformation) {
return NondeterministicSparseTransitionParser::parse(filename, true, modelInformation); return NondeterministicSparseTransitionParser::parse(filename, true, modelInformation);
} }
NondeterministicSparseTransitionParser::Result NondeterministicSparseTransitionParser::parse(std::string const &filename, bool isRewardFile, Result const & modelInformation) {
storm::storage::SparseMatrix<double> NondeterministicSparseTransitionParser::parse(std::string const &filename, bool isRewardFile, storm::storage::SparseMatrix<double> const & modelInformation) {
// Enforce locale where decimal point is '.'. // Enforce locale where decimal point is '.'.
setlocale(LC_NUMERIC, "C"); setlocale(LC_NUMERIC, "C");
@ -72,17 +72,17 @@ namespace storm {
if (isRewardFile) { if (isRewardFile) {
// The reward matrix should match the size of the transition matrix. // 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."); LOG4CPLUS_ERROR(logger, "Reward matrix size exceeds transition matrix size.");
throw storm::exceptions::OutOfRangeException() << "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."); 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."; 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"); 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."; throw storm::exceptions::OutOfRangeException() << "The reward matrix has more entries than the transition matrix.";
} else { } 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. // 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. // 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."); LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << firstPass.choices << " x " << (firstPass.highestStateIndex+1) << " with " << firstPass.numberOfNonzeroEntries << " entries.");
storm::storage::SparseMatrixBuilder<double> matrixBuilder(firstPass.choices, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries);
// Create row mapping.
std::vector<uint_fast64_t> rowMapping(firstPass.highestStateIndex + 2, 0);
storm::storage::SparseMatrixBuilder<double> matrixBuilder;
if(!isRewardFile) {
matrixBuilder = storm::storage::SparseMatrixBuilder<double>(firstPass.choices, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries, true, firstPass.highestStateIndex + 1);
} else {
matrixBuilder = storm::storage::SparseMatrixBuilder<double>(firstPass.choices, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries, true, modelInformation.getRowGroupCount());
}
// Initialize variables for the parsing run. // Initialize variables for the parsing run.
uint_fast64_t source = 0, target = 0, lastSource = 0, choice = 0, lastChoice = 0, curRow = 0; 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 fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks");
bool hadDeadlocks = false; bool hadDeadlocks = false;
// The first state already starts a new row group of the matrix.
matrixBuilder.newRowGroup(0);
// Read all transitions from file. // Read all transitions from file.
while (buf[0] != '\0') { 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 // If we have switched the source state, we possibly need to insert the rows of the last
// source state. // source state.
if (source != lastSource) { 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 // If we skipped some states, we need to reserve empty rows for all their nondeterministic
// choices. // choices.
for (uint_fast64_t i = lastSource + 1; i < source; ++i) { 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 // 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++) { for (uint_fast64_t node = lastSource + 1; node < source; node++) {
hadDeadlocks = true; hadDeadlocks = true;
if (fixDeadlocks) { if (fixDeadlocks) {
rowMapping.at(node) = curRow;
matrixBuilder.newRowGroup(curRow);
matrixBuilder.addNextValue(curRow, node, 1); matrixBuilder.addNextValue(curRow, node, 1);
++curRow; ++curRow;
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted."); 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) { if (source != lastSource) {
// Add this source to rowMapping, if this is the first choice we encounter for this state. // 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); 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."; 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<double> resultMatrix = matrixBuilder.build(); storm::storage::SparseMatrix<double> 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. // 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."); 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."; 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<double> const & modelInformation) {
// Check file header and extract number of transitions. // Check file header and extract number of transitions.
@ -228,13 +241,13 @@ namespace storm {
// source state. // source state.
if (source != lastSource) { if (source != lastSource) {
// number of choices skipped = number of choices of last state - number of choices read // 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 // If we skipped some states, we need to reserve empty rows for all their nondeterministic
// choices. // choices.
for (uint_fast64_t i = lastSource + 1; i < source; ++i) { 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 // 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 (isRewardFile) {
// If not all rows were filled for the last state, we need to insert them. // 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 // If we skipped some states, we need to reserve empty rows for all their nondeterministic
// choices. // 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]);
} }
} }

44
src/parser/NondeterministicSparseTransitionParser.h
View File

@ -43,48 +43,12 @@ namespace storm {
uint_fast64_t choices; 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<double> transitionMatrix, std::vector<uint_fast64_t> rowMapping) : transitionMatrix(transitionMatrix), rowMapping(rowMapping) {
// Intentionally left empty.
}
/*!
* The matrix containing the parsed transition system.
*/
storm::storage::SparseMatrix<double> transitionMatrix;
/*!
* A mapping from rows of the matrix to states of the model.
* This resolves the nondeterministic choices inside the transition system.
*/
std::vector<uint_fast64_t> rowMapping;
};
/*! /*!
* Load a nondeterministic transition system from file and create a sparse adjacency matrix whose entries represent the weights of the edges * 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. * @param filename The path and name of file to be parsed.
*/ */
static Result parseNondeterministicTransitions(std::string const & filename);
static storm::storage::SparseMatrix<double> 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 * 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. * @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. * @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<double> parseNondeterministicTransitionRewards(std::string const & filename, storm::storage::SparseMatrix<double> const & modelInformation);
private: 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. * @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. * @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<double> const & modelInformation);
/*! /*!
* The main parsing routine. * 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. * @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. * @return A SparseMatrix containing the parsed file contents.
*/ */
static Result parse(std::string const& filename, bool isRewardFile, Result const & modelInformation);
static storm::storage::SparseMatrix<double> parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix<double> const & modelInformation);
}; };

4
src/parser/SparseStateRewardParser.cpp
View File

@ -36,7 +36,7 @@ namespace storm {
// Now parse state reward assignments. // Now parse state reward assignments.
uint_fast64_t state = 0; uint_fast64_t state = 0;
uint_fast64_t lastState = -1;
uint_fast64_t lastState = (uint_fast64_t)-1;
double reward; double reward;
// Iterate over states. // 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). // 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). // 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."); 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."; throw storm::exceptions::WrongFormatException() << "State " << state << " was found but has already been read or skipped previously.";
} }

37
test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp
View File

@ -42,22 +42,23 @@ TEST(MarkovAutomatonSparseTransitionParserTest, BasicParsing) {
ASSERT_EQ(transitionMatrix.getColumnCount(), STATE_COUNT); ASSERT_EQ(transitionMatrix.getColumnCount(), STATE_COUNT);
ASSERT_EQ(transitionMatrix.getRowCount(), CHOICE_COUNT); ASSERT_EQ(transitionMatrix.getRowCount(), CHOICE_COUNT);
ASSERT_EQ(transitionMatrix.getEntryCount(), 12); 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.markovianChoices.size(), CHOICE_COUNT);
ASSERT_EQ(result.markovianStates.size(), STATE_COUNT); ASSERT_EQ(result.markovianStates.size(), STATE_COUNT);
ASSERT_EQ(result.markovianStates.getNumberOfSetBits(), 2); ASSERT_EQ(result.markovianStates.getNumberOfSetBits(), 2);
ASSERT_EQ(result.exitRates.size(), STATE_COUNT); 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 general structure of the transition system (that will be an Markov automaton).
// Test the mapping between states and transition matrix rows. // 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. // Test the Markovian states.
ASSERT_TRUE(result.markovianStates.get(0)); ASSERT_TRUE(result.markovianStates.get(0));
@ -119,22 +120,23 @@ TEST(MarkovAutomatonSparseTransitionParserTest, Whitespaces) {
ASSERT_EQ(transitionMatrix.getColumnCount(), STATE_COUNT); ASSERT_EQ(transitionMatrix.getColumnCount(), STATE_COUNT);
ASSERT_EQ(transitionMatrix.getRowCount(), CHOICE_COUNT); ASSERT_EQ(transitionMatrix.getRowCount(), CHOICE_COUNT);
ASSERT_EQ(transitionMatrix.getEntryCount(), 12); 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.markovianChoices.size(), CHOICE_COUNT);
ASSERT_EQ(result.markovianStates.size(), STATE_COUNT); ASSERT_EQ(result.markovianStates.size(), STATE_COUNT);
ASSERT_EQ(result.markovianStates.getNumberOfSetBits(), 2); ASSERT_EQ(result.markovianStates.getNumberOfSetBits(), 2);
ASSERT_EQ(result.exitRates.size(), STATE_COUNT); 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 general structure of the transition system (that will be an Markov automaton).
// Test the mapping between states and transition matrix rows. // 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. // Test the Markovian states.
ASSERT_TRUE(result.markovianStates.get(0)); ASSERT_TRUE(result.markovianStates.get(0));
@ -193,11 +195,12 @@ TEST(MarkovAutomatonSparseTransitionParserTest, FixDeadlocks) {
storm::storage::SparseMatrix<double> resultMatrix(result.transitionMatrixBuilder.build(0,0)); storm::storage::SparseMatrix<double> resultMatrix(result.transitionMatrixBuilder.build(0,0));
ASSERT_EQ(resultMatrix.getColumnCount(), STATE_COUNT + 1); ASSERT_EQ(resultMatrix.getColumnCount(), STATE_COUNT + 1);
ASSERT_EQ(resultMatrix.getEntryCount(), 13); 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.markovianChoices.size(), CHOICE_COUNT +1);
ASSERT_EQ(result.markovianStates.size(), STATE_COUNT +1); ASSERT_EQ(result.markovianStates.size(), STATE_COUNT +1);
ASSERT_EQ(result.markovianStates.getNumberOfSetBits(), 2); ASSERT_EQ(result.markovianStates.getNumberOfSetBits(), 2);
ASSERT_EQ(result.exitRates.size(), STATE_COUNT + 1); ASSERT_EQ(result.exitRates.size(), STATE_COUNT + 1);
ASSERT_EQ(result.nondeterministicChoiceIndices.size(), 8);
} }
TEST(MarkovAutomatonSparseTransitionParserTest, DontFixDeadlocks) { TEST(MarkovAutomatonSparseTransitionParserTest, DontFixDeadlocks) {

71
test/functional/parser/NondeterministicSparseTransitionParserTest.cpp
View File

@ -19,7 +19,7 @@ TEST(NondeterministicSparseTransitionParserTest, NonExistingFile) {
// No matter what happens, please do NOT create a file with the name "nonExistingFile.not"! // 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); ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException);
storm::parser::NondeterministicSparseTransitionParser::Result nullInformation;
storm::storage::SparseMatrix<double> nullInformation;
ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not", nullInformation), storm::exceptions::FileIoException); 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) { TEST(NondeterministicSparseTransitionParserTest, BasicTransitionsParsing) {
// Parse a nondeterministic transitions file and test the result. // 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<double> 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. // 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. // 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. // Test every entry of the matrix.
storm::storage::SparseMatrix<double>::const_iterator cIter = result.transitionMatrix.begin(0);
storm::storage::SparseMatrix<double>::const_iterator cIter = result.begin(0);
ASSERT_EQ(cIter->first, 0); ASSERT_EQ(cIter->first, 0);
ASSERT_EQ(cIter->second, 0.9); ASSERT_EQ(cIter->second, 0.9);
@ -116,8 +117,8 @@ TEST(NondeterministicSparseTransitionParserTest, BasicTransitionsParsing) {
TEST(NondeterministicSparseTransitionParserTest, BasicTransitionsRewardsParsing) { TEST(NondeterministicSparseTransitionParserTest, BasicTransitionsRewardsParsing) {
// Parse a nondeterministic transitions file and test the result. // 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<double> result(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_general.trans.rew", modelInformation).transitionMatrix);
storm::storage::SparseMatrix<double> modelInformation(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general.tra"));
storm::storage::SparseMatrix<double> result(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_general.trans.rew", modelInformation));
// Test the transition matrix. // Test the transition matrix.
ASSERT_EQ(result.getColumnCount(), 6); ASSERT_EQ(result.getColumnCount(), 6);
@ -182,17 +183,17 @@ TEST(NondeterministicSparseTransitionParserTest, BasicTransitionsRewardsParsing)
TEST(NondeterministicSparseTransitionParserTest, Whitespaces) { TEST(NondeterministicSparseTransitionParserTest, Whitespaces) {
// Test the resilience of the parser against 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. // 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<double> correctResult(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general.tra"));
storm::storage::SparseMatrix<double> 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) // 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) { 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_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); 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<double> 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_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); 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); storm::settings::InternalOptionMemento setDeadlockOption("fixDeadlocks", true);
// Parse a transitions file with the fixDeadlocks Flag set and test if it works. // 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<double> 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<double>::const_iterator cIter = result.transitionMatrix.begin(8);
storm::storage::SparseMatrix<double>::const_iterator cIter = result.begin(8);
ASSERT_EQ(cIter->first, 1); ASSERT_EQ(cIter->first, 1);
ASSERT_EQ(cIter->second, 0.7); ASSERT_EQ(cIter->second, 0.7);
@ -261,7 +262,7 @@ TEST(NondeterministicSparseTransitionParserTest, DoubledLines) {
TEST(NondeterministicSparseTransitionParserTest, RewardForNonExistentTransition) { TEST(NondeterministicSparseTransitionParserTest, RewardForNonExistentTransition) {
// First parse a transition file. Then parse a transition reward file for the resulting transition matrix. // 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<double> 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. // 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); ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_rewardForNonExTrans.trans.rew", transitionResult), storm::exceptions::WrongFormatException);

Write Preview
Loading…
Cancel
Save