A forum for Spin users
You are not logged in.
Pages: 1
Take the following simple model:
mtype = { Foo , Bar };
chan master = [10] of { mtype , int , int } ;
active proctype Master() {
chan sender;
int i , x ;
do
:: master ? Foo( i , x ) -> skip ;
:: master ? Bar( i ) -> skip;
od
}
active proctype Slave() {
do
:: master ! Foo( 5 , 10 ) -> skip ;
:: master ! Bar( 3 ) -> skip ;
od
}
I'd like to know whether there are any severe side effects to not satisfying all parameters for a message on a channel. The Foo constructor has only one int, Bar has two int's. When simulating, I see the following warnings:
11: warning: missing params in send
16: warning: missing params in next recv
17: warning: missing params in send
Is this a perfectly acceptable use of sending/receiving over channels?
Offline
Pages: 1