From 4733643bcf2a22b7c2e68456590e8aa6ed742c9b Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 2 Aug 2016 14:22:27 +0200 Subject: [PATCH] made the games compile again Former-commit-id: 35f3ab947134ca21529cd281a72a43b94380e06d --- src/builder/DdPrismModelBuilder.cpp | 4 --- src/models/symbolic/NondeterministicModel.cpp | 2 +- .../symbolic/StochasticTwoPlayerGame.cpp | 31 +++++++++-------- src/settings/modules/ResourceSettings.h | 7 ++-- src/storage/prism/Program.cpp | 34 ------------------- .../prism/menu_games/AbstractProgram.cpp | 3 +- src/storage/prism/menu_games/MenuGame.cpp | 3 +- src/storage/prism/menu_games/MenuGame.h | 2 ++ 8 files changed, 26 insertions(+), 60 deletions(-) diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index 765bfec19..a397b0de0 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -523,10 +523,6 @@ namespace storm { template void DdPrismModelBuilder::Options::setTerminalStatesFromFormula(storm::logic::Formula const& formula) { - // If cutting the model was disabled, we do not set anything. - if (storm::settings::generalSettings().isNoCutsSet()) { - return; - } if (formula.isAtomicExpressionFormula()) { terminalStates = formula.asAtomicExpressionFormula().getExpression(); } else if (formula.isAtomicLabelFormula()) { diff --git a/src/models/symbolic/NondeterministicModel.cpp b/src/models/symbolic/NondeterministicModel.cpp index ae6906776..da3607d02 100644 --- a/src/models/symbolic/NondeterministicModel.cpp +++ b/src/models/symbolic/NondeterministicModel.cpp @@ -25,7 +25,7 @@ namespace storm { std::set const& nondeterminismVariables, std::map labelToExpressionMap, std::unordered_map const& rewardModels) - : Model(modelType, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels), nondeterminismVariables(nondeterminismVariables) { + : Model(modelType, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels), nondeterminismVariables(nondeterminismVariables) { // Prepare the mask of illegal nondeterministic choices. illegalMask = !(transitionMatrix.notZero().existsAbstract(this->getColumnVariables())) && reachableStates; diff --git a/src/models/symbolic/StochasticTwoPlayerGame.cpp b/src/models/symbolic/StochasticTwoPlayerGame.cpp index ec14b07f4..e945b85d6 100644 --- a/src/models/symbolic/StochasticTwoPlayerGame.cpp +++ b/src/models/symbolic/StochasticTwoPlayerGame.cpp @@ -12,24 +12,25 @@ namespace storm { template StochasticTwoPlayerGame::StochasticTwoPlayerGame(std::shared_ptr> manager, - storm::dd::Bdd reachableStates, - storm::dd::Bdd initialStates, - storm::dd::Add transitionMatrix, - std::set const& rowVariables, - std::shared_ptr> rowExpressionAdapter, - std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, - std::vector> const& rowColumnMetaVariablePairs, - std::set const& player1Variables, - std::set const& player2Variables, - std::set const& nondeterminismVariables, - std::map labelToExpressionMap, - std::unordered_map const& rewardModels) - : NondeterministicModel(storm::models::ModelType::S2pg, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, nondeterminismVariables, labelToExpressionMap, rewardModels), player1Variables(player1Variables), player2Variables(player2Variables) { + storm::dd::Bdd reachableStates, + storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, + storm::dd::Add transitionMatrix, + std::set const& rowVariables, + std::shared_ptr> rowExpressionAdapter, + std::set const& columnVariables, + std::shared_ptr> columnExpressionAdapter, + std::vector> const& rowColumnMetaVariablePairs, + std::set const& player1Variables, + std::set const& player2Variables, + std::set const& nondeterminismVariables, + std::map labelToExpressionMap, + std::unordered_map const& rewardModels) + : NondeterministicModel(storm::models::ModelType::S2pg, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, nondeterminismVariables, labelToExpressionMap, rewardModels), player1Variables(player1Variables), player2Variables(player2Variables) { // Compute legal player 1 mask. illegalPlayer1Mask = transitionMatrix.notZero().existsAbstract(this->getColumnVariables()).existsAbstract(this->getPlayer2Variables()); - + // Correct the mask for player 2. This is necessary, because it is not yet restricted to the legal choices of player 1. this->illegalMask &= illegalPlayer1Mask; diff --git a/src/settings/modules/ResourceSettings.h b/src/settings/modules/ResourceSettings.h index 48be822c4..8c76346ed 100644 --- a/src/settings/modules/ResourceSettings.h +++ b/src/settings/modules/ResourceSettings.h @@ -1,5 +1,4 @@ -#ifndef STORM_SETTINGS_MODULES_RESOURCESETTINGS_H_ -#define STORM_SETTINGS_MODULES_RESOURCESETTINGS_H_ +#pragma once #include "storm-config.h" #include "src/settings/modules/ModuleSettings.h" @@ -40,7 +39,7 @@ namespace storm { // Define the string names of the options as constants. static const std::string timeoutOptionName; static const std::string timeoutOptionShortName; - } + }; } } -} \ No newline at end of file +} diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 14fddacc2..d1551eef9 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -384,40 +384,6 @@ namespace storm { return result; } - std::set Program::getAllExpressionVariables() const { - std::set result; - - for (auto const& constant : constants) { - result.insert(constant.getExpressionVariable()); - } - for (auto const& variable : globalBooleanVariables) { - result.insert(variable.getExpressionVariable()); - } - for (auto const& variable : globalIntegerVariables) { - result.insert(variable.getExpressionVariable()); - } - for (auto const& module : modules) { - auto const& moduleVariables = module.getAllExpressionVariables(); - result.insert(moduleVariables.begin(), moduleVariables.end()); - } - - return result; - } - - std::vector Program::getAllRangeExpressions() const { - std::vector result; - for (auto const& globalIntegerVariable : this->globalIntegerVariables) { - result.push_back(globalIntegerVariable.getRangeExpression()); - } - - for (auto const& module : modules) { - std::vector moduleRangeExpressions = module.getAllRangeExpressions(); - result.insert(result.end(), moduleRangeExpressions.begin(), moduleRangeExpressions.end()); - } - - return result; - } - bool Program::globalBooleanVariableExists(std::string const& variableName) const { return this->globalBooleanVariableToIndexMap.count(variableName) > 0; } diff --git a/src/storage/prism/menu_games/AbstractProgram.cpp b/src/storage/prism/menu_games/AbstractProgram.cpp index fd2403a91..e8ec36ea7 100644 --- a/src/storage/prism/menu_games/AbstractProgram.cpp +++ b/src/storage/prism/menu_games/AbstractProgram.cpp @@ -176,7 +176,8 @@ namespace storm { std::set allNondeterminismVariables = usedPlayer2Variables; allNondeterminismVariables.insert(ddInformation.commandDdVariable); - return std::unique_ptr>(new MenuGame(ddInformation.manager, reachableStates, initialStates, transitionMatrix, bottomStates, ddInformation.sourceVariables, ddInformation.successorVariables, ddInformation.predicateDdVariables, {ddInformation.commandDdVariable}, usedPlayer2Variables, allNondeterminismVariables, ddInformation.updateDdVariable, ddInformation.expressionToBddMap)); + // FIXME: no deadlock states guaranteed? + return std::unique_ptr>(new MenuGame(ddInformation.manager, reachableStates, initialStates, ddInformation.manager->getBddZero(), transitionMatrix, bottomStates, ddInformation.sourceVariables, ddInformation.successorVariables, ddInformation.predicateDdVariables, {ddInformation.commandDdVariable}, usedPlayer2Variables, allNondeterminismVariables, ddInformation.updateDdVariable, ddInformation.expressionToBddMap)); } template diff --git a/src/storage/prism/menu_games/MenuGame.cpp b/src/storage/prism/menu_games/MenuGame.cpp index 69e5ad83b..38967f7ee 100644 --- a/src/storage/prism/menu_games/MenuGame.cpp +++ b/src/storage/prism/menu_games/MenuGame.cpp @@ -16,6 +16,7 @@ namespace storm { MenuGame::MenuGame(std::shared_ptr> manager, storm::dd::Bdd reachableStates, storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, storm::dd::Add transitionMatrix, storm::dd::Bdd bottomStates, std::set const& rowVariables, @@ -25,7 +26,7 @@ namespace storm { std::set const& player2Variables, std::set const& allNondeterminismVariables, storm::expressions::Variable const& updateVariable, - std::map> const& expressionToBddMap) : storm::models::symbolic::StochasticTwoPlayerGame(manager, reachableStates, initialStates, transitionMatrix.sumAbstract({updateVariable}), rowVariables, nullptr, columnVariables, nullptr, rowColumnMetaVariablePairs, player1Variables, player2Variables, allNondeterminismVariables), updateVariable(updateVariable), expressionToBddMap(expressionToBddMap), bottomStates(bottomStates) { + std::map> const& expressionToBddMap) : storm::models::symbolic::StochasticTwoPlayerGame(manager, reachableStates, initialStates, deadlockStates, transitionMatrix.sumAbstract({updateVariable}), rowVariables, nullptr, columnVariables, nullptr, rowColumnMetaVariablePairs, player1Variables, player2Variables, allNondeterminismVariables), updateVariable(updateVariable), expressionToBddMap(expressionToBddMap), bottomStates(bottomStates) { // Intentionally left empty. } diff --git a/src/storage/prism/menu_games/MenuGame.h b/src/storage/prism/menu_games/MenuGame.h index d47e11c7a..fbec4e062 100644 --- a/src/storage/prism/menu_games/MenuGame.h +++ b/src/storage/prism/menu_games/MenuGame.h @@ -33,6 +33,7 @@ namespace storm { * @param manager The manager responsible for the decision diagrams. * @param reachableStates The reachable states of the model. * @param initialStates The initial states of the model. + * @param deadlockStates The deadlock states of the model. * @param transitionMatrix The matrix representing the transitions in the model. * @param bottomStates The bottom states of the model. * @param rowVariables The set of row meta variables used in the DDs. @@ -48,6 +49,7 @@ namespace storm { MenuGame(std::shared_ptr> manager, storm::dd::Bdd reachableStates, storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, storm::dd::Add transitionMatrix, storm::dd::Bdd bottomStates, std::set const& rowVariables,