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

removed or and not operation on ADDs as they should conceptually be used on BDDs 

Former-commit-id: 860ed79637
main
dehnert 9 years ago
parent
2c69232560
commit
31147a90d2
7 changed files with 7 additions and 133 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. 8
      src/builder/DdPrismModelBuilder.cpp
  2. 17
      src/storage/dd/Add.cpp
  3. 26
      src/storage/dd/Add.h
  4. 18
      src/storage/dd/cudd/InternalCuddAdd.cpp
  5. 26
      src/storage/dd/cudd/InternalCuddAdd.h
  6. 17
      src/storage/dd/sylvan/InternalSylvanAdd.cpp
  7. 28
      src/storage/dd/sylvan/InternalSylvanAdd.h

8
src/builder/DdPrismModelBuilder.cpp
View File

@ -543,7 +543,7 @@ namespace storm {
template <storm::dd::DdType Type, typename ValueType>
typename DdPrismModelBuilder<Type, ValueType>::ActionDecisionDiagram DdPrismModelBuilder<Type, ValueType>::combineCommandsToActionMDP(GenerationInformation& generationInfo, std::vector<ActionDecisionDiagram>& commandDds, uint_fast64_t nondeterminismVariableOffset) {
storm::dd::Add<Type, ValueType> allGuards = generationInfo.manager->template getAddZero<ValueType>();
storm::dd::Bdd<Type> allGuards = generationInfo.manager->getBddZero();
storm::dd::Add<Type, ValueType> allCommands = generationInfo.manager->template getAddZero<ValueType>();
// Make all command DDs assign to the same global variables.
@ -553,7 +553,7 @@ namespace storm {
storm::dd::Add<Type, ValueType> sumOfGuards = generationInfo.manager->template getAddZero<ValueType>();
for (auto const& commandDd : commandDds) {
sumOfGuards += commandDd.guardDd;
allGuards = allGuards || commandDd.guardDd;
allGuards |= commandDd.guardDd.toBdd();
}
uint_fast64_t maxChoices = static_cast<uint_fast64_t>(sumOfGuards.getMax());
@ -634,7 +634,7 @@ namespace storm {
sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd).template toAdd<ValueType>();
}
return ActionDecisionDiagram(allGuards, allCommands, assignedGlobalVariables, nondeterminismVariableOffset + numberOfBinaryVariables);
return ActionDecisionDiagram(allGuards.template toAdd<ValueType>(), allCommands, assignedGlobalVariables, nondeterminismVariableOffset + numberOfBinaryVariables);
}
}
@ -685,7 +685,7 @@ namespace storm {
// Add a new variable that resolves the nondeterminism between the two choices.
storm::dd::Add<Type, ValueType> combinedTransitions = generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[numberOfUsedNondeterminismVariables], 1).template toAdd<ValueType>().ite(action2Extended, action1Extended);
return ActionDecisionDiagram(action1.guardDd || action2.guardDd, combinedTransitions, assignedGlobalVariables, numberOfUsedNondeterminismVariables + 1);
return ActionDecisionDiagram((action1.guardDd.toBdd() || action2.guardDd.toBdd()).template toAdd<ValueType>(), combinedTransitions, assignedGlobalVariables, numberOfUsedNondeterminismVariables + 1);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Illegal model type.");
}

17
src/storage/dd/Add.cpp
View File

@ -35,23 +35,6 @@ namespace storm {
metaVariables.insert(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end());
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.ite(thenAdd.internalAdd, elseAdd.internalAdd), metaVariables);
}
// template<DdType LibraryType, typename ValueType>
// Add<LibraryType, ValueType> Add<LibraryType, ValueType>::operator!() const {
// return Add<LibraryType, ValueType>(this->getDdManager(), !internalAdd, this->getContainedMetaVariables());
// }
template<DdType LibraryType, typename ValueType>
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::operator||(Add<LibraryType, ValueType> const& other) const {
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd || other.internalAdd, Dd<LibraryType>::joinMetaVariables(*this, other));
}
template<DdType LibraryType, typename ValueType>
Add<LibraryType, ValueType>& Add<LibraryType, ValueType>::operator|=(Add<LibraryType, ValueType> const& other) {
this->addMetaVariables(other.getContainedMetaVariables());
internalAdd |= other.internalAdd;
return *this;
}
template<DdType LibraryType, typename ValueType>
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::operator+(Add<LibraryType, ValueType> const& other) const {

26
src/storage/dd/Add.h
View File

@ -75,32 +75,6 @@ namespace storm {
*/
Add<LibraryType, ValueType> ite(Add<LibraryType, ValueType> const& thenAdd, Add<LibraryType, ValueType> const& elseAdd) const;
/*!
* Logically inverts the current ADD. That is, all inputs yielding non-zero values will be mapped to zero in
* the result and vice versa.
*
* @return The resulting ADD.
*/
// Add<LibraryType, ValueType> operator!() const;
/*!
* Performs a logical or of the current anBd the given ADD. As a prerequisite, the operand ADDs need to be
* 0/1 ADDs.
*
* @param other The second ADD used for the operation.
* @return The logical or of the operands.
*/
Add<LibraryType, ValueType> operator||(Add<LibraryType, ValueType> const& other) const;
/*!
* Performs a logical or of the current and the given ADD and assigns it to the current ADD. As a
* prerequisite, the operand ADDs need to be 0/1 ADDs.
*
* @param other The second ADD used for the operation.
* @return A reference to the current ADD after the operation
*/
Add<LibraryType, ValueType>& operator|=(Add<LibraryType, ValueType> const& other);
/*!
* Adds the two ADDs.
*

18
src/storage/dd/cudd/InternalCuddAdd.cpp
View File

@ -31,23 +31,7 @@ namespace storm {
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::ite(InternalAdd<DdType::CUDD, ValueType> const& thenDd, InternalAdd<DdType::CUDD, ValueType> const& elseDd) const {
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().Ite(thenDd.getCuddAdd(), elseDd.getCuddAdd()));
}
template<typename ValueType>
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::operator!() const {
return InternalAdd<DdType::CUDD, ValueType>(ddManager, ~this->getCuddAdd());
}
template<typename ValueType>
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::operator||(InternalAdd<DdType::CUDD, ValueType> const& other) const {
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd() | other.getCuddAdd());
}
template<typename ValueType>
InternalAdd<DdType::CUDD, ValueType>& InternalAdd<DdType::CUDD, ValueType>::operator|=(InternalAdd<DdType::CUDD, ValueType> const& other) {
this->cuddAdd = this->getCuddAdd() | other.getCuddAdd();
return *this;
}
template<typename ValueType>
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::operator+(InternalAdd<DdType::CUDD, ValueType> const& other) const {
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd() + other.getCuddAdd());

26
src/storage/dd/cudd/InternalCuddAdd.h
View File

@ -82,32 +82,6 @@ namespace storm {
*/
InternalAdd<DdType::CUDD, ValueType> ite(InternalAdd<DdType::CUDD, ValueType> const& thenAdd, InternalAdd<DdType::CUDD, ValueType> const& elseAdd) const;
/*!
* Logically inverts the current ADD. That is, all inputs yielding non-zero values will be mapped to zero in
* the result and vice versa.
*
* @return The resulting ADD.
*/
InternalAdd<DdType::CUDD, ValueType> operator!() const;
/*!
* Performs a logical or of the current and the given ADD. As a prerequisite, the operand ADDs need to be
* 0/1 ADDs.
*
* @param other The second ADD used for the operation.
* @return The logical or of the operands.
*/
InternalAdd<DdType::CUDD, ValueType> operator||(InternalAdd<DdType::CUDD, ValueType> const& other) const;
/*!
* Performs a logical or of the current and the given ADD and assigns it to the current ADD. As a
* prerequisite, the operand ADDs need to be 0/1 ADDs.
*
* @param other The second ADD used for the operation.
* @return A reference to the current ADD after the operation
*/
InternalAdd<DdType::CUDD, ValueType>& operator|=(InternalAdd<DdType::CUDD, ValueType> const& other);
/*!
* Adds the two ADDs.
*

17
src/storage/dd/sylvan/InternalSylvanAdd.cpp
View File

@ -26,22 +26,7 @@ namespace storm {
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::ite(InternalAdd<DdType::Sylvan, ValueType> const& thenDd, InternalAdd<DdType::Sylvan, ValueType> const& elseDd) const {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
}
template<typename ValueType>
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::operator!() const {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
}
template<typename ValueType>
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::operator||(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
}
template<typename ValueType>
InternalAdd<DdType::Sylvan, ValueType>& InternalAdd<DdType::Sylvan, ValueType>::operator|=(InternalAdd<DdType::Sylvan, ValueType> const& other) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
}
template<typename ValueType>
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::operator+(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Plus(other.sylvanMtbdd));

28
src/storage/dd/sylvan/InternalSylvanAdd.h
View File

@ -81,33 +81,7 @@ namespace storm {
* @return The ADD corresponding to the if-then-else of the operands.
*/
InternalAdd<DdType::Sylvan, ValueType> ite(InternalAdd<DdType::Sylvan, ValueType> const& thenAdd, InternalAdd<DdType::Sylvan, ValueType> const& elseAdd) const;
/*!
* Logically inverts the current ADD. That is, all inputs yielding non-zero values will be mapped to zero in
* the result and vice versa.
*
* @return The resulting ADD.
*/
InternalAdd<DdType::Sylvan, ValueType> operator!() const;
/*!
* Performs a logical or of the current and the given ADD. As a prerequisite, the operand ADDs need to be
* 0/1 ADDs.
*
* @param other The second ADD used for the operation.
* @return The logical or of the operands.
*/
InternalAdd<DdType::Sylvan, ValueType> operator||(InternalAdd<DdType::Sylvan, ValueType> const& other) const;
/*!
* Performs a logical or of the current and the given ADD and assigns it to the current ADD. As a
* prerequisite, the operand ADDs need to be 0/1 ADDs.
*
* @param other The second ADD used for the operation.
* @return A reference to the current ADD after the operation
*/
InternalAdd<DdType::Sylvan, ValueType>& operator|=(InternalAdd<DdType::Sylvan, ValueType> const& other);
/*!
* Adds the two ADDs.
*

Write Preview
Loading…
Cancel
Save