Refine settings for improved dumping of automata to files

trunk/source/BuchiAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/buchiautomizer/cegar/AbstractBuchiCegarLoop.java

@@ -317,8 +317,8 @@ public final BuchiCegarLoopResult<L> 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<L> 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<L> 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<L> 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();

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 <http://www.gnu.org/licenses/>.
+ *
+ * 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;
+	}
+
+}

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();
 		}
 	}
 

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<L extends IIcfgTransition<?>, A extends
 	// used for debugging only
 	protected IAutomaton<L, IPredicate> 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,16 +216,18 @@ 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;
 		mCsToolkit = csToolkit;
 		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<L> 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<L> performLimitReachedActions(final IRunningTaskStackPro
 		return mResultBuilder.addResultForAllRemaining(res, null, e, null).getResult();
 	}
 
-	protected void writeAutomatonToFile(final IAutomaton<L, IPredicate> 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<L, IPredicate> automaton, final TaskIdentifier tid) {
 		mCegarLoopBenchmark.start(CegarLoopStatisticsDefinitions.DumpTime);
+		final String fullAutomataPath = this.getDumpAutomataPath(tid.toString());
 		new AutomatonDefinitionPrinter<String, String>(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<L, IPredicate>... automata) {
+	protected void writeAutomatonToFile(final IAutomaton<L, IPredicate> automaton, final String suffix) {
+		final TaskIdentifier tid = new SubtaskStringIdentifier(null, suffix);
+		this.writeAutomatonToFile(automaton, tid);
+	}
+
+	protected void writeAutomatonToFile(final IAutomaton<L, IPredicate> automaton, final int iteration) {
+		final TaskIdentifier tid = new SubtaskIterationIdentifier(null, iteration);
+		this.writeAutomatonToFile(automaton, tid);
+	}
+
+	protected void writeAutomatonToFile(final IAutomaton<L, IPredicate> 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<L, IPredicate>... 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<L, IPredicate>... automata) {
+		final TaskIdentifier tid = new SubtaskStringIdentifier(new SubtaskIterationIdentifier(null, iteration), suffix);
+		this.writeAutomataToFile(tid, atsHeaderMessage, atsCommands, automata);
+	}
+
 	private String determineAutomatonName(final IAutomaton<L, IPredicate> automaton) {
 		String result;
 		if (automaton instanceof INwaBasis) {

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<L, IPredicate> printedAutomaton;
 			final AutomataLibraryServices services = new AutomataLibraryServices(getServices());
 			final boolean addPredicateImplicationInformation = true;
@@ -526,9 +523,9 @@ protected void dumpOrAppendAutomatonForReuseIfEnabled(
 			} else {
 				printedAutomaton = automaton;
 			}
-			new AutomatonDefinitionPrinter<String, String>(services, "nwa" + getIteration(),
-					mPref.dumpPath() + File.separator + filename, mPrintAutomataLabeling, "", !mFirstReuseDump,
-					printedAutomaton);
+			final String fullAutomataPath = getDumpAutomataPath(new SubtaskStringIdentifier(null, "reuse").toString());
+			new AutomatonDefinitionPrinter<String, String>(services, "nwa" + getIteration(), fullAutomataPath,
+					mDumpAutomataFormat, "", !mFirstReuseDump, printedAutomaton);
 			mFirstReuseDump = false;
 			mLogger.info("Finished dumping");
 			mCegarLoopBenchmark.stop(CegarLoopStatisticsDefinitions.DumpTime);

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) {

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<L, IPredicate> diff =
-				new Difference<>(new AutomataLibraryServices(getServices()), mStateFactoryForRefinement,
-						(INwaOutgoingLetterAndTransitionProvider<L, IPredicate>) mAbstraction, reuseAut, psd,
-						explointSigmaStarConcatOfIA);
+				new Difference<>(new AutomataLibraryServices(getServices()), mStateFactoryForRefinement, mAbstraction,
+						reuseAut, psd, explointSigmaStarConcatOfIA);
 
 		if (reuseAut instanceof AbstractInterpolantAutomaton) {
 			final AbstractInterpolantAutomaton<L> aiReuseAut = (AbstractInterpolantAutomaton<L>) 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);