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

about the recursive process



Hello,
 
I am confused by the definition of recursive processes in PVS.  Is there anybody could give me some good ideas? Let's me make a example:
 
P = a -> b -> P
 
this is a recursive process of CSP. One of methods to solve this problem is to use the parametric process and the least fixed point.
 
X: VAR [U -> process]
 
F: VAR [[U->process] -> [U->process]]
 
F(X)(x)= a>>b>>X(x+1)
 
then P:[U->process] = mu(H)
 
This method is efficient only when we deal with the simply process like verifying the process P is a subset of specific specification. But when meet the little complex situation, it is difficult. For example, there are two group of processes:
 
P(i) = a->b->c->P(i)      Q(i)=c->Q(i)
 
First, we get the interleaving of all the P(i) and Q(i) respectively.
 
Interleave(P)   Interleave(Q)
 
 
then make them synchronized. Interleave(P) || Interleave(Q)
 
So, is it possible we give up the parametric processes to define the recursive process in PVS, is it easier?
 
Kun