-- twoclient.rpd
-- michael chen


-- types

type Address is string;
type HTML is string;
type GraphAnnotation is string;
type IPAddress is string;
type Question is string;
type Feedback is string;
type TutorAdvice is string;


-- client modules

type WebBrowser is interface
action in  HTMLPage(H : HTML), PageLinks(P : HTML);
       out  WebDocumentRequest(A : Address), LinkRequests(L : Address),
	    UseInfoInGraph(I : IPAddress; G : GraphAnnotation);
behavior
   A : Address is "http:\\www.dinosaurs.advlearn.com";
   L : Address is "link addresses go here";
   G : GraphAnnotation is "Open Graph";
   I : IPAddress is "36.216.0.211";
begin
   start ||> WebDocumentRequest(A);;
   (?H in HTML) HTMLPage(?H) ||> LinkRequests(L);;
   start ||> UseInfoInGraph(I, G);;
end WebBrowser;


type JavaTools is interface
action in  ReceiveGraphInfo(I : IPAddress; G : GraphAnnotation),
           AdviceToClient(T : TutorAdvice), GraphUpdate(G : GraphAnnotation),
	   HighlightUpdate();
       out  JavaGraphChange(N : GraphAnnotation), RequestHelp(), Highlight();
behavior
   N : GraphAnnotation is "Add Node To Graph";
   action UserWantsGraphChange(N : GraphAnnotation);
begin
   (?I in IPAddress, ?G in GraphAnnotation) ReceiveGraphInfo(?I, ?G) ||> 
	UserWantsGraphChange(N);;
   (?N in GraphAnnotation) UserWantsGraphChange(?N) ||> JavaGraphChange(?N);;
   start ||> RequestHelp;;
   start ||> Highlight;;
end JavaTools;



-- client architecture


type Client is interface
action in  HTMLPage(H : HTML), PageLinks(P : HTML), 
	   SendInfoToJava(I : IPAddress; G : GraphAnnotation),
	   AdviceToClient(T : TutorAdvice), GraphUpdate(G : GraphAnnotation),
	   HighlightUpdate();
       out  WebDocumentRequest(A : Address), LinkRequests(L : Address),
	    UseInfoInGraph(I : IPAddress; G : GraphAnnotation),
	    JavaGraphChange(N : GraphAnnotation), RequestHelp(), Highlight();
end;


architecture ClientArch() for Client is
   WB : WebBrowser;
   JT : JavaTools;
connect
   (?A in Address) WB.WebDocumentRequest(?A) ||> WebDocumentRequest(?A);
   (?H in HTML) HTMLPage(?H) ||> WB.HTMLPage(?H);
   (?L in Address) WB.LinkRequests(?L) ||> LinkRequests(?L);
   (?P in HTML) PageLinks(?P) ||> WB.PageLinks(?P);
   (?I in IPAddress, ?G in GraphAnnotation) WB.UseInfoInGraph(?I, ?G) ||> 
	UseInfoInGraph(?I, ?G);
   (?I in IPAddress, ?G in GraphAnnotation) SendInfoToJava(?I, ?G) ||> 
	JT.ReceiveGraphInfo(?I, ?G);
   (?N in GraphAnnotation) JT.JavaGraphChange(?N) ||> JavaGraphChange(?N);
   (?T in TutorAdvice) AdviceToClient(?T) ||> JT.AdviceToClient(?T);
   JT.RequestHelp ||> RequestHelp;
   JT.Highlight ||> Highlight;
   (?G in GraphAnnotation) GraphUpdate(?G) ||> JT.GraphUpdate(?G);
   HighlightUpdate ||> JT.HighlightUpdate;
end ClientArch;


-- server modules


type HTTPServer is interface
action in  WebDocumentRequest(A : Address; C : Client), 
	   LinkRequests(L : Address; C : Client),
	   UseInfoInGraph(I : IPAddress; G : GraphAnnotation; C : Client),
	   JavaGraphChange(N : GraphAnnotation; C : Client), 
	   RequestHelp(C : Client), Highlight(C : Client);
       out  HTMLPage(H : HTML; C : Client), PageLinks(P : HTML; C : Client), 
	    SendAddressToLog(A : Address; C : Client), 
	    SendInfoToJava(I : IPAddress; G : GraphAnnotation; C : Client),
	    GraphUpdateToPostgres(G : GraphAnnotation; C : Client),
	    GraphUpdateToCoach(G : GraphAnnotation; C : Client), 
	    GraphUpdateToConMan(G : GraphAnnotation; C : Client), 
	    HelpRequestToCoach(C : Client), 
	    HighlightCommandToConMan(C : Client);
behavior
   H : HTML is "this is an html page";
   P : HTML is "these are the page links";
begin
   (?A in Address, ?C in Client) WebDocumentRequest(?A, ?C) ||> 
	HTMLPage(H, ?C);;
   (?A in Address, ?C in Client) WebDocumentRequest(?A, ?C) ||> 
	SendAddressToLog(?A, ?C);;
   (?L in Address, ?C in Client) LinkRequests(?L, ?C) ||> PageLinks(P, ?C);;
   (?I in IPAddress, ?G in GraphAnnotation, ?C in Client) 
	UseInfoInGraph(?I, ?G, ?C) ||> SendInfoToJava(?I, ?G, ?C);; 
   (?I in IPAddress, ?G in GraphAnnotation, ?C in Client) 
	UseInfoInGraph(?I, ?G, ?C) ||> GraphUpdateToPostgres(?G, ?C);;
   (?I in IPAddress, ?G in GraphAnnotation, ?C in Client) 
	UseInfoInGraph(?I, ?G, ?C) ||> GraphUpdateToCoach(?G, ?C);;
   (?I in IPAddress, ?G in GraphAnnotation, ?C in Client) 
	UseInfoInGraph(?I, ?G, ?C) ||> GraphUpdateToConMan(?G, ?C);;
   (?N in GraphAnnotation, ?C in Client) JavaGraphChange(?N, ?C) ||> 
	GraphUpdateToPostgres(?N, ?C);;
   (?N in GraphAnnotation, ?C in Client) JavaGraphChange(?N, ?C) ||> 
	GraphUpdateToCoach(?N, ?C);;
   (?N in GraphAnnotation, ?C in Client) JavaGraphChange(?N, ?C) ||> 
	GraphUpdateToConMan(?N, ?C);;
   (?C in Client) RequestHelp(?C) ||> HelpRequestToCoach(?C);;
   (?C in Client) Highlight(?C) ||> HighlightCommandToConMan(?C);;
end HTTPServer;


type Logfile is interface
action in  ReceiveHTTPAddress(A : Address; C : Client);
       out  SendAddressToTracker(A : Address; C : Client);
behavior
begin
   (?A in Address, ?C in Client) ReceiveHTTPAddress(?A, ?C) ||> 
	SendAddressToTracker(?A, ?C);;
end Logfile;


type Tracker is interface
action in  ReceiveAddress(A : Address; C : Client);
end WWWTracker;


type Postgres is interface
action in  GraphUpdateToPostgres(G : GraphAnnotation; C : Client), 
	   QueryToDatabase(Q : Question; C : Client);
       out  FeedbackToCoach(F : Feedback; C : Client);
behavior
   F : Feedback is "yes, it is accurate";
begin
   (?Q in Question, ?C in Client) QueryToDatabase(?Q, ?C) ||> 
	FeedbackToCoach(F, ?C);; 
end Postgres;


type Coach is interface
action in  GraphUpdateToCoach(G : GraphAnnotation; C : Client), 
	   FeedbackToCoach(F : Feedback; C : Client), 
	   HelpRequestToCoach(C : Client);
       out  QueryToDatabase(Q : Question; C : Client), 
	    AdviceToClient(T : TutorAdvice; C : Client);
behavior
   Q : Question is "is this hypothesis accurate?";
   T : TutorAdvice is "you have learned well, young skywalker";
begin
   (?G in GraphAnnotation, ?C in Client) GraphUpdateToCoach(?G, ?C) ||> 
	QueryToDatabase(Q, ?C);;
   (?F in Feedback, ?C in Client) FeedbackToCoach(?F, ?C) ||> 
	AdviceToClient(T, ?C);;
   (?C in Client) HelpRequestToCoach(?C) ||> QueryToDatabase(Q, ?C);;
end Coach;


type ConnectionManager is interface
action in  GraphUpdateToConMan(G : GraphAnnotation; C : Client), 
	   Highlight(C : Client);
       out  UpdateToOtherClient(G : GraphAnnotation; C : Client),
	    UpdateHighlightToOtherClient(C : Client);
behavior
begin
   (?G in GraphAnnotation, ?C in Client) GraphUpdateToConMan(?G, ?C) ||>
	UpdateToOtherClient(?G, ?C);;
   (?C in Client) Highlight(?C) ||> UpdateHighlightToOtherClient(?C);;
end ConnectionManager;


-- server architecture


type Server is interface
action in  WebDocumentRequest(A : Address; C : Client), 
	   LinkRequests(L : Address; C : Client),
	   UseInfoInGraph(I : IPAddress; G : GraphAnnotation; C : Client), 
	   RequestHelp(C : Client), Highlight(C : Client), 
	   JavaGraphChange(N : GraphAnnotation; C : Client);
       out  HTMLPage(H : HTML; C : Client), PageLinks(P : HTML; C : Client), 
	    SendInfoToJava(I : IPAddress; G : GraphAnnotation; C : Client),
	    AdviceToClient(T : TutorAdvice; C : Client),
	    UpdateToOtherClient(G : GraphAnnotation; C : Client),
	    UpdateHighlightToOtherClient(C : Client);
end Server;


architecture ServerArch() for Server is
   HTTP : HTTPServer;
   LOG : Logfile;
   TRAC : Tracker;
   POST : Postgres;
   COACH : Coach;
   CONMAN : ConnectionManager;
connect
   (?A in Address, ?C in Client) WebDocumentRequest(?A, ?C) ||> 
	HTTP.WebDocumentRequest(?A, ?C);
   (?A in Address, ?C in Client) HTTP.SendAddressToLog(?A, ?C) ||> 
	LOG.ReceiveHTTPAddress(?A, ?C);
   (?A in Address, ?C in Client) LOG.SendAddressToTracker(?A, ?C) ||> 
	TRAC.ReceiveAddress(?A, ?C);
   (?H in HTML, ?C in Client) HTTP.HTMLPage(?H, ?C) ||> HTMLPage(?H, ?C);
   (?L in Address, ?C in Client) LinkRequests(?L, ?C) ||> 
	HTTP.LinkRequests(?L, ?C);
   (?P in HTML, ?C in Client) HTTP.PageLinks(?P, ?C) ||> PageLinks(?P, ?C);
   (?I in IPAddress, ?G in GraphAnnotation, ?C in Client) 
	UseInfoInGraph(?I, ?G, ?C) ||> HTTP.UseInfoInGraph(?I, ?G, ?C);
   (?I in IPAddress, ?G in GraphAnnotation, ?C in Client) 
	HTTP.SendInfoToJava(?I, ?G, ?C) ||> SendInfoToJava(?I, ?G, ?C);
   (?G in GraphAnnotation, ?C in Client) HTTP.GraphUpdateToPostgres(?G, ?C) ||>
	POST.GraphUpdateToPostgres(?G, ?C);
   (?G in GraphAnnotation, ?C in Client) HTTP.GraphUpdateToCoach(?G, ?C) ||>
	COACH.GraphUpdateToCoach(?G, ?C);
   (?G in GraphAnnotation, ?C in Client) HTTP.GraphUpdateToConMan(?G, ?C) ||>
	CONMAN.GraphUpdateToConMan(?G, ?C);
   (?N in GraphAnnotation, ?C in Client) JavaGraphChange(?N, ?C) ||> 
	HTTP.JavaGraphChange(?N, ?C);
   (?Q in Question, ?C in Client) COACH.QueryToDatabase(?Q, ?C) ||> 
	POST.QueryToDatabase(?Q, ?C);
   (?F in Feedback, ?C in Client) POST.FeedbackToCoach(?F, ?C) ||> 
	COACH.FeedbackToCoach(?F, ?C);
   (?T in TutorAdvice, ?C in Client) COACH.AdviceToClient(?T, ?C) ||> 
	AdviceToClient(?T, ?C);
   (?C in Client) RequestHelp(?C) ||> HTTP.RequestHelp(?C);
   (?C in Client) HTTP.HelpRequestToCoach(?C) ||> COACH.HelpRequestToCoach(?C);
   (?C in Client) Highlight(?C) ||> HTTP.Highlight(?C);
   (?C in Client) HTTP.HighlightCommandToConMan(?C) ||> CONMAN.Highlight(?C);
   (?G in GraphAnnotation, ?C in Client) CONMAN.UpdateToOtherClient(?G, ?C) ||>
	UpdateToOtherClient(?G, ?C);
   (?C in Client) CONMAN.UpdateHighlightToOtherClient(?C) ||>
	UpdateHighlightToOtherClient(?C);
end ServerArch;


-- abstract implementation architecture


architecture ail()
is
   C1, C2 : Client is ClientArch();
   S : Server is ServerArch();
connect
   (?A in Address, ?C in Client) ?C.WebDocumentRequest(?A) ||> 
	S.WebDocumentRequest(?A, ?C);
   (?H in HTML, ?C in Client) S.HTMLPage(?H, ?C) ||> ?C.HTMLPage(?H);
   (?L in Address, ?C in Client) ?C.LinkRequests(?L) ||> 
	S.LinkRequests(?L, ?C);
   (?P in HTML, ?C in Client) S.PageLinks(?P, ?C) ||> ?C.PageLinks(?P);
   (?I in IPAddress, ?G in GraphAnnotation, ?C in Client) 
	?C.UseInfoInGraph(?I, ?G) ||> S.UseInfoInGraph(?I, ?G, ?C);
   (?I in IPAddress, ?G in GraphAnnotation, ?C in Client) 
	S.SendInfoToJava(?I, ?G, ?C) ||> ?C.SendInfoToJava(?I, ?G);
   (?N in GraphAnnotation, ?C in Client) ?C.JavaGraphChange(?N) ||> 
	S.JavaGraphChange(?N, ?C);
   (?T in TutorAdvice, ?C in Client) S.AdviceToClient(?T, ?C) ||> 
	?C.AdviceToClient(?T);
   (?C in Client) ?C.RequestHelp ||> S.RequestHelp(?C);
   (?C in Client) ?C.Highlight ||> S.Highlight(?C);
   (?G in GraphAnnotation) S.UpdateToOtherClient(?G, C1) ||> 
	C2.GraphUpdate(?G);
   (?G in GraphAnnotation) S.UpdateToOtherClient(?G, C2) ||>
	C1.GraphUpdate(?G);
   S.UpdateHighlightToOtherClient(C1) ||> C2.HighlightUpdate;
   S.UpdateHighlightToOtherClient(C2) ||> C1.HighlightUpdate;
end ail;