Browse Source

Fixed typo leading to wrong variables in SMT encoding

tempestpy_adaptions
Matthias Volk 7 years ago
parent
commit
e99e5bf6bf
  1. 2
      src/storm-dft/modelchecker/dft/DFTASFChecker.cpp

2
src/storm-dft/modelchecker/dft/DFTASFChecker.cpp

@ -505,7 +505,7 @@ namespace storm {
tmpVars.push_back(varNames.size() - 1); tmpVars.push_back(varNames.size() - 1);
tmpTimePointVariables.push_back(varNames.size() - 1); tmpTimePointVariables.push_back(varNames.size() - 1);
// AND over the selected children // AND over the selected children
constraints.push_back(std::make_shared<IsMaximum>(tmpVars.at(i), combinationChildren));
constraints.push_back(std::make_shared<IsMaximum>(timePointVariables.at(i), combinationChildren));
constraints.back()->setDescription("VOT gate " + element->name() + ": AND no. " + std::to_string(i)); constraints.back()->setDescription("VOT gate " + element->name() + ": AND no. " + std::to_string(i));
// Generate next permutation // Generate next permutation
combination = nextBitPermutation(combination); combination = nextBitPermutation(combination);

Loading…
Cancel
Save