/* lockserver.m
 * EECS 570 Murphi Tutorial
 * Subarno Banerjee, Winter 2020
 */

Type
	server_t : Record
		lock : boolean;
	End;
	client_t : Record
		link : boolean;
	End;
	client_n: 0..9;

Var
	server : server_t;
	client : Array[client_n] of client_t;

StartState
Begin
	server.lock := true;
	For c : client_n Do
		client[c].link := false;
	End;
End;

RuleSet c : client_n Do
	Rule "client connect"
		server.lock
	==>
	Begin
		client[c].link := true;
		server.lock := false;
	End;
      
	Rule "client disconnect"
		client[c].link
	==>
	Begin
		client[c].link := false;
		server.lock := true;
	End;
End;

Invariant "only one client at a time"
	ForAll c : client_n Do
		!(client[c].link & client[1-c].link)
	End;
--	ForAll c1 : client_n Do
--	ForAll c2 : client_n Do
--		client[c1].link & client[c2].link
--		->
--			c1 = c2
--	End
--	End;
