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

Changed parsers to be compilable again. 

- Mostly effects of the SparseMatrix redesign.
- Plus some missing includes.


Former-commit-id: 11c5bc9970
tempestpy_adaptions
masawei 11 years ago
parent
8e5847ae19
commit
4245b3c4e3
8 changed files with 109 additions and 75 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      src/parser/DeterministicModelParser.cpp
  2. 44
      src/parser/DeterministicSparseTransitionParser.cpp
  3. 4
      src/parser/LtlFileParser.cpp
  4. 13
      src/parser/MarkovAutomatonParser.cpp
  5. 7
      src/parser/MarkovAutomatonSparseTransitionParser.cpp
  6. 5
      src/parser/MarkovAutomatonSparseTransitionParser.h
  7. 1
      src/parser/PrctlFileParser.cpp
  8. 106
      test/functional/parser/MarkovAutomatonParserTest.cpp

4
src/parser/DeterministicModelParser.cpp
View File

@ -59,7 +59,7 @@ DeterministicModelParser::ResultContainer DeterministicModelParser::parseDetermi
storm::models::Dtmc<double> DeterministicModelParser::parseDtmc(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) {
DeterministicModelParser::ResultContainer parserResult(std::move(parseDeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)));
return storm::models::Dtmc<double>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>>());
return storm::models::Dtmc<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>>>());
}
/*!
@ -70,7 +70,7 @@ storm::models::Dtmc<double> DeterministicModelParser::parseDtmc(std::string cons
storm::models::Ctmc<double> DeterministicModelParser::parseCtmc(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) {
DeterministicModelParser::ResultContainer parserResult(std::move(parseDeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)));
return storm::models::Ctmc<double>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>>());
return storm::models::Ctmc<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 */

44
src/parser/DeterministicSparseTransitionParser.cpp
View File

@ -14,6 +14,8 @@
#include <iostream>
#include <string>
#include "src/utility/constants.h"
#include "src/exceptions/FileIoException.h"
#include "src/exceptions/WrongFormatException.h"
#include "src/settings/Settings.h"
@ -150,15 +152,11 @@ storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser::parseD
buf = storm::parser::forwardToNextLine(buf, lineEndings);
}
// Creating matrix here.
// Creating matrix builder here.
// The number of non-zero elements is computed by firstPass().
LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << (firstPass.highestStateIndex+1) << " x " << (firstPass.highestStateIndex+1) << ".");
storm::storage::SparseMatrix<double> resultMatrix(firstPass.highestStateIndex + 1);
resultMatrix.initialize(firstPass.numberOfNonzeroEntries);
if (!resultMatrix.isInitialized()) {
LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << (firstPass.highestStateIndex+1) << " x " << (firstPass.highestStateIndex+1) << ".");
throw std::bad_alloc();
}
// The contents are inserted during the readout of the file, below.
// The actual matrix will be build once all contents are inserted.
storm::storage::SparseMatrixBuilder<double> resultMatrix(firstPass.highestStateIndex + 1, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries);
uint_fast64_t row, col, lastRow = 0;
double val;
@ -189,7 +187,7 @@ storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser::parseD
if (lastRow != row) {
if (!rowHadDiagonalEntry) {
if (insertDiagonalEntriesIfMissing) {
resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constGetZero<double>());
resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constantZero<double>());
LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (1)");
} else {
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself.");
@ -200,7 +198,7 @@ storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser::parseD
for (uint_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) {
hadDeadlocks = true;
if (fixDeadlocks) {
resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::constGetOne<double>());
resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::constantOne<double>());
rowHadDiagonalEntry = true;
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions. A self-loop was inserted.");
} else {
@ -218,7 +216,7 @@ storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser::parseD
if (col > row && !rowHadDiagonalEntry) {
if (insertDiagonalEntriesIfMissing) {
resultMatrix.addNextValue(row, row, storm::utility::constGetZero<double>());
resultMatrix.addNextValue(row, row, storm::utility::constantZero<double>());
LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << row << " has no transition to itself. Inserted a 0-transition. (2)");
} else {
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << row << " has no transition to itself.");
@ -232,7 +230,7 @@ storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser::parseD
if (!rowHadDiagonalEntry) {
if (insertDiagonalEntriesIfMissing) {
resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constGetZero<double>());
resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constantZero<double>());
LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (3)");
} else {
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself.");
@ -242,10 +240,7 @@ storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser::parseD
// If we encountered deadlock and did not fix them, now is the time to throw the exception.
if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFormatException() << "Some of the nodes had deadlocks. You can use --fixDeadlocks to insert self-loops on the fly.";
// Finalize Matrix.
resultMatrix.finalize();
return resultMatrix;
return resultMatrix.build();
}
/*!
@ -302,15 +297,11 @@ storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser::parseD
}
// Creating matrix here.
// Creating matrix builder here.
// The number of non-zero elements is computed by firstPass().
LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << (firstPass.highestStateIndex+1) << " x " << (firstPass.highestStateIndex+1) << ".");
storm::storage::SparseMatrix<double> resultMatrix(firstPass.highestStateIndex + 1);
resultMatrix.initialize(firstPass.numberOfNonzeroEntries);
if (!resultMatrix.isInitialized()) {
LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << (firstPass.highestStateIndex+1) << " x " << (firstPass.highestStateIndex+1) << ".");
throw std::bad_alloc();
}
// The contents are inserted during the readout of the file, below.
// The actual matrix will be build once all contents are inserted.
storm::storage::SparseMatrixBuilder<double> resultMatrix(firstPass.highestStateIndex + 1, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries);
uint_fast64_t row, col;
double val;
@ -329,10 +320,7 @@ storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser::parseD
buf = trimWhitespaces(buf);
}
// Finalize Matrix.
resultMatrix.finalize();
return resultMatrix;
return resultMatrix.build();
}
} // namespace parser

4
src/parser/LtlFileParser.cpp
View File

@ -5,9 +5,13 @@
* Author: thomas
*/
#include <fstream>
#include "LtlFileParser.h"
#include "LtlParser.h"
#include "src/exceptions/FileIoException.h"
namespace storm {
namespace parser {

13
src/parser/MarkovAutomatonParser.cpp
View File

@ -8,12 +8,19 @@ namespace storm {
namespace parser {
storm::models::MarkovAutomaton<double> MarkovAutomatonParser::parseMarkovAutomaton(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename, std::string const& transitionRewardFilename) {
// Parse the transitions of the Markov Automaton.
storm::parser::MarkovAutomatonSparseTransitionParser::ResultType transitionResult(storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(transitionsFilename));
storm::models::AtomicPropositionsLabeling resultLabeling(storm::parser::AtomicPropositionLabelingParser(transitionResult.transitionMatrix.getColumnCount(), labelingFilename));
// Build the actual transition matrix using the MatrixBuilder provided by the transitionResult.
storm::storage::SparseMatrix<double> transitionMatrix(transitionResult.transitionMatrixBuilder.build(0,0));
// Parse the state labeling.
storm::models::AtomicPropositionsLabeling resultLabeling(storm::parser::AtomicPropositionLabelingParser(transitionMatrix.getColumnCount(), labelingFilename));
boost::optional<std::vector<double>> stateRewards;
if (stateRewardFilename != "") {
stateRewards.reset(storm::parser::SparseStateRewardParser::parseSparseStateReward(transitionResult.transitionMatrix.getColumnCount(), stateRewardFilename));
stateRewards.reset(storm::parser::SparseStateRewardParser::parseSparseStateReward(transitionMatrix.getColumnCount(), stateRewardFilename));
}
if (transitionRewardFilename != "") {
@ -21,7 +28,7 @@ storm::models::MarkovAutomaton<double> MarkovAutomatonParser::parseMarkovAutomat
throw storm::exceptions::WrongFormatException() << "Transition rewards are unsupported for Markov automata.";
}
storm::models::MarkovAutomaton<double> resultingAutomaton(std::move(transitionResult.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<storm::storage::VectorSet<uint_fast64_t>>>());
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>>>());
return resultingAutomaton;
}

7
src/parser/MarkovAutomatonSparseTransitionParser.cpp
View File

@ -164,7 +164,7 @@ MarkovAutomatonSparseTransitionParser::ResultType MarkovAutomatonSparseTransitio
if (fixDeadlocks) {
for (uint_fast64_t index = lastsource + 1; index < source; ++index) {
result.nondeterministicChoiceIndices[index] = currentChoice;
result.transitionMatrix.addNextValue(currentChoice, index, 1);
result.transitionMatrixBuilder.addNextValue(currentChoice, index, 1);
++currentChoice;
}
} else {
@ -220,7 +220,7 @@ MarkovAutomatonSparseTransitionParser::ResultType MarkovAutomatonSparseTransitio
double val = checked_strtod(buf, &buf);
// Record the value as well as the exit rate in case of a Markovian choice.
result.transitionMatrix.addNextValue(currentChoice, target, val);
result.transitionMatrixBuilder.addNextValue(currentChoice, target, val);
if (isMarkovianChoice) {
result.exitRates[source] += val;
}
@ -236,9 +236,6 @@ MarkovAutomatonSparseTransitionParser::ResultType MarkovAutomatonSparseTransitio
++currentChoice;
}
// As we have added all entries at this point, we need to finalize the matrix.
result.transitionMatrix.finalize();
// Put a sentinel element at the end.
result.nondeterministicChoiceIndices[firstPassResult.highestStateIndex + 1] = currentChoice;

5
src/parser/MarkovAutomatonSparseTransitionParser.h
View File

@ -44,13 +44,12 @@ public:
* Creates a new instance of the struct using the result of the first pass to correctly initialize the container.
* @param firstPassResult A reference to the result of the first pass.
*/
ResultType(FirstPassResult const& firstPassResult) : transitionMatrix(firstPassResult.numberOfChoices, firstPassResult.highestStateIndex + 1), nondeterministicChoiceIndices(firstPassResult.highestStateIndex + 2), markovianChoices(firstPassResult.numberOfChoices), markovianStates(firstPassResult.highestStateIndex + 1), exitRates(firstPassResult.highestStateIndex + 1) {
transitionMatrix.initialize(firstPassResult.numberOfNonzeroEntries);
ResultType(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) {
// Intentionally left empty.
}
// A matrix representing the transitions of the model.
storm::storage::SparseMatrix<double> transitionMatrix;
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;

1
src/parser/PrctlFileParser.cpp
View File

@ -9,6 +9,7 @@
#include "PrctlFileParser.h"
#include "PrctlParser.h"
#include "src/exceptions/FileIoException.h"
namespace storm {
namespace parser {

106
test/functional/parser/MarkovAutomatonParserTest.cpp
View File

@ -25,14 +25,18 @@ TEST(MarkovAutomatonSparseTransitionParserTest, BasicParseTest) {
// The file that will be used for the test.
std::string filename = STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_general_input_01.tra";
// Execute the parser.
storm::parser::MarkovAutomatonSparseTransitionParser::ResultType result = storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(filename);
// Build the actual transition matrix.
storm::storage::SparseMatrix<double> transitionMatrix(result.transitionMatrixBuilder.build(0,0));
// Test all sizes and counts.
ASSERT_EQ(result.transitionMatrix.getColumnCount(), STATE_COUNT);
ASSERT_EQ(result.transitionMatrix.getRowCount(), CHOICE_COUNT);
ASSERT_EQ(result.transitionMatrix.getNonZeroEntryCount(), 12);
ASSERT_EQ(result.markovianChoices.getSize(), CHOICE_COUNT);
ASSERT_EQ(result.markovianStates.getSize(), STATE_COUNT);
ASSERT_EQ(transitionMatrix.getColumnCount(), STATE_COUNT);
ASSERT_EQ(transitionMatrix.getRowCount(), CHOICE_COUNT);
ASSERT_EQ(transitionMatrix.getEntryCount(), 12);
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);
@ -65,32 +69,51 @@ TEST(MarkovAutomatonSparseTransitionParserTest, BasicParseTest) {
ASSERT_EQ(result.exitRates[5], 0);
// Finally, test the transition matrix itself.
ASSERT_EQ(result.transitionMatrix.getValue(0,1), 2);
ASSERT_EQ(result.transitionMatrix.getValue(1,2), 1);
ASSERT_EQ(result.transitionMatrix.getValue(2,0), 1);
ASSERT_EQ(result.transitionMatrix.getValue(2,1), 2);
ASSERT_EQ(result.transitionMatrix.getValue(2,3), 4);
ASSERT_EQ(result.transitionMatrix.getValue(2,4), 8);
ASSERT_EQ(result.transitionMatrix.getValue(3,2), 0.5);
ASSERT_EQ(result.transitionMatrix.getValue(3,3), 0.5);
ASSERT_EQ(result.transitionMatrix.getValue(4,3), 1);
ASSERT_EQ(result.transitionMatrix.getValue(5,1), 0.5);
ASSERT_EQ(result.transitionMatrix.getValue(5,5), 0.5);
ASSERT_EQ(result.transitionMatrix.getValue(6,5), 1);
storm::storage::SparseMatrix<double>::const_iterator cIter = transitionMatrix.begin(0);
ASSERT_EQ(cIter->second, 2);
cIter++;
ASSERT_EQ(cIter->second, 1);
cIter++;
ASSERT_EQ(cIter->second, 1);
cIter++;
ASSERT_EQ(cIter->second, 2);
cIter++;
ASSERT_EQ(cIter->second, 4);
cIter++;
ASSERT_EQ(cIter->second, 8);
cIter++;
ASSERT_EQ(cIter->second, 0.5);
cIter++;
ASSERT_EQ(cIter->second, 0.5);
cIter++;
ASSERT_EQ(cIter->second, 1);
cIter++;
ASSERT_EQ(cIter->second, 0.5);
cIter++;
ASSERT_EQ(cIter->second, 0.5);
cIter++;
ASSERT_EQ(cIter->second, 1);
cIter++;
ASSERT_EQ(transitionMatrix.end(), cIter);
}
TEST(MarkovAutomatonSparseTransitionParserTest, WhiteSpaceTest) {
// The file that will be used for the test.
std::string filename = STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_whitespace_input_01.tra";
// Execute the parser.
storm::parser::MarkovAutomatonSparseTransitionParser::ResultType result = storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(filename);
// Build the actual transition matrix.
storm::storage::SparseMatrix<double> transitionMatrix(result.transitionMatrixBuilder.build(0,0));
// Test all sizes and counts.
ASSERT_EQ(result.transitionMatrix.getColumnCount(), STATE_COUNT);
ASSERT_EQ(result.transitionMatrix.getRowCount(), CHOICE_COUNT);
ASSERT_EQ(result.transitionMatrix.getNonZeroEntryCount(), 12);
ASSERT_EQ(result.markovianChoices.getSize(), CHOICE_COUNT);
ASSERT_EQ(result.markovianStates.getSize(), STATE_COUNT);
ASSERT_EQ(transitionMatrix.getColumnCount(), STATE_COUNT);
ASSERT_EQ(transitionMatrix.getRowCount(), CHOICE_COUNT);
ASSERT_EQ(transitionMatrix.getEntryCount(), 12);
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);
@ -123,18 +146,33 @@ TEST(MarkovAutomatonSparseTransitionParserTest, WhiteSpaceTest) {
ASSERT_EQ(result.exitRates[5], 0);
// Finally, test the transition matrix itself.
ASSERT_EQ(result.transitionMatrix.getValue(0,1), 2);
ASSERT_EQ(result.transitionMatrix.getValue(1,2), 1);
ASSERT_EQ(result.transitionMatrix.getValue(2,0), 1);
ASSERT_EQ(result.transitionMatrix.getValue(2,1), 2);
ASSERT_EQ(result.transitionMatrix.getValue(2,3), 4);
ASSERT_EQ(result.transitionMatrix.getValue(2,4), 8);
ASSERT_EQ(result.transitionMatrix.getValue(3,2), 0.5);
ASSERT_EQ(result.transitionMatrix.getValue(3,3), 0.5);
ASSERT_EQ(result.transitionMatrix.getValue(4,3), 1);
ASSERT_EQ(result.transitionMatrix.getValue(5,1), 0.5);
ASSERT_EQ(result.transitionMatrix.getValue(5,5), 0.5);
ASSERT_EQ(result.transitionMatrix.getValue(6,5), 1);
storm::storage::SparseMatrix<double>::const_iterator cIter = transitionMatrix.begin(0);
ASSERT_EQ(cIter->second, 2);
cIter++;
ASSERT_EQ(cIter->second, 1);
cIter++;
ASSERT_EQ(cIter->second, 1);
cIter++;
ASSERT_EQ(cIter->second, 2);
cIter++;
ASSERT_EQ(cIter->second, 4);
cIter++;
ASSERT_EQ(cIter->second, 8);
cIter++;
ASSERT_EQ(cIter->second, 0.5);
cIter++;
ASSERT_EQ(cIter->second, 0.5);
cIter++;
ASSERT_EQ(cIter->second, 1);
cIter++;
ASSERT_EQ(cIter->second, 0.5);
cIter++;
ASSERT_EQ(cIter->second, 0.5);
cIter++;
ASSERT_EQ(cIter->second, 1);
cIter++;
ASSERT_EQ(transitionMatrix.end(), cIter);
}
//TODO: Deadlock Test. I am quite sure that the deadlock state handling does not behave quite right.

Write Preview
Loading…
Cancel
Save