From 0e3c380e5e8ab54cb917f50a758d95f087b1d71c Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 13 Jul 2015 14:37:22 +0000 Subject: [PATCH] LTL2DA: Improve error handling. In some cases, errors in LTL2RabinLibrary should be treated as errors (when the formula contains temporal bounds), other times we want to give jltl2dstar / the external LTL2DA tools another try. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10287 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/automata/LTL2DA.java | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/prism/src/automata/LTL2DA.java b/prism/src/automata/LTL2DA.java index c3e57fc2..4daab413 100644 --- a/prism/src/automata/LTL2DA.java +++ b/prism/src/automata/LTL2DA.java @@ -103,8 +103,16 @@ public class LTL2DA extends PrismComponent getLog().println("Taking deterministic Rabin automaton from library..."); } } catch (Exception e) { - getLog().println("Warning: Exception during attempt to construct DRA using the LTL2RabinLibrary:"); - getLog().println(" "+e.getMessage()); + if (containsTemporalBounds) { + // there is (currently) no other way to translate LTL with temporal bounds, + // so treat an exception as a "real" one + throw e; + } else { + // there is the possibility that we might be able to construct + // an automaton below, just issue a warning + getLog().println("Warning: Exception during attempt to construct DRA using the LTL2RabinLibrary:"); + getLog().println(" "+e.getMessage()); + } } }