---

rStatus.java

package gov.nasa.arc.ase.jpf;

import gov.nasa.arc.ase.jpf.jvm.DynamicArea;
import gov.nasa.arc.ase.jpf.jvm.KernelState;
import gov.nasa.arc.ase.jpf.jvm.VirtualMachine;
import gov.nasa.arc.ase.util.Comma;
import gov.nasa.arc.ase.util.Counter;
import gov.nasa.arc.ase.util.Debug;
import gov.nasa.arc.ase.util.kMG;
import java.io.*;
import java.io.IOException;
import java.util.LinkedList;
import java.util.ListIterator;

public class rStatus {
  public int states;
  public int transitions;
  public int last_transitions;
  public long begin_time;
  public long last_time;
// ifdef DISTRIBUTED




//#endif DISTRIBUTED
  public ResultInfo results = null;
  private boolean isIdle = false;
  
  private class StatusServer extends Thread {
    public void run() {
      if(Engine.options.interactive) return;
      try {
    int t = Engine.options.report_period * 1000;
// ifdef DISTRIBUTED







//#endif DISTRIBUTED
      while(true) {
        Thread.sleep(t, 0);
        dump();
        tick();
      }
      } catch(InterruptedException e) {
      }
    }
  }

  private StatusServer ss;

// ifdef MEMORY_DUMP















// ifdef NO_COMPRESSION

//#else NO_COMPRESSION

//#endif NO_COMPRESSION


//#endif MEMORY_DUMP

  private LinkedList timers = new LinkedList();

  public rStatus() {
    begin_time = System.currentTimeMillis();
    last_time = 0;
    last_transitions = 0;
// ifdef DISTRIBUTED





//#endif DISTRIBUTED
  }  
// ifdef DISTRIBUTED











// ifdef DEBUG_DISTRIBUTED

//#endif DEBUG_DISTRIBUTED
// ifdef DEBUG

//#endif DEBUG








// ifdef DEBUG_DISTRIBUTED

//#endif DEBUG_DISTRIBUTED
// ifdef DEBUG

//#endif DEBUG











// ifdef DEBUG_DISTRIBUTED

//#endif DEBUG_DISTRIBUTED



















//#endif DISTRIBUTED

  public void decrStates() {
    states--;
  }  
  public void decrTransitions() {
    transitions--;
  }  
  public void dump() {
    if (Engine.options.verify) {
// ifdef DISTRIBUTED





//#endif DISTRIBUTED
      Runtime rt = Runtime.getRuntime();
      Runner.used_memory = rt.totalMemory() - rt.freeMemory();
      Debug.println(Debug.WARNING, Comma.format(states) + 
      " tr " + Comma.format(transitions) + 
      " sd " + Comma.format(Runner.max_stack_depth) + 
      gov.nasa.arc.ase.jpf.jvm.VirtualMachine.getStatus() + 
      " mem " + 
      kMG.format(Runner.used_memory) +
      " ela " + elapsed());
    } else
      Debug.println(Debug.WARNING, "States = " + Comma.format(states));
  }  
  public String elapsed() {
    long e = System.currentTimeMillis() - begin_time;
    long s = (e / 1000) % 60;
    long m = e / 60000;
    long spd = 0;
    if (e != last_time)
      spd = ResultInfo.speed(transitions - last_transitions, e - last_time);
    last_time = e;
    last_transitions = transitions;

    if (s < 10)
      return m + ":0" + s + " spd " + Comma.format(spd) + "t/s";
    else
      return m + ":" + s + " spd " + Comma.format(spd) + "t/s";
  }  
  public void generateResults() {
    results = new ResultInfo(this);
  }  
  public int getStates() {
    return states;
  }  
  public int getTransitions() {
    return transitions;
  }  
  public void incrStates(int depth) {
    states++;
// ifdef MEMORY_DUMP

//#endif MEMORY_DUMP
  }  
  public void incrTransitions(int depth) {
    transitions++;
// ifdef MEMORY_DUMP

//#endif MEMORY_DUMP
  }  
  public void print(String message) {
    long time_end = System.currentTimeMillis();
// ifdef DISTRIBUTED

//#endif DISTRIBUTED

    if(results == null) generateResults();
    results.print(message);
// ifdef DEBUG_DISTRIBUTED


















//#endif DEBUG_DISTRIBUTED
  }  
  public void registerTimer(Timer t) {
    timers.addLast(t);
  }  
  public void start() {
    ss = new StatusServer();
    ss.start();
  }  
  public void stop() {
    ss.interrupt();
  }  
  public void tick() {
    for(ListIterator i = timers.listIterator(); i.hasNext(); ) {
      Timer t = (Timer)i.next();

      t.tick();
    }
  }  
}

---