Skip to content

Commit

Permalink
see #109 -- added additional debug logging
Browse files Browse the repository at this point in the history
  • Loading branch information
@danieldietsch
danieldietsch committed Mar 21, 2017
1 parent 40b1d6c commit 27d561c
Show file tree
Hide file tree
Showing 3 changed files with 87 additions and 36 deletions.
1 change: 1 addition & 0 deletions ...formatik/ultimate/plugins/analysis/abstractinterpretationv2/algorithm/FixpointEngine.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -105,6 +105,7 @@ public AbstractInterpretationResult<STATE, ACTION, VARDECL, LOC> run(final Colle
calculateFixpoint(start);
mResult.saveRootStorage(mStateStorage);
mResult.saveSummaryStorage(mSummaryMap);
mLogger.debug("Fixpoint computation completed");
return mResult;
}

Expand Down
31 changes: 25 additions & 6 deletions ...e/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/BasicCegarLoop.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@
import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryException;
import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices;
import de.uni_freiburg.informatik.ultimate.automata.AutomataOperationCanceledException;
import de.uni_freiburg.informatik.ultimate.automata.IRun;
import de.uni_freiburg.informatik.ultimate.automata.Word;
import de.uni_freiburg.informatik.ultimate.automata.nestedword.IDoubleDeckerAutomaton;
import de.uni_freiburg.informatik.ultimate.automata.nestedword.INestedWordAutomaton;
Expand Down Expand Up @@ -282,8 +283,8 @@ protected boolean isAbstractionCorrect() throws AutomataOperationCanceledExcepti
@Override
protected LBool isCounterexampleFeasible() throws AutomataOperationCanceledException {

final IRefinementStrategy<LETTER> strategy = mRefinementStrategyFactory.createStrategy(mPref.getRefinementStrategy(), mCounterexample,
mAbstraction, getIteration(), getCegarLoopBenchmark());
final IRefinementStrategy<LETTER> strategy = mRefinementStrategyFactory.createStrategy(
mPref.getRefinementStrategy(), mCounterexample, mAbstraction, getIteration(), getCegarLoopBenchmark());
try {
mTraceCheckAndRefinementEngine = new TraceAbstractionRefinementEngine<>(mLogger, strategy);
} catch (final ToolchainCanceledException tce) {
Expand Down Expand Up @@ -320,10 +321,10 @@ protected LBool isCounterexampleFeasible() throws AutomataOperationCanceledExcep
mRcfgProgramExecution = mRcfgProgramExecution.addRelevanceInformation(a.getRelevanceInformation());
}
} else {
if (DUMP_DIFFICULT_PATH_PROGRAMS
&& !((TraceAbstractionRefinementEngine) mTraceCheckAndRefinementEngine).somePerfectSequenceFound()) {
final String filename = mPref.dumpPath() + File.separator + mIcfgContainer.getIdentifier() + "_"
+ mIteration + ".bpl";
if (DUMP_DIFFICULT_PATH_PROGRAMS && !((TraceAbstractionRefinementEngine) mTraceCheckAndRefinementEngine)
.somePerfectSequenceFound()) {
final String filename =
mPref.dumpPath() + File.separator + mIcfgContainer.getIdentifier() + "_" + mIteration + ".bpl";
new PathProgramDumper(mIcfgContainer, mServices,
(NestedRun<? extends IAction, IPredicate>) mCounterexample, filename);
}
Expand Down Expand Up @@ -424,6 +425,7 @@ private boolean refineWithGivenAutomaton(final NestedWordAutomaton<LETTER, IPred

if (!new Accepts<>(new AutomataLibraryServices(mServices), interpolantAutomaton,
(NestedWord<LETTER>) mCounterexample.getWord(), true, false).getResult()) {
debugLogBrokenInterpolantAutomaton(inputInterpolantAutomaton, interpolantAutomaton, mCounterexample);
throw new AssertionError("enhanced interpolant automaton in iteration " + mIteration
+ " broken: counterexample of length " + mCounterexample.getLength() + " not accepted");
}
Expand Down Expand Up @@ -484,6 +486,23 @@ private boolean refineWithGivenAutomaton(final NestedWordAutomaton<LETTER, IPred
return !stillAccepted;
}

private void debugLogBrokenInterpolantAutomaton(
final INestedWordAutomatonSimple<LETTER, IPredicate> interpolantAutomaton,
final INestedWordAutomatonSimple<LETTER, IPredicate> enhancedInterpolantAutomaton,
final IRun<LETTER, IPredicate, ?> counterexample) {
mLogger.fatal("--");
mLogger.fatal("enhanced interpolant automaton broken: counterexample not accepted");
mLogger.fatal("word:");
for (final LETTER letter : counterexample.getWord()) {
mLogger.fatal(letter);
}
mLogger.fatal("original automaton:");
mLogger.fatal(interpolantAutomaton);
mLogger.fatal("enhanced automaton:");
mLogger.fatal(enhancedInterpolantAutomaton);
mLogger.fatal("--");
}

private INestedWordAutomatonSimple<LETTER, IPredicate> constructInterpolantAutomatonForOnDemandEnhancement(
final NestedWordAutomaton<LETTER, IPredicate> inputInterpolantAutomaton,
final IPredicateUnifier predicateUnifier, final IHoareTripleChecker htc,
Expand Down
91 changes: 61 additions & 30 deletions ...atik/ultimate/plugins/generator/traceabstraction/predicates/AbsIntHoareTripleChecker.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -147,19 +147,60 @@ public HoareTripleCheckerStatisticsGenerator getEdgeCheckerBenchmark() {
private Validity checkNonReturnTransition(final AbstractMultiState<STATE, ACTION, VARDECL> pre, final ACTION act,
final AbstractMultiState<STATE, ACTION, VARDECL> succ) {
final AbstractMultiState<STATE, ACTION, VARDECL> preState = createValidPostOpStateAfterLeaving(act, pre, null);
final Validity result = checkNonReturnTransitionNoLogging(preState, act, succ);
if (mLogger.isDebugEnabled()) {
logDebugIfNotEqual(pre, preState, "Modified preState");
mLogger.debug("Pre : " + preState.toLogString());
mLogger.debug("Act : " + act);
mLogger.debug("Post: " + succ.toLogString());
}

final Validity result = checkNonReturnTransitionWithValidState(preState, act, succ);
if (mLogger.isDebugEnabled()) {
mLogger.debug("Result: " + result);
mLogger.debug("--");
}
assert assertValidity(preState, null, act, succ, result) : MSG_INVALID_HOARE_TRIPLE_CHECK;
return result;
}

private Validity checkNonReturnTransitionWithValidState(final AbstractMultiState<STATE, ACTION, VARDECL> preState,
final ACTION act, final AbstractMultiState<STATE, ACTION, VARDECL> postState) {
if (preState.isBottom()) {
return Validity.VALID;
}

final AbstractMultiState<STATE, ACTION, VARDECL> calculatedPost = preState.apply(mPostOp, act);
if (mLogger.isDebugEnabled()) {
mLogger.debug("Calculated post: " + calculatedPost.toLogString());
}
if (calculatedPost.isBottom() && postState.isBottom()) {
return trackPost(Validity.VALID, act);
}

final AbstractMultiState<STATE, ACTION, VARDECL> synchronizedCalculatedPost =
synchronizeState(postState, calculatedPost);
if (mLogger.isDebugEnabled()) {
mLogger.debug("Synchronized calculated post: " + synchronizedCalculatedPost.toLogString());
}
assert postState.getVariables()
.equals(synchronizedCalculatedPost.getVariables()) : MSG_TRACKED_VARIABLES_DIFFER;
final SubsetResult included = synchronizedCalculatedPost.isSubsetOf(postState);
if (mLogger.isDebugEnabled()) {
mLogger.debug("Inclusion (NO): " + included);
}
if (included != SubsetResult.NONE) {
return trackPost(Validity.VALID, act);
}
final SubsetResult excluded = postState.isSubsetOf(synchronizedCalculatedPost);
if (mLogger.isDebugEnabled()) {
mLogger.debug("Exclusion (ON): " + excluded);
}
if (excluded == SubsetResult.NONE) {
return trackPost(Validity.INVALID, act);
}
return Validity.UNKNOWN;
}

private Validity checkReturnTransition(final AbstractMultiState<STATE, ACTION, VARDECL> preLin,
final AbstractMultiState<STATE, ACTION, VARDECL> preHier, final ACTION act,
final AbstractMultiState<STATE, ACTION, VARDECL> succ) {
Expand All @@ -174,7 +215,6 @@ private Validity checkReturnTransition(final AbstractMultiState<STATE, ACTION, V
createValidPostOpStateBeforeLeaving(correspondingCall, preHier);
final AbstractMultiState<STATE, ACTION, VARDECL> stateAfterLeaving =
createValidPostOpStateAfterLeaving(act, validPreLinState, validPreHierState);
final Validity result = checkReturnTransitionNoLogging(validPreLinState, stateAfterLeaving, act, succ);
if (mLogger.isDebugEnabled()) {
logDebugIfNotEqual(preLin, validPreLinState, "Modified preLinState");
logDebugIfNotEqual(preHier, validPreHierState, "Modified preHierState");
Expand All @@ -184,40 +224,19 @@ private Validity checkReturnTransition(final AbstractMultiState<STATE, ACTION, V
mLogger.debug(
"Act : (" + act.getPrecedingProcedure() + ") " + act + " (" + act.getSucceedingProcedure() + ")");
mLogger.debug("Post: " + succ.toLogString());
}

final Validity result = checkReturnTransitionWithValidState(validPreLinState, stateAfterLeaving, act, succ);
if (mLogger.isDebugEnabled()) {
mLogger.debug("Result: " + result);
mLogger.debug("--");
}
assert assertValidity(validPreLinState, stateAfterLeaving, act, succ, result) : MSG_INVALID_HOARE_TRIPLE_CHECK;
return result;
}

private Validity checkNonReturnTransitionNoLogging(final AbstractMultiState<STATE, ACTION, VARDECL> preState,
final ACTION act, final AbstractMultiState<STATE, ACTION, VARDECL> postState) {
if (preState.isBottom()) {
return Validity.VALID;
}

final AbstractMultiState<STATE, ACTION, VARDECL> calculatedPost = preState.apply(mPostOp, act);
if (calculatedPost.isBottom() && postState.isBottom()) {
return trackPost(Validity.VALID, act);
}

final AbstractMultiState<STATE, ACTION, VARDECL> synchronizedCalculatedPost =
synchronizeState(postState, calculatedPost);
assert postState.getVariables()
.equals(synchronizedCalculatedPost.getVariables()) : MSG_TRACKED_VARIABLES_DIFFER;
final SubsetResult included = synchronizedCalculatedPost.isSubsetOf(postState);
if (included != SubsetResult.NONE) {
return trackPost(Validity.VALID, act);
}
final SubsetResult excluded = postState.isSubsetOf(synchronizedCalculatedPost);
if (excluded == SubsetResult.NONE) {
return trackPost(Validity.INVALID, act);
}
return Validity.UNKNOWN;
}

private Validity checkReturnTransitionNoLogging(final AbstractMultiState<STATE, ACTION, VARDECL> validPreLinState,
private Validity checkReturnTransitionWithValidState(
final AbstractMultiState<STATE, ACTION, VARDECL> validPreLinState,
final AbstractMultiState<STATE, ACTION, VARDECL> stateAfterLeaving, final ACTION act,
final AbstractMultiState<STATE, ACTION, VARDECL> postState) {

Expand All @@ -231,21 +250,33 @@ private Validity checkReturnTransitionNoLogging(final AbstractMultiState<STATE,

final AbstractMultiState<STATE, ACTION, VARDECL> calculatedPost =
stateAfterLeaving.apply(mPostOp, validPreLinState, act);
if (mLogger.isDebugEnabled()) {
mLogger.debug("Calculated post: " + calculatedPost.toLogString());
}
if (calculatedPost.isBottom() && postState.isBottom()) {
return trackPost(Validity.VALID, act);
}

final AbstractMultiState<STATE, ACTION, VARDECL> synchronizedCalculatedPost =
synchronizeState(postState, calculatedPost);
if (mLogger.isDebugEnabled()) {
mLogger.debug("Synchronized calculated post: " + calculatedPost.toLogString());
}
assert postState.getVariables()
.equals(synchronizedCalculatedPost.getVariables()) : MSG_TRACKED_VARIABLES_DIFFER;
final SubsetResult included = synchronizedCalculatedPost.isSubsetOf(postState);
if (mLogger.isDebugEnabled()) {
mLogger.debug("Inclusion (NO): " + included);
}
if (included != SubsetResult.NONE) {
return trackPost(Validity.VALID, act);
}
final SubsetResult excluded = postState.isSubsetOf(synchronizedCalculatedPost);
if (mLogger.isDebugEnabled()) {
mLogger.debug("Exclusion (ON): " + excluded);
}
if (excluded == SubsetResult.NONE) {
assert !synchronizedCalculatedPost.isBottom() : "Nothing is a subsetf of bottom";
assert !synchronizedCalculatedPost.isBottom() : "Nothing is a subset of bottom";
return trackPost(Validity.INVALID, act);
}
return Validity.UNKNOWN;
Expand Down

0 comments on commit 27d561c

Please sign in to comment.