Skip to content

Commit

Permalink
Fixed double comparisons in SMG model checker
Browse files Browse the repository at this point in the history
  • Loading branch information
@TheGreatfpmK
TheGreatfpmK committed Dec 6, 2024
1 parent 55eeeb6 commit dc3ee84
Showing 1 changed file with 17 additions and 6 deletions.
23 changes: 17 additions & 6 deletions payntbind/src/synthesis/smg/modelchecker/helper/SparseSmgRpatlHelper.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,8 @@
#include "SparseSmgRpatlHelper.h"

#include <queue>
#include <cmath>
#include <cassert>

#include <storm/environment/solver/GameSolverEnvironment.h>
#include <storm/environment/Environment.h>
Expand All @@ -28,6 +30,10 @@ namespace synthesis {
}
}

bool epsilonGreaterOrEqual(double x, double y, double eps=1e-8) {
return (x>=y) || (abs(x - y) <= eps);
}

template<typename ValueType>
SMGSparseModelCheckingHelperReturnType<ValueType> SparseSmgRpatlHelper<ValueType>::computeUntilProbabilities(storm::Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, storm::modelchecker::ModelCheckerHint const& hint) {
auto solverEnv = env;
Expand Down Expand Up @@ -86,12 +92,12 @@ namespace synthesis {
for (uint64_t row = transitionMatrix.getRowGroupIndices()[state], endRow = transitionMatrix.getRowGroupIndices()[state + 1]; row < endRow; ++row) {
// check if the choice belongs to MEC, if not then this choice is the best exit choice for the MEC
// the states with such choices will be used as the initial states for backwards BFS
if ((!statesOfCoalition.get(state)) && (maximize ? constrainedChoiceValues[row] >= result[state] : constrainedChoiceValues[row] <= result[state]) && (stateActions.second.find(row) == stateActions.second.end())) {
if ((!statesOfCoalition.get(state)) && (maximize ? epsilonGreaterOrEqual(constrainedChoiceValues[row], result[state]) : epsilonGreaterOrEqual(result[state], constrainedChoiceValues[row])) && (stateActions.second.find(row) == stateActions.second.end())) {
BFSqueue.push(state);
optimalChoices[state] = stateChoiceIndex;
optimalChoiceSet.set(state);
break;
} else if ((statesOfCoalition.get(state)) && (maximize ? constrainedChoiceValues[row] <= result[state] : constrainedChoiceValues[row] >= result[state]) && (stateActions.second.find(row) == stateActions.second.end())) {
} else if ((statesOfCoalition.get(state)) && (maximize ? epsilonGreaterOrEqual(result[state], constrainedChoiceValues[row]) : epsilonGreaterOrEqual(constrainedChoiceValues[row], result[state])) && (stateActions.second.find(row) == stateActions.second.end())) {
BFSqueue.push(state);
optimalChoices[state] = stateChoiceIndex;
optimalChoiceSet.set(state);
Expand All @@ -113,7 +119,7 @@ namespace synthesis {
uint64_t stateChoiceIndex = 0;
bool choiceFound = false;
for (uint64_t row = transitionMatrix.getRowGroupIndices()[preState], endRow = transitionMatrix.getRowGroupIndices()[preState + 1]; row < endRow; ++row) {
if ((!statesOfCoalition.get(preState)) && (maximize ? constrainedChoiceValues[row] >= result[preState] : constrainedChoiceValues[row] <= result[preState])) {
if ((!statesOfCoalition.get(preState)) && (maximize ? epsilonGreaterOrEqual(constrainedChoiceValues[row], result[preState]) : epsilonGreaterOrEqual(result[preState], constrainedChoiceValues[row]))) {
for (auto const &preStateEntry : transitionMatrix.getRow(row)) {
if (preStateEntry.getColumn() == currentState) {
BFSqueue.push(preState);
Expand All @@ -123,7 +129,7 @@ namespace synthesis {
break;
}
}
} else if ((statesOfCoalition.get(preState)) && (maximize ? constrainedChoiceValues[row] <= result[preState] : constrainedChoiceValues[row] >= result[preState])) {
} else if ((statesOfCoalition.get(preState)) && (maximize ? epsilonGreaterOrEqual(result[preState], constrainedChoiceValues[row]) : epsilonGreaterOrEqual(constrainedChoiceValues[row], result[preState]))) {
for (auto const &preStateEntry : transitionMatrix.getRow(row)) {
if (preStateEntry.getColumn() == currentState) {
BFSqueue.push(preState);
Expand Down Expand Up @@ -152,7 +158,7 @@ namespace synthesis {
if (!statesOfCoalition.get(state)) { // not sure why the statesOfCoalition bitvector is flipped
uint64_t stateRowIndex = 0;
for (auto choice : transitionMatrix.getRowGroupIndices(state)) {
if (maximize ? constrainedChoiceValues[choice] >= result[state] : constrainedChoiceValues[choice] <= result[state]) {
if (maximize ? epsilonGreaterOrEqual(constrainedChoiceValues[choice], result[state]) : epsilonGreaterOrEqual(result[state], constrainedChoiceValues[choice])) {
optimalChoices[state] = stateRowIndex;
break;
}
Expand All @@ -161,7 +167,7 @@ namespace synthesis {
} else {
uint64_t stateRowIndex = 0;
for (auto choice : transitionMatrix.getRowGroupIndices(state)) {
if (maximize ? constrainedChoiceValues[choice] <= result[state] : constrainedChoiceValues[choice] >= result[state]) {
if (maximize ? epsilonGreaterOrEqual(result[state], constrainedChoiceValues[choice]) : epsilonGreaterOrEqual(constrainedChoiceValues[choice], result[state])) {
optimalChoices[state] = stateRowIndex;
break;
}
Expand All @@ -170,6 +176,11 @@ namespace synthesis {
}
}

// double check if all states have a choice
for (uint64_t state = 0; state < stateCount; state++) {
assert(optimalChoiceSet.get(state));
}

storm::storage::Scheduler<ValueType> tempScheduler(optimalChoices.size());
for (uint64_t state = 0; state < optimalChoices.size(); ++state) {
tempScheduler.setChoice(optimalChoices[state], state);
Expand Down

0 comments on commit dc3ee84

Please sign in to comment.