COSTABS MHP analysis prototype

Write your ABS code in the text area:
module ABSChat.Main;

data ServerMsg = Welcome
   	           | GoodBye
          	   | NewMessage(String);

data ClientMsg = ChatMessage(String,String);

interface Server {
   Unit start();
   [Near] Session connect(Client c);
}

interface Session {
   Unit receive(ClientMsg m);
   Unit close();
}

interface Client {
	Unit setServer(Server s);
	Unit start();
	Unit receive(ServerMsg m);
	[Near] ClientGUI getGUI();
}

interface ClientGUI {
   Unit init2();
   [Far] Button getSendButton();
   [Far] TextField getTextField();
}

interface ClientIntern extends Client {
	 Unit sendText(String text);
}
 
interface ClientGUIIntern extends ClientGUI {
   [Near] ClientIntern getClientIntern();
   String getTextFieldText();
} 

class ClientGUIImpl([Near] ClientIntern client) implements ClientGUIIntern {
   Window gui;
   Button sendButton;   
   TextField textField; 
   Bool initialized = False;
   
   {   
   	  gui = new WindowImpl();
   } 
   
   Unit init2() { 
   	  Fut<Button> f = gui!newButton("Send");
   	  sendButton = f.get;
   	  ButtonListener l = new local SendButtonListener(this);
   	  sendButton!registerListener(l);

      Fut<TextField> tf;
      tf = gui!newTextField();
      textField = tf.get;

   	  initialized = True;
   }
   
   Button getSendButton() {
      await initialized;
      return sendButton;
   }
   
   TextField getTextField() {
      await initialized;
      return textField;
   }
   
   String getTextFieldText() {
      Fut<String> f = textField!getText();
      return f.get;
   }
   
   ClientIntern getClientIntern() {
      return client;
   }
}

[Plain]
class SendButtonListener([Final] [Near] ClientGUIIntern client) implements ButtonListener {
   Unit pressed() {
       ClientIntern ci = client.getClientIntern();
       String s = client.getTextFieldText();
   	   ci.sendText(s);
   }
}


[COG]
class ClientImpl implements ClientIntern { 
   String name = "Alice";
   Server server;
   Session session;
   [Near] ClientGUI gui;

   ClientGUI getGUI() {
	  if (gui == null) {
	     gui = new local ClientGUIImpl(this);
	     gui.init2();
	  }
   	  return gui;
   }

   Unit setServer(Server s) { 
   	   this.server = s;
   }
   
   Unit start() {
      await server != null;
      Fut<Session> f = server!connect(this);
      await f?;
      session = f.get; 
   }
   
   Unit receive(ServerMsg msg) {
   	  await session != null;
	  ClientMsg ans = ChatMessage("","");
	  //if(msg==Welcome){
   	      ans = ChatMessage(name,"Welt"); 
      	  //}
   	  
   	  Fut<Unit> u = session ! receive(ans);
   	  await u?;
   	  session ! close();
   }  
   
   Unit sendText(String text) {
      await session != null;
      session ! receive(ChatMessage(name,text));
   }
}
interface ButtonListener {
   Unit pressed();
}

interface Window {
   [Near] Button newButton(String label);
   [Near] TextField newTextField();
}

interface TextField {
   String getText();
   Unit setText(String newText);
}

interface Button {
   Unit press();
   String getLabel();
   Unit registerListener(ButtonListener l);
}

class TextFieldImpl implements TextField {
  String text = "";
  String getText() {
     return text;
  }

  Unit setText(String s) {
  	 text = s;
  }
}

[COG]
class WindowImpl implements Window {
   [Near] Button newButton(String label) {
      return new local ButtonImpl(this, label);
   }
   
   TextField newTextField() {
   	  return new local TextFieldImpl();
   }
}

[Plain] 
class ButtonImpl([Near] Window gui, String label) implements Button {
    List<ButtonListener> listener = Nil;
   
	Unit press() {
		List<ButtonListener> r = listener;
		while (r != Nil) {
			ButtonListener l = head(r);
			l ! pressed();
			r = tail(r);
		}	
	}
	
	String getLabel() {
		return label;
	}
	
	Unit registerListener(ButtonListener l) {
		listener = Cons(l,listener);
	}
}


interface ServerIntern extends Server {
	Unit sessionClosed(SessionIntern i);
}

interface SessionIntern extends Session {
   Unit init2();
}

[COG]
class ServerImpl implements ServerIntern { 
   Bool running = False;
   List<SessionIntern> sessions = Nil;
   
   Unit start() {
      running = True;
   }
   
   Session connect(Client c) {
       await running;
       SessionIntern s;
       s = new local SessionImpl(this, c);
       sessions = Cons(s,sessions);
       s!init2();
       return s;
   }

	Unit sessionClosed(SessionIntern i) {
	   sessions = without(sessions,i);
	}

}

[Plain]
class SessionImpl(ServerIntern server, Client c) implements SessionIntern {
	Unit init2() {
		c!receive(Welcome);
	}
	
	Unit close() {
	   server.sessionClosed(this);
	}
	
	Unit receive(ClientMsg m) {
	}

}

interface User {
   Unit use(ClientGUI client);
}

[COG] 
class UserImpl implements User {
   ClientGUI gui;
   Button sendBtn;
   TextField textField;
	
   Unit use(ClientGUI client) { 
	  gui = client;
	  Fut<Button> f = gui!getSendButton();
	  await f?;//MZ
	  sendBtn = f.get;
	  
	  Fut<TextField> f2 = gui!getTextField();
	  await f2?;//MZ
	  textField = f2.get;
	  
	  textField!setText("Hello");
	  sendBtn!press();
   }

}

{
    Server server = new ServerImpl();  
    server ! start();
    
    Client client = new ClientImpl();
    client ! setServer(server);
    client ! start();
    
    Fut<ClientGUI> fgui = client ! getGUI();	
    ClientGUI gui = fgui.get;
    
    User user = new UserImpl();
    user ! use(gui);
}
Or you can choose one of our examples: