Module dev.civl.gmc
Package dev.civl.gmc

Class ErrorLog

java.lang.Object
dev.civl.gmc.ErrorLog
public class ErrorLog extends Object

A log for recording errors and corresponding traces encountered during a model checking run.

In the course of performing a search, various kinds of "errors" may be encountered. These do not necessarily pause the search. They are not even necessarily noticed by the searcher. Each application using this package is free to determine what in an error is and how to report them. Typically, an error occurs in the process of computing the enabled transitions at a state, or in the process of executing a transition. Division by zero, null pointer dereferences, and so on, are typical errors that should be logged and reported.

This class provides a convenient mechanism for logging such as errors as the search progresses. Many applications do not necessarily stop after the first error is discovered, but instead take some corrective mechanism (like constraining the path condition in symbolic execution) and proceed with the search. Those applications can use this class to record the errors encountered.

In addition to recording errors, this class provides a number of convenient services: using information provided by the application, it can determine when two errors are considered "equivalent" and therefore only one instance needs to be reported; it can prioritize the errors so that the most important are reported to the user first; it can associate a trace to each error and save these in a file, so the user can later replay the trace associate to each error discovered.

  • Constructor Details

    • ErrorLog

      public ErrorLog(File directory, String sessionName, PrintStream out)
      Creates new ErrorLog.
      Parameters:
      directory - the directory in which traces and the log file will be stored
      sessionName - the name to use for this session; it will form the root of the names of all the files created
      out - the stream to which errors should be printed when they are reported to this log

  • Method Details

    • getMinimize

      public boolean getMinimize()
      Are we searching for a minimal counterexample?
      Returns:
      value of minimize flag

    • setMinimize

      public void setMinimize(boolean value)
      Sets the minimize flag to given value. If true, each time a violation is found, the search depth will be restricted to its current depth minus one.
      Parameters:
      value - true iff we want to search for a minimal counterexample

    • getDirectory

      public File getDirectory()
      Returns the directory in which trace files and the log will be stored.
      Returns:
      the directory associated to this log

    • getLogFile

      public File getLogFile()

    • save

      public void save() throws FileNotFoundException
      Throws:
      FileNotFoundException

    • setSearcher

      public void setSearcher(DfsSearcher<?,?> searcher)

    • searcher

      public DfsSearcher<?,?> searcher()

    • errorBound

      public int errorBound()

    • setErrorBound

      public void setErrorBound(int value)

    • numErrors

      public int numErrors()

    • numEntries

      public int numEntries()

    • print

      public void print(PrintStream out)

    • report

      public void report(LogEntry entry) throws FileNotFoundException
      Throws:
      ExcessiveErrorException - if the number of errors reported has exceeded the specified bound
      FileNotFoundException

    • getIgnoreErrors

      public boolean getIgnoreErrors()

    • setIgnoreErrors

      public void setIgnoreErrors(boolean ignoreErrors)

    • getMinimalCounterexampleSize

      public int getMinimalCounterexampleSize()
      Returns the minimal size of a counterexample reported to this logger, or -1 if no counterexamples have been logged. The size is the length of the depth first search stack at the time of the log event.
      Returns:
      the minimal counterexample size