From 00db8794e6ea2e3c04b6f9430bbf4ef3bfaaa44f Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 22 Oct 2016 17:11:41 +0900 Subject: [PATCH] fixed bug in explicit jani model generator Former-commit-id: 445ee6a4ba17d2360d6d7c6b0833e7694e1c02b2 [formerly 702d0fb0de3dfdc024b8f6b50867c22504cbc98e] Former-commit-id: 0fb52d40d49233b78c5498e4c2d2972230f37857 --- src/generator/JaniNextStateGenerator.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index b2c786b77..80473c2f9 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -486,6 +486,8 @@ namespace storm { currentTargetStates = newTargetStates; newTargetStates = new boost::container::flat_map(); } + + ++locationVariableIt; } // At this point, we applied all commands of the current command combination and newTargetStates @@ -541,7 +543,6 @@ namespace storm { // Iterate over all automata. uint64_t automatonIndex = 0; for (auto const& automaton : model.getAutomata()) { - // If the automaton has no edge labeled with the given action, we can skip it. if (!automaton.hasEdgeLabeledWithActionIndex(actionIndex)) { continue;