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

renamed prob branching variables to aux variables in preparation for proper bottom state creation in game abstraction 

Former-commit-id: e855b14b46
main
dehnert 9 years ago
parent
1be735ec1b
commit
1280c88b4f
4 changed files with 52 additions and 48 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. 47
      src/abstraction/AbstractionInformation.cpp
  2. 41
      src/abstraction/AbstractionInformation.h
  3. 6
      src/abstraction/prism/AbstractCommand.cpp
  4. 6
      src/abstraction/prism/AbstractProgram.cpp

47
src/abstraction/AbstractionInformation.cpp
View File

@ -129,44 +129,44 @@ namespace storm {
}
template<storm::dd::DdType DdType>
void AbstractionInformation<DdType>::createEncodingVariables(uint64_t player1VariableCount, uint64_t player2VariableCount, uint64_t probabilisticBranchingVariableCount) {
STORM_LOG_THROW(player1Variables.empty() && player2Variables.empty() && probabilisticBranchingVariables.empty(), storm::exceptions::InvalidOperationException, "Variables have already been created.");
void AbstractionInformation<DdType>::createEncodingVariables(uint64_t player1VariableCount, uint64_t player2VariableCount, uint64_t auxVariableCount) {
STORM_LOG_THROW(player1Variables.empty() && player2Variables.empty() && auxVariables.empty(), storm::exceptions::InvalidOperationException, "Variables have already been created.");
for (uint64_t index = 0; index < player1VariableCount; ++index) {
storm::expressions::Variable newVariable = ddManager->addMetaVariable("pl1_" + std::to_string(index)).first;
storm::expressions::Variable newVariable = ddManager->addMetaVariable("pl1." + std::to_string(index)).first;
player1Variables.push_back(newVariable);
player1VariableBdds.push_back(ddManager->getEncoding(newVariable, 1));
}
STORM_LOG_DEBUG("Created " << player1VariableCount << " player 1 variables.");
for (uint64_t index = 0; index < player2VariableCount; ++index) {
storm::expressions::Variable newVariable = ddManager->addMetaVariable("pl2_" + std::to_string(index)).first;
storm::expressions::Variable newVariable = ddManager->addMetaVariable("pl2." + std::to_string(index)).first;
player2Variables.push_back(newVariable);
player2VariableBdds.push_back(ddManager->getEncoding(newVariable, 1));
}
STORM_LOG_DEBUG("Created " << player2VariableCount << " player 2 variables.");
for (uint64_t index = 0; index < probabilisticBranchingVariableCount; ++index) {
storm::expressions::Variable newVariable = ddManager->addMetaVariable("pb_" + std::to_string(index)).first;
probabilisticBranchingVariables.push_back(newVariable);
probabilisticBranchingVariableBdds.push_back(ddManager->getEncoding(newVariable, 1));
for (uint64_t index = 0; index < auxVariableCount; ++index) {
storm::expressions::Variable newVariable = ddManager->addMetaVariable("aux_" + std::to_string(index)).first;
auxVariables.push_back(newVariable);
auxVariableBdds.push_back(ddManager->getEncoding(newVariable, 1));
}
STORM_LOG_DEBUG("Created " << probabilisticBranchingVariableCount << " probabilistic branching variables.");
STORM_LOG_DEBUG("Created " << auxVariableCount << " auxiliary variables.");
}
template<storm::dd::DdType DdType>
storm::dd::Bdd<DdType> AbstractionInformation<DdType>::encodePlayer1Choice(uint_fast64_t index, uint_fast64_t numberOfVariables) const {
return encodeChoice(index, numberOfVariables, player1VariableBdds);
return encodeChoice(index, 0, numberOfVariables, player1VariableBdds);
}
template<storm::dd::DdType DdType>
storm::dd::Bdd<DdType> AbstractionInformation<DdType>::encodePlayer2Choice(uint_fast64_t index, uint_fast64_t numberOfVariables) const {
return encodeChoice(index, numberOfVariables, player2VariableBdds);
return encodeChoice(index, 0, numberOfVariables, player2VariableBdds);
}
template<storm::dd::DdType DdType>
storm::dd::Bdd<DdType> AbstractionInformation<DdType>::encodeProbabilisticChoice(uint_fast64_t index, uint_fast64_t numberOfVariables) const {
return encodeChoice(index, numberOfVariables, probabilisticBranchingVariableBdds);
storm::dd::Bdd<DdType> AbstractionInformation<DdType>::encodeAux(uint_fast64_t index, uint_fast64_t offset, uint_fast64_t numberOfVariables) const {
return encodeChoice(index, offset, numberOfVariables, auxVariableBdds);
}
template<storm::dd::DdType DdType>
@ -200,13 +200,13 @@ namespace storm {
}
template<storm::dd::DdType DdType>
std::vector<storm::expressions::Variable> const& AbstractionInformation<DdType>::getProbabilisticBranchingVariables() const {
return probabilisticBranchingVariables;
std::vector<storm::expressions::Variable> const& AbstractionInformation<DdType>::getAuxVariables() const {
return auxVariables;
}
template<storm::dd::DdType DdType>
std::set<storm::expressions::Variable> AbstractionInformation<DdType>::getProbabilisticBranchingVariableSet(uint_fast64_t count) const {
return std::set<storm::expressions::Variable>(probabilisticBranchingVariables.begin(), probabilisticBranchingVariables.begin() + count);
std::set<storm::expressions::Variable> AbstractionInformation<DdType>::getAuxVariableSet(uint_fast64_t offset, uint_fast64_t count) const {
return std::set<storm::expressions::Variable>(auxVariables.begin() + offset, auxVariables.begin() + offset + count);
}
template<storm::dd::DdType DdType>
@ -235,8 +235,8 @@ namespace storm {
}
template<storm::dd::DdType DdType>
std::size_t AbstractionInformation<DdType>::getProbabilisticBranchingVariableCount() const {
return probabilisticBranchingVariables.size();
std::size_t AbstractionInformation<DdType>::getAuxVariableCount() const {
return auxVariables.size();
}
template<storm::dd::DdType DdType>
@ -298,13 +298,14 @@ namespace storm {
}
template<storm::dd::DdType DdType>
storm::dd::Bdd<DdType> AbstractionInformation<DdType>::encodeChoice(uint_fast64_t index, uint_fast64_t numberOfVariables, std::vector<storm::dd::Bdd<DdType>> const& variables) const {
storm::dd::Bdd<DdType> AbstractionInformation<DdType>::encodeChoice(uint_fast64_t index, uint_fast64_t offset, uint_fast64_t numberOfVariables, std::vector<storm::dd::Bdd<DdType>> const& variables) const {
storm::dd::Bdd<DdType> result = ddManager->getBddOne();
for (uint_fast64_t bitIndex = 0; bitIndex < numberOfVariables; ++bitIndex) {
numberOfVariables += offset;
for (uint_fast64_t bitIndex = numberOfVariables; bitIndex > offset; --bitIndex) {
if ((index & 1) != 0) {
result &= variables[bitIndex];
result &= variables[bitIndex - 1];
} else {
result &= !variables[bitIndex];
result &= !variables[bitIndex - 1];
}
index >>= 1;
}

41
src/abstraction/AbstractionInformation.h
View File

@ -162,13 +162,13 @@ namespace storm {
std::set<storm::expressions::Variable> const& getVariables() const;
/*!
* Creates the given number of variables used to encode the choices of player 1/2 and probabilistic branching.
* Creates the given number of variables used to encode the choices of player 1/2 and auxiliary information.
*
* @param player1VariableCount The number of variables to use for encoding player 1 choices.
* @param player2VariableCount The number of variables to use for encoding player 2 choices.
* @param probabilisticBranchingVariableCount The number of variables to use for encoding probabilistic branching.
* @param auxVariableCount The number of variables to use for encoding auxiliary information.
*/
void createEncodingVariables(uint64_t player1VariableCount, uint64_t player2VariableCount, uint64_t probabilisticBranchingVariableCount);
void createEncodingVariables(uint64_t player1VariableCount, uint64_t player2VariableCount, uint64_t auxVariableCount);
/*!
* Encodes the given index using the indicated player 1 variables.
@ -192,10 +192,11 @@ namespace storm {
* Encodes the given index using the indicated probabilistic branching variables.
*
* @param index The index to encode.
* @param offset The offset within the auxiliary variables at which to start encoding.
* @param numberOfVariables The number of variables to use for encoding the index.
* @return The index encoded as a BDD.
*/
storm::dd::Bdd<DdType> encodeProbabilisticChoice(uint_fast64_t index, uint_fast64_t numberOfVariables) const;
storm::dd::Bdd<DdType> encodeAux(uint_fast64_t index, uint_fast64_t offset, uint_fast64_t numberOfVariables) const;
/*!
* Retrieves the cube of player 2 variables in the given range [offset, numberOfVariables).
@ -252,26 +253,27 @@ namespace storm {
std::set<storm::expressions::Variable> getPlayer2VariableSet(uint_fast64_t count) const;
/*!
* Retrieves the meta variables associated with the probabilistic branching.
* Retrieves the meta variables associated with auxiliary information.
*
* @return The meta variables associated with the probabilistic branching.
* @return The meta variables associated with auxiliary information.
*/
std::vector<storm::expressions::Variable> const& getProbabilisticBranchingVariables() const;
std::vector<storm::expressions::Variable> const& getAuxVariables() const;
/*!
* Retrieves the set of probabilistic branching variables.
* Retrieves the requested set of auxiliary variables.
*
* @param count The number of probabilistic branching variables to include.
* @return The set of probabilistic branching variables.
* @param offset The offset at which to start gatherin the auxiliary variables.
* @param count The number of auxiliary variables to include.
* @return The set of auxiliary variables.
*/
std::set<storm::expressions::Variable> getProbabilisticBranchingVariableSet(uint_fast64_t count) const;
std::set<storm::expressions::Variable> getAuxVariableSet(uint_fast64_t offset, uint_fast64_t count) const;
/*!
* Retrieves the number of probabilistic branching variables.
* Retrieves the number of auxiliary variables.
*
* @return The number of probabilistic branching variables.
* @return The number of auxiliary variables.
*/
std::size_t getProbabilisticBranchingVariableCount() const;
std::size_t getAuxVariableCount() const;
/*!
* Retrieves the set of source meta variables.
@ -354,10 +356,11 @@ namespace storm {
* Encodes the given index with the given number of variables from the given variables.
*
* @param index The index to encode.
* @param offset The offset at which to start encoding.
* @param numberOfVariables The total number of variables to use.
* @param variables The BDDs of the variables to use to encode the index.
*/
storm::dd::Bdd<DdType> encodeChoice(uint_fast64_t index, uint_fast64_t numberOfVariables, std::vector<storm::dd::Bdd<DdType>> const& variables) const;
storm::dd::Bdd<DdType> encodeChoice(uint_fast64_t index, uint_fast64_t offset, uint_fast64_t numberOfVariables, std::vector<storm::dd::Bdd<DdType>> const& variables) const;
// The expression related data.
@ -415,11 +418,11 @@ namespace storm {
/// The BDDs associated with the meta variables of player 2.
std::vector<storm::dd::Bdd<DdType>> player2VariableBdds;
/// Variables that can be used to encode the probabilistic branching.
std::vector<storm::expressions::Variable> probabilisticBranchingVariables;
/// Variables that can be used to encode auxiliary information.
std::vector<storm::expressions::Variable> auxVariables;
/// The BDDs associated with the meta variables encoding the probabilistic branching.
std::vector<storm::dd::Bdd<DdType>> probabilisticBranchingVariableBdds;
/// The BDDs associated with the meta variables encoding auxiliary information.
std::vector<storm::dd::Bdd<DdType>> auxVariableBdds;
};
}

6
src/abstraction/prism/AbstractCommand.cpp
View File

@ -226,7 +226,7 @@ namespace storm {
} else {
updateBdd &= !this->getAbstractionInformation().encodePredicateAsSuccessor(variableIndexPair.second);
}
updateBdd &= this->getAbstractionInformation().encodeProbabilisticChoice(updateIndex, this->getAbstractionInformation().getProbabilisticBranchingVariableCount());
updateBdd &= this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount());
}
result |= updateBdd;
@ -265,7 +265,7 @@ namespace storm {
}
}
result |= updateIdentity && this->getAbstractionInformation().encodeProbabilisticChoice(updateIndex, this->getAbstractionInformation().getProbabilisticBranchingVariableCount());
result |= updateIdentity && this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount());
}
return result;
}
@ -295,7 +295,7 @@ namespace storm {
storm::dd::Add<DdType, ValueType> AbstractCommand<DdType, ValueType>::getCommandUpdateProbabilitiesAdd() const {
storm::dd::Add<DdType, ValueType> result = this->getAbstractionInformation().getDdManager().template getAddZero<ValueType>();
for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) {
result += this->getAbstractionInformation().encodeProbabilisticChoice(updateIndex, this->getAbstractionInformation().getProbabilisticBranchingVariableCount()).template toAdd<ValueType>() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(command.get().getUpdate(updateIndex).getLikelihoodExpression()));
result += this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()).template toAdd<ValueType>() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(command.get().getUpdate(updateIndex).getLikelihoodExpression()));
}
result *= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()).template toAdd<ValueType>();
return result;

6
src/abstraction/prism/AbstractProgram.cpp
View File

@ -132,7 +132,7 @@ namespace storm {
std::set<storm::expressions::Variable> variablesToAbstract(abstractionInformation.getPlayer1VariableSet(abstractionInformation.getPlayer1VariableCount()));
auto player2Variables = abstractionInformation.getPlayer2VariableSet(gameBdd.second);
variablesToAbstract.insert(player2Variables.begin(), player2Variables.end());
auto probBranchingVariables = abstractionInformation.getProbabilisticBranchingVariableSet(abstractionInformation.getProbabilisticBranchingVariableCount());
auto probBranchingVariables = abstractionInformation.getAuxVariableSet(0, abstractionInformation.getAuxVariableCount());
variablesToAbstract.insert(probBranchingVariables.begin(), probBranchingVariables.end());
// Do a reachability analysis on the raw transition relation.
@ -156,7 +156,7 @@ namespace storm {
// If there are deadlock states, we fix them now.
storm::dd::Add<DdType, ValueType> deadlockTransitions = abstractionInformation.getDdManager().template getAddZero<ValueType>();
if (!deadlockStates.isZero()) {
deadlockTransitions = (deadlockStates && abstractionInformation.getAllPredicateIdentities() && abstractionInformation.encodePlayer1Choice(0, abstractionInformation.getPlayer1VariableCount()) && abstractionInformation.encodePlayer2Choice(0, gameBdd.second) && abstractionInformation.encodeProbabilisticChoice(0, abstractionInformation.getProbabilisticBranchingVariableCount())).template toAdd<ValueType>();
deadlockTransitions = (deadlockStates && abstractionInformation.getAllPredicateIdentities() && abstractionInformation.encodePlayer1Choice(0, abstractionInformation.getPlayer1VariableCount()) && abstractionInformation.encodePlayer2Choice(0, gameBdd.second) && abstractionInformation.encodeAux(0, 0, abstractionInformation.getAuxVariableCount())).template toAdd<ValueType>();
}
// Construct the transition matrix by cutting away the transitions of unreachable states.
@ -167,7 +167,7 @@ namespace storm {
std::set<storm::expressions::Variable> allNondeterminismVariables = usedPlayer2Variables;
allNondeterminismVariables.insert(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end());
return std::make_unique<MenuGame<DdType, ValueType>>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStates, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables(), abstractionInformation.getSourceSuccessorVariablePairs(), std::set<storm::expressions::Variable>(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, std::set<storm::expressions::Variable>(abstractionInformation.getProbabilisticBranchingVariables().begin(), abstractionInformation.getProbabilisticBranchingVariables().end()), abstractionInformation.getPredicateToBddMap());
return std::make_unique<MenuGame<DdType, ValueType>>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStates, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables(), abstractionInformation.getSourceSuccessorVariablePairs(), std::set<storm::expressions::Variable>(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, std::set<storm::expressions::Variable>(abstractionInformation.getAuxVariables().begin(), abstractionInformation.getAuxVariables().end()), abstractionInformation.getPredicateToBddMap());
}
template <storm::dd::DdType DdType, typename ValueType>

Write Preview
Loading…
Cancel
Save