Skip to content

Commit

Permalink
#182 - use IsFinite check; log effective automaton enhancement
Browse files Browse the repository at this point in the history
  • Loading branch information
@schillic
schillic committed Jun 29, 2017
1 parent f0fb6fc commit 6d0f1ef
Show file tree
Hide file tree
Showing 4 changed files with 98 additions and 23 deletions.
4 changes: 3 additions & 1 deletion ...gins/generator/traceabstraction/errorabstraction/ErrorAutomatonStatisticsDefinitions.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<Object, Function<Object, Object>> mAggr;
Expand Down
76 changes: 58 additions & 18 deletions ...lugins/generator/traceabstraction/errorabstraction/ErrorAutomatonStatisticsGenerator.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -76,14 +77,34 @@
* @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;
private boolean mRunningConstruction = false;
private boolean mRunningDifference = false;
private int mTraceLength = -1;
private final List<AutomatonStatisticsEntry> mAutomatonStatistics = new LinkedList<>();
private Boolean mAcceptsSingleTrace;
private EnhancementType mEnhancement;

public ErrorAutomatonStatisticsGenerator() {
mBenchmark = new Benchmark();
Expand Down Expand Up @@ -126,17 +147,14 @@ public <LETTER extends IIcfgTransition<?>> void evaluateFinalErrorAutomaton(fina
final PredicateFactoryResultChecking predicateFactoryResultChecking,
final IRun<LETTER, IPredicate, ?> errorTrace) throws AutomataLibraryException {
final NestedWordAutomaton<LETTER, IPredicate> 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());
Expand All @@ -154,28 +172,42 @@ public <LETTER extends IIcfgTransition<?>> void evaluateFinalErrorAutomaton(fina
new PowersetDeterminizer<>(subtrahend, true, predicateFactory);
final IDoubleDeckerAutomaton<LETTER, IPredicate> 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<LETTER, IPredicate> 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));
}

/**
Expand All @@ -192,6 +224,10 @@ public Object getTotalNumber() {
return mAutomatonStatistics.size();
}

public EnhancementType getEnhancement() {
return mEnhancement;
}

@Override
public Collection<String> getKeys() {
return ErrorAutomatonStatisticsType.getInstance().getKeys();
Expand All @@ -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);
}
Expand All @@ -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;
}
}
Expand Down Expand Up @@ -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;
}
}
}
27 changes: 23 additions & 4 deletions ...timate/plugins/generator/traceabstraction/errorabstraction/ErrorGeneralizationEngine.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -213,6 +213,7 @@ public void stopDifference(final INestedWordAutomaton<LETTER, IPredicate> abstra
(INwaOutgoingLetterAndTransitionProvider<LETTER, IPredicate>) abstraction,
predicateFactoryInterpolantAutomata, predicateFactoryResultChecking, errorTrace);
mErrorAutomatonStatisticsGenerator.finishAutomatonInstance();
mErrorTraces.addEnhancementType(mErrorAutomatonStatisticsGenerator.getEnhancement());
}

/**
Expand Down Expand Up @@ -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<LETTER> 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.
Expand Down
14 changes: 14 additions & 0 deletions ...tik/ultimate/plugins/generator/traceabstraction/errorabstraction/ErrorTraceContainer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;

/**
Expand Down Expand Up @@ -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.
*/
Expand Down Expand Up @@ -101,6 +110,7 @@ public Iterator<ErrorTrace<LETTER>> iterator() {
public static final class ErrorTrace<LETTER> {
private final IRun<LETTER, IPredicate, ?> mTrace;
private IPredicate mPrecondition;
public EnhancementType mEnhancement;

/**
* @param trace
Expand Down Expand Up @@ -128,5 +138,9 @@ public ErrorTrace(final IRun<LETTER, IPredicate, ?> trace) {
public IPredicate getPrecondition() {
return mPrecondition;
}

public EnhancementType getEnhancement() {
return mEnhancement;
}
}
}

0 comments on commit 6d0f1ef

Please sign in to comment.