Browse Source

Enabled checking formula nodes that contain an expression in the variable of the program.

Former-commit-id: fba632e7f4
tempestpy_adaptions
dehnert 10 years ago
parent
commit
f0a2db6485
  1. 4
      src/modelchecker/AbstractModelChecker.cpp
  2. 2
      src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp

4
src/modelchecker/AbstractModelChecker.cpp

@ -115,7 +115,9 @@ namespace storm {
} }
std::unique_ptr<CheckResult> AbstractModelChecker::checkAtomicExpressionFormula(storm::logic::AtomicExpressionFormula const& stateFormula) { std::unique_ptr<CheckResult> AbstractModelChecker::checkAtomicExpressionFormula(storm::logic::AtomicExpressionFormula const& stateFormula) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << stateFormula << ".");
std::stringstream stream;
stream << stateFormula.getExpression();
return this->checkAtomicLabelFormula(storm::logic::AtomicLabelFormula(stream.str()));
} }
std::unique_ptr<CheckResult> AbstractModelChecker::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) { std::unique_ptr<CheckResult> AbstractModelChecker::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) {

2
src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp

@ -58,6 +58,8 @@ namespace storm {
} }
} else if (formula.isPropositionalFormula()) { } else if (formula.isPropositionalFormula()) {
return true; return true;
} else {
std::cout << formula << " and type " << typeid(formula).name() << std::endl;
} }
return false; return false;
} }

Loading…
Cancel
Save