From f0a2db648584ee1fb063fc923c430a8fe83d6be2 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 28 Jan 2015 19:07:03 +0100 Subject: [PATCH] Enabled checking formula nodes that contain an expression in the variable of the program. Former-commit-id: fba632e7f4043eceb5240c002c97719a34410869 --- src/modelchecker/AbstractModelChecker.cpp | 4 +++- .../reachability/SparseDtmcEliminationModelChecker.cpp | 2 ++ 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp index 85b62563a..3185298cd 100644 --- a/src/modelchecker/AbstractModelChecker.cpp +++ b/src/modelchecker/AbstractModelChecker.cpp @@ -115,7 +115,9 @@ namespace storm { } std::unique_ptr 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 AbstractModelChecker::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) { diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index c74fc06e4..4ac0cbd16 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -58,6 +58,8 @@ namespace storm { } } else if (formula.isPropositionalFormula()) { return true; + } else { + std::cout << formula << " and type " << typeid(formula).name() << std::endl; } return false; }