Spinroot

A forum for Spin users

You are not logged in.

#1 2011-05-26 11:22:06

Usman
Member
Registered: 2011-05-20
Posts: 7

how to create delay in a transition

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

#2 2011-05-27 03:09:53

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: how to create delay in a transition

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

#3 2011-05-27 06:05:12

Usman
Member
Registered: 2011-05-20
Posts: 7

Re: how to create delay in a transition

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

#4 2011-05-27 06:08:43

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: how to create delay in a transition

'delay' cannot be modeled in Spin: the analysis is independent of time

Offline

#5 2013-11-12 19:30:54

Usman
Member
Registered: 2011-05-20
Posts: 7

Re: how to create delay in a transition

Can I Use real numbers in spin ? is there any extension since 2011 ?

Offline

#6 2013-11-13 05:42:56

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: how to create delay in a transition

no real numbers or floating point -- it would make the model intractable....

Offline

Board footer

Powered by FluxBB