sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

made the games compile again 

Former-commit-id: 35f3ab9471
tempestpy_adaptions
dehnert 9 years ago
parent
6bee853a5a
commit
4733643bcf
8 changed files with 26 additions and 60 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      src/builder/DdPrismModelBuilder.cpp
  2. 2
      src/models/symbolic/NondeterministicModel.cpp
  3. 31
      src/models/symbolic/StochasticTwoPlayerGame.cpp
  4. 7
      src/settings/modules/ResourceSettings.h
  5. 34
      src/storage/prism/Program.cpp
  6. 3
      src/storage/prism/menu_games/AbstractProgram.cpp
  7. 3
      src/storage/prism/menu_games/MenuGame.cpp
  8. 2
      src/storage/prism/menu_games/MenuGame.h

4
src/builder/DdPrismModelBuilder.cpp
View File

@ -523,10 +523,6 @@ namespace storm {
template <storm::dd::DdType Type, typename ValueType>
void DdPrismModelBuilder<Type, ValueType>::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()) {

2
src/models/symbolic/NondeterministicModel.cpp
View File

@ -25,7 +25,7 @@ namespace storm {
std::set<storm::expressions::Variable> const& nondeterminismVariables,
std::map<std::string, storm::expressions::Expression> labelToExpressionMap,
std::unordered_map<std::string, RewardModelType> const& rewardModels)
: Model<Type, ValueType>(modelType, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels), nondeterminismVariables(nondeterminismVariables) {
: Model<Type, ValueType>(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;

31
src/models/symbolic/StochasticTwoPlayerGame.cpp
View File

@ -12,24 +12,25 @@ namespace storm {
template<storm::dd::DdType Type, typename ValueType>
StochasticTwoPlayerGame<Type, ValueType>::StochasticTwoPlayerGame(std::shared_ptr<storm::dd::DdManager<Type>> manager,
storm::dd::Bdd<Type> reachableStates,
storm::dd::Bdd<Type> initialStates,
storm::dd::Add<Type, ValueType> transitionMatrix,
std::set<storm::expressions::Variable> const& rowVariables,
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> rowExpressionAdapter,
std::set<storm::expressions::Variable> const& columnVariables,
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> columnExpressionAdapter,
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
std::set<storm::expressions::Variable> const& player1Variables,
std::set<storm::expressions::Variable> const& player2Variables,
std::set<storm::expressions::Variable> const& nondeterminismVariables,
std::map<std::string, storm::expressions::Expression> labelToExpressionMap,
std::unordered_map<std::string, RewardModelType> const& rewardModels)
: NondeterministicModel<Type, ValueType>(storm::models::ModelType::S2pg, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, nondeterminismVariables, labelToExpressionMap, rewardModels), player1Variables(player1Variables), player2Variables(player2Variables) {
storm::dd::Bdd<Type> reachableStates,
storm::dd::Bdd<Type> initialStates,
storm::dd::Bdd<Type> deadlockStates,
storm::dd::Add<Type, ValueType> transitionMatrix,
std::set<storm::expressions::Variable> const& rowVariables,
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> rowExpressionAdapter,
std::set<storm::expressions::Variable> const& columnVariables,
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> columnExpressionAdapter,
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
std::set<storm::expressions::Variable> const& player1Variables,
std::set<storm::expressions::Variable> const& player2Variables,
std::set<storm::expressions::Variable> const& nondeterminismVariables,
std::map<std::string, storm::expressions::Expression> labelToExpressionMap,
std::unordered_map<std::string, RewardModelType> const& rewardModels)
: NondeterministicModel<Type, ValueType>(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;

7
src/settings/modules/ResourceSettings.h
View File

@ -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;
}
};
}
}
}
}

34
src/storage/prism/Program.cpp
View File

@ -384,40 +384,6 @@ namespace storm {
return result;
}
std::set<storm::expressions::Variable> Program::getAllExpressionVariables() const {
std::set<storm::expressions::Variable> 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<storm::expressions::Expression> Program::getAllRangeExpressions() const {
std::vector<storm::expressions::Expression> result;
for (auto const& globalIntegerVariable : this->globalIntegerVariables) {
result.push_back(globalIntegerVariable.getRangeExpression());
}
for (auto const& module : modules) {
std::vector<storm::expressions::Expression> 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;
}

3
src/storage/prism/menu_games/AbstractProgram.cpp
View File

@ -176,7 +176,8 @@ namespace storm {
std::set<storm::expressions::Variable> allNondeterminismVariables = usedPlayer2Variables;
allNondeterminismVariables.insert(ddInformation.commandDdVariable);
return std::unique_ptr<MenuGame<DdType, ValueType>>(new MenuGame<DdType, ValueType>(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<MenuGame<DdType, ValueType>>(new MenuGame<DdType, ValueType>(ddInformation.manager, reachableStates, initialStates, ddInformation.manager->getBddZero(), transitionMatrix, bottomStates, ddInformation.sourceVariables, ddInformation.successorVariables, ddInformation.predicateDdVariables, {ddInformation.commandDdVariable}, usedPlayer2Variables, allNondeterminismVariables, ddInformation.updateDdVariable, ddInformation.expressionToBddMap));
}
template <storm::dd::DdType DdType, typename ValueType>

3
src/storage/prism/menu_games/MenuGame.cpp
View File

@ -16,6 +16,7 @@ namespace storm {
MenuGame<Type, ValueType>::MenuGame(std::shared_ptr<storm::dd::DdManager<Type>> manager,
storm::dd::Bdd<Type> reachableStates,
storm::dd::Bdd<Type> initialStates,
storm::dd::Bdd<Type> deadlockStates,
storm::dd::Add<Type, ValueType> transitionMatrix,
storm::dd::Bdd<Type> bottomStates,
std::set<storm::expressions::Variable> const& rowVariables,
@ -25,7 +26,7 @@ namespace storm {
std::set<storm::expressions::Variable> const& player2Variables,
std::set<storm::expressions::Variable> const& allNondeterminismVariables,
storm::expressions::Variable const& updateVariable,
std::map<storm::expressions::Expression, storm::dd::Bdd<Type>> const& expressionToBddMap) : storm::models::symbolic::StochasticTwoPlayerGame<Type>(manager, reachableStates, initialStates, transitionMatrix.sumAbstract({updateVariable}), rowVariables, nullptr, columnVariables, nullptr, rowColumnMetaVariablePairs, player1Variables, player2Variables, allNondeterminismVariables), updateVariable(updateVariable), expressionToBddMap(expressionToBddMap), bottomStates(bottomStates) {
std::map<storm::expressions::Expression, storm::dd::Bdd<Type>> const& expressionToBddMap) : storm::models::symbolic::StochasticTwoPlayerGame<Type>(manager, reachableStates, initialStates, deadlockStates, transitionMatrix.sumAbstract({updateVariable}), rowVariables, nullptr, columnVariables, nullptr, rowColumnMetaVariablePairs, player1Variables, player2Variables, allNondeterminismVariables), updateVariable(updateVariable), expressionToBddMap(expressionToBddMap), bottomStates(bottomStates) {
// Intentionally left empty.
}

2
src/storage/prism/menu_games/MenuGame.h
View File

@ -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<storm::dd::DdManager<Type>> manager,
storm::dd::Bdd<Type> reachableStates,
storm::dd::Bdd<Type> initialStates,
storm::dd::Bdd<Type> deadlockStates,
storm::dd::Add<Type, ValueType> transitionMatrix,
storm::dd::Bdd<Type> bottomStates,
std::set<storm::expressions::Variable> const& rowVariables,

Write Preview
Loading…
Cancel
Save