A forum for Spin users
You are not logged in.
Pages: 1
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 ?
Offline
the analysis performed by Spin is for logical properties, not performance properties.
so, when using Spin you cannot make any assumptions about the relative speeds of processes, because whatever the system does should be correct no matter how those relative speeds change.
so i'm afraid you cannot introduce delay and hope that the model checker will take it into account. you can make that happen in simulations, but not in actual verifications
Offline
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.
Offline
Can I Use real numbers in spin ? is there any extension since 2011 ?
Offline
Pages: 1