diff --git a/src/storm/abstraction/ExplicitQualitativeGameResult.cpp b/src/storm/abstraction/ExplicitQualitativeGameResult.cpp index 8ff41f18a..1a903249d 100644 --- a/src/storm/abstraction/ExplicitQualitativeGameResult.cpp +++ b/src/storm/abstraction/ExplicitQualitativeGameResult.cpp @@ -7,7 +7,6 @@ namespace storm { // Intentionally left empty. } - storm::storage::BitVector const& ExplicitQualitativeGameResult::getStates() const { return this->getPlayer1States(); } diff --git a/src/storm/abstraction/ExplicitQuantitativeResult.cpp b/src/storm/abstraction/ExplicitQuantitativeResult.cpp index b15db88bb..fc6cc14b0 100644 --- a/src/storm/abstraction/ExplicitQuantitativeResult.cpp +++ b/src/storm/abstraction/ExplicitQuantitativeResult.cpp @@ -2,6 +2,8 @@ #include "storm/storage/BitVector.h" +#include "storm/adapters/RationalNumberAdapter.h" + #include "storm/utility/macros.h" #include "storm/exceptions/InvalidArgumentException.h" @@ -55,5 +57,6 @@ namespace storm { } template class ExplicitQuantitativeResult; + template class ExplicitQuantitativeResult; } } diff --git a/src/storm/abstraction/ExplicitQuantitativeResultMinMax.cpp b/src/storm/abstraction/ExplicitQuantitativeResultMinMax.cpp index fe8799a9f..34a3ed22d 100644 --- a/src/storm/abstraction/ExplicitQuantitativeResultMinMax.cpp +++ b/src/storm/abstraction/ExplicitQuantitativeResultMinMax.cpp @@ -1,5 +1,7 @@ #include "storm/abstraction/ExplicitQuantitativeResultMinMax.h" +#include "storm/adapters/RationalNumberAdapter.h" + namespace storm { namespace abstraction { @@ -57,5 +59,6 @@ namespace storm { } template class ExplicitQuantitativeResultMinMax; + template class ExplicitQuantitativeResultMinMax; } } diff --git a/src/storm/abstraction/MenuGame.cpp b/src/storm/abstraction/MenuGame.cpp index 6252697bc..8258ddb51 100644 --- a/src/storm/abstraction/MenuGame.cpp +++ b/src/storm/abstraction/MenuGame.cpp @@ -82,8 +82,9 @@ namespace storm { template class MenuGame; template class MenuGame; + #ifdef STORM_HAVE_CARL - template class MenuGame; + template class MenuGame; #endif } } diff --git a/src/storm/abstraction/MenuGameAbstractor.cpp b/src/storm/abstraction/MenuGameAbstractor.cpp index c999b9316..2094568a2 100644 --- a/src/storm/abstraction/MenuGameAbstractor.cpp +++ b/src/storm/abstraction/MenuGameAbstractor.cpp @@ -176,7 +176,7 @@ namespace storm { template class MenuGameAbstractor; #ifdef STORM_HAVE_CARL - template class MenuGameAbstractor; + template class MenuGameAbstractor; #endif } } diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index f829ff440..987aaa367 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -1119,7 +1119,12 @@ namespace storm { continue; } - ValueType alternateDistance = probabilityDistances ? currentDistance * entry.getValue() : currentDistance + storm::utility::one(); + ValueType alternateDistance; + if (probabilityDistances) { + alternateDistance = currentDistance * entry.getValue(); + } else { + alternateDistance = currentDistance + storm::utility::one(); + } if (probabilityDistances ? alternateDistance > distances[player1Successor] : alternateDistance < distances[player1Successor]) { distances[player1Successor] = alternateDistance; if (generatePredecessors) { @@ -1682,6 +1687,7 @@ namespace storm { template class MenuGameRefiner; template class MenuGameRefiner; + template class MenuGameRefiner; #ifdef STORM_HAVE_CARL // Currently, this instantiation does not work. diff --git a/src/storm/abstraction/StateSetAbstractor.cpp b/src/storm/abstraction/StateSetAbstractor.cpp index 4e4a88ee1..21b03a476 100644 --- a/src/storm/abstraction/StateSetAbstractor.cpp +++ b/src/storm/abstraction/StateSetAbstractor.cpp @@ -159,7 +159,7 @@ namespace storm { template class StateSetAbstractor; template class StateSetAbstractor; #ifdef STORM_HAVE_CARL - template class StateSetAbstractor; + template class StateSetAbstractor; #endif } } diff --git a/src/storm/abstraction/SymbolicQuantitativeGameResult.cpp b/src/storm/abstraction/SymbolicQuantitativeGameResult.cpp index 9c91b1b97..839ba732e 100644 --- a/src/storm/abstraction/SymbolicQuantitativeGameResult.cpp +++ b/src/storm/abstraction/SymbolicQuantitativeGameResult.cpp @@ -55,6 +55,7 @@ namespace storm { template class SymbolicQuantitativeGameResult; template class SymbolicQuantitativeGameResult; + template class SymbolicQuantitativeGameResult; } } diff --git a/src/storm/abstraction/SymbolicQuantitativeGameResultMinMax.cpp b/src/storm/abstraction/SymbolicQuantitativeGameResultMinMax.cpp index 08be6fad6..9a58c2597 100644 --- a/src/storm/abstraction/SymbolicQuantitativeGameResultMinMax.cpp +++ b/src/storm/abstraction/SymbolicQuantitativeGameResultMinMax.cpp @@ -7,6 +7,6 @@ namespace storm { SymbolicQuantitativeGameResultMinMax::SymbolicQuantitativeGameResultMinMax(SymbolicQuantitativeGameResult const& min, SymbolicQuantitativeGameResult const& max) : min(min), max(max) { // Intentionally left empty. } - + } } diff --git a/src/storm/abstraction/jani/AutomatonAbstractor.cpp b/src/storm/abstraction/jani/AutomatonAbstractor.cpp index 3063c5b1b..21481f00c 100644 --- a/src/storm/abstraction/jani/AutomatonAbstractor.cpp +++ b/src/storm/abstraction/jani/AutomatonAbstractor.cpp @@ -151,7 +151,7 @@ namespace storm { template class AutomatonAbstractor; template class AutomatonAbstractor; #ifdef STORM_HAVE_CARL - template class AutomatonAbstractor; + template class AutomatonAbstractor; #endif } } diff --git a/src/storm/abstraction/jani/EdgeAbstractor.cpp b/src/storm/abstraction/jani/EdgeAbstractor.cpp index e37676c64..950221dcd 100644 --- a/src/storm/abstraction/jani/EdgeAbstractor.cpp +++ b/src/storm/abstraction/jani/EdgeAbstractor.cpp @@ -727,7 +727,7 @@ namespace storm { template class EdgeAbstractor; template class EdgeAbstractor; #ifdef STORM_HAVE_CARL - template class EdgeAbstractor; + template class EdgeAbstractor; #endif } } diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp index 886bcbdcc..d233e3f5f 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp @@ -285,7 +285,7 @@ namespace storm { template class JaniMenuGameAbstractor; template class JaniMenuGameAbstractor; #ifdef STORM_HAVE_CARL - template class JaniMenuGameAbstractor; + template class JaniMenuGameAbstractor; #endif } } diff --git a/src/storm/abstraction/prism/CommandAbstractor.cpp b/src/storm/abstraction/prism/CommandAbstractor.cpp index bc65bc453..d73526454 100644 --- a/src/storm/abstraction/prism/CommandAbstractor.cpp +++ b/src/storm/abstraction/prism/CommandAbstractor.cpp @@ -703,7 +703,7 @@ namespace storm { template class CommandAbstractor; template class CommandAbstractor; #ifdef STORM_HAVE_CARL - template class CommandAbstractor; + template class CommandAbstractor; #endif } } diff --git a/src/storm/abstraction/prism/ModuleAbstractor.cpp b/src/storm/abstraction/prism/ModuleAbstractor.cpp index bafb43717..ab031eeab 100644 --- a/src/storm/abstraction/prism/ModuleAbstractor.cpp +++ b/src/storm/abstraction/prism/ModuleAbstractor.cpp @@ -125,7 +125,7 @@ namespace storm { template class ModuleAbstractor; template class ModuleAbstractor; #ifdef STORM_HAVE_CARL - template class ModuleAbstractor; + template class ModuleAbstractor; #endif } } diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index 60ab41e92..d25a51712 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -277,7 +277,7 @@ namespace storm { template class PrismMenuGameAbstractor; template class PrismMenuGameAbstractor; #ifdef STORM_HAVE_CARL - template class PrismMenuGameAbstractor; + template class PrismMenuGameAbstractor; #endif } } diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index eb253e625..d1078b8c8 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -97,14 +97,14 @@ namespace storm { } template - bool GameBasedMdpModelChecker::canHandle(CheckTask const& checkTask) const { + bool GameBasedMdpModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); storm::logic::FragmentSpecification fragment = storm::logic::reachability(); return formula.isInFragment(fragment) && checkTask.isOnlyInitialStatesRelevantSet(); } template - std::unique_ptr GameBasedMdpModelChecker::computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) { + std::unique_ptr GameBasedMdpModelChecker::computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); std::map labelToExpressionMapping; if (preprocessedModel.isPrismProgram()) { @@ -121,11 +121,11 @@ namespace storm { storm::expressions::Expression constraintExpression = pathFormula.getLeftSubformula().toExpression(preprocessedModel.getManager(), labelToExpressionMapping); storm::expressions::Expression targetStateExpression = pathFormula.getRightSubformula().toExpression(preprocessedModel.getManager(), labelToExpressionMapping); - return performGameBasedAbstractionRefinement(env, checkTask.substituteFormula(pathFormula), constraintExpression, targetStateExpression); + return performGameBasedAbstractionRefinement(env, checkTask.template substituteFormula(pathFormula), constraintExpression, targetStateExpression); } template - std::unique_ptr GameBasedMdpModelChecker::computeReachabilityProbabilities(Environment const& env, CheckTask const& checkTask) { + std::unique_ptr GameBasedMdpModelChecker::computeReachabilityProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& pathFormula = checkTask.getFormula(); std::map labelToExpressionMapping; if (preprocessedModel.isPrismProgram()) { @@ -142,11 +142,11 @@ namespace storm { storm::expressions::Expression constraintExpression = preprocessedModel.getManager().boolean(true); storm::expressions::Expression targetStateExpression = pathFormula.getSubformula().toExpression(preprocessedModel.getManager(), labelToExpressionMapping); - return performGameBasedAbstractionRefinement(env, checkTask.substituteFormula(pathFormula), constraintExpression, targetStateExpression); + return performGameBasedAbstractionRefinement(env, checkTask.template substituteFormula(pathFormula), constraintExpression, targetStateExpression); } template - std::unique_ptr checkForResultAfterQualitativeCheck(CheckTask const& checkTask, storm::OptimizationDirection player2Direction, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& prob0, storm::dd::Bdd const& prob1) { + std::unique_ptr checkForResultAfterQualitativeCheck(CheckTask const& checkTask, storm::OptimizationDirection player2Direction, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& prob0, storm::dd::Bdd const& prob1) { std::unique_ptr result; if (checkTask.isBoundSet()) { @@ -185,7 +185,7 @@ namespace storm { } template - std::unique_ptr checkForResultAfterQualitativeCheck(CheckTask const& checkTask, storm::dd::Bdd const& initialStates, SymbolicQualitativeGameResultMinMax const& qualitativeResult) { + std::unique_ptr checkForResultAfterQualitativeCheck(CheckTask const& checkTask, storm::dd::Bdd const& initialStates, SymbolicQualitativeGameResultMinMax const& qualitativeResult) { // Check whether we can already give the answer based on the current information. std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, storm::OptimizationDirection::Minimize, initialStates, qualitativeResult.prob0Min.getPlayer1States(), qualitativeResult.prob1Min.getPlayer1States()); if (result) { @@ -199,7 +199,7 @@ namespace storm { } template - std::unique_ptr checkForResultAfterQualitativeCheck(CheckTask const& checkTask, storm::OptimizationDirection player2Direction, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& prob0, storm::storage::BitVector const& prob1) { + std::unique_ptr checkForResultAfterQualitativeCheck(CheckTask const& checkTask, storm::OptimizationDirection player2Direction, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& prob0, storm::storage::BitVector const& prob1) { std::unique_ptr result; if (checkTask.isBoundSet()) { @@ -238,7 +238,7 @@ namespace storm { } template - std::unique_ptr checkForResultAfterQualitativeCheck(CheckTask const& checkTask, storm::storage::BitVector const& initialStates, ExplicitQualitativeGameResultMinMax const& qualitativeResult) { + std::unique_ptr checkForResultAfterQualitativeCheck(CheckTask const& checkTask, storm::storage::BitVector const& initialStates, ExplicitQualitativeGameResultMinMax const& qualitativeResult) { // Check whether we can already give the answer based on the current information. std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, storm::OptimizationDirection::Minimize, initialStates, qualitativeResult.prob0Min.getPlayer1States(), qualitativeResult.prob1Min.getPlayer1States()); if (result) { @@ -252,7 +252,7 @@ namespace storm { } template - std::unique_ptr checkForResultAfterQuantitativeCheck(CheckTask const& checkTask, storm::OptimizationDirection const& player2Direction, std::pair const& initialValueRange) { + std::unique_ptr checkForResultAfterQuantitativeCheck(CheckTask const& checkTask, storm::OptimizationDirection const& player2Direction, std::pair const& initialValueRange) { std::unique_ptr result; // If the minimum value exceeds an upper threshold or the maximum value is below a lower threshold, we can @@ -476,7 +476,7 @@ namespace storm { uint64_t maybeStatePosition = 0; previousPlayer2States = 0; for (auto state : maybeStates) { - if (state == 25305 || state == 67442 || state == 67440) { + if (state == 1976 || state == 46452 || state == 114590 || state == 84730 || state == 84575 || state == 84562 || state == 31895 || state == 84574 || state == 84561 || state == 32933 || state == 86740 || state == 86734 || state == 31789 || state == 86740 || state == 84360 || state == 84358) { std::cout << "dealing with problematic state " << state << " whose local offset is " << maybeStatePosition << std::endl; } uint64_t chosenPlayer2State = startingStrategyPair->getPlayer1Strategy().getChoice(state); @@ -484,13 +484,13 @@ namespace storm { uint64_t previousPlayer2MaybeStatesForState = 0; for (uint64_t player2State = player1Groups[state]; player2State < player1Groups[state + 1]; ++player2State) { if (player2MaybeStates.get(player2State)) { - if (state == 25305 || state == 67442 || state == 67440) { - std::cout << "player 2 state " << player2State << " is a player 2 maybe state with local index " << previousPlayer2States << std::endl; + if (state == 1976 || state == 46452 || state == 114590 || state == 84730 || state == 84575 || state == 84562 || state == 31895 || state == 84574 || state == 84561 || state == 32933 || state == 86740 || state == 86734 || state == 31789 || state == 86740 || state == 84360 || state == 84358) { + std::cout << "player 2 state " << player2State << " is a player 2 maybe state with local index " << previousPlayer2States << " ranging from row " << submatrix.getRowGroupIndices()[previousPlayer2States] << " to " << submatrix.getRowGroupIndices()[previousPlayer2States + 1] << std::endl; } if (player2State == chosenPlayer2State) { player1Scheduler[maybeStatePosition] = previousPlayer2MaybeStatesForState; - if (state == 25305 || state == 67442 || state == 67440) { + if (state == 1976 || state == 46452 || state == 114590 || state == 84730 || state == 84575 || state == 84562 || state == 31895 || state == 84574 || state == 84561 || state == 32933 || state == 86740 || state == 86734 || state == 31789 || state == 86740 || state == 84360 || state == 84358) { std::cout << "player 1 scheduler chooses " << previousPlayer2MaybeStatesForState << " which globally is " << player2State << std::endl; } } @@ -499,12 +499,12 @@ namespace storm { if (startingStrategyPair->getPlayer2Strategy().hasDefinedChoice(player2State)) { player2Scheduler[previousPlayer2States] = startingStrategyPair->getPlayer2Strategy().getChoice(player2State) - transitionMatrix.getRowGroupIndices() [player2State]; - if (state == 25305 || state == 67442 || state == 67440) { + if (state == 1976 || state == 46452 || state == 114590 || state == 84730 || state == 84575 || state == 84562 || state == 31895 || state == 84574 || state == 84561 || state == 32933 || state == 86740 || state == 86734 || state == 31789 || state == 86740 || state == 84360 || state == 84358) { std::cout << "copied over choice " << player2Scheduler[previousPlayer2States] << " for player 2 (global index " << startingStrategyPair->getPlayer2Strategy().getChoice(player2State) << ")" << std::endl; } } else { player2Scheduler[previousPlayer2States] = 0; - if (state == 25305 || state == 67442 || state == 67440) { + if (state == 1976 || state == 46452 || state == 114590 || state == 84730 || state == 84575 || state == 84562 || state == 31895 || state == 84574 || state == 84561 || state == 32933 || state == 86740 || state == 86734 || state == 31789 || state == 86740 || state == 84360 || state == 84358) { std::cout << "did not copy (undefined) choice for player 2 (global index " << startingStrategyPair->getPlayer2Strategy().getChoice(player2State) << ")" << std::endl; } } @@ -516,16 +516,11 @@ namespace storm { ++maybeStatePosition; } + STORM_LOG_ASSERT(previousPlayer2States == submatrix.getRowGroupCount(), "Expected correct number of player 2 states."); } // Solve actual game and track schedulers. - if (player1Scheduler.size() > 4713) { - std::cout << "before: player1Scheduler[4713] = " << player1Scheduler[4713] << std::endl; - } gameSolver->solveGame(env, player1Direction, player2Direction, values, b, &player1Scheduler, &player2Scheduler); - if (player1Scheduler.size() > 67440) { - std::cout << "after: player1Scheduler[4713] = " << player1Scheduler[4713] << std::endl; - } // Set values according to quantitative result (qualitative result has already been taken care of). storm::utility::vector::setVectorValues(result.getValues(), maybeStates, values); @@ -555,7 +550,7 @@ namespace storm { } template - std::unique_ptr GameBasedMdpModelChecker::performGameBasedAbstractionRefinement(Environment const& env, CheckTask const& checkTask, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) { + std::unique_ptr GameBasedMdpModelChecker::performGameBasedAbstractionRefinement(Environment const& env, CheckTask const& checkTask, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) { STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidPropertyException, "The game-based abstraction refinement model checker can only compute the result for the initial states."); // Optimization: do not compute both bounds if not necessary (e.g. if bound given and exceeded, etc.) @@ -652,7 +647,7 @@ namespace storm { } template - std::unique_ptr GameBasedMdpModelChecker::performSymbolicAbstractionSolutionStep(Environment const& env, CheckTask const& checkTask, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::MenuGameRefiner const& refiner, boost::optional>& previousQualitativeResult, boost::optional>& previousMinQuantitativeResult) { + std::unique_ptr GameBasedMdpModelChecker::performSymbolicAbstractionSolutionStep(Environment const& env, CheckTask const& checkTask, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::MenuGameRefiner const& refiner, boost::optional>& previousQualitativeResult, boost::optional>& previousMinQuantitativeResult) { STORM_LOG_TRACE("Using dd-based solving."); @@ -845,24 +840,49 @@ namespace storm { template class ExplicitGameExporter { public: + ExplicitGameExporter() : showNonStrategyAlternatives(false) { + // Intentionally left empty. + } + void exportToJson(std::string const& filename, std::vector const& player1Groups, std::vector const& player2Groups, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ExplicitQuantitativeResultMinMax const& quantitativeResult, ExplicitGameStrategyPair const* minStrategyPair, ExplicitGameStrategyPair const* maxStrategyPair) { // Export game as json. std::ofstream outfile(filename); - - // Export nodes. - outfile << "{\n\t\"nodes\": [" << std::endl; - exportNodes(outfile, player1Groups, player2Groups, transitionMatrix, initialStates, constraintStates, targetStates, quantitativeResult, minStrategyPair, maxStrategyPair); - outfile << "\n\t]," << std::endl; - - // Export edges. - outfile << "\t\"edges\": [" << std::endl; - exportEdges(outfile, player1Groups, player2Groups, transitionMatrix, initialStates, constraintStates, targetStates, quantitativeResult, minStrategyPair, maxStrategyPair); - outfile << "\n\t]\n}" << std::endl; + exportGame(outfile, player1Groups, player2Groups, transitionMatrix, initialStates, constraintStates, targetStates, quantitativeResult, minStrategyPair, maxStrategyPair); + } + + void setShowNonStrategyAlternatives(bool value) { + showNonStrategyAlternatives = value; } private: - void exportEdge(std::ofstream& out, uint64_t id, uint64_t source, uint64_t target, std::string const& name, bool& first) { + + struct NodeData { + NodeData(uint64_t id, uint64_t player, bool initial, bool target) : id(id), player(player), initial(initial), target(target) { + // Intentionally left empty. + } + + uint64_t id; + uint64_t player; // 0 = probabilistic player, 1 = player 1, 2 = player 2 + bool initial; + bool target; + }; + + struct EdgeData { + EdgeData(uint64_t id, uint64_t source, uint64_t target, ValueType probability, uint64_t label, bool min, bool max) : id(id), source(source), target(target), probability(probability), label(label), min(min), max(max) { + // Intentionally left empty. + } + + uint64_t id; + uint64_t source; + uint64_t target; + ValueType probability; + uint64_t label; + bool min; + bool max; + }; + + void exportEdge(std::ofstream& out, EdgeData const& data, bool& first) { if (!first) { out << "," << std::endl; } else { @@ -870,74 +890,30 @@ namespace storm { } out << "\t\t{" << std::endl; out << "\t\t\t\"data\": {" << std::endl; - out << "\t\t\t\t\"id\": \"" << id << "\"," << std::endl; - out << "\t\t\t\t\"name\": \"" << name << "\"," << std::endl; - out << "\t\t\t\t\"source\": \"" << source << "\"," << std::endl; - out << "\t\t\t\t\"target\": \"" << target << "\"" << std::endl; - out << "\t\t\t}" << std::endl; - out << "\t\t}"; - } - - void exportEdges(std::ofstream& out, std::vector const& player1Groups, std::vector const& player2Groups, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ExplicitQuantitativeResultMinMax const& quantitativeResult, ExplicitGameStrategyPair const* minStrategyPair, ExplicitGameStrategyPair const* maxStrategyPair) { - std::vector stack; - for (auto state : initialStates) { - stack.push_back(state); + out << "\t\t\t\t\"id\": \"" << data.id << "\"," << std::endl; + if (data.probability != storm::utility::zero()) { + out << "\t\t\t\t\"name\": \"" << data.probability << "\"," << std::endl; + } else { + out << "\t\t\t\t\"name\": \"" << data.label << "\"," << std::endl; } - storm::storage::BitVector reachablePlayer1(player1Groups.size() - 1); - - bool first = true; - uint64_t edgeId = 0; - while (!stack.empty()) { - uint64_t currentState = stack.back(); - stack.pop_back(); - - // Follow lower. - if (minStrategyPair) { - if (minStrategyPair->getPlayer1Strategy().hasDefinedChoice(currentState)) { - uint64_t player2State = minStrategyPair->getPlayer1Strategy().getChoice(currentState); - exportEdge(out, edgeId++, currentState, player2State, "lo", first); - - uint64_t playerPState = minStrategyPair->getPlayer2Strategy().getChoice(player2State); - exportEdge(out, edgeId++, player2State, playerPState, "lo", first); - - for (auto const& entry : transitionMatrix.getRow(playerPState)) { - auto player1Successor = entry.getColumn(); - - exportEdge(out, edgeId++, playerPState, player1Successor, std::to_string(entry.getValue()), first); - - if (!reachablePlayer1.get(player1Successor)) { - reachablePlayer1.set(player1Successor); - stack.push_back(player1Successor); - } - } - } - } - - // Follow upper. - if (maxStrategyPair) { - if (maxStrategyPair->getPlayer1Strategy().hasDefinedChoice(currentState)) { - uint64_t player2State = maxStrategyPair->getPlayer1Strategy().getChoice(currentState); - exportEdge(out, edgeId++, currentState, player2State, "hi", first); - - uint64_t playerPState = maxStrategyPair->getPlayer2Strategy().getChoice(player2State); - exportEdge(out, edgeId++, player2State, playerPState, "hi", first); - - for (auto const& entry : transitionMatrix.getRow(playerPState)) { - auto player1Successor = entry.getColumn(); - - exportEdge(out, edgeId++, playerPState, player1Successor, std::to_string(entry.getValue()), first); - - if (!reachablePlayer1.get(player1Successor)) { - reachablePlayer1.set(player1Successor); - stack.push_back(player1Successor); - } - } - } - } + out << "\t\t\t\t\"source\": \"" << data.source << "\"," << std::endl; + out << "\t\t\t\t\"target\": \"" << data.target << "\"" << std::endl; + out << "\t\t\t}," << std::endl; + out << "\t\t\t\"classes\": \""; + if (data.min && data.max) { + out << "minMaxEdge"; + } else if (data.min) { + out << "minEdge"; + } else if (data.max) { + out << "maxEdge"; + } else { + out << "edge"; } + out << "\"" << std::endl; + out << "\t\t}"; } - void exportNode(std::ofstream& out, uint64_t state, ExplicitQuantitativeResultMinMax const* quantitativeResult, bool& first, bool target = false) { + void exportNode(std::ofstream& out, NodeData const& data, ExplicitQuantitativeResultMinMax const* quantitativeResult, bool& first) { if (!first) { out << "," << std::endl; } else { @@ -945,75 +921,122 @@ namespace storm { } out << "\t\t{" << std::endl; out << "\t\t\t\"data\": {" << std::endl; - out << "\t\t\t\t\"id\": \"" << state << "\"," << std::endl; - out << "\t\t\t\t\"name\": \"" << state; - if (quantitativeResult) { - out << " [" << quantitativeResult->getMin().getValues()[state] << ", " << quantitativeResult->getMax().getValues()[state] << "]"; - if (target) { - out << ", T"; - } + out << "\t\t\t\t\"id\": \"" << data.id << "\"," << std::endl; + out << "\t\t\t\t\"name\": \"" << data.id; + if (quantitativeResult && data.player == 1) { + out << " [" << quantitativeResult->getMin().getValues()[data.id] << ", " << quantitativeResult->getMax().getValues()[data.id] << "]"; } out << "\"" << std::endl; out << "\t\t\t}," << std::endl; out << "\t\t\t\"group\": \"nodes\"," << std::endl; - out << "\t\t\t\"classes\": \"node\"" << std::endl; + out << "\t\t\t\"classes\": \""; + if (data.player == 1) { + if (data.initial) { + out << "initialNode"; + } else if (data.target) { + out << "targetNode"; + } else { + out << "node"; + } + } else if (data.player == 2) { + out << "pl2node"; + } else if (data.player == 0) { + out << "plpnode"; + } + out << "\"" << std::endl; out << "\t\t}"; } - void exportNodes(std::ofstream& out, std::vector const& player1Groups, std::vector const& player2Groups, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ExplicitQuantitativeResultMinMax const& quantitativeResult, ExplicitGameStrategyPair const* minStrategyPair, ExplicitGameStrategyPair const* maxStrategyPair) { + void exportGame(std::ofstream& out, std::vector const& player1Groups, std::vector const& player2Groups, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ExplicitQuantitativeResultMinMax const& quantitativeResult, ExplicitGameStrategyPair const* minStrategyPair, ExplicitGameStrategyPair const* maxStrategyPair) { + // To export the game as JSON, we build some data structures through a traversal and then emit them. + std::vector nodes; + std::vector edges; + std::vector stack; for (auto state : initialStates) { stack.push_back(state); } storm::storage::BitVector reachablePlayer1(player1Groups.size() - 1); - - bool first = true; + + uint64_t edgeId = 0; while (!stack.empty()) { uint64_t currentState = stack.back(); stack.pop_back(); + + nodes.emplace_back(currentState, 1, initialStates.get(currentState), targetStates.get(currentState)); - exportNode(out, currentState, &quantitativeResult, first, targetStates.get(currentState)); - - // Follow lower. - if (minStrategyPair) { - if (minStrategyPair->getPlayer1Strategy().hasDefinedChoice(currentState)) { - uint64_t player2State = minStrategyPair->getPlayer1Strategy().getChoice(currentState); - exportNode(out, player2State, nullptr, first); - - uint64_t playerPState = minStrategyPair->getPlayer2Strategy().getChoice(player2State); - exportNode(out, playerPState, nullptr, first); - - for (auto const& entry : transitionMatrix.getRow(playerPState)) { - auto player1Successor = entry.getColumn(); - if (!reachablePlayer1.get(player1Successor)) { - reachablePlayer1.set(player1Successor); - stack.push_back(player1Successor); - } - } + for (uint64_t player2State = player1Groups[currentState]; player2State < player1Groups[currentState + 1]; ++player2State) { + bool emit = (minStrategyPair || maxStrategyPair) ? this->showNonStrategyAlternatives : true; + bool min = false; + bool max = false; + + if (minStrategyPair && minStrategyPair->getPlayer1Strategy().hasDefinedChoice(currentState) && minStrategyPair->getPlayer1Strategy().getChoice(currentState) == player2State) { + emit = true; + min = true; } - } - - // Follow upper. - if (maxStrategyPair) { - if (maxStrategyPair->getPlayer1Strategy().hasDefinedChoice(currentState)) { - uint64_t player2State = maxStrategyPair->getPlayer1Strategy().getChoice(currentState); - exportNode(out, player2State, nullptr, first); - - uint64_t playerPState = maxStrategyPair->getPlayer2Strategy().getChoice(player2State); - exportNode(out, playerPState, nullptr, first); - - for (auto const& entry : transitionMatrix.getRow(playerPState)) { - auto player1Successor = entry.getColumn(); - if (!reachablePlayer1.get(player1Successor)) { - reachablePlayer1.set(player1Successor); - stack.push_back(player1Successor); + if (maxStrategyPair && maxStrategyPair->getPlayer1Strategy().hasDefinedChoice(currentState) && maxStrategyPair->getPlayer1Strategy().getChoice(currentState) == player2State) { + emit = true; + max = true; + } + + if (emit) { + nodes.emplace_back(player2State, 2, false, false); + edges.emplace_back(edgeId++, currentState, player2State, storm::utility::zero(), player2State - player1Groups[currentState], min, max); + + for (uint64_t playerPState = player2Groups[player2State]; playerPState < player2Groups[player2State + 1]; ++playerPState) { + emit = (minStrategyPair || maxStrategyPair) ? this->showNonStrategyAlternatives : true; + min = false; + max = false; + + if (minStrategyPair && minStrategyPair->getPlayer2Strategy().hasDefinedChoice(player2State) && minStrategyPair->getPlayer2Strategy().getChoice(player2State) == playerPState) { + emit = true; + min = true; + } + if (maxStrategyPair && maxStrategyPair->getPlayer2Strategy().hasDefinedChoice(player2State) && maxStrategyPair->getPlayer2Strategy().getChoice(player2State) == playerPState) { + emit = true; + max = true; + } + + if (emit) { + nodes.emplace_back(playerPState, 0, false, false); + edges.emplace_back(edgeId++, player2State, playerPState, storm::utility::zero(), playerPState - player2Groups[player2State], min, max); + + for (auto const& entry : transitionMatrix.getRow(playerPState)) { + auto player1Successor = entry.getColumn(); + if (!reachablePlayer1.get(player1Successor)) { + reachablePlayer1.set(player1Successor); + stack.push_back(player1Successor); + } + + edges.emplace_back(edgeId++, playerPState, player1Successor, entry.getValue(), 0, false, false); + } } } } } } + + // Finally, export the data structures we built. + + // Export nodes. + out << "{\n\t\"nodes\": [" << std::endl; + bool first = true; + for (auto const& node : nodes) { + exportNode(out, node, &quantitativeResult, first); + } + out << "\n\t]," << std::endl; + + // Export edges. + first = true; + out << "\t\"edges\": [" << std::endl; + for (auto const& edge : edges) { + exportEdge(out, edge, first); + } + out << "\n\t]\n}" << std::endl; } + + bool showNonStrategyAlternatives; }; template @@ -1091,8 +1114,12 @@ namespace storm { } } +// ExplicitGameExporter exporter; +// exporter.exportToJson("game" + std::to_string(iteration) + ".json", player1Groups, player2Groups, transitionMatrix, initialStates, constraintStates, targetStates, quantitativeResult, &minStrategyPair, &maxStrategyPair); +// exit(-1); + if (sanityCheck) { - storm::utility::ConstantsComparator sanityComparator(1e-6, true); + storm::utility::ConstantsComparator sanityComparator( 1e-6, true); ///////// SANITY CHECK: apply lower strategy, obtain DTMC matrix and model check it. the values should ///////// still be the lower ones. @@ -1115,7 +1142,7 @@ namespace storm { ValueType maxDiff = storm::utility::zero(); uint64_t maxState = 0; for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) { - ValueType const& diff = std::abs(sanityValues[state] - quantitativeResult.getMin().getValues()[state]); + ValueType const& diff = storm::utility::abs(sanityValues[state] - quantitativeResult.getMin().getValues()[state]); if (diff > maxDiff) { maxState = state; maxDiff = diff; @@ -1153,7 +1180,7 @@ namespace storm { maxDiff = storm::utility::zero(); maxState = 0; for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) { - ValueType const& diff = std::abs(sanityValues[state] - quantitativeResult.getMax().getValues()[state]); + ValueType const& diff = storm::utility::abs(sanityValues[state] - quantitativeResult.getMax().getValues()[state]); if (diff > maxDiff) { maxState = state; maxDiff = diff; @@ -1189,9 +1216,9 @@ namespace storm { uint64_t currentState = stack.back(); stack.pop_back(); - std::cout << "exploring player 1 state " << currentState << std::endl; + std::cout << "exploring player 1 state " << currentState << " with " << (player1Groups[currentState + 1] - player1Groups[currentState]) << " player 2 successors from" << player1Groups[currentState] << " to " << player1Groups[currentState + 1] << std::endl; uint64_t player2State = maxStrategyPair.getPlayer1Strategy().getChoice(currentState); - std::cout << "going to player 2 state " << player2State << std::endl; + std::cout << "going to player 2 state " << player2State << " with " << (player2Groups[player2State + 1] - player2Groups[player2State]) << " player 2 choices from " << player2Groups[player2State] << " to " << player2Groups[player2State + 1] << std::endl; uint64_t player2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(player2State); std::cout << "which takes choice " << player2Choice << " which locally is " << (player2Choice - transitionMatrix.getRowGroupIndices()[player2State]) << std::endl; for (auto const& entry : transitionMatrix.getRow(player2Choice)) { @@ -1214,7 +1241,7 @@ namespace storm { } template - std::unique_ptr GameBasedMdpModelChecker::performExplicitAbstractionSolutionStep(Environment const& env, CheckTask const& checkTask, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& initialStatesBdd, storm::dd::Bdd const& constraintStatesBdd, storm::dd::Bdd const& targetStatesBdd, storm::abstraction::MenuGameRefiner const& refiner, boost::optional>& previousResult) { + std::unique_ptr GameBasedMdpModelChecker::performExplicitAbstractionSolutionStep(Environment const& env, CheckTask const& checkTask, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& initialStatesBdd, storm::dd::Bdd const& constraintStatesBdd, storm::dd::Bdd const& targetStatesBdd, storm::abstraction::MenuGameRefiner const& refiner, boost::optional>& previousResult) { STORM_LOG_TRACE("Using sparse solving."); // (0) Start by transforming the necessary symbolic elements to explicit ones. @@ -1413,7 +1440,7 @@ namespace storm { } template - storm::OptimizationDirection GameBasedMdpModelChecker::getPlayer1Direction(CheckTask const& checkTask) { + storm::OptimizationDirection GameBasedMdpModelChecker::getPlayer1Direction(CheckTask const& checkTask) { if (preprocessedModel.getModelType() == storm::storage::SymbolicModelDescription::ModelType::DTMC) { return storm::OptimizationDirection::Maximize; } else if (checkTask.isOptimizationDirectionSet()) { @@ -1594,5 +1621,8 @@ namespace storm { template class GameBasedMdpModelChecker>; template class GameBasedMdpModelChecker>; template class GameBasedMdpModelChecker>; + + template class GameBasedMdpModelChecker>; + template class GameBasedMdpModelChecker>; } } diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h index 0c585f993..c8af37073 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h @@ -87,18 +87,18 @@ namespace storm { explicit GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr const& smtSolverFactory = std::make_shared()); /// Overridden methods from super class. - virtual bool canHandle(CheckTask const& checkTask) const override; - virtual std::unique_ptr computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; - virtual std::unique_ptr computeReachabilityProbabilities(Environment const& env, CheckTask const& checkTask) override; + virtual bool canHandle(CheckTask const& checkTask) const override; + virtual std::unique_ptr computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityProbabilities(Environment const& env, CheckTask const& checkTask) override; private: /*! * Performs the core part of the abstraction-refinement loop. */ - std::unique_ptr performGameBasedAbstractionRefinement(Environment const& env, CheckTask const& checkTask, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression); + std::unique_ptr performGameBasedAbstractionRefinement(Environment const& env, CheckTask const& checkTask, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression); - std::unique_ptr performSymbolicAbstractionSolutionStep(Environment const& env, CheckTask const& checkTask, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::MenuGameRefiner const& refiner, boost::optional>& previousQualitativeResult, boost::optional>& previousMinQuantitativeResult); - std::unique_ptr performExplicitAbstractionSolutionStep(Environment const& env, CheckTask const& checkTask, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::MenuGameRefiner const& refiner, boost::optional>& previousResult); + std::unique_ptr performSymbolicAbstractionSolutionStep(Environment const& env, CheckTask const& checkTask, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::MenuGameRefiner const& refiner, boost::optional>& previousQualitativeResult, boost::optional>& previousMinQuantitativeResult); + std::unique_ptr performExplicitAbstractionSolutionStep(Environment const& env, CheckTask const& checkTask, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::MenuGameRefiner const& refiner, boost::optional>& previousResult); /*! * Retrieves the initial predicates for the abstraction. @@ -108,7 +108,7 @@ namespace storm { /*! * Derives the optimization direction of player 1. */ - storm::OptimizationDirection getPlayer1Direction(CheckTask const& checkTask); + storm::OptimizationDirection getPlayer1Direction(CheckTask const& checkTask); /*! * Performs a qualitative check on the the given game to compute the (player 1) states that have probability diff --git a/src/storm/solver/GmmxxMultiplier.cpp b/src/storm/solver/GmmxxMultiplier.cpp index f145317da..bfed0bf25 100644 --- a/src/storm/solver/GmmxxMultiplier.cpp +++ b/src/storm/solver/GmmxxMultiplier.cpp @@ -116,10 +116,20 @@ namespace storm { gmm::mult(gmmMatrix, x, result); } } + + template + void GmmxxMultiplier::multAddReduceHelper(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { + if (dir == storm::OptimizationDirection::Minimize) { + multAddReduceHelper>(rowGroupIndices, x, b, result, choices); + } else { + multAddReduceHelper>(rowGroupIndices, x, b, result, choices); + } + } template - void GmmxxMultiplier::multAddReduceHelper(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { - bool min = dir == OptimizationDirection::Minimize; + template + void GmmxxMultiplier::multAddReduceHelper(std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { + Compare compare; typedef std::vector VectorType; typedef gmm::csr_matrix MatrixType; @@ -170,7 +180,7 @@ namespace storm { oldSelectedChoiceValue = newValue; } - if (min ? newValue < currentValue : newValue > currentValue) { + if (compare(newValue, currentValue)) { currentValue = newValue; if (choices) { selectedChoice = currentRow - *row_group_it; @@ -180,7 +190,7 @@ namespace storm { // Finally write value to target vector. *target_it = currentValue; - if (choices && (min ? currentValue < oldSelectedChoiceValue : currentValue > oldSelectedChoiceValue)) { + if (choices && compare(currentValue, oldSelectedChoiceValue)) { *choice_it = selectedChoice; } } @@ -188,7 +198,8 @@ namespace storm { } template<> - void GmmxxMultiplier::multAddReduceHelper(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { + template + void GmmxxMultiplier::multAddReduceHelper(std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported for this data type."); } @@ -207,10 +218,10 @@ namespace storm { } #ifdef STORM_HAVE_INTELTBB - template + template class TbbMultAddReduceFunctor { public: - TbbMultAddReduceFunctor(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, gmm::csr_matrix const& matrix, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) : dir(dir), rowGroupIndices(rowGroupIndices), matrix(matrix), x(x), b(b), result(result), choices(choices) { + TbbMultAddReduceFunctor(std::vector const& rowGroupIndices, gmm::csr_matrix const& matrix, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) : dir(dir), rowGroupIndices(rowGroupIndices), matrix(matrix), x(x), b(b), result(result), choices(choices) { // Intentionally left empty. } @@ -265,7 +276,7 @@ namespace storm { ValueType newValue = b ? *bIt : storm::utility::zero(); newValue += vect_sp(gmm::linalg_traits::row(itr), x); - if (min ? newValue < currentValue : newValue > currentValue) { + if (compare(newValue, currentValue)) { currentValue = newValue; if (choices) { selectedChoice = currentRow - *groupIt; @@ -276,14 +287,14 @@ namespace storm { // Finally write value to target vector. *resultIt = currentValue; - if (choices && (min ? currentValue < oldSelectedChoiceValue : currentValue > oldSelectedChoiceValue)) { + if (choices && compare(currentValue, oldSelectedChoiceValue)) { *choiceIt = selectedChoice; } } } private: - storm::solver::OptimizationDirection dir; + Compare compare; std::vector const& rowGroupIndices; gmm::csr_matrix const& matrix; std::vector const& x; @@ -296,7 +307,11 @@ namespace storm { template void GmmxxMultiplier::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { #ifdef STORM_HAVE_INTELTBB - tbb::parallel_for(tbb::blocked_range(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor(dir, rowGroupIndices, this->gmmMatrix, x, b, result, choices)); + if (dir == storm::OptimizationDirection::Minimize) { + tbb::parallel_for(tbb::blocked_range(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor>(rowGroupIndices, this->gmmMatrix, x, b, result, choices)); + } else { + tbb::parallel_for(tbb::blocked_range(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor>(rowGroupIndices, this->gmmMatrix, x, b, result, choices)); + } #else STORM_LOG_WARN("Storm was built without support for Intel TBB, defaulting to sequential version."); multAddReduceHelper(dir, rowGroupIndices, x, b, result, choices); diff --git a/src/storm/solver/GmmxxMultiplier.h b/src/storm/solver/GmmxxMultiplier.h index fdebd557d..da70e2a05 100644 --- a/src/storm/solver/GmmxxMultiplier.h +++ b/src/storm/solver/GmmxxMultiplier.h @@ -27,6 +27,7 @@ namespace storm { virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices = nullptr) const override; virtual void multiplyRow(uint64_t const& rowIndex, std::vector const& x, ValueType& value) const override; virtual void clearCache() const override; + private: void initialize() const; @@ -37,6 +38,9 @@ namespace storm { void multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr) const; void multAddReduceHelper(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr) const; + template + void multAddReduceHelper(std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr) const; + mutable gmm::csr_matrix gmmMatrix; }; diff --git a/src/storm/solver/Multiplier.cpp b/src/storm/solver/Multiplier.cpp index 38d81fee4..3347ef2dc 100644 --- a/src/storm/solver/Multiplier.cpp +++ b/src/storm/solver/Multiplier.cpp @@ -73,7 +73,7 @@ namespace storm { STORM_LOG_INFO_COND(!changed, "Selecting '" + toString(type) + "' as the multiplier type to match the selected equation solver. If you want to override this, please explicitly specify a different multiplier type."); } - switch (env.solver().multiplier().getType()) { + switch (type) { case MultiplierType::Gmmxx: return std::make_unique>(matrix); case MultiplierType::Native: diff --git a/src/storm/solver/SymbolicGameSolver.cpp b/src/storm/solver/SymbolicGameSolver.cpp index 7ed466650..957a5de78 100644 --- a/src/storm/solver/SymbolicGameSolver.cpp +++ b/src/storm/solver/SymbolicGameSolver.cpp @@ -156,9 +156,11 @@ namespace storm { template class SymbolicGameSolver; template class SymbolicGameSolver; - + template class SymbolicGameSolver; + template class SymbolicGameSolverFactory; template class SymbolicGameSolverFactory; - + template class SymbolicGameSolverFactory; + } } diff --git a/src/storm/solver/SymbolicGameSolver.h b/src/storm/solver/SymbolicGameSolver.h index 69446f3d1..6ca502ef9 100644 --- a/src/storm/solver/SymbolicGameSolver.h +++ b/src/storm/solver/SymbolicGameSolver.h @@ -73,10 +73,10 @@ namespace storm { storm::dd::Bdd allRows; // An ADD that can be used to compensate for the illegal choices of player 1. - storm::dd::Add illegalPlayer1Mask; + storm::dd::Add illegalPlayer1Mask; // An ADD that can be used to compensate for the illegal choices of player 2. - storm::dd::Add illegalPlayer2Mask; + storm::dd::Add illegalPlayer2Mask; // The row variables. std::set rowMetaVariables; diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index e27fae045..24d9e55f7 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -1588,7 +1588,17 @@ namespace storm { template void SparseMatrix::multiplyAndReduceForward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices) const { - bool min = dir == OptimizationDirection::Minimize; + if (dir == OptimizationDirection::Minimize) { + multiplyAndReduceForward>(rowGroupIndices, vector, summand, result, choices); + } else { + multiplyAndReduceForward>(rowGroupIndices, vector, summand, result, choices); + } + } + + template + template + void SparseMatrix::multiplyAndReduceForward(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices) const { + Compare compare; auto elementIt = this->begin(); auto rowGroupIt = rowGroupIndices.begin(); auto rowIt = rowIndications.begin(); @@ -1600,7 +1610,7 @@ namespace storm { if (choices) { choiceIt = choices->begin(); } - + // Variables for correctly tracking choices (only update if new choice is strictly better). ValueType oldSelectedChoiceValue; uint64_t selectedChoice; @@ -1608,14 +1618,14 @@ namespace storm { uint64_t currentRow = 0; for (auto resultIt = result.begin(), resultIte = result.end(); resultIt != resultIte; ++resultIt, ++choiceIt, ++rowGroupIt) { ValueType currentValue = storm::utility::zero(); - + // Only multiply and reduce if there is at least one row in the group. if (*rowGroupIt < *(rowGroupIt + 1)) { if (summand) { currentValue = *summandIt; ++summandIt; } - + for (auto elementIte = this->begin() + *(rowIt + 1); elementIt != elementIte; ++elementIt) { currentValue += elementIt->getValue() * vector[elementIt->getColumn()]; } @@ -1640,7 +1650,7 @@ namespace storm { oldSelectedChoiceValue = newValue; } - if (min ? newValue < currentValue : newValue > currentValue) { + if (compare(newValue, currentValue)) { currentValue = newValue; if (choices) { selectedChoice = currentRow - *rowGroupIt; @@ -1650,16 +1660,16 @@ namespace storm { ++summandIt; } } - + // Finally write value to target vector. *resultIt = currentValue; - if (choices && (min ? currentValue < oldSelectedChoiceValue : currentValue > oldSelectedChoiceValue)) { + if (choices && compare(currentValue, oldSelectedChoiceValue)) { *choiceIt = selectedChoice; } } } } - + #ifdef STORM_HAVE_CARL template<> void SparseMatrix::multiplyAndReduceForward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices) const { @@ -1669,7 +1679,17 @@ namespace storm { template void SparseMatrix::multiplyAndReduceBackward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices) const { - bool min = dir == OptimizationDirection::Minimize; + if (dir == storm::OptimizationDirection::Minimize) { + multiplyAndReduceBackward>(rowGroupIndices, vector, summand, result, choices); + } else { + multiplyAndReduceBackward>(rowGroupIndices, vector, summand, result, choices); + } + } + + template + template + void SparseMatrix::multiplyAndReduceBackward(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices) const { + Compare compare; auto elementIt = this->end() - 1; auto rowGroupIt = rowGroupIndices.end() - 2; auto rowIt = rowIndications.end() - 2; @@ -1681,22 +1701,22 @@ namespace storm { if (choices) { choiceIt = choices->end() - 1; } - + // Variables for correctly tracking choices (only update if new choice is strictly better). ValueType oldSelectedChoiceValue; uint64_t selectedChoice; - + uint64_t currentRow = this->getRowCount() - 1; for (auto resultIt = result.end() - 1, resultIte = result.begin() - 1; resultIt != resultIte; --resultIt, --choiceIt, --rowGroupIt) { ValueType currentValue = storm::utility::zero(); - + // Only multiply and reduce if there is at least one row in the group. if (*rowGroupIt < *(rowGroupIt + 1)) { if (summand) { currentValue = *summandIt; --summandIt; } - + for (auto elementIte = this->begin() + *rowIt - 1; elementIt != elementIte; --elementIt) { currentValue += elementIt->getValue() * vector[elementIt->getColumn()]; } @@ -1719,17 +1739,17 @@ namespace storm { oldSelectedChoiceValue = newValue; } - if (min ? newValue < currentValue : newValue > currentValue) { + if (compare(newValue, currentValue)) { currentValue = newValue; if (choices) { selectedChoice = currentRow - *rowGroupIt; } } } - + // Finally write value to target vector. *resultIt = currentValue; - if (choices && (min ? currentValue < oldSelectedChoiceValue : currentValue > oldSelectedChoiceValue)) { + if (choices && compare(currentValue, oldSelectedChoiceValue)) { *choiceIt = selectedChoice; } } @@ -1744,14 +1764,14 @@ namespace storm { #endif #ifdef STORM_HAVE_INTELTBB - template + template class TbbMultAddReduceFunctor { public: typedef typename storm::storage::SparseMatrix::index_type index_type; typedef typename storm::storage::SparseMatrix::value_type value_type; typedef typename storm::storage::SparseMatrix::const_iterator const_iterator; - TbbMultAddReduceFunctor(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector> const& columnsAndEntries, std::vector const& rowIndications, std::vector const& x, std::vector& result, std::vector const* summand, std::vector* choices) : dir(dir), rowGroupIndices(rowGroupIndices), columnsAndEntries(columnsAndEntries), rowIndications(rowIndications), x(x), result(result), summand(summand), choices(choices) { + TbbMultAddReduceFunctor(std::vector const& rowGroupIndices, std::vector> const& columnsAndEntries, std::vector const& rowIndications, std::vector const& x, std::vector& result, std::vector const* summand, std::vector* choices) : dir(dir), rowGroupIndices(rowGroupIndices), columnsAndEntries(columnsAndEntries), rowIndications(rowIndications), x(x), result(result), summand(summand), choices(choices) { // Intentionally left empty. } @@ -1813,7 +1833,7 @@ namespace storm { oldSelectedChoiceValue = newValue; } - if (min ? newValue < currentValue : newValue > currentValue) { + if (compare(newValue, currentValue)) { currentValue = newValue; if (choices) { selectedChoice = currentRow - *groupIt; @@ -1823,7 +1843,7 @@ namespace storm { // Finally write value to target vector. *resultIt = currentValue; - if (choices && (min ? currentValue < oldSelectedChoiceValue : currentValue > oldSelectedChoiceValue)) { + if (choices && compare(currentValue, oldSelectedValue)) { *choiceIt = selectedChoice; } } @@ -1831,7 +1851,7 @@ namespace storm { } private: - OptimizationDirection dir; + Compare compare; std::vector const& rowGroupIndices; std::vector> const& columnsAndEntries; std::vector const& rowIndications; @@ -1843,7 +1863,11 @@ namespace storm { template void SparseMatrix::multiplyAndReduceParallel(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices) const { - tbb::parallel_for(tbb::blocked_range(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor(dir, rowGroupIndices, columnsAndValues, rowIndications, vector, result, summand, choices)); + if (dir == storm::OptimizationDirection::Minimize) { + tbb::parallel_for(tbb::blocked_range(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor>(rowGroupIndices, columnsAndValues, rowIndications, vector, result, summand, choices)); + } else { + tbb::parallel_for(tbb::blocked_range(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor>(rowGroupIndices, columnsAndValues, rowIndications, vector, result, summand, choices)); + } } #ifdef STORM_HAVE_CARL diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h index 9f9abd952..f742a7c49 100644 --- a/src/storm/storage/SparseMatrix.h +++ b/src/storm/storage/SparseMatrix.h @@ -859,9 +859,16 @@ namespace storm { void multiplyAndReduce(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices) const; void multiplyAndReduceForward(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices) const; + template + void multiplyAndReduceForward(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices) const; + void multiplyAndReduceBackward(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices) const; + template + void multiplyAndReduceBackward(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices) const; #ifdef STORM_HAVE_INTELTBB void multiplyAndReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices) const; + template + void multiplyAndReduceParallel(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices) const; #endif /*! diff --git a/src/storm/utility/ConstantsComparator.cpp b/src/storm/utility/ConstantsComparator.cpp index a4ed2e024..6d8318047 100644 --- a/src/storm/utility/ConstantsComparator.cpp +++ b/src/storm/utility/ConstantsComparator.cpp @@ -108,6 +108,52 @@ namespace storm { return value1 < value2 - precision; } + ConstantsComparator::ConstantsComparator() : precision(storm::utility::zero()), relative(false) { + // Intentionally left empty. + } + + ConstantsComparator::ConstantsComparator(storm::RationalNumber precision, bool relative) : precision(precision), relative(false) { + // Intentionally left empty. + } + + bool ConstantsComparator::isOne(storm::RationalNumber const& value) const { + if (storm::utility::isZero(precision)) { + return storm::utility::isOne(value); + } + return storm::utility::abs(value - one()) <= precision; + } + + bool ConstantsComparator::isZero(storm::RationalNumber const& value) const { + if (storm::utility::isZero(precision)) { + return storm::utility::isOne(value); + } + return storm::utility::abs(value) <= precision; + } + + bool ConstantsComparator::isEqual(storm::RationalNumber const& value1, storm::RationalNumber const& value2) const { + if (storm::utility::isZero(precision)) { + return value1 == value2; + } + + if (relative) { + return value1 == value2 || storm::utility::abs(value1 - value2)/storm::utility::abs(value1 + value2) <= precision; + } else { + return storm::utility::abs(value1 - value2) <= precision; + } + } + + bool ConstantsComparator::isConstant(storm::RationalNumber const& value) const { + return true; + } + + bool ConstantsComparator::isInfinity(storm::RationalNumber const& value) const { + return false; + } + + bool ConstantsComparator::isLess(storm::RationalNumber const& value1, storm::RationalNumber const& value2) const { + return value1 < value2 - precision; + } + // Explicit instantiations. template class ConstantsComparator; template class ConstantsComparator; diff --git a/src/storm/utility/ConstantsComparator.h b/src/storm/utility/ConstantsComparator.h index 9f32551f3..99f7cd625 100644 --- a/src/storm/utility/ConstantsComparator.h +++ b/src/storm/utility/ConstantsComparator.h @@ -77,6 +77,31 @@ namespace storm { // Whether to use relative comparison for equality. bool relative; }; + + // For rational numbers we specialize this class and consider the comparison modulo some predefined precision. + template<> + class ConstantsComparator { + public: + ConstantsComparator(); + + ConstantsComparator(storm::RationalNumber precision, bool relative); + + bool isOne(storm::RationalNumber const& value) const; + + bool isZero(storm::RationalNumber const& value) const; + + bool isEqual(storm::RationalNumber const& value1, storm::RationalNumber const& value2) const; + + bool isConstant(storm::RationalNumber const& value) const; + + bool isInfinity(storm::RationalNumber const& value) const; + + bool isLess(storm::RationalNumber const& value1, storm::RationalNumber const& value2) const; + + private: + storm::RationalNumber precision; + bool relative; + }; } } diff --git a/src/storm/utility/shortestPaths.cpp b/src/storm/utility/shortestPaths.cpp index 8432ce1a5..b18e309d4 100644 --- a/src/storm/utility/shortestPaths.cpp +++ b/src/storm/utility/shortestPaths.cpp @@ -377,6 +377,7 @@ namespace storm { template class ShortestPathsGenerator; + template class ShortestPathsGenerator; // only prints the info stored in the Path struct; // does not traverse the actual path (see printKShortestPath for that)