A forum for Spin users
You are not logged in.
Pages: 1
Thank you. Now it works!
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.
Pages: 1