Unify parsing exceptions and hide implementation details (#74)

* unify parsing exceptions and hide implementation details

* add changelog entry

* add missing throws statements

CHANGELOG.md

@@ -26,6 +26,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
   * The `net:automatalib.tooling:automata-build-tools` module has been renamed to `net.automatalib:automata-build-config`.
   * The `Alphabets#toGrowingAlphabetOrThrowException` method has been moved to `Alphabet#asGrowingAlphabetOrThrowException` so that one does not require an `automata-core` dependency for a simple cast.
   * The `Visualization` factory has been moved from the `automata-core` artifact to the `automata-api` artifact. Furthermore, the previous `DummyVP` has been replaced with a `NoopVP` that does not show a swing window anymore when no proper VisualizationProvider is configured but instead logs an error message. This allows us to drop the `java.desktop` (module) dependency for headless setups and only require it in actual visualizers (DOT, JUNG, etc.).
+* The `FormatException` is now a checked exception because we can [reasonably expect clients to recover from this error](https://docs.oracle.com/javase/tutorial/essential/exceptions/runtime.html). Furthermore, all parsing-related code has been aligned to use the `FormatException` instead of leaking implementation details (such as the `ParseException`s generated by JavaCC).
 
 ### Removed
 

api/src/main/java/net/automatalib/exception/FormatException.java

@@ -16,9 +16,10 @@
 package net.automatalib.exception;
 
 /**
- * An exception that may be thrown when encountering an invalid format while de-serializing an automaton model.
+ * An exception that may be thrown when encountering an invalid format while de-serializing entities such as automata
+ * models or formulas.
  */
-public class FormatException extends IllegalArgumentException {
+public class FormatException extends Exception {
 
     public FormatException() {}
 

api/src/main/java/net/automatalib/serialization/ModelDeserializer.java

@@ -47,7 +47,7 @@ public interface ModelDeserializer<M> {
      * @throws FormatException
      *         if the content of the stream was not in the expected format
      */
-    M readModel(InputStream is) throws IOException;
+    M readModel(InputStream is) throws IOException, FormatException;
 
     /**
      * Reads the contents from the given URL and de-serializes it into a model instance.
@@ -62,7 +62,7 @@ public interface ModelDeserializer<M> {
      * @throws FormatException
      *         if the content of the stream was not in the expected format
      */
-    default M readModel(URL url) throws IOException {
+    default M readModel(URL url) throws IOException, FormatException {
         try (InputStream is = IOUtil.asBufferedInputStream(url.openStream())) {
             return readModel(is);
         }
@@ -81,7 +81,7 @@ default M readModel(URL url) throws IOException {
      * @throws FormatException
      *         if the content of the stream was not in the expected format
      */
-    default M readModel(File f) throws IOException {
+    default M readModel(File f) throws IOException, FormatException {
         try (InputStream is = IOUtil.asBufferedInputStream(f)) {
             return readModel(is);
         }
@@ -100,7 +100,7 @@ default M readModel(File f) throws IOException {
      * @throws FormatException
      *         if the content of the stream was not in the expected format
      */
-    default M readModel(byte[] buf) throws IOException {
+    default M readModel(byte[] buf) throws IOException, FormatException {
         try (ByteArrayInputStream is = new ByteArrayInputStream(buf)) {
             return readModel(is);
         }

api/src/main/java/net/automatalib/serialization/automaton/SimpleAutomatonDeserializer.java

@@ -64,7 +64,7 @@ public interface SimpleAutomatonDeserializer<S, I> extends InputModelDeserialize
      *         if the content of the stream was not in the expected format
      */
     <I2> InputModelData<I2, SimpleAutomaton<S, I2>> readModel(InputStream is, Function<I, I2> inputTransformer)
-            throws IOException;
+            throws IOException, FormatException;
 
     /**
      * Reads the contents from the given URL and de-serializes it into a {@link InputModelData} that contains the model
@@ -85,7 +85,7 @@ <I2> InputModelData<I2, SimpleAutomaton<S, I2>> readModel(InputStream is, Functi
      *         if the content of the stream was not in the expected format
      */
     default <I2> InputModelData<I2, SimpleAutomaton<S, I2>> readModel(URL url, Function<I, I2> inputTransformer)
-            throws IOException {
+            throws IOException, FormatException {
         try (InputStream is = IOUtil.asBufferedInputStream(url.openStream())) {
             return readModel(is, inputTransformer);
         }
@@ -110,7 +110,7 @@ default <I2> InputModelData<I2, SimpleAutomaton<S, I2>> readModel(URL url, Funct
      *         if the content of the stream was not in the expected format
      */
     default <I2> InputModelData<I2, SimpleAutomaton<S, I2>> readModel(File f, Function<I, I2> inputTransformer)
-            throws IOException {
+            throws IOException, FormatException {
         try (InputStream is = IOUtil.asBufferedInputStream(f)) {
             return readModel(is, inputTransformer);
         }
@@ -135,14 +135,14 @@ default <I2> InputModelData<I2, SimpleAutomaton<S, I2>> readModel(File f, Functi
      *         if the content of the stream was not in the expected format
      */
     default <I2> InputModelData<I2, SimpleAutomaton<S, I2>> readModel(byte[] buf, Function<I, I2> inputTransformer)
-            throws IOException {
+            throws IOException, FormatException {
         try (ByteArrayInputStream is = new ByteArrayInputStream(buf)) {
             return readModel(is, inputTransformer);
         }
     }
 
     @Override
-    default InputModelData<I, SimpleAutomaton<S, I>> readModel(InputStream is) throws IOException {
+    default InputModelData<I, SimpleAutomaton<S, I>> readModel(InputStream is) throws IOException, FormatException {
         return readModel(is, Function.identity());
     }
 }

examples/src/main/java/net/automatalib/example/modelchecking/M3CSPAExample.java

@@ -19,10 +19,10 @@
 
 import net.automatalib.automaton.procedural.SPA;
 import net.automatalib.example.procedural.PalindromeExample;
+import net.automatalib.exception.FormatException;
 import net.automatalib.graph.ContextFreeModalProcessSystem;
 import net.automatalib.modelchecker.m3c.formula.FormulaNode;
 import net.automatalib.modelchecker.m3c.formula.parser.M3CParser;
-import net.automatalib.modelchecker.m3c.formula.parser.ParseException;
 import net.automatalib.modelchecker.m3c.solver.M3CSolver;
 import net.automatalib.modelchecker.m3c.solver.M3CSolver.TypedM3CSolver;
 import net.automatalib.modelchecker.m3c.solver.M3CSolvers;
@@ -43,7 +43,7 @@ private M3CSPAExample() {
         // prevent initialization
     }
 
-    public static void main(String[] args) throws ParseException {
+    public static void main(String[] args) throws FormatException {
         final SPA<?, Character> spa = PalindromeExample.buildSPA();
         final ContextFreeModalProcessSystem<Character, Void> view = SPAs.toCFMPS(spa);
 

examples/src/test/java/net/automatalib/example/ExamplesTest.java

@@ -37,9 +37,9 @@
 import net.automatalib.example.modelchecking.M3CSPAExample;
 import net.automatalib.example.procedural.PalindromeExample;
 import net.automatalib.example.vpa.OneSEVPAExample;
+import net.automatalib.exception.FormatException;
 import net.automatalib.modelchecker.ltsmin.LTSminUtil;
 import net.automatalib.modelchecker.ltsmin.LTSminVersion;
-import net.automatalib.modelchecker.m3c.formula.parser.ParseException;
 import org.testng.SkipException;
 import org.testng.annotations.BeforeClass;
 import org.testng.annotations.Test;
@@ -133,7 +133,7 @@ public void testM3CSPAExample() throws InterruptedException, InvocationTargetExc
         SwingUtilities.invokeAndWait(() -> {
             try {
                 M3CSPAExample.main(new String[0]);
-            } catch (ParseException e) {
+            } catch (FormatException e) {
                 throw new RuntimeException(e);
             }
         });

modelchecking/ltsmin/src/main/java/net/automatalib/modelchecker/ltsmin/AbstractLTSmin.java

@@ -26,6 +26,7 @@
 import net.automatalib.common.util.IOUtil;
 import net.automatalib.common.util.collection.CollectionUtil;
 import net.automatalib.common.util.process.ProcessUtil;
+import net.automatalib.exception.FormatException;
 import net.automatalib.exception.ModelCheckingException;
 import net.automatalib.modelchecking.ModelChecker;
 import net.automatalib.serialization.etf.writer.AbstractETFWriter;
@@ -123,7 +124,7 @@ protected AbstractLTSmin(boolean keepFiles, Function<String, I> string2Input) {
      * @param formula
      *         the formula to verify
      */
-    protected abstract void verifyFormula(String formula);
+    protected abstract void verifyFormula(String formula) throws FormatException;
 
     @Override
     public boolean isKeepFiles() {
@@ -154,8 +155,8 @@ public Function<String, I> getString2Input() {
 
         try {
             verifyFormula(formula);
-        } catch (IllegalArgumentException iae) {
-            throw new ModelCheckingException(iae);
+        } catch (FormatException fe) {
+            throw new ModelCheckingException(fe);
         }
 
         final File etf;

modelchecking/ltsmin/src/main/java/net/automatalib/modelchecker/ltsmin/LTSminAlternating.java

@@ -22,6 +22,7 @@
 import net.automatalib.alphabet.impl.Alphabets;
 import net.automatalib.automaton.transducer.MealyMachine;
 import net.automatalib.automaton.transducer.impl.CompactMealy;
+import net.automatalib.exception.FormatException;
 import net.automatalib.serialization.etf.writer.Mealy2ETFWriterAlternating;
 import net.automatalib.serialization.fsm.parser.FSM2MealyParserAlternating;
 
@@ -50,7 +51,7 @@ public interface LTSminAlternating<I, O, R> extends LTSminMealy<I, O, R> {
     @Override
     default CompactMealy<I, O> fsm2Mealy(File fsm,
                                          MealyMachine<?, I, ?, O> originalAutomaton,
-                                         Collection<? extends I> inputs) throws IOException {
+                                         Collection<? extends I> inputs) throws IOException, FormatException {
 
         // Here we optionally provide the parse method with the original automaton. So that an implementation can
         // decide whether undefined outputs are allowed in the fsm or not.

modelchecking/ltsmin/src/main/java/net/automatalib/modelchecker/ltsmin/LTSminIO.java

@@ -22,6 +22,7 @@
 import net.automatalib.alphabet.impl.Alphabets;
 import net.automatalib.automaton.transducer.MealyMachine;
 import net.automatalib.automaton.transducer.impl.CompactMealy;
+import net.automatalib.exception.FormatException;
 import net.automatalib.serialization.etf.writer.Mealy2ETFWriterIO;
 import net.automatalib.serialization.fsm.parser.FSM2MealyParserIO;
 
@@ -43,7 +44,7 @@ public interface LTSminIO<I, O, R> extends LTSminMealy<I, O, R> {
     @Override
     default CompactMealy<I, O> fsm2Mealy(File fsm,
                                          MealyMachine<?, I, ?, O> originalAutomaton,
-                                         Collection<? extends I> inputs) throws IOException {
+                                         Collection<? extends I> inputs) throws IOException, FormatException {
         return FSM2MealyParserIO.getParser(inputs, getString2Input(), getString2Output()).readModel(fsm);
     }
 

modelchecking/ltsmin/src/main/java/net/automatalib/modelchecker/ltsmin/LTSminLTLParser.java

@@ -19,6 +19,7 @@
 
 import net.automatalib.automaton.fsa.DFA;
 import net.automatalib.automaton.transducer.MealyMachine;
+import net.automatalib.exception.FormatException;
 import net.automatalib.serialization.etf.writer.DFA2ETFWriter;
 import net.automatalib.serialization.etf.writer.Mealy2ETFWriterAlternating;
 import net.automatalib.serialization.etf.writer.Mealy2ETFWriterIO;
@@ -53,18 +54,18 @@ private LTSminLTLParser() {}
      *
      * @return {@code formula}
      *
-     * @throws IllegalArgumentException
+     * @throws FormatException
      *         if the formula does not adhere to LTSmin's expected format ('letter' flavor)
      * @see DFA2ETFWriter
      * @see Mealy2ETFWriterAlternating
      */
-    public static String requireValidLetterFormula(String formula) {
+    public static String requireValidLetterFormula(String formula) throws FormatException {
         final InternalLTSminLTLParser parser = new InternalLTSminLTLParser(new StringReader(formula));
 
         try {
             parser.letterFormula();
         } catch (ParseException | TokenMgrError e) {
-            throw new IllegalArgumentException("Given formula does not adhere to expected format", e);
+            throw new FormatException("Given formula does not adhere to expected format", e);
         }
 
         return formula;
@@ -85,8 +86,8 @@ public static String requireValidLetterFormula(String formula) {
     public static boolean isValidLetterFormula(String formula) {
         try {
             requireValidLetterFormula(formula);
-        } catch (IllegalArgumentException iae) {
-            LOGGER.debug("Couldn't parse formula", iae);
+        } catch (FormatException fe) {
+            LOGGER.debug("Couldn't parse formula", fe);
             return false;
         }
 
@@ -101,17 +102,17 @@ public static boolean isValidLetterFormula(String formula) {
      *
      * @return {@code formula}
      *
-     * @throws IllegalArgumentException
+     * @throws FormatException
      *         if the formula does not adhere to LTSmin's expected format ('io' flavor)
      * @see Mealy2ETFWriterIO
      */
-    public static String requireValidIOFormula(String formula) {
+    public static String requireValidIOFormula(String formula) throws FormatException {
         final InternalLTSminLTLParser parser = new InternalLTSminLTLParser(new StringReader(formula));
 
         try {
             parser.ioFormula();
         } catch (ParseException | TokenMgrError e) {
-            throw new IllegalArgumentException("Given formula does not adhere to expected format", e);
+            throw new FormatException("Given formula does not adhere to expected format", e);
         }
 
         return formula;
@@ -130,8 +131,8 @@ public static String requireValidIOFormula(String formula) {
     public static boolean isValidIOFormula(String formula) {
         try {
             requireValidIOFormula(formula);
-        } catch (IllegalArgumentException iae) {
-            LOGGER.debug("Couldn't parse formula", iae);
+        } catch (FormatException fe) {
+            LOGGER.debug("Couldn't parse formula", fe);
             return false;
         }
 

modelchecking/ltsmin/src/main/java/net/automatalib/modelchecker/ltsmin/LTSminMealy.java

@@ -24,8 +24,8 @@
 import net.automatalib.alphabet.impl.Alphabets;
 import net.automatalib.automaton.transducer.MealyMachine;
 import net.automatalib.automaton.transducer.impl.CompactMealy;
+import net.automatalib.exception.FormatException;
 import net.automatalib.modelchecking.ModelChecker;
-import net.automatalib.serialization.fsm.parser.FSMFormatException;
 import net.automatalib.util.automaton.transducer.MealyFilter;
 
 /**
@@ -57,11 +57,11 @@ public interface LTSminMealy<I, O, R>
      *
      * @throws IOException
      *         when {@code fsm} can not be read.
-     * @throws FSMFormatException
+     * @throws FormatException
      *         when {@code fsm} is invalid.
      */
     CompactMealy<I, O> fsm2Mealy(File fsm, MealyMachine<?, I, ?, O> originalAutomaton, Collection<? extends I> inputs)
-            throws IOException;
+            throws IOException, FormatException;
 
     /**
      * Writes the given {@link MealyMachine} to the {@code etf} file.

modelchecking/ltsmin/src/main/java/net/automatalib/modelchecker/ltsmin/ltl/AbstractLTSminLTLMealy.java

@@ -22,13 +22,13 @@
 
 import net.automatalib.automaton.transducer.MealyMachine;
 import net.automatalib.automaton.transducer.impl.CompactMealy;
+import net.automatalib.exception.FormatException;
 import net.automatalib.exception.ModelCheckingException;
 import net.automatalib.modelchecker.ltsmin.LTSminLTLParser;
 import net.automatalib.modelchecker.ltsmin.LTSminMealy;
 import net.automatalib.modelchecking.Lasso.MealyLasso;
 import net.automatalib.modelchecking.ModelCheckerLasso.MealyModelCheckerLasso;
 import net.automatalib.modelchecking.impl.MealyLassoImpl;
-import net.automatalib.serialization.fsm.parser.FSMFormatException;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
@@ -108,7 +108,7 @@ public void setSkipOutputs(Collection<? super O> skipOutputs) {
     }
 
     @Override
-    protected void verifyFormula(String formula) {
+    protected void verifyFormula(String formula) throws FormatException {
         LTSminLTLParser.requireValidIOFormula(formula);
     }
 
@@ -126,7 +126,7 @@ protected void verifyFormula(String formula) {
             final CompactMealy<I, O> mealy = fsm2Mealy(fsm, automaton, inputs);
 
             return new MealyLassoImpl<>(mealy, inputs, computeUnfolds(automaton.size()));
-        } catch (IOException | FSMFormatException e) {
+        } catch (IOException | FormatException e) {
             throw new ModelCheckingException(e);
         } finally {
             // check if we must keep the FSM

modelchecking/ltsmin/src/main/java/net/automatalib/modelchecker/ltsmin/ltl/LTSminLTLAlternating.java

@@ -19,6 +19,7 @@
 import java.util.function.Function;
 
 import de.learnlib.tooling.annotation.builder.GenerateBuilder;
+import net.automatalib.exception.FormatException;
 import net.automatalib.modelchecker.ltsmin.LTSminAlternating;
 import net.automatalib.modelchecker.ltsmin.LTSminLTLParser;
 import net.automatalib.modelchecking.Lasso.MealyLasso;
@@ -53,7 +54,7 @@ public boolean requiresOriginalAutomaton() {
     }
 
     @Override
-    protected void verifyFormula(String formula) {
+    protected void verifyFormula(String formula) throws FormatException {
         LTSminLTLParser.requireValidLetterFormula(formula);
     }
 }

modelchecking/ltsmin/src/main/java/net/automatalib/modelchecker/ltsmin/ltl/LTSminLTLDFA.java

@@ -23,14 +23,14 @@
 import de.learnlib.tooling.annotation.builder.GenerateBuilder;
 import net.automatalib.automaton.fsa.DFA;
 import net.automatalib.automaton.fsa.impl.CompactDFA;
+import net.automatalib.exception.FormatException;
 import net.automatalib.exception.ModelCheckingException;
 import net.automatalib.modelchecker.ltsmin.LTSminDFA;
 import net.automatalib.modelchecker.ltsmin.LTSminLTLParser;
 import net.automatalib.modelchecking.Lasso.DFALasso;
 import net.automatalib.modelchecking.ModelCheckerLasso.DFAModelCheckerLasso;
 import net.automatalib.modelchecking.impl.DFALassoImpl;
 import net.automatalib.serialization.fsm.parser.FSM2DFAParser;
-import net.automatalib.serialization.fsm.parser.FSMFormatException;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
@@ -62,7 +62,7 @@ public LTSminLTLDFA(boolean keepFiles, Function<String, I> string2Input, int min
     }
 
     @Override
-    protected void verifyFormula(String formula) {
+    protected void verifyFormula(String formula) throws FormatException {
         LTSminLTLParser.requireValidLetterFormula(formula);
     }
 
@@ -87,7 +87,7 @@ protected void verifyFormula(String formula) {
                     FSM2DFAParser.getParser(inputs, getString2Input(), LABEL_NAME, LABEL_VALUE).readModel(fsm);
 
             return new DFALassoImpl<>(dfa, inputs, computeUnfolds(automaton.size()));
-        } catch (IOException | FSMFormatException e) {
+        } catch (IOException | FormatException e) {
             throw new ModelCheckingException(e);
         } finally {
             // check if we must keep the FSM