Home

We provide here a collection of examples of interaction models taken from our test cases, based on areas such as bioinformatics, business and emergency response.

3-D Structure Prediction of Yeast Proteins 

//  Written by Xueping Quan and modified by Paolo Besana
//
//  LCC Specification for consistency checking of yeast protein 3-D models:

r( experimenter, initial)
r( data_coordinator, necessary, 1)
r( data_collector, auxiliary, 1)
r( data_retriever, auxiliary,1)
r( data_source, necessary, 1)
r( data_filter, necessary, 1)
r( data_comparer, necessary, 1)
r( pairwise_comparer,necessary,1)

a(experimenter, E)::
data_request(Is) => a(data_coordinator, X) <- ask_user(Is) then
data_compared(Is,Sd) <= a(data_coordinator, X) then
null <- printresults(Sd)

a(data_coordinator, X)::
data_request(Is) <= a(experimenter, E) then
null<-getInterestedRole(R) and getPeers(R,Sp) and 
	makeEmptyList(SdS) then
a(data_collector(Is, Sp, SdS, SdF),X) then
filter(Is,Sp,SdF) => a(data_filter,Y) then
filtered(S) <= a(data_filter, Y) then
filtered(Is,Sp,S) => a(data_comparer, C) then
data_compared(Is,Df) <= a(data_comparer, C) then
data_compared(Is,Df) => a(experimenter,E)

a(data_collector(Is,Sp,SdS,SdF),X)::
null <- Is=[] and assign(SdS,SdF) or
(null <- Is=[I|Ri] then
data_request(I) => a(data_source,P) then
data_report(I,Ds) <= a(data_source,P) then
null <- NewSdS=[Ds|SdS] then
a(data_collector(Ri,Sp,NewSdS,SdF),X))

a(data_retriever(I,Sp,SBuildUp,SF),X)::
null <- Sp=[] and assign(SBuildUp, SF) or
(null <- Sp = [P|Rp] then
data_request(I) => a(data_source,P) then
data_report(I,Ds) <= a(data_source,P) then
null <- NewSBuildUp = [Ds|SBuildUp] then
a(data_retriever(I,Rp,NewSBuildUp,SF),X))

a(data_filter, Y)::
filter(Is,Sp,Sd) <= a(data_coordinator,X) then
filtered(S) => a(data_coordinator,X) <- apply_filter(Sd,S)

a(data_source, P)::
data_request(I) <= a(data_collector,X) then
data_report(I,Ds) => a(data_collector,X) <- lookup(I,Ds)

a(data_comparer, C)::
filtered(Is,Sp,S) <= a(data_coordinator,X) then
data_tocompare(Is,Sp,S) => a(pairwise_comparer, M) then
data_pairwise(Is, Pc) <= a(pairwise_comparer, M) then
data_compared(Is,Df) => a(data_coordinator,X) <-
		     threeway_check(Is,Pc,Df)

a(pairwise_comparer, M)::
data_tocompare(Is,Sp,S) <= a(data_comparer, C) then
data_pairwise(Is,Pc) => a(data_comparer, C) <- 
		     pairwise_check(Is,S,Pc)
De Novo Protein Sequencing by MS/MS 

//  Written by Xueping Quan and modified by Paolo Besana
//
//  LCC Specification for cross-checking of de novo sequencing by MS/MS:

r( experimenter, initial)
r( data_coordinator, necessary, 1)
r( data_collector, auxiliary, 1)
r( data_retriever, auxiliary,1)
r( data_source, necessary, 1)
r( data_comparer, necessary, 1)

a(experimenter, E)::
null <- ask_files(Lst_dtas_file) then
null <- get_content_from_file(Lst_dtas_file, Dtas) then
data_request(Lst_dtas_file, Dtas) => a(data_coordinator, X) then
data_compared(Lst_dtas_file,Sd) <= a(data_coordinator, X)  then
null <- printresults(Sd)

a(data_coordinator, X)::
data_request(Lst_dtas_file, Dtas) <= a(experimenter, E) then
null <- getInterestedRole(R) and getPeers(R,Sp) and 
	makeEmptyList(SdS)  then
a(data_collector(Lst_dtas_file, Dtas, Sp, SdS, SdF),X) then
data_tocompare(Lst_dtas_file,Sp,SdF) => a(data_comparer, C)  then
data_compared(Lst_dtas_file,Df) <= a(data_comparer, C) then
data_compared(Lst_dtas_file,Sd) => a(experimenter,E)

a(data_collector(Lst_dtas_file, Dtas, Sp, SdS, SdF),X)::
null <- Lst_dtas_file=[] and assign(SdS,SdF) or
(null <- Lst_dtas_file=[F|Rdtas_filesTail] and Dtas = [D|DtasTail]
then
data_request(F,D) => a(data_source,P) then
data_report(F,Ds) <= a(data_source,P)  then
null <- NewSdS=[Ds|SdS] then
a(data_collector(Rdtas_filesTail,DtasTail,Sp,NewSdS,SdF),X))

a(data_retriever(I,Sp,SBuildUp,SF),X)::
null <- Sp=[] and assign(SBuildUp, SF) or
(null <- Sp = [P|Rp] then
data_request(I) => a(data_source,P) then
data_report(I,Ds) <= a(data_source,P) then
null <- NewSBuildUp = [Ds|SBuildUp] then
a(data_retriever(I,Rp,NewSBuildUp,SF),X))

a(data_source, P)::
data_request(F,D) <= a(data_collector,X) then
data_report(F,Ds)=>a(data_collector,X)<-denovoanalysis(F,D,Ds)

a(data_comparer, C)::
data_tocompare(Lst_dtas_file,Sp,SdF) <= a(data_coordinator,X) then
data_compared(Lst_dtas_file,Df) => a(data_coordinator,X) <-
				threeway_check(Lst_dtas_file,SdF,Df)
Egglue Powered