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

not calling sylvan_var on leaf nodes of sylvan anymore

tempestpy_adaptions
dehnert 8 years ago
parent
5856d9fe51
commit
e2e1407f3e
9 changed files with 51 additions and 20 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. 1
      CHANGELOG.md
  2. 2
      resources/3rdparty/sylvan/src/storm_wrapper.cpp
  3. 6
      src/storm/solver/SymbolicLinearEquationSolver.cpp
  4. 23
      src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
  5. 4
      src/storm/storage/dd/bisimulation/SignatureRefiner.cpp
  6. 5
      src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp
  7. 10
      src/storm/storage/dd/sylvan/InternalSylvanAdd.h
  8. 10
      src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp
  9. 10
      src/storm/storage/dd/sylvan/InternalSylvanBdd.h

1
CHANGELOG.md
View File

@ -12,6 +12,7 @@ Long run average computation via ValueIteration, LP based MDP model checking, pa
- c++ api changes: Building model takes BuilderOptions instead of extended list of Booleans, does not depend on settings anymore.
- storm-cli-utilities now contains cli related stuff, instead of storm-lib
- storm-pars: support for welldefinedness constraints in mdps.
- symbolic (MT/BDD) bisimulation
### Version 1.1.0 (2017/8)

2
resources/3rdparty/sylvan/src/storm_wrapper.cpp
View File

@ -125,6 +125,8 @@ int storm_rational_number_is_zero(storm_rational_number_ptr a) {
std::lock_guard<std::mutex> lock(rationalNumberMutex);
#endif
std::cout << "got ptr for eq check " << a << std::endl;
return storm::utility::isZero(*(storm::RationalNumber const*)a) ? 1 : 0;
}

6
src/storm/solver/SymbolicLinearEquationSolver.cpp
View File

@ -63,12 +63,10 @@ namespace storm {
std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<DdType, storm::RationalNumber>> GeneralSymbolicLinearEquationSolverFactory<DdType, storm::RationalNumber>::create(storm::dd::Add<DdType, storm::RationalNumber> const& A, storm::dd::Bdd<DdType> const& allRows, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs) const {
auto const& coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
storm::solver::EquationSolverType equationSolver;
if (coreSettings.isEquationSolverSetFromDefaultValue()) {
storm::solver::EquationSolverType equationSolver = coreSettings.getEquationSolver();
if (coreSettings.isEquationSolverSetFromDefaultValue() && equationSolver != storm::solver::EquationSolverType::Elimination) {
STORM_LOG_WARN("Selecting the elimination solver to guarantee exact results. If you want to override this, please explicitly specify a different equation solver.");
equationSolver = storm::solver::EquationSolverType::Elimination;
} else {
equationSolver = coreSettings.getEquationSolver();
}
if (equationSolver != storm::solver::EquationSolverType::Elimination) {

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

@ -175,7 +175,7 @@ namespace storm {
bool skipped = false;
BDD elsePartitionNode;
BDD thenPartitionNode;
if (sylvan_var(partitionNode) == sylvan_var(stateVariablesCube)) {
if (storm::dd::InternalBdd<storm::dd::DdType::Sylvan>::matchesVariableIndex(partitionNode, sylvan_var(stateVariablesCube))) {
elsePartitionNode = sylvan_low(partitionNode);
thenPartitionNode = sylvan_high(partitionNode);
} else {
@ -652,7 +652,7 @@ namespace storm {
} else {
MTBDD vectorT;
MTBDD vectorE;
if (sylvan_var(vector) == sylvan_var(variables)) {
if (storm::dd::InternalAdd<storm::dd::DdType::Sylvan, ValueType>::matchesVariableIndex(vector, sylvan_var(variables))) {
vectorT = sylvan_high(vector);
vectorE = sylvan_low(vector);
} else {
@ -661,7 +661,7 @@ namespace storm {
BDD representativesT;
BDD representativesE;
if (sylvan_var(representativesNode) == sylvan_var(variables)) {
if (storm::dd::InternalBdd<storm::dd::DdType::Sylvan>::matchesVariableIndex(representativesNode, sylvan_var(variables))) {
representativesT = sylvan_high(representativesNode);
representativesE = sylvan_low(representativesNode);
} else {
@ -692,7 +692,7 @@ namespace storm {
STORM_LOG_ASSERT(!odd.isTerminalNode(), "Expected non-terminal node.");
BDD partitionT;
BDD partitionE;
if (sylvan_var(partitionNode) == sylvan_var(variables)) {
if (storm::dd::InternalBdd<storm::dd::DdType::Sylvan>::matchesVariableIndex(partitionNode, sylvan_var(variables))) {
partitionT = sylvan_high(partitionNode);
partitionE = sylvan_low(partitionNode);
} else {
@ -701,7 +701,7 @@ namespace storm {
BDD representativesT;
BDD representativesE;
if (sylvan_var(representativesNode) == sylvan_var(variables)) {
if (storm::dd::InternalBdd<storm::dd::DdType::Sylvan>::matchesVariableIndex(representativesNode, sylvan_var(variables))) {
representativesT = sylvan_high(representativesNode);
representativesE = sylvan_low(representativesNode);
} else {
@ -714,6 +714,7 @@ namespace storm {
}
void extractTransitionMatrixRec(MTBDD transitionMatrixNode, storm::dd::Odd const& sourceOdd, uint64_t sourceOffset, BDD targetPartitionNode, BDD representativesNode, BDD variables, BDD nondeterminismVariables, storm::dd::Odd const* stateOdd, uint64_t stateOffset) {
// For the empty DD, we do not need to add any entries. Note that the partition nodes cannot be zero
// as all states of the model have to be contained.
if (mtbdd_iszero(transitionMatrixNode) || representativesNode == sylvan_false) {
@ -736,7 +737,7 @@ namespace storm {
MTBDD e;
// Determine whether the variable was skipped in the matrix.
if (sylvan_var(transitionMatrixNode) == sylvan_var(variables)) {
if (storm::dd::InternalAdd<storm::dd::DdType::Sylvan, ValueType>::matchesVariableIndex(transitionMatrixNode, sylvan_var(variables))) {
t = sylvan_high(transitionMatrixNode);
e = sylvan_low(transitionMatrixNode);
} else {
@ -753,7 +754,7 @@ namespace storm {
MTBDD e;
MTBDD et;
MTBDD ee;
if (sylvan_var(transitionMatrixNode) == sylvan_var(variables)) {
if (storm::dd::InternalAdd<storm::dd::DdType::Sylvan, ValueType>::matchesVariableIndex(transitionMatrixNode, sylvan_var(variables))) {
// Source node was not skipped in transition matrix.
t = sylvan_high(transitionMatrixNode);
e = sylvan_low(transitionMatrixNode);
@ -761,7 +762,7 @@ namespace storm {
t = e = transitionMatrixNode;
}
if (sylvan_var(t) == sylvan_var(variables) + 1) {
if (storm::dd::InternalAdd<storm::dd::DdType::Sylvan, ValueType>::matchesVariableIndex(t, sylvan_var(variables) + 1)) {
// Target node was not skipped in transition matrix.
tt = sylvan_high(t);
te = sylvan_low(t);
@ -770,7 +771,7 @@ namespace storm {
tt = te = t;
}
if (t != e) {
if (sylvan_var(e) == sylvan_var(variables) + 1) {
if (storm::dd::InternalAdd<storm::dd::DdType::Sylvan, ValueType>::matchesVariableIndex(e, sylvan_var(variables) + 1)) {
// Target node was not skipped in transition matrix.
et = sylvan_high(e);
ee = sylvan_low(e);
@ -785,7 +786,7 @@ namespace storm {
BDD targetT;
BDD targetE;
if (sylvan_var(targetPartitionNode) == sylvan_var(variables)) {
if (storm::dd::InternalBdd<storm::dd::DdType::Sylvan>::matchesVariableIndex(targetPartitionNode, sylvan_var(variables))) {
// Node was not skipped in target partition.
targetT = sylvan_high(targetPartitionNode);
targetE = sylvan_low(targetPartitionNode);
@ -796,7 +797,7 @@ namespace storm {
BDD representativesT;
BDD representativesE;
if (sylvan_var(representativesNode) == sylvan_var(variables)) {
if (storm::dd::InternalBdd<storm::dd::DdType::Sylvan>::matchesVariableIndex(representativesNode, sylvan_var(variables))) {
// Node was not skipped in representatives.
representativesT = sylvan_high(representativesNode);
representativesE = sylvan_low(representativesNode);

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

@ -371,7 +371,7 @@ namespace storm {
offset = 0;
}
if (sylvan_var(partitionNode) - offset == sylvan_var(nonBlockVariablesNode)) {
if (storm::dd::InternalAdd<storm::dd::DdType::Sylvan, ValueType>::matchesVariableIndex(partitionNode, sylvan_var(nonBlockVariablesNode), -offset)) {
partitionThen = sylvan_high(partitionNode);
partitionElse = sylvan_low(partitionNode);
skippedBoth = false;
@ -379,7 +379,7 @@ namespace storm {
partitionThen = partitionElse = partitionNode;
}
if (sylvan_var(signatureNode) == sylvan_var(nonBlockVariablesNode)) {
if (storm::dd::InternalAdd<storm::dd::DdType::Sylvan, ValueType>::matchesVariableIndex(signatureNode, sylvan_var(nonBlockVariablesNode))) {
signatureThen = sylvan_high(signatureNode);
signatureElse = sylvan_low(signatureNode);
skippedBoth = false;

5
src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp
View File

@ -81,6 +81,11 @@ namespace storm {
}
#endif
template<typename ValueType>
bool InternalAdd<DdType::Sylvan, ValueType>::matchesVariableIndex(MTBDD const& node, uint64_t variableIndex, int64_t offset) {
return !mtbdd_isleaf(node) && static_cast<uint64_t>(sylvan_var(node) + offset) == variableIndex;
}
template<typename ValueType>
bool InternalAdd<DdType::Sylvan, ValueType>::operator==(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
return this->sylvanMtbdd == other.sylvanMtbdd;

10
src/storm/storage/dd/sylvan/InternalSylvanAdd.h
View File

@ -612,6 +612,16 @@ namespace storm {
*/
static ValueType getValue(MTBDD const& node);
/*!
* Retrieves whether the topmost variable in the MTBDD is the one with the given index.
*
* @param The top node of the MTBDD.
* @param variableIndex The variable index.
* @param offset An offset that is applied to the index of the top variable in the MTBDD.
* @return True iff the MTBDD's top variable has the given index.
*/
static bool matchesVariableIndex(MTBDD const& node, uint64_t variableIndex, int64_t offset = 0);
private:
/*!
* Recursively builds the ODD from an ADD.

10
src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp
View File

@ -283,7 +283,7 @@ namespace storm {
// If we are at the maximal level, the value to be set is stored as a constant in the DD.
if (currentRowLevel == maxLevel) {
result.set(currentRowOffset, true);
} else if (ddRowVariableIndices[currentRowLevel] < sylvan_var(dd)) {
} else if (bdd_isterminal(dd) || ddRowVariableIndices[currentRowLevel] < sylvan_var(dd)) {
toVectorRec(dd, result, rowOdd.getElseSuccessor(), complement, currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices);
toVectorRec(dd, result, rowOdd.getThenSuccessor(), complement, currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices);
} else {
@ -390,7 +390,7 @@ namespace storm {
if (currentLevel == maxLevel) {
result[currentIndex++] = values[currentOffset];
} else if (ddVariableIndices[currentLevel] < sylvan_var(dd)) {
} else if (bdd_isterminal(dd) || ddVariableIndices[currentLevel] < sylvan_var(dd)) {
// If we skipped a level, we need to enumerate the explicit entries for the case in which the bit is set
// and for the one in which it is not set.
filterExplicitVectorRec(dd, currentLevel + 1, complement, maxLevel, ddVariableIndices, currentOffset, odd.getElseSuccessor(), result, currentIndex, values);
@ -424,7 +424,7 @@ namespace storm {
if (currentLevel == maxLevel) {
result.set(currentIndex++, values.get(currentOffset));
} else if (ddVariableIndices[currentLevel] < sylvan_var(dd)) {
} else if (bdd_isterminal(dd) || ddVariableIndices[currentLevel] < sylvan_var(dd)) {
// If we skipped a level, we need to enumerate the explicit entries for the case in which the bit is set
// and for the one in which it is not set.
filterExplicitVectorRec(dd, currentLevel + 1, complement, maxLevel, ddVariableIndices, currentOffset, odd.getElseSuccessor(), result, currentIndex, values);
@ -527,6 +527,10 @@ namespace storm {
return newNodeVariable;
}
bool InternalBdd<DdType::Sylvan>::matchesVariableIndex(BDD const& node, uint64_t variableIndex, int64_t offset) {
return !sylvan_isconst(node) && static_cast<uint64_t>(sylvan_var(node) + offset) == variableIndex;
}
template InternalAdd<DdType::Sylvan, double> InternalBdd<DdType::Sylvan>::toAdd() const;
template InternalAdd<DdType::Sylvan, uint_fast64_t> InternalBdd<DdType::Sylvan>::toAdd() const;
template InternalAdd<DdType::Sylvan, storm::RationalNumber> InternalBdd<DdType::Sylvan>::toAdd() const;

10
src/storm/storage/dd/sylvan/InternalSylvanBdd.h
View File

@ -374,6 +374,16 @@ namespace storm {
*/
void filterExplicitVector(Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, storm::storage::BitVector const& sourceValues, storm::storage::BitVector& targetValues) const;
/*!
* Retrieves whether the topmost variable in the BDD is the one with the given index.
*
* @param The top node of the BDD.
* @param variableIndex The variable index.
* @param offset An offset that is applied to the index of the top variable in the BDD.
* @return True iff the BDD's top variable has the given index.
*/
static bool matchesVariableIndex(BDD const& node, uint64_t variableIndex, int64_t offset = 0);
friend struct std::hash<storm::dd::InternalBdd<storm::dd::DdType::Sylvan>>;
/*!

Write Preview
Loading…
Cancel
Save