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

further in debugging MDP bisimulation

main
dehnert 8 years ago
parent
a1db269e8f
commit
d0840f783a
5 changed files with 80 additions and 43 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. 10
      src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp
  2. 6
      src/storm/storage/dd/bisimulation/PartitionRefiner.cpp
  3. 88
      src/storm/storage/dd/bisimulation/SignatureComputer.cpp
  4. 17
      src/storm/storage/dd/bisimulation/SignatureComputer.h
  5. 2
      src/storm/storage/dd/bisimulation/SignatureMode.h

10
src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp
View File

@ -7,8 +7,10 @@ namespace storm {
namespace bisimulation {
template<storm::dd::DdType DdType, typename ValueType>
MdpPartitionRefiner<DdType, ValueType>::MdpPartitionRefiner(storm::models::symbolic::Mdp<DdType, ValueType> const& mdp, Partition<DdType, ValueType> const& initialStatePartition) : PartitionRefiner<DdType, ValueType>(mdp, initialStatePartition), choicePartition(Partition<DdType, ValueType>::createTrivialChoicePartition(mdp, initialStatePartition.getBlockVariables())), stateSignatureComputer(mdp.getQualitativeTransitionMatrix(false), mdp.getColumnAndNondeterminismVariables()), stateSignatureRefiner(mdp.getManager(), this->statePartition.getBlockVariable(), mdp.getRowVariables()) {
MdpPartitionRefiner<DdType, ValueType>::MdpPartitionRefiner(storm::models::symbolic::Mdp<DdType, ValueType> const& mdp, Partition<DdType, ValueType> const& initialStatePartition) : PartitionRefiner<DdType, ValueType>(mdp, initialStatePartition), choicePartition(Partition<DdType, ValueType>::createTrivialChoicePartition(mdp, initialStatePartition.getBlockVariables())), stateSignatureComputer(mdp.getQualitativeTransitionMatrix(), mdp.getColumnAndNondeterminismVariables(), SignatureMode::Qualitative, true), stateSignatureRefiner(mdp.getManager(), this->statePartition.getBlockVariable(), mdp.getRowVariables()) {
// Intentionally left empty.
mdp.getTransitionMatrix().exportToDot("fulltrans.dot");
}
template<storm::dd::DdType DdType, typename ValueType>
@ -26,9 +28,11 @@ namespace storm {
this->status = Status::FixedPoint;
return false;
} else {
// If the choice partition changed, refine the state partition. Use eager mode as abstracting from the probabilities is not worth doing.
this->choicePartition = newChoicePartition;
// If the choice partition changed, refine the state partition. Use qualitative mode we must properly abstract from choice counts.
STORM_LOG_TRACE("Refining state partition.");
Partition<DdType, ValueType> newStatePartition = this->internalRefine(this->stateSignatureComputer, this->stateSignatureRefiner, this->statePartition, this->choicePartition, SignatureMode::Eager);
Partition<DdType, ValueType> newStatePartition = this->internalRefine(this->stateSignatureComputer, this->stateSignatureRefiner, this->statePartition, this->choicePartition, SignatureMode::Qualitative);
if (newStatePartition == this->statePartition) {
this->status = Status::FixedPoint;

6
src/storm/storage/dd/bisimulation/PartitionRefiner.cpp
View File

@ -45,9 +45,9 @@ namespace storm {
STORM_LOG_DEBUG("Signature " << refinements << "[" << index << "] DD has " << signature.getSignatureAdd().getNodeCount() << " nodes.");
signature.getSignatureAdd().exportToDot("sig" + std::to_string(refinements) + ".dot");
if (refinements == 1) {
exit(-1);
}
// if (refinements == 1) {
// exit(-1);
// }
auto refinementStart = std::chrono::high_resolution_clock::now();
newPartition = signatureRefiner.refine(statePartition, signature);

88
src/storm/storage/dd/bisimulation/SignatureComputer.cpp
View File

@ -16,23 +16,35 @@ namespace storm {
template<storm::dd::DdType DdType, typename ValueType>
bool SignatureIterator<DdType, ValueType>::hasNext() const {
if (signatureComputer.getSignatureMode() == SignatureMode::Eager) {
return position < 1;
} else {
return position < 2;
switch (signatureComputer.getSignatureMode()) {
case SignatureMode::Qualitative:
case SignatureMode::Eager: return position < 1;
case SignatureMode::Lazy: return position < 2;
}
}
template<storm::dd::DdType DdType, typename ValueType>
Signature<DdType, ValueType> SignatureIterator<DdType, ValueType>::next() {
auto mode = signatureComputer.getSignatureMode();
STORM_LOG_THROW((mode == SignatureMode::Eager && position < 1) || (mode == SignatureMode::Lazy && position < 2), storm::exceptions::OutOfRangeException, "Iterator is out of range.");
STORM_LOG_THROW((mode == SignatureMode::Eager && position < 1) || (mode == SignatureMode::Lazy && position < 2) || (mode == SignatureMode::Qualitative && position < 1), storm::exceptions::OutOfRangeException, "Iterator is out of range.");
Signature<DdType, ValueType> result;
if (mode == SignatureMode::Eager || position == 1) {
result = signatureComputer.getFullSignature(partition);
} else if (position == 0) {
result = signatureComputer.getQualitativeSignature(partition);
if (mode == SignatureMode::Eager) {
if (position == 0) {
result = signatureComputer.getFullSignature(partition);
}
} else if (mode == SignatureMode::Lazy) {
if (position == 0) {
result = signatureComputer.getQualitativeSignature(partition);
} else {
result = signatureComputer.getFullSignature(partition);
}
} else if (mode == SignatureMode::Qualitative) {
if (position == 0) {
result = signatureComputer.getQualitativeSignature(partition);
}
} else {
STORM_LOG_ASSERT(false, "Unknown signature mode.");
}
++position;
@ -40,29 +52,29 @@ namespace storm {
}
template<storm::dd::DdType DdType, typename ValueType>
SignatureComputer<DdType, ValueType>::SignatureComputer(storm::models::symbolic::Model<DdType, ValueType> const& model, SignatureMode const& mode) : SignatureComputer(model.getTransitionMatrix(), boost::none, model.getColumnVariables(), mode) {
SignatureComputer<DdType, ValueType>::SignatureComputer(storm::models::symbolic::Model<DdType, ValueType> const& model, SignatureMode const& mode, bool ensureQualitative) : SignatureComputer(model.getTransitionMatrix(), boost::none, model.getColumnVariables(), mode, ensureQualitative) {
// Intentionally left empty.
}
template<storm::dd::DdType DdType, typename ValueType>
SignatureComputer<DdType, ValueType>::SignatureComputer(storm::dd::Add<DdType, ValueType> const& transitionMatrix, std::set<storm::expressions::Variable> const& columnVariables, SignatureMode const& mode) : SignatureComputer(transitionMatrix, boost::none, columnVariables, mode) {
SignatureComputer<DdType, ValueType>::SignatureComputer(storm::dd::Add<DdType, ValueType> const& transitionMatrix, std::set<storm::expressions::Variable> const& columnVariables, SignatureMode const& mode, bool ensureQualitative) : SignatureComputer(transitionMatrix, boost::none, columnVariables, mode, ensureQualitative) {
// Intentionally left empty.
}
template<storm::dd::DdType DdType, typename ValueType>
SignatureComputer<DdType, ValueType>::SignatureComputer(storm::dd::Bdd<DdType> const& qualitativeTransitionMatrix, std::set<storm::expressions::Variable> const& columnVariables, SignatureMode const& mode) : SignatureComputer(qualitativeTransitionMatrix.template toAdd<ValueType>(), boost::none, columnVariables, mode) {
SignatureComputer<DdType, ValueType>::SignatureComputer(storm::dd::Bdd<DdType> const& qualitativeTransitionMatrix, std::set<storm::expressions::Variable> const& columnVariables, SignatureMode const& mode, bool ensureQualitative) : SignatureComputer(qualitativeTransitionMatrix.template toAdd<ValueType>(), boost::none, columnVariables, mode, ensureQualitative) {
// Intentionally left empty.
}
template<storm::dd::DdType DdType, typename ValueType>
SignatureComputer<DdType, ValueType>::SignatureComputer(storm::dd::Add<DdType, ValueType> const& transitionMatrix, boost::optional<storm::dd::Bdd<DdType>> const& qualitativeTransitionMatrix, std::set<storm::expressions::Variable> const& columnVariables, SignatureMode const& mode) : transitionMatrix(transitionMatrix), columnVariables(columnVariables), mode(mode) {
SignatureComputer<DdType, ValueType>::SignatureComputer(storm::dd::Add<DdType, ValueType> const& transitionMatrix, boost::optional<storm::dd::Bdd<DdType>> const& qualitativeTransitionMatrix, std::set<storm::expressions::Variable> const& columnVariables, SignatureMode const& mode, bool ensureQualitative) : transitionMatrix(transitionMatrix), columnVariables(columnVariables), mode(mode), ensureQualitative(ensureQualitative) {
if (DdType == storm::dd::DdType::Sylvan) {
this->transitionMatrix = this->transitionMatrix.notZero().ite(this->transitionMatrix, this->transitionMatrix.getDdManager().template getAddUndefined<ValueType>());
}
if (qualitativeTransitionMatrix) {
if (DdType == storm::dd::DdType::Sylvan) {
this->transitionMatrix01 = qualitativeTransitionMatrix.get().ite(this->transitionMatrix.getDdManager().template getAddOne<ValueType>(), this->transitionMatrix.getDdManager().template getAddUndefined<ValueType>());
if (DdType == storm::dd::DdType::Sylvan || ensureQualitative) {
this->transitionMatrix01 = qualitativeTransitionMatrix.get();
} else {
this->transitionMatrix01 = qualitativeTransitionMatrix.get().template toAdd<ValueType>();
}
@ -86,40 +98,54 @@ namespace storm {
template<storm::dd::DdType DdType, typename ValueType>
Signature<DdType, ValueType> SignatureComputer<DdType, ValueType>::getFullSignature(Partition<DdType, ValueType> const& partition) const {
this->transitionMatrix.exportToDot("trans.dot");
if (partition.storedAsBdd()) {
return Signature<DdType, ValueType>(this->transitionMatrix.multiplyMatrix(partition.asBdd(), columnVariables));
} else {
auto result = Signature<DdType, ValueType>(this->transitionMatrix.multiplyMatrix(partition.asAdd(), columnVariables));
std::cout << "abstracting vars" << std::endl;
for (auto const& v : columnVariables) {
std::cout << v.getName() << std::endl;
}
std::cout << "----" << std::endl;
result.getSignatureAdd().exportToDot("fullsig.dot");
return result;
return Signature<DdType, ValueType>(this->transitionMatrix.multiplyMatrix(partition.asAdd(), columnVariables));
}
}
template<storm::dd::DdType DdType, typename ValueType>
Signature<DdType, ValueType> SignatureComputer<DdType, ValueType>::getQualitativeSignature(Partition<DdType, ValueType> const& partition) const {
if (this->mode == SignatureMode::Lazy && !transitionMatrix01) {
if (DdType == storm::dd::DdType::Sylvan) {
this->transitionMatrix01 = this->transitionMatrix.notZero().ite(this->transitionMatrix.getDdManager().template getAddOne<ValueType>(), this->transitionMatrix.getDdManager().template getAddUndefined<ValueType>());
if (!transitionMatrix01) {
if (DdType == storm::dd::DdType::Sylvan || this->ensureQualitative) {
this->transitionMatrix01 = this->transitionMatrix.notZero();
} else {
this->transitionMatrix01 = this->transitionMatrix.notZero().template toAdd<ValueType>();
}
}
if (partition.storedAsBdd()) {
return Signature<DdType, ValueType>(this->transitionMatrix01.get().multiplyMatrix(partition.asBdd(), columnVariables));
return this->getQualitativeTransitionMatrixAsBdd().andExists(partition.asBdd(), columnVariables).template toAdd<ValueType>();
} else {
return Signature<DdType, ValueType>(this->transitionMatrix01.get().multiplyMatrix(partition.asAdd(), columnVariables));
if (this->qualitativeTransitionMatrixIsBdd()) {
this->getQualitativeTransitionMatrixAsBdd().template toAdd<ValueType>().exportToDot("lasttrans.dot");
partition.asAdd().exportToDot("lastpart.dot");
this->getQualitativeTransitionMatrixAsBdd().andExists(partition.asAdd().toBdd(), columnVariables).template toAdd<ValueType>().exportToDot("lastresult.dot");
return Signature<DdType, ValueType>(this->getQualitativeTransitionMatrixAsBdd().andExists(partition.asAdd().toBdd(), columnVariables).template toAdd<ValueType>());
} else {
return Signature<DdType, ValueType>(this->getQualitativeTransitionMatrixAsAdd().multiplyMatrix(partition.asAdd(), columnVariables));
}
}
}
template<storm::dd::DdType DdType, typename ValueType>
bool SignatureComputer<DdType, ValueType>::qualitativeTransitionMatrixIsBdd() const {
return transitionMatrix01.get().which() == 0;
}
template<storm::dd::DdType DdType, typename ValueType>
storm::dd::Bdd<DdType> const& SignatureComputer<DdType, ValueType>::getQualitativeTransitionMatrixAsBdd() const {
STORM_LOG_ASSERT(this->transitionMatrix01, "Missing qualitative transition matrix.");
return boost::get<storm::dd::Bdd<DdType>>(this->transitionMatrix01.get());
}
template<storm::dd::DdType DdType, typename ValueType>
storm::dd::Add<DdType, ValueType> const& SignatureComputer<DdType, ValueType>::getQualitativeTransitionMatrixAsAdd() const {
STORM_LOG_ASSERT(this->transitionMatrix01, "Missing qualitative transition matrix.");
return boost::get<storm::dd::Add<DdType, ValueType>>(this->transitionMatrix01.get());
}
template class SignatureIterator<storm::dd::DdType::CUDD, double>;
template class SignatureIterator<storm::dd::DdType::Sylvan, double>;
template class SignatureIterator<storm::dd::DdType::Sylvan, storm::RationalNumber>;

17
src/storm/storage/dd/bisimulation/SignatureComputer.h
View File

@ -42,10 +42,10 @@ namespace storm {
public:
friend class SignatureIterator<DdType, ValueType>;
SignatureComputer(storm::models::symbolic::Model<DdType, ValueType> const& model, SignatureMode const& mode = SignatureMode::Eager);
SignatureComputer(storm::dd::Add<DdType, ValueType> const& transitionMatrix, std::set<storm::expressions::Variable> const& columnVariables, SignatureMode const& mode = SignatureMode::Eager);
SignatureComputer(storm::dd::Bdd<DdType> const& qualitativeTransitionMatrix, std::set<storm::expressions::Variable> const& columnVariables, SignatureMode const& mode = SignatureMode::Eager);
SignatureComputer(storm::dd::Add<DdType, ValueType> const& transitionMatrix, boost::optional<storm::dd::Bdd<DdType>> const& qualitativeTransitionMatrix, std::set<storm::expressions::Variable> const& columnVariables, SignatureMode const& mode = SignatureMode::Eager);
SignatureComputer(storm::models::symbolic::Model<DdType, ValueType> const& model, SignatureMode const& mode = SignatureMode::Eager, bool ensureQualitative = false);
SignatureComputer(storm::dd::Add<DdType, ValueType> const& transitionMatrix, std::set<storm::expressions::Variable> const& columnVariables, SignatureMode const& mode = SignatureMode::Eager, bool ensureQualitative = false);
SignatureComputer(storm::dd::Bdd<DdType> const& qualitativeTransitionMatrix, std::set<storm::expressions::Variable> const& columnVariables, SignatureMode const& mode = SignatureMode::Eager, bool ensureQualitative = false);
SignatureComputer(storm::dd::Add<DdType, ValueType> const& transitionMatrix, boost::optional<storm::dd::Bdd<DdType>> const& qualitativeTransitionMatrix, std::set<storm::expressions::Variable> const& columnVariables, SignatureMode const& mode = SignatureMode::Eager, bool ensureQualitative = false);
void setSignatureMode(SignatureMode const& newMode);
@ -56,6 +56,10 @@ namespace storm {
Signature<DdType, ValueType> getFullSignature(Partition<DdType, ValueType> const& partition) const;
Signature<DdType, ValueType> getQualitativeSignature(Partition<DdType, ValueType> const& partition) const;
bool qualitativeTransitionMatrixIsBdd() const;
storm::dd::Bdd<DdType> const& getQualitativeTransitionMatrixAsBdd() const;
storm::dd::Add<DdType, ValueType> const& getQualitativeTransitionMatrixAsAdd() const;
SignatureMode const& getSignatureMode() const;
/// The transition matrix to use for the signature computation.
@ -67,8 +71,11 @@ namespace storm {
/// The mode to use for signature computation.
SignatureMode mode;
/// A flag indicating whether the qualitative signature needs to make sure that the result is in fact qualitative.
bool ensureQualitative;
/// Only used when using lazy signatures is enabled.
mutable boost::optional<storm::dd::Add<DdType, ValueType>> transitionMatrix01;
mutable boost::optional<boost::variant<storm::dd::Bdd<DdType>, storm::dd::Add<DdType, ValueType>>> transitionMatrix01;
};
}

2
src/storm/storage/dd/bisimulation/SignatureMode.h
View File

@ -4,7 +4,7 @@ namespace storm {
namespace dd {
namespace bisimulation {
enum class SignatureMode { Eager, Lazy };
enum class SignatureMode { Eager, Lazy, Qualitative };
}
}

Write Preview
Loading…
Cancel
Save