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

more time output in dd-based bisimulation

tempestpy_adaptions
dehnert 7 years ago
parent
34b6593ed8
commit
66e08f9cd7
4 changed files with 22 additions and 5 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. 2
      src/storm/storage/dd/BisimulationDecomposition.cpp
  2. 3
      src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp
  3. 19
      src/storm/storage/dd/bisimulation/PartitionRefiner.cpp
  4. 3
      src/storm/storage/dd/bisimulation/PartitionRefiner.h

2
src/storm/storage/dd/BisimulationDecomposition.cpp
View File

@ -93,7 +93,7 @@ namespace storm {
}
auto end = std::chrono::high_resolution_clock::now();
STORM_LOG_INFO("Partition refinement completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms (" << iterations << " iterations).");
STORM_LOG_INFO("Partition refinement completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms (" << iterations << " iterations, signature: " << std::chrono::duration_cast<std::chrono::milliseconds>(refiner->getTotalSignatureTime()).count() << "ms, refinement: " << std::chrono::duration_cast<std::chrono::milliseconds>(refiner->getTotalRefinementTime()).count() << "ms).");
}
template <storm::dd::DdType DdType, typename ValueType>

3
src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp
View File

@ -46,7 +46,8 @@ namespace storm {
auto signatureStart = std::chrono::high_resolution_clock::now();
Signature<DdType, ValueType> stateSignature(choicePartitionAsBdd.existsAbstract(model.getNondeterminismVariables()).template toAdd<ValueType>());
auto signatureEnd = std::chrono::high_resolution_clock::now();
this->totalSignatureTime += (signatureEnd - signatureStart);
// If the choice partition changed, refine the state partition.
STORM_LOG_TRACE("Refining state partition.");
auto refinementStart = std::chrono::high_resolution_clock::now();

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

@ -12,7 +12,7 @@ namespace storm {
namespace bisimulation {
template <storm::dd::DdType DdType, typename ValueType>
PartitionRefiner<DdType, ValueType>::PartitionRefiner(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& initialStatePartition) : status(Status::Initialized), refinements(0), statePartition(initialStatePartition), signatureComputer(model), signatureRefiner(model.getManager(), statePartition.getBlockVariable(), model.getRowAndNondeterminismVariables(), model.getColumnVariables(), !model.isNondeterministicModel(), model.getNondeterminismVariables()) {
PartitionRefiner<DdType, ValueType>::PartitionRefiner(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& initialStatePartition) : status(Status::Initialized), refinements(0), statePartition(initialStatePartition), signatureComputer(model), signatureRefiner(model.getManager(), statePartition.getBlockVariable(), model.getRowAndNondeterminismVariables(), model.getColumnVariables(), !model.isNondeterministicModel(), model.getNondeterminismVariables()), totalSignatureTime(0), totalRefinementTime(0) {
// Intentionally left empty.
}
@ -50,7 +50,7 @@ namespace storm {
auto signatureEnd = std::chrono::high_resolution_clock::now();
totalSignatureTime += (signatureEnd - signatureStart);
STORM_LOG_TRACE("Signature " << refinements << "[" << index << "] DD has " << signature.getSignatureAdd().getNodeCount() << " nodes.");
auto refinementStart = std::chrono::high_resolution_clock::now();
newPartition = signatureRefiner.refine(oldPartition, signature);
auto refinementEnd = std::chrono::high_resolution_clock::now();
@ -78,8 +78,11 @@ namespace storm {
Partition<DdType, ValueType> PartitionRefiner<DdType, ValueType>::internalRefine(Signature<DdType, ValueType> const& signature, SignatureRefiner<DdType, ValueType>& signatureRefiner, Partition<DdType, ValueType> const& oldPartition) {
STORM_LOG_TRACE("Signature " << refinements << " DD has " << signature.getSignatureAdd().getNodeCount() << " nodes.");
auto refinementStart = std::chrono::high_resolution_clock::now();
auto newPartition = signatureRefiner.refine(oldPartition, signature);
auto refinementEnd = std::chrono::high_resolution_clock::now();
totalRefinementTime += (refinementEnd - refinementStart);
++refinements;
return newPartition;
}
@ -132,6 +135,16 @@ namespace storm {
return status;
}
template <storm::dd::DdType DdType, typename ValueType>
std::chrono::high_resolution_clock::duration PartitionRefiner<DdType, ValueType>::getTotalSignatureTime() const {
return totalSignatureTime;
}
template <storm::dd::DdType DdType, typename ValueType>
std::chrono::high_resolution_clock::duration PartitionRefiner<DdType, ValueType>::getTotalRefinementTime() const {
return totalRefinementTime;
}
template class PartitionRefiner<storm::dd::DdType::CUDD, double>;
template class PartitionRefiner<storm::dd::DdType::Sylvan, double>;

3
src/storm/storage/dd/bisimulation/PartitionRefiner.h
View File

@ -53,6 +53,9 @@ namespace storm {
*/
Status getStatus() const;
std::chrono::high_resolution_clock::duration getTotalSignatureTime() const;
std::chrono::high_resolution_clock::duration getTotalRefinementTime() const;
protected:
Partition<DdType, ValueType> internalRefine(SignatureComputer<DdType, ValueType>& stateSignatureComputer, SignatureRefiner<DdType, ValueType>& signatureRefiner, Partition<DdType, ValueType> const& oldPartition, Partition<DdType, ValueType> const& targetPartition, SignatureMode const& mode = SignatureMode::Eager);
Partition<DdType, ValueType> internalRefine(Signature<DdType, ValueType> const& signature, SignatureRefiner<DdType, ValueType>& signatureRefiner, Partition<DdType, ValueType> const& oldPartition);

Write Preview
Loading…
Cancel
Save