<commit_before>// 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 13:18:34 PST by lamport  
//      modified on Fri Mar  2 23:46:22 PST 2001 by yuanyu   

package tlc2.tool.distributed;

import java.rmi.RemoteException;
import java.util.Date;
import java.util.concurrent.BrokenBarrierException;
import java.util.concurrent.CyclicBarrier;

import tlc2.TLCGlobals;
import tlc2.output.EC;
import tlc2.output.MP;
import tlc2.tool.TLCState;
import tlc2.tool.TLCStateVec;
import tlc2.tool.WorkerException;
import tlc2.tool.queue.StateQueue;
import tlc2.util.BitVector;
import tlc2.util.IdThread;
import tlc2.util.LongVec;
import util.ToolIO;

/**
 * 
 * @deprecated not used currently
 * @version $Id$
 */
public class TLCServerThread extends IdThread {
	private static final String BLOCK_SIZE = "tlc2.tool.distributed.TLCServerThread.BlockSize";
	/**
	 * TLC server threads manage the set of existing TLC workers.
	 */
	private final static int BlockSize = Integer.getInteger(BLOCK_SIZE, 1024);
	private CyclicBarrier barrier;
	/**
	 * Identifies the worker
	 */
	private String url = "";
	private int receivedStates, sentStates;

	public TLCServerThread(int id, TLCWorkerRMI worker, String url, TLCServer tlc, CyclicBarrier aBarrier) {
		super(id);
		this.worker = worker;
		this.url  = url;
		this.tlcServer = tlc;
		this.barrier = aBarrier;
	}

	private TLCWorkerRMI worker;
	private TLCServer tlcServer;

	public final TLCWorkerRMI getWorker() {
		return this.worker;
	}

	public final void setWorker(TLCWorkerRMI worker) {
		this.worker = worker;
	}

	/**
	 * This method gets a state from the queue, generates all the possible next
	 * states of the state, checks the invariants, and updates the state set and
	 * state queue.
	 */
	public void run() {
		waitOnBarrier();
		
		TLCGlobals.incNumWorkers(1);
		TLCStateVec[] newStates = null;
		LongVec[] newFps = null;

		final StateQueue stateQueue = this.tlcServer.stateQueue;
		try {
			while (true) {
				TLCState[] states = stateQueue
						.sDequeue(getBlockSize(stateQueue.size()));
				if (states == null) {
					synchronized (this.tlcServer) {
						this.tlcServer.setDone();
						this.tlcServer.notify();
					}
					stateQueue.finishAll();
					return;
				}
				// count statistics
				sentStates += states.length;

				boolean workDone = false;
				while (!workDone) {
					try {
						long start = System.currentTimeMillis();
						Object[] res = this.worker.getNextStates(states);
						long end = System.currentTimeMillis();
						newStates = (TLCStateVec[]) res[0];
						receivedStates += newStates.length;
						newFps = (LongVec[]) res[1];
						workDone = true;
						ToolIO.out.println(new Date() + " Worker: " + url
								+ " Sent: " + states.length + " Rcvd: "
								+ newStates.length + " Time: " + (end - start)
								+ " ms");
					} catch (RemoteException e) {
						if (!this.tlcServer.reassignWorker(this)) {
							ToolIO.out
									.println("Error: No TLC worker is available. Exit.");
							return;
						}
					} catch (NullPointerException e) {
						if (!this.tlcServer.reassignWorker(this)) {<commit_msg>NEW - bug 107: Distributed TLC based on RMI broken  http://bugzilla.tlaplus.net/show_bug.cgi?id=107 - Fix statistics - Skip worker call on empty initial state<commit_after>// 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 13:18:34 PST by lamport  
//      modified on Fri Mar  2 23:46:22 PST 2001 by yuanyu   

package tlc2.tool.distributed;

import java.rmi.RemoteException;
import java.util.Date;
import java.util.concurrent.BrokenBarrierException;
import java.util.concurrent.CyclicBarrier;

import tlc2.TLCGlobals;
import tlc2.output.EC;
import tlc2.output.MP;
import tlc2.tool.TLCState;
import tlc2.tool.TLCStateVec;
import tlc2.tool.WorkerException;
import tlc2.tool.queue.StateQueue;
import tlc2.util.BitVector;
import tlc2.util.IdThread;
import tlc2.util.LongVec;
import util.ToolIO;

/**
 * 
 * @deprecated not used currently
 * @version $Id$
 */
public class TLCServerThread extends IdThread {
	private static final String BLOCK_SIZE = "tlc2.tool.distributed.TLCServerThread.BlockSize";
	/**
	 * TLC server threads manage the set of existing TLC workers.
	 */
	private final static int BlockSize = Integer.getInteger(BLOCK_SIZE, 1024);
	private CyclicBarrier barrier;
	/**
	 * Identifies the worker
	 */
	private String url = "";
	private int receivedStates, sentStates;

	public TLCServerThread(int id, TLCWorkerRMI worker, String url, TLCServer tlc, CyclicBarrier aBarrier) {
		super(id);
		this.worker = worker;
		this.url  = url;
		this.tlcServer = tlc;
		this.barrier = aBarrier;
	}

	private TLCWorkerRMI worker;
	private TLCServer tlcServer;

	public final TLCWorkerRMI getWorker() {
		return this.worker;
	}

	public final void setWorker(TLCWorkerRMI worker) {
		this.worker = worker;
	}

	/**
	 * This method gets a state from the queue, generates all the possible next
	 * states of the state, checks the invariants, and updates the state set and
	 * state queue.
	 */
	public void run() {
		waitOnBarrier();
		
		TLCGlobals.incNumWorkers(1);
		TLCStateVec[] newStates = null;
		LongVec[] newFps = null;

		final StateQueue stateQueue = this.tlcServer.stateQueue;
		try {
			while (true) {
				TLCState[] states = stateQueue
						.sDequeue(getBlockSize(stateQueue.size()));
				if (states == null) {
					synchronized (this.tlcServer) {
						this.tlcServer.setDone();
						this.tlcServer.notify();
					}
					stateQueue.finishAll();
					return;
				}
				
				// without initial states no need to bother workers
				if (states.length == 0) {
					continue;
				}
				
				// count statistics
				sentStates += states.length;

				boolean workDone = false;
				while (!workDone) {
					try {
						long start = System.currentTimeMillis();
						Object[] res = this.worker.getNextStates(states);
						long end = System.currentTimeMillis();
						newStates = (TLCStateVec[]) res[0];
						receivedStates += newStates[0].size();
						newFps = (LongVec[]) res[1];
						workDone = true;
						ToolIO.out.println(new Date() + " Worker: " + url
								+ " Sent: " + states.length + " Rcvd: "
								+ newStates[0].size() + " Time: " + (end - start)
								+ " ms");
					} catch (RemoteException e) {
						if (!this.tlcServer.reassignWorker(this)) {
							ToolIO.out
									.println("Error: No TLC worker is available. Exit.");
							return;
						}
					} catch (NullPointerException e) {
						if (!this.tlcServer.reassignWorker(this)) {
{'fraction_non_alphanumeric': 0.11079714455681142, 'fraction_numerical': 0.016210588935157644, 'mean_word_length': 3.272554002541296, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5447890', 'n_tokens_mistral': 2642, 'n_tokens_neox': 2136, 'n_words': 584}