Browse Source

Finished initial remerge.

- Fixed comments.
- It seems to be ASSERT_EQ(expected, actual);
|-> Switched arguments of nearly all ASSERT_EQs to correctly use this macro in the parser tests.


Former-commit-id: e5059709f2
main
masawei 11 years ago
parent
commit
8f171c7dc5
  1. 3
      src/parser/MarkovAutomatonSparseTransitionParser.cpp
  2. 2
      src/parser/MarkovAutomatonSparseTransitionParser.h
  3. 7
      src/parser/NondeterministicSparseTransitionParser.cpp
  4. 38
      test/functional/parser/AutoParserTest.cpp
  5. 36
      test/functional/parser/DeterministicModelParserTest.cpp
  6. 180
      test/functional/parser/DeterministicSparseTransitionParserTest.cpp
  7. 4
      test/functional/parser/MappedFileTest.cpp
  8. 30
      test/functional/parser/MarkovAutomatonParserTest.cpp
  9. 156
      test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp
  10. 42
      test/functional/parser/NondeterministicModelParserTest.cpp
  11. 224
      test/functional/parser/NondeterministicSparseTransitionParserTest.cpp
  12. 4
      test/functional/parser/SparseStateRewardParserTest.cpp

3
src/parser/MarkovAutomatonSparseTransitionParser.cpp

@ -31,6 +31,7 @@ namespace storm {
bool stateHasMarkovianChoice = false;
bool stateHasProbabilisticChoice = false;
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);
@ -193,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.
// If we skipped to a new state we need to create a new row group for the choices of the new state.
result.transitionMatrixBuilder.newRowGroup(currentChoice);
}

2
src/parser/MarkovAutomatonSparseTransitionParser.h

@ -12,7 +12,7 @@ namespace storm {
*
* The file is parsed in two passes.
* The first pass tests the file format and collects statistical data needed for the second pass.
* The second pass then collects the actual file data and compiles it into a ResultType.
* The second pass then collects the actual file data and compiles it into a Result.
*/
class MarkovAutomatonSparseTransitionParser {
public:

7
src/parser/NondeterministicSparseTransitionParser.cpp

@ -139,9 +139,10 @@ namespace storm {
if ((source != lastSource || choice != lastChoice)) {
++curRow;
}
// Check if we have skipped any source node, i.e. if any node has no
// outgoing transitions. If so, insert a self-loop.
// Also add self-loops to rowMapping.
// Also begin a new rowGroup for the skipped state.
for (uint_fast64_t node = lastSource + 1; node < source; node++) {
hadDeadlocks = true;
if (fixDeadlocks) {
@ -154,7 +155,7 @@ namespace storm {
}
}
if (source != lastSource) {
// Add this source to rowMapping, if this is the first choice we encounter for this state.
// Add create a new rowGroup for the source, if this is the first choice we encounter for this state.
matrixBuilder.newRowGroup(curRow);
}
}
@ -187,7 +188,7 @@ namespace storm {
}
}
// Finally, build the actual matrix, test and return.
// Finally, build the actual matrix, test and return it.
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.

38
test/functional/parser/AutoParserTest.cpp

@ -22,10 +22,10 @@ TEST(AutoParserTest, BasicParsing) {
std::shared_ptr<storm::models::AbstractModel<double>> modelPtr = storm::parser::AutoParser::parseModel(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/autoParser/dtmc.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/autoParser.lab");
// Test if parsed correctly.
ASSERT_EQ(modelPtr->getType(), storm::models::DTMC);
ASSERT_EQ(modelPtr->getNumberOfStates(), 12);
ASSERT_EQ(modelPtr->getNumberOfTransitions(), 32);
ASSERT_EQ(modelPtr->getInitialStates().getNumberOfSetBits(), 1);
ASSERT_EQ(storm::models::DTMC, modelPtr->getType());
ASSERT_EQ(12, modelPtr->getNumberOfStates());
ASSERT_EQ(32, modelPtr->getNumberOfTransitions());
ASSERT_EQ(1, modelPtr->getInitialStates().getNumberOfSetBits());
ASSERT_TRUE(modelPtr->hasAtomicProposition("three"));
ASSERT_FALSE(modelPtr->hasStateRewards());
ASSERT_FALSE(modelPtr->hasTransitionRewards());
@ -54,23 +54,23 @@ TEST(AutoParserTest, Decision) {
// Dtmc
std::shared_ptr<storm::models::AbstractModel<double>> modelPtr = storm::parser::AutoParser::parseModel(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/autoParser/dtmc.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/autoParser.lab");
ASSERT_EQ(modelPtr->getType(), storm::models::DTMC);
ASSERT_EQ(modelPtr->getNumberOfStates(), 12);
ASSERT_EQ(modelPtr->getNumberOfTransitions(), 32);
ASSERT_EQ(storm::models::DTMC, modelPtr->getType());
ASSERT_EQ(12, modelPtr->getNumberOfStates());
ASSERT_EQ(32, modelPtr->getNumberOfTransitions());
// Ctmc
modelPtr.reset();
modelPtr = storm::parser::AutoParser::parseModel(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/autoParser/ctmc.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/autoParser.lab");
ASSERT_EQ(modelPtr->getType(), storm::models::CTMC);
ASSERT_EQ(modelPtr->getNumberOfStates(), 12);
ASSERT_EQ(modelPtr->getNumberOfTransitions(), 31);
ASSERT_EQ(storm::models::CTMC, modelPtr->getType());
ASSERT_EQ(12, modelPtr->getNumberOfStates());
ASSERT_EQ(31, modelPtr->getNumberOfTransitions());
// Mdp
modelPtr.reset();
modelPtr = storm::parser::AutoParser::parseModel(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/autoParser/mdp.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/autoParser.lab");
ASSERT_EQ(modelPtr->getType(), storm::models::MDP);
ASSERT_EQ(modelPtr->getNumberOfStates(), 12);
ASSERT_EQ(modelPtr->getNumberOfTransitions(), 36);
ASSERT_EQ(storm::models::MDP, modelPtr->getType());
ASSERT_EQ(12, modelPtr->getNumberOfStates());
ASSERT_EQ(36, modelPtr->getNumberOfTransitions());
// Ctmdp
// Note: For now we use the Mdp from above just given the ctmdp hint, since the implementation of the Ctmdp model seems not Quite right yet.
@ -78,14 +78,14 @@ TEST(AutoParserTest, Decision) {
// TODO: Fix the Ctmdp implementation and use an actual Ctmdp for testing.
modelPtr.reset();
modelPtr = storm::parser::AutoParser::parseModel(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/autoParser/ctmdp.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/autoParser.lab");
ASSERT_EQ(modelPtr->getType(), storm::models::CTMDP);
ASSERT_EQ(modelPtr->getNumberOfStates(), 12);
ASSERT_EQ(modelPtr->getNumberOfTransitions(), 36);
ASSERT_EQ(storm::models::CTMDP, modelPtr->getType());
ASSERT_EQ(12, modelPtr->getNumberOfStates());
ASSERT_EQ(36, modelPtr->getNumberOfTransitions());
// MA
modelPtr.reset();
modelPtr = storm::parser::AutoParser::parseModel(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/autoParser/ma.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/autoParser.lab");
ASSERT_EQ(modelPtr->getType(), storm::models::MA);
ASSERT_EQ(modelPtr->getNumberOfStates(), 12);
ASSERT_EQ(modelPtr->getNumberOfTransitions(), 35);
ASSERT_EQ(storm::models::MA, modelPtr->getType());
ASSERT_EQ(12, modelPtr->getNumberOfStates());
ASSERT_EQ(35, modelPtr->getNumberOfTransitions());
}

36
test/functional/parser/DeterministicModelParserTest.cpp

@ -25,30 +25,30 @@ TEST(DeterministicModelParserTest, BasicDtmcParsing) {
// Parse a Dtmc and check the result.
storm::models::Dtmc<double> dtmc(storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_general.lab", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_general.state.rew", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_general.trans.rew"));
ASSERT_EQ(dtmc.getNumberOfStates(), 8);
ASSERT_EQ(dtmc.getNumberOfTransitions(), 21);
ASSERT_EQ(8, dtmc.getNumberOfStates());
ASSERT_EQ(21, dtmc.getNumberOfTransitions());
ASSERT_EQ(dtmc.getInitialStates().getNumberOfSetBits(), 2);
ASSERT_EQ(2, dtmc.getInitialStates().getNumberOfSetBits());
ASSERT_TRUE(dtmc.getInitialStates().get(0));
ASSERT_TRUE(dtmc.getInitialStates().get(7));
ASSERT_EQ(dtmc.getStateLabeling().getNumberOfAtomicPropositions(), 5);
ASSERT_EQ(dtmc.getLabelsForState(6).size(), 2);
ASSERT_EQ(5, dtmc.getStateLabeling().getNumberOfAtomicPropositions());
ASSERT_EQ(2, dtmc.getLabelsForState(6).size());
ASSERT_TRUE(dtmc.hasStateRewards());
ASSERT_EQ(dtmc.getStateRewardVector()[7], 42);
ASSERT_EQ(42, dtmc.getStateRewardVector()[7]);
double rewardSum = 0;
for(uint_fast64_t i = 0; i < dtmc.getStateRewardVector().size(); i++) {
rewardSum += dtmc.getStateRewardVector()[i];
}
ASSERT_EQ(rewardSum, 263.32);
ASSERT_EQ(263.32, rewardSum);
ASSERT_TRUE(dtmc.hasTransitionRewards());
ASSERT_EQ(dtmc.getTransitionRewardMatrix().getEntryCount(), 17);
ASSERT_EQ(17, dtmc.getTransitionRewardMatrix().getEntryCount());
rewardSum = 0;
for(uint_fast64_t i = 0; i < dtmc.getTransitionRewardMatrix().getRowCount(); i++) {
rewardSum += dtmc.getTransitionRewardMatrix().getRowSum(i);
}
ASSERT_EQ(rewardSum, 125.4);
ASSERT_EQ(125.4, rewardSum);
}
@ -57,30 +57,30 @@ TEST(DeterministicModelParserTest, BasicCtmcParsing) {
// Parse a Ctmc and check the result.
storm::models::Ctmc<double> ctmc(storm::parser::DeterministicModelParser::parseCtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_general.lab", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_general.state.rew", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_general.trans.rew"));
ASSERT_EQ(ctmc.getNumberOfStates(), 8);
ASSERT_EQ(ctmc.getNumberOfTransitions(), 21);
ASSERT_EQ(8, ctmc.getNumberOfStates());
ASSERT_EQ(21, ctmc.getNumberOfTransitions());
ASSERT_EQ(ctmc.getInitialStates().getNumberOfSetBits(), 2);
ASSERT_EQ(2, ctmc.getInitialStates().getNumberOfSetBits());
ASSERT_TRUE(ctmc.getInitialStates().get(0));
ASSERT_TRUE(ctmc.getInitialStates().get(7));
ASSERT_EQ(ctmc.getStateLabeling().getNumberOfAtomicPropositions(), 5);
ASSERT_EQ(ctmc.getLabelsForState(6).size(), 2);
ASSERT_EQ(5, ctmc.getStateLabeling().getNumberOfAtomicPropositions());
ASSERT_EQ(2, ctmc.getLabelsForState(6).size());
ASSERT_TRUE(ctmc.hasStateRewards());
ASSERT_EQ(ctmc.getStateRewardVector()[7], 42);
ASSERT_EQ(42, ctmc.getStateRewardVector()[7]);
double rewardSum = 0;
for(uint_fast64_t i = 0; i < ctmc.getStateRewardVector().size(); i++) {
rewardSum += ctmc.getStateRewardVector()[i];
}
ASSERT_EQ(rewardSum, 263.32);
ASSERT_EQ(263.32, rewardSum);
ASSERT_TRUE(ctmc.hasTransitionRewards());
ASSERT_EQ(ctmc.getTransitionRewardMatrix().getEntryCount(), 17);
ASSERT_EQ(17, ctmc.getTransitionRewardMatrix().getEntryCount());
rewardSum = 0;
for(uint_fast64_t i = 0; i < ctmc.getTransitionRewardMatrix().getRowCount(); i++) {
rewardSum += ctmc.getTransitionRewardMatrix().getRowSum(i);
}
ASSERT_EQ(rewardSum, 125.4);
ASSERT_EQ(125.4, rewardSum);
}
TEST(DeterministicModelParserTest, MismatchedFiles) {

180
test/functional/parser/DeterministicSparseTransitionParserTest.cpp

@ -29,74 +29,74 @@ TEST(DeterministicSparseTransitionParserTest, BasicTransitionsParsing) {
// Parse a deterministic transitions file and test the resulting matrix.
storm::storage::SparseMatrix<double> transitionMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general.tra");
ASSERT_EQ(transitionMatrix.getColumnCount(), 8);
ASSERT_EQ(transitionMatrix.getEntryCount(), 21);
ASSERT_EQ(8, transitionMatrix.getColumnCount());
ASSERT_EQ(21, transitionMatrix.getEntryCount());
// Test every entry of the matrix.
storm::storage::SparseMatrix<double>::const_iterator cIter = transitionMatrix.begin(0);
ASSERT_EQ(cIter->first, 0);
ASSERT_EQ(cIter->second, 0);
ASSERT_EQ(0, cIter->first);
ASSERT_EQ(0, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 1);
ASSERT_EQ(cIter->second, 1);
ASSERT_EQ(1, cIter->first);
ASSERT_EQ(1, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 1);
ASSERT_EQ(cIter->second, 0);
ASSERT_EQ(1, cIter->first);
ASSERT_EQ(0, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 2);
ASSERT_EQ(cIter->second, 0.5);
ASSERT_EQ(2, cIter->first);
ASSERT_EQ(0.5, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 3);
ASSERT_EQ(cIter->second, 0.5);
ASSERT_EQ(3, cIter->first);
ASSERT_EQ(0.5, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 2);
ASSERT_EQ(cIter->second, 0);
ASSERT_EQ(2, cIter->first);
ASSERT_EQ(0, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 3);
ASSERT_EQ(cIter->second, 0.4);
ASSERT_EQ(3, cIter->first);
ASSERT_EQ(0.4, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 4);
ASSERT_EQ(cIter->second, 0.4);
ASSERT_EQ(4, cIter->first);
ASSERT_EQ(0.4, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 5);
ASSERT_EQ(cIter->second, 0.2);
ASSERT_EQ(5, cIter->first);
ASSERT_EQ(0.2, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 3);
ASSERT_EQ(cIter->second, 1);
ASSERT_EQ(3, cIter->first);
ASSERT_EQ(1, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 3);
ASSERT_EQ(cIter->second, 1);
ASSERT_EQ(3, cIter->first);
ASSERT_EQ(1, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 4);
ASSERT_EQ(cIter->second, 0);
ASSERT_EQ(4, cIter->first);
ASSERT_EQ(0, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 3);
ASSERT_EQ(cIter->second, 0.1);
ASSERT_EQ(3, cIter->first);
ASSERT_EQ(0.1, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 4);
ASSERT_EQ(cIter->second, 0.1);
ASSERT_EQ(4, cIter->first);
ASSERT_EQ(0.1, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 5);
ASSERT_EQ(cIter->second, 0.1);
ASSERT_EQ(5, cIter->first);
ASSERT_EQ(0.1, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 6);
ASSERT_EQ(cIter->second, 0.7);
ASSERT_EQ(6, cIter->first);
ASSERT_EQ(0.7, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 0);
ASSERT_EQ(cIter->second, 0.9);
ASSERT_EQ(0, cIter->first);
ASSERT_EQ(0.9, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 5);
ASSERT_EQ(cIter->second, 0);
ASSERT_EQ(5, cIter->first);
ASSERT_EQ(0, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 6);
ASSERT_EQ(cIter->second, 0.1);
ASSERT_EQ(6, cIter->first);
ASSERT_EQ(0.1, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 6);
ASSERT_EQ(cIter->second, 0.224653);
ASSERT_EQ(6, cIter->first);
ASSERT_EQ(0.224653, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 7);
ASSERT_EQ(cIter->second, 0.775347);
ASSERT_EQ(7, cIter->first);
ASSERT_EQ(0.775347, cIter->second);
}
TEST(DeterministicSparseTransitionParserTest, BasicTransitionsRewardsParsing) {
@ -106,62 +106,62 @@ TEST(DeterministicSparseTransitionParserTest, BasicTransitionsRewardsParsing) {
storm::storage::SparseMatrix<double> rewardMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_general.trans.rew", transitionMatrix);
ASSERT_EQ(rewardMatrix.getColumnCount(), 8);
ASSERT_EQ(rewardMatrix.getEntryCount(), 17);
ASSERT_EQ(8, rewardMatrix.getColumnCount());
ASSERT_EQ(17, rewardMatrix.getEntryCount());
// Test every entry of the matrix.
storm::storage::SparseMatrix<double>::const_iterator cIter = rewardMatrix.begin(0);
ASSERT_EQ(cIter->first, 1);
ASSERT_EQ(cIter->second, 10);
ASSERT_EQ(1, cIter->first);
ASSERT_EQ(10, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 2);
ASSERT_EQ(cIter->second, 5);
ASSERT_EQ(2, cIter->first);
ASSERT_EQ(5, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 3);
ASSERT_EQ(cIter->second, 5.5);
ASSERT_EQ(3, cIter->first);
ASSERT_EQ(5.5, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 3);
ASSERT_EQ(cIter->second, 21.4);
ASSERT_EQ(3, cIter->first);
ASSERT_EQ(21.4, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 4);
ASSERT_EQ(cIter->second, 4);
ASSERT_EQ(4, cIter->first);
ASSERT_EQ(4, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 5);
ASSERT_EQ(cIter->second, 2);
ASSERT_EQ(5, cIter->first);
ASSERT_EQ(2, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 3);
ASSERT_EQ(cIter->second, 1);
ASSERT_EQ(3, cIter->first);
ASSERT_EQ(1, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 3);
ASSERT_EQ(cIter->second, 1);
ASSERT_EQ(3, cIter->first);
ASSERT_EQ(1, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 3);
ASSERT_EQ(cIter->second, 0.1);
ASSERT_EQ(3, cIter->first);
ASSERT_EQ(0.1, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 4);
ASSERT_EQ(cIter->second, 1.1);
ASSERT_EQ(4, cIter->first);
ASSERT_EQ(1.1, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 5);
ASSERT_EQ(cIter->second, 9.5);
ASSERT_EQ(5, cIter->first);
ASSERT_EQ(9.5, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 6);
ASSERT_EQ(cIter->second, 6.7);
ASSERT_EQ(6, cIter->first);
ASSERT_EQ(6.7, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 0);
ASSERT_EQ(cIter->second, 1);
ASSERT_EQ(0, cIter->first);
ASSERT_EQ(1, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 5);
ASSERT_EQ(cIter->second, 0);
ASSERT_EQ(5, cIter->first);
ASSERT_EQ(0, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 6);
ASSERT_EQ(cIter->second, 12);
ASSERT_EQ(6, cIter->first);
ASSERT_EQ(12, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 6);
ASSERT_EQ(cIter->second, 35.224653);
ASSERT_EQ(6, cIter->first);
ASSERT_EQ(35.224653, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 7);
ASSERT_EQ(cIter->second, 9.875347);
ASSERT_EQ(7, cIter->first);
ASSERT_EQ(9.875347, cIter->second);
}
@ -197,21 +197,21 @@ TEST(DeterministicSparseTransitionParserTest, FixDeadlocks) {
// Parse a transitions file with the fixDeadlocks Flag set and test if it works.
storm::storage::SparseMatrix<double> transitionMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_deadlock.tra");
ASSERT_EQ(transitionMatrix.getColumnCount(), 9);
ASSERT_EQ(transitionMatrix.getEntryCount(), 23);
ASSERT_EQ(9, transitionMatrix.getColumnCount());
ASSERT_EQ(23, transitionMatrix.getEntryCount());
storm::storage::SparseMatrix<double>::const_iterator cIter = transitionMatrix.begin(7);
ASSERT_EQ(cIter->first, 7);
ASSERT_EQ(cIter->second, 1);
ASSERT_EQ(7, cIter->first);
ASSERT_EQ(1, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 6);
ASSERT_EQ(cIter->second, 0.224653);
ASSERT_EQ(6, cIter->first);
ASSERT_EQ(0.224653, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 7);
ASSERT_EQ(cIter->second, 0.775347);
ASSERT_EQ(7, cIter->first);
ASSERT_EQ(0.775347, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 8);
ASSERT_EQ(cIter->second, 0);
ASSERT_EQ(8, cIter->first);
ASSERT_EQ(0, cIter->second);
}
TEST(DeterministicSparseTransitionParserTest, DontFixDeadlocks) {

4
test/functional/parser/MappedFileTest.cpp

@ -22,10 +22,10 @@ TEST(MappedFileTest, BasicFunctionality) {
// Open a file and test if the content is loaded as expected.
storm::parser::MappedFile file(STORM_CPP_TESTS_BASE_PATH "/functional/parser/testStringFile.txt");
std::string testString = "This is a test string.\n";
ASSERT_EQ(file.getDataEnd() - file.getData(), testString.length());
ASSERT_EQ(testString.length(), file.getDataEnd() - file.getData());
char const * testStringPtr = testString.c_str();
for(char* dataPtr = file.getData(); dataPtr < file.getDataEnd(); dataPtr++) {
ASSERT_EQ(*dataPtr, *testStringPtr);
ASSERT_EQ(*testStringPtr, *dataPtr);
testStringPtr++;
}
}

30
test/functional/parser/MarkovAutomatonParserTest.cpp

@ -23,28 +23,28 @@ TEST(MarkovAutomatonParserTest, BasicParsing) {
storm::models::MarkovAutomaton<double> result = storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_general.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/ma_general.lab", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/ma_general.state.rew");
// Test sizes and counts.
ASSERT_EQ(result.getNumberOfStates(), 6);
ASSERT_EQ(result.getNumberOfChoices(), 7);
ASSERT_EQ(result.getNumberOfTransitions(), 12);
ASSERT_EQ(6, result.getNumberOfStates());
ASSERT_EQ(7, result.getNumberOfChoices());
ASSERT_EQ(12, result.getNumberOfTransitions());
// Test the exit rates. These have to be 0 for all non-Markovian states.
std::vector<double> rates = result.getExitRates();
ASSERT_EQ(result.getExitRate(0), 2);
ASSERT_EQ(2, result.getExitRate(0));
ASSERT_FALSE(result.isMarkovianState(1));
ASSERT_EQ(result.getExitRate(1), 0);
ASSERT_EQ(result.getExitRate(2), 15);
ASSERT_EQ(0, result.getExitRate(1));
ASSERT_EQ(15, result.getExitRate(2));
ASSERT_FALSE(result.isMarkovianState(3));
ASSERT_EQ(result.getExitRate(3), 0);
ASSERT_EQ(0, result.getExitRate(3));
ASSERT_FALSE(result.isMarkovianState(4));
ASSERT_EQ(result.getExitRate(4), 0);
ASSERT_EQ(0, result.getExitRate(4));
ASSERT_FALSE(result.isMarkovianState(5));
ASSERT_EQ(result.getExitRate(5), 0);
ASSERT_EQ(0, result.getExitRate(5));
// Test the labeling.
ASSERT_EQ(result.getStateLabeling().getNumberOfAtomicPropositions(), 3);
ASSERT_EQ(result.getInitialStates().getNumberOfSetBits(), 1);
ASSERT_EQ(result.getLabelsForState(4).size(), 0);
ASSERT_EQ(result.getStateLabeling().getLabeledStates("goal").getNumberOfSetBits(), 1);
ASSERT_EQ(3, result.getStateLabeling().getNumberOfAtomicPropositions());
ASSERT_EQ(1, result.getInitialStates().getNumberOfSetBits());
ASSERT_EQ(0, result.getLabelsForState(4).size());
ASSERT_EQ(1, result.getStateLabeling().getLabeledStates("goal").getNumberOfSetBits());
// Test the state rewards.
ASSERT_TRUE(result.hasStateRewards());
@ -52,8 +52,8 @@ TEST(MarkovAutomatonParserTest, BasicParsing) {
for(uint_fast64_t i = 0; i < result.getStateRewardVector().size(); i++) {
rewardSum += result.getStateRewardVector()[i];
}
ASSERT_EQ(rewardSum, 1015.765099984);
ASSERT_EQ(result.getStateRewardVector()[0], 0);
ASSERT_EQ(1015.765099984, rewardSum);
ASSERT_EQ(0, result.getStateRewardVector()[0]);
// Test the transition rewards.
ASSERT_FALSE(result.hasTransitionRewards());

156
test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp

@ -39,26 +39,26 @@ TEST(MarkovAutomatonSparseTransitionParserTest, BasicParsing) {
storm::storage::SparseMatrix<double> transitionMatrix(result.transitionMatrixBuilder.build(0,0));
// Test all sizes and counts.
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(STATE_COUNT, transitionMatrix.getColumnCount());
ASSERT_EQ(CHOICE_COUNT, transitionMatrix.getRowCount());
ASSERT_EQ(12, transitionMatrix.getEntryCount());
ASSERT_EQ(6, transitionMatrix.getRowGroupCount());
ASSERT_EQ(7, transitionMatrix.getRowGroupIndices().size());
ASSERT_EQ(CHOICE_COUNT, result.markovianChoices.size());
ASSERT_EQ(STATE_COUNT, result.markovianStates.size());
ASSERT_EQ(2, result.markovianStates.getNumberOfSetBits());
ASSERT_EQ(STATE_COUNT, result.exitRates.size());
// 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(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);
ASSERT_EQ(0, transitionMatrix.getRowGroupIndices()[0]);
ASSERT_EQ(1, transitionMatrix.getRowGroupIndices()[1]);
ASSERT_EQ(2, transitionMatrix.getRowGroupIndices()[2]);
ASSERT_EQ(3, transitionMatrix.getRowGroupIndices()[3]);
ASSERT_EQ(4, transitionMatrix.getRowGroupIndices()[4]);
ASSERT_EQ(6, transitionMatrix.getRowGroupIndices()[5]);
ASSERT_EQ(7, transitionMatrix.getRowGroupIndices()[6]);
// Test the Markovian states.
ASSERT_TRUE(result.markovianStates.get(0));
@ -69,39 +69,39 @@ TEST(MarkovAutomatonSparseTransitionParserTest, BasicParsing) {
ASSERT_FALSE(result.markovianStates.get(5));
// Test the exit rates. These have to be 0 for all non-Markovian states.
ASSERT_EQ(result.exitRates[0], 2);
ASSERT_EQ(result.exitRates[1], 0);
ASSERT_EQ(result.exitRates[2], 15);
ASSERT_EQ(result.exitRates[3], 0);
ASSERT_EQ(result.exitRates[4], 0);
ASSERT_EQ(result.exitRates[5], 0);
ASSERT_EQ(2, result.exitRates[0]);
ASSERT_EQ(0, result.exitRates[1]);
ASSERT_EQ(15, result.exitRates[2]);
ASSERT_EQ(0, result.exitRates[3]);
ASSERT_EQ(0, result.exitRates[4]);
ASSERT_EQ(0, result.exitRates[5]);
// Finally, test the transition matrix itself.
storm::storage::SparseMatrix<double>::const_iterator cIter = transitionMatrix.begin(0);
ASSERT_EQ(cIter->second, 2);
ASSERT_EQ(2, cIter->second);
cIter++;
ASSERT_EQ(cIter->second, 1);
ASSERT_EQ(1, cIter->second);
cIter++;
ASSERT_EQ(cIter->second, 1);
ASSERT_EQ(1, cIter->second);
cIter++;
ASSERT_EQ(cIter->second, 2);
ASSERT_EQ(2, cIter->second);
cIter++;
ASSERT_EQ(cIter->second, 4);
ASSERT_EQ(4, cIter->second);
cIter++;
ASSERT_EQ(cIter->second, 8);
ASSERT_EQ(8, cIter->second);
cIter++;
ASSERT_EQ(cIter->second, 0.5);
ASSERT_EQ(0.5, cIter->second);
cIter++;
ASSERT_EQ(cIter->second, 0.5);
ASSERT_EQ(0.5, cIter->second);
cIter++;
ASSERT_EQ(cIter->second, 1);
ASSERT_EQ(1, cIter->second);
cIter++;
ASSERT_EQ(cIter->second, 0.5);
ASSERT_EQ(0.5, cIter->second);
cIter++;
ASSERT_EQ(cIter->second, 0.5);
ASSERT_EQ(0.5, cIter->second);
cIter++;
ASSERT_EQ(cIter->second, 1);
ASSERT_EQ(1, cIter->second);
cIter++;
ASSERT_EQ(transitionMatrix.end(), cIter);
}
@ -114,29 +114,29 @@ TEST(MarkovAutomatonSparseTransitionParserTest, Whitespaces) {
storm::parser::MarkovAutomatonSparseTransitionParser::Result result = storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(filename);
// Build the actual transition matrix.
storm::storage::SparseMatrix<double> transitionMatrix(result.transitionMatrixBuilder.build(0,0));
storm::storage::SparseMatrix<double> transitionMatrix(result.transitionMatrixBuilder.build());
// Test all sizes and counts.
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(STATE_COUNT, transitionMatrix.getColumnCount());
ASSERT_EQ(CHOICE_COUNT, transitionMatrix.getRowCount());
ASSERT_EQ(12, transitionMatrix.getEntryCount());
ASSERT_EQ(6, transitionMatrix.getRowGroupCount());
ASSERT_EQ(7, transitionMatrix.getRowGroupIndices().size());
ASSERT_EQ(CHOICE_COUNT, result.markovianChoices.size());
ASSERT_EQ(STATE_COUNT, result.markovianStates.size());
ASSERT_EQ(2, result.markovianStates.getNumberOfSetBits());
ASSERT_EQ(STATE_COUNT, result.exitRates.size());
// 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(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);
ASSERT_EQ(0, transitionMatrix.getRowGroupIndices()[0]);
ASSERT_EQ(1, transitionMatrix.getRowGroupIndices()[1]);
ASSERT_EQ(2, transitionMatrix.getRowGroupIndices()[2]);
ASSERT_EQ(3, transitionMatrix.getRowGroupIndices()[3]);
ASSERT_EQ(4, transitionMatrix.getRowGroupIndices()[4]);
ASSERT_EQ(6, transitionMatrix.getRowGroupIndices()[5]);
ASSERT_EQ(7, transitionMatrix.getRowGroupIndices()[6]);
// Test the Markovian states.
ASSERT_TRUE(result.markovianStates.get(0));
@ -147,39 +147,39 @@ TEST(MarkovAutomatonSparseTransitionParserTest, Whitespaces) {
ASSERT_FALSE(result.markovianStates.get(5));
// Test the exit rates. These have to be 0 for all non-Markovian states.
ASSERT_EQ(result.exitRates[0], 2);
ASSERT_EQ(result.exitRates[1], 0);
ASSERT_EQ(result.exitRates[2], 15);
ASSERT_EQ(result.exitRates[3], 0);
ASSERT_EQ(result.exitRates[4], 0);
ASSERT_EQ(result.exitRates[5], 0);
ASSERT_EQ(2, result.exitRates[0]);
ASSERT_EQ(0, result.exitRates[1]);
ASSERT_EQ(15, result.exitRates[2]);
ASSERT_EQ(0, result.exitRates[3]);
ASSERT_EQ(0, result.exitRates[4]);
ASSERT_EQ(0, result.exitRates[5]);
// Finally, test the transition matrix itself.
storm::storage::SparseMatrix<double>::const_iterator cIter = transitionMatrix.begin(0);
ASSERT_EQ(cIter->second, 2);
ASSERT_EQ(2, cIter->second);
cIter++;
ASSERT_EQ(cIter->second, 1);
ASSERT_EQ(1, cIter->second);
cIter++;
ASSERT_EQ(cIter->second, 1);
ASSERT_EQ(1, cIter->second);
cIter++;
ASSERT_EQ(cIter->second, 2);
ASSERT_EQ(2, cIter->second);
cIter++;
ASSERT_EQ(cIter->second, 4);
ASSERT_EQ(4, cIter->second);
cIter++;
ASSERT_EQ(cIter->second, 8);
ASSERT_EQ(8, cIter->second);
cIter++;
ASSERT_EQ(cIter->second, 0.5);
ASSERT_EQ(0.5, cIter->second);
cIter++;
ASSERT_EQ(cIter->second, 0.5);
ASSERT_EQ(0.5, cIter->second);
cIter++;
ASSERT_EQ(cIter->second, 1);
ASSERT_EQ(1, cIter->second);
cIter++;
ASSERT_EQ(cIter->second, 0.5);
ASSERT_EQ(0.5, cIter->second);
cIter++;
ASSERT_EQ(cIter->second, 0.5);
ASSERT_EQ(0.5, cIter->second);
cIter++;
ASSERT_EQ(cIter->second, 1);
ASSERT_EQ(1, cIter->second);
cIter++;
ASSERT_EQ(transitionMatrix.end(), cIter);
}
@ -192,15 +192,15 @@ TEST(MarkovAutomatonSparseTransitionParserTest, FixDeadlocks) {
storm::parser::MarkovAutomatonSparseTransitionParser::Result result = storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_deadlock.tra");
// Test if the result is consistent with the parsed Markov Automaton.
storm::storage::SparseMatrix<double> 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);
storm::storage::SparseMatrix<double> resultMatrix(result.transitionMatrixBuilder.build());
ASSERT_EQ(STATE_COUNT + 1, resultMatrix.getColumnCount());
ASSERT_EQ(13, resultMatrix.getEntryCount());
ASSERT_EQ(7, resultMatrix.getRowGroupCount());
ASSERT_EQ(8, resultMatrix.getRowGroupIndices().size());
ASSERT_EQ(CHOICE_COUNT +1, result.markovianChoices.size());
ASSERT_EQ(STATE_COUNT +1, result.markovianStates.size());
ASSERT_EQ(2, result.markovianStates.getNumberOfSetBits());
ASSERT_EQ(STATE_COUNT + 1, result.exitRates.size());
}
TEST(MarkovAutomatonSparseTransitionParserTest, DontFixDeadlocks) {

42
test/functional/parser/NondeterministicModelParserTest.cpp

@ -25,32 +25,32 @@ TEST(NondeterministicModelParserTest, BasicMdpParsing) {
// Parse a Mdp and check the result.
storm::models::Mdp<double> mdp(storm::parser::NondeterministicModelParser::parseMdp(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/mdp_general.lab", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_general.state.rew", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_general.trans.rew"));
ASSERT_EQ(mdp.getNumberOfStates(), 6);
ASSERT_EQ(mdp.getNumberOfTransitions(), 22);
ASSERT_EQ(mdp.getNumberOfChoices(), 11);
ASSERT_EQ(6, mdp.getNumberOfStates());
ASSERT_EQ(22, mdp.getNumberOfTransitions());
ASSERT_EQ(11, mdp.getNumberOfChoices());
ASSERT_EQ(mdp.getInitialStates().getNumberOfSetBits(), 2);
ASSERT_EQ(2, mdp.getInitialStates().getNumberOfSetBits());
ASSERT_TRUE(mdp.getInitialStates().get(0));
ASSERT_TRUE(mdp.getInitialStates().get(4));
ASSERT_EQ(mdp.getStateLabeling().getNumberOfAtomicPropositions(), 4);
ASSERT_EQ(mdp.getLabelsForState(0).size(), 3);
ASSERT_EQ(4, mdp.getStateLabeling().getNumberOfAtomicPropositions());
ASSERT_EQ(3, mdp.getLabelsForState(0).size());
ASSERT_TRUE(mdp.hasStateRewards());
ASSERT_EQ(mdp.getStateRewardVector()[0], 0);
ASSERT_EQ(mdp.getStateRewardVector()[4], 42);
ASSERT_EQ(0, mdp.getStateRewardVector()[0]);
ASSERT_EQ(42, mdp.getStateRewardVector()[4]);
double rewardSum = 0;
for(uint_fast64_t i = 0; i < mdp.getStateRewardVector().size(); i++) {
rewardSum += mdp.getStateRewardVector()[i];
}
ASSERT_EQ(rewardSum, 158.32);
ASSERT_EQ(158.32, rewardSum);
ASSERT_TRUE(mdp.hasTransitionRewards());
ASSERT_EQ(mdp.getTransitionRewardMatrix().getEntryCount(), 17);
ASSERT_EQ(17, mdp.getTransitionRewardMatrix().getEntryCount());
rewardSum = 0;
for(uint_fast64_t i = 0; i < mdp.getTransitionRewardMatrix().getRowCount(); i++) {
rewardSum += mdp.getTransitionRewardMatrix().getRowSum(i);
}
ASSERT_EQ(rewardSum, 1376.864);
ASSERT_EQ(1376.864, rewardSum);
}
@ -58,24 +58,24 @@ TEST(NondeterministicModelParserTest, BasicCtmdpParsing) {
// Parse a Ctmdp and check the result.
storm::models::Ctmdp<double> ctmdp(storm::parser::NondeterministicModelParser::parseCtmdp(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/mdp_general.lab", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_general.state.rew", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_general.trans.rew"));
ASSERT_EQ(ctmdp.getNumberOfStates(), 6);
ASSERT_EQ(ctmdp.getNumberOfTransitions(), 22);
ASSERT_EQ(ctmdp.getNumberOfChoices(), 11);
ASSERT_EQ(6, ctmdp.getNumberOfStates());
ASSERT_EQ(22, ctmdp.getNumberOfTransitions());
ASSERT_EQ(11, ctmdp.getNumberOfChoices());
ASSERT_EQ(ctmdp.getInitialStates().getNumberOfSetBits(), 2);
ASSERT_EQ(2, ctmdp.getInitialStates().getNumberOfSetBits());
ASSERT_TRUE(ctmdp.getInitialStates().get(0));
ASSERT_TRUE(ctmdp.getInitialStates().get(4));
ASSERT_EQ(ctmdp.getStateLabeling().getNumberOfAtomicPropositions(), 4);
ASSERT_EQ(ctmdp.getLabelsForState(0).size(), 3);
ASSERT_EQ(4, ctmdp.getStateLabeling().getNumberOfAtomicPropositions());
ASSERT_EQ(3, ctmdp.getLabelsForState(0).size());
ASSERT_TRUE(ctmdp.hasStateRewards());
ASSERT_EQ(ctmdp.getStateRewardVector()[0], 0);
ASSERT_EQ(ctmdp.getStateRewardVector()[4], 42);
ASSERT_EQ(0, ctmdp.getStateRewardVector()[0]);
ASSERT_EQ(42, ctmdp.getStateRewardVector()[4]);
double rewardSum = 0;
for(uint_fast64_t i = 0; i < ctmdp.getStateRewardVector().size(); i++) {
rewardSum += ctmdp.getStateRewardVector()[i];
}
ASSERT_EQ(rewardSum, 158.32);
ASSERT_EQ(158.32, rewardSum);
ASSERT_TRUE(ctmdp.hasTransitionRewards());
ASSERT_EQ(ctmdp.getTransitionRewardMatrix().getEntryCount(), 17);
@ -83,7 +83,7 @@ TEST(NondeterministicModelParserTest, BasicCtmdpParsing) {
for(uint_fast64_t i = 0; i < ctmdp.getTransitionRewardMatrix().getRowCount(); i++) {
rewardSum += ctmdp.getTransitionRewardMatrix().getRowSum(i);
}
ASSERT_EQ(rewardSum, 1376.864);
ASSERT_EQ(1376.864, rewardSum);
}
TEST(NondeterministicModelParserTest, MismatchedFiles) {

224
test/functional/parser/NondeterministicSparseTransitionParserTest.cpp

@ -32,87 +32,87 @@ TEST(NondeterministicSparseTransitionParserTest, BasicTransitionsParsing) {
// Test the row mapping, i.e. at which row which state starts.
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);
ASSERT_EQ(0, result.getRowGroupIndices()[0]);
ASSERT_EQ(4, result.getRowGroupIndices()[1]);
ASSERT_EQ(5, result.getRowGroupIndices()[2]);
ASSERT_EQ(7, result.getRowGroupIndices()[3]);
ASSERT_EQ(8, result.getRowGroupIndices()[4]);
ASSERT_EQ(9, result.getRowGroupIndices()[5]);
ASSERT_EQ(11, result.getRowGroupIndices()[6]);
// Test the transition matrix.
ASSERT_EQ(result.getColumnCount(), 6);
ASSERT_EQ(result.getRowCount(), 11);
ASSERT_EQ(result.getEntryCount(), 22);
ASSERT_EQ(6, result.getColumnCount());
ASSERT_EQ(11, result.getRowCount());
ASSERT_EQ(22, result.getEntryCount());
// Test every entry of the matrix.
storm::storage::SparseMatrix<double>::const_iterator cIter = result.begin(0);
ASSERT_EQ(cIter->first, 0);
ASSERT_EQ(cIter->second, 0.9);
ASSERT_EQ(0, cIter->first);
ASSERT_EQ(0.9, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 1);
ASSERT_EQ(cIter->second, 0.1);
ASSERT_EQ(1, cIter->first);
ASSERT_EQ(0.1, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 1);
ASSERT_EQ(cIter->second, 0.2);
ASSERT_EQ(1, cIter->first);
ASSERT_EQ(0.2, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 2);
ASSERT_EQ(cIter->second, 0.2);
ASSERT_EQ(2, cIter->first);
ASSERT_EQ(0.2, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 3);
ASSERT_EQ(cIter->second, 0.2);
ASSERT_EQ(3, cIter->first);
ASSERT_EQ(0.2, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 4);
ASSERT_EQ(cIter->second, 0.2);
ASSERT_EQ(4, cIter->first);
ASSERT_EQ(0.2, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 5);
ASSERT_EQ(cIter->second, 0.2);
ASSERT_EQ(5, cIter->first);
ASSERT_EQ(0.2, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 5);
ASSERT_EQ(cIter->second, 1);
ASSERT_EQ(5, cIter->first);
ASSERT_EQ(1, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 0);
ASSERT_EQ(cIter->second, 0.1);
ASSERT_EQ(0, cIter->first);
ASSERT_EQ(0.1, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 4);
ASSERT_EQ(cIter->second, 0.9);
ASSERT_EQ(4, cIter->first);
ASSERT_EQ(0.9, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 2);
ASSERT_EQ(cIter->second, 1);
ASSERT_EQ(2, cIter->first);
ASSERT_EQ(1, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 2);
ASSERT_EQ(cIter->second, 0.5);
ASSERT_EQ(2, cIter->first);
ASSERT_EQ(0.5, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 3);
ASSERT_EQ(cIter->second, 0.5);
ASSERT_EQ(3, cIter->first);
ASSERT_EQ(0.5, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 2);
ASSERT_EQ(cIter->second, 1);
ASSERT_EQ(2, cIter->first);
ASSERT_EQ(1, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 2);
ASSERT_EQ(cIter->second, 0.001);
ASSERT_EQ(2, cIter->first);
ASSERT_EQ(0.001, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 3);
ASSERT_EQ(cIter->second, 0.999);
ASSERT_EQ(3, cIter->first);
ASSERT_EQ(0.999, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 1);
ASSERT_EQ(cIter->second, 0.7);
ASSERT_EQ(1, cIter->first);
ASSERT_EQ(0.7, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 4);
ASSERT_EQ(cIter->second, 0.3);
ASSERT_EQ(4, cIter->first);
ASSERT_EQ(0.3, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 1);
ASSERT_EQ(cIter->second, 0.2);
ASSERT_EQ(1, cIter->first);
ASSERT_EQ(0.2, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 4);
ASSERT_EQ(cIter->second, 0.2);
ASSERT_EQ(4, cIter->first);
ASSERT_EQ(0.2, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 5);
ASSERT_EQ(cIter->second, 0.6);
ASSERT_EQ(5, cIter->first);
ASSERT_EQ(0.6, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 5);
ASSERT_EQ(cIter->second, 1);
ASSERT_EQ(5, cIter->first);
ASSERT_EQ(1, cIter->second);
}
TEST(NondeterministicSparseTransitionParserTest, BasicTransitionsRewardsParsing) {
@ -121,63 +121,63 @@ TEST(NondeterministicSparseTransitionParserTest, BasicTransitionsRewardsParsing)
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.
ASSERT_EQ(result.getColumnCount(), 6);
ASSERT_EQ(result.getRowCount(), 11);
ASSERT_EQ(result.getEntryCount(), 17);
ASSERT_EQ(6, result.getColumnCount());
ASSERT_EQ(11, result.getRowCount());
ASSERT_EQ(17, result.getEntryCount());
// Test every entry of the matrix.
storm::storage::SparseMatrix<double>::const_iterator cIter = result.begin(0);
ASSERT_EQ(cIter->first, 0);
ASSERT_EQ(cIter->second, 1);
ASSERT_EQ(0, cIter->first);
ASSERT_EQ(1, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 1);
ASSERT_EQ(cIter->second, 30);
ASSERT_EQ(1, cIter->first);
ASSERT_EQ(30, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 1);
ASSERT_EQ(cIter->second, 15.2);
ASSERT_EQ(1, cIter->first);
ASSERT_EQ(15.2, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 2);
ASSERT_EQ(cIter->second, 75);
ASSERT_EQ(2, cIter->first);
ASSERT_EQ(75, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 5);
ASSERT_EQ(cIter->second, 2.45);
ASSERT_EQ(5, cIter->first);
ASSERT_EQ(2.45, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 5);
ASSERT_EQ(cIter->second, 1);
ASSERT_EQ(5, cIter->first);
ASSERT_EQ(1, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 0);
ASSERT_EQ(cIter->second, 0.114);
ASSERT_EQ(0, cIter->first);
ASSERT_EQ(0.114, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 4);
ASSERT_EQ(cIter->second, 90);
ASSERT_EQ(4, cIter->first);
ASSERT_EQ(90, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 2);
ASSERT_EQ(cIter->second, 1);
ASSERT_EQ(2, cIter->first);
ASSERT_EQ(1, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 2);
ASSERT_EQ(cIter->second, 55);
ASSERT_EQ(2, cIter->first);
ASSERT_EQ(55, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 3);
ASSERT_EQ(cIter->second, 87);
ASSERT_EQ(3, cIter->first);
ASSERT_EQ(87, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 2);
ASSERT_EQ(cIter->second, 13);
ASSERT_EQ(2, cIter->first);
ASSERT_EQ(13, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 3);
ASSERT_EQ(cIter->second, 999);
ASSERT_EQ(3, cIter->first);
ASSERT_EQ(999, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 1);
ASSERT_EQ(cIter->second, 0.7);
ASSERT_EQ(1, cIter->first);
ASSERT_EQ(0.7, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 4);
ASSERT_EQ(cIter->second, 0.3);
ASSERT_EQ(4, cIter->first);
ASSERT_EQ(0.3, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 1);
ASSERT_EQ(cIter->second, 0.1);
ASSERT_EQ(1, cIter->first);
ASSERT_EQ(0.1, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 5);
ASSERT_EQ(cIter->second, 6);
ASSERT_EQ(5, cIter->first);
ASSERT_EQ(6, cIter->second);
}
TEST(NondeterministicSparseTransitionParserTest, Whitespaces) {
@ -213,37 +213,37 @@ TEST(NondeterministicSparseTransitionParserTest, FixDeadlocks) {
// Parse a transitions file with the fixDeadlocks Flag set and test if it works.
storm::storage::SparseMatrix<double> result(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_deadlock.tra"));
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(8, result.getRowGroupIndices().size());
ASSERT_EQ(9, result.getRowGroupIndices()[5]);
ASSERT_EQ(10, result.getRowGroupIndices()[6]);
ASSERT_EQ(12, result.getRowGroupIndices()[7]);
ASSERT_EQ(result.getColumnCount(), 7);
ASSERT_EQ(result.getRowCount(), 12);
ASSERT_EQ(result.getEntryCount(), 23);
ASSERT_EQ(7, result.getColumnCount());
ASSERT_EQ(12, result.getRowCount());
ASSERT_EQ(23, result.getEntryCount());
storm::storage::SparseMatrix<double>::const_iterator cIter = result.begin(8);
ASSERT_EQ(cIter->first, 1);
ASSERT_EQ(cIter->second, 0.7);
ASSERT_EQ(1, cIter->first);
ASSERT_EQ(0.7, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 4);
ASSERT_EQ(cIter->second, 0.3);
ASSERT_EQ(4, cIter->first);
ASSERT_EQ(0.3, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 5);
ASSERT_EQ(cIter->second, 1);
ASSERT_EQ(5, cIter->first);
ASSERT_EQ(1, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 1);
ASSERT_EQ(cIter->second, 0.2);
ASSERT_EQ(1, cIter->first);
ASSERT_EQ(0.2, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 4);
ASSERT_EQ(cIter->second, 0.2);
ASSERT_EQ(4, cIter->first);
ASSERT_EQ(0.2, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 5);
ASSERT_EQ(cIter->second, 0.6);
ASSERT_EQ(5, cIter->first);
ASSERT_EQ(0.6, cIter->second);
cIter++;
ASSERT_EQ(cIter->first, 5);
ASSERT_EQ(cIter->second, 1);
ASSERT_EQ(5, cIter->first);
ASSERT_EQ(1, cIter->second);
}

4
test/functional/parser/SparseStateRewardParserTest.cpp

@ -36,7 +36,7 @@ TEST(SparseStateRewardParserTest, BasicParsing) {
// Now test if the correct value were parsed.
for(int i = 0; i < 100; i++) {
ASSERT_EQ(std::round(result[i]) , std::round(2*i + 15/13*i*i - 1.5/(i+0.1) + 15.7));
ASSERT_EQ(std::round(2*i + 15/13*i*i - 1.5/(i+0.1) + 15.7), std::round(result[i]));
}
}
@ -47,7 +47,7 @@ TEST(SparseStateRewardParserTest, Whitespaces) {
// Now test if the correct value were parsed.
for(int i = 0; i < 100; i++) {
ASSERT_EQ(std::round(result[i]) , std::round(2*i + 15/13*i*i - 1.5/(i+0.1) + 15.7));
ASSERT_EQ(std::round(2*i + 15/13*i*i - 1.5/(i+0.1) + 15.7), std::round(result[i]));
}
}

Loading…
Cancel
Save