Browse Source

Check if derivative is constant in validation of assumption

tempestpy_adaptions
Jip Spel 6 years ago
parent
commit
4999ac5440
  1. 10
      src/storm-pars/analysis/AssumptionChecker.cpp

10
src/storm-pars/analysis/AssumptionChecker.cpp

@ -171,6 +171,7 @@ namespace storm {
typename storm::storage::SparseMatrix<ValueType>::iterator state1succ2, typename storm::storage::SparseMatrix<ValueType>::iterator state1succ2,
typename storm::storage::SparseMatrix<ValueType>::iterator state2succ1, typename storm::storage::SparseMatrix<ValueType>::iterator state2succ1,
typename storm::storage::SparseMatrix<ValueType>::iterator state2succ2) { typename storm::storage::SparseMatrix<ValueType>::iterator state2succ2) {
bool result = true;
ValueType prob; ValueType prob;
auto comp = lattice->compare(state1succ1->getColumn(), state1succ2->getColumn()); auto comp = lattice->compare(state1succ1->getColumn(), state1succ2->getColumn());
@ -183,16 +184,19 @@ namespace storm {
// TODO: Type // TODO: Type
std::map<storm::RationalFunctionVariable, typename ValueType::CoeffType> substitutions; std::map<storm::RationalFunctionVariable, typename ValueType::CoeffType> substitutions;
for (auto var:vars) {
for (auto var : vars) {
auto derivative = prob.derivative(var); auto derivative = prob.derivative(var);
assert(derivative.isConstant());
if(derivative.isConstant()) {
if (derivative.constantPart() >= 0) { if (derivative.constantPart() >= 0) {
substitutions[var] = 0; substitutions[var] = 0;
} else if (derivative.constantPart() <= 0) { } else if (derivative.constantPart() <= 0) {
substitutions[var] = 1; substitutions[var] = 1;
} }
} else {
result = false;
}
} }
return prob.evaluate(substitutions) >= 0;
return result && prob.evaluate(substitutions) >= 0;
} }
template <typename ValueType> template <typename ValueType>

Loading…
Cancel
Save