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..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 @@ -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,15 +171,17 @@ 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 TaskIdentifier mTaskIdentifier; + protected final String mTaskFilename; + + protected final DebugIdentifier mTaskDebugIdentifier; - protected Dumper mDumper; + protected final TaskIdentifier mTaskIdentifier; /** * Unique mName of this CEGAR loop to distinguish this instance from other instances in a complex verification task. @@ -208,7 +214,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 +222,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(); } @@ -345,10 +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()) { - mDumper = new Dumper(mLogger, mPref, mName, mIteration); - } try { if (!computeInitialAbstraction()) { iterate(); @@ -384,8 +388,7 @@ private boolean computeInitialAbstraction() throws AutomataLibraryException { mArtifactAutomaton = mAbstraction; } if (mPref.dumpAutomata()) { - final String filename = mTaskIdentifier + "_InitialAbstraction"; - writeAutomatonToFile(mAbstraction, filename); + writeAutomatonToFile(mAbstraction, "InitialAbstraction"); } mCegarLoopBenchmark.reportAbstractionSize(mAbstraction.size(), mIteration); @@ -413,13 +416,6 @@ protected void iterate() throws AutomataLibraryException { try { mCegarLoopBenchmark.announceNextIteration(); - if (mDumper != null) { - mDumper.close(); - } - if (mPref.dumpAutomata()) { - mDumper = new Dumper(mLogger, mPref, mName, mIteration); - } - try { final Pair> isCexResult = isCounterexampleFeasible(); final AutomatonType automatonType = processFeasibilityCheckResult(isCexResult.getFirst(), @@ -499,8 +495,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); + writeAutomatonToFile(mAbstraction, "BiggestAutomaton"); } } @@ -624,23 +619,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 = 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); + writeAutomatonToFile(automaton, tid); + } + + protected void writeAutomatonToFile(final IAutomaton automaton, final int iteration) { + final TaskIdentifier tid = new SubtaskIterationIdentifier(null, iteration); + 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); + 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 = 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); + 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..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 @@ -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); + 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 deleted file mode 100644 index 16bd7214ca3..00000000000 --- a/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/Dumper.java +++ /dev/null @@ -1,173 +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.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; -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.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"); - 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/EagerReuseCegarLoop.java b/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/EagerReuseCegarLoop.java index 10ad3d87d88..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 @@ -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..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,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); + 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); + 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..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 @@ -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; @@ -191,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()) { @@ -394,9 +388,7 @@ private void computeAutomataDifference(final INestedWordAutomaton } if (mPref.dumpAutomata()) { - final String filename = - new SubtaskIterationIdentifier(mTaskIdentifier, getIteration()) + "AbstractionAfterDifference"; - super.writeAutomatonToFile(subtrahend, filename); + writeAutomatonToFile(subtrahend, getIteration(), "AbstractionAfterDifference"); } dumpOrAppendAutomatonForReuseIfEnabled(subtrahend, predicateUnifier); @@ -416,9 +408,7 @@ private void computeAutomataDifference(final INestedWordAutomaton } mAbstraction = diff.getResult(); if (mPref.dumpAutomata()) { - final String filename = new SubtaskIterationIdentifier(mTaskIdentifier, getIteration()) - + "AbstractionAfterDifferenceAndDeadEndRemoval"; - super.writeAutomatonToFile(mAbstraction, filename); + 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..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 @@ -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; @@ -190,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()) { @@ -232,9 +226,8 @@ protected boolean refineAbstraction() throws AutomataLibraryException { } if (mPref.dumpAutomata()) { - final String filename = new SubtaskIterationIdentifier(mTaskIdentifier, getIteration()) - + "_AbstractionAfterDifferencePairwiseOnDemand"; - super.writeAutomatonToFile(enhancementResult.getSecond().getResult(), filename); + writeAutomatonToFile(enhancementResult.getSecond().getResult(), getIteration(), + "AbstractionAfterDifferencePairwiseOnDemand"); } if (getIteration() <= mPref.watchIteration() && mPref.artifact() == Artifact.NEG_INTERPOLANT_AUTOMATON) { @@ -271,9 +264,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, " @@ -285,9 +276,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(); } @@ -297,9 +286,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(); } @@ -384,8 +371,7 @@ protected boolean refineAbstraction() throws AutomataLibraryException { mArtifactAutomaton = mAbstraction; } if (mPref.dumpAutomata()) { - final String filename = "Abstraction" + getIteration(); - writeAutomatonToFile(mAbstraction, filename); + writeAutomatonToFile(mAbstraction, getIteration()); } return true; } @@ -486,11 +472,9 @@ 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, + writeAutomataToFile(getIteration(), "DifferencePairwiseOnDemandInput", atsHeaderMessage, atsCode, new NamedAutomaton<>("net", mAbstraction), new NamedAutomaton<>("nwa", dia)); } } else { @@ -508,9 +492,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); + 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..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,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); + writeAutomatonToFile(mInterpolAutomaton, getIteration()); } mCegarLoopBenchmark.stop(CegarLoopStatisticsDefinitions.AutomataDifference.toString());