package tlc2.tool.distributed;

import java.io.File;
import java.io.FileNotFoundException;
import java.io.FileOutputStream;
import java.io.IOException;
import java.rmi.RemoteException;
import java.util.HashMap;
import java.util.Map;

import util.FilenameToStream;
import util.SimpleFilenameToStream;

/**
 * This class extends the SimpleFilenameToStream class in the way that it first
 * tries to resolve file with the local {@link FilenameToStream} resolver, but
 * falls back to RMI if the local resolver fails.
 * 
 * This is used for distributed TLC where a worker does not necessarily have
 * access to the specification and/or configuration files.
 * 
 * Care must be taken with transferring big files. This implementation is
 * inefficient in the way that it requires the server to read the full file into
 * memory before it gets transferred to the client. The client too, will buffer
 * the full file in memory. This constraint is acceptable for TLA specifications
 * and configurations as they are usually small enough to fit into memory "easily".
 */
public class RMIFilenameToStreamResolver extends SimpleFilenameToStream {

	private static final String javaTempDir = System.getProperty("java.io.tmpdir") + File.separator;

	private TLCServerRMI server;
	
	private final Map<String, File> fileCache = new HashMap<String, File>();
	private final String rndPrefix;
	
	public RMIFilenameToStreamResolver() {
		super();
		rndPrefix = getRandomStoragePrefix();
	}

	public RMIFilenameToStreamResolver(final String[] libraryPaths) {
		super(libraryPaths);
		rndPrefix = getRandomStoragePrefix();
	}

	public void setTLCServer(final TLCServerRMI aServer) {
		this.server = aServer;
	}
	
	/* (non-Javadoc)
	 * @see util.FilenameToStream#resolve(java.lang.String, boolean)
	 */
	@Override
	public File resolve(final String filename, final boolean isModule) {
		// try to resolve locally first
		File file = super.resolve(filename, isModule);
		
		// read the file from the server if local resolution has failed
		if(!file.exists()) {
			// strip off path
			final String name = new File(filename).getName();
			
			File tempFile = fileCache.get(name);
			
			// not in cache
			if (tempFile == null) {
				
				// read bytes from server
				byte[] bs = new byte[0];
				try {
					bs = server.getFile(name);
				} catch (RemoteException e) {
					e.printStackTrace();
				}

				// write into temp file
				file = writeToNewTempFile(name, bs);
				
				// add to local file cache
				fileCache.put(name, file);
			}
		}
		
		return file;
	}

	private String getRandomStoragePrefix() {
		final File file = new File(javaTempDir + System.currentTimeMillis());
		file.deleteOnExit();
		file.mkdir();
		return file.getAbsolutePath();
	}
	
	private File writeToNewTempFile(String name, byte[] bs) {
		final File f = new File(rndPrefix + File.separator + name);
		f.deleteOnExit();
		
		FileOutputStream outputStream = null;
		try {
			outputStream = new FileOutputStream(f);
			outputStream.write(bs);
		} catch (FileNotFoundException e) {
			e.printStackTrace();
		} catch (IOException e) {
			e.printStackTrace();
		} finally {
			if(outputStream != null) {
				try {
					outputStream.close();
				} catch (IOException e) {
					e.printStackTrace();
				}
			}
		}
		return f;
	}
}

@@ -260,44 +260,8 @@
 eam;
-%0Aimport util.SimpleFilenameToStream;
 %0A%0A/*
@@ -1064,22 +1064,19 @@
 ver 
-extend
+implement
 s 
-Simple
 File
@@ -1375,19 +1375,8 @@
 ) %7B%0A
-%09%09super();%0A
 %09%09rn
@@ -1486,31 +1486,8 @@
 ) %7B%0A
-%09%09super(libraryPaths);%0A
 %09%09rn
@@ -1705,19 +1705,8 @@
  */%0A
-%09@Override%0A
 %09pub
@@ -1777,182 +1777,44 @@
 %7B%0A%09%09
-// try to resolve locally first%0A%09%09File file = super.resolve(filename, isModule);%0A%09%09%0A%09%09// read the file from the server if local resolution has failed%0A%09%09if(!file.exists()) %7B%0A%09
+%0A%09%09// read the file from the server%0A
 %09%09//
@@ -1829,17 +1829,16 @@
 ff path%0A
-%09
 %09%09final 
@@ -1883,19 +1883,17 @@
 me();%0A%09%09
-%09%0A%09
+%0A
 %09%09File t
@@ -1925,19 +1925,37 @@
 ame);%0A%09%09
-%09
 %0A%09
+%09File file = null;%0A
 %09%09// not
@@ -1964,17 +1964,16 @@
 n cache%0A
-%09
 %09%09if (te
@@ -1989,27 +1989,25 @@
  null) %7B%0A%09%09%09
-%09%0A%09
+%0A
 %09%09%09// read b
@@ -2023,17 +2023,16 @@
  server%0A
-%09
 %09%09%09byte%5B
@@ -2050,32 +2050,30 @@
 byte%5B0%5D;%0A%09%09%09
-%09
 try %7B%0A
-%09
 %09%09%09%09bs = ser
@@ -2091,17 +2091,16 @@
 (name);%0A
-%09
 %09%09%09%7D cat
@@ -2120,33 +2120,32 @@
 eption e) %7B%0A%09%09%09%09
-%09
 e.printStackTrac
@@ -2145,25 +2145,24 @@
 ackTrace();%0A
-%09
 %09%09%09%7D%0A%0A%09%09%09%09//
@@ -2158,17 +2158,16 @@
 %09%09%7D%0A%0A%09%09%09
-%09
 // write
@@ -2189,14 +2189,14 @@
 %0A%09%09%09
-%09
 file 
+ 
 = wr
@@ -2226,19 +2226,17 @@
 bs);%0A%09%09%09
-%09%0A%09
+%0A
 %09%09%09// ad
@@ -2257,17 +2257,16 @@
 e cache%0A
-%09
 %09%09%09fileC
@@ -2287,21 +2287,16 @@
  file);%0A
-%09%09%09%7D%0A
 %09%09%7D%0A%09%09%0A%09

Resolve all files (especially standard modules) by the master instead of at each worker node (to allow users to resolve custom standard modules) #2