Browse Source

Found a fix for a bug causing the functional tests to segfault at DeterministicModelBisimulationDecomposition.Die.

- By setting the blocks to be not sorted and unique a different constructor is used by the boost container. This prevents the segfault.
|- I can't say exactly why this works nor do I know if the blocks are actually sorted and unique in the sense meant by the underlying container implementation.


Former-commit-id: a1bfbab75a
tempestpy_adaptions
masawei 10 years ago
parent
commit
97936cbd8e
  1. 4
      src/storage/DeterministicModelBisimulationDecomposition.cpp

4
src/storage/DeterministicModelBisimulationDecomposition.cpp

@ -875,7 +875,7 @@ namespace storm {
// Convert the state-value-pairs to states only.
std::function<storm::storage::sparse::state_type (std::pair<storm::storage::sparse::state_type, ValueType> const&)> projection = [] (std::pair<storm::storage::sparse::state_type, ValueType> const& a) -> storm::storage::sparse::state_type { return a.first; };
this->blocks[block.getId()] = block_type(boost::make_transform_iterator(partition.getBegin(block), projection), boost::make_transform_iterator(partition.getEnd(block), projection), true);
this->blocks[block.getId()] = block_type(boost::make_transform_iterator(partition.getBegin(block), projection), boost::make_transform_iterator(partition.getEnd(block), projection), false);
}
// If we are required to build the quotient model, do so now.
@ -1493,4 +1493,4 @@ namespace storm {
template class DeterministicModelBisimulationDecomposition<storm::RationalFunction>;
#endif
}
}
}
Loading…
Cancel
Save