Spinroot

Chengxiu

Member

Registered: 2011-07-28

Posts: 19

concurrency issue of two processes (NEW)

Dear all,

this is still for my two robots interaction program (attached below). two processes proctype Robot1 and proctype Robot2, corresponds to two robots. and they share several global variables 'connected1', 'connected2', 'robot1x', 'robot1y', 'robot2x', 'robot2y'. In each process, there is a 'do .....od ' and executing the codes in it repeatedly. I verified the never claim property '[] <> (connected1 ==1)' and found out the a counter-example (failing trace, cyclic execution which the 'connected1' remain being 0 forever).

But in fact this property should hold, and I found out the mainly problem is that the two processes do not run concurrently, which let two robots do not move synchronously. e.g. the codes in 'do...od' of proctype Robot2 executes two times but the codes in 'do...od' do not execute once.

Is this possible to let two process run synchronously, that is the codes in 'do .. od' of proctype Robot1 execute once and the codes in 'do..od' executes once and repeat ? through configuring different simulation option or modifying the codes?

Many Thanks.

Chengxiu

bool connected1 = 0;
bool connected2 = 0;
int robot1x;
int robot1y;
int robot2x;
int robot2y;
mtype = {n, s, e, w};

proctype Robot1()
{
int robot1Loc = 0;  
int range =1;         
int lenmax = 5;      
int abs12x;
int abs12y;
mtype direction;
mtype nextDirection;       
bool ford =1, coh = 0;  
bool fcon, fnocon, cohcon, cohnocon;  

if /*initially, random direction*/
:: direction = n; printf ("%e", direction);
:: direction = s; printf ("%e", direction);
:: direction = e; printf ("%e", direction);
:: direction = w; printf ("%e", direction);
fi;

do  

::robot1x = robot1Loc / 10; printf ("%d", robot1x); /*xcoordinate*/
  robot1y = robot1Loc % 10; printf("%d", robot1y);/*ycoordinate*/

if
::(robot2x >= robot1x) -> abs12x = robot2x - robot1x;
::(robot2x < robot1x) -> abs12x = robot1x - robot2x;
fi;

if
::(robot2y >= robot1y) -> abs12y = robot2y - robot1y;
::(robot2y < robot1y) -> abs12y = robot1y - robot2y;
fi;

connected1 = ((abs12x <= range) || ((lenmax - abs12x) <= range))&& ((abs12y <= range) ||  ((lenmax - abs12y) <= range));  printf("%d", connected1);

fcon = (ford ==1 && coh == 0 && connected1 == 1);  printf ("%d", fcon);
fnocon = (ford == 1 && coh == 0 && connected1 == 0);  printf ("%d", fnocon);
cohcon = (ford == 0 && coh == 1 && connected1== 1);  printf ("%d", cohcon);
cohnocon = (ford == 0 && coh == 1 && connected1 == 0);  printf ("%d", cohnocon);

/*next location*/
if  /*if there are two statements executable, one of them will be selected randomly*/

::(fcon &&  direction == n ) -> robot1Loc = 10 * (robot1Loc/10)  + (((robot1Loc % 10) + 1) % lenmax) ;  printf ("%d", robot1Loc); /*next robot location, moving north*/
::(fcon && direction  == s) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax) ;  printf ("%d", robot1Loc); /*next robot location, moving south*/
::(fcon && direction == e) -> robot1Loc = (robot1Loc +10) % (lenmax*10) ;  printf ("%d", robot1Loc);  /*next robot location, moving east*/
::(fcon && direction == w) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10); printf ("%d", robot1Loc); /*next robot location, moving west*/


::(fnocon && direction == n) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax);  printf ("%d", robot1Loc);
::(fnocon && direction == s) -> robot1Loc = 10 * (robot1Loc/10)  + (((robot1Loc % 10) + 1) % lenmax);    printf ("%d", robot1Loc);   
::(fnocon && direction == e) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10);  printf (" %d", robot1Loc);      
::(fnocon && direction == w) -> robot1Loc =  (robot1Loc +10) % (lenmax*10);  printf ("%d", robot1Loc);


::(cohnocon &&  direction == n ) -> robot1Loc = 10 * (robot1Loc/10)  + (((robot1Loc % 10) + 1) % lenmax);        printf ("%d", robot1Loc);
::(cohnocon && direction  == s) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax);     printf ("%d", robot1Loc);
::(cohnocon && direction == e) -> robot1Loc = (robot1Loc +10) % (lenmax*10);       printf ("%d", robot1Loc);  
::(cohnocon && direction == w) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10);   printf ("%d", robot1Loc);  


:: (cohcon && direction == n && nextDirection == e) -> robot1Loc = (robot1Loc +10) % (lenmax*10);  printf ("%d", robot1Loc);
:: (cohcon && direction == n && nextDirection == w) ->robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10);   printf ("%d", robot1Loc);
  
:: (cohcon && direction == s && nextDirection == e) -> robot1Loc = (robot1Loc +10) % (lenmax*10) ; printf ("%d", robot1Loc);
:: (cohcon && direction == s && nextDirection == w) ->robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10);   printf ("%d", robot1Loc);
 
:: (cohcon && direction == e && nextDirection == n) -> robot1Loc = 10 * (robot1Loc/10)  + (((robot1Loc % 10) + 1) % lenmax) ;   printf ("%d", robot1Loc);
:: (cohcon && direction == e && nextDirection == s) ->robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax);  printf ("%d", robot1Loc);

:: (cohcon && direction == w && nextDirection == n) -> robot1Loc = 10 * (robot1Loc/10)  + (((robot1Loc % 10) + 1) % lenmax) ;  printf ("%d", robot1Loc);
:: (cohcon && direction == w && nextDirection == s) ->robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax);  printf ("%d", robot1Loc);
 
fi;

/*next motion*/

if
:: (fcon) -> ford = 1; coh = 0;
:: (fnocon) -> ford = 0; coh = 1;
::(cohnocon) -> ford = 0; coh =1;
::(cohcon) -> ford = 1; coh = 0;
fi;

/*next direction*/

if

:: (fcon && direction == n) -> direction = n; printf ("%e", direction);
:: (fcon && direction == s) -> direction = s; printf ("%e", direction);
:: (fcon && direction == e) -> direction = e; printf ("%e", direction);
:: (fcon && direction == w) -> direction = w; printf ("%e", direction);

::(fnocon && direction == n) ->  direction = s; printf ("%e", direction);
::(fnocon && direction == e) ->  direction = w; printf ("%e", direction);
::(fnocon && direction == s) ->  direction = n; printf ("%e", direction);
::(fnocon && direction == w) ->  direction = e; printf ("%e", direction);

:: (cohnocon&& direction == n) -> direction = n; printf ("%e", direction);
:: (cohnocon && direction == s) -> direction = s; printf ("%e", direction);
:: (cohnocon && direction == e) -> direction = e; printf ("%e", direction);
:: (cohnocon && direction == w) -> direction = w; printf ("%e", direction);

:: (cohcon && direction == n) ->  direction = e;  nextDirection = e; printf ("%e", direction);
:: (cohcon && direction == n) ->  direction = w; nextDirection = w; printf ("%e", direction);
 
:: (cohcon && direction == s) ->  direction = e; nextDirection = e; printf ("%e", direction);
:: (cohcon && direction == s) ->  direction = w; nextDirection = w; printf ("%e", direction);

:: (cohcon && direction == e) ->  direction = n; nextDirection = n; printf ("%e", direction);
:: (cohcon && direction == e) ->  direction = s; nextDirection = s; printf ("%e", direction);
 
:: (cohcon && direction == w) ->  direction = n; nextDirection = n; printf ("%e", direction);
:: (cohcon && direction == w) ->  direction = s; nextDirection = s; printf ("%e", direction);

fi;


od

}

proctype Robot2()
{

int robot2Loc = 11;
int range =1;
int lenmax = 5;
int abs12x;
int abs12y;

mtype direction;
mtype nextDirection;
bool ford =1, coh = 0; 
bool fcon, fnocon, cohcon, cohnocon; 

if
:: direction = n; printf ("%e", direction);
:: direction = s; printf ("%e", direction);
:: direction = e; printf ("%e", direction);
:: direction = w; printf ("%e", direction);
fi;

do

::robot2x = robot2Loc / 10; printf ("%d", robot2x); 
  robot2y = robot2Loc % 10; printf ("%d", robot2y); 

if
::(robot2x >= robot1x) -> abs12x = robot2x - robot1x;
::(robot2x < robot1x) -> abs12x = robot1x - robot2x;
fi;

if
::(robot2y >= robot1y) -> abs12y = robot2y - robot1y;
::(robot2y < robot1y) -> abs12y = robot1y - robot2y;
fi;

connected2 = ((abs12x <= range) || ((lenmax - abs12x) <= range))&& ((abs12y <= range) ||  ((lenmax - abs12y) <= range)); printf("%d", connected2);

fcon = (ford ==1 && coh ==0 && connected2 == 1);   printf ("%d", fcon);
fnocon = (ford == 1 && coh == 0 && connected2 == 0);   printf ("%d", fnocon);
cohcon = (ford == 0 && coh == 1 && connected2== 1);   printf ("%d", cohcon);
cohnocon = (ford == 0 && coh == 1 && connected2 == 0);   printf ("%d", cohnocon);

/*next location*/
if  /*if there are two statements executable, one of them will be selected randomly*/

::(fcon &&  direction == n ) -> robot2Loc = 10 * (robot2Loc/10)  + (((robot2Loc % 10) + 1) % lenmax) ; printf ("%d", robot2Loc);
::(fcon && direction  == s) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax) ;   printf ("%d", robot2Loc);
::(fcon && direction == e) -> robot2Loc = (robot2Loc +10) % (lenmax*10) ;  printf ("%d", robot2Loc);
::(fcon && direction == w) -> robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10);   printf ("%d", robot2Loc);


::(fnocon && direction == n) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax);    printf ("%d", robot2Loc);  
::(fnocon && direction == s) -> robot2Loc = 10 * (robot2Loc/10)  + (((robot2Loc % 10) + 1) % lenmax);   printf ("%d", robot2Loc);        
::(fnocon && direction == e) -> robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10);  printf ("%d", robot2Loc);             
::(fnocon && direction == w) -> robot2Loc =  (robot2Loc +10) % (lenmax*10);   printf ("%d", robot2Loc);


::(cohnocon &&  direction == n ) -> robot2Loc = 10 * (robot2Loc/10)  + (((robot2Loc % 10) + 1) % lenmax);   printf ("%d", robot2Loc);      
::(cohnocon && direction  == s) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax);      printf ("%d", robot2Loc);
::(cohnocon && direction == e) -> robot2Loc = (robot2Loc +10) % (lenmax*10);   printf ("%d", robot2Loc);                  
::(cohnocon && direction == w) -> robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10);     printf ("%d", robot2Loc);


:: (cohcon && direction == n && nextDirection == e) -> robot2Loc = (robot2Loc +10) % (lenmax*10);   printf ("%d", robot2Loc);
:: (cohcon && direction == n && nextDirection == w) ->robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10);  printf ("%d", robot2Loc);
  
:: (cohcon && direction == s && nextDirection == e) -> robot2Loc = (robot2Loc +10) % (lenmax*10) ;   printf ("%d", robot2Loc);
::  (cohcon && direction == s && nextDirection == w) ->robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10);   printf ("%d", robot2Loc);
 
:: (cohcon && direction == e && nextDirection == n) -> robot2Loc = 10 * (robot2Loc/10)  + (((robot2Loc % 10) + 1) % lenmax) ;   printf ("%d", robot2Loc);
:: (cohcon && direction == e && nextDirection == s) ->robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax);   printf ("%d", robot2Loc);

:: (cohcon && direction == w && nextDirection == n) -> robot2Loc = 10 * (robot2Loc/10)  + (((robot2Loc % 10) + 1) % lenmax) ;  printf ("%d", robot2Loc);
:: (cohcon && direction == w && nextDirection == s) -> robot2Loc = 10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax);   printf ("%d", robot2Loc);
 
fi;


/*next motion*/

if
:: (fcon) -> ford = 1; coh = 0;
:: (fnocon) -> ford = 0; coh = 1;
::(cohnocon) -> ford = 0; coh =1;
::(cohcon) -> ford = 1; coh = 0;
fi;

/*next direction*/

if

:: (fcon && direction == n) -> direction = n; printf ("%e", direction);
:: (fcon && direction == s) -> direction = s; printf ("%e", direction);
:: (fcon && direction == e) -> direction = e; printf ("%e", direction);
:: (fcon && direction == w) -> direction = w; printf ("%e", direction);

::(fnocon && direction == n) ->  direction = s; printf ("%e", direction);
::(fnocon && direction == e) ->  direction = w; printf ("%e", direction);
::(fnocon && direction == s) ->  direction = n; printf ("%e", direction);
::(fnocon && direction == w) ->  direction = e; printf ("%e", direction);

:: (cohnocon&& direction == n) -> direction = n; printf ("%e", direction);
:: (cohnocon && direction == s) -> direction = s; printf ("%e", direction);
:: (cohnocon && direction == e) -> direction = e; printf ("%e", direction);
:: (cohnocon && direction == w) -> direction = w; printf ("%e", direction);

:: (cohcon && direction == n ) ->  direction = e; nextDirection = e; printf ("%e", direction);
:: (cohcon && direction == n ) ->  direction = w; nextDirection = w; printf ("%e", direction);
 
:: (cohcon && direction == s) ->  direction = e; nextDirection = e; printf ("%e", direction);
:: (cohcon && direction == s) ->  direction = w; nextDirection = w; printf ("%e", direction);

:: (cohcon && direction == e ) ->  direction = n; nextDirection = n; printf ("%e", direction);
:: (cohcon && direction == e ) ->  direction = s; nextDirection = s; printf ("%e", direction);
 
:: (cohcon && direction == w ) ->  direction = n; nextDirection = n; printf ("%e", direction);
:: (cohcon && direction == w ) ->  direction = s; nextDirection = s; printf ("%e", direction);

fi;

od
}

init { atomic {run Robot1(); run Robot2()} }

never  {    /* !([]  <>  (connected1 == 1)) */
T0_init:
    if
    :: (! ((connected1 == 1))) -> goto accept_S4
    :: (1) -> goto T0_init
    fi;
accept_S4:
    if
    :: (! ((connected1 == 1))) -> goto accept_S4
    fi;
}

spinroot

forum

Registered: 2010-11-18

Posts: 702

Website

Re: concurrency issue of two processes (NEW)

Promela is fundamentally a language for specifying asynchronous process behaviors.
Any type of synchronization that you want to enforce has to be enforced explicitly, just like you would need to do if you were to write it as a C program running as multiple threads or processes in a standard operating system. There's no predefined way to let two processes execute in lock-step. So if you'd like to do that, you do have to specify precisely how you'd enforce that....
Perhaps one simple way out would be to fold the two proctypes that must execute synchronously into a single one -- then you can specify precisely what happens and in what order.

Chengxiu

Member

Registered: 2011-07-28

Posts: 19

Re: concurrency issue of two processes (NEW)

[quote=spinroot]Promela is fundamentally a language for specifying asynchronous process behaviors.
Any type of synchronization that you want to enforce has to be enforced explicitly, just like you would need to do if you were to write it as a C program running as multiple threads or processes in a standard operating system. There's no predefined way to let two processes execute in lock-step. So if you'd like to do that, you do have to specify precisely how you'd enforce that....
Perhaps one simple way out would be to fold the two proctypes that must execute synchronously into a single one -- then you can specify precisely what happens and in what order.[/quote]

Ok, thanks. By the way, this piece of code is just for two robots case. Do you think the SPIN can deal with say twenty robots case? will it suffer from the state exploration problem ? I mean I write the code for twenty robots case ,and run the verification, will it work?

Many Thanks,

Chengxiu

spinroot

forum

Registered: 2010-11-18

Posts: 702

Website

Re: concurrency issue of two processes (NEW)

remember that this is a verification tool. are there, for instance, any property violations in a system with 20 robots that could not be exhibited by a system with 19 robots? or 10? or 3?
there's no point in making the problem harder if there's no real gain in return of course.
then note also that this is just a tool to assist you in proving something. it's like math: if used well, you can prove interesting things -- if not used well, you wont be able to prove anything.
so, model the system carefully, making abstractions, finding the simplest possible way to express things formally, and then you'll be able to prove interesting properties of your design.  it's the principle of the 'smallest sufficient model' that allows you to prove things.
just like in ordinary math: keep things as simple as possible, but no simpler, and you can prove remarkable results.  there's no short-cut here -- spin is one of the better tools out there that can handle systems with astounding complexity -- but then again, if you're not careful you can also easily build models that exhibit even greater unnecessary complexity to befuddle even the best of tools.... :-)

Chengxiu

Member

Registered: 2011-07-28

Posts: 19

Re: concurrency issue of two processes (NEW)

[quote=spinroot]remember that this is a verification tool. are there, for instance, any property violations in a system with 20 robots that could not be exhibited by a system with 19 robots? or 10? or 3?
there's no point in making the problem harder if there's no real gain in return of course.
then note also that this is just a tool to assist you in proving something. it's like math: if used well, you can prove interesting things -- if not used well, you wont be able to prove anything.
so, model the system carefully, making abstractions, finding the simplest possible way to express things formally, and then you'll be able to prove interesting properties of your design.  it's the principle of the 'smallest sufficient model' that allows you to prove things.
just like in ordinary math: keep things as simple as possible, but no simpler, and you can prove remarkable results.  there's no short-cut here -- spin is one of the better tools out there that can handle systems with astounding complexity -- but then again, if you're not careful you can also easily build models that exhibit even greater unnecessary complexity to befuddle even the best of tools.... :-)[/quote]

Yes, my study is a control algorithm for a swarm of robots, and the algorithm is able to at certain level keep all robots in connected. the algorithm's performance will increase as the increasing of robot's population. For instance, the algorithm is not good to keep all robots connected in 3,10 robots case, but it is better to keep connected in 20,40 robots case. actually it doesn't make much sense if we only verify small number of robots. But we have done the same thing using NuSMV and already faced state exploration problem for 3 robots case. So I am just wondering, based on your experience, can SPIN do better than NuSMV for verifying larger robot's population? Thanks.

spinroot

forum

Registered: 2010-11-18

Posts: 702

Website

Re: concurrency issue of two processes (NEW)

Spin can handle models with up to 255 asynchronous processes, in principle.
A swarm of robots does sound like a fundamentally asynchronous system. (nuSMV would be the best choice for a purely synchronous system, but Spin specifically targets asynchronous system models).  Whether the verification with a 20 process system remains tractable depends completely on how the model is constructed (the formalization of the algorithm that you want to verify). In general, you should not expect a 1 to 1 translation of implementation code into Promela code to be very tractable -- a successful model checking run normally requires some abstractions to keep things tractable.
You may be able to abstract the behavior (the externally visible behavior that is) of groups of robots, and use that as part of the model, to see how one robot behaves in the presence of multiple others. That then would lead to a 2 process abstraction (i.e., one robot and its environment as far as it is visible to that one robot). In short: it requires thought....

Chengxiu

Member

Registered: 2011-07-28

Posts: 19

Re: concurrency issue of two processes (NEW)

[quote=spinroot]Spin can handle models with up to 255 asynchronous processes, in principle.
A swarm of robots does sound like a fundamentally asynchronous system. (nuSMV would be the best choice for a purely synchronous system, but Spin specifically targets asynchronous system models).  Whether the verification with a 20 process system remains tractable depends completely on how the model is constructed (the formalization of the algorithm that you want to verify). In general, you should not expect a 1 to 1 translation of implementation code into Promela code to be very tractable -- a successful model checking run normally requires some abstractions to keep things tractable.
You may be able to abstract the behavior (the externally visible behavior that is) of groups of robots, and use that as part of the model, to see how one robot behaves in the presence of multiple others. That then would lead to a 2 process abstraction (i.e., one robot and its environment as far as it is visible to that one robot). In short: it requires thought....[/quote]

We have already done some abstractions and clever representations to the control algorithm, we simplify robot's behaviour, discretise the arena and etc. and we write the input for NuSMV and SPIN. for 2,3 robots the verification runs well, I am just thinking whether it is worth trying to verify larger say 20 robots case.

smithaloha13

Member

Registered: 2011-08-07

Posts: 1

Re: concurrency issue of two processes (NEW)

thank for info

Chengxiu

Member

Registered: 2011-07-28

Posts: 19

Re: concurrency issue of two processes (NEW)

[quote=spinroot]Promela is fundamentally a language for specifying asynchronous process behaviors.
Any type of synchronization that you want to enforce has to be enforced explicitly, just like you would need to do if you were to write it as a C program running as multiple threads or processes in a standard operating system. There's no predefined way to let two processes execute in lock-step. So if you'd like to do that, you do have to specify precisely how you'd enforce that....
Perhaps one simple way out would be to fold the two proctypes that must execute synchronously into a single one -- then you can specify precisely what happens and in what order.[/quote]

sorry, I just notice that if we fold the two proctypes into a single one, we do can specify precisely what happens and in what order. However this does not make two robots move synchronously, it just makes robots move in turn in a particular order, e.g. robot1, robot2, robot1, robot2...... is it possible to make two robots (processes) execute in parallel in SPIN? thanks.

spinroot

forum

Registered: 2010-11-18

Posts: 702

Website

Re: concurrency issue of two processes (NEW)

To enforce synchronous behavior of two separate (asynchronous) processes, you have to provide the mechanism that accomplishes this. By default, processes execute asynchronously. (Other than in nuSMV.)
There is no global 'clock' that can step the system, as one would be able to do in a hardware circuit, because Spin models process systems (where you don't have a global clock -- just a process scheduler that can arbitrarily interleave the asynchronous execution of multiple processes).
So, yes, Spin can execute processes in parallel, but no it cannot do this synchronously. But, you can design synchronization mechanisms to accomplish it (just like you would have to do in any real system with multiple robots: they are asynchronous until you explicitly synchronize their behaviors).

Chengxiu

Member

Registered: 2011-07-28

Posts: 19

Re: concurrency issue of two processes (NEW)

> spinroot wrote:

> To enforce synchronous behavior of two separate (asynchronous) processes, you have to provide the mechanism that accomplishes this. By default, processes execute asynchronously. (Other than in nuSMV.)
There is no global 'clock' that can step the system, as one would be able to do in a hardware circuit, because Spin models process systems (where you don't have a global clock -- just a process scheduler that can arbitrarily interleave the asynchronous execution of multiple processes).
So, yes, Spin can execute processes in parallel, but no it cannot do this synchronously. But, you can design synchronization mechanisms to accomplish it (just like you would have to do in any real system with multiple robots: they are asynchronous until you explicitly synchronize their behaviors).

Hi,

Recently I am considering this question again. I am trying to run two SPIN processes in "synchrony". Last time I did this by separating statements of both processes and combining them into a single process. I agree with your 'there is no global clock in SPIN and just a process scheduler that can arbitrarily interleave the asynchronous execution of multiple processes (it looks like run in synchrony), and Spin can execute processes in parallel, but no it cannot do this in pure synchrony '. But I am wondering how to do this in SPIN? how to explicitly 'synchronize' two processes in SPIN, without combining them into a single one?

Many Thanks.

spinroot

forum

Registered: 2010-11-18

Posts: 702

Website

Re: concurrency issue of two processes (NEW)

It's a good question, but the solution is up to you really.
Consider how you would synchronize the actions of two robots who can only synchronize by exchanging messages, or by consulting shared data.
Remember that you're modeling a real-world system, and there is no real synchrony there either...