COSTABS MHP analysis prototype

Write your ABS code in the text area:
module MailServer;
import * from ABS.StdLib;

type UserName = String ;
type Message = String;

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);
  };

def Map<A, B> myput<A, B>(Map<A, B> ms, A k, B v) =
  case ms {
    EmptyMap => InsertAssoc(Pair(k, v),EmptyMap);
    InsertAssoc(Pair(k, _), ts) => InsertAssoc(Pair(k, v), ts);
    InsertAssoc(p, ts) => InsertAssoc(p, myput(ts, k, v));
  };


interface AddressBook {
      User getUserAddress(UserName u);
      Unit addUser(UserName uname,User u);
}

class AddressBookImp implements AddressBook {
      Map<UserName,User> users = EmptyMap;

      [users <= max(users)]
      User getUserAddress(UserName u){
      	      return mylookup(users,u);
      }

      Unit addUser(UserName uname,User u){
      	      users = myput(users,uname,u);
      }
}

interface User {
     Unit receive(Message msg);
}

class UserImp implements User {
      List<Message> msgs = Nil;

      Unit receive(Message msg) {
         msgs = Cons(msg,msgs);
      }
}


interface MailServer {
      Unit addUser(UserName uname,User u);
      Unit notify(Message m);
}

class MailServerImp(AddressBook ab) implements MailServer {

    List<UserName> listUsers = Nil;
    
    Unit addUser(UserName uname,User u) {
        listUsers = Cons(uname, listUsers);
	ab!addUser(uname,u);
    }
    
    [listUsers <= max(listUsers)]
    Unit notify(Message m) {
	Fut<User> u; User us;
	List<UserName> listUsersAux = list(listUsers);
        while ( listUsersAux != Nil ) {
            u = ab ! getUserAddress( head(listUsersAux) );
            [old(listUsersAux) == listUsersAux]
            await u?;
            us = u.get;
            us!receive(m);
            listUsersAux = tail(listUsersAux);
        }
    }
}


{ // building three users
/*    
    Map<String,Int> map = EmptyMap;
    map = myput(map,"a",32);
    map = myput(map,"b",40);
*/
    User u1 = new UserImp();
    User u2 = new UserImp();
    User u3 = new UserImp();
    // building the address book and mail server
    AddressBook ab= new AddressBookImp();
    MailServer ms = new MailServerImp(ab);
    // adding users to the mail server which in turn adds them to the AddressBook
    ms ! addUser("John",u1);
    ms ! addUser("Mary",u2);
    ms ! addUser("Mike",u3);
    List<Message> mssg = Cons("m1",Cons("m2",Cons("m3",Cons("m4",Nil))));
    while (mssg!=Nil){
	ms!notify(head(mssg));
	mssg=tail(mssg);
    }

}
Or you can choose one of our examples: