Spinroot

I had a difficulty when compilingthe new  6.2.0 version of spin on a 64-bit Linux system.

The difficulty was solved by putting "extern YYSTYPE yylval" at the beginning of the file "reprosrc.c" .
Strangely enough, the error did not occur on two Ubuntu systems.

Kees Pronk

=================================================================

Here is the compilation error:

yacc         -v -d          spin.y
gcc -c y?tab.c
rm -f y?tab.c
mv y?tab.o spin.o
gcc -O2 -DNXT       -c -o spinlex.o spinlex.c
gcc -O2 -DNXT       -c -o sym.o sym.c
gcc -O2 -DNXT       -c -o vars.o vars.c
gcc -O2 -DNXT       -c -o main.o main.c
gcc -O2 -DNXT       -c -o ps_msc.o ps_msc.c
gcc -O2 -DNXT       -c -o mesg.o mesg.c
gcc -O2 -DNXT       -c -o flow.o flow.c
gcc -O2 -DNXT       -c -o sched.o sched.c
gcc -O2 -DNXT       -c -o run.o run.c
gcc -O2 -DNXT       -c -o pangen1.o pangen1.c
gcc -O2 -DNXT       -c -o pangen2.o pangen2.c
gcc -O2 -DNXT       -c -o pangen3.o pangen3.c
gcc -O2 -DNXT       -c -o pangen4.o pangen4.c
gcc -O2 -DNXT       -c -o pangen5.o pangen5.c
gcc -O2 -DNXT       -c -o guided.o guided.c
gcc -O2 -DNXT       -c -o dstep.o dstep.c
gcc -O2 -DNXT       -c -o structs.o structs.c
gcc -O2 -DNXT       -c -o pc_zpp.o pc_zpp.c
gcc -O2 -DNXT       -c -o pangen6.o pangen6.c
gcc -O2 -DNXT       -c -o pangen7.o pangen7.c
gcc -O2 -DNXT       -c -o reprosrc.o reprosrc.c
reprosrc.c: In function 'blip':
reprosrc.c:190: error: 'yylval' undeclared (first use in this function)
reprosrc.c:190: error: (Each undeclared identifier is reported only once
reprosrc.c:190: error: for each function it appears in.)
reprosrc.c: In function 'pretty_print':
reprosrc.c:341: error: 'yylval' undeclared (first use in this function)
make: *** [reprosrc.o] Error 1

Here is how "gcc -v" identifies itself:

Using built-in specs.
Target: x86_64-redhat-linux
Configured with: ../configure --prefix=/usr --mandir=/usr/share/man --infodir=/usr/share/info --with-bugurl=http://bugzilla.redhat.com/bugzilla --enable-bootstrap --enable-shared --enable-threads=posix --enable-checking=release --with-system-zlib --enable-__cxa_atexit --disable-libunwind-exceptions --enable-gnu-unique-object --enable-languages=c,c++,objc,obj-c++,java,fortran,ada --enable-java-awt=gtk --disable-dssi --with-java-home=/usr/lib/jvm/java-1.5.0-gcj-1.5.0.0/jre --enable-libgcj-multifile --enable-java-maintainer-mode --with-ecj-jar=/usr/share/java/eclipse-ecj.jar --disable-libjava-multilib --with-ppl --with-cloog --with-tune=generic --with-arch_32=i686 --build=x86_64-redhat-linux
Thread model: posix
gcc version 4.4.5 20101112 (Red Hat 4.4.5-2) (GCC)

==================================================================

The following program, when translated with spin -a p7.pml

byte p;
byte q;

ltl p7 {p equivalent q}
ltl p7a {p <-> q}

init{skip;}

will give the following unexpected error message:

ltl p7: (p) <-> (q)
ltl p7a: (p) <-> (q)
spin: _spin_nvr.tmp:4, Error: syntax error    saw ';'
spin: _spin_nvr.tmp:13, Error: syntax error    saw ';'
spin: p7.pml:18, Error: proctype p7a not found

Kees

I am having the following (very stupid) program divzero.pml:

init{
    int k;
    k = k + 1;
    k = k / 0;   
    skip;   
}

When I work from the command prompt:
spin -a divzero.pml         // is ok
gcc -w -o pan pan.c        // is ok; BTW leaving out the -w will draw my attention to the error made
./pan                             // will report a floating point exception, which is OK.

However, when running from iSpin:

- the simulator is silent
- the verifier is silent; the only action I notice is that the processor load is increased.

So it seems exceptions are not propagated back into iSpin?

In [url]http://spinroot.com/spin/Man/for.html[/url] the second grammar line states that one should use the colon in the for statement for arrays:
   for '(' varref ':' array ')' '{' sequence '}'  .

However, the example given a little later shows that one should use the 'in' keyword.

      int a[10];
    for (i in a) {
        printf("i = %d\n", i)
    }

This problem is also in the grammar in [url]http://spinroot.com/spin/Man/grammar.html[/url] .

As an aside, the examples would be slightly more self-explanatory if they would show that one needs to declare the loop control variable.

Kees.

I'm having a problem with the new ispin:

When I load a promela program and start a verification I get the error message

invalid command name ".f.fVp.top.right.row0.ent"
invalid command name ".f.fVp.top.right.row0.ent"
    while executing
"$t.top.right.row0.ent get"
    (procedure "run_ver" line 67)
    invoked from within
"run_ver .f.fVp "
    invoked from within
".f.fVp.top.fourth.row6.go invoke"
    ("uplevel" body line 1)
    invoked from within
"uplevel #0 [list $w invoke]"
    (procedure "tk::ButtonUp" line 22)
    invoked from within
"tk::ButtonUp .f.fVp.top.fourth.row6.go"
    (command bound to event)

The problem disappears if I open the "Show advanced parameter setting" window, and reoccurs when I close that window.
It seems the tcl-code cannot read from a closed window?
The problem occurs both on 64-bit Fedora Linux with Gnome and on a 64-bit Suse installation.
Kees