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

fixed severe bug in symbolic bisimulation minimization

tempestpy_adaptions
dehnert 7 years ago
parent
45a4b63a2e
commit
a427eae699
9 changed files with 50 additions and 33 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 8
      src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp
  2. 2
      src/storm/solver/SymbolicNativeLinearEquationSolver.cpp
  3. 2
      src/storm/storage/dd/BisimulationDecomposition.cpp
  4. 2
      src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp
  5. 2
      src/storm/storage/dd/bisimulation/Partition.cpp
  6. 4
      src/storm/storage/dd/bisimulation/PartitionRefiner.cpp
  7. 37
      src/storm/storage/dd/bisimulation/SignatureRefiner.cpp
  8. 2
      src/storm/storage/dd/bisimulation/SignatureRefiner.h
  9. 24
      src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp

8
src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp
View File

@ -35,6 +35,14 @@ namespace storm {
default:
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique.");
}
// Adjust the method if none was specified and we are using rational numbers.
if (std::is_same<ValueType, storm::RationalNumber>::value) {
if (settings.isMinMaxEquationSolvingMethodSetFromDefaultValue() && this->solutionMethod != SolutionMethod::RationalSearch) {
STORM_LOG_INFO("Selecting 'rational search' as the solution technique to guarantee exact results. If you want to override this, please explicitly specify a different method.");
this->solutionMethod = SolutionMethod::RationalSearch;
}
}
}
template<typename ValueType>

2
src/storm/solver/SymbolicNativeLinearEquationSolver.cpp
View File

@ -39,7 +39,7 @@ namespace storm {
// Adjust the method if none was specified and we are using rational numbers.
if (std::is_same<ValueType, storm::RationalNumber>::value) {
if (settings.isLinearEquationSystemTechniqueSetFromDefaultValue() && this->method != SolutionMethod::RationalSearch) {
STORM_LOG_INFO("Selecting the rational search as the solution technique to guarantee exact results. If you want to override this, please explicitly specify a different method.");
STORM_LOG_INFO("Selecting 'rational search' as the solution technique to guarantee exact results. If you want to override this, please explicitly specify a different method.");
this->method = SolutionMethod::RationalSearch;
}
}

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

@ -94,7 +94,7 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType>
std::shared_ptr<storm::models::Model<ValueType>> BisimulationDecomposition<DdType, ValueType>::getQuotient() const {
STORM_LOG_THROW(this->refiner->getStatus() == Status::FixedPoint, storm::exceptions::InvalidOperationException, "Cannot extract quotient, because bisimulation decomposition was not completed.");
STORM_LOG_TRACE("Starting quotient extraction.");
QuotientExtractor<DdType, ValueType> extractor;
std::shared_ptr<storm::models::Model<ValueType>> quotient = extractor.extract(model, refiner->getStatePartition(), preservationInformation);

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

@ -8,7 +8,7 @@ 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(), mdp.getColumnAndNondeterminismVariables(), SignatureMode::Qualitative, true), 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(), true) {
// Intentionally left empty.
}

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

@ -100,7 +100,7 @@ namespace storm {
template<storm::dd::DdType DdType, typename ValueType>
Partition<DdType, ValueType> Partition<DdType, ValueType>::createTrivialChoicePartition(storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, std::pair<storm::expressions::Variable, storm::expressions::Variable> const& blockVariables) {
storm::dd::Bdd<DdType> choicePartitionBdd = !model.getIllegalMask().renameVariables(model.getRowVariables(), model.getColumnVariables()) && model.getManager().getEncoding(blockVariables.first, 0, false);
storm::dd::Bdd<DdType> choicePartitionBdd = (!model.getIllegalMask() && model.getReachableStates()).renameVariables(model.getRowVariables(), model.getColumnVariables()) && model.getManager().getEncoding(blockVariables.first, 0, false);
// Store the partition as an ADD only in the case of CUDD.
if (DdType == storm::dd::DdType::CUDD) {

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

@ -10,7 +10,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.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.isOfType(storm::models::ModelType::Mdp), model.getNondeterminismVariables()) {
// Intentionally left empty.
}
@ -50,7 +50,7 @@ namespace storm {
STORM_LOG_TRACE("Signature " << refinements << "[" << index << "] DD has " << signature.getSignatureAdd().getNodeCount() << " nodes.");
auto refinementStart = std::chrono::high_resolution_clock::now();
newPartition = signatureRefiner.refine(statePartition, signature);
newPartition = signatureRefiner.refine(oldPartition, signature);
auto refinementEnd = std::chrono::high_resolution_clock::now();
totalRefinementTime += (refinementEnd - refinementStart);

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

@ -61,7 +61,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) : manager(manager), internalDdManager(manager.getInternalDdManager()), ddman(internalDdManager.getCuddManager().getManager()), blockVariable(blockVariable), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), 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, 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) {
// Initialize precomputed data.
auto const& ddMetaVariable = manager.getMetaVariable(blockVariable);
@ -147,12 +147,14 @@ namespace storm {
DdNode* partitionElse;
DdNode* signatureThen;
DdNode* signatureElse;
short offset = 1;
short offset;
bool isNondeterminismVariable = false;
while (skippedBoth && !Cudd_IsConstant(nonBlockVariablesNode)) {
// Remember an offset that indicates whether the top variable is a nondeterminism variable or not.
offset = 1;
offset = shiftStateVariables ? 1 : 0;
if (!Cudd_IsConstant(nondeterminismVariablesNode) && Cudd_NodeReadIndex(nondeterminismVariablesNode) == Cudd_NodeReadIndex(nonBlockVariablesNode)) {
offset = 0;
isNondeterminismVariable = true;
}
if (Cudd_NodeReadIndex(partitionNode) - offset == Cudd_NodeReadIndex(nonBlockVariablesNode)) {
@ -175,7 +177,7 @@ namespace storm {
if (skippedBoth) {
// 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 (offset == 0) {
if (isNondeterminismVariable) {
nondeterminismVariablesNode = Cudd_T(nondeterminismVariablesNode);
}
}
@ -186,9 +188,9 @@ namespace storm {
return refine(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode);
}
DdNode* thenResult = refine(partitionThen, signatureThen, offset == 0 ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode));
DdNode* thenResult = refine(partitionThen, signatureThen, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode));
Cudd_Ref(thenResult);
DdNode* elseResult = refine(partitionElse, signatureElse, offset == 0 ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode));
DdNode* elseResult = refine(partitionElse, signatureElse, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode));
Cudd_Ref(elseResult);
DdNode* result;
@ -223,6 +225,9 @@ namespace storm {
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 indices of the DD variables associated with the block variable.
std::vector<uint64_t> blockDdVariableIndices;
@ -248,7 +253,7 @@ 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) : manager(manager), internalDdManager(manager.getInternalDdManager()), blockVariable(blockVariable), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), 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, 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() {
// Perform garbage collection to clean up stuff not needed anymore.
LACE_ME;
sylvan_gc();
@ -363,12 +368,14 @@ namespace storm {
BDD partitionElse;
MTBDD signatureThen;
MTBDD signatureElse;
short offset = 1;
short offset;
bool isNondeterminismVariable = false;
while (skippedBoth && !sylvan_isconst(nonBlockVariablesNode)) {
// Remember an offset that indicates whether the top variable is a nondeterminism variable or not.
offset = 1;
offset = 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(partitionNode, sylvan_var(nonBlockVariablesNode), -offset)) {
@ -391,7 +398,7 @@ namespace storm {
if (skippedBoth) {
// 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 (offset == 0) {
if (isNondeterminismVariable) {
nondeterminismVariablesNode = sylvan_high(nondeterminismVariablesNode);
}
}
@ -402,9 +409,9 @@ namespace storm {
return refine(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode);
}
BDD thenResult = refine(partitionThen, signatureThen, offset == 0 ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode));
BDD thenResult = refine(partitionThen, signatureThen, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode));
bdd_refs_push(thenResult);
BDD elseResult = refine(partitionElse, signatureElse, offset == 0 ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode));
BDD elseResult = refine(partitionElse, signatureElse, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode));
bdd_refs_push(elseResult);
BDD result;
@ -432,6 +439,8 @@ namespace storm {
storm::dd::Bdd<storm::dd::DdType::Sylvan> nondeterminismVariables;
storm::dd::Bdd<storm::dd::DdType::Sylvan> nonBlockVariables;
bool shiftStateVariables;
uint64_t numberOfBlockVariables;
storm::dd::Bdd<storm::dd::DdType::Sylvan> blockCube;
@ -462,7 +471,7 @@ namespace storm {
};
template<storm::dd::DdType DdType, typename ValueType>
SignatureRefiner<DdType, ValueType>::SignatureRefiner(storm::dd::DdManager<DdType> const& manager, storm::expressions::Variable const& blockVariable, std::set<storm::expressions::Variable> const& stateVariables, std::set<storm::expressions::Variable> const& nondeterminismVariables) : manager(&manager), stateVariables(stateVariables) {
SignatureRefiner<DdType, ValueType>::SignatureRefiner(storm::dd::DdManager<DdType> const& manager, storm::expressions::Variable const& blockVariable, std::set<storm::expressions::Variable> const& stateVariables, bool shiftStateVariables, std::set<storm::expressions::Variable> const& nondeterminismVariables) : manager(&manager), stateVariables(stateVariables) {
storm::dd::Bdd<DdType> nonBlockVariablesCube = manager.getBddOne();
storm::dd::Bdd<DdType> nondeterminismVariablesCube = manager.getBddOne();
@ -476,7 +485,7 @@ namespace storm {
nonBlockVariablesCube &= cube;
}
internalRefiner = std::make_unique<InternalSignatureRefiner<DdType, ValueType>>(manager, blockVariable, nondeterminismVariablesCube, nonBlockVariablesCube);
internalRefiner = std::make_unique<InternalSignatureRefiner<DdType, ValueType>>(manager, blockVariable, nondeterminismVariablesCube, nonBlockVariablesCube, shiftStateVariables);
}
template<storm::dd::DdType DdType, typename ValueType>

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

@ -17,7 +17,7 @@ namespace storm {
template<storm::dd::DdType DdType, typename ValueType>
class SignatureRefiner {
public:
SignatureRefiner(storm::dd::DdManager<DdType> const& manager, storm::expressions::Variable const& blockVariable, std::set<storm::expressions::Variable> const& stateVariables, std::set<storm::expressions::Variable> const& nondeterminismVariables = std::set<storm::expressions::Variable>());
SignatureRefiner(storm::dd::DdManager<DdType> const& manager, storm::expressions::Variable const& blockVariable, std::set<storm::expressions::Variable> const& stateVariables, bool shiftStateVariables, std::set<storm::expressions::Variable> const& nondeterminismVariables = std::set<storm::expressions::Variable>());
Partition<DdType, ValueType> refine(Partition<DdType, ValueType> const& oldPartition, Signature<DdType, ValueType> const& signature);

24
src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp
View File

@ -87,11 +87,11 @@ TEST(SymbolicModelBisimulationDecomposition, TwoDice_Cudd) {
decomposition.compute();
std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient();
EXPECT_EQ(77ul, quotient->getNumberOfStates());
EXPECT_EQ(210ul, quotient->getNumberOfTransitions());
EXPECT_EQ(135ul, quotient->getNumberOfStates());
EXPECT_EQ(366ul, quotient->getNumberOfTransitions());
EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType());
EXPECT_TRUE(quotient->isSymbolicModel());
EXPECT_EQ(116ul, (quotient->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>()->getNumberOfChoices()));
EXPECT_EQ(194ul, (quotient->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>()->getNumberOfChoices()));
storm::parser::FormulaParser formulaParser;
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
@ -103,11 +103,11 @@ TEST(SymbolicModelBisimulationDecomposition, TwoDice_Cudd) {
decomposition2.compute();
quotient = decomposition2.getQuotient();
EXPECT_EQ(19ul, quotient->getNumberOfStates());
EXPECT_EQ(58ul, quotient->getNumberOfTransitions());
EXPECT_EQ(40ul, quotient->getNumberOfStates());
EXPECT_EQ(110ul, quotient->getNumberOfTransitions());
EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType());
EXPECT_TRUE(quotient->isSymbolicModel());
EXPECT_EQ(34ul, (quotient->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>()->getNumberOfChoices()));
EXPECT_EQ(66ul, (quotient->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>()->getNumberOfChoices()));
}
TEST(SymbolicModelBisimulationDecomposition, AsynchronousLeader_Cudd) {
@ -125,11 +125,11 @@ TEST(SymbolicModelBisimulationDecomposition, AsynchronousLeader_Cudd) {
decomposition.compute();
std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient();
EXPECT_EQ(252ul, quotient->getNumberOfStates());
EXPECT_EQ(624ul, quotient->getNumberOfTransitions());
EXPECT_EQ(1166ul, quotient->getNumberOfStates());
EXPECT_EQ(2769ul, quotient->getNumberOfTransitions());
EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType());
EXPECT_TRUE(quotient->isSymbolicModel());
EXPECT_EQ(500ul, (quotient->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>()->getNumberOfChoices()));
EXPECT_EQ(2237ul, (quotient->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>()->getNumberOfChoices()));
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
formulas.push_back(formula);
@ -138,9 +138,9 @@ TEST(SymbolicModelBisimulationDecomposition, AsynchronousLeader_Cudd) {
decomposition2.compute();
quotient = decomposition2.getQuotient();
EXPECT_EQ(252ul, quotient->getNumberOfStates());
EXPECT_EQ(624ul, quotient->getNumberOfTransitions());
EXPECT_EQ(1166ul, quotient->getNumberOfStates());
EXPECT_EQ(2769ul, quotient->getNumberOfTransitions());
EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType());
EXPECT_TRUE(quotient->isSymbolicModel());
EXPECT_EQ(500ul, (quotient->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>()->getNumberOfChoices()));
EXPECT_EQ(2237ul, (quotient->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>()->getNumberOfChoices()));
}
Write Preview
Loading…
Cancel
Save