[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

No Subject




hi, sorry for the last message but it was a bug of my navigator for the ->

now, i'm another problems, i have this two record based on the same record, 

	define_abstraction_client : abstraction_type -> (#
		abs :-> "client",
		behaving :-> replicate(prefix(send(nam,call),prefix(receive(nam,wait),prefix(unobservable,done)))),
		local :-> emptyset,
		bound :-> add(wait,emptyset),
		free :-> emptyset,
		param :-> emptyset
	#)

define_abstraction_server : abstraction_type -> (#
		abs :-> "server",
		behaving :-> replicate(prefix(receive(nam,request),prefix(unobservable,prefix(send(nam,reply),done)))),
		local :-> emptyset,
		bound :-> add(request,emptyset),
		free :-> emptyset,
		param :-> emptyset
	#)

behaving is a behaviour, and replicate,send, receive prefix are functions

the record is : 

	abstraction_type : type->  [#
		 abs : string,
		 local :  setof[value], 
		 bound : setof[value] ,
		 free  :  setof[value],
		 behaving : behaviour,
		 param : setof[base_type] #] 
	

i will do a theorem  of this type : for example if the behaving of the first record has a send with "call" then the second record has a receive   with "call" in its behaving.

is it possible to do this ?

thx for answer 

ps : there are no problems with my code, typechecked ok