Spinroot

A forum for Spin users

You are not logged in.

#1 2011-02-03 18:33:20

dwende
Member
Registered: 2011-02-02
Posts: 7

ispin questions

Hello

I am a newcomer to spin, I am trying to (dis)prove an algorithm used for repairing torn pages in a flash device.

I have purchased the Spin book (Holzmann) and am currently learning how to use the software and language.

I am using printf("MSC: statements\n") liberally but they are not printed out anyway in the ispin windows.

I did check the MSC+stmnt box.

Within ispin, how are the 'tracked variable' and 'track scaling' used?

I have worked out that 'var names' is a filter on tracked variable names.

Another question - is there any EASY guide to writing never statements?

Thanks a lot.

Offline

#2 2011-02-04 05:26:28

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

Re: ispin questions

the MSC prefix, as described in the last book from 2004, was supported in xspin, but isn't supported (yet) in the new GUI ispin.
If you want to experiment with Xspin, you can still find old copies on the spinroot page, e.g.:
[url]http://spinroot.com/spin/Src/xspin525.tcl[/url]
but it's no longer supported officially (i.e., no more bug fixes in that older GUI).
the 'tracked variable' is of little real use -- it was just an experiment to see if it might be useful.
the effect of tracking a variable is to get an extra bar in the MSC view indicating the variable value.
then of course you may need to scale it just right tomake the visual work nicely -- it'll probably disappear again since it's not too useful.
I would recommend not using never claims, but learn how to use inline LTL formula instead.
it's much easier now that it was when the book came out. Look at some of the examples (grep for "ltl" in all the examples in especiallu the iSpin/ltl_examples directory and you'll get the idea -- and also read about LTL in the book of course)

Offline

#3 2011-02-04 11:44:51

dwende
Member
Registered: 2011-02-02
Posts: 7

Re: ispin questions

Thanks for the reply regarding MSC.

As for "never" versus LTL I did try using the latter but found that the syntax checker within ispin always gave the error:

spin: hnvm2.pml:56, Error: cannot create temporary file
child process exited abnormally

The LTL is:

ltl f0 { []!failure }

The never claim that DOES work is this:

never f1 {
    do
    :: failure -> break
    :: else
    od
    }

On the other hand, running spin from a cygwin terminal did NOT complain about the LTL version.

I am assuming (hoping) that the above two forms of the claim are identical as far as verification is concerned.

Thanks again

Offline

#4 2011-02-04 17:12:05

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

Re: ispin questions

please tell me more about the circumstances under which you get the error.
is it a linux or a windows system?
do you execute the command in a directory where you have write permission?
(i.e., can you create files in that directory yourself?)

Offline

#5 2011-02-05 20:04:14

dwende
Member
Registered: 2011-02-02
Posts: 7

Re: ispin questions

This problem occurs running spin 6.01 under windows 7.
Note that I can normally  create a sub-directory in the current working directory.

I have spin installed also on Linux, and have no problems running spin -a file.pml on the Linux box.

Thanks

BTW - are the two forms (never and LTL) synonymous?

Offline

#6 2011-02-05 20:37:12

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

Re: ispin questions

LTL formula are translated into never-claims, so yes they're related.
Never claims, though, can specify more properties than LTL, so they are more expressive.
Can you show what happens when you give the command spin -a file.pml ?
(i.e., what precise error message do you see)

Offline

#7 2011-02-05 21:14:50

dwende
Member
Registered: 2011-02-02
Posts: 7

Re: ispin questions

The following is the exact message.

C:\Users\dwende\Projects\spin>spin -a hnvm2.pml
spin: hnvm2.pml:47, Error: cannot create temporary file

The following is the pml file:

/*
Model the HNVM anti tearing process

Processes are:
0 init
1 cpu
2,3,4 pages

Will choose pages 2 and 3 as data and 4 as flag

cpu can do following 'actions' to a page:
- do_read (no side effects on page)
- do_erase (side effects, page becomes 'erase')
- do_prog (side effects - page becomes 'prog')

If a reset occurs during either erase or prog the page is marked as torn
and then will return randomly either good, bad or erase.

We wish to check whether it is possible to have both data pages torn concurrently

*/
mtype {good_data, torn, erased,do_read, do_tear, do_erase, do_prog, all_ones, programmed, bad_data};

#define pF 0
#define p0 1
#define p1 2
inline pb(a) {
printf("MSC: ~B Step %d\n",a);
}
inline pr(a) {
printf("MSC: ~R hello from %d\n",a);
}

// bool wasProgrammed = false

chan to_page = [0] of { byte, byte, byte };
chan from_page = [0] of { byte, byte };

byte state[3];
bool done =  false;

bool p0_torn = (state[p0] == torn);
bool p1_torn = (state[p1] == torn);

#define failure (state[p0] == torn && state[p1] == torn )

ltl f0 { []!failure }

//never f0 {    /* !( ![]<>failure) */
//T0_init:
//    if
//    :: ((!failure)) -> goto accept_S9
//    :: (1) -> goto T0_init
//    fi;
//accept_S9:
//    if
//    :: (1) -> goto T0_init
//    fi;
//}

//never f1 {
//do
//:: failure -> break
//:: else
//od
//}



/*
Models the CPU
It can read, erase and program flash and take action if tearing
*/

active [3] proctype page()
{
    byte me = _pid;
    byte v  ;
    state[me] = erased;

on_reset:

pr(me);
    /* get action requests from CPU */
    do
    :: to_page?eval(me),do_read,v -> atomic {
        printf("=>Page %d got read cmd\n",me);
        if
        :: state[me] == erased     -> from_page!all_ones,v
        :: state[me] == programmed -> from_page!good_data,v
        :: state[me] == torn       ->
            if
            :: from_page!good_data,v
            :: from_page!bad_data,v
            :: from_page!all_ones,v
            fi
        fi
        }
    :: to_page?eval(me),do_erase,v -> printf("=>Page %d got erase cmd\n",me); state[me] = erased; done = true
    :: to_page?eval(me),do_prog,v  -> printf("=>Page %d got prog cmd with v %d\n",me,v); state[me] = programmed; done = true
    :: to_page?eval(me),do_tear,v  -> printf("=>!!!Page %d got TEAR cmd\n",me); state[me] = torn; done = true
    od
}

active proctype cpu ()
{
unsigned i : 2 ;
byte newpage, oldpage, v[3];
byte pointer; /* point to good page */
    byte result[3];

do_reset:


    // read all pages
    to_page!0,do_read,v[0];
    from_page?result[0],v[0];
    to_page!1,do_read,v[1];
    from_page?result[1],v[1];
    to_page!2,do_read,v[2];
    from_page?result[2],v[2];

// assert  (state[p0] != torn || state[p1] != torn);
    printf("C=>Got read result from all pages\n");

    /* get highest v from p0 and p1 */
    if
    :: v[p0] > v[p1] -> newpage = p0; oldpage = p1
    :: else -> newpage = p1; oldpage = p0
    fi;

    /* now analyse results */
    printf("C=>Analyze results\n");
    if
    :: result[pF] == all_ones && result[p0] == good_data && result[p1] == all_ones  ->
        pb(1);
        pointer = p0
    :: result[pF] == all_ones && result[p0] == all_ones  && result[p1] == good_data ->
        pb(2);
        pointer = p1

    :: result[pF] == all_ones && result[p0] == good_data && result[p1] == good_data ->
        pb(3);
        pointer = oldpage;
        if
        :: done=false;
            printf("C=>Erase page %d\n",newpage);
            to_page!newpage,do_erase,0;
            done -> skip
        :: done=false;
            printf("C=>Tear page %d\n",newpage);
            to_page!newpage,do_tear,v[newpage];
            done -> goto do_reset
        fi
    :: result[pF] == all_ones && result[p0] == all_ones  && result[p1] == all_ones  ->
        pb(4);
        pointer = p0

    :: result[pF] != all_ones && result[p0] == good_data && result[p1] == all_ones  ->
        pb(5);
        pointer = p0;
        if
        :: done=false;
            printf("C=>Erase page %d\n",pF);
            to_page!pF,do_erase,0;
            done -> skip
        :: done=false;
            printf("C=>Tear page %d\n",pF);
            to_page!pF,do_tear,0;
            done -> goto do_reset
        fi

    :: result[pF] != all_ones && result[p0] == all_ones  && result[p1] == good_data ->
        pb(6);
        pointer = p1;
        if
        :: done=false;
            to_page!pF,do_erase,0;
            done -> skip
        :: done=false;
            to_page!pF,do_tear,0;
            done -> goto do_reset
        fi

    :: result[pF] != all_ones && result[p0] == good_data && result[p1] == good_data ->
        pb(7);
        pointer = newpage;
        if
        :: done=false;
            printf("C=>Erase page %d\n",oldpage);
            to_page!oldpage,do_erase,0;
            done -> skip
        :: done=false;
            printf("C=>Tear page %d\n",oldpage);
            to_page!oldpage,do_tear,v[oldpage];
            done -> goto do_reset
        fi;
        if
        :: done=false;
            printf("C=>Erase page %d\n",pF);
            to_page!pF,do_erase,0;
            done -> skip
        :: done=false;
            printf("C=>Erase page %d\n",pF);
            to_page!pF,do_tear,0;
            done -> goto do_reset
        fi

    :: result[pF] != all_ones && result[p0] == all_ones  && result[p1] == all_ones  ->
        pb(8);
        pointer = p0

    :: result[p0] == bad_data ->
        pb(9);
        if
        :: done = false;
            printf("C=>Bad so Erase page %d\n",p0);
            to_page!p0,do_erase,v[p0];
            done -> pointer = p1
        :: done = false;
            printf("C=>Bad so Erase-tear page %d\n",p0);
            to_page!p0,do_tear,v[p0];
            done -> goto do_reset
        fi

    :: result[p1] == bad_data -> pb(10);
        if
        :: done = false;
            printf("C=>Bad so Erase page %d\n",p1);
            to_page!p1,do_erase,v[p1];
            done -> pointer = p0
        :: done = false;
            printf("C=>Bad so Erase-tear page %d\n",p1);
            to_page!p1,do_tear,v[p1];
            done -> goto do_reset
        fi
    fi;

    /* now program a page */
    printf("C=>>>Erase old page %d\n",3-pointer);
    if
    :: done=false; to_page!(3-pointer),do_erase,0; done -> skip
    :: done=false; to_page!(3-pointer),do_tear,v[3-pointer]; done -> goto do_reset
    fi;

    printf("C=>>>Erase flag\n");
    if
    :: done=false; to_page!pF,do_erase,0; done -> skip
    :: done=false; to_page!pF,do_tear,0; done -> goto do_reset
    fi;

    printf("C=>>>Prog page %d\n",pointer);
    if
    :: done=false; to_page!pointer,do_prog,(v[pointer]+1); done -> skip
    :: done=false; to_page!pointer,do_tear,(v[pointer]+1); done -> goto do_reset
    fi;

    printf("C=>>>Prog flag\n");
    if
    :: done=false; to_page!pF,do_prog,0; done -> skip
    :: done=false; to_page!pF,do_tear,0; done -> goto do_reset
    fi;

goto do_reset

}

Offline

#8 2011-02-05 21:32:38

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

Re: ispin questions

that's interesting, because this then means that the function tmpfile fails
this is an ANSI C standard library function that is perhaps not supported in Windows 7.
it looks like you do not have cygwin installed -- it most likely would work normally if you used that.
is that an option?

Offline

#9 2011-02-05 21:51:09

dwende
Member
Registered: 2011-02-02
Posts: 7

Re: ispin questions

Here is the strange part. I actually have cygwin installed. When I run spin from within cygwin terminal then spin does NOT complain. Of course I only
have the single executable spin on my PC, it's just that when it is run from a regular cmd window that I get the error, when the same exe is run from the
cygwin then OK.

The ispin GUI is installed normally (not through cygwin), so the sequence I follow (to get around this problem) is:

1. run "spin -a file" from within cygwin.
2. compile pan in either cygwin or regular cmd window (I have gcc installed both under cygwin and as a standalone).
3. run ispin and use the trail from step 2.

BTW - without imposing any more than you allow yourself to be imposed upon, could you give me hints to improve the pml I sent in the previous email.

Thanks

Offline

#10 2011-02-06 02:11:23

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

Re: ispin questions

I'll remove the call to tmpfile in the next release of spin, to make sure it works also on Windows 7

Offline

#11 2011-02-06 02:15:14

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

Re: ispin questions

to find redundancies in a model, you can try spin -A file.pml
sometimes that helps -- you can also try to make more things atomic, to reduce complexity somewhat
other than that, i don't see too much that could be improved
you can of course also use bitstate hashing, or hashcompact, to get a handle on a large search space

Offline

#12 2011-02-06 14:19:24

dwende
Member
Registered: 2011-02-02
Posts: 7

Re: ispin questions

Thanks for the advice.

I realize that the two LTL statements:

a) []!failure
and
b) ![]failure

are probably different since running spin -f on them both produces different results.

I would read these in English as 'always never failure' and 'never (always) failure' but then again, I am a complete
novice in this field.

Could you explain what is the difference, and if I just want to check whether the failure could ever exist, which
is the correct form to use?

Thanks

Offline

#13 2011-02-06 20:20:34

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

Re: ispin questions

yes these two formula express different properties:
![] failure is equivalent to saying <>!failure
(not always is the same as eventually not)
i think in your case you want the first form: []! failure if you want to make sure that no failure could ever exist, and get a counter-example if it can anyway

Offline

#14 2011-02-07 07:11:08

dwende
Member
Registered: 2011-02-02
Posts: 7

Re: ispin questions

Thank you for the answer

Offline

Board footer

Powered by FluxBB