Spinroot

A forum for Spin users

You are not logged in.

#2 General » How to use "never claims"? » 2010-11-23 12:19:32

Yana_b
Replies: 2

I started to work with JSpin (GUI) about a mounth ago.
Now I want to use a never claim []<>bb   in my Promela-program to check some konfiguration charakteristics.
In JSpin I can generate a code for this LTL-formula, and it looks like this:

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

Where should I write this code, so that I can start a verification?
After the verification ran, I see the output-file, where I can read that no never claims were used. Why???

(Spin Version 4.3.0 -- 22 June 2007)
Warning: Search not completed
Full statespace search for:
    never claim             - (none specified)
    assertion violations    +
    cycle checks           - (disabled by -DSAFETY)
    invalid end states    +
State-vector 52 byte, depth reached 19, ••• errors: 1 •••
     135 states, stored
     208 states, matched
       0 matches within stack
     343 transitions (= stored+matched)
       0 atomic steps
hash conflicts: 0 (resolved)
stackframes: 0/0
stats: fa 0, fh 0, zh 0, zn 0 - check 0 holds 0
stack stats: puts 0, probes 0, zaps 0
2.302     memory usage (Mbyte)

Can anybody help me? Thanks.


My programm looks as:

chan input_system = [0] of {mtype};
chan system_output = [0] of {mtype};

mtype = {in_5euro, in_1euro, in_zeit, in_weiter, in_abbruch};
mtype = {out_parkschein, out_1euro, out_2euro};

active proctype Input()

    do
     :: input_system!in_zeit
     :: input_system!in_weiter
     :: input_system!in_abbruch
     :: input_system!in_5euro
     :: input_system!in_1euro
    od
}

active proctype System()
{     
      int zeit = 0;
      int gezahlt = 0;
      int zuzahlen = 0;
      int rest = 0;       
      bit bb=0;
   
      a:      do
               :: input_system?in_zeit -> zeit=zeit+1; goto a
               :: input_system?in_abbruch -> zeit = 0; goto a
               :: input_system?in_weiter; zeit>0 -> zuzahlen=zeit; bb=1;
                  b:  do
                        :: input_system?in_1euro -> gezahlt=gezahlt+1; goto b
                        :: input_system?in_5euro -> gezahlt=gezahlt+5; goto b
                        :: input_system?in_abbruch -> zeit=0; rest=gezahlt;
                           d:     do
                                    :: rest >= 2 -> system_output!out_2euro; rest=rest-2; goto d
                                    :: rest == 1 -> system_output!out_1euro; rest=rest-1; goto d
                                    :: rest == 0 -> zeit=0; gezahlt=0; goto a
                                   od   
                        :: gezahlt>=zuzahlen ->
                           c:     do
                                    :: system_output!out_parkschein; rest=gezahlt-zuzahlen; goto c
                                    :: rest > 0 -> goto d
                                    :: rest == 0 -> zeit=0; gezahlt=0; goto a
                                   od
                       od
               od
}

active proctype Output()
{
     int ausgabe_2euro, ausgabe_1euro;
     ausgabe_2euro=0;
     ausgabe_1euro=0;

     id1:    do
                :: system_output?out_parkschein
                :: system_output?out_2euro -> ausgabe_2euro=ausgabe_2euro+1; goto id1
                :: system_output?out_1euro -> ausgabe_1euro=ausgabe_1euro+1; goto id1
               od
}

It should represent a parking automat.

Board footer

Powered by FluxBB