Spinroot

A forum for Spin users

You are not logged in.

#1 2011-08-01 11:13:23

Chengxiu
Member
Registered: 2011-07-28
Posts: 19

about the Xspin verification output

Dear all,

I just finished writing the following code, two processes Robot1 and Robot2, they repeatedly execute and have several global variables 'connected1', 'connected2', 'robot1x', 'robot1y', 'robot2x', 'robot2y'. At the last part, I added the 'never claim' which was automatically generated by system corresponding to the temporal logic formula "[] <> (connected1 && connected2 = 1)", infinitely often the global variables 'connected1' and 'connected2' are true. But when I run this code in Xspin, I don't quite understand the outputs, could anyone run this and give me some feedback, does this 'never claim' property hold?

Cheers,

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;
bool ford =1, coh = 0;  /*ford = for, for is keyword, so we cannot use it*/
bool fcon, fnocon, cohcon, cohnocon; 

if
:: direction = n;
:: direction = s;
:: direction = e;
:: direction = w;
fi;

do

::robot1x = robot1Loc / 10;
  robot1y = robot1Loc % 10;

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));

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);
::(fcon && direction  == s) -> robot1Loc = 10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax) ; printf("%d", robot1Loc);
::(fcon && direction == e) -> robot1Loc = (robot1Loc +10) % (lenmax*10) ; printf("%d", robot1Loc);
::(fcon && direction == w) -> robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10);  printf("%d", robot1Loc);     


::(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) -> robot1Loc = (robot1Loc +10) % (lenmax*10);     printf("%d", robot1Loc);         
::  (cohcon && direction == n) ->robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10);   printf("%d", robot1Loc);         
  
:: (cohcon && direction == s) -> robot1Loc = (robot1Loc +10) % (lenmax*10) ;     printf("%d", robot1Loc);         
::  (cohcon && direction == s) ->robot1Loc = (robot1Loc +(lenmax*10) -10) %(lenmax*10);   printf("%d", robot1Loc);         
 
:: (cohcon && direction == e) -> robot1Loc = 10 * (robot1Loc/10)  + (((robot1Loc % 10) + 1) % lenmax) ;  printf("%d", robot1Loc);         
::  (cohcon && direction == e) ->10*(robot1Loc/10) + (((robot1Loc % 10) + lenmax -1) % lenmax);   printf("%d", robot1Loc);         

:: (cohcon && direction == w) -> robot1Loc = 10 * (robot1Loc/10)  + (((robot1Loc % 10) + 1) % lenmax) ;   printf("%d", robot1Loc);         
::  (cohcon && direction == w) ->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;
:: (fcon && direction == s) -> direction = s;
:: (fcon && direction == e) -> direction = e;
:: (fcon && direction == w) -> direction = w;

::(fnocon && direction == n) ->  direction = s;
::(fnocon && direction == e) ->  direction = w;
::(fnocon && direction == s) ->  direction = n;
::(fnocon && direction == w) ->  direction = e;

:: (cohnocon&& direction == n) -> direction = n;
:: (cohnocon && direction == s) -> direction = s;
:: (cohnocon && direction == e) -> direction = e;
:: (cohnocon && direction == w) -> direction = w;

:: (cohcon && direction == n) ->  direction = e;
:: (cohcon && direction == n) ->  direction = w;
 
:: (cohcon && direction == s) ->  direction = e;
:: (cohcon && direction == s) ->  direction = w;

:: (cohcon && direction == e) ->  direction = n;
:: (cohcon && direction == e) ->  direction = s;
 
:: (cohcon && direction == w) ->  direction = n;
:: (cohcon && direction == w) ->  direction = s;

fi;


od

}

proctype Robot2()
{

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

mtype direction;
bool ford =1, coh = 0;  /*ford = for, for is keyword, so we cannot use it*/
bool fcon, fnocon, cohcon, cohnocon; 

if
:: direction = n;
:: direction = s;
:: direction = e;
:: direction = w;
fi;

do

::robot2x = robot2Loc / 10;
  robot2y = robot2Loc % 10;

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));

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 ) -> 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) -> robot2Loc = (robot2Loc +10) % (lenmax*10);     printf("%d", robot2Loc);         
::  (cohcon && direction == n) ->robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10);   printf("%d", robot2Loc);         
  
:: (cohcon && direction == s) -> robot2Loc = (robot2Loc +10) % (lenmax*10) ;     printf("%d", robot2Loc);         
::  (cohcon && direction == s) ->robot2Loc = (robot2Loc +(lenmax*10) -10) %(lenmax*10);   printf("%d", robot2Loc);         
 
:: (cohcon && direction == e) -> robot2Loc = 10 * (robot2Loc/10)  + (((robot2Loc % 10) + 1) % lenmax) ;  printf("%d", robot2Loc);         
::  (cohcon && direction == e) ->10*(robot2Loc/10) + (((robot2Loc % 10) + lenmax -1) % lenmax);   printf("%d", robot2Loc);         

:: (cohcon && direction == w) -> robot2Loc = 10 * (robot2Loc/10)  + (((robot2Loc % 10) + 1) % lenmax) ;   printf("%d", robot2Loc);         
::  (cohcon && direction == w) ->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;
:: (fcon && direction == s) -> direction = s;
:: (fcon && direction == e) -> direction = e;
:: (fcon && direction == w) -> direction = w;

::(fnocon && direction == n) ->  direction = s;
::(fnocon && direction == e) ->  direction = w;
::(fnocon && direction == s) ->  direction = n;
::(fnocon && direction == w) ->  direction = e;

:: (cohnocon&& direction == n) -> direction = n;
:: (cohnocon && direction == s) -> direction = s;
:: (cohnocon && direction == e) -> direction = e;
:: (cohnocon && direction == w) -> direction = w;

:: (cohcon && direction == n) ->  direction = e;
:: (cohcon && direction == n) ->  direction = w;
 
:: (cohcon && direction == s) ->  direction = e;
:: (cohcon && direction == s) ->  direction = w;

:: (cohcon && direction == e) ->  direction = n;
:: (cohcon && direction == e) ->  direction = s;
 
:: (cohcon && direction == w) ->  direction = n;
:: (cohcon && direction == w) ->  direction = s;

fi;

od
}

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

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

Offline

#2 2011-08-01 15:37:30

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

Re: about the Xspin verification output

did you mean to say that connected1 and connected2 are always eventually *simultaneously* true? (because that's what your property states....)

Offline

#3 2011-08-01 17:42:13

Chengxiu
Member
Registered: 2011-07-28
Posts: 19

Re: about the Xspin verification output

[quote=spinroot]did you mean to say that connected1 and connected2 are always eventually *simultaneously* true? (because that's what your property states....)[/quote]


Thanks, I understand your question.

In fact, I want to verify, for each global variable 'connected1' and 'connected2', infinitely often (always eventually) they hold.

so it should verify them separately.

1. verifying never claim for '[] <> (connected1 == 1)' to the program.
2. verifying never claim for '[] <> (connected2 == 1)' to the program.

could you give me some feedback for the results, do them hold? because I don't quite understand
the output, thanks.

Cheers,

Chengxiu

Offline

#4 2011-08-02 05:08:46

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

Re: about the Xspin verification output

i did the following:
- removed "&& connected2" from the property
- spin -a spec.pml
- cc -o pan pan.c
- ./pan -a
this generated a counter-example -- showing that the property does not hold
i.e., there is an execition where connected1 does not eventually return to the value 1, but can permanently remain 0
you then replay the precise steps in that error scenario but saying something like:
- spin -t -p spec.pml
This will print a cyclic execution that can be repeated forever after, with connected1 being zero. The cycle starts at the point in the printout where it says "Start of Cycle".
You can add more detail to the trace with various spin options (see spin -- for a list).
The counter-example I generated is 223 steps long.
Easier perhaps to learn the basics by using these shell command-line steps at first.

Offline

#5 2011-08-03 21:12:07

Chengxiu
Member
Registered: 2011-07-28
Posts: 19

Re: about the Xspin verification output

[quote=spinroot]i did the following:
- removed "&& connected2" from the property
- spin -a spec.pml
- cc -o pan pan.c
- ./pan -a
this generated a counter-example -- showing that the property does not hold
i.e., there is an execition where connected1 does not eventually return to the value 1, but can permanently remain 0
you then replay the precise steps in that error scenario but saying something like:
- spin -t -p spec.pml
This will print a cyclic execution that can be repeated forever after, with connected1 being zero. The cycle starts at the point in the printout where it says "Start of Cycle".
You can add more detail to the trace with various spin options (see spin -- for a list).
The counter-example I generated is 223 steps long.
Easier perhaps to learn the basics by using these shell command-line steps at first.[/quote]

ok, thanks so much!

Offline

Board footer

Powered by FluxBB