Spinroot

After opening a model, if I switch to "verification" tab, "non-progress cycles" is selected by default. I think that is ok. However, if I choose "safety" and verify and then go to "Edit/View" tab and come back to "verification" tab, I see that "non-progress cycles" is selected again by default. I would expect whatever verification options I chose before (in this case, "safety") to be sticky. And, it is my expectation and I would not complain if the current behavior is by design though.

It looks like "Edit/View" window that shows the model uses 8 spaces for tabs. I use tabs for indenting my PROMELA models. Though I use a different editor to edit the model, I tend to view the model in iSpin as I can click on file-name/line-number in the simulation output of error trails. It would be nice, if I can configure the tab size to 2 spaces so that the model will fit nicer within the window. If not through GUI dialog, a shell env variable or a command-line argument for iSpin would be very acceptable.

PS: Why is "Edit/View" window not using a mono-space font to show code? Is it an error or intentional to fit within space?

When inline functions are used, the error trail information refers to the line number inside the function but it does not report the line number of the call-site (calling function or proctype body). When macros are used, it reports the line number of the call-site. I prefer to use inline functions to macros in the models (like I do very much in C/C++). I hate to implement everything in proctype body without inline functions as it lacks clarity in reading the model (especially, when the model gets bigger). So, now, for quickly interpreting and debugging my model, I implement all the abstracted functions using both inline and macros and use a conditional directive (like "#define USE_INLINE 1") and turn it on and off to interpret the error trail information in both cases to debug my model. While this is not extremely tedious, it is quite a bit of work. It would be nice, if SPIN error-trail information shows the call-stack of functions (from proctype body to function A to function B). A depth of 3 or 4 might be more than sufficient, I think. Actually as inline functions are expanded directly and don't have their own scope, even showing call-stack with a depth of 2 might be sufficient for most use-cases, IMHO.

Here is the portion of a simplified model to illustrate a few questions. This models acquire_semaphore and release_semaphore functions.
********************************************
inline acq_sem1(sem)
{
L0:
    atomic {
        if
        ::    sem == 0 -> goto L0
        ::    else -> sem--
    fi
    }
}

inline acq_sem(sem)  // Using do to fix the errors with above inline function
{
    atomic {
        do
        ::    sem == 0;
        ::    else ->
//progress: // warning, progress label inside atomic is invisible
                sem--; break;
        od;
    }
}

inline rel_sem(sem)
{
    sem++;
}

#define MAX_SEM_VAL 2
int sem = MAX_SEM_VAL;

active [3] proctype P()
{
end:
    do
    ::    acq_sem1(sem);
progress:   
        rel_sem(sem);
    od;
}

active proctype Check()
{
end:
    do
    ::    skip;// This is needed to use the progress label
progress:
        assert(sem >=0 && sem <= MAX_SEM_VAL);
    od
}

********************************************
Q-1:
In acq_sem1, no matter where I place the label L0, I always get the error "label L0 placed incorrectly. Instead of ....., always use ....". My understanding is that I need "atomic", otherwise my assertion would fail, even if I get this to compile. It looks like SPIN has stringent restrictions on using labels and expansion of inline function inside proctype P ends up violating all limitations on where I can place the label, am I right? Or, is there a way to fix the placing of labels to get this to work?

Q-2:
So, I came up with acq_sem() function where I replaced "if" with "do...od" inside "atomic" and that seems to work. Is that the only work-around/solution for problem explained in Q-1?

Q-3:
When I verify this mode for "safety", I get the error "unreached in proctype" for both processes "P" and "Check" and this seems to be a bug, since I do have the "end" labels in both processes "P" and "Check". I got the same error when I did not have the "end" label and that was ok.

Q-4:
As you see in "acq_sem" function, I get a warning for using "progress" label inside "atomic". I am curious whether it is a deficiency that can be fixed or it is a hard-to-solve/unsolvable problem in verification when "atomic" has "progress" label. I moved the "progress" label to process "P" after calling "acq_sem". Hope that is the right way to fix it.

Q-5:
Can I use ltl formulae instead of "proctype Check" to achieve the same? I see that ltl formulae can be used inline. But, I do not find documentation "how" or examples. I have the "SPIN Model Checker" book. But, I think this is a new feature. Could you please point me to some documentation and examples of using inline ltl in SPIN models? Are there any limitations doing that as opposed to using never claims separately? Also, some documentation and examples on how to use "claim name" and "use claim" in iSpin. I have used sometime back using xSpin but iSpin seems to be different and cannot find how to use this feature correctly.

Q-6:
Is there a way to attach model files (.pml) to forum post? That would help simplify explanation and I can use line-numbers,etc to refer to in the post.

Thanks a lot in advance for any help.

In several window panes (syntax check, verification, simulation), it would be nice to give shortcut keys or buttons to select all the text and delete or to clear the entire window pane. Now, I need to select and scroll the entire window pane and delete. Ctrl+A does not select all text. It has been a while since I used xSpin, but I remember I was able to do these in xSpin.