formatSupplier) {
mFormatSupplier = formatSupplier;
}
public IFormat getFormat() {
return mFormatSupplier.get();
}
}
private final AutomataLibraryServices mServices;
private final ILogger mLogger;
/**
* Base constructor.
*
* @param services
* Ultimate services
*/
private AutomatonDefinitionPrinter(final AutomataLibraryServices services) {
mServices = services;
mLogger = mServices.getLoggingService().getLogger(LibraryIdentifiers.PLUGIN_ID);
}
/**
* Constructor for printing multiple {@link IAutomaton} objects to a file.
*
* @param services
* Ultimate services
* @param automatonName
* automaton name
* @param fileName
* file name
* @param format
* output format
* @param message
* message
* @param automata
* sequence of automata to print
* @param append
* whether the automata should be added at the end of the file (true) or replace the content of the file
* (false)
*/
public AutomatonDefinitionPrinter(final AutomataLibraryServices services, final String automatonName,
final String fileName, final IFormat format, final String message, final boolean append,
final IAutomaton... automata) {
this(services);
final FileWriter fileWriter = getFileWriterWithOptionalAppend(fileName, format, append);
if (fileWriter != null) {
if (mLogger.isWarnEnabled()) {
mLogger.warn(String.format("Dumping automata %s to %s", automatonName, fileName));
}
final PrintWriter printWriter = new PrintWriter(fileWriter);
printAutomataToFileWriter(mServices, printWriter, automatonName, format, message, automata);
}
}
public AutomatonDefinitionPrinter(final AutomataLibraryServices services, final String automatonName,
final String fileName, final Format format, final String message, final boolean append,
final IAutomaton... automata) {
this(services, automatonName, fileName, format.getFormat(), message, append, automata);
}
public AutomatonDefinitionPrinter(final AutomataLibraryServices services, final String automatonName,
final String fileName, final IFormat format, final String message, final IAutomaton... automata) {
this(services, automatonName, fileName, format, message, false, automata);
}
public AutomatonDefinitionPrinter(final AutomataLibraryServices services, final String automatonName,
final String fileName, final Format format, final String message, final IAutomaton... automata) {
this(services, automatonName, fileName, format.getFormat(), message, automata);
}
public static String toString(final AutomataLibraryServices services, final String automatonName,
final IAutomaton automaton) {
final StringWriter stringWriter = new StringWriter();
final PrintWriter printWriter = new PrintWriter(stringWriter);
printAutomaton(services, new NamedAutomaton<>(automatonName, automaton), Format.ATS.getFormat(), printWriter);
return stringWriter.toString();
}
public static void writeAutomatonToFile(final AutomataLibraryServices services, final String fileName,
final Format format, final String atsHeaderMessage, final String atsCommands,
final NamedAutomaton... nas) {
writeAutomatonToFile(services, fileName, format.getFormat(), atsHeaderMessage, atsCommands, nas);
}
public static void writeAutomatonToFile(final AutomataLibraryServices services, final String fileName,
final IFormat format, final String atsHeaderMessage, final String atsCommands,
final NamedAutomaton... nas) {
final File file = new File(fileName + '.' + format.getFileEnding());
final FileWriter fileWriter;
try {
fileWriter = new FileWriter(file);
} catch (final IOException e) {
throw new AssertionError("Unable to create file writer for " + fileName);
}
try (final PrintWriter printWriter = new PrintWriter(fileWriter)) {
format.printHeader(printWriter, atsHeaderMessage);
printWriter.println();
printWriter.println(atsCommands);
printWriter.println();
for (final NamedAutomaton na : nas) {
printAutomaton(services, na, format, printWriter);
}
} finally {
try {
fileWriter.close();
} catch (final IOException e) {
throw new AssertionError("failed to close file writer");
}
}
}
/**
* Writes the passed {@link IAutomaton} objects to files if the option is enabled. Does nothing otherwise.
*
* This method is intended to be used for dumping automata when an error occurs e.g., when the
* {@link IOperation#checkResult()} method fails.
*
* @param services
* Ultimate services
* @param fileNamePrefix
* prefix of the file name (e.g., operation name)
* @param message
* message to be printed in the file
* @param automata
* sequence of automata to be printed
*/
@SafeVarargs
@SuppressWarnings({ "findbugs:UC_USELESS_VOID_METHOD" })
public static void writeToFileIfPreferred(final AutomataLibraryServices services, final String fileNamePrefix,
final String message, final IAutomaton... automata) {
if (!DUMP_AUTOMATON) {
return;
}
final String workingDirectory = System.getProperty("user.dir");
final String fileName = workingDirectory + File.separator + fileNamePrefix + getDateTimeFileName();
new AutomatonDefinitionPrinter<>(services, fileNamePrefix, fileName, Format.ATS_NUMERATE, message, automata);
}
/**
* @param append
*
*/
private FileWriter getFileWriterWithOptionalAppend(final String fileName, final IFormat format,
final boolean append) {
final File testfile = new File(fileName + '.' + format.getFileEnding());
try {
return new FileWriter(testfile, append);
} catch (final IOException e) {
if (mLogger.isErrorEnabled()) {
mLogger.error("Creating FileWriter did not work.", e);
}
return null;
}
}
/**
* Date/time string used for file names (no special characters).
*
* @return date/time string
*/
private static String getDateTimeFileName() {
return getDateTimeFromFormat("yyyyMMddHHmmss");
}
static String getDateTimeFromFormat(final String format) {
final DateFormat dateFormat = new SimpleDateFormat(format, Locale.ENGLISH);
final Date date = new Date();
return dateFormat.format(date);
}
private static void printAutomataToFileWriter(final AutomataLibraryServices services, final PrintWriter printWriter,
final String automatonName, final IFormat format, final String atsHeaderMessage,
final IAutomaton... automata) {
format.printHeader(printWriter, atsHeaderMessage);
if (automata.length == ONE) {
printAutomaton(services, new NamedAutomaton<>(automatonName, automata[0]), format, printWriter);
} else {
for (int i = 0; i < automata.length; i++) {
printAutomaton(services, new NamedAutomaton<>(automatonName + i, automata[i]), format, printWriter);
}
}
printWriter.close();
}
/**
* Determines the input automaton type and calls the respective print method.
*
* @param services
*
* @param name
* name of the automaton in the output
* @param automaton
* automaton object
* @param format
* output format
* @param printWriter
*/
private static void printAutomaton(final AutomataLibraryServices services,
final NamedAutomaton na, final IFormat format, final PrintWriter printWriter) {
if (na.getAutomaton() instanceof INwaOutgoingLetterAndTransitionProvider) {
printNestedWordAutomaton(services, na.getName(),
(INwaOutgoingLetterAndTransitionProvider) na.getAutomaton(), format, printWriter);
} else if (na.getAutomaton() instanceof IPetriNet) {
printPetriNet(na.getName(), (IPetriNet) na.getAutomaton(), format, printWriter);
} else if (na.getAutomaton() instanceof AlternatingAutomaton) {
format.printAlternatingAutomaton(printWriter, na.getName(),
(AlternatingAutomaton) na.getAutomaton());
} else if (na.getAutomaton() instanceof TreeAutomatonBU) {
format.printTreeAutomaton(printWriter, na.getName(), (TreeAutomatonBU) na.getAutomaton());
} else if (na.getAutomaton() instanceof BranchingProcess) {
format.printBranchingProcess(printWriter, na.getName(),
(BranchingProcess) na.getAutomaton());
} else if (na.getAutomaton() instanceof CountingAutomaton) {
format.printCountingAutomaton(printWriter, na.getName(),
(CountingAutomaton) na.getAutomaton());
} else if (na.getAutomaton() instanceof CountingAutomatonDataStructure) {
format.printCountingAutomatonDataStructure(printWriter, na.getName(),
(CountingAutomatonDataStructure) na.getAutomaton());
} else {
throw new AssertionError("unknown kind of automaton");
}
}
private static void printNestedWordAutomaton(final AutomataLibraryServices services,
final String name, final INwaOutgoingLetterAndTransitionProvider automaton,
final IFormat format, final PrintWriter printWriter) throws AssertionError {
INestedWordAutomaton nwa;
if (automaton instanceof INestedWordAutomaton) {
nwa = (INestedWordAutomaton) automaton;
} else {
try {
nwa = new NestedWordAutomatonReachableStates<>(services, automaton);
} catch (final AutomataOperationCanceledException e) {
throw new AssertionError("Timeout while preparing automaton for printing.");
}
}
format.printNestedWordAutomaton(printWriter, name, nwa);
}
private static void printPetriNet(final String name, final IPetriNet net,
final IFormat format, final PrintWriter printWriter) throws AssertionError {
if (!(net instanceof BoundedPetriNet)) {
final String msg =
"Unknown Petri net type. Only supported type is " + BoundedPetriNet.class.getSimpleName();
throw new IllegalArgumentException(msg);
}
final BoundedPetriNet castNet = (BoundedPetriNet) net;
format.printPetriNet(printWriter, name, castNet);
}
private static void ensureNoCallReturn(final IFormat format, final INestedWordAutomaton nwa) {
if (!NestedWordAutomataUtils.isFiniteAutomaton(nwa)) {
throw new UnsupportedOperationException(
format.getClass().getSimpleName() + " does not support call transitions or return transitions");
}
}
static void failUnsupported() {
throw new AssertionError(UNSUPPORTED_LABELING);
}
public static class NamedAutomaton {
private final String mName;
private final IAutomaton mAutomaton;
public NamedAutomaton(final String name, final IAutomaton automaton) {
super();
Objects.requireNonNull(name);
Objects.requireNonNull(automaton);
mName = name;
mAutomaton = automaton;
}
public String getName() {
return mName;
}
public IAutomaton getAutomaton() {
return mAutomaton;
}
}
/**
* Defines how various kinds of automata are printed as strings.
*
* @author Dominik Klumpp (klumpp@informatik.uni-freiburg.de)
*
*/
public interface IFormat {
String getFileEnding();
default void printHeader(final PrintWriter pw, final String header) {
// do nothing
}
void printNestedWordAutomaton(final PrintWriter printWriter, final String name,
INestedWordAutomaton nwa);
default void printCountingAutomaton(final PrintWriter printWriter, final String name,
final CountingAutomaton automaton) {
failUnsupported();
}
default void printTreeAutomaton(final PrintWriter printWriter, final String name,
final TreeAutomatonBU automaton) {
failUnsupported();
}
default void printCountingAutomatonDataStructure(final PrintWriter printWriter, final String name,
final CountingAutomatonDataStructure automaton) {
failUnsupported();
}
default void printPetriNet(final PrintWriter printWriter, final String name,
final BoundedPetriNet net) {
failUnsupported();
}
default void printAlternatingAutomaton(final PrintWriter printWriter, final String name,
final AlternatingAutomaton alternating) {
failUnsupported();
}
default void printBranchingProcess(final PrintWriter printWriter, final String name,
final BranchingProcess branchingProcess) {
failUnsupported();
}
}
private static class BaFormat implements IFormat {
@Override
public String getFileEnding() {
return "ba";
}
@Override
public void printNestedWordAutomaton(final PrintWriter printWriter, final String name,
final INestedWordAutomaton nwa) {
ensureNoCallReturn(this, nwa);
new BaFormatWriter<>(printWriter, nwa);
}
}
private static class GffFormat implements IFormat {
@Override
public String getFileEnding() {
return "gff";
}
@Override
public void printNestedWordAutomaton(final PrintWriter printWriter, final String name,
final INestedWordAutomaton nwa) {
ensureNoCallReturn(this, nwa);
new GoalFormatWriter<>(printWriter, nwa);
}
}
private static class HoaFormat implements IFormat {
@Override
public String getFileEnding() {
return "hoa";
}
@Override
public void printNestedWordAutomaton(final PrintWriter printWriter, final String name,
final INestedWordAutomaton nwa) {
ensureNoCallReturn(this, nwa);
new HanoiFormatWriter<>(printWriter, nwa);
}
}
}