From 889af75be64431024cebd9e5c1826377986d561e Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Fri, 19 Jun 2026 09:15:26 +0200 Subject: [PATCH 1/3] Refine settings for improved dumping of automata to files This change refines the existing automata dumping settings to enable more detailed and configurable automata dump options. The enhanced settings align with the 'WitnessPrinter' settings and simplify the dump configuration in BenchExec runs, particularly for reuse interpolant automata (incremental verification). The change also introduces a standardized naming convention for the dumped files (using 'TaskIdentifier' for proper filename patterns). --- .../cegar/AbstractBuchiCegarLoop.java | 16 ++-- .../SubtaskStringIdentifier.java | 43 ++++++++++ .../taskidentifier/TaskIdentifier.java | 4 +- .../traceabstraction/AbstractCegarLoop.java | 81 +++++++++++++++---- .../traceabstraction/BasicCegarLoop.java | 19 ++--- .../generator/traceabstraction/Dumper.java | 6 +- .../traceabstraction/EagerReuseCegarLoop.java | 10 +-- .../IncrementalInclusionCegarLoop.java | 8 +- .../traceabstraction/NwaCegarLoop.java | 9 +-- .../PathProgramDumpController.java | 2 +- .../concurrency/CegarLoopForPetriNet.java | 15 ++-- .../preferences/TAPreferences.java | 53 ++++++++---- ...TraceAbstractionPreferenceInitializer.java | 56 ++++++++----- .../TAwAFAsCegarLoop.java | 3 +- 14 files changed, 220 insertions(+), 105 deletions(-) create mode 100644 trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/taskidentifier/SubtaskStringIdentifier.java diff --git a/trunk/source/BuchiAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/buchiautomizer/cegar/AbstractBuchiCegarLoop.java b/trunk/source/BuchiAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/buchiautomizer/cegar/AbstractBuchiCegarLoop.java index 33ac8f52a83..b8dfe6c9320 100644 --- a/trunk/source/BuchiAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/buchiautomizer/cegar/AbstractBuchiCegarLoop.java +++ b/trunk/source/BuchiAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/buchiautomizer/cegar/AbstractBuchiCegarLoop.java @@ -317,8 +317,8 @@ public final BuchiCegarLoopResult runCegarLoop() throws IOException { if (mPref.dumpAutomata()) { final String filename = mIdentifier + "_" + name + "Abstraction" + mIteration; - BuchiAutomizerUtils.writeAutomatonToFile(mServices, mAbstraction, mPref.dumpPath(), filename, - mPref.getAutomataFormat(), ""); + BuchiAutomizerUtils.writeAutomatonToFile(mServices, mAbstraction, mPref.dumpAutomataDirectory(), filename, + mPref.dumpAutomataFormat(), ""); } boolean initalAbstractionCorrect; try { @@ -433,8 +433,8 @@ public final BuchiCegarLoopResult runCegarLoop() throws IOException { if (mPref.dumpAutomata()) { final String filename = mIdentifier + "_" + name + "Abstraction" + mIteration; - BuchiAutomizerUtils.writeAutomatonToFile(mServices, mAbstraction, mPref.dumpPath(), filename, - mPref.getAutomataFormat(), ""); + BuchiAutomizerUtils.writeAutomatonToFile(mServices, mAbstraction, mPref.dumpAutomataDirectory(), filename, + mPref.dumpAutomataFormat(), ""); } } catch (final AutomataLibraryException e) { @@ -485,8 +485,8 @@ private A refineFiniteInternal(final A abstraction, final LassoCheck lassoChe determinized.switchToReadonlyMode(); if (mPref.dumpAutomata()) { final String filename = mIdentifier + "_" + "interpolAutomatonUsedInRefinement" + mIteration + "after"; - BuchiAutomizerUtils.writeAutomatonToFile(mServices, interpolAutomaton, mPref.dumpPath(), filename, - mPref.getAutomataFormat(), ""); + BuchiAutomizerUtils.writeAutomatonToFile(mServices, interpolAutomaton, mPref.dumpAutomataDirectory(), filename, + mPref.dumpAutomataFormat(), ""); } if (mConstructTermcompProof) { mTermcompProofBenchmark.reportFiniteModule(mIteration, interpolAutomaton); @@ -529,8 +529,8 @@ private A refineBuchiInternal(final LassoCheck lassoCheck) throws AutomataOpe assert !SmtUtils.isFalseLiteral(rankEqAndSi.getFormula()); final boolean dumpAutomata = mPref.dumpAutomata(); - final String dumpPath = mPref.dumpPath(); - final Format format = mPref.getAutomataFormat(); + final String dumpPath = mPref.dumpAutomataDirectory(); + final Format format = mPref.dumpAutomataFormat(); final RankingFunction rankingFunction = bspmResult.getTerminationArgument().getRankingFunction(); final Script script = mCsToolkitWithRankVars.getManagedScript().getScript(); diff --git a/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/taskidentifier/SubtaskStringIdentifier.java b/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/taskidentifier/SubtaskStringIdentifier.java new file mode 100644 index 00000000000..2ba3d6a5118 --- /dev/null +++ b/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/taskidentifier/SubtaskStringIdentifier.java @@ -0,0 +1,43 @@ +/* + * Copyright (C) 2026 Manuel Bentele + * Copyright (C) 2026 University of Freiburg + * + * This file is part of the ULTIMATE ModelCheckerUtils Library. + * + * The ULTIMATE ModelCheckerUtils Library is free software: you can redistribute it and/or modify it under the terms of + * the GNU Lesser General Public License as published by the Free Software Foundation, either version 3 of the License, + * or (at your option) any later version. + * + * The ULTIMATE ModelCheckerUtils Library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; + * without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General + * Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License along with the ULTIMATE ModelCheckerUtils + * Library. If not, see . + * + * Additional permission under GNU GPL version 3 section 7: If you modify the ULTIMATE ModelCheckerUtils Library, or + * any covered work, by linking or combining it with Eclipse RCP (or a modified version of Eclipse RCP), containing + * parts covered by the terms of the Eclipse Public License, the licensors of the ULTIMATE ModelCheckerUtils Library + * grant you additional permission to convey the resulting work. + */ + +package de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.taskidentifier; + +/** + * @author Manuel Bentele + */ +public class SubtaskStringIdentifier extends TaskIdentifier { + + private final String mString; + + public SubtaskStringIdentifier(final TaskIdentifier parentTaskIdentifier, final String string) { + super(parentTaskIdentifier); + mString = string; + } + + @Override + protected String getSubtaskIdentifier() { + return mString; + } + +} diff --git a/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/taskidentifier/TaskIdentifier.java b/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/taskidentifier/TaskIdentifier.java index c2536367a0a..269c16d1804 100644 --- a/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/taskidentifier/TaskIdentifier.java +++ b/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/taskidentifier/TaskIdentifier.java @@ -48,6 +48,8 @@ */ public abstract class TaskIdentifier { + public static final String SEPARATOR = "_"; + private final TaskIdentifier mParentTaskIdentifier; protected abstract String getSubtaskIdentifier(); @@ -61,7 +63,7 @@ public String toString() { if (mParentTaskIdentifier == null) { return getSubtaskIdentifier(); } else { - return mParentTaskIdentifier.toString() + "_" + getSubtaskIdentifier(); + return mParentTaskIdentifier.toString() + SEPARATOR + getSubtaskIdentifier(); } } diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/AbstractCegarLoop.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/AbstractCegarLoop.java index 21f9874f5e5..329e56dc7cf 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/AbstractCegarLoop.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/AbstractCegarLoop.java @@ -28,6 +28,7 @@ package de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction; import java.io.File; +import java.nio.file.Paths; import java.util.ArrayList; import java.util.Collections; import java.util.EnumSet; @@ -60,6 +61,7 @@ import de.uni_freiburg.informatik.ultimate.core.lib.results.StatisticsResult; import de.uni_freiburg.informatik.ultimate.core.lib.results.UnprovabilityReason; import de.uni_freiburg.informatik.ultimate.core.model.models.IElement; +import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger; import de.uni_freiburg.informatik.ultimate.core.model.services.IProgressAwareTimer; import de.uni_freiburg.informatik.ultimate.core.model.services.IProgressMonitorService; @@ -77,6 +79,8 @@ import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.IPredicateUnifier; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.PredicateFactory; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.taskidentifier.SubtaskFileIdentifier; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.taskidentifier.SubtaskIterationIdentifier; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.taskidentifier.SubtaskStringIdentifier; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.taskidentifier.TaskIdentifier; import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.SmtUtils.SimplificationTechnique; import de.uni_freiburg.informatik.ultimate.logic.Script; @@ -167,12 +171,16 @@ public abstract class AbstractCegarLoop, A extends // used for debugging only protected IAutomaton mArtifactAutomaton; - protected final Format mPrintAutomataLabeling; + protected final Format mDumpAutomataFormat; protected CegarLoopStatisticsGenerator mCegarLoopBenchmark; protected IUltimateServiceProvider mServices; + protected final String mTaskFilename; + + protected final DebugIdentifier mTaskDebugIdentifier; + protected final TaskIdentifier mTaskIdentifier; protected Dumper mDumper; @@ -208,7 +216,7 @@ protected AbstractCegarLoop(final IUltimateServiceProvider services, final Debug mServices = services; mLogger = services.getLoggingService().getLogger(Activator.PLUGIN_ID); mSimplificationTechnique = taPrefs.getSimplificationTechnique(); - mPrintAutomataLabeling = taPrefs.getAutomataFormat(); + mDumpAutomataFormat = taPrefs.dumpAutomataFormat(); mName = name; mAbstraction = initialAbstraction; mIcfg = rootNode; @@ -216,8 +224,10 @@ protected AbstractCegarLoop(final IUltimateServiceProvider services, final Debug mPredicateFactory = predicateFactory; mPref = taPrefs; mErrorLocs = errorLocs; + mTaskFilename = ILocation.getAnnotation(rootNode).getFileName(); + mTaskDebugIdentifier = name; // TODO: TaskIdentifier should probably be provided by caller - mTaskIdentifier = new SubtaskFileIdentifier(null, mIcfg.getIdentifier() + "_" + name); + mTaskIdentifier = new SubtaskFileIdentifier(null, mIcfg.getIdentifier() + "_" + mTaskDebugIdentifier); mResultBuilder = new CegarLoopResultBuilder(); } @@ -347,7 +357,8 @@ private final CegarLoopResult startCegar() { } // initialize dump of debugging output to files if necessary if (mPref.dumpAutomata()) { - mDumper = new Dumper(mLogger, mPref, mName, mIteration); + final TaskIdentifier tid = new SubtaskIterationIdentifier(null, mIteration); + mDumper = new Dumper(mLogger, this.getDumpAutomataPath(tid.toString())); } try { if (!computeInitialAbstraction()) { @@ -384,8 +395,7 @@ private boolean computeInitialAbstraction() throws AutomataLibraryException { mArtifactAutomaton = mAbstraction; } if (mPref.dumpAutomata()) { - final String filename = mTaskIdentifier + "_InitialAbstraction"; - writeAutomatonToFile(mAbstraction, filename); + this.writeAutomatonToFile(mAbstraction, "InitialAbstraction"); } mCegarLoopBenchmark.reportAbstractionSize(mAbstraction.size(), mIteration); @@ -417,7 +427,8 @@ protected void iterate() throws AutomataLibraryException { mDumper.close(); } if (mPref.dumpAutomata()) { - mDumper = new Dumper(mLogger, mPref, mName, mIteration); + final TaskIdentifier tid = new SubtaskIterationIdentifier(null, mIteration); + mDumper = new Dumper(mLogger, this.getDumpAutomataPath(tid.toString())); } try { @@ -499,8 +510,7 @@ private void refineAbstractionInternal(final AutomatonType automatonType) final boolean newMaximumReached = mCegarLoopBenchmark.reportAbstractionSize(mAbstraction.size(), mIteration); if (DUMP_BIGGEST_AUTOMATON && mIteration > 4 && newMaximumReached) { - final String filename = mIcfg.getIdentifier() + "_BiggestAutomaton"; - writeAutomatonToFile(mAbstraction, filename); + this.writeAutomatonToFile(mAbstraction, "BiggestAutomaton"); } } @@ -624,23 +634,60 @@ private CegarLoopResult performLimitReachedActions(final IRunningTaskStackPro return mResultBuilder.addResultForAllRemaining(res, null, e, null).getResult(); } - protected void writeAutomatonToFile(final IAutomaton automaton, final String filename) { + protected String getDumpAutomataPath(final String suffix) { + String filePath = null; + + if (mPref.dumpAutomataBesideFile()) { + assert Paths.get(mTaskFilename).isAbsolute(); + filePath = mTaskFilename; + } else { + filePath = mPref.dumpAutomataDirectory() + File.separator + mPref.dumpAutomataFilename(); + } + + filePath += TaskIdentifier.SEPARATOR + mTaskDebugIdentifier.toString(); + + return (suffix != null && !suffix.isEmpty()) ? filePath + TaskIdentifier.SEPARATOR + suffix : filePath; + } + + protected void writeAutomatonToFile(final IAutomaton automaton, final TaskIdentifier tid) { mCegarLoopBenchmark.start(CegarLoopStatisticsDefinitions.DumpTime); + final String fullAutomataPath = this.getDumpAutomataPath(tid.toString()); new AutomatonDefinitionPrinter(new AutomataLibraryServices(getServices()), - determineAutomatonName(automaton), mPref.dumpPath() + File.separator + filename, mPrintAutomataLabeling, - "", automaton); + determineAutomatonName(automaton), fullAutomataPath, mDumpAutomataFormat, "", automaton); mCegarLoopBenchmark.stop(CegarLoopStatisticsDefinitions.DumpTime); } - protected void writeAutomataToFile(final String filename, final String atsHeaderMessage, final String atsCommands, - final NamedAutomaton... automata) { + protected void writeAutomatonToFile(final IAutomaton automaton, final String suffix) { + final TaskIdentifier tid = new SubtaskStringIdentifier(null, suffix); + this.writeAutomatonToFile(automaton, tid); + } + + protected void writeAutomatonToFile(final IAutomaton automaton, final int iteration) { + final TaskIdentifier tid = new SubtaskIterationIdentifier(null, iteration); + this.writeAutomatonToFile(automaton, tid); + } + + protected void writeAutomatonToFile(final IAutomaton automaton, final int iteration, + final String suffix) { + final TaskIdentifier tid = new SubtaskStringIdentifier(new SubtaskIterationIdentifier(null, iteration), suffix); + this.writeAutomatonToFile(automaton, tid); + } + + protected void writeAutomataToFile(final TaskIdentifier tid, final String atsHeaderMessage, + final String atsCommands, final NamedAutomaton... automata) { mCegarLoopBenchmark.start(CegarLoopStatisticsDefinitions.DumpTime); - AutomatonDefinitionPrinter.writeAutomatonToFile(new AutomataLibraryServices(getServices()), - mPref.dumpPath() + File.separator + filename, mPrintAutomataLabeling, atsHeaderMessage, atsCommands, - automata); + final String fullAutomataPath = this.getDumpAutomataPath(tid.toString()); + AutomatonDefinitionPrinter.writeAutomatonToFile(new AutomataLibraryServices(getServices()), fullAutomataPath, + mDumpAutomataFormat, atsHeaderMessage, atsCommands, automata); mCegarLoopBenchmark.stop(CegarLoopStatisticsDefinitions.DumpTime); } + protected void writeAutomataToFile(final int iteration, final String suffix, final String atsHeaderMessage, + final String atsCommands, final NamedAutomaton... automata) { + final TaskIdentifier tid = new SubtaskStringIdentifier(new SubtaskIterationIdentifier(null, iteration), suffix); + this.writeAutomataToFile(tid, atsHeaderMessage, atsCommands, automata); + } + private String determineAutomatonName(final IAutomaton automaton) { String result; if (automaton instanceof INwaBasis) { diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/BasicCegarLoop.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/BasicCegarLoop.java index 99538f560e5..4ab84dd6a44 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/BasicCegarLoop.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/BasicCegarLoop.java @@ -93,6 +93,7 @@ import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.PredicateFactory; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.PredicateUnifier; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.taskidentifier.SubtaskIterationIdentifier; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.taskidentifier.SubtaskStringIdentifier; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.tracehandling.IRefinementEngineResult; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.tracehandling.IRefinementEngineResult.BasicRefinementEngineResult; import de.uni_freiburg.informatik.ultimate.lib.proofs.floydhoare.NwaFloydHoareValidityCheck; @@ -198,10 +199,9 @@ public BasicCegarLoop(final DebugIdentifier name, final A initialAbstraction, fi // Construct an empty file. We need this empty file in cases where // the CFG does not have error location and no automaton is dumped. mLogger.info("Dumping reuse automata for " + mTaskIdentifier.toString()); - final String filename = mTaskIdentifier + "-reuse"; - final String fullPath = mPref.dumpPath() + File.separator + filename + "." - + mPrintAutomataLabeling.getFormat().getFileEnding(); - final File file = new File(fullPath); + final String fullAutomataPath = getDumpAutomataPath(new SubtaskStringIdentifier(null, "reuse").toString()) + + "." + mPref.dumpAutomataFormat().getFormat().getFileEnding(); + final File file = new File(fullAutomataPath); try { final FileWriter fw = new FileWriter(file, false); fw.close(); @@ -378,9 +378,7 @@ protected void constructInterpolantAutomaton() throws AutomataOperationCanceledE mInterpolAutomaton = mRefinementResult.getInfeasibilityProof(); if (mPref.dumpAutomata()) { - final String filename = - new SubtaskIterationIdentifier(mTaskIdentifier, getIteration()) + "_RawFloydHoareAutomaton"; - super.writeAutomatonToFile(mInterpolAutomaton, filename); + super.writeAutomatonToFile(mInterpolAutomaton, getIteration(), "RawFloydHoareAutomaton"); } assert isInterpolantAutomatonOfSingleStateType(mInterpolAutomaton); @@ -503,7 +501,6 @@ protected void dumpOrAppendAutomatonForReuseIfEnabled( mCegarLoopBenchmark.start(CegarLoopStatisticsDefinitions.DumpTime); mLogger.info("Dumping reuse automata for " + mTaskIdentifier.toString() + " " + automaton.getClass()); - final String filename = mTaskIdentifier + "-reuse"; final INwaOutgoingLetterAndTransitionProvider printedAutomaton; final AutomataLibraryServices services = new AutomataLibraryServices(getServices()); final boolean addPredicateImplicationInformation = true; @@ -526,9 +523,9 @@ protected void dumpOrAppendAutomatonForReuseIfEnabled( } else { printedAutomaton = automaton; } - new AutomatonDefinitionPrinter(services, "nwa" + getIteration(), - mPref.dumpPath() + File.separator + filename, mPrintAutomataLabeling, "", !mFirstReuseDump, - printedAutomaton); + final String fullAutomataPath = getDumpAutomataPath(new SubtaskStringIdentifier(null, "reuse").toString()); + new AutomatonDefinitionPrinter(services, "nwa" + getIteration(), fullAutomataPath, + mDumpAutomataFormat, "", !mFirstReuseDump, printedAutomaton); mFirstReuseDump = false; mLogger.info("Finished dumping"); mCegarLoopBenchmark.stop(CegarLoopStatisticsDefinitions.DumpTime); diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/Dumper.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/Dumper.java index 16bd7214ca3..f1f5b4e4d68 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/Dumper.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/Dumper.java @@ -39,7 +39,6 @@ import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWord; import de.uni_freiburg.informatik.ultimate.core.lib.exceptions.ToolchainExceptionWrapper; import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger; -import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.debugidentifiers.DebugIdentifier; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.IPredicate; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.ISLPredicate; import de.uni_freiburg.informatik.ultimate.logic.FormulaUnLet; @@ -48,15 +47,14 @@ import de.uni_freiburg.informatik.ultimate.logic.Term; import de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder.cfg.BoogieIcfgLocation; import de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder.cfg.CodeBlock; -import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.preferences.TAPreferences; import de.uni_freiburg.informatik.ultimate.util.CoreUtil; public final class Dumper implements AutoCloseable { private final PrintWriter mIterationPW; private final ILogger mLogger; - Dumper(final ILogger logger, final TAPreferences prefs, final DebugIdentifier name, final int iteration) { - final File file = new File(prefs.dumpPath() + "/" + name + "_iteration" + iteration + ".txt"); + Dumper(final ILogger logger, final String path) { + final File file = new File(path + ".txt"); try { mIterationPW = new PrintWriter(new FileWriter(file)); } catch (final IOException e) { diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/EagerReuseCegarLoop.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/EagerReuseCegarLoop.java index 10ad3d87d88..32f72572adc 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/EagerReuseCegarLoop.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/EagerReuseCegarLoop.java @@ -119,7 +119,7 @@ private void computeDifferenceForReuseAutomaton(final int iteration, final int oneBasedi = iteration + 1; if (mPref.dumpAutomata()) { - writeAutomatonToFile(reuseAut, "ReusedAutomata" + oneBasedi); + super.writeAutomatonToFile(reuseAut, "ReusedAutomata" + oneBasedi); } if (reuseAut instanceof AbstractInterpolantAutomaton) { @@ -131,9 +131,8 @@ private void computeDifferenceForReuseAutomaton(final int iteration, new PowersetDeterminizer<>(reuseAut, true, mPredicateFactoryInterpolantAutomata); final boolean explointSigmaStarConcatOfIA = true; final IOpWithDelayedDeadEndRemoval diff = - new Difference<>(new AutomataLibraryServices(getServices()), mStateFactoryForRefinement, - (INwaOutgoingLetterAndTransitionProvider) mAbstraction, reuseAut, psd, - explointSigmaStarConcatOfIA); + new Difference<>(new AutomataLibraryServices(getServices()), mStateFactoryForRefinement, mAbstraction, + reuseAut, psd, explointSigmaStarConcatOfIA); if (reuseAut instanceof AbstractInterpolantAutomaton) { final AbstractInterpolantAutomaton aiReuseAut = (AbstractInterpolantAutomaton) reuseAut; @@ -147,8 +146,7 @@ assert checkInterpolantAutomatonInductivity( predicateUnifier); if (mPref.dumpAutomata()) { - final String filename = "DiffAfterEagerReuse" + oneBasedi; - writeAutomatonToFile(diff.getResult(), filename); + writeAutomatonToFile(diff.getResult(), "DiffAfterEagerReuse" + oneBasedi); } dumpOrAppendAutomatonForReuseIfEnabled(reuseAut, predicateUnifier); diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/IncrementalInclusionCegarLoop.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/IncrementalInclusionCegarLoop.java index beaf4a56c60..5dc6d679a07 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/IncrementalInclusionCegarLoop.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/IncrementalInclusionCegarLoop.java @@ -231,9 +231,7 @@ protected boolean refineAbstraction() throws AutomataLibraryException { } if (mPref.dumpAutomata()) { for (int i = 0; i < mInterpolantAutomata.size(); i++) { - final String filename = - "IncrementalInclusion_Interation" + getIteration() + "_InterpolantAutomaton" + i; - super.writeAutomatonToFile(mInterpolantAutomata.get(i), filename); + super.writeAutomatonToFile(mInterpolantAutomata.get(i), getIteration(), "InterpolantAutomaton" + i); } } } finally { @@ -255,9 +253,7 @@ private void switchAllInterpolantAutomataToReadOnlyMode() { } if (mPref.dumpAutomata()) { for (final AbstractInterpolantAutomaton element : mInterpolantAutomata) { - final String filename = - "EnhancedInterpolantAutomaton_WhoseConstructionWasStartedIn_Iteration" + getIteration(); - super.writeAutomatonToFile(element, filename); + super.writeAutomatonToFile(element, getIteration(), "EnhancedInterpolantAutomaton"); } } } diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/NwaCegarLoop.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/NwaCegarLoop.java index d0c4e23585d..b3e4358b56a 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/NwaCegarLoop.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/NwaCegarLoop.java @@ -82,7 +82,6 @@ import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.PredicateFactory; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.PredicateUnifier; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.PredicateUtils; -import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.taskidentifier.SubtaskIterationIdentifier; import de.uni_freiburg.informatik.ultimate.lib.proofs.floydhoare.HoareAnnotationPositions; import de.uni_freiburg.informatik.ultimate.lib.proofs.floydhoare.NwaFloydHoareValidityCheck; import de.uni_freiburg.informatik.ultimate.lib.proofs.floydhoare.NwaHoareProofProducer; @@ -394,9 +393,7 @@ private void computeAutomataDifference(final INestedWordAutomaton } if (mPref.dumpAutomata()) { - final String filename = - new SubtaskIterationIdentifier(mTaskIdentifier, getIteration()) + "AbstractionAfterDifference"; - super.writeAutomatonToFile(subtrahend, filename); + super.writeAutomatonToFile(subtrahend, getIteration(), "AbstractionAfterDifference"); } dumpOrAppendAutomatonForReuseIfEnabled(subtrahend, predicateUnifier); @@ -416,9 +413,7 @@ private void computeAutomataDifference(final INestedWordAutomaton } mAbstraction = diff.getResult(); if (mPref.dumpAutomata()) { - final String filename = new SubtaskIterationIdentifier(mTaskIdentifier, getIteration()) - + "AbstractionAfterDifferenceAndDeadEndRemoval"; - super.writeAutomatonToFile(mAbstraction, filename); + super.writeAutomatonToFile(mAbstraction, getIteration(), "AbstractionAfterDifferenceAndDeadEndRemoval"); } } finally { diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/PathProgramDumpController.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/PathProgramDumpController.java index 964ba2ce268..7a9cc1d6df3 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/PathProgramDumpController.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/PathProgramDumpController.java @@ -105,7 +105,7 @@ private void doDump(final IRun counterexample, final int iteration) { throw createToolchainCanceledException(message, iteration); } - final String filename = mPref.dumpPath() + File.separator + mIcfg.getIdentifier() + "_" + iteration + ".bpl"; + final String filename = mPref.dumpAutomataDirectory() + File.separator + mIcfg.getIdentifier() + "_" + iteration + ".bpl"; new PathProgramDumper(mIcfg, mServices, counterexample, filename, DUMP_PATH_PROGRAMS_INPUT_MODE); if (mDumpStopMode == PathProgramDumpStop.AFTER_FIRST_DUMP) { diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/concurrency/CegarLoopForPetriNet.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/concurrency/CegarLoopForPetriNet.java index 17c27a5591b..1275b6fdb17 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/concurrency/CegarLoopForPetriNet.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/concurrency/CegarLoopForPetriNet.java @@ -232,9 +232,8 @@ protected boolean refineAbstraction() throws AutomataLibraryException { } if (mPref.dumpAutomata()) { - final String filename = new SubtaskIterationIdentifier(mTaskIdentifier, getIteration()) - + "_AbstractionAfterDifferencePairwiseOnDemand"; - super.writeAutomatonToFile(enhancementResult.getSecond().getResult(), filename); + super.writeAutomatonToFile(enhancementResult.getSecond().getResult(), getIteration(), + "AbstractionAfterDifferencePairwiseOnDemand"); } if (getIteration() <= mPref.watchIteration() && mPref.artifact() == Artifact.NEG_INTERPOLANT_AUTOMATON) { @@ -486,12 +485,10 @@ protected boolean refineAbstraction() throws AutomataLibraryException { dia = new RemoveUnreachable<>(new AutomataLibraryServices(getServices()), awis).getResult(); final long end = System.nanoTime(); if (end - start > DEBUG_DUMP_DRYRUNRESULT_THRESHOLD * 1_000_000_000L) { - final String filename = new SubtaskIterationIdentifier(mTaskIdentifier, getIteration()) - + "_DifferencePairwiseOnDemandInput"; final String atsHeaderMessage = "inputs of difference operation in iteration " + getIteration(); final String atsCode = "PetriNet diff = differencePairwiseOnDemand(net, nwa);"; - super.writeAutomataToFile(filename, atsHeaderMessage, atsCode, - new NamedAutomaton<>("net", mAbstraction), new NamedAutomaton<>("nwa", dia)); + super.writeAutomataToFile(getIteration(), "DifferencePairwiseOnDemandInput", atsHeaderMessage, + atsCode, new NamedAutomaton<>("net", mAbstraction), new NamedAutomaton<>("nwa", dia)); } } else { dpod = null; @@ -508,9 +505,7 @@ protected boolean refineAbstraction() throws AutomataLibraryException { .getTransitionDensity(SymbolType.INTERNAL); mLogger.info("DFA transition density " + dfaTransitionDensity); if (mPref.dumpAutomata()) { - final String filename = - new SubtaskIterationIdentifier(mTaskIdentifier, getIteration()) + "_EagerFloydHoareAutomaton"; - super.writeAutomatonToFile(dia, filename); + super.writeAutomatonToFile(dia, getIteration(), "EagerFloydHoareAutomaton"); } break; default: diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/preferences/TAPreferences.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/preferences/TAPreferences.java index e881a823dca..6c91ed02a3d 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/preferences/TAPreferences.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/preferences/TAPreferences.java @@ -70,8 +70,11 @@ public final class TAPreferences { private final InterpolationTechnique mInterpolation; private final InterpolantAutomaton mInterpolantAutomaton; private final boolean mDumpAutomata; - private final Format mAutomataFormat; - private final String mDumpPath; + private final Format mDumpAutomataFormat; + private final String mDumpAutomataDirectory; + private final String mDumpAutomataFilename; + private final boolean mDumpAutomataBesideFile; + private final boolean mDumpOnlyReuseAutomata; private final InterpolantAutomatonEnhancement mDeterminiation; private final Minimization mMinimize; private final Concurrency mAutomataTypeConcurrency; @@ -79,7 +82,6 @@ public final class TAPreferences { @Reflected(excluded = true) private final IPreferenceProvider mPrefs; private final HoareAnnotationPositions mHoareAnnotationPositions; - private final boolean mDumpOnlyReuseAutomata; private final int mLimitTraceHistogram; private final int mErrorLocTimeLimit; private final int mLimitPathProgramCount; @@ -140,12 +142,15 @@ public TAPreferences(final IUltimateServiceProvider services) { mInterpolantAutomaton = mPrefs.getEnum(TraceAbstractionPreferenceInitializer.LABEL_INTERPOLANT_AUTOMATON, InterpolantAutomaton.class); - mDumpAutomata = mPrefs.getBoolean(TraceAbstractionPreferenceInitializer.LABEL_DUMPAUTOMATA); - - mAutomataFormat = mPrefs.getEnum(TraceAbstractionPreferenceInitializer.LABEL_AUTOMATAFORMAT, Format.class); - - mDumpPath = mPrefs.getString(TraceAbstractionPreferenceInitializer.LABEL_DUMPPATH); - mDumpOnlyReuseAutomata = mPrefs.getBoolean(TraceAbstractionPreferenceInitializer.LABEL_DUMP_ONLY_REUSE); + mDumpAutomata = mPrefs.getBoolean(TraceAbstractionPreferenceInitializer.LABEL_DUMP_AUTOMATA); + mDumpAutomataFormat = + mPrefs.getEnum(TraceAbstractionPreferenceInitializer.LABEL_DUMP_AUTOMATA_FORMAT, Format.class); + mDumpAutomataDirectory = mPrefs.getString(TraceAbstractionPreferenceInitializer.LABEL_DUMP_AUTOMATA_DIRECTORY); + mDumpAutomataFilename = mPrefs.getString(TraceAbstractionPreferenceInitializer.LABEL_DUMP_AUTOMATA_FILENAME); + mDumpAutomataBesideFile = + mPrefs.getBoolean(TraceAbstractionPreferenceInitializer.LABEL_DUMP_AUTOMATA_BESIDE_FILE); + mDumpOnlyReuseAutomata = + mPrefs.getBoolean(TraceAbstractionPreferenceInitializer.LABEL_DUMP_AUTOMATA_ONLY_REUSE); mDeterminiation = mPrefs.getEnum(TraceAbstractionPreferenceInitializer.LABEL_INTERPOLANT_AUTOMATON_ENHANCEMENT, InterpolantAutomatonEnhancement.class); @@ -315,17 +320,37 @@ public boolean dumpAutomata() { return mDumpAutomata && !mDumpOnlyReuseAutomata; } - public Format getAutomataFormat() { - return mAutomataFormat; + /** + * @return The automata dump format. + */ + public Format dumpAutomataFormat() { + return mDumpAutomataFormat; + } + + /** + * @return The automata dump directory. + */ + public String dumpAutomataDirectory() { + return mDumpAutomataDirectory; + } + + /** + * @return The automata dump filename. + */ + public String dumpAutomataFilename() { + return mDumpAutomataFilename; } /** - * @return The dump path. + * @return The automata dump besides input file flag. */ - public String dumpPath() { - return mDumpPath; + public boolean dumpAutomataBesideFile() { + return mDumpAutomataBesideFile; } + /** + * @return The only-resue automata dump flag. + */ public boolean dumpOnlyReuseAutomata() { return mDumpAutomata && mDumpOnlyReuseAutomata; } diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/preferences/TraceAbstractionPreferenceInitializer.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/preferences/TraceAbstractionPreferenceInitializer.java index f17dc28559c..065e51274ec 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/preferences/TraceAbstractionPreferenceInitializer.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/preferences/TraceAbstractionPreferenceInitializer.java @@ -349,18 +349,32 @@ public enum CoinflipMode { // Automata dumping // ======================================================================== - public static final String LABEL_DUMPAUTOMATA = "Dump automata to files"; - private static final boolean DEF_DUMPAUTOMATA = false; - - public static final String LABEL_AUTOMATAFORMAT = "Output format of dumped automata"; - private static final Format DEF_AUTOMATAFORMAT = Format.ATS_NUMERATE; - - public static final String LABEL_DUMPPATH = "Dump automata to the following directory"; - private static final String DEF_DUMPPATH = "."; - - public static final String LABEL_DUMP_ONLY_REUSE = "Dump only reuse-automata"; - private static final boolean DEF_ONLY_REUSE = false; - private static final String DESC_DUMP_ONLY_REUSE = + public static final String LABEL_DUMP_AUTOMATA = "Dump automata"; + private static final boolean DEF_DUMP_AUTOMATA = false; + private static final String DESC_DUMP_AUTOMATA = "Dump automata to files."; + + public static final String LABEL_DUMP_AUTOMATA_FORMAT = "Dump automata format"; + private static final Format DEF_DUMP_AUTOMATA_FORMAT = Format.ATS_NUMERATE; + private static final String DESC_DUMP_AUTOMATA_FORMAT = "Output format of dumped automata."; + + public static final String LABEL_DUMP_AUTOMATA_DIRECTORY = "Dump automata directory"; + private static final String DEF_DUMP_AUTOMATA_DIRECTORY = "."; + private static final String DESC_DUMP_AUTOMATA_DIRECTORY = "Dump automata to the specified directory."; + + public static final String LABEL_DUMP_AUTOMATA_FILENAME = "Dump automata filename"; + private static final String DEF_DUMP_AUTOMATA_FILENAME = "automata"; + private static final String DESC_DUMP_AUTOMATA_FILENAME = + "The filename of the dumped automata (without file extension)."; + + public static final String LABEL_DUMP_AUTOMATA_BESIDE_FILE = "Dump automata besides input file"; + private static final boolean DEF_DUMP_AUTOMATA_BESIDE_FILE = true; + private static final String DESC_DUMP_AUTOMATA_BESIDE_FILE = + "Dump automata as \"-automata.ats\" in the same directory as the input file. " + + "All other output options are ignored."; + + public static final String LABEL_DUMP_AUTOMATA_ONLY_REUSE = "Dump only reuse-automata"; + private static final boolean DEF_DUMP_AUTOMATA_ONLY_REUSE = false; + private static final String DESC_DUMP_AUTOMATA_ONLY_REUSE = "When dumping automata is enabled, we only dump the interpolant automaton and add to that file if it " + "exists s.t. it can be reused by later verification runs."; @@ -673,12 +687,18 @@ protected BaseUltimatePreferenceItem[] initDefaultPreferences() { PreferenceType.Combo, HoareTripleChecks.values()), new UltimatePreferenceItemGroup("Automata Dumping", - new UltimatePreferenceItem<>(LABEL_DUMPAUTOMATA, DEF_DUMPAUTOMATA, PreferenceType.Boolean), - new UltimatePreferenceItem<>(LABEL_AUTOMATAFORMAT, DEF_AUTOMATAFORMAT, PreferenceType.Combo, - Format.values()), - new UltimatePreferenceItem<>(LABEL_DUMPPATH, DEF_DUMPPATH, PreferenceType.Directory), - new UltimatePreferenceItem<>(LABEL_DUMP_ONLY_REUSE, DEF_ONLY_REUSE, DESC_DUMP_ONLY_REUSE, - PreferenceType.Boolean)), + new UltimatePreferenceItem<>(LABEL_DUMP_AUTOMATA, DEF_DUMP_AUTOMATA, DESC_DUMP_AUTOMATA, + PreferenceType.Boolean), + new UltimatePreferenceItem<>(LABEL_DUMP_AUTOMATA_FORMAT, DEF_DUMP_AUTOMATA_FORMAT, + DESC_DUMP_AUTOMATA_FORMAT, PreferenceType.Combo, Format.values()), + new UltimatePreferenceItem<>(LABEL_DUMP_AUTOMATA_DIRECTORY, DEF_DUMP_AUTOMATA_DIRECTORY, + DESC_DUMP_AUTOMATA_DIRECTORY, PreferenceType.Directory), + new UltimatePreferenceItem<>(LABEL_DUMP_AUTOMATA_FILENAME, DEF_DUMP_AUTOMATA_FILENAME, + DESC_DUMP_AUTOMATA_FILENAME, PreferenceType.String), + new UltimatePreferenceItem<>(LABEL_DUMP_AUTOMATA_BESIDE_FILE, DEF_DUMP_AUTOMATA_BESIDE_FILE, + DESC_DUMP_AUTOMATA_BESIDE_FILE, PreferenceType.Boolean), + new UltimatePreferenceItem<>(LABEL_DUMP_AUTOMATA_ONLY_REUSE, DEF_DUMP_AUTOMATA_ONLY_REUSE, + DESC_DUMP_AUTOMATA_ONLY_REUSE, PreferenceType.Boolean)), new UltimatePreferenceItem<>(LABEL_LANGUAGE_OPERATION, LanguageOperation.DIFFERENCE, PreferenceType.Combo, LanguageOperation.values()), diff --git a/trunk/source/TraceAbstractionWithAFAs/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstractionwithafas/TAwAFAsCegarLoop.java b/trunk/source/TraceAbstractionWithAFAs/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstractionwithafas/TAwAFAsCegarLoop.java index a62c1893072..be0ebcfcc80 100644 --- a/trunk/source/TraceAbstractionWithAFAs/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstractionwithafas/TAwAFAsCegarLoop.java +++ b/trunk/source/TraceAbstractionWithAFAs/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstractionwithafas/TAwAFAsCegarLoop.java @@ -573,8 +573,7 @@ protected boolean refineAbstraction() throws AutomataLibraryException { // copie mAbstraction = diff.getResult(); // mDeadEndRemovalTime = diff.getDeadEndRemovalTime(); if (mPref.dumpAutomata()) { - final String filename = "InterpolantAutomaton_Iteration" + getIteration(); - super.writeAutomatonToFile(mInterpolAutomaton, filename); + super.writeAutomatonToFile(mInterpolAutomaton, getIteration()); } mCegarLoopBenchmark.stop(CegarLoopStatisticsDefinitions.AutomataDifference.toString()); From bcdd8f2f167455791e393ad0eb69bfc927c1c4cc Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Sun, 21 Jun 2026 16:25:26 +0200 Subject: [PATCH 2/3] Remove explicit (but unneccessary) 'this' and 'super' reference keywords --- .../traceabstraction/AbstractCegarLoop.java | 20 ++++++++-------- .../traceabstraction/BasicCegarLoop.java | 2 +- .../traceabstraction/EagerReuseCegarLoop.java | 2 +- .../IncrementalInclusionCegarLoop.java | 4 ++-- .../traceabstraction/NwaCegarLoop.java | 4 ++-- .../concurrency/CegarLoopForPetriNet.java | 24 +++++++------------ .../TAwAFAsCegarLoop.java | 2 +- 7 files changed, 25 insertions(+), 33 deletions(-) diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/AbstractCegarLoop.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/AbstractCegarLoop.java index 329e56dc7cf..1688f49b717 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/AbstractCegarLoop.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/AbstractCegarLoop.java @@ -358,7 +358,7 @@ private final CegarLoopResult startCegar() { // initialize dump of debugging output to files if necessary if (mPref.dumpAutomata()) { final TaskIdentifier tid = new SubtaskIterationIdentifier(null, mIteration); - mDumper = new Dumper(mLogger, this.getDumpAutomataPath(tid.toString())); + mDumper = new Dumper(mLogger, getDumpAutomataPath(tid.toString())); } try { if (!computeInitialAbstraction()) { @@ -395,7 +395,7 @@ private boolean computeInitialAbstraction() throws AutomataLibraryException { mArtifactAutomaton = mAbstraction; } if (mPref.dumpAutomata()) { - this.writeAutomatonToFile(mAbstraction, "InitialAbstraction"); + writeAutomatonToFile(mAbstraction, "InitialAbstraction"); } mCegarLoopBenchmark.reportAbstractionSize(mAbstraction.size(), mIteration); @@ -428,7 +428,7 @@ protected void iterate() throws AutomataLibraryException { } if (mPref.dumpAutomata()) { final TaskIdentifier tid = new SubtaskIterationIdentifier(null, mIteration); - mDumper = new Dumper(mLogger, this.getDumpAutomataPath(tid.toString())); + mDumper = new Dumper(mLogger, getDumpAutomataPath(tid.toString())); } try { @@ -510,7 +510,7 @@ private void refineAbstractionInternal(final AutomatonType automatonType) final boolean newMaximumReached = mCegarLoopBenchmark.reportAbstractionSize(mAbstraction.size(), mIteration); if (DUMP_BIGGEST_AUTOMATON && mIteration > 4 && newMaximumReached) { - this.writeAutomatonToFile(mAbstraction, "BiggestAutomaton"); + writeAutomatonToFile(mAbstraction, "BiggestAutomaton"); } } @@ -651,7 +651,7 @@ protected String getDumpAutomataPath(final String suffix) { protected void writeAutomatonToFile(final IAutomaton automaton, final TaskIdentifier tid) { mCegarLoopBenchmark.start(CegarLoopStatisticsDefinitions.DumpTime); - final String fullAutomataPath = this.getDumpAutomataPath(tid.toString()); + final String fullAutomataPath = getDumpAutomataPath(tid.toString()); new AutomatonDefinitionPrinter(new AutomataLibraryServices(getServices()), determineAutomatonName(automaton), fullAutomataPath, mDumpAutomataFormat, "", automaton); mCegarLoopBenchmark.stop(CegarLoopStatisticsDefinitions.DumpTime); @@ -659,24 +659,24 @@ protected void writeAutomatonToFile(final IAutomaton automaton, f protected void writeAutomatonToFile(final IAutomaton automaton, final String suffix) { final TaskIdentifier tid = new SubtaskStringIdentifier(null, suffix); - this.writeAutomatonToFile(automaton, tid); + writeAutomatonToFile(automaton, tid); } protected void writeAutomatonToFile(final IAutomaton automaton, final int iteration) { final TaskIdentifier tid = new SubtaskIterationIdentifier(null, iteration); - this.writeAutomatonToFile(automaton, tid); + writeAutomatonToFile(automaton, tid); } protected void writeAutomatonToFile(final IAutomaton automaton, final int iteration, final String suffix) { final TaskIdentifier tid = new SubtaskStringIdentifier(new SubtaskIterationIdentifier(null, iteration), suffix); - this.writeAutomatonToFile(automaton, tid); + writeAutomatonToFile(automaton, tid); } protected void writeAutomataToFile(final TaskIdentifier tid, final String atsHeaderMessage, final String atsCommands, final NamedAutomaton... automata) { mCegarLoopBenchmark.start(CegarLoopStatisticsDefinitions.DumpTime); - final String fullAutomataPath = this.getDumpAutomataPath(tid.toString()); + final String fullAutomataPath = getDumpAutomataPath(tid.toString()); AutomatonDefinitionPrinter.writeAutomatonToFile(new AutomataLibraryServices(getServices()), fullAutomataPath, mDumpAutomataFormat, atsHeaderMessage, atsCommands, automata); mCegarLoopBenchmark.stop(CegarLoopStatisticsDefinitions.DumpTime); @@ -685,7 +685,7 @@ protected void writeAutomataToFile(final TaskIdentifier tid, final String atsHea protected void writeAutomataToFile(final int iteration, final String suffix, final String atsHeaderMessage, final String atsCommands, final NamedAutomaton... automata) { final TaskIdentifier tid = new SubtaskStringIdentifier(new SubtaskIterationIdentifier(null, iteration), suffix); - this.writeAutomataToFile(tid, atsHeaderMessage, atsCommands, automata); + writeAutomataToFile(tid, atsHeaderMessage, atsCommands, automata); } private String determineAutomatonName(final IAutomaton automaton) { diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/BasicCegarLoop.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/BasicCegarLoop.java index 4ab84dd6a44..b7b4234cb95 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/BasicCegarLoop.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/BasicCegarLoop.java @@ -378,7 +378,7 @@ protected void constructInterpolantAutomaton() throws AutomataOperationCanceledE mInterpolAutomaton = mRefinementResult.getInfeasibilityProof(); if (mPref.dumpAutomata()) { - super.writeAutomatonToFile(mInterpolAutomaton, getIteration(), "RawFloydHoareAutomaton"); + writeAutomatonToFile(mInterpolAutomaton, getIteration(), "RawFloydHoareAutomaton"); } assert isInterpolantAutomatonOfSingleStateType(mInterpolAutomaton); diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/EagerReuseCegarLoop.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/EagerReuseCegarLoop.java index 32f72572adc..164510f6075 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/EagerReuseCegarLoop.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/EagerReuseCegarLoop.java @@ -119,7 +119,7 @@ private void computeDifferenceForReuseAutomaton(final int iteration, final int oneBasedi = iteration + 1; if (mPref.dumpAutomata()) { - super.writeAutomatonToFile(reuseAut, "ReusedAutomata" + oneBasedi); + writeAutomatonToFile(reuseAut, "ReusedAutomata" + oneBasedi); } if (reuseAut instanceof AbstractInterpolantAutomaton) { diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/IncrementalInclusionCegarLoop.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/IncrementalInclusionCegarLoop.java index 5dc6d679a07..9ac611baf5e 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/IncrementalInclusionCegarLoop.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/IncrementalInclusionCegarLoop.java @@ -231,7 +231,7 @@ protected boolean refineAbstraction() throws AutomataLibraryException { } if (mPref.dumpAutomata()) { for (int i = 0; i < mInterpolantAutomata.size(); i++) { - super.writeAutomatonToFile(mInterpolantAutomata.get(i), getIteration(), "InterpolantAutomaton" + i); + writeAutomatonToFile(mInterpolantAutomata.get(i), getIteration(), "InterpolantAutomaton" + i); } } } finally { @@ -253,7 +253,7 @@ private void switchAllInterpolantAutomataToReadOnlyMode() { } if (mPref.dumpAutomata()) { for (final AbstractInterpolantAutomaton element : mInterpolantAutomata) { - super.writeAutomatonToFile(element, getIteration(), "EnhancedInterpolantAutomaton"); + writeAutomatonToFile(element, getIteration(), "EnhancedInterpolantAutomaton"); } } } diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/NwaCegarLoop.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/NwaCegarLoop.java index b3e4358b56a..0aae2e242a0 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/NwaCegarLoop.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/NwaCegarLoop.java @@ -393,7 +393,7 @@ private void computeAutomataDifference(final INestedWordAutomaton } if (mPref.dumpAutomata()) { - super.writeAutomatonToFile(subtrahend, getIteration(), "AbstractionAfterDifference"); + writeAutomatonToFile(subtrahend, getIteration(), "AbstractionAfterDifference"); } dumpOrAppendAutomatonForReuseIfEnabled(subtrahend, predicateUnifier); @@ -413,7 +413,7 @@ private void computeAutomataDifference(final INestedWordAutomaton } mAbstraction = diff.getResult(); if (mPref.dumpAutomata()) { - super.writeAutomatonToFile(mAbstraction, getIteration(), "AbstractionAfterDifferenceAndDeadEndRemoval"); + writeAutomatonToFile(mAbstraction, getIteration(), "AbstractionAfterDifferenceAndDeadEndRemoval"); } } finally { diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/concurrency/CegarLoopForPetriNet.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/concurrency/CegarLoopForPetriNet.java index 1275b6fdb17..200da708ac0 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/concurrency/CegarLoopForPetriNet.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/concurrency/CegarLoopForPetriNet.java @@ -80,7 +80,6 @@ import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.IPredicate; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.IPredicateCoverageChecker; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.PredicateFactory; -import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.taskidentifier.SubtaskIterationIdentifier; import de.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.ILooperCheck; import de.uni_freiburg.informatik.ultimate.logic.Script.LBool; import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.BasicCegarLoop; @@ -232,7 +231,7 @@ protected boolean refineAbstraction() throws AutomataLibraryException { } if (mPref.dumpAutomata()) { - super.writeAutomatonToFile(enhancementResult.getSecond().getResult(), getIteration(), + writeAutomatonToFile(enhancementResult.getSecond().getResult(), getIteration(), "AbstractionAfterDifferencePairwiseOnDemand"); } @@ -270,9 +269,7 @@ protected boolean refineAbstraction() throws AutomataLibraryException { } if (mPref.dumpAutomata()) { - final String filename = - new SubtaskIterationIdentifier(mTaskIdentifier, getIteration()) + "_AbstractionAfterDifference"; - super.writeAutomatonToFile(mAbstraction, filename); + writeAutomatonToFile(mAbstraction, getIteration(), "AbstractionAfterDifference"); } mLogger.info(mProgramPointPlaces.size() + " programPoint places, " @@ -284,9 +281,7 @@ protected boolean refineAbstraction() throws AutomataLibraryException { mCegarLoopBenchmark.addAutomataMinimizationData(minimizationResult.getSecond()); if (mPref.dumpAutomata() || minimizationResult.getThird() > DEBUG_DUMP_REMOVEUNREACHABLEINPUT_THRESHOLD * 1_000_000_000L) { - final String filename = new SubtaskIterationIdentifier(mTaskIdentifier, getIteration()) - + "_AbstractionBeforeRemoveDead"; - super.writeAutomatonToFile(mAbstraction, filename); + writeAutomatonToFile(mAbstraction, getIteration(), "AbstractionBeforeRemoveDead"); } mAbstraction = minimizationResult.getFirst(); } @@ -296,9 +291,7 @@ protected boolean refineAbstraction() throws AutomataLibraryException { mCegarLoopBenchmark.addAutomataMinimizationData(minimizationResult.getSecond()); if (mPref.dumpAutomata() || minimizationResult.getThird() > DEBUG_DUMP_REMOVEUNREACHABLEINPUT_THRESHOLD * 1_000_000_000L) { - final String filename = new SubtaskIterationIdentifier(mTaskIdentifier, getIteration()) - + "_AbstractionBeforeRemoveRedundantFlow"; - super.writeAutomatonToFile(mAbstraction, filename); + writeAutomatonToFile(mAbstraction, getIteration(), "AbstractionBeforeRemoveRedundantFlow"); } mAbstraction = minimizationResult.getFirst(); } @@ -383,8 +376,7 @@ protected boolean refineAbstraction() throws AutomataLibraryException { mArtifactAutomaton = mAbstraction; } if (mPref.dumpAutomata()) { - final String filename = "Abstraction" + getIteration(); - writeAutomatonToFile(mAbstraction, filename); + writeAutomatonToFile(mAbstraction, getIteration()); } return true; } @@ -487,8 +479,8 @@ protected boolean refineAbstraction() throws AutomataLibraryException { if (end - start > DEBUG_DUMP_DRYRUNRESULT_THRESHOLD * 1_000_000_000L) { final String atsHeaderMessage = "inputs of difference operation in iteration " + getIteration(); final String atsCode = "PetriNet diff = differencePairwiseOnDemand(net, nwa);"; - super.writeAutomataToFile(getIteration(), "DifferencePairwiseOnDemandInput", atsHeaderMessage, - atsCode, new NamedAutomaton<>("net", mAbstraction), new NamedAutomaton<>("nwa", dia)); + writeAutomataToFile(getIteration(), "DifferencePairwiseOnDemandInput", atsHeaderMessage, atsCode, + new NamedAutomaton<>("net", mAbstraction), new NamedAutomaton<>("nwa", dia)); } } else { dpod = null; @@ -505,7 +497,7 @@ protected boolean refineAbstraction() throws AutomataLibraryException { .getTransitionDensity(SymbolType.INTERNAL); mLogger.info("DFA transition density " + dfaTransitionDensity); if (mPref.dumpAutomata()) { - super.writeAutomatonToFile(dia, getIteration(), "EagerFloydHoareAutomaton"); + writeAutomatonToFile(dia, getIteration(), "EagerFloydHoareAutomaton"); } break; default: diff --git a/trunk/source/TraceAbstractionWithAFAs/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstractionwithafas/TAwAFAsCegarLoop.java b/trunk/source/TraceAbstractionWithAFAs/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstractionwithafas/TAwAFAsCegarLoop.java index be0ebcfcc80..329b368af31 100644 --- a/trunk/source/TraceAbstractionWithAFAs/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstractionwithafas/TAwAFAsCegarLoop.java +++ b/trunk/source/TraceAbstractionWithAFAs/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstractionwithafas/TAwAFAsCegarLoop.java @@ -573,7 +573,7 @@ protected boolean refineAbstraction() throws AutomataLibraryException { // copie mAbstraction = diff.getResult(); // mDeadEndRemovalTime = diff.getDeadEndRemovalTime(); if (mPref.dumpAutomata()) { - super.writeAutomatonToFile(mInterpolAutomaton, getIteration()); + writeAutomatonToFile(mInterpolAutomaton, getIteration()); } mCegarLoopBenchmark.stop(CegarLoopStatisticsDefinitions.AutomataDifference.toString()); From bc73632e77ee21bbb01cc59a77df8dd8fe60127f Mon Sep 17 00:00:00 2001 From: Manuel Bentele Date: Sun, 21 Jun 2026 16:43:45 +0200 Subject: [PATCH 3/3] Remove obsolete and unused CEGAR debug file dumper The file dumper misused the automata dump settings to write CEGAR debug information to a text file. Since this is no longer needed, this change remove the obsolete dumper. --- .../traceabstraction/AbstractCegarLoop.java | 15 -- .../generator/traceabstraction/Dumper.java | 171 ------------------ .../traceabstraction/NwaCegarLoop.java | 5 - .../concurrency/CegarLoopForPetriNet.java | 5 - 4 files changed, 196 deletions(-) delete mode 100644 trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/Dumper.java diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/AbstractCegarLoop.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/AbstractCegarLoop.java index 1688f49b717..73f4a585c79 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/AbstractCegarLoop.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/AbstractCegarLoop.java @@ -183,8 +183,6 @@ public abstract class AbstractCegarLoop, A extends protected final TaskIdentifier mTaskIdentifier; - protected Dumper mDumper; - /** * Unique mName of this CEGAR loop to distinguish this instance from other instances in a complex verification task. * Important only for debugging and debugging output written to files. @@ -355,11 +353,6 @@ private final CegarLoopResult startCegar() { mLogger.info("Settings: %s", ReflectionUtil.instanceFieldsToString(mPref)); mLogger.info("Starting to check reachability of %s error locations.", mErrorLocs.size()); } - // initialize dump of debugging output to files if necessary - if (mPref.dumpAutomata()) { - final TaskIdentifier tid = new SubtaskIterationIdentifier(null, mIteration); - mDumper = new Dumper(mLogger, getDumpAutomataPath(tid.toString())); - } try { if (!computeInitialAbstraction()) { iterate(); @@ -423,14 +416,6 @@ protected void iterate() throws AutomataLibraryException { try { mCegarLoopBenchmark.announceNextIteration(); - if (mDumper != null) { - mDumper.close(); - } - if (mPref.dumpAutomata()) { - final TaskIdentifier tid = new SubtaskIterationIdentifier(null, mIteration); - mDumper = new Dumper(mLogger, getDumpAutomataPath(tid.toString())); - } - try { final Pair> isCexResult = isCounterexampleFeasible(); final AutomatonType automatonType = processFeasibilityCheckResult(isCexResult.getFirst(), diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/Dumper.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/Dumper.java deleted file mode 100644 index f1f5b4e4d68..00000000000 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/Dumper.java +++ /dev/null @@ -1,171 +0,0 @@ -/* - * Copyright (C) 2013-2015 Daniel Dietsch (dietsch@informatik.uni-freiburg.de) - * Copyright (C) 2010-2015 Matthias Heizmann (heizmann@informatik.uni-freiburg.de) - * Copyright (C) 2015 University of Freiburg - * - * This file is part of the ULTIMATE TraceAbstraction plug-in. - * - * The ULTIMATE TraceAbstraction plug-in is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as published - * by the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * The ULTIMATE TraceAbstraction plug-in is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU Lesser General Public License for more details. - * - * You should have received a copy of the GNU Lesser General Public License - * along with the ULTIMATE TraceAbstraction plug-in. If not, see . - * - * Additional permission under GNU GPL version 3 section 7: - * If you modify the ULTIMATE TraceAbstraction plug-in, or any covered work, by linking - * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), - * containing parts covered by the terms of the Eclipse Public License, the - * licensors of the ULTIMATE TraceAbstraction plug-in grant you additional permission - * to convey the resulting work. - */ -package de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction; - -import java.io.File; -import java.io.FileWriter; -import java.io.IOException; -import java.io.PrintWriter; -import java.util.Collection; -import java.util.List; - -import de.uni_freiburg.informatik.ultimate.automata.IRun; -import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedRun; -import de.uni_freiburg.informatik.ultimate.automata.nestedword.NestedWord; -import de.uni_freiburg.informatik.ultimate.core.lib.exceptions.ToolchainExceptionWrapper; -import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger; -import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.IPredicate; -import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.ISLPredicate; -import de.uni_freiburg.informatik.ultimate.logic.FormulaUnLet; -import de.uni_freiburg.informatik.ultimate.logic.Script; -import de.uni_freiburg.informatik.ultimate.logic.Script.LBool; -import de.uni_freiburg.informatik.ultimate.logic.Term; -import de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder.cfg.BoogieIcfgLocation; -import de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder.cfg.CodeBlock; -import de.uni_freiburg.informatik.ultimate.util.CoreUtil; - -public final class Dumper implements AutoCloseable { - private final PrintWriter mIterationPW; - private final ILogger mLogger; - - Dumper(final ILogger logger, final String path) { - final File file = new File(path + ".txt"); - try { - mIterationPW = new PrintWriter(new FileWriter(file)); - } catch (final IOException e) { - throw new ToolchainExceptionWrapper(Activator.PLUGIN_ID, e); - } - mLogger = logger; - } - - @Override - public void close() { - if (mIterationPW != null) { - mIterationPW.close(); - } - } - - @SuppressWarnings("unused") - private void dumpSsa(final Term[] ssa) { - final FormulaUnLet unflet = new FormulaUnLet(); - try { - mIterationPW.println("===============SSA of potential Counterexample=========="); - for (int i = 0; i < ssa.length; i++) { - mIterationPW.println("UnFletedTerm" + i + ": " + unflet.unlet(ssa[i])); - } - mIterationPW.println(""); - mIterationPW.println(""); - } finally { - mIterationPW.flush(); - } - } - - @SuppressWarnings("unused") - private void dumpStateFormulas(final IPredicate[] interpolants) { - try { - mIterationPW.println("===============Interpolated StateFormulas=========="); - for (int i = 0; i < interpolants.length; i++) { - mIterationPW.println("Interpolant" + i + ": " + interpolants[i]); - } - mIterationPW.println(""); - mIterationPW.println(""); - } finally { - mIterationPW.flush(); - } - } - - public void dumpNestedRun(final IRun run) { - if (run == null || !(run instanceof NestedRun)) { - return; - } - - final List stateSequence = ((NestedRun) run).getStateSequence(); - final NestedWord counterexample = NestedWord.nestedWord(((IRun) run).getWord()); - String line; - int indentation = 0; - try { - line = "===============Run of potential Counterexample=========="; - mIterationPW.println(line); - for (int i = 0; i < counterexample.length(); i++) { - - if (run instanceof NestedRun) { - line = CoreUtil.addIndentation(indentation, - "Location" + i + ": " + ((ISLPredicate) stateSequence.get(i)).getProgramPoint()); - if (mLogger.isDebugEnabled()) { - mLogger.debug(line); - } - mIterationPW.println(line); - } - - if (counterexample.isCallPosition(i)) { - indentation++; - } - line = CoreUtil.addIndentation(indentation, - "Statement" + i + ": " + counterexample.getSymbol(i).getPrettyPrintedStatements()); - if (mLogger.isDebugEnabled()) { - mLogger.debug(line); - } - mIterationPW.println(line); - if (counterexample.isReturnPosition(i)) { - indentation--; - } - } - mIterationPW.println("ErrorLocation"); - mIterationPW.println(""); - mIterationPW.println(""); - } finally { - mIterationPW.flush(); - } - } - - void dumpBackedges(final BoogieIcfgLocation repLocName, final int position, final IPredicate state, - final Collection linPredStates, final CodeBlock transition, final IPredicate succState, - final IPredicate sf1, final IPredicate sf2, final LBool result, final int iteration, final int satProblem) { - try { - mIterationPW.println(repLocName + " occured once again at position " + position + ". Added backedge"); - mIterationPW.println("from: " + state); - mIterationPW.println("labeled with: " + transition.getPrettyPrintedStatements()); - mIterationPW.println("to: " + succState); - if (linPredStates != null) { - mIterationPW.println("for each linPredStates: " + linPredStates); - } - if (satProblem == -1) { - mIterationPW.println("because "); - } else { - assert result == Script.LBool.UNSAT; - mIterationPW.println("because Iteration" + iteration + "_SatProblem" + satProblem + " says:"); - } - mIterationPW.println(" " + sf1); - mIterationPW.println("implies"); - mIterationPW.println(" " + sf2); - mIterationPW.println(""); - } finally { - mIterationPW.flush(); - } - } -} diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/NwaCegarLoop.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/NwaCegarLoop.java index 0aae2e242a0..9a05ad8adae 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/NwaCegarLoop.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/NwaCegarLoop.java @@ -190,11 +190,6 @@ protected boolean isAbstractionEmpty() throws AutomataOperationCanceledException return true; } - if (mPref.dumpAutomata()) { - mCegarLoopBenchmark.start(CegarLoopStatisticsDefinitions.DumpTime); - mDumper.dumpNestedRun(mCounterexample); - mCegarLoopBenchmark.stop(CegarLoopStatisticsDefinitions.DumpTime); - } mLogger.info("Found error trace"); if (mLogger.isDebugEnabled()) { diff --git a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/concurrency/CegarLoopForPetriNet.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/concurrency/CegarLoopForPetriNet.java index 200da708ac0..591f8af13f4 100644 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/concurrency/CegarLoopForPetriNet.java +++ b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/concurrency/CegarLoopForPetriNet.java @@ -189,11 +189,6 @@ protected boolean isAbstractionEmpty() throws AutomataOperationCanceledException if (mCounterexample == null) { return true; } - if (mPref.dumpAutomata()) { - mCegarLoopBenchmark.start(CegarLoopStatisticsDefinitions.DumpTime); - mDumper.dumpNestedRun(mCounterexample); - mCegarLoopBenchmark.stop(CegarLoopStatisticsDefinitions.DumpTime); - } mLogger.info("Found error trace"); if (mLogger.isDebugEnabled()) {