From dc3ee84d2b57bd49a56e148bf64a0aaaaf2a8cdd Mon Sep 17 00:00:00 2001 From: Filip Macak Date: Fri, 6 Dec 2024 17:25:11 +0100 Subject: [PATCH] Fixed double comparisons in SMG model checker --- .../helper/SparseSmgRpatlHelper.cpp | 23 ++++++++++++++----- 1 file changed, 17 insertions(+), 6 deletions(-) diff --git a/payntbind/src/synthesis/smg/modelchecker/helper/SparseSmgRpatlHelper.cpp b/payntbind/src/synthesis/smg/modelchecker/helper/SparseSmgRpatlHelper.cpp index 8786d76e..0cb1d710 100644 --- a/payntbind/src/synthesis/smg/modelchecker/helper/SparseSmgRpatlHelper.cpp +++ b/payntbind/src/synthesis/smg/modelchecker/helper/SparseSmgRpatlHelper.cpp @@ -5,6 +5,8 @@ #include "SparseSmgRpatlHelper.h" #include +#include +#include #include #include @@ -28,6 +30,10 @@ namespace synthesis { } } + bool epsilonGreaterOrEqual(double x, double y, double eps=1e-8) { + return (x>=y) || (abs(x - y) <= eps); + } + template SMGSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeUntilProbabilities(storm::Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix 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; @@ -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); @@ -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); @@ -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); @@ -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; } @@ -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; } @@ -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 tempScheduler(optimalChoices.size()); for (uint64_t state = 0; state < optimalChoices.size(); ++state) { tempScheduler.setChoice(optimalChoices[state], state);