content: /* Alloy Analyzer 4 -- Copyright (c) 2006-2009, Felix Chang
   *
   * Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files
   * (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify,
   * merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
   * furnished to do so, subject to the following conditions:
   *
   * The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
   *
   * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
   * OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
   * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF
   * OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
   */
  
  package edu.mit.csail.sdg.alloy4viz;
  
  import java.util.Collection;
  import java.util.Collections;
  import java.util.HashMap;
  import java.util.LinkedHashMap;
  import java.util.List;
  import java.util.Map;
  import java.util.Set;
  import java.util.TreeSet;
  
  import edu.mit.csail.sdg.alloy4.ConstList;
  import edu.mit.csail.sdg.alloy4.ConstList.TempList;
  
  /**
   * Immutable; represents an Alloy model.
   * <p>
   * <b>Thread Safety:</b> Can be called only by the AWT event thread.
   */
  
  public final class AlloyModel {
  
      /**
       * An unmodifiable sorted set of all types in this model.
       */
      private final Set<AlloyType>           types;
  
      /**
       * An unmodifiable sorted set of all sets in this model. <br>
       * AlloyModel's constructor guarantees that, for each set here, set.getType() is
       * in this.types
       */
      private final Set<AlloySet>            sets;
  
      /**
       * An unmodifiable sorted set of all relations in this model. <br>
       * AlloyModel's constructor guarantees that, for each relation here,
       * relation.getTypes() are in this.types
       */
      private final Set<AlloyRelation>       relations;
  
      private final Set<AlloyElement>       nonempty;
  
      /**
       * If A extends B, then "(A,B)" will be in this map.
       * <p>
       * AlloyModel's constructor ensures the following: <br>
       * (1) hierarchy.keySet() is always a subset of this.types <br>
       * (2) hierarchy.valueSet() is always a subset of this.types <br>
       * (3) "univ" is never in the keySet <br>
       * (4) null is never in the keySet nor valueSet <br>
       * (5) there is no cycle in this relation
       */
      private final Map<AlloyType,AlloyType> hierarchy;
  
      /**
       * The map from name to AlloyType. <br>
       * AlloyModel's constructor guarantees that this.name2types.values() has the
       * same entries as this.types
       */
      private final Map<String,AlloyType>    name2types = new HashMap<String,AlloyType>();
  
      /**
       * Returns true iff the nodes x, map.get(x), map.get(map.get(x))... form an
       * infinite chain of nonnull objects.
       *
       * @param map - a map from AlloyType to AlloyType
       * @param x - the AlloyType object we want to check
       */
      public static boolean isCycle(Map<AlloyType,AlloyType> map, AlloyType x) {
          int i = (-5), n = map.size();
          while (x != null) {
              x = map.get(x);
              i++;
              if (i >= n)
                  return true;
          }
          return false;
      }
  
      /**
       * Construct a new AlloyModel object.
       *
       * @param types - the types; we will always add "univ" to it if it's not there
       *            already
       * @param sets - the sets
       * @param rels - the relations
       * @param map - we consult this "sig to parent sig" map and extract the mappings
       *            relevant to this model. (If we detect a cycle, we will arbitrarily
       *            break the cycle)
       */
      public AlloyModel(Collection<AlloyType> types, Collection<AlloySet> sets, Collection<AlloyRelation> rels, Set<AlloyElement> nonempty, Map<AlloyType,AlloyType> map) {
          // The following 3 have to be tree sets, since we want to keep them
          // sorted
          Set<AlloyType> allTypes = new TreeSet<AlloyType>();
          Set<AlloySet> allSets = new TreeSet<AlloySet>();
          Set<AlloyRelation> allRelations = new TreeSet<AlloyRelation>();
          allTypes.addAll(types);
          allTypes.add(AlloyType.UNIV);
          for (AlloySet s : sets)
              if (allTypes.contains(s.getType()))
                  allSets.add(s);
          for (AlloyRelation r : rels)
              if (allTypes.containsAll(r.getTypes()))
                  allRelations.add(r);
          this.types = Collections.unmodifiableSet(allTypes);
          this.sets = Collections.unmodifiableSet(allSets);
          this.relations = Collections.unmodifiableSet(allRelations);
          this.nonempty = Collections.unmodifiableSet(nonempty);
          Map<AlloyType,AlloyType> newmap = new LinkedHashMap<AlloyType,AlloyType>();
          for (AlloyType type : allTypes) {
              AlloyType sup = isCycle(map, type) ? null : map.get(type);
              if (sup == null || !allTypes.contains(sup))
                  sup = AlloyType.UNIV;
              newmap.put(type, sup);
          }
          newmap.remove(AlloyType.UNIV); // This ensures univ is not in
                                        // hierarchy's keySet
          this.hierarchy = Collections.unmodifiableMap(newmap);
          for (AlloyType t : this.types)
              this.name2types.put(t.getName(), t);
      }
  
      /**
       * Construct a new AlloyModel object.
       *
       * @param types - the types ; we will always add "univ" to it if it's not there
       *            already
       * @param sets - the sets
       * @param rels - the relations
       * @param old - we consult this model's "sig to parent sig" map, and extract the
       *            mappings relevant to this model.
       */
      public AlloyModel(Collection<AlloyType> types, Collection<AlloySet> sets, Collection<AlloyRelation> rels, AlloyModel old) {
          this(types, sets, rels, old.nonempty, old.hierarchy);
      }
  
      /**
       * If type==univ, return null; otherwise, return a nonnull AlloyType object
       * representing its super type. <br>
       * (In particular, if "type" does not exist in this model, we'll return "univ"
       * as the answer).
       */
      public AlloyType getSuperType(AlloyType type) {
          if (type.getName().equals("univ"))
              return null;
          AlloyType answer = hierarchy.get(type);
          return answer == null ? AlloyType.UNIV : answer;
      }
  
      /**
       * If type==univ, return null; otherwise, return a nonnull AlloyType object
       * representing its topmost non-univ super type.
       * <p>
       * Thus, if "type" is in this model, but its supertype is univ, then we'll
       * return type as-is.
       * <p>
       * Note: if "type" does not exist in this model, we'll return it as-is.
       */
      public AlloyType getTopmostSuperType(AlloyType type) {
          if (type == null || type.equals(AlloyType.UNIV))
              return null;
          while (true) {
              AlloyType top = getSuperType(type);
              if (top == null || top.equals(AlloyType.UNIV))
                  break;
              type = top;
          }
          return type;
      }
  
      /**
       * Returns a sorted, unmodifiable list of types that are direct or indirect
       * subtypes of the given type. <br>
       * This method will search recursively, so if the subtypes themselves have
       * subtypes, they too are included. <br>
       * If type==null, or it does not exist in this model, or it has no subsigs, then
       * we return an empty set.
       */
      public ConstList<AlloyType> getSubTypes(AlloyType type) {
          TempList<AlloyType> subtypes = new TempList<AlloyType>();
          for (AlloyType subType : types)
              if (isSubtype(subType, type))
                  subtypes.add(subType);
          return subtypes.makeConst(); // Since this.types is sorted, the result
                                      // is already sorted.
      }
  
      /**
       * Returns a sorted, unmodifiable list of types that are direct subtypes of the
       * given type. <br>
       * This method will only return types that are direct subtypes of the given
       * argument. <br>
       * If type==null, or it does not exist in this model, or it has no subsigs, then
       * we return an empty set.
       */
      public ConstList<AlloyType> getDirectSubTypes(AlloyType type) {
          TempList<AlloyType> subtypes = new TempList<AlloyType>();
          for (AlloyType subType : types)
              if (isDirectSubtype(subType, type))
                  subtypes.add(subType);
          return subtypes.makeConst(); // Since this.types is sorted, the result
                                      // is already sorted.
      }
  
      /**
       * Returns true iff "subType" is a direct or indirect subsig of "superType".
       * <br>
       * If subType==null or superType==null, it always returns false.
       */
      public boolean isSubtype(AlloyType subType, AlloyType superType) {
          if (subType == null || superType == null || !types.contains(subType) || subType.equals(AlloyType.UNIV))
              return false;
          while (subType != null) {
              subType = getSuperType(subType); // Do this before calling equals(),
                                              // since we want
                                              // isSubtype(X,X)==false
              if (superType.equals(subType))
                  return true;
          }
          return false;
      }
  
      /**
       * Returns true iff "subType" is a direct subsig of "superType". <br>
       * If subType==null or superType==null, it always returns false.
       */
      public boolean isDirectSubtype(AlloyType subType, AlloyType superType) {
          if (subType == null || superType == null || !types.contains(subType) || subType.equals(AlloyType.UNIV))
              return false;
          if (superType.equals(AlloyType.UNIV) && hierarchy.get(subType) == null)
              return true;
          return superType.equals(hierarchy.get(subType));
      }
  
      /**
       * Returns true iff "subType" is equal to, or is a direct or indirect subsig of
       * "superType". <br>
       * If subType==null or superType==null, it always returns false.
       */
      public boolean isEqualOrSubtype(AlloyType subType, AlloyType superType) {
          if (superType == null)
              return false;
          while (subType != null) {
              if (superType.equals(subType))
                  return true;
              subType = getSuperType(subType);
          }
          return false;
      }
  
      /**
       * Two AlloyModel objects are equal if they have the same types, sets,
       * relations, and extension relationship.
       */
      @Override
      public boolean equals(Object other) {
          if (!(other instanceof AlloyModel))
              return false;
          if (other == this)
              return true;
          AlloyModel x = (AlloyModel) other;
          return types.equals(x.types) && sets.equals(x.sets) && relations.equals(x.relations) && hierarchy.equals(x.hierarchy);
      }
  
      /**
       * Compute a hashcode based on the types, sets, relations, and the extension
       * relationship.
       */
      @Override
      public int hashCode() {
          return types.hashCode() + 3 * sets.hashCode() + 5 * relations.hashCode() + 7 * hierarchy.hashCode();
      }
  
      /** Returns true if this model contains the given type. */
      public boolean hasType(AlloyType type) {
          return types.contains(type);
      }
  
      /**
       * Returns the AlloyType object if this model contains the given type; or return
       * null otherwise.
       */
      public AlloyType hasType(String name) {
          return name2types.get(name);
      }
  
      /**
       * Returns the AlloyRelation object if this model contains the given relation;
       * or return null otherwise.
       */
      public AlloySet hasSet(String name, AlloyType type) {
          for (AlloySet s : sets)
              if (s.getName().equals(name) && s.getType().equals(type))
                  return s;
          return null;
      }
  
      /**
       * Returns the AlloyRelation object if this model contains the given relation;
       * or return null otherwise.
       */
      public AlloyRelation hasRelation(String name, List<AlloyType> types) {
          for (AlloyRelation r : relations)
              if (r.getName().equals(name) && r.getTypes().equals(types))
                  return r;
          return null;
      }
  
      /**
       * Returns an unmodifiable sorted set of all AlloyType(s) in this model.
       */
      public Set<AlloyType> getTypes() {
          return types;
      }
  
      /**
       * Returns an unmodifiable sorted set of all AlloySet(s) in this model.
       */
      public Set<AlloySet> getSets() {
          return sets;
      }
  
      /**
       * Returns an unmodifiable sorted set of all AlloyRelation(s) in this model.
       */
      public Set<AlloyRelation> getRelations() {
          return relations;
      }
  
      public Set<AlloyElement> getNonEmpty() {
          return nonempty;
      }
  }
  