// Copyright (c) 2003 Compaq Corporation.  All rights reserved.
// Portions Copyright (c) 2003 Microsoft Corporation.  All rights reserved.
// Last modified on Mon 30 Apr 2007 at 15:29:58 PST by lamport
//      modified on Tue Oct 23 16:48:38 PDT 2001 by yuanyu

package tlc2.tool;

import java.io.IOException;
import java.io.Serializable;
import java.util.Set;
import java.util.HashMap;

import tla2sany.semantic.OpDeclNode;
import tla2sany.semantic.SemanticNode;
import tla2sany.semantic.SymbolNode;
import tlc2.value.Value;
import tlc2.value.ValueInputStream;
import tlc2.value.ValueOutputStream;
import util.UniqueString;

public abstract class TLCState implements Cloneable, Serializable {
  public long uid = -1;   // Must be set to a non-negative number
  
  // Set by subclasses. Cannot set until we know what the variables are.
  public static TLCState Empty = null;

  // The state variables.
  protected static OpDeclNode[] vars = null;
  
  public static void setVariables(OpDeclNode[] variables) 
  {
      vars = variables;
      // SZ 10.04.2009: since this method is called exactly one from Spec#processSpec
      // moved the call of UniqueString#setVariables to that place
      
      // UniqueString[] varNames = new UniqueString[variables.length];
      // for (int i = 0; i < varNames.length; i++)
      // {
      //  varNames[i] = variables[i].getName();
      //}
      //UniqueString.setVariables(varNames);
  }

  public void read(ValueInputStream vis) throws IOException {
    this.uid = vis.readLongNat();
  }
  
  public void write(ValueOutputStream vos) throws IOException {
    vos.writeLongNat(this.uid);
  }

  public abstract TLCState bind(UniqueString name, Value value, SemanticNode expr);
  public abstract TLCState bind(SymbolNode id, Value value, SemanticNode expr);  
  public abstract TLCState unbind(UniqueString name);
  public abstract Value lookup(UniqueString var);
  public abstract boolean containsKey(UniqueString var);
  public abstract TLCState copy();
  public abstract TLCState deepCopy();
  public abstract StateVec addToVec(StateVec states);
  public abstract void deepNormalize();
  public abstract long fingerPrint();
  public abstract boolean allAssigned();
  public abstract Set<OpDeclNode> getUnassigned();
  public abstract TLCState createEmpty();
  
  /** 
   * Returns a mapping of variable names to their assigned values in this state.
   */ 
  public HashMap<UniqueString, Value> getVals() {
	HashMap<UniqueString, Value> valMap = new HashMap<UniqueString, Value>();
    for(int i=0;i<vars.length;i++) {
        UniqueString key = vars[i].getName();
        Value val = this.lookup(key);
        valMap.put(key, val);
    }
    return valMap;
  }
  
  /** 
   * Returns a map of all variables that are different between this state and 'otherState' along
   * with their values in 'otherState'.
   */
  public HashMap<UniqueString, Value> diff(TLCState otherState){
		HashMap<UniqueString, Value> stateVals = this.getVals();
		HashMap<UniqueString, Value> succStateVals = otherState.getVals();
		HashMap<UniqueString, Value> diffMap = new HashMap<>();
		
		for(UniqueString key : stateVals.keySet()) {
			Value valSucc = succStateVals.get(key);
			// Check if the value in the new state is different from the old state.
			if(!stateVals.get(key).equals(valSucc)) {
				diffMap.put(key, valSucc);
			}
		}
		
		return diffMap;
  }
  
  /* Returns a string representation of this state.  */
  public abstract String toString();
  public abstract String toString(TLCState lastState);
}

@@ -2713,690 +2713,8 @@
 %0A  %0A
-  /** %0A   * Returns a map of all variables that are different between this state and 'otherState' along%0A   * with their values in 'otherState'.%0A   */%0A  public HashMap%3CUniqueString, Value%3E diff(TLCState otherState)%7B%0A%09%09HashMap%3CUniqueString, Value%3E stateVals = this.getVals();%0A%09%09HashMap%3CUniqueString, Value%3E succStateVals = otherState.getVals();%0A%09%09HashMap%3CUniqueString, Value%3E diffMap = new HashMap%3C%3E();%0A%09%09%0A%09%09for(UniqueString key : stateVals.keySet()) %7B%0A%09%09%09Value valSucc = succStateVals.get(key);%0A%09%09%09// Check if the value in the new state is different from the old state.%0A%09%09%09if(!stateVals.get(key).equals(valSucc)) %7B%0A%09%09%09%09diffMap.put(key, valSucc);%0A%09%09%09%7D%0A%09%09%7D%0A%09%09%0A%09%09return diffMap;%0A  %7D%0A  %0A
   /*

Remove unused diff method