code: /****************************************************************************
  
      ePMC - an extensible probabilistic model checker
      Copyright (C) 2017
  
      This program is free software: you can redistribute it and/or modify
      it under the terms of the GNU General Public License as published by
      the Free Software Foundation, either version 3 of the License, or
      (at your option) any later version.
  
      This program 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 General Public License for more details.
  
      You should have received a copy of the GNU General Public License
      along with this program.  If not, see <http://www.gnu.org/licenses/>.
  
   *****************************************************************************/
  
  package epmc.error;
  
  import java.io.Serializable;
  import java.util.Locale;
  import java.util.ResourceBundle;
  
  /**
   * Description of a particular problem during any phase of analysis.
   * This class is intended to describe the exact cause of an
   * {@link EPMCException}. The class is particularly meant to generate
   * (possibly localised) strings readable by end users. Using
   * {@link #getIdentifier()}, it is however also possible to obtain the exact
   * cause of an exception programmatically and e.g. replace an exception by
   * another one. The identifiers should be globally unique, that is unique
   * within the EPMC main part and all of its plugins. Thus, problem
   * description identifiers of plugins should be prefixed by the name of this
   * plugin.
   * 
   * @author Ernst Moritz Hahn
   * @see UtilError
   * @see EPMCException
   */
  public final class Problem implements Serializable {
      /** Serial version UID - 1L as I don't know any better. */
      private static final long serialVersionUID = 1L;
      /** Base name of resource bundle to read user information from. */
      private final String resourceBundle;
      /** Identifier of the problem, key in resource file to obtain user-readable text. */
      private final String name;
  
      /**
       * Construct new problem identifier.
       * The problem identifier will be given the base name of the resource bundle
       * to read its user-readable text from as well as a name, which servers as
       * they key of the message in the resource file.
       * 
       * @param resourceBundle base name of resource bundle to use
       * @param name name of problem
       */
      Problem(String resourceBundle, String name) {
          assert resourceBundle != null;
          assert name != null;
          ResourceBundle testResourceBundle = ResourceBundle.getBundle(resourceBundle,
                  Locale.getDefault(), Thread.currentThread().getContextClassLoader());
          assert testResourceBundle.containsKey(name) : name + " " + resourceBundle;
          this.resourceBundle = resourceBundle;
          this.name = name;
      }
  
      /**
       * Obtain problem identifier.
       * The string returned should be globally unique among the tool and all
       * its plugins to allow easy identification of the problem cause. This is
       * especially important in case an EPMCException shall be catched and
       * replacedd by a newly created exception, so as to avoid different causes
       * with identical identifiers being mistaken for each other.
       * 
       * @return problem identifier
       */
      public String getIdentifier() {
          return name;
      }
  
  
      /**
       * Obtain base name of resource bundle containing problem description.
       * 
       * @return base name of resource bundle of this problem
       */
      public String getResourceBundle() {
          return resourceBundle;
      }
  
      /**
       * Get the localised message string of the problem.
       * The locale parameter must not be {@code null}. The exact message
       * returned depends on the implementation of this interface. In most cases,
       * it should be sufficient to use the instances generated by
       * {@link UtilError#newProblem(String, String)}, thus please also take a
       * look at the description of this method. Note that the result of the
       * method is not the final message to be shown to the user, but a string
       * containing placeholds e.g. for the model name, etc., yet to be filled
       * out by the according arguments of a particular {@link EPMCException}
       * instance. The class loader used is provided by
       * {@link Thread#getContextClassLoader()}.
       * 
       * @param locale locale to generate localised message for
       * @return localised message
       * @see UtilError#newProblem(String, String)
       * @see EPMCException#getLocalizedMessage()
       */
      public String getMessage(Locale locale) {
          ResourceBundle messages = ResourceBundle.getBundle(this.resourceBundle,
                  locale, Thread.currentThread().getContextClassLoader());
          return messages.getString(this.name);
      }
  
      @Override
      public String toString() {
          return name;
      }
  
      @Override
      public boolean equals(Object obj) {
          assert obj != null;
          if (!(obj instanceof Problem)) {
              return false;
          }
          Problem other = (Problem) obj;
          return name.equals(other.getIdentifier());
      }
  
      @Override
      public int hashCode() {
          return name.hashCode();
      }
  }
  