When looking at the outline window, Epispin does not recognise init{} as a name, but mentions the skip occurring inside as the name of the init clause.

active proctype p1() {

skip;

}

active proctype p2(){

skip;

}

init {

skip;

}

When you change the skip into

init {

L4: goto L4;

L5: skip;

}

It will recognise L4 as the name of the init clause.

As init in Spin is unique, why not call it init?

This “error” leads to a question;

Obviously, in Java there are no goto’s and no labels, so no one has thought of entering them in the outline view.
In Spin, goto’s and labels are used quite often. Need for an addition?

Submitted by Kees Pronk on 9 September 2011 at 17:49