Browse Source

Fixed some compiler warnings

tempestpy_adaptions
Matthias Volk 5 years ago
parent
commit
4c1958c245
  1. 3
      src/storm-pars-cli/storm-pars.cpp
  2. 2
      src/storm-pars/analysis/AssumptionChecker.cpp
  3. 6
      src/storm-pars/analysis/MonotonicityChecker.cpp
  4. 12
      src/storm-pars/analysis/Order.cpp
  5. 10
      src/storm-pars/analysis/OrderExtender.cpp
  6. 16
      src/test/storm-pars/analysis/AssumptionCheckerTest.cpp
  7. 8
      src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp
  8. 6
      src/test/storm-pars/analysis/OrderExtenderTest.cpp

3
src/storm-pars-cli/storm-pars.cpp

@ -679,10 +679,9 @@ namespace storm {
storm::storage::BitVector selectedStates(matrix.getRowCount()); storm::storage::BitVector selectedStates(matrix.getRowCount());
storm::storage::BitVector selfLoopStates(matrix.getRowCount()); storm::storage::BitVector selfLoopStates(matrix.getRowCount());
for (auto i = 0; i < decomposition.size(); ++i) {
for (size_t i = 0; i < decomposition.size(); ++i) {
auto scc = decomposition.getBlock(i); auto scc = decomposition.getBlock(i);
if (scc.size() > 1) { if (scc.size() > 1) {
auto nrInitial = 0;
auto statesScc = scc.getStates(); auto statesScc = scc.getStates();
std::vector<uint_fast64_t> entryStates; std::vector<uint_fast64_t> entryStates;
for (auto state : statesScc) { for (auto state : statesScc) {

2
src/storm-pars/analysis/AssumptionChecker.cpp

@ -30,7 +30,7 @@ namespace storm {
auto matrix = model->getTransitionMatrix(); auto matrix = model->getTransitionMatrix();
std::set<typename utility::parametric::VariableType<ValueType>::type> variables = models::sparse::getProbabilityParameters(*model); std::set<typename utility::parametric::VariableType<ValueType>::type> variables = models::sparse::getProbabilityParameters(*model);
for (auto i = 0; i < numberOfSamples; ++i) {
for (uint_fast64_t i = 0; i < numberOfSamples; ++i) {
auto valuation = utility::parametric::Valuation<ValueType>(); auto valuation = utility::parametric::Valuation<ValueType>();
for (auto var: variables) { for (auto var: variables) {
auto lb = region.getLowerBoundary(var.name()); auto lb = region.getLowerBoundary(var.name());

6
src/storm-pars/analysis/MonotonicityChecker.cpp

@ -104,7 +104,7 @@ namespace storm {
} }
} else { } else {
auto i = 0;
size_t i = 0;
for (auto itr = map.begin(); i < map.size() && itr != map.end(); ++itr) { for (auto itr = map.begin(); i < map.size() && itr != map.end(); ++itr) {
auto order = itr->first; auto order = itr->first;
@ -553,7 +553,7 @@ namespace storm {
// Check monotonicity in variable (*itr) by instantiating the model // Check monotonicity in variable (*itr) by instantiating the model
// all other variables fixed on lb, only increasing (*itr) // all other variables fixed on lb, only increasing (*itr)
for (auto i = 0; (monDecr || monIncr) && i < numberOfSamples; ++i) {
for (uint_fast64_t i = 0; (monDecr || monIncr) && i < numberOfSamples; ++i) {
// Create valuation // Create valuation
auto valuation = storm::utility::parametric::Valuation<ValueType>(); auto valuation = storm::utility::parametric::Valuation<ValueType>();
for (auto itr2 = variables.begin(); itr2 != variables.end(); ++itr2) { for (auto itr2 = variables.begin(); itr2 != variables.end(); ++itr2) {
@ -629,7 +629,7 @@ namespace storm {
bool monDecr = true; bool monDecr = true;
bool monIncr = true; bool monIncr = true;
for (auto i = 0; i < numberOfSamples; ++i) {
for (uint_fast64_t i = 0; i < numberOfSamples; ++i) {
auto valuation = storm::utility::parametric::Valuation<ValueType>(); auto valuation = storm::utility::parametric::Valuation<ValueType>();
for (auto itr2 = variables.begin(); itr2 != variables.end(); ++itr2) { for (auto itr2 = variables.begin(); itr2 != variables.end(); ++itr2) {
// Only change value for current variable // Only change value for current variable

12
src/storm-pars/analysis/Order.cpp

@ -231,14 +231,14 @@ namespace storm {
} }
std::vector<uint_fast64_t> Order::sortStates(storm::storage::BitVector* states) { std::vector<uint_fast64_t> Order::sortStates(storm::storage::BitVector* states) {
auto numberOfSetBits = states->getNumberOfSetBits();
uint_fast64_t numberOfSetBits = states->getNumberOfSetBits();
auto stateSize = states->size(); auto stateSize = states->size();
auto result = std::vector<uint_fast64_t>(numberOfSetBits, stateSize); auto result = std::vector<uint_fast64_t>(numberOfSetBits, stateSize);
for (auto state : *states) { for (auto state : *states) {
if (result[0] == stateSize) { if (result[0] == stateSize) {
result[0] = state; result[0] = state;
} else { } else {
auto i = 0;
uint_fast64_t i = 0;
bool added = false; bool added = false;
while (i < numberOfSetBits && !added) { while (i < numberOfSetBits && !added) {
if (result[i] == stateSize) { if (result[i] == stateSize) {
@ -249,7 +249,7 @@ namespace storm {
if (compareRes == ABOVE) { if (compareRes == ABOVE) {
auto temp = result[i]; auto temp = result[i];
result[i] = state; result[i] = state;
for (auto j = i + 1; j < numberOfSetBits && result[j + 1] != stateSize; j++) {
for (uint_fast64_t j = i + 1; j < numberOfSetBits && result[j + 1] != stateSize; j++) {
auto temp2 = result[j]; auto temp2 = result[j];
result[j] = temp; result[j] = temp;
temp = temp2; temp = temp2;
@ -261,7 +261,7 @@ namespace storm {
++i; ++i;
auto temp = result[i]; auto temp = result[i];
result[i] = state; result[i] = state;
for (auto j = i + 1; j < numberOfSetBits && result[j + 1] != stateSize; j++) {
for (uint_fast64_t j = i + 1; j < numberOfSetBits && result[j + 1] != stateSize; j++) {
auto temp2 = result[j]; auto temp2 = result[j];
result[j] = temp; result[j] = temp;
temp = temp2; temp = temp2;
@ -277,10 +277,6 @@ namespace storm {
return result; return result;
} }
void Order::toString(std::ostream &out) {
}
bool Order::above(Node *node1, Node *node2) { bool Order::above(Node *node1, Node *node2) {
bool found = false; bool found = false;
for (auto const& state : node1->states) { for (auto const& state : node1->states) {

10
src/storm-pars/analysis/OrderExtender.cpp

@ -53,7 +53,7 @@ namespace storm {
storm::storage::StronglyConnectedComponentDecompositionOptions const options; storm::storage::StronglyConnectedComponentDecompositionOptions const options;
this->sccs = storm::storage::StronglyConnectedComponentDecomposition<ValueType>(matrix, options); this->sccs = storm::storage::StronglyConnectedComponentDecomposition<ValueType>(matrix, options);
acyclic = true; acyclic = true;
for (auto i = 0; acyclic && i < sccs.size(); ++i) {
for (size_t i = 0; acyclic && i < sccs.size(); ++i) {
acyclic &= sccs.getBlock(i).size() <= 1; acyclic &= sccs.getBlock(i).size() <= 1;
} }
} }
@ -91,13 +91,9 @@ namespace storm {
auto matrix = this->model->getTransitionMatrix(); auto matrix = this->model->getTransitionMatrix();
auto initialMiddleStates = storm::storage::BitVector(numberOfStates); auto initialMiddleStates = storm::storage::BitVector(numberOfStates);
// Check if MC contains cycles
storm::storage::StronglyConnectedComponentDecompositionOptions const options;
// Create the Order
// Add possible cycle breaking states
if (!acyclic) { if (!acyclic) {
for (auto i = 0; i < sccs.size(); ++i) {
for (size_t i = 0; i < sccs.size(); ++i) {
auto scc = sccs.getBlock(i); auto scc = sccs.getBlock(i);
if (scc.size() > 1) { if (scc.size() > 1) {
auto states = scc.getStates(); auto states = scc.getStates();

16
src/test/storm-pars/analysis/AssumptionCheckerTest.cpp

@ -131,8 +131,8 @@ TEST(AssumptionCheckerTest, Simple1) {
model = simplifier.getSimplifiedModel(); model = simplifier.getSimplifiedModel();
dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
ASSERT_EQ(dtmc->getNumberOfStates(), 5);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 8);
ASSERT_EQ(dtmc->getNumberOfStates(), 5ul);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 8ul);
// Create the region // Create the region
auto vars = storm::models::sparse::getProbabilityParameters(*dtmc); auto vars = storm::models::sparse::getProbabilityParameters(*dtmc);
@ -183,8 +183,8 @@ TEST(AssumptionCheckerTest, Simple2) {
model = simplifier.getSimplifiedModel(); model = simplifier.getSimplifiedModel();
dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
ASSERT_EQ(dtmc->getNumberOfStates(), 5);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 8);
ASSERT_EQ(dtmc->getNumberOfStates(), 5ul);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 8ul);
// Create the region // Create the region
auto vars = storm::models::sparse::getProbabilityParameters(*dtmc); auto vars = storm::models::sparse::getProbabilityParameters(*dtmc);
@ -249,8 +249,8 @@ TEST(AssumptionCheckerTest, Simple3) {
model = simplifier.getSimplifiedModel(); model = simplifier.getSimplifiedModel();
dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
ASSERT_EQ(6, dtmc->getNumberOfStates());
ASSERT_EQ(12, dtmc->getNumberOfTransitions());
ASSERT_EQ(6ul, dtmc->getNumberOfStates());
ASSERT_EQ(12ul, dtmc->getNumberOfTransitions());
// Create the region // Create the region
auto vars = storm::models::sparse::getProbabilityParameters(*dtmc); auto vars = storm::models::sparse::getProbabilityParameters(*dtmc);
@ -318,8 +318,8 @@ TEST(AssumptionCheckerTest, Simple4) {
model = simplifier.getSimplifiedModel(); model = simplifier.getSimplifiedModel();
dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
ASSERT_EQ(dtmc->getNumberOfStates(), 5);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 8);
ASSERT_EQ(dtmc->getNumberOfStates(), 5ul);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 8ul);
// Create the region // Create the region
auto vars = storm::models::sparse::getProbabilityParameters(*dtmc); auto vars = storm::models::sparse::getProbabilityParameters(*dtmc);

8
src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp

@ -150,8 +150,8 @@ std::vector<storm::storage::ParameterRegion<storm::RationalFunction>> regions =
storm::analysis::MonotonicityChecker<storm::RationalFunction> monotonicityChecker = storm::analysis::MonotonicityChecker<storm::RationalFunction>(dtmc, formulas, regions, true); storm::analysis::MonotonicityChecker<storm::RationalFunction> monotonicityChecker = storm::analysis::MonotonicityChecker<storm::RationalFunction>(dtmc, formulas, regions, true);
auto result = monotonicityChecker.checkMonotonicity(); auto result = monotonicityChecker.checkMonotonicity();
EXPECT_EQ(1, result.size());
EXPECT_EQ(2, result.begin()->second.size());
EXPECT_EQ(1ul, result.size());
EXPECT_EQ(2ul, result.begin()->second.size());
auto monotone = result.begin()->second.begin(); auto monotone = result.begin()->second.begin();
EXPECT_EQ(true, monotone->second.first); EXPECT_EQ(true, monotone->second.first);
EXPECT_EQ(false, monotone->second.second); EXPECT_EQ(false, monotone->second.second);
@ -198,8 +198,8 @@ TEST(MonotonicityCheckerTest, Brp_with_bisimulation_samples) {
auto monotonicityChecker = storm::analysis::MonotonicityChecker<storm::RationalFunction>(dtmc, formulas, regions, true, 50); auto monotonicityChecker = storm::analysis::MonotonicityChecker<storm::RationalFunction>(dtmc, formulas, regions, true, 50);
auto result = monotonicityChecker.checkMonotonicity(); auto result = monotonicityChecker.checkMonotonicity();
EXPECT_EQ(1, result.size());
EXPECT_EQ(2, result.begin()->second.size());
EXPECT_EQ(1ul, result.size());
EXPECT_EQ(2ul, result.begin()->second.size());
auto monotone = result.begin()->second.begin(); auto monotone = result.begin()->second.begin();
EXPECT_EQ(true, monotone->second.first); EXPECT_EQ(true, monotone->second.first);
EXPECT_EQ(false, monotone->second.second); EXPECT_EQ(false, monotone->second.second);

6
src/test/storm-pars/analysis/OrderExtenderTest.cpp

@ -53,7 +53,7 @@ TEST(OrderExtenderTest, Brp_with_bisimulation) {
EXPECT_EQ(dtmc->getNumberOfStates(), std::get<2>(criticalTuple)); EXPECT_EQ(dtmc->getNumberOfStates(), std::get<2>(criticalTuple));
auto order = std::get<0>(criticalTuple); auto order = std::get<0>(criticalTuple);
for (auto i = 0; i < dtmc->getNumberOfStates(); ++i) {
for (uint_fast64_t i = 0; i < dtmc->getNumberOfStates(); ++i) {
EXPECT_TRUE((*order->getAddedStates())[i]); EXPECT_TRUE((*order->getAddedStates())[i]);
} }
@ -86,8 +86,8 @@ TEST(OrderExtenderTest, Brp_without_bisimulation) {
auto *extender = new storm::analysis::OrderExtender<storm::RationalFunction>(dtmc); auto *extender = new storm::analysis::OrderExtender<storm::RationalFunction>(dtmc);
auto criticalTuple = extender->toOrder(formulas); auto criticalTuple = extender->toOrder(formulas);
EXPECT_EQ(183, std::get<1>(criticalTuple));
EXPECT_EQ(186, std::get<2>(criticalTuple));
EXPECT_EQ(183ul, std::get<1>(criticalTuple));
EXPECT_EQ(186ul, std::get<2>(criticalTuple));
} }
Loading…
Cancel
Save