From bfb416687fdbd23294ee7fb2c6f5c552ec058f29 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 19 Nov 2013 22:33:51 +0100 Subject: [PATCH] Bugfix for Markov automaton parser. Number of choices now gets computed correctly in the presence of deadlock states. Former-commit-id: afd996d4a31a94d3ac292dc272d07cfc0f1ed844 --- .../MarkovAutomatonSparseTransitionParser.cpp | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/parser/MarkovAutomatonSparseTransitionParser.cpp index 52af4c6f2..5838a6fb3 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.cpp +++ b/src/parser/MarkovAutomatonSparseTransitionParser.cpp @@ -8,6 +8,8 @@ namespace storm { MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTransitionParser::firstPass(char* buf, SupportedLineEndingsEnum lineEndings) { MarkovAutomatonSparseTransitionParser::FirstPassResult result; + bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks"); + // Skip the format hint. buf = storm::parser::forwardToNextLine(buf, lineEndings); @@ -28,12 +30,17 @@ namespace storm { // If we have skipped some states, we need to reserve the space for the self-loop insertion in the second pass. if (source > lastsource + 1) { - result.numberOfNonzeroEntries += source - lastsource - 1; - result.numberOfChoices += source - lastsource - 1; - } else { - ++result.numberOfChoices; + if (fixDeadlocks) { + result.numberOfNonzeroEntries += source - lastsource - 1; + result.numberOfChoices += source - lastsource - 1; + } else { + LOG4CPLUS_ERROR(logger, "Found deadlock states (e.g. " << lastsource + 1 << ") during parsing. Please fix them or set the appropriate flag."); + throw storm::exceptions::WrongFormatException() << "Found deadlock states (e.g. " << lastsource + 1 << ") during parsing. Please fix them or set the appropriate flag."; + } } + ++result.numberOfChoices; + // If we have moved to the next state, we need to clear the flag that stores whether or not the source has a Markovian or probabilistic choice. if (source != lastsource) { stateHasMarkovianChoice = false;