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

fixed DD-based quotient extraction in bisimulation

tempestpy_adaptions
dehnert 7 years ago
parent
653e5fc184
commit
cdf76b0c15
12 changed files with 46 additions and 39 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
      resources/3rdparty/CMakeLists.txt
  2. 1
      src/storm/cli/cli.cpp
  3. 1
      src/storm/storage/dd/BisimulationDecomposition.cpp
  4. 3
      src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp
  5. 1
      src/storm/storage/dd/bisimulation/Partition.cpp
  6. 2
      src/storm/storage/dd/bisimulation/PartitionRefiner.cpp
  7. 8
      src/storm/storage/dd/bisimulation/PreservationInformation.cpp
  8. 51
      src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
  9. 2
      src/storm/storage/dd/bisimulation/SignatureComputer.cpp
  10. 4
      src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp
  11. 2
      src/storm/storage/expressions/LinearityCheckVisitor.cpp
  12. 2
      src/storm/storage/expressions/ToRationalNumberVisitor.cpp

8
resources/3rdparty/CMakeLists.txt
View File

@ -418,12 +418,18 @@ else()
set(sylvan_dep lib_carl)
endif()
if (STORM_DEBUG_SYLVAN)
set(SYLVAN_BUILD_TYPE "Debug")
else()
set(SYLVAN_BUILD_TYPE "Release")
endif()
ExternalProject_Add(
sylvan
DOWNLOAD_COMMAND ""
PREFIX "sylvan"
SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/sylvan
CMAKE_ARGS -DCMAKE_C_COMPILER=${CMAKE_C_COMPILER} -DGMP_LOCATION=${GMP_LIB_LOCATION} -DGMP_INCLUDE=${GMP_INCLUDE_DIR} -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DSYLVAN_BUILD_DOCS=OFF -DSYLVAN_BUILD_EXAMPLES=OFF -DCMAKE_BUILD_TYPE=Release -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DUSE_CARL=ON -Dcarl_INCLUDE_DIR=${carl_INCLUDE_DIR} -DSYLVAN_PORTABLE=${STORM_PORTABLE} -Dcarl_LIBRARIES=${carl_LIBRARIES} -DBUILD_SHARED_LIBS=OFF -DSYLVAN_BUILD_TESTS=OFF
CMAKE_ARGS -DCMAKE_C_COMPILER=${CMAKE_C_COMPILER} -DGMP_LOCATION=${GMP_LIB_LOCATION} -DGMP_INCLUDE=${GMP_INCLUDE_DIR} -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DSYLVAN_BUILD_DOCS=OFF -DSYLVAN_BUILD_EXAMPLES=OFF -DCMAKE_BUILD_TYPE=${SYLVAN_BUILD_TYPE} -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DUSE_CARL=ON -Dcarl_INCLUDE_DIR=${carl_INCLUDE_DIR} -DSYLVAN_PORTABLE=${STORM_PORTABLE} -Dcarl_LIBRARIES=${carl_LIBRARIES} -DBUILD_SHARED_LIBS=OFF -DSYLVAN_BUILD_TESTS=OFF
BINARY_DIR ${STORM_3RDPARTY_BINARY_DIR}/sylvan
BUILD_IN_SOURCE 0
INSTALL_COMMAND ""

1
src/storm/cli/cli.cpp
View File

@ -514,6 +514,7 @@ namespace storm {
result = preprocessDdModel<DdType, ValueType>(result.first->as<storm::models::symbolic::Model<DdType, ValueType>>(), input);
}
preprocessingWatch.stop();
if (result.second) {
STORM_PRINT_AND_LOG(std::endl << "Time for model preprocessing: " << preprocessingWatch << "." << std::endl << std::endl);
}

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

@ -7,6 +7,7 @@
#include "storm/models/symbolic/Model.h"
#include "storm/models/symbolic/Mdp.h"
#include "storm/models/symbolic/StandardRewardModel.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidOperationException.h"

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

@ -1,6 +1,7 @@
#include "storm/storage/dd/bisimulation/MdpPartitionRefiner.h"
#include "storm/models/symbolic/Mdp.h"
#include "storm/models/symbolic/StandardRewardModel.h"
namespace storm {
namespace dd {
@ -9,8 +10,6 @@ namespace storm {
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(), 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>

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

@ -9,6 +9,7 @@
#include "storm/logic/AtomicLabelFormula.h"
#include "storm/models/symbolic/Mdp.h"
#include "storm/models/symbolic/StandardRewardModel.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/BisimulationSettings.h"

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

@ -1,5 +1,7 @@
#include "storm/storage/dd/bisimulation/PartitionRefiner.h"
#include "storm/models/symbolic/StandardRewardModel.h"
namespace storm {
namespace dd {
namespace bisimulation {

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

@ -2,6 +2,8 @@
#include "storm/logic/Formulas.h"
#include "storm/models/symbolic/StandardRewardModel.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidPropertyException.h"
@ -15,7 +17,7 @@ namespace storm {
}
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& bisimulationType) {
PreservationInformation<DdType, ValueType>::PreservationInformation(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::string> const& labels, storm::storage::BisimulationType const&) {
for (auto const& label : labels) {
this->addLabel(label);
this->addExpression(model.getExpression(label));
@ -23,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& bisimulationType) {
PreservationInformation<DdType, ValueType>::PreservationInformation(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<storm::expressions::Expression> const& expressions, storm::storage::BisimulationType const&) {
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& bisimulationType) {
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&) {
if (formulas.empty()) {
// Default to respect all labels if no formulas are given.
for (auto const& label : model.getLabels()) {

51
src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
View File

@ -551,9 +551,6 @@ namespace storm {
// Sanity checks.
STORM_LOG_ASSERT(partition.getNumberOfStates() == model.getNumberOfStates(), "Mismatching partition size.");
partition.getStates().renameVariables(model.getColumnVariables(), model.getRowVariables()).exportToDot("partstates.dot");
model.getReachableStates().exportToDot("origstates.dot");
std::cout << "equal? " << (partition.getStates().renameVariables(model.getColumnVariables(), model.getRowVariables()).template toAdd<ValueType>().notZero() == model.getReachableStates().template toAdd<ValueType>().notZero()) << std::endl;
STORM_LOG_ASSERT(partition.getStates().renameVariables(model.getColumnVariables(), model.getRowVariables()) == model.getReachableStates(), "Mismatching partition.");
std::set<storm::expressions::Variable> blockVariableSet = {partition.getBlockVariable()};
@ -567,36 +564,10 @@ namespace storm {
partitionAsBdd = (representativePartition && partitionAsBddOverPrimedBlockVariable).existsAbstract(blockPrimeVariableSet);
}
storm::dd::Add<DdType, ValueType> partitionAsAdd = partitionAsBdd.template toAdd<ValueType>();
partitionAsAdd.exportToDot("partition.dot");
model.getTransitionMatrix().sumAbstract(model.getColumnVariables()).exportToDot("origdist.dot");
auto start = std::chrono::high_resolution_clock::now();
storm::dd::Add<DdType, ValueType> quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(blockVariableSet, blockPrimeVariableSet), model.getColumnVariables());
STORM_LOG_ASSERT(quotientTransitionMatrix.sumAbstract(blockPrimeVariableSet).equalModuloPrecision(model.getTransitionMatrix().sumAbstract(model.getColumnVariables()), ValueType(1e-6)), "Expected something else.");
quotientTransitionMatrix.sumAbstract(blockPrimeVariableSet).exportToDot("sanity.dot");
quotientTransitionMatrix.exportToDot("trans-1.dot");
partitionAsAdd = partitionAsAdd / partitionAsAdd.sumAbstract(model.getColumnVariables());
quotientTransitionMatrix = quotientTransitionMatrix.multiplyMatrix(partitionAsAdd.renameVariables(model.getColumnVariables(), model.getRowVariables()), model.getRowVariables());
quotientTransitionMatrix.exportToDot("quottrans.dot");
auto partCount = partitionAsAdd.sumAbstract(model.getColumnVariables());
partCount.exportToDot("partcount.dot");
auto end = std::chrono::high_resolution_clock::now();
// Check quotient matrix for sanity.
auto quotdist = quotientTransitionMatrix.sumAbstract(blockPrimeVariableSet);
quotdist.exportToDot("quotdists.dot");
(quotdist / partCount).exportToDot("distcount.dot");
STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one<ValueType>()).isZero(), "Illegal entries in quotient matrix.");
STORM_LOG_ASSERT(quotientTransitionMatrix.sumAbstract(blockPrimeVariableSet).equalModuloPrecision(quotientTransitionMatrix.notZero().existsAbstract(blockPrimeVariableSet).template toAdd<ValueType>(), ValueType(1e-6)), "Illegal non-probabilistic matrix.");
STORM_LOG_TRACE("Quotient transition matrix extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
storm::dd::Bdd<DdType> quotientTransitionMatrixBdd = quotientTransitionMatrix.notZero();
start = std::chrono::high_resolution_clock::now();
storm::dd::Bdd<DdType> partitionAsBddOverRowVariables = partitionAsBdd.renameVariables(model.getColumnVariables(), model.getRowVariables());
storm::dd::Bdd<DdType> reachableStates = partitionAsBdd.existsAbstract(model.getColumnVariables());
storm::dd::Bdd<DdType> initialStates = (model.getInitialStates() && partitionAsBddOverRowVariables).existsAbstract(model.getRowVariables());
storm::dd::Bdd<DdType> deadlockStates = !quotientTransitionMatrixBdd.existsAbstract(blockPrimeVariableSet) && reachableStates;
std::map<std::string, storm::dd::Bdd<DdType>> preservedLabelBdds;
for (auto const& label : preservationInformation.getLabels()) {
@ -614,9 +585,29 @@ namespace storm {
preservedLabelBdds.emplace(stream.str(), (model.getStates(expression) && partitionAsBddOverRowVariables).existsAbstract(model.getRowVariables()));
}
}
end = std::chrono::high_resolution_clock::now();
auto end = std::chrono::high_resolution_clock::now();
STORM_LOG_TRACE("Quotient labels extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
storm::dd::Add<DdType, ValueType> partitionAsAdd = partitionAsBdd.template toAdd<ValueType>();
start = std::chrono::high_resolution_clock::now();
storm::dd::Add<DdType, ValueType> quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(blockVariableSet, blockPrimeVariableSet), model.getColumnVariables());
// Pick a representative from each block.
partitionAsBdd = partitionAsBdd.existsAbstractRepresentative(model.getColumnVariables());
partitionAsAdd = partitionAsBdd.template toAdd<ValueType>();
quotientTransitionMatrix = quotientTransitionMatrix.multiplyMatrix(partitionAsAdd.renameVariables(model.getColumnVariables(), model.getRowVariables()), model.getRowVariables());
end = std::chrono::high_resolution_clock::now();
// Check quotient matrix for sanity.
STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one<ValueType>()).isZero(), "Illegal entries in quotient matrix.");
STORM_LOG_ASSERT(quotientTransitionMatrix.sumAbstract(blockPrimeVariableSet).equalModuloPrecision(quotientTransitionMatrix.notZero().existsAbstract(blockPrimeVariableSet).template toAdd<ValueType>(), ValueType(1e-6)), "Illegal non-probabilistic matrix.");
STORM_LOG_TRACE("Quotient transition matrix extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
storm::dd::Bdd<DdType> quotientTransitionMatrixBdd = quotientTransitionMatrix.notZero();
storm::dd::Bdd<DdType> deadlockStates = !quotientTransitionMatrixBdd.existsAbstract(blockPrimeVariableSet) && reachableStates;
if (modelType == storm::models::ModelType::Dtmc) {
return std::shared_ptr<storm::models::symbolic::Dtmc<DdType, ValueType>>(new storm::models::symbolic::Dtmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, {}));
} else if (modelType == storm::models::ModelType::Ctmc) {

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

@ -2,6 +2,8 @@
#include "storm/storage/dd/DdManager.h"
#include "storm/models/symbolic/StandardRewardModel.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/OutOfRangeException.h"

4
src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp
View File

@ -67,8 +67,8 @@ namespace storm {
maxTableSize >>= 1;
}
uint64_t initialTableSize = 1ull << std::max(powerOfTwo - 4, 16ull);
uint64_t initialCacheSize = 1ull << std::max(powerOfTwo - 4, 16ull);
uint64_t initialTableSize = 1ull << std::max(powerOfTwo - 4, static_cast<uint_fast64_t>(16));
uint64_t initialCacheSize = initialTableSize;
STORM_LOG_DEBUG("Initializing sylvan. Initial/max table size: " << initialTableSize << "/" << maxTableSize << ", initial/max cache size: " << initialCacheSize << "/" << maxCacheSize << ".");
sylvan::Sylvan::initPackage(initialTableSize, maxTableSize, initialCacheSize, maxCacheSize);

2
src/storm/storage/expressions/LinearityCheckVisitor.cpp
View File

@ -125,7 +125,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Illegal unary numerical expression operator.");
}
boost::any LinearityCheckVisitor::visit(BooleanLiteralExpression const& expression, boost::any const& data) {
boost::any LinearityCheckVisitor::visit(BooleanLiteralExpression const&, boost::any const& data) {
bool booleanIsLinear = boost::any_cast<bool>(data);
if (booleanIsLinear) {

2
src/storm/storage/expressions/ToRationalNumberVisitor.cpp
View File

@ -119,6 +119,8 @@ namespace storm {
return result;
break;
}
// Dummy return.
return result;
}
template<typename RationalNumberType>
Write Preview
Loading…
Cancel
Save