Spinroot

Harry

Member

Registered: 2012-01-18

Posts: 8

SPIN - bug with "-F" operator

Hello,

I compiled SPIN by myself using cygwin on Win7 (64bit system).
I tried all three variants "make_pc", "makefile", and "makefile" (picky commandline).
Compilation works without errors.
I can start the "spin.exe" if i use "cygwin1.dll".

Everything seems fine, but if I use the command "     C:\jspin\bin\spin.exe -O -a -F model.ltl model.pml    " the following output I get:

tl_spin: syntax error, saw '.'
tl_spin: model.ltl.nvr
----------------^

If I change the command to "    C:\jspin\bin\spin.exe -O -a -f ..... model.pml      " (..... = any ltl formula) it works (pan.c is created).

With the official/precompiled spin.exe both command-lines are working.
If this is not a bug... and I'm doing anything wrong, please help me.

Last edited by Harry (2012-01-26 23:49:41)

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: SPIN - bug with "-F" operator

this is difficult to chase down since i cannot reproduce it
from the error message you get with the version you compiled it seems that the -F argument is actually read as a -f argument -- but that doesn't seem to make sense.
are you sure you didn't mistype the command and typed an '-f' instead of a '-F' ?
i can't imagine that a compiler would map 'F' to 'f' -- if so, it would do the same with all other uppercase parameter flags (e.g., -T or -I).   You could try: spin -I model.pml   and see if it gives you interactive mode, or performs inlining as it is supposed to....?

Harry

Member

Registered: 2012-01-18

Posts: 8

Re: SPIN - bug with "-F" operator

Hi, I checked it and "-i" (=> interactive mode) works different as "-I" (=> prints the model) with the same "spin.exe".

The problem only occurs with "-F"