From e8003769cad61f6e9e21e4d1b895b537408424f5 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 11 Apr 2019 15:12:11 +0200 Subject: [PATCH] JaniParser: Better error messages for property parsing. --- src/storm-parsers/parser/JaniParser.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index 1864be23d..2a467a27a 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/src/storm-parsers/parser/JaniParser.cpp @@ -322,7 +322,7 @@ namespace storm { } else if (opString == "∀" || opString == "∃") { assert(bound == boost::none); - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Forall and Exists are currently not supported"); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Forall and Exists are currently not supported in " << scope.description); } else if (opString == "Emin" || opString == "Emax") { STORM_LOG_WARN_COND(model.getJaniVersion() == 1, "Model not compliant: Contains Emin/Emax property in " << scope.description << "."); STORM_LOG_THROW(propertyStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting reward-expression for operator " << opString << " in " << scope.description); @@ -558,7 +558,7 @@ namespace storm { ct = storm::logic::ComparisonType::Less; } } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Comparison operators '=' or '≠' in property specifications are currently not supported."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Comparison operators '=' or '≠' in property specifications are currently not supported in " << scope.description << "."); } } return parseFormula(model, propertyStructure.at(leftRight[i]), formulaContext, scope, storm::logic::Bound(ct, boundExpr));