Browse Source

slight fix to bit vector sizes used in explicit model builder

tempestpy_adaptions
dehnert 6 years ago
parent
commit
7af70a77aa
  1. 2
      src/storm/generator/JaniNextStateGenerator.cpp
  2. 2
      src/storm/generator/PrismNextStateGenerator.cpp

2
src/storm/generator/JaniNextStateGenerator.cpp

@ -185,7 +185,7 @@ namespace storm {
std::vector<StateType> initialStateIndices;
while (solver->check() == storm::solver::SmtSolver::CheckResult::Sat) {
// Create fresh state.
CompressedState initialState(this->variableInformation.getTotalBitOffset());
CompressedState initialState(this->variableInformation.getTotalBitOffset(true));
// Read variable assignment from the solution of the solver. Also, create an expression we can use to
// prevent the variable assignment from being enumerated again.

2
src/storm/generator/PrismNextStateGenerator.cpp

@ -150,7 +150,7 @@ namespace storm {
std::vector<StateType> initialStateIndices;
while (solver->check() == storm::solver::SmtSolver::CheckResult::Sat) {
// Create fresh state.
CompressedState initialState(this->variableInformation.getTotalBitOffset());
CompressedState initialState(this->variableInformation.getTotalBitOffset(true));
// Read variable assignment from the solution of the solver. Also, create an expression we can use to
// prevent the variable assignment from being enumerated again.
Loading…
Cancel
Save