Spinroot

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

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

}

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