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

work on variations which data is reused in dd-based bisimulation

main
dehnert 8 years ago
parent
41828ca27d
commit
a19c2fe59b
13 changed files with 417 additions and 126 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. 37
      src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp
  2. 1
      src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h
  3. 2
      src/storm/settings/modules/AbstractionSettings.cpp
  4. 21
      src/storm/settings/modules/BisimulationSettings.cpp
  5. 8
      src/storm/settings/modules/BisimulationSettings.h
  6. 4
      src/storm/storage/dd/BisimulationDecomposition.cpp
  7. 2
      src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp
  8. 24
      src/storm/storage/dd/bisimulation/Partition.cpp
  9. 19
      src/storm/storage/dd/bisimulation/Partition.h
  10. 2
      src/storm/storage/dd/bisimulation/PartitionRefiner.cpp
  11. 8
      src/storm/storage/dd/bisimulation/PreservationInformation.cpp
  12. 8
      src/storm/storage/dd/bisimulation/PreservationInformation.h
  13. 407
      src/storm/storage/dd/bisimulation/SignatureRefiner.cpp

37
src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp
View File

@ -61,19 +61,17 @@ namespace storm {
STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidPropertyException, "The game-based abstraction refinement model checker can only compute the result for the initial states.");
// Create the appropriate preservation information.
storm::dd::bisimulation::PreservationInformation<DdType, ValueType> preservationInformation(model, storm::storage::BisimulationType::Strong);
if (checkTask.isRewardModelSet()) {
if (checkTask.getRewardModel() != "" || model.hasRewardModel(checkTask.getRewardModel())) {
preservationInformation.addRewardModel(checkTask.getRewardModel());
} else if (model.hasUniqueRewardModel()) {
storm::dd::bisimulation::PreservationInformation<DdType, ValueType> preservationInformation(model, {checkTask.getFormula().asSharedPointer()});
if (rewards) {
if (!checkTask.isRewardModelSet() || model.hasUniqueRewardModel()) {
preservationInformation.addRewardModel(model.getUniqueRewardModelName());
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Property refers to illegal reward model '" << checkTask.getRewardModel() << "'.");
} else if (checkTask.isRewardModelSet()) {
preservationInformation.addRewardModel(checkTask.getRewardModel());
}
}
// Create a bisimulation object that is used to obtain (partial) quotients.
storm::dd::BisimulationDecomposition<DdType, ValueType> bisimulation(this->model, {checkTask.getFormula().asSharedPointer()}, storm::storage::BisimulationType::Strong);
storm::dd::BisimulationDecomposition<DdType, ValueType> bisimulation(this->model, storm::storage::BisimulationType::Strong, preservationInformation);
auto start = std::chrono::high_resolution_clock::now();
@ -124,20 +122,17 @@ namespace storm {
if (lowerBounds.getStates().getNonZeroCount() == 1 && upperBounds.getStates().getNonZeroCount() == 1) {
STORM_LOG_TRACE("Obtained bounds [" << lowerBounds.getValueVector().getMax() << ", " << upperBounds.getValueVector().getMax() << "] on actual result.");
} else {
STORM_LOG_TRACE("Largest difference over initial states is " << getLargestDifference(bounds) << ".");
storm::dd::Add<DdType, ValueType> diffs = upperBounds.getValueVector() - lowerBounds.getValueVector();
storm::dd::Bdd<DdType> maxDiffRepresentative = diffs.maxAbstractRepresentative(diffs.getContainedMetaVariables());
std::pair<ValueType, ValueType> bounds;
bounds.first = (lowerBounds.getValueVector() * maxDiffRepresentative.template toAdd<ValueType>()).getMax();
bounds.second = (upperBounds.getValueVector() * maxDiffRepresentative.template toAdd<ValueType>()).getMax();
STORM_LOG_TRACE("Largest interval over initial is [" << bounds.first << ", " << bounds.second << "], difference " << (bounds.second - bounds.first) << ".");
}
}
template<typename ModelType>
typename PartialBisimulationMdpModelChecker<ModelType>::ValueType PartialBisimulationMdpModelChecker<ModelType>::getLargestDifference(std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> const& bounds) {
STORM_LOG_THROW(bounds.first->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidTypeException, "Expected symbolic quantitative check result.");
storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType> const& lowerBounds = bounds.first->asSymbolicQuantitativeCheckResult<DdType, ValueType>();
STORM_LOG_THROW(bounds.second->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidTypeException, "Expected symbolic quantitative check result.");
storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType> const& upperBounds = bounds.second->asSymbolicQuantitativeCheckResult<DdType, ValueType>();
return (upperBounds.getValueVector() - lowerBounds.getValueVector()).getMax();
}
template<typename ModelType>
bool PartialBisimulationMdpModelChecker<ModelType>::checkBoundsSufficientlyClose(std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> const& bounds) {
STORM_LOG_THROW(bounds.first->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidTypeException, "Expected symbolic quantitative check result.");
@ -174,15 +169,17 @@ namespace storm {
} else {
result.first = checker.computeProbabilities(newCheckTask);
}
STORM_LOG_ASSERT(result.first, "Expected result.");
result.first->asSymbolicQuantitativeCheckResult<DdType, ValueType>().getValueVector().exportToDot("lower_values" + std::to_string(i) + ".dot");
result.first->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotient.getReachableStates(), quotient.getInitialStates()));
newCheckTask.setOptimizationDirection(storm::OptimizationDirection::Maximize);
if (rewards) {
result.first = checker.computeRewards(storm::logic::RewardMeasureType::Expectation, newCheckTask);
result.second = checker.computeRewards(storm::logic::RewardMeasureType::Expectation, newCheckTask);
} else {
result.second = checker.computeProbabilities(newCheckTask);
}
STORM_LOG_ASSERT(result.second, "Expected result.");
result.first->asSymbolicQuantitativeCheckResult<DdType, ValueType>().getValueVector().exportToDot("upper_values" + std::to_string(i++) + ".dot");
result.second->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotient.getReachableStates(), quotient.getInitialStates()));

1
src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h
View File

@ -52,7 +52,6 @@ namespace storm {
bool checkBoundsSufficientlyClose(std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> const& bounds);
std::unique_ptr<CheckResult> getAverageOfBounds(std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> const& bounds);
void printBoundsInformation(std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> const& bounds);
ValueType getLargestDifference(std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> const& bounds);
// Methods to compute bounds on the partial quotient.
std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> computeBoundsPartialQuotient(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask);

2
src/storm/settings/modules/AbstractionSettings.cpp
View File

@ -121,7 +121,7 @@ namespace storm {
}
AbstractionSettings::ReuseMode AbstractionSettings::getReuseMode() const {
std::string reuseModeAsString = this->getOption(splitModeOptionName).getArgumentByName("mode").getValueAsString();
std::string reuseModeAsString = this->getOption(reuseResultsOptionName).getArgumentByName("mode").getValueAsString();
if (reuseModeAsString == "all") {
return ReuseMode::All;
} else if (reuseModeAsString == "none") {

21
src/storm/settings/modules/BisimulationSettings.cpp
View File

@ -17,6 +17,7 @@ namespace storm {
const std::string BisimulationSettings::representativeOptionName = "repr";
const std::string BisimulationSettings::quotientFormatOptionName = "quot";
const std::string BisimulationSettings::signatureModeOptionName = "sigmode";
const std::string BisimulationSettings::reuseOptionName = "reuse";
BisimulationSettings::BisimulationSettings() : ModuleSettings(moduleName) {
std::vector<std::string> types = { "strong", "weak" };
@ -29,6 +30,12 @@ namespace storm {
std::vector<std::string> signatureModes = { "eager", "lazy" };
this->addOption(storm::settings::OptionBuilder(moduleName, signatureModeOptionName, false, "Sets the signature computation mode.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(signatureModes)).setDefaultValueString("eager").build()).build());
std::vector<std::string> reuseModes = {"all", "none", "blocks", "sig"};
this->addOption(storm::settings::OptionBuilder(moduleName, reuseOptionName, true, "Sets whether to reuse all results.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(reuseModes))
.setDefaultValueString("blocks").build())
.build());
}
bool BisimulationSettings::isStrongBisimulationSet() const {
@ -67,6 +74,20 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unknown signature mode '" << modeAsString << ".");
}
BisimulationSettings::ReuseMode BisimulationSettings::getReuseMode() const {
std::string reuseModeAsString = this->getOption(reuseOptionName).getArgumentByName("mode").getValueAsString();
if (reuseModeAsString == "all") {
return ReuseMode::All;
} else if (reuseModeAsString == "none") {
return ReuseMode::None;
} else if (reuseModeAsString == "blocks") {
return ReuseMode::BlockNumbers;
} else if (reuseModeAsString == "sig") {
return ReuseMode::SignatureResults;
}
return ReuseMode::All;
}
bool BisimulationSettings::check() const {
bool optionsSet = this->getOption(typeOptionName).getHasOptionBeenSet();
STORM_LOG_WARN_COND(storm::settings::getModule<storm::settings::modules::GeneralSettings>().isBisimulationSet() || !optionsSet, "Bisimulation minimization is not selected, so setting options for bisimulation has no effect.");

8
src/storm/settings/modules/BisimulationSettings.h
View File

@ -19,6 +19,8 @@ namespace storm {
enum class QuotientFormat { Sparse, Dd };
enum class ReuseMode { All, None, BlockNumbers, SignatureResults };
/*!
* Creates a new set of bisimulation settings.
*/
@ -55,6 +57,11 @@ namespace storm {
*/
storm::dd::bisimulation::SignatureMode getSignatureMode() const;
/*!
* Retrieves the selected reuse mode.
*/
ReuseMode getReuseMode() const;
virtual bool check() const override;
// The name of the module.
@ -66,6 +73,7 @@ namespace storm {
static const std::string representativeOptionName;
static const std::string quotientFormatOptionName;
static const std::string signatureModeOptionName;
static const std::string reuseOptionName;
};
} // namespace modules
} // namespace settings

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

@ -32,7 +32,7 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType>
BisimulationDecomposition<DdType, ValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model, bisimulationType), refiner(createRefiner(model, Partition<DdType, ValueType>::create(model, bisimulationType, preservationInformation))) {
BisimulationDecomposition<DdType, ValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model), refiner(createRefiner(model, Partition<DdType, ValueType>::create(model, bisimulationType, preservationInformation))) {
this->initialize();
}
@ -42,7 +42,7 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType>
BisimulationDecomposition<DdType, ValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model, formulas, bisimulationType), refiner(createRefiner(model, Partition<DdType, ValueType>::create(model, bisimulationType, preservationInformation))) {
BisimulationDecomposition<DdType, ValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model, formulas), refiner(createRefiner(model, Partition<DdType, ValueType>::create(model, bisimulationType, preservationInformation))) {
this->initialize();
}

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

@ -23,7 +23,7 @@ namespace storm {
STORM_LOG_TRACE("Refining choice partition.");
Partition<DdType, ValueType> newChoicePartition = this->internalRefine(this->signatureComputer, this->signatureRefiner, this->choicePartition, this->statePartition, mode);
if (newChoicePartition == choicePartition) {
if (newChoicePartition.getNumberOfBlocks() == choicePartition.getNumberOfBlocks()) {
this->status = Status::FixedPoint;
return false;
} else {

24
src/storm/storage/dd/bisimulation/Partition.cpp
View File

@ -28,28 +28,28 @@ namespace storm {
}
template<storm::dd::DdType DdType, typename ValueType>
Partition<DdType, ValueType>::Partition(storm::dd::Add<DdType, ValueType> const& partitionAdd, std::pair<storm::expressions::Variable, storm::expressions::Variable> const& blockVariables, uint64_t nextFreeBlockIndex) : partition(partitionAdd), blockVariables(blockVariables), nextFreeBlockIndex(nextFreeBlockIndex) {
Partition<DdType, ValueType>::Partition(storm::dd::Add<DdType, ValueType> const& partitionAdd, std::pair<storm::expressions::Variable, storm::expressions::Variable> const& blockVariables, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex) : partition(partitionAdd), blockVariables(blockVariables), numberOfBlocks(numberOfBlocks), nextFreeBlockIndex(nextFreeBlockIndex) {
// Intentionally left empty.
}
template<storm::dd::DdType DdType, typename ValueType>
Partition<DdType, ValueType>::Partition(storm::dd::Bdd<DdType> const& partitionBdd, std::pair<storm::expressions::Variable, storm::expressions::Variable> const& blockVariables, uint64_t nextFreeBlockIndex) : partition(partitionBdd), blockVariables(blockVariables), nextFreeBlockIndex(nextFreeBlockIndex) {
Partition<DdType, ValueType>::Partition(storm::dd::Bdd<DdType> const& partitionBdd, std::pair<storm::expressions::Variable, storm::expressions::Variable> const& blockVariables, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex) : partition(partitionBdd), blockVariables(blockVariables), numberOfBlocks(numberOfBlocks), nextFreeBlockIndex(nextFreeBlockIndex) {
// Intentionally left empty.
}
template<storm::dd::DdType DdType, typename ValueType>
bool Partition<DdType, ValueType>::operator==(Partition<DdType, ValueType> const& other) {
return this->partition == other.partition && this->blockVariables == other.blockVariables && this->nextFreeBlockIndex == other.nextFreeBlockIndex;
return this->partition == other.partition && this->blockVariables == other.blockVariables && this->numberOfBlocks == other.numberOfBlocks && this->nextFreeBlockIndex == other.nextFreeBlockIndex;
}
template<storm::dd::DdType DdType, typename ValueType>
Partition<DdType, ValueType> Partition<DdType, ValueType>::replacePartition(storm::dd::Add<DdType, ValueType> const& newPartitionAdd, uint64_t nextFreeBlockIndex) const {
return Partition<DdType, ValueType>(newPartitionAdd, blockVariables, nextFreeBlockIndex);
Partition<DdType, ValueType> Partition<DdType, ValueType>::replacePartition(storm::dd::Add<DdType, ValueType> const& newPartitionAdd, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex) const {
return Partition<DdType, ValueType>(newPartitionAdd, blockVariables, numberOfBlocks, nextFreeBlockIndex);
}
template<storm::dd::DdType DdType, typename ValueType>
Partition<DdType, ValueType> Partition<DdType, ValueType>::replacePartition(storm::dd::Bdd<DdType> const& newPartitionBdd, uint64_t nextFreeBlockIndex) const {
return Partition<DdType, ValueType>(newPartitionBdd, blockVariables, nextFreeBlockIndex);
Partition<DdType, ValueType> Partition<DdType, ValueType>::replacePartition(storm::dd::Bdd<DdType> const& newPartitionBdd, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex) const {
return Partition<DdType, ValueType>(newPartitionBdd, blockVariables, numberOfBlocks, nextFreeBlockIndex);
}
template<storm::dd::DdType DdType, typename ValueType>
@ -92,9 +92,9 @@ namespace storm {
// Store the partition as an ADD only in the case of CUDD.
if (DdType == storm::dd::DdType::CUDD) {
return Partition<DdType, ValueType>(partitionBddAndBlockCount.first.template toAdd<ValueType>(), blockVariables, partitionBddAndBlockCount.second);
return Partition<DdType, ValueType>(partitionBddAndBlockCount.first.template toAdd<ValueType>(), blockVariables, partitionBddAndBlockCount.second, partitionBddAndBlockCount.second);
} else {
return Partition<DdType, ValueType>(partitionBddAndBlockCount.first, blockVariables, partitionBddAndBlockCount.second);
return Partition<DdType, ValueType>(partitionBddAndBlockCount.first, blockVariables, partitionBddAndBlockCount.second, partitionBddAndBlockCount.second);
}
}
@ -104,9 +104,9 @@ namespace storm {
// Store the partition as an ADD only in the case of CUDD.
if (DdType == storm::dd::DdType::CUDD) {
return Partition<DdType, ValueType>(choicePartitionBdd.template toAdd<ValueType>(), blockVariables, 1);
return Partition<DdType, ValueType>(choicePartitionBdd.template toAdd<ValueType>(), blockVariables, 1, 1);
} else {
return Partition<DdType, ValueType>(choicePartitionBdd, blockVariables, 1);
return Partition<DdType, ValueType>(choicePartitionBdd, blockVariables, 1, 1);
}
}
@ -126,7 +126,7 @@ namespace storm {
template<storm::dd::DdType DdType, typename ValueType>
uint64_t Partition<DdType, ValueType>::getNumberOfBlocks() const {
return nextFreeBlockIndex;
return numberOfBlocks;
}
template<storm::dd::DdType DdType, typename ValueType>

19
src/storm/storage/dd/bisimulation/Partition.h
View File

@ -31,8 +31,8 @@ namespace storm {
bool operator==(Partition<DdType, ValueType> const& other);
Partition<DdType, ValueType> replacePartition(storm::dd::Add<DdType, ValueType> const& newPartitionAdd, uint64_t nextFreeBlockIndex) const;
Partition<DdType, ValueType> replacePartition(storm::dd::Bdd<DdType> const& newPartitionBdd, uint64_t nextFreeBlockIndex) const;
Partition<DdType, ValueType> replacePartition(storm::dd::Add<DdType, ValueType> const& newPartitionAdd, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex) const;
Partition<DdType, ValueType> replacePartition(storm::dd::Bdd<DdType> const& newPartitionBdd, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex) const;
static Partition create(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::storage::BisimulationType const& bisimulationType, PreservationInformation<DdType, ValueType> const& preservationInformation);
static Partition createTrivialChoicePartition(storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, std::pair<storm::expressions::Variable, storm::expressions::Variable> const& blockVariables);
@ -63,10 +63,10 @@ namespace storm {
* one iff the state is in the block.
* @param blockVariables The variables to use for the block encoding. Its range must be [0, x] where x is
* greater or equal than the number of states in the partition.
* @param nextFreeBlockIndex The next free block index. The existing blocks must be encoded with indices
* between 0 and this number.
* @param numberOfBlocks The number of blocks in this partition.
* @param nextFreeBlockIndex The next free block index.
*/
Partition(storm::dd::Add<DdType, ValueType> const& partitionAdd, std::pair<storm::expressions::Variable, storm::expressions::Variable> const& blockVariables, uint64_t nextFreeBlockIndex);
Partition(storm::dd::Add<DdType, ValueType> const& partitionAdd, std::pair<storm::expressions::Variable, storm::expressions::Variable> const& blockVariables, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex);
/*!
* Creates a new partition from the given data.
@ -75,10 +75,10 @@ namespace storm {
* true iff the state is in the block.
* @param blockVariables The variables to use for the block encoding. Their range must be [0, x] where x is
* greater or equal than the number of states in the partition.
* @param nextFreeBlockIndex The next free block index. The existing blocks must be encoded with indices
* between 0 and this number.
* @param numberOfBlocks The number of blocks in this partition.
* @param nextFreeBlockIndex The next free block index.
*/
Partition(storm::dd::Bdd<DdType> const& partitionBdd, std::pair<storm::expressions::Variable, storm::expressions::Variable> const& blockVariables, uint64_t nextFreeBlockIndex);
Partition(storm::dd::Bdd<DdType> const& partitionBdd, std::pair<storm::expressions::Variable, storm::expressions::Variable> const& blockVariables, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex);
/*!
* Creates a partition from the given model that respects the given expressions.
@ -95,6 +95,9 @@ namespace storm {
/// The meta variables used to encode the block of each state in this partition.
std::pair<storm::expressions::Variable, storm::expressions::Variable> blockVariables;
/// The number of blocks in this partition.
uint64_t numberOfBlocks;
/// The next free block index.
uint64_t nextFreeBlockIndex;
};

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

@ -17,7 +17,7 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType>
bool PartitionRefiner<DdType, ValueType>::refine(SignatureMode const& mode) {
Partition<DdType, ValueType> newStatePartition = this->internalRefine(signatureComputer, signatureRefiner, statePartition, statePartition, mode);
if (statePartition == newStatePartition) {
if (statePartition.getNumberOfBlocks() == newStatePartition.getNumberOfBlocks()) {
this->status = Status::FixedPoint;
return false;
} else {

8
src/storm/storage/dd/bisimulation/PreservationInformation.cpp
View File

@ -12,12 +12,12 @@ namespace storm {
namespace bisimulation {
template <storm::dd::DdType DdType, typename ValueType>
PreservationInformation<DdType, ValueType>::PreservationInformation(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::storage::BisimulationType const& bisimulationType) : PreservationInformation(model, model.getLabels(), bisimulationType) {
PreservationInformation<DdType, ValueType>::PreservationInformation(storm::models::symbolic::Model<DdType, ValueType> const& model) : PreservationInformation(model, model.getLabels()) {
// Intentionally left empty.
}
template <storm::dd::DdType DdType, typename ValueType>
PreservationInformation<DdType, ValueType>::PreservationInformation(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::string> const& labels, storm::storage::BisimulationType const&) {
PreservationInformation<DdType, ValueType>::PreservationInformation(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::string> const& labels) {
for (auto const& label : labels) {
this->addLabel(label);
this->addExpression(model.getExpression(label));
@ -25,14 +25,14 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType>
PreservationInformation<DdType, ValueType>::PreservationInformation(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<storm::expressions::Expression> const& expressions, storm::storage::BisimulationType const&) {
PreservationInformation<DdType, ValueType>::PreservationInformation(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<storm::expressions::Expression> const& expressions) {
for (auto const& e : expressions) {
this->addExpression(e);
}
}
template <storm::dd::DdType DdType, typename ValueType>
PreservationInformation<DdType, ValueType>::PreservationInformation(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType const&) {
PreservationInformation<DdType, ValueType>::PreservationInformation(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
if (formulas.empty()) {
// Default to respect all labels if no formulas are given.
for (auto const& label : model.getLabels()) {

8
src/storm/storage/dd/bisimulation/PreservationInformation.h
View File

@ -21,10 +21,10 @@ namespace storm {
public:
PreservationInformation() = default;
PreservationInformation(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::storage::BisimulationType const& bisimulationType);
PreservationInformation(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::string> const& labels, storm::storage::BisimulationType const& bisimulationType);
PreservationInformation(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<storm::expressions::Expression> const& expressions, storm::storage::BisimulationType const& bisimulationType);
PreservationInformation(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType const& bisimulationType);
PreservationInformation(storm::models::symbolic::Model<DdType, ValueType> const& model);
PreservationInformation(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::string> const& labels);
PreservationInformation(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<storm::expressions::Expression> const& expressions);
PreservationInformation(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas);
void addLabel(std::string const& label);
void addExpression(storm::expressions::Expression const& expression);

407
src/storm/storage/dd/bisimulation/SignatureRefiner.cpp
View File

@ -36,6 +36,24 @@ namespace storm {
template<storm::dd::DdType DdType, typename ValueType>
class InternalSignatureRefiner;
struct InternalSignatureRefinerOptions {
InternalSignatureRefinerOptions() : InternalSignatureRefinerOptions(true) {
// Intentionally left empty.
}
InternalSignatureRefinerOptions(bool shiftStateVariables) : shiftStateVariables(shiftStateVariables) {
auto const& bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
storm::settings::modules::BisimulationSettings::ReuseMode reuseMode = bisimulationSettings.getReuseMode();
this->reuseBlockNumbers = reuseMode == storm::settings::modules::BisimulationSettings::ReuseMode::All || reuseMode == storm::settings::modules::BisimulationSettings::ReuseMode::BlockNumbers;
this->reuseSignatureResult = reuseMode == storm::settings::modules::BisimulationSettings::ReuseMode::All || reuseMode == storm::settings::modules::BisimulationSettings::ReuseMode::SignatureResults;
}
bool shiftStateVariables;
bool reuseBlockNumbers;
bool reuseSignatureResult;
};
class ReuseWrapper {
public:
ReuseWrapper() : ReuseWrapper(false) {
@ -61,7 +79,7 @@ namespace storm {
template<typename ValueType>
class InternalSignatureRefiner<storm::dd::DdType::CUDD, ValueType> {
public:
InternalSignatureRefiner(storm::dd::DdManager<storm::dd::DdType::CUDD> const& manager, storm::expressions::Variable const& blockVariable, storm::dd::Bdd<storm::dd::DdType::CUDD> const& nondeterminismVariables, storm::dd::Bdd<storm::dd::DdType::CUDD> const& nonBlockVariables, bool shiftStateVariables) : manager(manager), internalDdManager(manager.getInternalDdManager()), ddman(internalDdManager.getCuddManager().getManager()), blockVariable(blockVariable), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), shiftStateVariables(shiftStateVariables), nextFreeBlockIndex(0), numberOfRefinements(0), lastNumberOfVisitedNodes(10000), signatureCache(lastNumberOfVisitedNodes), reuseBlocksCache(lastNumberOfVisitedNodes) {
InternalSignatureRefiner(storm::dd::DdManager<storm::dd::DdType::CUDD> const& manager, storm::expressions::Variable const& blockVariable, storm::dd::Bdd<storm::dd::DdType::CUDD> const& nondeterminismVariables, storm::dd::Bdd<storm::dd::DdType::CUDD> const& nonBlockVariables, InternalSignatureRefinerOptions const& options = InternalSignatureRefinerOptions()) : manager(manager), internalDdManager(manager.getInternalDdManager()), ddman(internalDdManager.getCuddManager().getManager()), blockVariable(blockVariable), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), options(options), nextFreeBlockIndex(0), numberOfRefinements(0), lastNumberOfVisitedNodes(10000), signatureCache(lastNumberOfVisitedNodes), reuseBlocksCache(lastNumberOfVisitedNodes) {
// Initialize precomputed data.
auto const& ddMetaVariable = manager.getMetaVariable(blockVariable);
@ -72,30 +90,67 @@ namespace storm {
}
Partition<storm::dd::DdType::CUDD, ValueType> refine(Partition<storm::dd::DdType::CUDD, ValueType> const& oldPartition, Signature<storm::dd::DdType::CUDD, ValueType> const& signature) {
storm::dd::Add<storm::dd::DdType::CUDD, ValueType> newPartitionAdd = refine(oldPartition, signature.getSignatureAdd());
storm::dd::Add<storm::dd::DdType::CUDD, ValueType> newPartitionAdd;
if (options.reuseBlockNumbers && !options.reuseSignatureResult) {
newPartitionAdd = refineReuseBlockNumber(oldPartition, signature.getSignatureAdd());
} else {
newPartitionAdd = refineReuseSignatureResults(oldPartition, signature.getSignatureAdd());
}
++numberOfRefinements;
return oldPartition.replacePartition(newPartitionAdd, nextFreeBlockIndex);
uint64_t numberOfBlocks = nextFreeBlockIndex;
if (options.reuseSignatureResult) {
std::set<storm::expressions::Variable> blockVariableSet = {blockVariable};
std::set<storm::expressions::Variable> nonBlockExpressionVariables;
std::set_difference(oldPartition.asAdd().getContainedMetaVariables().begin(), oldPartition.asAdd().getContainedMetaVariables().end(), blockVariableSet.begin(), blockVariableSet.end(), std::inserter(nonBlockExpressionVariables, nonBlockExpressionVariables.begin()));
numberOfBlocks = newPartitionAdd.notZero().existsAbstract(nonBlockExpressionVariables).getNonZeroCount();
}
return oldPartition.replacePartition(newPartitionAdd, numberOfBlocks, nextFreeBlockIndex);
}
private:
storm::dd::Add<storm::dd::DdType::CUDD, ValueType> refine(Partition<storm::dd::DdType::CUDD, ValueType> const& oldPartition, storm::dd::Add<storm::dd::DdType::CUDD, ValueType> const& signatureAdd) {
STORM_LOG_ASSERT(oldPartition.storedAsAdd(), "Expecting partition to be stored as ADD for CUDD.");
// Clear the caches.
void clearCaches() {
signatureCache.clear();
signatureCache2.clear();
reuseBlocksCache.clear();
}
storm::dd::Add<storm::dd::DdType::CUDD, ValueType> refineReuseBlockNumber(Partition<storm::dd::DdType::CUDD, ValueType> const& oldPartition, storm::dd::Add<storm::dd::DdType::CUDD, ValueType> const& signatureAdd) {
STORM_LOG_ASSERT(oldPartition.storedAsAdd(), "Expecting partition to be stored as ADD for CUDD.");
nextFreeBlockIndex = oldPartition.getNextFreeBlockIndex();
// Perform the actual recursive refinement step.
DdNodePtr result = refine(oldPartition.asAdd().getInternalAdd().getCuddDdNode(), signatureAdd.getInternalAdd().getCuddDdNode(), nondeterminismVariables.getInternalBdd().getCuddDdNode(), nonBlockVariables.getInternalBdd().getCuddDdNode());
DdNodePtr result = refineReuseBlockNumber(oldPartition.asAdd().getInternalAdd().getCuddDdNode(), signatureAdd.getInternalAdd().getCuddDdNode(), nondeterminismVariables.getInternalBdd().getCuddDdNode(), nonBlockVariables.getInternalBdd().getCuddDdNode());
// Construct resulting ADD from the obtained node and the meta information.
storm::dd::InternalAdd<storm::dd::DdType::CUDD, ValueType> internalNewPartitionAdd(&internalDdManager, cudd::ADD(internalDdManager.getCuddManager(), result));
storm::dd::Add<storm::dd::DdType::CUDD, ValueType> newPartitionAdd(oldPartition.asAdd().getDdManager(), internalNewPartitionAdd, oldPartition.asAdd().getContainedMetaVariables());
clearCaches();
return newPartitionAdd;
}
storm::dd::Add<storm::dd::DdType::CUDD, ValueType> refineReuseSignatureResults(Partition<storm::dd::DdType::CUDD, ValueType> const& oldPartition, storm::dd::Add<storm::dd::DdType::CUDD, ValueType> const& signatureAdd) {
STORM_LOG_ASSERT(oldPartition.storedAsAdd(), "Expecting partition to be stored as ADD for CUDD.");
nextFreeBlockIndex = options.reuseSignatureResult ? oldPartition.getNextFreeBlockIndex() : 0;
// Perform the actual recursive refinement step.
DdNodePtr result = refineReuseSignatureResults(signatureAdd.getInternalAdd().getCuddDdNode(), nondeterminismVariables.getInternalBdd().getCuddDdNode(), nonBlockVariables.getInternalBdd().getCuddDdNode());
// Construct resulting ADD from the obtained node and the meta information.
storm::dd::InternalAdd<storm::dd::DdType::CUDD, ValueType> internalNewPartitionAdd(&internalDdManager, cudd::ADD(internalDdManager.getCuddManager(), result));
storm::dd::Add<storm::dd::DdType::CUDD, ValueType> newPartitionAdd(oldPartition.asAdd().getDdManager(), internalNewPartitionAdd, oldPartition.asAdd().getContainedMetaVariables());
if (options.reuseSignatureResult) {
oldSignatureCache = signatureCache;
}
clearCaches();
return newPartitionAdd;
}
DdNodePtr encodeBlock(uint64_t blockIndex) {
for (auto const& blockDdVariableIndex : blockDdVariableIndices) {
blockEncoding[blockDdVariableIndex] = blockIndex & 1 ? 1 : 0;
@ -110,7 +165,102 @@ namespace storm {
return result;
}
DdNodePtr refine(DdNode* partitionNode, DdNode* signatureNode, DdNode* nondeterminismVariablesNode, DdNode* nonBlockVariablesNode) {
DdNodePtr refineReuseSignatureResults(DdNode* signatureNode, DdNode* nondeterminismVariablesNode, DdNode* nonBlockVariablesNode) {
// If we arrived at the constant zero node, then this was an illegal state encoding (we require
// all states to be non-deadlock).
if (signatureNode == Cudd_ReadZero(ddman)) {
return signatureNode;
}
// Check the cache whether we have seen the same node before.
auto it = signatureCache.find(signatureNode);
if (it != signatureCache.end()) {
// If so, we return the corresponding result.
return it->second;
}
// If we are to reuse signature results, check the old cache.
if (options.reuseSignatureResult) {
it = oldSignatureCache.find(signatureNode);
if (it != oldSignatureCache.end()) {
// If so, we return the corresponding result.
return it->second;
}
}
// If there are no more non-block variables, we hit the signature.
if (Cudd_IsConstant(nonBlockVariablesNode)) {
DdNode* result = encodeBlock(nextFreeBlockIndex++);
signatureCache[signatureNode] = result;
return result;
} else {
// If there are more variables that belong to the non-block part of the encoding, we need to recursively descend.
bool skipped = true;
DdNode* signatureThen;
DdNode* signatureElse;
short offset;
bool isNondeterminismVariable = false;
while (skipped && !Cudd_IsConstant(nonBlockVariablesNode)) {
// Remember an offset that indicates whether the top variable is a nondeterminism variable or not.
offset = options.shiftStateVariables ? 1 : 0;
if (!Cudd_IsConstant(nondeterminismVariablesNode) && Cudd_NodeReadIndex(nondeterminismVariablesNode) == Cudd_NodeReadIndex(nonBlockVariablesNode)) {
offset = 0;
isNondeterminismVariable = true;
}
if (Cudd_NodeReadIndex(signatureNode) == Cudd_NodeReadIndex(nonBlockVariablesNode)) {
signatureThen = Cudd_T(signatureNode);
signatureElse = Cudd_E(signatureNode);
skipped = false;
} else {
signatureThen = signatureElse = signatureNode;
}
// If we skipped the next variable, we fast-forward.
if (skipped) {
// If the current variable is a nondeterminism variable, we need to advance both variable sets otherwise just the non-block variables.
nonBlockVariablesNode = Cudd_T(nonBlockVariablesNode);
if (isNondeterminismVariable) {
nondeterminismVariablesNode = Cudd_T(nondeterminismVariablesNode);
}
}
}
// If there are no more non-block variables remaining, make a recursive call to enter the base case.
if (Cudd_IsConstant(nonBlockVariablesNode)) {
return refineReuseSignatureResults(signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode);
}
DdNode* thenResult = refineReuseSignatureResults(signatureThen, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode));
Cudd_Ref(thenResult);
DdNode* elseResult = refineReuseSignatureResults(signatureElse, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode));
Cudd_Ref(elseResult);
DdNode* result;
if (thenResult == elseResult) {
Cudd_Deref(thenResult);
Cudd_Deref(elseResult);
result = thenResult;
} else {
// Get the node to connect the subresults.
bool complemented = Cudd_IsComplement(thenResult);
result = cuddUniqueInter(ddman, Cudd_NodeReadIndex(nonBlockVariablesNode) + offset, Cudd_Regular(thenResult), complemented ? Cudd_Not(elseResult) : elseResult);
if (complemented) {
result = Cudd_Not(result);
}
Cudd_Deref(thenResult);
Cudd_Deref(elseResult);
}
// Store the result in the cache.
signatureCache[signatureNode] = result;
return result;
}
}
DdNodePtr refineReuseBlockNumber(DdNode* partitionNode, DdNode* signatureNode, DdNode* nondeterminismVariablesNode, DdNode* nonBlockVariablesNode) {
// If we arrived at the constant zero node, then this was an illegal state encoding (we require
// all states to be non-deadlock).
if (partitionNode == Cudd_ReadZero(ddman)) {
@ -119,8 +269,8 @@ namespace storm {
// Check the cache whether we have seen the same node before.
auto nodePair = std::make_pair(signatureNode, partitionNode);
auto it = signatureCache.find(nodePair);
if (it != signatureCache.end()) {
auto it = signatureCache2.find(nodePair);
if (it != signatureCache2.end()) {
// If so, we return the corresponding result.
return it->second;
}
@ -132,11 +282,11 @@ namespace storm {
auto& reuseEntry = reuseBlocksCache[partitionNode];
if (!reuseEntry.isReused()) {
reuseEntry.setReused();
signatureCache[nodePair] = partitionNode;
signatureCache2[nodePair] = partitionNode;
return partitionNode;
} else {
DdNode* result = encodeBlock(nextFreeBlockIndex++);
signatureCache[nodePair] = result;
signatureCache2[nodePair] = result;
return result;
}
} else {
@ -151,7 +301,7 @@ namespace storm {
bool isNondeterminismVariable = false;
while (skippedBoth && !Cudd_IsConstant(nonBlockVariablesNode)) {
// Remember an offset that indicates whether the top variable is a nondeterminism variable or not.
offset = shiftStateVariables ? 1 : 0;
offset = options.shiftStateVariables ? 1 : 0;
if (!Cudd_IsConstant(nondeterminismVariablesNode) && Cudd_NodeReadIndex(nondeterminismVariablesNode) == Cudd_NodeReadIndex(nonBlockVariablesNode)) {
offset = 0;
isNondeterminismVariable = true;
@ -185,12 +335,12 @@ namespace storm {
// If there are no more non-block variables remaining, make a recursive call to enter the base case.
if (Cudd_IsConstant(nonBlockVariablesNode)) {
return refine(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode);
return refineReuseBlockNumber(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode);
}
DdNode* thenResult = refine(partitionThen, signatureThen, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode));
DdNode* thenResult = refineReuseBlockNumber(partitionThen, signatureThen, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode));
Cudd_Ref(thenResult);
DdNode* elseResult = refine(partitionElse, signatureElse, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode));
DdNode* elseResult = refineReuseBlockNumber(partitionElse, signatureElse, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode));
Cudd_Ref(elseResult);
DdNode* result;
@ -210,7 +360,7 @@ namespace storm {
}
// Store the result in the cache.
signatureCache[nodePair] = result;
signatureCache2[nodePair] = result;
return result;
}
@ -224,9 +374,9 @@ namespace storm {
// The cubes representing all non-block and all nondeterminism variables, respectively.
storm::dd::Bdd<storm::dd::DdType::CUDD> nondeterminismVariables;
storm::dd::Bdd<storm::dd::DdType::CUDD> nonBlockVariables;
// A flag indicating whether we are to shift the state variables by one.
bool shiftStateVariables;
// The provided options.
InternalSignatureRefinerOptions options;
// The indices of the DD variables associated with the block variable.
std::vector<uint64_t> blockDdVariableIndices;
@ -244,7 +394,9 @@ namespace storm {
uint64_t lastNumberOfVisitedNodes;
// The cache used to identify states with identical signature.
spp::sparse_hash_map<std::pair<DdNode const*, DdNode const*>, DdNode*, CuddPointerPairHash> signatureCache;
spp::sparse_hash_map<DdNode const*, DdNode*> oldSignatureCache;
spp::sparse_hash_map<DdNode const*, DdNode*> signatureCache;
spp::sparse_hash_map<std::pair<DdNode const*, DdNode const*>, DdNode*, CuddPointerPairHash> signatureCache2;
// The cache used to identify which old block numbers have already been reused.
spp::sparse_hash_map<DdNode const*, ReuseWrapper> reuseBlocksCache;
@ -253,64 +405,79 @@ namespace storm {
template<typename ValueType>
class InternalSignatureRefiner<storm::dd::DdType::Sylvan, ValueType> {
public:
InternalSignatureRefiner(storm::dd::DdManager<storm::dd::DdType::Sylvan> const& manager, storm::expressions::Variable const& blockVariable, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& nondeterminismVariables, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& nonBlockVariables, bool shiftStateVariables) : manager(manager), internalDdManager(manager.getInternalDdManager()), blockVariable(blockVariable), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), shiftStateVariables(shiftStateVariables), numberOfBlockVariables(manager.getMetaVariable(blockVariable).getNumberOfDdVariables()), blockCube(manager.getMetaVariable(blockVariable).getCube()), nextFreeBlockIndex(0), numberOfRefinements(0), signatureCache() {
InternalSignatureRefiner(storm::dd::DdManager<storm::dd::DdType::Sylvan> const& manager, storm::expressions::Variable const& blockVariable, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& nondeterminismVariables, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& nonBlockVariables, InternalSignatureRefinerOptions const& options) : manager(manager), internalDdManager(manager.getInternalDdManager()), blockVariable(blockVariable), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), options(options), numberOfBlockVariables(manager.getMetaVariable(blockVariable).getNumberOfDdVariables()), blockCube(manager.getMetaVariable(blockVariable).getCube()), nextFreeBlockIndex(0), numberOfRefinements(0), signatureCache() {
// Perform garbage collection to clean up stuff not needed anymore.
LACE_ME;
sylvan_gc();
}
Partition<storm::dd::DdType::Sylvan, ValueType> refine(Partition<storm::dd::DdType::Sylvan, ValueType> const& oldPartition, Signature<storm::dd::DdType::Sylvan, ValueType> const& signature) {
storm::dd::Bdd<storm::dd::DdType::Sylvan> newPartitionBdd = refine(oldPartition, signature.getSignatureAdd());
return oldPartition.replacePartition(newPartitionBdd, nextFreeBlockIndex);
storm::dd::Bdd<storm::dd::DdType::Sylvan> newPartitionBdd;
if (options.reuseBlockNumbers && !options.reuseSignatureResult) {
newPartitionBdd = refineReuseBlockNumber(oldPartition, signature.getSignatureAdd());
} else {
newPartitionBdd = refineReuseSignatureResults(oldPartition, signature.getSignatureAdd());
}
auto start = std::chrono::high_resolution_clock::now();
uint64_t numberOfBlocks = nextFreeBlockIndex;
if (options.reuseSignatureResult) {
std::set<storm::expressions::Variable> blockVariableSet = {blockVariable};
std::set<storm::expressions::Variable> nonBlockExpressionVariables;
std::set_difference(oldPartition.asBdd().getContainedMetaVariables().begin(), oldPartition.asBdd().getContainedMetaVariables().end(), blockVariableSet.begin(), blockVariableSet.end(), std::inserter(nonBlockExpressionVariables, nonBlockExpressionVariables.begin()));
numberOfBlocks = newPartitionBdd.existsAbstract(nonBlockExpressionVariables).getNonZeroCount();
}
auto end = std::chrono::high_resolution_clock::now();
std::cout << "took " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << std::endl;
return oldPartition.replacePartition(newPartitionBdd, numberOfBlocks, nextFreeBlockIndex);
}
private:
storm::dd::Bdd<storm::dd::DdType::Sylvan> refine(Partition<storm::dd::DdType::Sylvan, ValueType> const& oldPartition, storm::dd::Add<storm::dd::DdType::Sylvan, ValueType> const& signatureAdd) {
void clearCaches() {
signatureCache.clear();
signatureCache2.clear();
reuseBlocksCache.clear();
}
storm::dd::Bdd<storm::dd::DdType::Sylvan> refineReuseBlockNumber(Partition<storm::dd::DdType::Sylvan, ValueType> const& oldPartition, storm::dd::Add<storm::dd::DdType::Sylvan, ValueType> const& signatureAdd) {
STORM_LOG_ASSERT(oldPartition.storedAsBdd(), "Expecting partition to be stored as BDD for Sylvan.");
LACE_ME;
// Set up next refinement.
++numberOfRefinements;
// Clear the caches.
std::size_t oldSize = signatureCache.size();
signatureCache.clear();
signatureCache.reserve(3 * oldSize);
reuseBlocksCache.clear();
reuseBlocksCache.reserve(3 * oldPartition.getNumberOfBlocks());
nextFreeBlockIndex = oldPartition.getNextFreeBlockIndex();
// Clear performance counters.
// signatureCacheLookups = 0;
// signatureCacheHits = 0;
// numberOfVisitedNodes = 0;
// totalSignatureCacheLookupTime = std::chrono::high_resolution_clock::duration(0);
// totalSignatureCacheStoreTime = std::chrono::high_resolution_clock::duration(0);
// totalReuseBlocksLookupTime = std::chrono::high_resolution_clock::duration(0);
// totalLevelLookupTime = std::chrono::high_resolution_clock::duration(0);
// totalBlockEncodingTime = std::chrono::high_resolution_clock::duration(0);
// totalMakeNodeTime = std::chrono::high_resolution_clock::duration(0);
// Perform the actual recursive refinement step.
BDD result = refine(oldPartition.asBdd().getInternalBdd().getSylvanBdd().GetBDD(), signatureAdd.getInternalAdd().getSylvanMtbdd().GetMTBDD(), nondeterminismVariables.getInternalBdd().getSylvanBdd().GetBDD(), nonBlockVariables.getInternalBdd().getSylvanBdd().GetBDD());
BDD result = refineReuseBlockNumber(oldPartition.asBdd().getInternalBdd().getSylvanBdd().GetBDD(), signatureAdd.getInternalAdd().getSylvanMtbdd().GetMTBDD(), nondeterminismVariables.getInternalBdd().getSylvanBdd().GetBDD(), nonBlockVariables.getInternalBdd().getSylvanBdd().GetBDD());
// Construct resulting BDD from the obtained node and the meta information.
storm::dd::InternalBdd<storm::dd::DdType::Sylvan> internalNewPartitionBdd(&internalDdManager, sylvan::Bdd(result));
storm::dd::Bdd<storm::dd::DdType::Sylvan> newPartitionBdd(oldPartition.asBdd().getDdManager(), internalNewPartitionBdd, oldPartition.asBdd().getContainedMetaVariables());
// // Display some statistics.
// STORM_LOG_TRACE("Refinement visited " << numberOfVisitedNodes << " nodes.");
// STORM_LOG_TRACE("Current #nodes in table: " << llmsset_count_marked(nodes) << " of " << llmsset_get_size(nodes) << ", cache: " << cache_getused() << " of " << cache_getsize() << ".");
// STORM_LOG_TRACE("Signature cache hits: " << signatureCacheHits << ", misses: " << (signatureCacheLookups - signatureCacheHits) << ".");
// STORM_LOG_TRACE("Signature cache lookup time: " << std::chrono::duration_cast<std::chrono::milliseconds>(totalSignatureCacheLookupTime).count() << "ms");
// STORM_LOG_TRACE("Signature cache store time: " << std::chrono::duration_cast<std::chrono::milliseconds>(totalSignatureCacheStoreTime).count() << "ms");
// STORM_LOG_TRACE("Signature cache total time: " << std::chrono::duration_cast<std::chrono::milliseconds>(totalSignatureCacheStoreTime + totalSignatureCacheLookupTime).count() << "ms");
// STORM_LOG_TRACE("Reuse blocks lookup time: " << std::chrono::duration_cast<std::chrono::milliseconds>(totalReuseBlocksLookupTime).count() << "ms");
// STORM_LOG_TRACE("Level lookup time: " << std::chrono::duration_cast<std::chrono::milliseconds>(totalLevelLookupTime).count() << "ms");
// STORM_LOG_TRACE("Block encoding time: " << std::chrono::duration_cast<std::chrono::milliseconds>(totalBlockEncodingTime).count() << "ms");
// STORM_LOG_TRACE("Make node time: " << std::chrono::duration_cast<std::chrono::milliseconds>(totalMakeNodeTime).count() << "ms");
clearCaches();
return newPartitionBdd;
}
storm::dd::Bdd<storm::dd::DdType::Sylvan> refineReuseSignatureResults(Partition<storm::dd::DdType::Sylvan, ValueType> const& oldPartition, storm::dd::Add<storm::dd::DdType::Sylvan, ValueType> const& signatureAdd) {
STORM_LOG_ASSERT(oldPartition.storedAsBdd(), "Expecting partition to be stored as BDD for Sylvan.");
// Set up next refinement.
++numberOfRefinements;
nextFreeBlockIndex = options.reuseSignatureResult ? oldPartition.getNextFreeBlockIndex() : 0;
// Perform the actual recursive refinement step.
BDD result = refineReuseSignatureResults(signatureAdd.getInternalAdd().getSylvanMtbdd().GetMTBDD(), nondeterminismVariables.getInternalBdd().getSylvanBdd().GetBDD(), nonBlockVariables.getInternalBdd().getSylvanBdd().GetBDD());
// Construct resulting BDD from the obtained node and the meta information.
storm::dd::InternalBdd<storm::dd::DdType::Sylvan> internalNewPartitionBdd(&internalDdManager, sylvan::Bdd(result));
storm::dd::Bdd<storm::dd::DdType::Sylvan> newPartitionBdd(oldPartition.asBdd().getDdManager(), internalNewPartitionBdd, oldPartition.asBdd().getContainedMetaVariables());
if (options.reuseSignatureResult) {
oldSignatureCache = signatureCache;
}
clearCaches();
return newPartitionBdd;
}
@ -323,7 +490,101 @@ namespace storm {
return sylvan_cube(blockCube.getInternalBdd().getSylvanBdd().GetBDD(), e.data());
}
BDD refine(BDD partitionNode, MTBDD signatureNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode) {
BDD refineReuseSignatureResults(MTBDD signatureNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode) {
LACE_ME;
// If we arrived at the constant zero node, then this was an illegal state encoding (we require
// all states to be non-deadlock).
if (mtbdd_iszero(signatureNode)) {
return sylvan_false;
}
// Check the cache whether we have seen the same node before.
auto it = signatureCache.find(signatureNode);
if (it != signatureCache.end()) {
// If so, we return the corresponding result.
return it->second;
}
// If we are to reuse signature results, check the old cache.
if (options.reuseSignatureResult) {
it = oldSignatureCache.find(signatureNode);
if (it != oldSignatureCache.end()) {
// If so, we return the corresponding result.
return it->second;
}
}
sylvan_gc_test();
// If there are no more non-block variables, we hit the signature.
if (sylvan_isconst(nonBlockVariablesNode)) {
BDD result = encodeBlock(nextFreeBlockIndex++);
signatureCache[signatureNode] = result;
return result;
} else {
// If there are more variables that belong to the non-block part of the encoding, we need to recursively descend.
bool skipped = true;
MTBDD signatureThen;
MTBDD signatureElse;
short offset;
bool isNondeterminismVariable = false;
while (skipped && !sylvan_isconst(nonBlockVariablesNode)) {
// Remember an offset that indicates whether the top variable is a nondeterminism variable or not.
offset = options.shiftStateVariables ? 1 : 0;
if (!sylvan_isconst(nondeterminismVariablesNode) && sylvan_var(nondeterminismVariablesNode) == sylvan_var(nonBlockVariablesNode)) {
offset = 0;
isNondeterminismVariable = true;
}
if (storm::dd::InternalAdd<storm::dd::DdType::Sylvan, ValueType>::matchesVariableIndex(signatureNode, sylvan_var(nonBlockVariablesNode))) {
signatureThen = sylvan_high(signatureNode);
signatureElse = sylvan_low(signatureNode);
skipped = false;
} else {
signatureThen = signatureElse = signatureNode;
}
// If we skipped the next variable, we fast-forward.
if (skipped) {
// If the current variable is a nondeterminism variable, we need to advance both variable sets otherwise just the non-block variables.
nonBlockVariablesNode = sylvan_high(nonBlockVariablesNode);
if (isNondeterminismVariable) {
nondeterminismVariablesNode = sylvan_high(nondeterminismVariablesNode);
}
}
}
// If there are no more non-block variables remaining, make a recursive call to enter the base case.
if (sylvan_isconst(nonBlockVariablesNode)) {
return refineReuseSignatureResults(signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode);
}
BDD thenResult = refineReuseSignatureResults(signatureThen, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode));
bdd_refs_push(thenResult);
BDD elseResult = refineReuseSignatureResults(signatureElse, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode));
bdd_refs_push(elseResult);
BDD result;
if (thenResult == elseResult) {
result = thenResult;
} else {
// Get the node to connect the subresults.
result = sylvan_makenode(sylvan_var(nonBlockVariablesNode) + offset, elseResult, thenResult);
}
// Dispose of the intermediate results.
bdd_refs_pop(2);
// Store the result in the cache.
signatureCache[signatureNode] = result;
return result;
}
}
BDD refineReuseBlockNumber(BDD partitionNode, MTBDD signatureNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode) {
LACE_ME;
// If we arrived at the constant zero node, then this was an illegal state encoding (we require
@ -336,8 +597,8 @@ namespace storm {
// Check the cache whether we have seen the same node before.
auto nodePair = std::make_pair(signatureNode, partitionNode);
auto it = signatureCache.find(nodePair);
if (it != signatureCache.end()) {
auto it = signatureCache2.find(nodePair);
if (it != signatureCache2.end()) {
// If so, we return the corresponding result.
return it->second;
}
@ -353,11 +614,11 @@ namespace storm {
if (!reuseBlockEntry.isReused()) {
reuseBlockEntry.setReused();
reuseBlocksCache.emplace(partitionNode, true);
signatureCache[nodePair] = partitionNode;
signatureCache2[nodePair] = partitionNode;
return partitionNode;
} else {
BDD result = encodeBlock(nextFreeBlockIndex++);
signatureCache[nodePair] = result;
signatureCache2[nodePair] = result;
return result;
}
} else {
@ -372,7 +633,7 @@ namespace storm {
bool isNondeterminismVariable = false;
while (skippedBoth && !sylvan_isconst(nonBlockVariablesNode)) {
// Remember an offset that indicates whether the top variable is a nondeterminism variable or not.
offset = shiftStateVariables ? 1 : 0;
offset = options.shiftStateVariables ? 1 : 0;
if (!sylvan_isconst(nondeterminismVariablesNode) && sylvan_var(nondeterminismVariablesNode) == sylvan_var(nonBlockVariablesNode)) {
offset = 0;
isNondeterminismVariable = true;
@ -406,12 +667,12 @@ namespace storm {
// If there are no more non-block variables remaining, make a recursive call to enter the base case.
if (sylvan_isconst(nonBlockVariablesNode)) {
return refine(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode);
return refineReuseBlockNumber(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode);
}
BDD thenResult = refine(partitionThen, signatureThen, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode));
BDD thenResult = refineReuseBlockNumber(partitionThen, signatureThen, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode));
bdd_refs_push(thenResult);
BDD elseResult = refine(partitionElse, signatureElse, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode));
BDD elseResult = refineReuseBlockNumber(partitionElse, signatureElse, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode));
bdd_refs_push(elseResult);
BDD result;
@ -426,7 +687,7 @@ namespace storm {
bdd_refs_pop(2);
// Store the result in the cache.
signatureCache[nodePair] = result;
signatureCache2[nodePair] = result;
return result;
}
@ -439,8 +700,9 @@ namespace storm {
storm::dd::Bdd<storm::dd::DdType::Sylvan> nondeterminismVariables;
storm::dd::Bdd<storm::dd::DdType::Sylvan> nonBlockVariables;
bool shiftStateVariables;
// The provided options.
InternalSignatureRefinerOptions options;
uint64_t numberOfBlockVariables;
storm::dd::Bdd<storm::dd::DdType::Sylvan> blockCube;
@ -452,7 +714,9 @@ namespace storm {
uint64_t numberOfRefinements;
// The cache used to identify states with identical signature.
spp::sparse_hash_map<std::pair<MTBDD, MTBDD>, MTBDD, SylvanMTBDDPairHash> signatureCache;
spp::sparse_hash_map<MTBDD, MTBDD> oldSignatureCache;
spp::sparse_hash_map<MTBDD, MTBDD> signatureCache;
spp::sparse_hash_map<std::pair<MTBDD, MTBDD>, MTBDD, SylvanMTBDDPairHash> signatureCache2;
// The cache used to identify which old block numbers have already been reused.
spp::sparse_hash_map<MTBDD, ReuseWrapper> reuseBlocksCache;
@ -467,7 +731,6 @@ namespace storm {
// std::chrono::high_resolution_clock::duration totalLevelLookupTime;
// std::chrono::high_resolution_clock::duration totalBlockEncodingTime;
// std::chrono::high_resolution_clock::duration totalMakeNodeTime;
};
template<storm::dd::DdType DdType, typename ValueType>
@ -485,7 +748,7 @@ namespace storm {
nonBlockVariablesCube &= cube;
}
internalRefiner = std::make_unique<InternalSignatureRefiner<DdType, ValueType>>(manager, blockVariable, nondeterminismVariablesCube, nonBlockVariablesCube, shiftStateVariables);
internalRefiner = std::make_unique<InternalSignatureRefiner<DdType, ValueType>>(manager, blockVariable, nondeterminismVariablesCube, nonBlockVariablesCube, InternalSignatureRefinerOptions(shiftStateVariables));
}
template<storm::dd::DdType DdType, typename ValueType>

Write Preview
Loading…
Cancel
Save