COSTABS MHP analysis prototype

Write your ABS code in the text area:
//$id: Peertopeer.abs 5108 2010-07-17 20:14:12Z jschaefer $ 

module PeerToPeer;

//type synonyms  

type Filename = String ;
type Filenames = Set<String> ;
type Packet = String ;
type File = List<Packet> ;
type Catalog = List<Pair<Peer, Filenames> > ;

def B mylookup<A, B>(Map<A, B> ms, A k) = // retrieve from the map
  case ms {
     InsertAssoc(Pair(k, y), _) => y;
     // InsertAssoc(_, tm) => lookup(tm, k);
     // Rewritten for aPET (to avoid having fresh vars in the nomatch not present in the match)
     InsertAssoc(Pair(_, _), tm) => mylookup(tm, k);
  };

 
// Application functions
def Peer findServer(Filename file, Catalog catalog) =
case catalog {
    Nil => null;
    Cons(Pair(server, files), rest) =>
    case contains(files, file) { True => server;
        False => findServer(file, rest); };
    };
    
interface Server {
    Filenames enquire();
    Int getLength(Filename fId);
    Packet getPack(Filename fId, Int pNbr);
}


interface Peer extends Client, Server { 
    Unit setAdmin(Network admin);
    Unit run();
}

interface Network {
    List<Peer> getNeighbors(Peer caller);
}

interface DataBase {
    File getFile(Filename fId);
    Int getLength(Filename fId);
    Unit storeFile(Filename fId, File file);
    Filenames listFiles();
}

interface Client {
    Unit reqFile(Server sId, Filename fId);
}

class DataBaseImpl(Map<Filename, File> dbT) implements DataBase {

    [dbT <= max(dbT)]
    File getFile(Filename fId) {
	return mylookup(dbT, fId);
    }
    
    [dbT <= max(dbT)]
    Int getLength(Filename fId) {
	return length(mylookup(dbT,fId));
    }
    
    Unit storeFile(Filename fId, File file) {
	dbT = InsertAssoc(Pair(fId,file), dbT);
    } 
    
    [dbT <= max(dbT)]
    Filenames listFiles() {
	return keys(dbT);
    }
}

class Node(DataBase db, Filename file) implements Peer {
    Catalog catalog = Nil;
    List<Peer> myNeighbors = Nil;
    Network admin = null;
    
    Unit run() {
	Fut<Catalog> c ; 
	Fut<List<Peer>> f;
	Server server; 
	
	await admin != null;
	f = admin!getNeighbors(this);   // Asynchronous call to admin
	[f <= max(myNeighbors)]
	await f?;
	myNeighbors = f.get;
	c = this!availFiles(myNeighbors); // Asynchronous call
	[c <= max(myNeighbors)][file <= max(file)][file >= 0]
	await c?;               // Allow other peers to call in the meantime
	catalog = c.get;        // Build the catalog
	server = findServer(file, catalog); // Find the server for the requested file
	if (server != null) {
	    this.reqFile(server,file) ;        // Download file
	}
    }

    Unit setAdmin(Network admin) {
	this.admin = admin;
    }
    
    Filenames enquire() { 
	Fut<Filenames> f ;  
	f = db!listFiles();
	await f?;
	return f.get;
    }
    
    Int getLength(Filename fId) {
	Fut<Int> length ; 
	length = db!getLength(fId);
	await length?;
	return length.get;
    }
    
    Packet getPack(Filename fId, Int pNbr) {
	File f = Nil;
	Fut<File> ff;
	ff = db!getFile(fId);
	await ff?;
	f = ff.get;
	return nth(f, pNbr);
    }
    
    Catalog availFiles (List<Peer> sList) {
	Catalog cat = Nil;
	Filenames fNames = EmptySet; 
	Fut<Filenames> fN;
	Catalog catList = Nil; 
	Fut<Catalog> cL;
	
	if (sList != Nil) {
	    fN = head(sList)!enquire();
	    cL = this!availFiles(tail(sList));
	    [cL <= max(myNeighbors)]
	    await fN? & cL?;
	    catList = cL.get;
	    fNames = fN.get;
	    cat = appendright(catList, Pair(head(sList), fNames)); 
	}
	return cat; 
    }
    
    Unit reqFile(Server sId, Filename fId) {
	File file = Nil;
	Packet pack = "";
	Int lth = 0;
	Fut<Int> l1;
	Fut<Packet> l2;
	
	l1 = sId!getLength(fId);
	await l1?;
	lth = l1.get; 
	while (lth > 0) {
	    lth = lth - 1;            // indexing is zero-based
	    l2 = sId!getPack(fId, lth);
	    [db <= max(db)]
	    await l2?;
	    pack = l2.get ;
	    file = Cons(pack, file); 
	} 
	db!storeFile(fId, file);
    }
}

class OurTopology(Peer node0, Peer node1, Peer node2, Peer node3)
implements Network
{
    List<Peer> getNeighbors(Peer caller) {
	List<Peer> res = Nil;
	if (caller == node0) { res = list[node1, node2]; }
	if (caller == node1) { res = list[node3]; }
	if (caller == node2) { res = list[node0, node1, node3]; }
	if (caller == node3) { res = list[node0, node2]; }
	return res;
    }
}

{ 
    // Map<Filename, File>
    DataBase db0 = new local DataBaseImpl(map[Pair("file0", list["file", "from", "db0"])]);
    DataBase db1 = new local DataBaseImpl(map[Pair("file1", list["file", "from", "db1"])]);
    DataBase db2 = new local DataBaseImpl(map[Pair("file2", list["file", "from", "db2"])]);
    Peer node0 = new local Node(db0, "file2");
    Peer node1 = new local Node(db1, "file2");
    Peer node2 = new local Node(db2, "file0");
    Peer node3 = new local Node(db2, "file1");
    Network admin = new local OurTopology(node0, node1, node2, node3);
    node0!setAdmin(admin);
    node1!setAdmin(admin);
    node2!setAdmin(admin);
    node3!setAdmin(admin);
    Int i=0;
    while (i<5) {
	node0.run();
	node1.run();
	node2.run();
	node3.run();
	i=i+1;
    }
}
Or you can choose one of our examples: