Spinroot

Yana_b

Member

Registered: 2010-11-23

Posts: 2

How to use "never claims"?

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.

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: How to use "never claims"?

You should include the text of the never claim that is generated in the file with the model.
You can either do that by just copying the text into the file, or by adding a line
#include "never.pml"
in the file with the model, and storing the text of the never claim in a separate file called never.pml.

Yana_b

Member

Registered: 2010-11-23

Posts: 2

Re: How to use "never claims"?

Thank you. Now it works!