From 2fe9a4d994d084c388173fefc50e5620342d5f25 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Tue, 14 Jul 2015 14:31:17 +0000 Subject: [PATCH] More gracefully handle deterministic automata in HOAF2DA If the HOA automaton has multiple edges to the same state, do not throw an error. Additionally, better error reporting. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10300 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/automata/HOAF2DA.java | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/prism/src/automata/HOAF2DA.java b/prism/src/automata/HOAF2DA.java index 130c4c80..cd517b9e 100644 --- a/prism/src/automata/HOAF2DA.java +++ b/prism/src/automata/HOAF2DA.java @@ -546,8 +546,15 @@ public class HOAF2DA implements HOAConsumer { APMonom2APElements it = new APMonom2APElements(aps, monom); while(it.hasNext()) { APElement el = it.next(); - if (da.hasEdge(stateId, el)) { - throw new HOAConsumerException("Not a deterministic automaton, non-determinism detected (state "+stateId+")"); + // check whether this edge already exist + int previousTo = da.getEdgeDestByLabel(stateId, el); + if (previousTo == to) { + // there is already an edge for this label, but the target + // state is the same, so we don't add an additional edge + continue; + } + if (previousTo != -1) { + throw new HOAConsumerException("Not a deterministic automaton, non-determinism detected (state "+stateId+", label = "+el+", to="+to+", previously to "+previousTo+")"); } da.addEdge(stateId, el, to); }