A forum for Spin users
You are not logged in.
Pages: 1
Can I Use real numbers in spin ? is there any extension since 2011 ?
hi,
can you please elaborate the difference between these two following codes, as the use of atomic {} is not clear to me.
i used it to avoid interleaving but in 1st case it gives me my required results, where as in some cases the 2nd approach is better.please guide me in detail.
what is the difference in using atomic{} before do loop and using in do loop after implication sign.
i will be very grateful to you for responding.
First case
byte turn = 1, x=0;
proctype p() {
atomic {do :: turn == 1 ->turn = 2;x=2;
od
}}
proctype q() {
atomic{ do :: (turn == 2) -> turn = 1; x=1;
od
}}
init {atomic{run q();run p()}}
2nd case
byte turn = 1, x=0;
proctype p() {
do :: (turn == 1) -> atomic{turn = 2;x=2;
}od
}
proctype q() {
do :: (turn == 2) -> atomic{turn = 1; x=1;
}od
}
init {atomic{run q();run p()}}
what if i introduce empty loop in a process? all i want to check is that how a process will evolve if i would introduce delay .the above system has two paths.one leads from x=0 & y= 0 towards X==2 && y==1, and another path is a cycle which starts from x=0 & y= 0 reaches at x=1 & y= 1 and goes to x=0 & y= 0.
i want to check that by introduce delay in a process can i force system to stay in a cycle ? rather than it goes towards 2,1 state.
hi ,
i am trying to compose 2 parallel processes and trying to create delay in one of the process for that if delay is enabled priority goes to another process and it executes before the first one.
here is the example i want to create delay in process A.
proctype A()
16 {
17 do :: x< maxX || x == maxX ->
18 atomic
19 {
20 if /*resX==1 means y=0 and x can evolve*/
21 :: (resX == 1 && y< maxY && x < maxX) -> x++;;
22
23 :: (resX==0 && x > 0/*minX*/) -> x--;/*resx1==resX;*/
24
25 ::( resX==1 && x==maxX) -> x=2;/*x=maxX resx1==resX;*/
26 ::( resX==0 && x==minX) -> x=0/*x=minX*/;
27 fi;}
28 od
29 }
30 proctype B ()
31 {
32 do :: y < maxY || y == maxY->
33 atomic {
34 if
35 :: (resY==1 && x > minX && y < maxY ) -> y++;
36 ::(resY==0 && y==minY)-> y= 0 /*minY*/;
37 ::( resY==0 && y > minY ) -> y--;/*resy1==resY*/;
38 ::( resY==1 && y==maxY)-> y= 1/*maxY*/;/*resy1==resY*/;
39 fi;}
40 od
41 }
please guide me is there any way to model delay ?
Pages: 1