From 6d0f1ef8a09cbb8b5330dfd86b1f79209c64a0b3 Mon Sep 17 00:00:00 2001 From: schillic Date: Thu, 29 Jun 2017 19:00:18 +0200 Subject: [PATCH] #182 - use IsFinite check; log effective automaton enhancement --- .../ErrorAutomatonStatisticsDefinitions.java | 4 +- .../ErrorAutomatonStatisticsGenerator.java | 76 ++++++++++++++----- .../ErrorGeneralizationEngine.java | 27 ++++++- .../errorabstraction/ErrorTraceContainer.java | 14 ++++ 4 files changed, 98 insertions(+), 23 deletions(-) diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/errorabstraction/ErrorAutomatonStatisticsDefinitions.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/errorabstraction/ErrorAutomatonStatisticsDefinitions.java index 5cf8793c108..a20e66f92c8 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/errorabstraction/ErrorAutomatonStatisticsDefinitions.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/errorabstraction/ErrorAutomatonStatisticsDefinitions.java @@ -40,7 +40,9 @@ public enum ErrorAutomatonStatisticsDefinitions implements IStatisticsElement { ErrorAutomatonConstructionTimeTotal(Long.class, AStatisticsType.sLongAddition, AStatisticsType.sTimeBeforeKey), ErrorAutomatonDifferenceTimeAvg(Long.class, AStatisticsType.sLongAddition, AStatisticsType.sTimeBeforeKey), ErrorAutomatonDifferenceTimeTotal(Long.class, AStatisticsType.sLongAddition, AStatisticsType.sTimeBeforeKey), - AcceptsSingleTrace(Boolean.class, AStatisticsType.sIntegerAddition, AStatisticsType.sKeyBeforeData); + NumberOfNoEnhancement(Integer.class, AStatisticsType.sIntegerAddition, AStatisticsType.sKeyBeforeData), + NumberOfFiniteEnhancement(Integer.class, AStatisticsType.sIntegerAddition, AStatisticsType.sKeyBeforeData), + NumberOfInfiniteEnhancement(Integer.class, AStatisticsType.sIntegerAddition, AStatisticsType.sKeyBeforeData); private final Class mClazz; private final Function> mAggr; diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/errorabstraction/ErrorAutomatonStatisticsGenerator.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/errorabstraction/ErrorAutomatonStatisticsGenerator.java index 43aafbdeee5..043a8097bd8 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/errorabstraction/ErrorAutomatonStatisticsGenerator.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/errorabstraction/ErrorAutomatonStatisticsGenerator.java @@ -48,6 +48,7 @@ import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.Difference; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.Intersect; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.IsEmpty; +import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.IsFinite; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.PowersetDeterminizer; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.RemoveDeadEnds; import de.uni_freiburg.informatik.ultimate.automata.nestedword.operations.RemoveUnreachable; @@ -76,6 +77,26 @@ * @author Christian Schilling (schillic@informatik.uni-freiburg.de) */ public class ErrorAutomatonStatisticsGenerator implements IStatisticsDataProvider { + /** + * Type of enhancement over the {@code StraightLineInterpolantAutomatonBuilder} result. + * + * @author Christian Schilling (schillic@informatik.uni-freiburg.de) + */ + public enum EnhancementType { + /** + * No enhancement, just the straight-line automaton. + */ + NONE, + /** + * Enhancement, but language is finite. + */ + FINITE, + /** + * Enhancement, language is infinite. + */ + INFINITE + } + private static final String ERROR_AUTOMATON_CONSTRUCTION_TIME = "ErrorAutomatonConstructionTime"; private static final String ERROR_AUTOMATON_DIFFERENCE_TIME = "ErrorAutomatonDifferenceTime"; private final Benchmark mBenchmark; @@ -83,7 +104,7 @@ public class ErrorAutomatonStatisticsGenerator implements IStatisticsDataProvide private boolean mRunningDifference = false; private int mTraceLength = -1; private final List mAutomatonStatistics = new LinkedList<>(); - private Boolean mAcceptsSingleTrace; + private EnhancementType mEnhancement; public ErrorAutomatonStatisticsGenerator() { mBenchmark = new Benchmark(); @@ -126,17 +147,14 @@ public > void evaluateFinalErrorAutomaton(fina final PredicateFactoryResultChecking predicateFactoryResultChecking, final IRun errorTrace) throws AutomataLibraryException { final NestedWordAutomaton subtrahend; - String automatonType; final AutomataLibraryServices alServices = new AutomataLibraryServices(services); switch (errorAutomatonBuilder.getType()) { case ERROR_AUTOMATON: subtrahend = errorAutomatonBuilder.getResultBeforeEnhancement(); - automatonType = "error"; break; case DANGER_AUTOMATON: subtrahend = constructStraightLineAutomaton(services, errorTrace, new VpAlphabet<>(abstraction), predicateFactory); - automatonType = "danger"; break; default: throw new IllegalArgumentException("Unknown error automaton type: " + errorAutomatonBuilder.getType()); @@ -154,28 +172,42 @@ public > void evaluateFinalErrorAutomaton(fina new PowersetDeterminizer<>(subtrahend, true, predicateFactory); final IDoubleDeckerAutomaton diff = new Difference<>(alServices, predicateFactoryResultChecking, effectiveErrorAutomaton, subtrahend, psd, false).getResult(); - mAcceptsSingleTrace = new IsEmpty<>(alServices, diff).getResult(); - if (mAcceptsSingleTrace) { - logger.warn("Enhancement did not add additional traces."); + if (new IsEmpty<>(alServices, diff).getResult()) { + mEnhancement = EnhancementType.NONE; + if (logger.isWarnEnabled()) { + logger.warn("Automaton did not add additional traces."); + } + } else if (new IsFinite<>(alServices, effectiveErrorAutomaton).getResult()) { + mEnhancement = EnhancementType.FINITE; + if (logger.isWarnEnabled()) { + logger.warn("Automaton has a finite language."); + } + } else { + mEnhancement = EnhancementType.INFINITE; + if (logger.isInfoEnabled()) { + logger.info("Automaton has an infinite language."); + } } final NestedWordAutomatonReachableStates nwars = new NestedWordAutomatonReachableStates<>(alServices, effectiveErrorAutomaton); nwars.computeAcceptingComponents(); - logger.info("Effective " + automatonType + " automaton size information: " + nwars.sizeInformation()); + if (logger.isInfoEnabled()) { + logger.info("Effective automaton size information: " + nwars.sizeInformation()); + } } public void finishAutomatonInstance() { - if (mRunningConstruction || mRunningDifference || mTraceLength == -1 || mAcceptsSingleTrace == null) { + if (mRunningConstruction || mRunningDifference || mTraceLength == -1 || mEnhancement == null) { throw new IllegalAccessError("Not all statistics data were provided."); } final long constructionTime = getLastConstructionTime(); final long differenceTime = (long) mBenchmark.getElapsedTime(ERROR_AUTOMATON_DIFFERENCE_TIME, TimeUnit.NANOSECONDS); final int traceLength = mTraceLength; - final boolean acceptsSingleTrace = mAcceptsSingleTrace; + final EnhancementType enhancement = mEnhancement; mTraceLength = -1; mAutomatonStatistics - .add(new AutomatonStatisticsEntry(constructionTime, differenceTime, traceLength, acceptsSingleTrace)); + .add(new AutomatonStatisticsEntry(constructionTime, differenceTime, traceLength, enhancement)); } /** @@ -192,6 +224,10 @@ public Object getTotalNumber() { return mAutomatonStatistics.size(); } + public EnhancementType getEnhancement() { + return mEnhancement; + } + @Override public Collection getKeys() { return ErrorAutomatonStatisticsType.getInstance().getKeys(); @@ -214,8 +250,12 @@ public Object getValue(final String key) { return getAverageErrorAutomatonConstructionTime(stats -> stats.mDifferenceTime); case ErrorAutomatonDifferenceTimeTotal: return getTotalErrorAutomatonConstructionTime(stats -> stats.mDifferenceTime); - case AcceptsSingleTrace: - return getTotalNumberOfSingleTraceAcceptance(); + case NumberOfNoEnhancement: + return getNumberOfGivenEnhancementType(EnhancementType.NONE); + case NumberOfFiniteEnhancement: + return getNumberOfGivenEnhancementType(EnhancementType.FINITE); + case NumberOfInfiniteEnhancement: + return getNumberOfGivenEnhancementType(EnhancementType.INFINITE); default: throw new AssertionError("Unknown key: " + key); } @@ -238,10 +278,10 @@ private int getAverageTraceLength() { return result / total; } - private Object getTotalNumberOfSingleTraceAcceptance() { + private Object getNumberOfGivenEnhancementType(final EnhancementType enhancementType) { int result = 0; for (final AutomatonStatisticsEntry stats : mAutomatonStatistics) { - if (stats.mAcceptsSingleTrace) { + if (stats.mEnhancement == enhancementType) { ++result; } } @@ -352,14 +392,14 @@ private static class AutomatonStatisticsEntry { private final long mConstructionTime; private final int mTraceLength; private final long mDifferenceTime; - private final boolean mAcceptsSingleTrace; + private final EnhancementType mEnhancement; public AutomatonStatisticsEntry(final long constructionTime, final long differenceTime, final int traceLength, - final boolean acceptsSingleTrace) { + final EnhancementType enhancement) { mDifferenceTime = differenceTime; mConstructionTime = constructionTime; mTraceLength = traceLength; - mAcceptsSingleTrace = acceptsSingleTrace; + mEnhancement = enhancement; } } } diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/errorabstraction/ErrorGeneralizationEngine.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/errorabstraction/ErrorGeneralizationEngine.java index 769969fe661..6bd71a4c19f 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/errorabstraction/ErrorGeneralizationEngine.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/errorabstraction/ErrorGeneralizationEngine.java @@ -213,6 +213,7 @@ public void stopDifference(final INestedWordAutomaton abstra (INwaOutgoingLetterAndTransitionProvider) abstraction, predicateFactoryInterpolantAutomata, predicateFactoryResultChecking, errorTrace); mErrorAutomatonStatisticsGenerator.finishAutomatonInstance(); + mErrorTraces.addEnhancementType(mErrorAutomatonStatisticsGenerator.getEnhancement()); } /** @@ -243,12 +244,30 @@ public boolean isResultUnsafe(final Result abstractResult) { + (mErrorTraces.size() == 1 ? " error trace:" : " different error traces in total:")); int ctr = 0; for (final ErrorTrace errorTrace : mErrorTraces) { + final StringBuilder builder = new StringBuilder(); + builder.append(++ctr).append(": Error trace of length ") + .append(errorTrace.getTrace().getWord().length()); + switch (errorTrace.getEnhancement()) { + case NONE: + builder.append(" (no additional traces)"); + break; + case FINITE: + builder.append(" (finite language)"); + break; + case INFINITE: + builder.append(" (infinite language)"); + break; + default: + throw new IllegalArgumentException("Unknown enhancement type: " + errorTrace.getEnhancement()); + } final IPredicate precondition = errorTrace.getPrecondition(); // TODO 2017-06-14 Christian: Do not print error precondition on info level after testing phase. - mLogger.info(++ctr + ": Error trace of length " + errorTrace.getTrace().getWord().length() - + (precondition == null - ? " (precondition not computed)." - : " has precondition " + precondition.getFormula() + '.')); + if (precondition == null) { + builder.append(" (precondition not computed)."); + } else { + builder.append(" has precondition ").append(precondition.getFormula()).append('.'); + } + mLogger.warn(builder.toString()); } } // TODO 2017-06-18 Christian: Currently we want to run the CEGAR loop until the abstraction is empty. diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/errorabstraction/ErrorTraceContainer.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/errorabstraction/ErrorTraceContainer.java index 0b5d9860275..041a2a4cc8c 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/errorabstraction/ErrorTraceContainer.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/errorabstraction/ErrorTraceContainer.java @@ -32,6 +32,7 @@ import de.uni_freiburg.informatik.ultimate.automata.IRun; import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.predicates.IPredicate; +import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.errorabstraction.ErrorAutomatonStatisticsGenerator.EnhancementType; import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.errorabstraction.ErrorTraceContainer.ErrorTrace; /** @@ -72,6 +73,14 @@ public void addPrecondition(final IPredicate precondition) { } } + /** + * TODO remove this and the field after collecting statistics. + * @param enhancement Enhancement type. + */ + public void addEnhancementType(final EnhancementType enhancement) { + mTraces.get(mTraces.size() - 1).mEnhancement = enhancement; + } + /** * @return {@code true} iff there is no error trace. */ @@ -101,6 +110,7 @@ public Iterator> iterator() { public static final class ErrorTrace { private final IRun mTrace; private IPredicate mPrecondition; + public EnhancementType mEnhancement; /** * @param trace @@ -128,5 +138,9 @@ public ErrorTrace(final IRun trace) { public IPredicate getPrecondition() { return mPrecondition; } + + public EnhancementType getEnhancement() { + return mEnhancement; + } } }