|
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
|