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

got rid of more warnings 

Former-commit-id: 5c39f63c69
main
dehnert 10 years ago
parent
1e61030fa3
commit
56b4f53ce7
16 changed files with 217 additions and 210 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. 2
      CMakeLists.txt
  2. 2
      resources/3rdparty/cudd-2.5.0/CMakeLists.txt
  3. 6
      resources/3rdparty/log4cplus-1.1.3-rc1/src/CMakeLists.txt
  4. 4
      src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
  5. 1
      src/storage/BitVector.cpp
  6. 4
      src/storage/DeterministicModelBisimulationDecomposition.cpp
  7. 6
      src/storage/SparseMatrix.cpp
  8. 64
      src/utility/prism.cpp
  9. 56
      src/utility/prism.h
  10. 6
      test/functional/parser/DeterministicSparseTransitionParserTest.cpp
  11. 14
      test/functional/parser/NondeterministicModelParserTest.cpp
  12. 136
      test/functional/parser/NondeterministicSparseTransitionParserTest.cpp
  13. 2
      test/functional/parser/PrismParserTest.cpp
  14. 10
      test/functional/storage/BitVectorTest.cpp
  15. 110
      test/functional/storage/CuddDdTest.cpp
  16. 2
      test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp

2
CMakeLists.txt
View File

@ -163,7 +163,7 @@ else(CLANG)
endif() endif()
add_definitions(-DBOOST_RESULT_OF_USE_DECLTYPE) add_definitions(-DBOOST_RESULT_OF_USE_DECLTYPE)
set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11 -stdlib=${CLANG_STDLIB} -Wall -pedantic -Wno-unused-variable -ftemplate-depth=1024")
set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11 -stdlib=${CLANG_STDLIB} -Wall -pedantic -Wno-newline-eof -Wno-mismatched-tags -ftemplate-depth=1024")
set (CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wall -pedantic") set (CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wall -pedantic")
# Turn on popcnt instruction if desired (yes by default) # Turn on popcnt instruction if desired (yes by default)

2
resources/3rdparty/cudd-2.5.0/CMakeLists.txt
View File

@ -26,7 +26,7 @@ elseif(MSVC)
# required for GMM to compile, ugly error directive in their code # required for GMM to compile, ugly error directive in their code
add_definitions(/D_SCL_SECURE_NO_DEPRECATE /D_CRT_SECURE_NO_WARNINGS) add_definitions(/D_SCL_SECURE_NO_DEPRECATE /D_CRT_SECURE_NO_WARNINGS)
else(CLANG) else(CLANG)
set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wno-unused-variable -Wno-unused-but-set-variable -Wno-unused-function")
set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wno-newline-eof -Wno-unneeded-internal-declaration -Wno-unused-variable -Wno-unused-const-variable")
endif() endif()
# Since we do not target Alphas, this symbol is always set # Since we do not target Alphas, this symbol is always set

6
resources/3rdparty/log4cplus-1.1.3-rc1/src/CMakeLists.txt
View File

@ -75,6 +75,12 @@ if (WIN32)
add_definitions (-D_WIN32_WINNT=${_WIN32_WINNT}) add_definitions (-D_WIN32_WINNT=${_WIN32_WINNT})
endif (WIN32) endif (WIN32)
if(CMAKE_COMPILER_IS_GNUCC)
# nothing to do in this case
else(CLANG)
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-unused-variable")
endif()
add_library (${log4cplus} ${log4cplus_sources}) add_library (${log4cplus} ${log4cplus_sources})
set (log4cplus_LIBS ${CMAKE_THREAD_LIBS_INIT}) set (log4cplus_LIBS ${CMAKE_THREAD_LIBS_INIT})

4
src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
View File

@ -694,7 +694,6 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
void SparseDtmcEliminationModelChecker<ValueType>::eliminateState(FlexibleSparseMatrix& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions, boost::optional<std::vector<ValueType>>& stateRewards, bool removeForwardTransitions, bool constrained, storm::storage::BitVector const& predecessorConstraint) { void SparseDtmcEliminationModelChecker<ValueType>::eliminateState(FlexibleSparseMatrix& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions, boost::optional<std::vector<ValueType>>& stateRewards, bool removeForwardTransitions, bool constrained, storm::storage::BitVector const& predecessorConstraint) {
auto eliminationStart = std::chrono::high_resolution_clock::now();
bool hasSelfLoop = false; bool hasSelfLoop = false;
ValueType loopProbability = storm::utility::zero<ValueType>(); ValueType loopProbability = storm::utility::zero<ValueType>();
@ -917,9 +916,6 @@ namespace storm {
} else { } else {
currentStatePredecessors = std::move(newCurrentStatePredecessors); currentStatePredecessors = std::move(newCurrentStatePredecessors);
} }
auto eliminationEnd = std::chrono::high_resolution_clock::now();
auto eliminationTime = eliminationEnd - eliminationStart;
} }
template<typename ValueType> template<typename ValueType>

1
src/storage/BitVector.cpp
View File

@ -109,7 +109,6 @@ namespace storm {
std::vector<uint64_t>::const_iterator first1 = this->bucketVector.begin(); std::vector<uint64_t>::const_iterator first1 = this->bucketVector.begin();
std::vector<uint64_t>::const_iterator last1 = this->bucketVector.end(); std::vector<uint64_t>::const_iterator last1 = this->bucketVector.end();
std::vector<uint64_t>::const_iterator first2 = other.bucketVector.begin(); std::vector<uint64_t>::const_iterator first2 = other.bucketVector.begin();
std::vector<uint64_t>::const_iterator last2 = other.bucketVector.end();
for (; first1 != last1; ++first1, ++first2) { for (; first1 != last1; ++first1, ++first2) {
if (*first1 < *first2) { if (*first1 < *first2) {

4
src/storage/DeterministicModelBisimulationDecomposition.cpp
View File

@ -913,7 +913,6 @@ namespace storm {
// Finally, we need to scan the ranges of states that agree on the probability. // Finally, we need to scan the ranges of states that agree on the probability.
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator begin = partition.getBegin(block); typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator begin = partition.getBegin(block);
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator current = begin;
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator end = partition.getEnd(block) - 1; typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator end = partition.getEnd(block) - 1;
storm::storage::sparse::state_type currentIndex = block.getBegin(); storm::storage::sparse::state_type currentIndex = block.getBegin();
@ -999,7 +998,6 @@ namespace storm {
// Now we have everything in place to actually split the block by just scanning for ranges of equal label. // Now we have everything in place to actually split the block by just scanning for ranges of equal label.
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator begin = partition.getBegin(block); typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator begin = partition.getBegin(block);
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator current = begin;
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator end = partition.getEnd(block) - 1; typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator end = partition.getEnd(block) - 1;
storm::storage::sparse::state_type currentIndex = block.getBegin(); storm::storage::sparse::state_type currentIndex = block.getBegin();
@ -1093,7 +1091,6 @@ namespace storm {
// Then, we scan for the ranges of states that agree on the probability. // Then, we scan for the ranges of states that agree on the probability.
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator begin = partition.getStatesAndValues().begin() + block.getOriginalBegin(); typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator begin = partition.getStatesAndValues().begin() + block.getOriginalBegin();
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator current = begin;
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator end = partition.getStatesAndValues().begin() + block.getBegin() - 1; typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator end = partition.getStatesAndValues().begin() + block.getBegin() - 1;
storm::storage::sparse::state_type currentIndex = block.getOriginalBegin(); storm::storage::sparse::state_type currentIndex = block.getOriginalBegin();
result.push_back(currentIndex); result.push_back(currentIndex);
@ -1462,7 +1459,6 @@ namespace storm {
// Finally, we need to scan the ranges of states that agree on the probability. // Finally, we need to scan the ranges of states that agree on the probability.
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator begin = partition.getBegin(block); typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator begin = partition.getBegin(block);
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator current = begin;
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator end = partition.getEnd(block) - 1; typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator end = partition.getEnd(block) - 1;
storm::storage::sparse::state_type currentIndex = block.getBegin(); storm::storage::sparse::state_type currentIndex = block.getBegin();

6
src/storage/SparseMatrix.cpp
View File

@ -677,11 +677,12 @@ namespace storm {
SparseMatrix<ValueType> SparseMatrix<ValueType>::transpose(bool joinGroups, bool keepZeros) const { SparseMatrix<ValueType> SparseMatrix<ValueType>::transpose(bool joinGroups, bool keepZeros) const {
index_type rowCount = this->getColumnCount(); index_type rowCount = this->getColumnCount();
index_type columnCount = joinGroups ? this->getRowGroupCount() : this->getRowCount(); index_type columnCount = joinGroups ? this->getRowGroupCount() : this->getRowCount();
index_type entryCount;
if (keepZeros) { if (keepZeros) {
index_type entryCount = this->getEntryCount();
entryCount = this->getEntryCount();
} else { } else {
this->updateNonzeroEntryCount(); this->updateNonzeroEntryCount();
index_type entryCount = this->getNonzeroEntryCount();
entryCount = this->getNonzeroEntryCount();
} }
std::vector<index_type> rowIndications(rowCount + 1); std::vector<index_type> rowIndications(rowCount + 1);
@ -914,7 +915,6 @@ namespace storm {
const_iterator ite; const_iterator ite;
std::vector<index_type>::const_iterator rowIterator = rowIndications.begin(); std::vector<index_type>::const_iterator rowIterator = rowIndications.begin();
typename std::vector<ValueType>::const_iterator bIt = b.begin(); typename std::vector<ValueType>::const_iterator bIt = b.begin();
typename std::vector<ValueType>::const_iterator bIte = b.end();
typename std::vector<ValueType>::iterator resultIterator = x.begin(); typename std::vector<ValueType>::iterator resultIterator = x.begin();
typename std::vector<ValueType>::iterator resultIteratorEnd = x.end(); typename std::vector<ValueType>::iterator resultIteratorEnd = x.end();

64
src/utility/prism.cpp
View File

@ -0,0 +1,64 @@
#include "src/utility/prism.h"
namespace storm {
namespace utility {
namespace prism {
std::map<storm::expressions::Variable, storm::expressions::Expression> parseConstantDefinitionString(storm::prism::Program const& program, std::string const& constantDefinitionString) {
std::map<storm::expressions::Variable, storm::expressions::Expression> constantDefinitions;
std::set<storm::expressions::Variable> definedConstants;
if (!constantDefinitionString.empty()) {
// Parse the string that defines the undefined constants of the model and make sure that it contains exactly
// one value for each undefined constant of the model.
std::vector<std::string> definitions;
boost::split(definitions, constantDefinitionString, boost::is_any_of(","));
for (auto& definition : definitions) {
boost::trim(definition);
// Check whether the token could be a legal constant definition.
uint_fast64_t positionOfAssignmentOperator = definition.find('=');
if (positionOfAssignmentOperator == std::string::npos) {
throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: syntax error.";
}
// Now extract the variable name and the value from the string.
std::string constantName = definition.substr(0, positionOfAssignmentOperator);
boost::trim(constantName);
std::string value = definition.substr(positionOfAssignmentOperator + 1);
boost::trim(value);
// Check whether the constant is a legal undefined constant of the program and if so, of what type it is.
if (program.hasConstant(constantName)) {
// Get the actual constant and check whether it's in fact undefined.
auto const& constant = program.getConstant(constantName);
storm::expressions::Variable variable = constant.getExpressionVariable();
STORM_LOG_THROW(!constant.isDefined(), storm::exceptions::InvalidArgumentException, "Illegally trying to define already defined constant '" << constantName <<"'.");
STORM_LOG_THROW(definedConstants.find(variable) == definedConstants.end(), storm::exceptions::InvalidArgumentException, "Illegally trying to define constant '" << constantName <<"' twice.");
definedConstants.insert(variable);
if (constant.getType().isBooleanType()) {
if (value == "true") {
constantDefinitions[variable] = program.getManager().boolean(true);
} else if (value == "false") {
constantDefinitions[variable] = program.getManager().boolean(false);
} else {
throw storm::exceptions::InvalidArgumentException() << "Illegal value for boolean constant: " << value << ".";
}
} else if (constant.getType().isIntegerType()) {
int_fast64_t integerValue = std::stoi(value);
constantDefinitions[variable] = program.getManager().integer(integerValue);
} else if (constant.getType().isRationalType()) {
double doubleValue = std::stod(value);
constantDefinitions[variable] = program.getManager().rational(doubleValue);
}
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal constant definition string: unknown undefined constant " << constantName << ".");
}
}
}
return constantDefinitions;
}
}
}
}

56
src/utility/prism.h
View File

@ -176,62 +176,8 @@ namespace storm {
std::shared_ptr<boost::container::flat_set<uint_fast64_t>> choiceLabels; std::shared_ptr<boost::container::flat_set<uint_fast64_t>> choiceLabels;
}; };
static std::map<storm::expressions::Variable, storm::expressions::Expression> parseConstantDefinitionString(storm::prism::Program const& program, std::string const& constantDefinitionString) {
std::map<storm::expressions::Variable, storm::expressions::Expression> constantDefinitions;
std::set<storm::expressions::Variable> definedConstants;
if (!constantDefinitionString.empty()) {
// Parse the string that defines the undefined constants of the model and make sure that it contains exactly
// one value for each undefined constant of the model.
std::vector<std::string> definitions;
boost::split(definitions, constantDefinitionString, boost::is_any_of(","));
for (auto& definition : definitions) {
boost::trim(definition);
// Check whether the token could be a legal constant definition.
uint_fast64_t positionOfAssignmentOperator = definition.find('=');
if (positionOfAssignmentOperator == std::string::npos) {
throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: syntax error.";
}
// Now extract the variable name and the value from the string.
std::string constantName = definition.substr(0, positionOfAssignmentOperator);
boost::trim(constantName);
std::string value = definition.substr(positionOfAssignmentOperator + 1);
boost::trim(value);
// Check whether the constant is a legal undefined constant of the program and if so, of what type it is.
if (program.hasConstant(constantName)) {
// Get the actual constant and check whether it's in fact undefined.
auto const& constant = program.getConstant(constantName);
storm::expressions::Variable variable = constant.getExpressionVariable();
STORM_LOG_THROW(!constant.isDefined(), storm::exceptions::InvalidArgumentException, "Illegally trying to define already defined constant '" << constantName <<"'.");
STORM_LOG_THROW(definedConstants.find(variable) == definedConstants.end(), storm::exceptions::InvalidArgumentException, "Illegally trying to define constant '" << constantName <<"' twice.");
definedConstants.insert(variable);
if (constant.getType().isBooleanType()) {
if (value == "true") {
constantDefinitions[variable] = program.getManager().boolean(true);
} else if (value == "false") {
constantDefinitions[variable] = program.getManager().boolean(false);
} else {
throw storm::exceptions::InvalidArgumentException() << "Illegal value for boolean constant: " << value << ".";
}
} else if (constant.getType().isIntegerType()) {
int_fast64_t integerValue = std::stoi(value);
constantDefinitions[variable] = program.getManager().integer(integerValue);
} else if (constant.getType().isRationalType()) {
double doubleValue = std::stod(value);
constantDefinitions[variable] = program.getManager().rational(doubleValue);
}
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal constant definition string: unknown undefined constant " << constantName << ".");
}
}
}
std::map<storm::expressions::Variable, storm::expressions::Expression> parseConstantDefinitionString(storm::prism::Program const& program, std::string const& constantDefinitionString);
return constantDefinitions;
}
} // namespace prism } // namespace prism
} // namespace utility } // namespace utility
} // namespace storm } // namespace storm

6
test/functional/parser/DeterministicSparseTransitionParserTest.cpp
View File

@ -106,8 +106,8 @@ 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); 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(8, rewardMatrix.getColumnCount());
ASSERT_EQ(17, rewardMatrix.getEntryCount());
ASSERT_EQ(8ul, rewardMatrix.getColumnCount());
ASSERT_EQ(17ul, rewardMatrix.getEntryCount());
// Test every entry of the matrix. // Test every entry of the matrix.
storm::storage::SparseMatrix<double>::const_iterator cIter = rewardMatrix.begin(0); storm::storage::SparseMatrix<double>::const_iterator cIter = rewardMatrix.begin(0);
@ -197,7 +197,7 @@ TEST(DeterministicSparseTransitionParserTest, FixDeadlocks) {
storm::storage::SparseMatrix<double> transitionMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_deadlock.tra"); storm::storage::SparseMatrix<double> transitionMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_deadlock.tra");
ASSERT_EQ(9ul, transitionMatrix.getColumnCount()); ASSERT_EQ(9ul, transitionMatrix.getColumnCount());
ASSERT_EQ(23, transitionMatrix.getEntryCount());
ASSERT_EQ(23ul, transitionMatrix.getEntryCount());
storm::storage::SparseMatrix<double>::const_iterator cIter = transitionMatrix.begin(7); storm::storage::SparseMatrix<double>::const_iterator cIter = transitionMatrix.begin(7);
ASSERT_EQ(7ul, cIter->getColumn()); ASSERT_EQ(7ul, cIter->getColumn());

14
test/functional/parser/NondeterministicModelParserTest.cpp
View File

@ -15,15 +15,15 @@ TEST(NondeterministicModelParserTest, BasicMdpParsing) {
// Parse a Mdp and check the result. // Parse a Mdp and check the result.
storm::models::sparse::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")); storm::models::sparse::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(6, mdp.getNumberOfStates());
ASSERT_EQ(22, mdp.getNumberOfTransitions());
ASSERT_EQ(11, mdp.getNumberOfChoices());
ASSERT_EQ(6ul, mdp.getNumberOfStates());
ASSERT_EQ(22ul, mdp.getNumberOfTransitions());
ASSERT_EQ(11ul, mdp.getNumberOfChoices());
ASSERT_EQ(2, mdp.getInitialStates().getNumberOfSetBits());
ASSERT_EQ(2ul, mdp.getInitialStates().getNumberOfSetBits());
ASSERT_TRUE(mdp.getInitialStates().get(0)); ASSERT_TRUE(mdp.getInitialStates().get(0));
ASSERT_TRUE(mdp.getInitialStates().get(4)); ASSERT_TRUE(mdp.getInitialStates().get(4));
ASSERT_EQ(4, mdp.getStateLabeling().getNumberOfLabels());
ASSERT_EQ(3, mdp.getLabelsOfState(0).size());
ASSERT_EQ(4ul, mdp.getStateLabeling().getNumberOfLabels());
ASSERT_EQ(3ul, mdp.getLabelsOfState(0).size());
ASSERT_TRUE(mdp.hasStateRewards()); ASSERT_TRUE(mdp.hasStateRewards());
ASSERT_EQ(0, mdp.getStateRewardVector()[0]); ASSERT_EQ(0, mdp.getStateRewardVector()[0]);
@ -35,7 +35,7 @@ TEST(NondeterministicModelParserTest, BasicMdpParsing) {
ASSERT_EQ(158.32, rewardSum); ASSERT_EQ(158.32, rewardSum);
ASSERT_TRUE(mdp.hasTransitionRewards()); ASSERT_TRUE(mdp.hasTransitionRewards());
ASSERT_EQ(17, mdp.getTransitionRewardMatrix().getEntryCount());
ASSERT_EQ(17ul, mdp.getTransitionRewardMatrix().getEntryCount());
rewardSum = 0; rewardSum = 0;
for(uint_fast64_t i = 0; i < mdp.getTransitionRewardMatrix().getRowCount(); i++) { for(uint_fast64_t i = 0; i < mdp.getTransitionRewardMatrix().getRowCount(); i++) {
rewardSum += mdp.getTransitionRewardMatrix().getRowSum(i); rewardSum += mdp.getTransitionRewardMatrix().getRowSum(i);

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

@ -30,88 +30,88 @@ TEST(NondeterministicSparseTransitionParserTest, BasicTransitionsParsing) {
storm::storage::SparseMatrix<double> 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(6, result.getRowGroupCount());
ASSERT_EQ(7, result.getRowGroupIndices().size());
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]);
ASSERT_EQ(6ul, result.getRowGroupCount());
ASSERT_EQ(7ul, result.getRowGroupIndices().size());
ASSERT_EQ(0ul, result.getRowGroupIndices()[0]);
ASSERT_EQ(4ul, result.getRowGroupIndices()[1]);
ASSERT_EQ(5ul, result.getRowGroupIndices()[2]);
ASSERT_EQ(7ul, result.getRowGroupIndices()[3]);
ASSERT_EQ(8ul, result.getRowGroupIndices()[4]);
ASSERT_EQ(9ul, result.getRowGroupIndices()[5]);
ASSERT_EQ(11ul, result.getRowGroupIndices()[6]);
// Test the transition matrix. // Test the transition matrix.
ASSERT_EQ(6, result.getColumnCount());
ASSERT_EQ(11, result.getRowCount());
ASSERT_EQ(22, result.getEntryCount());
ASSERT_EQ(6ul, result.getColumnCount());
ASSERT_EQ(11ul, result.getRowCount());
ASSERT_EQ(22ul, result.getEntryCount());
// Test every entry of the matrix. // Test every entry of the matrix.
storm::storage::SparseMatrix<double>::const_iterator cIter = result.begin(0); storm::storage::SparseMatrix<double>::const_iterator cIter = result.begin(0);
ASSERT_EQ(0, cIter->getColumn());
ASSERT_EQ(0ul, cIter->getColumn());
ASSERT_EQ(0.9, cIter->getValue()); ASSERT_EQ(0.9, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(1, cIter->getColumn());
ASSERT_EQ(1ul, cIter->getColumn());
ASSERT_EQ(0.1, cIter->getValue()); ASSERT_EQ(0.1, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(1, cIter->getColumn());
ASSERT_EQ(1ul, cIter->getColumn());
ASSERT_EQ(0.2, cIter->getValue()); ASSERT_EQ(0.2, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(2, cIter->getColumn());
ASSERT_EQ(2ul, cIter->getColumn());
ASSERT_EQ(0.2, cIter->getValue()); ASSERT_EQ(0.2, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(3, cIter->getColumn());
ASSERT_EQ(3ul, cIter->getColumn());
ASSERT_EQ(0.2, cIter->getValue()); ASSERT_EQ(0.2, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(4, cIter->getColumn());
ASSERT_EQ(4ul, cIter->getColumn());
ASSERT_EQ(0.2, cIter->getValue()); ASSERT_EQ(0.2, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(5, cIter->getColumn());
ASSERT_EQ(5ul, cIter->getColumn());
ASSERT_EQ(0.2, cIter->getValue()); ASSERT_EQ(0.2, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(5, cIter->getColumn());
ASSERT_EQ(5ul, cIter->getColumn());
ASSERT_EQ(1, cIter->getValue()); ASSERT_EQ(1, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(0, cIter->getColumn());
ASSERT_EQ(0ul, cIter->getColumn());
ASSERT_EQ(0.1, cIter->getValue()); ASSERT_EQ(0.1, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(4, cIter->getColumn());
ASSERT_EQ(4ul, cIter->getColumn());
ASSERT_EQ(0.9, cIter->getValue()); ASSERT_EQ(0.9, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(2, cIter->getColumn());
ASSERT_EQ(2ul, cIter->getColumn());
ASSERT_EQ(1, cIter->getValue()); ASSERT_EQ(1, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(2, cIter->getColumn());
ASSERT_EQ(2ul, cIter->getColumn());
ASSERT_EQ(0.5, cIter->getValue()); ASSERT_EQ(0.5, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(3, cIter->getColumn());
ASSERT_EQ(3ul, cIter->getColumn());
ASSERT_EQ(0.5, cIter->getValue()); ASSERT_EQ(0.5, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(2, cIter->getColumn());
ASSERT_EQ(2ul, cIter->getColumn());
ASSERT_EQ(1, cIter->getValue()); ASSERT_EQ(1, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(2, cIter->getColumn());
ASSERT_EQ(2ul, cIter->getColumn());
ASSERT_EQ(0.001, cIter->getValue()); ASSERT_EQ(0.001, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(3, cIter->getColumn());
ASSERT_EQ(3ul, cIter->getColumn());
ASSERT_EQ(0.999, cIter->getValue()); ASSERT_EQ(0.999, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(1, cIter->getColumn());
ASSERT_EQ(1ul, cIter->getColumn());
ASSERT_EQ(0.7, cIter->getValue()); ASSERT_EQ(0.7, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(4, cIter->getColumn());
ASSERT_EQ(4ul, cIter->getColumn());
ASSERT_EQ(0.3, cIter->getValue()); ASSERT_EQ(0.3, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(1, cIter->getColumn());
ASSERT_EQ(1ul, cIter->getColumn());
ASSERT_EQ(0.2, cIter->getValue()); ASSERT_EQ(0.2, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(4, cIter->getColumn());
ASSERT_EQ(4ul, cIter->getColumn());
ASSERT_EQ(0.2, cIter->getValue()); ASSERT_EQ(0.2, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(5, cIter->getColumn());
ASSERT_EQ(5ul, cIter->getColumn());
ASSERT_EQ(0.6, cIter->getValue()); ASSERT_EQ(0.6, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(5, cIter->getColumn());
ASSERT_EQ(5ul, cIter->getColumn());
ASSERT_EQ(1, cIter->getValue()); ASSERT_EQ(1, cIter->getValue());
} }
@ -121,62 +121,62 @@ 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)); 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(6, result.getColumnCount());
ASSERT_EQ(11, result.getRowCount());
ASSERT_EQ(17, result.getEntryCount());
ASSERT_EQ(6ul, result.getColumnCount());
ASSERT_EQ(11ul, result.getRowCount());
ASSERT_EQ(17ul, result.getEntryCount());
// Test every entry of the matrix. // Test every entry of the matrix.
storm::storage::SparseMatrix<double>::const_iterator cIter = result.begin(0); storm::storage::SparseMatrix<double>::const_iterator cIter = result.begin(0);
ASSERT_EQ(0, cIter->getColumn());
ASSERT_EQ(0ul, cIter->getColumn());
ASSERT_EQ(1, cIter->getValue()); ASSERT_EQ(1, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(1, cIter->getColumn());
ASSERT_EQ(1ul, cIter->getColumn());
ASSERT_EQ(30, cIter->getValue()); ASSERT_EQ(30, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(1, cIter->getColumn());
ASSERT_EQ(1ul, cIter->getColumn());
ASSERT_EQ(15.2, cIter->getValue()); ASSERT_EQ(15.2, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(2, cIter->getColumn());
ASSERT_EQ(2ul, cIter->getColumn());
ASSERT_EQ(75, cIter->getValue()); ASSERT_EQ(75, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(5, cIter->getColumn());
ASSERT_EQ(5ul, cIter->getColumn());
ASSERT_EQ(2.45, cIter->getValue()); ASSERT_EQ(2.45, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(5, cIter->getColumn());
ASSERT_EQ(5ul, cIter->getColumn());
ASSERT_EQ(1, cIter->getValue()); ASSERT_EQ(1, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(0, cIter->getColumn());
ASSERT_EQ(0ul, cIter->getColumn());
ASSERT_EQ(0.114, cIter->getValue()); ASSERT_EQ(0.114, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(4, cIter->getColumn());
ASSERT_EQ(4ul, cIter->getColumn());
ASSERT_EQ(90, cIter->getValue()); ASSERT_EQ(90, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(2, cIter->getColumn());
ASSERT_EQ(2ul, cIter->getColumn());
ASSERT_EQ(1, cIter->getValue()); ASSERT_EQ(1, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(2, cIter->getColumn());
ASSERT_EQ(2ul, cIter->getColumn());
ASSERT_EQ(55, cIter->getValue()); ASSERT_EQ(55, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(3, cIter->getColumn());
ASSERT_EQ(3ul, cIter->getColumn());
ASSERT_EQ(87, cIter->getValue()); ASSERT_EQ(87, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(2, cIter->getColumn());
ASSERT_EQ(2ul, cIter->getColumn());
ASSERT_EQ(13, cIter->getValue()); ASSERT_EQ(13, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(3, cIter->getColumn());
ASSERT_EQ(3ul, cIter->getColumn());
ASSERT_EQ(999, cIter->getValue()); ASSERT_EQ(999, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(1, cIter->getColumn());
ASSERT_EQ(1ul, cIter->getColumn());
ASSERT_EQ(0.7, cIter->getValue()); ASSERT_EQ(0.7, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(4, cIter->getColumn());
ASSERT_EQ(4ul, cIter->getColumn());
ASSERT_EQ(0.3, cIter->getValue()); ASSERT_EQ(0.3, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(1, cIter->getColumn());
ASSERT_EQ(1ul, cIter->getColumn());
ASSERT_EQ(0.1, cIter->getValue()); ASSERT_EQ(0.1, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(5, cIter->getColumn());
ASSERT_EQ(5ul, cIter->getColumn());
ASSERT_EQ(6, cIter->getValue()); ASSERT_EQ(6, cIter->getValue());
} }
@ -213,36 +213,36 @@ TEST(NondeterministicSparseTransitionParserTest, FixDeadlocks) {
// 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::storage::SparseMatrix<double> 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(8, result.getRowGroupIndices().size());
ASSERT_EQ(9, result.getRowGroupIndices()[5]);
ASSERT_EQ(10, result.getRowGroupIndices()[6]);
ASSERT_EQ(12, result.getRowGroupIndices()[7]);
ASSERT_EQ(8ul, result.getRowGroupIndices().size());
ASSERT_EQ(9ul, result.getRowGroupIndices()[5]);
ASSERT_EQ(10ul, result.getRowGroupIndices()[6]);
ASSERT_EQ(12ul, result.getRowGroupIndices()[7]);
ASSERT_EQ(7, result.getColumnCount());
ASSERT_EQ(12, result.getRowCount());
ASSERT_EQ(23, result.getEntryCount());
ASSERT_EQ(7ul, result.getColumnCount());
ASSERT_EQ(12ul, result.getRowCount());
ASSERT_EQ(23ul, result.getEntryCount());
storm::storage::SparseMatrix<double>::const_iterator cIter = result.begin(8); storm::storage::SparseMatrix<double>::const_iterator cIter = result.begin(8);
ASSERT_EQ(1, cIter->getColumn());
ASSERT_EQ(1ul, cIter->getColumn());
ASSERT_EQ(0.7, cIter->getValue()); ASSERT_EQ(0.7, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(4, cIter->getColumn());
ASSERT_EQ(4ul, cIter->getColumn());
ASSERT_EQ(0.3, cIter->getValue()); ASSERT_EQ(0.3, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(5, cIter->getColumn());
ASSERT_EQ(5ul, cIter->getColumn());
ASSERT_EQ(1, cIter->getValue()); ASSERT_EQ(1, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(1, cIter->getColumn());
ASSERT_EQ(1ul, cIter->getColumn());
ASSERT_EQ(0.2, cIter->getValue()); ASSERT_EQ(0.2, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(4, cIter->getColumn());
ASSERT_EQ(4ul, cIter->getColumn());
ASSERT_EQ(0.2, cIter->getValue()); ASSERT_EQ(0.2, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(5, cIter->getColumn());
ASSERT_EQ(5ul, cIter->getColumn());
ASSERT_EQ(0.6, cIter->getValue()); ASSERT_EQ(0.6, cIter->getValue());
cIter++; cIter++;
ASSERT_EQ(5, cIter->getColumn());
ASSERT_EQ(5ul, cIter->getColumn());
ASSERT_EQ(1, cIter->getValue()); ASSERT_EQ(1, cIter->getValue());
} }

2
test/functional/parser/PrismParserTest.cpp
View File

@ -27,7 +27,7 @@ TEST(PrismParser, SimpleTest) {
storm::prism::Program result; storm::prism::Program result;
EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile")); EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"));
EXPECT_EQ(1, result.getNumberOfModules());
EXPECT_EQ(1ul, result.getNumberOfModules());
EXPECT_EQ(storm::prism::Program::ModelType::DTMC, result.getModelType()); EXPECT_EQ(storm::prism::Program::ModelType::DTMC, result.getModelType());
testInput = testInput =

10
test/functional/storage/BitVectorTest.cpp
View File

@ -455,7 +455,7 @@ TEST(BitVectorTest, NumberOfSetBitsBeforeIndex) {
vector.set(i, i % 2 == 0); vector.set(i, i % 2 == 0);
} }
ASSERT_EQ(7, vector.getNumberOfSetBitsBeforeIndex(14));
ASSERT_EQ(7ul, vector.getNumberOfSetBitsBeforeIndex(14));
} }
TEST(BitVectorTest, BeginEnd) { TEST(BitVectorTest, BeginEnd) {
@ -478,10 +478,10 @@ TEST(BitVectorTest, NextSetIndex) {
vector.set(14); vector.set(14);
vector.set(17); vector.set(17);
ASSERT_EQ(14, vector.getNextSetIndex(14));
ASSERT_EQ(17, vector.getNextSetIndex(15));
ASSERT_EQ(17, vector.getNextSetIndex(16));
ASSERT_EQ(17, vector.getNextSetIndex(17));
ASSERT_EQ(14ul, vector.getNextSetIndex(14));
ASSERT_EQ(17ul, vector.getNextSetIndex(15));
ASSERT_EQ(17ul, vector.getNextSetIndex(16));
ASSERT_EQ(17ul, vector.getNextSetIndex(17));
ASSERT_EQ(vector.size(), vector.getNextSetIndex(18)); ASSERT_EQ(vector.size(), vector.getNextSetIndex(18));
} }

110
test/functional/storage/CuddDdTest.cpp
View File

@ -11,27 +11,27 @@ TEST(CuddDdManager, Constants) {
storm::dd::Add<storm::dd::DdType::CUDD> zero; storm::dd::Add<storm::dd::DdType::CUDD> zero;
ASSERT_NO_THROW(zero = manager->getAddZero()); ASSERT_NO_THROW(zero = manager->getAddZero());
EXPECT_EQ(0, zero.getNonZeroCount());
EXPECT_EQ(1, zero.getLeafCount());
EXPECT_EQ(1, zero.getNodeCount());
EXPECT_EQ(0ul, zero.getNonZeroCount());
EXPECT_EQ(1ul, zero.getLeafCount());
EXPECT_EQ(1ul, zero.getNodeCount());
EXPECT_EQ(0, zero.getMin()); EXPECT_EQ(0, zero.getMin());
EXPECT_EQ(0, zero.getMax()); EXPECT_EQ(0, zero.getMax());
storm::dd::Add<storm::dd::DdType::CUDD> one; storm::dd::Add<storm::dd::DdType::CUDD> one;
ASSERT_NO_THROW(one = manager->getAddOne()); ASSERT_NO_THROW(one = manager->getAddOne());
EXPECT_EQ(1, one.getNonZeroCount());
EXPECT_EQ(1, one.getLeafCount());
EXPECT_EQ(1, one.getNodeCount());
EXPECT_EQ(1ul, one.getNonZeroCount());
EXPECT_EQ(1ul, one.getLeafCount());
EXPECT_EQ(1ul, one.getNodeCount());
EXPECT_EQ(1, one.getMin()); EXPECT_EQ(1, one.getMin());
EXPECT_EQ(1, one.getMax()); EXPECT_EQ(1, one.getMax());
storm::dd::Add<storm::dd::DdType::CUDD> two; storm::dd::Add<storm::dd::DdType::CUDD> two;
ASSERT_NO_THROW(two = manager->getConstant(2)); ASSERT_NO_THROW(two = manager->getConstant(2));
EXPECT_EQ(1, two.getNonZeroCount());
EXPECT_EQ(1, two.getLeafCount());
EXPECT_EQ(1, two.getNodeCount());
EXPECT_EQ(1ul, two.getNonZeroCount());
EXPECT_EQ(1ul, two.getLeafCount());
EXPECT_EQ(1ul, two.getNodeCount());
EXPECT_EQ(2, two.getMin()); EXPECT_EQ(2, two.getMin());
EXPECT_EQ(2, two.getMax()); EXPECT_EQ(2, two.getMax());
} }
@ -39,12 +39,12 @@ TEST(CuddDdManager, Constants) {
TEST(CuddDdManager, AddGetMetaVariableTest) { TEST(CuddDdManager, AddGetMetaVariableTest) {
std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>()); std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9)); ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9));
EXPECT_EQ(2, manager->getNumberOfMetaVariables());
EXPECT_EQ(2ul, manager->getNumberOfMetaVariables());
ASSERT_THROW(manager->addMetaVariable("x", 0, 3), storm::exceptions::InvalidArgumentException); ASSERT_THROW(manager->addMetaVariable("x", 0, 3), storm::exceptions::InvalidArgumentException);
ASSERT_NO_THROW(manager->addMetaVariable("y", 0, 3)); ASSERT_NO_THROW(manager->addMetaVariable("y", 0, 3));
EXPECT_EQ(4, manager->getNumberOfMetaVariables());
EXPECT_EQ(4ul, manager->getNumberOfMetaVariables());
EXPECT_TRUE(manager->hasMetaVariable("x'")); EXPECT_TRUE(manager->hasMetaVariable("x'"));
EXPECT_TRUE(manager->hasMetaVariable("y'")); EXPECT_TRUE(manager->hasMetaVariable("y'"));
@ -61,16 +61,16 @@ TEST(CuddDdManager, EncodingTest) {
ASSERT_THROW(encoding = manager->getEncoding(x.first, 0), storm::exceptions::InvalidArgumentException); ASSERT_THROW(encoding = manager->getEncoding(x.first, 0), storm::exceptions::InvalidArgumentException);
ASSERT_THROW(encoding = manager->getEncoding(x.first, 10), storm::exceptions::InvalidArgumentException); ASSERT_THROW(encoding = manager->getEncoding(x.first, 10), storm::exceptions::InvalidArgumentException);
ASSERT_NO_THROW(encoding = manager->getEncoding(x.first, 4)); ASSERT_NO_THROW(encoding = manager->getEncoding(x.first, 4));
EXPECT_EQ(1, encoding.getNonZeroCount());
EXPECT_EQ(1ul, encoding.getNonZeroCount());
// As a BDD, this DD has one only leaf, because there does not exist a 0-leaf, and (consequently) one node less // As a BDD, this DD has one only leaf, because there does not exist a 0-leaf, and (consequently) one node less
// than the MTBDD. // than the MTBDD.
EXPECT_EQ(5, encoding.getNodeCount());
EXPECT_EQ(1, encoding.getLeafCount());
EXPECT_EQ(5ul, encoding.getNodeCount());
EXPECT_EQ(1ul, encoding.getLeafCount());
// As an MTBDD, the 0-leaf is there, so the count is actually 2 and the node count is 6. // As an MTBDD, the 0-leaf is there, so the count is actually 2 and the node count is 6.
EXPECT_EQ(6, encoding.toAdd().getNodeCount());
EXPECT_EQ(2, encoding.toAdd().getLeafCount());
EXPECT_EQ(6ul, encoding.toAdd().getNodeCount());
EXPECT_EQ(2ul, encoding.toAdd().getLeafCount());
} }
TEST(CuddDdManager, RangeTest) { TEST(CuddDdManager, RangeTest) {
@ -81,9 +81,9 @@ TEST(CuddDdManager, RangeTest) {
storm::dd::Bdd<storm::dd::DdType::CUDD> range; storm::dd::Bdd<storm::dd::DdType::CUDD> range;
ASSERT_NO_THROW(range = manager->getRange(x.first)); ASSERT_NO_THROW(range = manager->getRange(x.first));
EXPECT_EQ(9, range.getNonZeroCount());
EXPECT_EQ(1, range.getLeafCount());
EXPECT_EQ(5, range.getNodeCount());
EXPECT_EQ(9ul, range.getNonZeroCount());
EXPECT_EQ(1ul, range.getLeafCount());
EXPECT_EQ(5ul, range.getNodeCount());
} }
TEST(CuddDdManager, IdentityTest) { TEST(CuddDdManager, IdentityTest) {
@ -93,9 +93,9 @@ TEST(CuddDdManager, IdentityTest) {
storm::dd::Add<storm::dd::DdType::CUDD> identity; storm::dd::Add<storm::dd::DdType::CUDD> identity;
ASSERT_NO_THROW(identity = manager->getIdentity(x.first)); ASSERT_NO_THROW(identity = manager->getIdentity(x.first));
EXPECT_EQ(9, identity.getNonZeroCount());
EXPECT_EQ(10, identity.getLeafCount());
EXPECT_EQ(21, identity.getNodeCount());
EXPECT_EQ(9ul, identity.getNonZeroCount());
EXPECT_EQ(10ul, identity.getLeafCount());
EXPECT_EQ(21ul, identity.getNodeCount());
} }
TEST(CuddDd, OperatorTest) { TEST(CuddDd, OperatorTest) {
@ -143,26 +143,26 @@ TEST(CuddDd, OperatorTest) {
dd2 = manager->getConstant(5); dd2 = manager->getConstant(5);
dd3 = dd1.equals(dd2); dd3 = dd1.equals(dd2);
EXPECT_EQ(1, dd3.getNonZeroCount());
EXPECT_EQ(1ul, dd3.getNonZeroCount());
storm::dd::Add<storm::dd::DdType::CUDD> dd4 = dd1.notEquals(dd2); storm::dd::Add<storm::dd::DdType::CUDD> dd4 = dd1.notEquals(dd2);
EXPECT_TRUE(dd4.toBdd() == !dd3.toBdd()); EXPECT_TRUE(dd4.toBdd() == !dd3.toBdd());
dd3 = dd1.less(dd2); dd3 = dd1.less(dd2);
EXPECT_EQ(11, dd3.getNonZeroCount());
EXPECT_EQ(11ul, dd3.getNonZeroCount());
dd3 = dd1.lessOrEqual(dd2); dd3 = dd1.lessOrEqual(dd2);
EXPECT_EQ(12, dd3.getNonZeroCount());
EXPECT_EQ(12ul, dd3.getNonZeroCount());
dd3 = dd1.greater(dd2); dd3 = dd1.greater(dd2);
EXPECT_EQ(4, dd3.getNonZeroCount());
EXPECT_EQ(4ul, dd3.getNonZeroCount());
dd3 = dd1.greaterOrEqual(dd2); dd3 = dd1.greaterOrEqual(dd2);
EXPECT_EQ(5, dd3.getNonZeroCount());
EXPECT_EQ(5ul, dd3.getNonZeroCount());
dd3 = (manager->getEncoding(x.first, 2).toAdd()).ite(dd2, dd1); dd3 = (manager->getEncoding(x.first, 2).toAdd()).ite(dd2, dd1);
dd4 = dd3.less(dd2); dd4 = dd3.less(dd2);
EXPECT_EQ(10, dd4.getNonZeroCount());
EXPECT_EQ(10ul, dd4.getNonZeroCount());
dd4 = dd3.minimum(dd1); dd4 = dd3.minimum(dd1);
dd4 *= manager->getEncoding(x.first, 2).toAdd(); dd4 *= manager->getEncoding(x.first, 2).toAdd();
@ -191,15 +191,15 @@ TEST(CuddDd, AbstractionTest) {
dd2 = manager->getConstant(5); dd2 = manager->getConstant(5);
dd3 = dd1.equals(dd2); dd3 = dd1.equals(dd2);
storm::dd::Bdd<storm::dd::DdType::CUDD> dd3Bdd = dd3.toBdd(); storm::dd::Bdd<storm::dd::DdType::CUDD> dd3Bdd = dd3.toBdd();
EXPECT_EQ(1, dd3Bdd.getNonZeroCount());
EXPECT_EQ(1ul, dd3Bdd.getNonZeroCount());
ASSERT_THROW(dd3Bdd = dd3Bdd.existsAbstract({x.second}), storm::exceptions::InvalidArgumentException); ASSERT_THROW(dd3Bdd = dd3Bdd.existsAbstract({x.second}), storm::exceptions::InvalidArgumentException);
ASSERT_NO_THROW(dd3Bdd = dd3Bdd.existsAbstract({x.first})); ASSERT_NO_THROW(dd3Bdd = dd3Bdd.existsAbstract({x.first}));
EXPECT_EQ(1, dd3Bdd.getNonZeroCount());
EXPECT_EQ(1ul, dd3Bdd.getNonZeroCount());
EXPECT_EQ(1, dd3Bdd.toAdd().getMax()); EXPECT_EQ(1, dd3Bdd.toAdd().getMax());
dd3 = dd1.equals(dd2); dd3 = dd1.equals(dd2);
dd3 *= manager->getConstant(3); dd3 *= manager->getConstant(3);
EXPECT_EQ(1, dd3.getNonZeroCount());
EXPECT_EQ(1ul, dd3.getNonZeroCount());
ASSERT_THROW(dd3Bdd = dd3.toBdd().existsAbstract({x.second}), storm::exceptions::InvalidArgumentException); ASSERT_THROW(dd3Bdd = dd3.toBdd().existsAbstract({x.second}), storm::exceptions::InvalidArgumentException);
ASSERT_NO_THROW(dd3Bdd = dd3.toBdd().existsAbstract({x.first})); ASSERT_NO_THROW(dd3Bdd = dd3.toBdd().existsAbstract({x.first}));
EXPECT_TRUE(dd3Bdd.isOne()); EXPECT_TRUE(dd3Bdd.isOne());
@ -208,21 +208,21 @@ TEST(CuddDd, AbstractionTest) {
dd3 *= manager->getConstant(3); dd3 *= manager->getConstant(3);
ASSERT_THROW(dd3 = dd3.sumAbstract({x.second}), storm::exceptions::InvalidArgumentException); ASSERT_THROW(dd3 = dd3.sumAbstract({x.second}), storm::exceptions::InvalidArgumentException);
ASSERT_NO_THROW(dd3 = dd3.sumAbstract({x.first})); ASSERT_NO_THROW(dd3 = dd3.sumAbstract({x.first}));
EXPECT_EQ(1, dd3.getNonZeroCount());
EXPECT_EQ(1ul, dd3.getNonZeroCount());
EXPECT_EQ(3, dd3.getMax()); EXPECT_EQ(3, dd3.getMax());
dd3 = dd1.equals(dd2); dd3 = dd1.equals(dd2);
dd3 *= manager->getConstant(3); dd3 *= manager->getConstant(3);
ASSERT_THROW(dd3 = dd3.minAbstract({x.second}), storm::exceptions::InvalidArgumentException); ASSERT_THROW(dd3 = dd3.minAbstract({x.second}), storm::exceptions::InvalidArgumentException);
ASSERT_NO_THROW(dd3 = dd3.minAbstract({x.first})); ASSERT_NO_THROW(dd3 = dd3.minAbstract({x.first}));
EXPECT_EQ(0, dd3.getNonZeroCount());
EXPECT_EQ(0ul, dd3.getNonZeroCount());
EXPECT_EQ(0, dd3.getMax()); EXPECT_EQ(0, dd3.getMax());
dd3 = dd1.equals(dd2); dd3 = dd1.equals(dd2);
dd3 *= manager->getConstant(3); dd3 *= manager->getConstant(3);
ASSERT_THROW(dd3 = dd3.maxAbstract({x.second}), storm::exceptions::InvalidArgumentException); ASSERT_THROW(dd3 = dd3.maxAbstract({x.second}), storm::exceptions::InvalidArgumentException);
ASSERT_NO_THROW(dd3 = dd3.maxAbstract({x.first})); ASSERT_NO_THROW(dd3 = dd3.maxAbstract({x.first}));
EXPECT_EQ(1, dd3.getNonZeroCount());
EXPECT_EQ(1ul, dd3.getNonZeroCount());
EXPECT_EQ(3, dd3.getMax()); EXPECT_EQ(3, dd3.getMax());
} }
@ -260,7 +260,7 @@ TEST(CuddDd, GetSetValueTest) {
storm::dd::Add<storm::dd::DdType::CUDD> dd1 = manager->getAddOne(); storm::dd::Add<storm::dd::DdType::CUDD> dd1 = manager->getAddOne();
ASSERT_NO_THROW(dd1.setValue(x.first, 4, 2)); ASSERT_NO_THROW(dd1.setValue(x.first, 4, 2));
EXPECT_EQ(2, dd1.getLeafCount());
EXPECT_EQ(2ul, dd1.getLeafCount());
std::map<storm::expressions::Variable, int_fast64_t> metaVariableToValueMap; std::map<storm::expressions::Variable, int_fast64_t> metaVariableToValueMap;
metaVariableToValueMap.emplace(x.first, 1); metaVariableToValueMap.emplace(x.first, 1);
@ -289,7 +289,7 @@ TEST(CuddDd, ForwardIteratorTest) {
ASSERT_NO_THROW(++it); ASSERT_NO_THROW(++it);
++numberOfValuations; ++numberOfValuations;
} }
EXPECT_EQ(9, numberOfValuations);
EXPECT_EQ(9ul, numberOfValuations);
dd = manager->getRange(x.first).toAdd(); dd = manager->getRange(x.first).toAdd();
dd = dd.ite(manager->getAddOne(), manager->getAddOne()); dd = dd.ite(manager->getAddOne(), manager->getAddOne());
@ -301,7 +301,7 @@ TEST(CuddDd, ForwardIteratorTest) {
ASSERT_NO_THROW(++it); ASSERT_NO_THROW(++it);
++numberOfValuations; ++numberOfValuations;
} }
EXPECT_EQ(16, numberOfValuations);
EXPECT_EQ(16ul, numberOfValuations);
ASSERT_NO_THROW(it = dd.begin(false)); ASSERT_NO_THROW(it = dd.begin(false));
ASSERT_NO_THROW(ite = dd.end()); ASSERT_NO_THROW(ite = dd.end());
@ -311,7 +311,7 @@ TEST(CuddDd, ForwardIteratorTest) {
ASSERT_NO_THROW(++it); ASSERT_NO_THROW(++it);
++numberOfValuations; ++numberOfValuations;
} }
EXPECT_EQ(1, numberOfValuations);
EXPECT_EQ(1ul, numberOfValuations);
} }
TEST(CuddDd, AddOddTest) { TEST(CuddDd, AddOddTest) {
@ -322,12 +322,12 @@ TEST(CuddDd, AddOddTest) {
storm::dd::Add<storm::dd::DdType::CUDD> dd = manager->getIdentity(x.first); storm::dd::Add<storm::dd::DdType::CUDD> dd = manager->getIdentity(x.first);
storm::dd::Odd<storm::dd::DdType::CUDD> odd; storm::dd::Odd<storm::dd::DdType::CUDD> odd;
ASSERT_NO_THROW(odd = storm::dd::Odd<storm::dd::DdType::CUDD>(dd)); ASSERT_NO_THROW(odd = storm::dd::Odd<storm::dd::DdType::CUDD>(dd));
EXPECT_EQ(9, odd.getTotalOffset());
EXPECT_EQ(12, odd.getNodeCount());
EXPECT_EQ(9ul, odd.getTotalOffset());
EXPECT_EQ(12ul, odd.getNodeCount());
std::vector<double> ddAsVector; std::vector<double> ddAsVector;
ASSERT_NO_THROW(ddAsVector = dd.toVector<double>()); ASSERT_NO_THROW(ddAsVector = dd.toVector<double>());
EXPECT_EQ(9, ddAsVector.size());
EXPECT_EQ(9ul, ddAsVector.size());
for (uint_fast64_t i = 0; i < ddAsVector.size(); ++i) { for (uint_fast64_t i = 0; i < ddAsVector.size(); ++i) {
EXPECT_TRUE(i+1 == ddAsVector[i]); EXPECT_TRUE(i+1 == ddAsVector[i]);
} }
@ -346,16 +346,16 @@ TEST(CuddDd, AddOddTest) {
storm::storage::SparseMatrix<double> matrix; storm::storage::SparseMatrix<double> matrix;
ASSERT_NO_THROW(matrix = dd.toMatrix({x.first}, {x.second}, rowOdd, columnOdd)); ASSERT_NO_THROW(matrix = dd.toMatrix({x.first}, {x.second}, rowOdd, columnOdd));
EXPECT_EQ(9, matrix.getRowCount());
EXPECT_EQ(9, matrix.getColumnCount());
EXPECT_EQ(25, matrix.getNonzeroEntryCount());
EXPECT_EQ(9ul, matrix.getRowCount());
EXPECT_EQ(9ul, matrix.getColumnCount());
EXPECT_EQ(25ul, matrix.getNonzeroEntryCount());
dd = manager->getRange(x.first).toAdd() * manager->getRange(x.second).toAdd() * manager->getEncoding(a.first, 0).toAdd().ite(dd, dd + manager->getConstant(1)); dd = manager->getRange(x.first).toAdd() * manager->getRange(x.second).toAdd() * manager->getEncoding(a.first, 0).toAdd().ite(dd, dd + manager->getConstant(1));
ASSERT_NO_THROW(matrix = dd.toMatrix({a.first}, rowOdd, columnOdd)); ASSERT_NO_THROW(matrix = dd.toMatrix({a.first}, rowOdd, columnOdd));
EXPECT_EQ(18, matrix.getRowCount());
EXPECT_EQ(9, matrix.getRowGroupCount());
EXPECT_EQ(9, matrix.getColumnCount());
EXPECT_EQ(106, matrix.getNonzeroEntryCount());
EXPECT_EQ(18ul, matrix.getRowCount());
EXPECT_EQ(9ul, matrix.getRowGroupCount());
EXPECT_EQ(9ul, matrix.getColumnCount());
EXPECT_EQ(106ul, matrix.getNonzeroEntryCount());
} }
TEST(CuddDd, BddOddTest) { TEST(CuddDd, BddOddTest) {
@ -393,14 +393,14 @@ TEST(CuddDd, BddOddTest) {
storm::storage::SparseMatrix<double> matrix; storm::storage::SparseMatrix<double> matrix;
ASSERT_NO_THROW(matrix = dd.toMatrix({x.first}, {x.second}, rowOdd, columnOdd)); ASSERT_NO_THROW(matrix = dd.toMatrix({x.first}, {x.second}, rowOdd, columnOdd));
EXPECT_EQ(9, matrix.getRowCount());
EXPECT_EQ(9, matrix.getColumnCount());
EXPECT_EQ(25, matrix.getNonzeroEntryCount());
EXPECT_EQ(9ul, matrix.getRowCount());
EXPECT_EQ(9ul, matrix.getColumnCount());
EXPECT_EQ(25ul, matrix.getNonzeroEntryCount());
dd = manager->getRange(x.first).toAdd() * manager->getRange(x.second).toAdd() * manager->getEncoding(a.first, 0).toAdd().ite(dd, dd + manager->getConstant(1)); dd = manager->getRange(x.first).toAdd() * manager->getRange(x.second).toAdd() * manager->getEncoding(a.first, 0).toAdd().ite(dd, dd + manager->getConstant(1));
ASSERT_NO_THROW(matrix = dd.toMatrix({a.first}, rowOdd, columnOdd)); ASSERT_NO_THROW(matrix = dd.toMatrix({a.first}, rowOdd, columnOdd));
EXPECT_EQ(18, matrix.getRowCount());
EXPECT_EQ(9, matrix.getRowGroupCount());
EXPECT_EQ(9, matrix.getColumnCount());
EXPECT_EQ(106, matrix.getNonzeroEntryCount());
EXPECT_EQ(18ul, matrix.getRowCount());
EXPECT_EQ(9ul, matrix.getRowGroupCount());
EXPECT_EQ(9ul, matrix.getColumnCount());
EXPECT_EQ(106ul, matrix.getNonzeroEntryCount());
} }

2
test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp
View File

@ -62,7 +62,7 @@ TEST(StronglyConnectedComponentDecomposition, FullSystem2) {
storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition; storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*markovAutomaton, true, false)); ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*markovAutomaton, true, false));
ASSERT_EQ(sccDecomposition.size(), 2);
ASSERT_EQ(2ul, sccDecomposition.size());
// Now, because there is no ordering we have to check the contents of the MECs in a symmetrical way. // Now, because there is no ordering we have to check the contents of the MECs in a symmetrical way.
storm::storage::StateBlock const& scc1 = sccDecomposition[0]; storm::storage::StateBlock const& scc1 = sccDecomposition[0];

Write Preview
Loading…
Cancel
Save