When a memory hungry promela program is verified, there are (at least) three problems;

1- the Stop button is not functioning

2 - the output of the verifier is not displayed in the console window.
More precise: the output of the verifier is displayed only after the pan process has been killed (using the system monitor, or, by pan itself).

3 - It is quite difficult to kill the pan program.

Compare the verification of the below program in epispin with the way ispin handles this.
Also note how/when the error message that the standard search depth is too small is displayed.
Please have the System Monitor switched on.
…

mtype = {aap, noot, mies, wim, zus};

chan s11 = [3] of {mtype}; // sending and receiving to/from yourself

chan s12 = [3] of {mtype}; // sending s1 to/from s2

chan s21 = [3] of {mtype};

chan s23 = [3] of {mtype}; // sending s2 to/from s2

chan s32 = [3] of {mtype};

chan s33 = [3] of {mtype}; // sending s3 to from s3

//
active proctype f1() {

byte ff1 = aap;

do

:: s11 ? ff1;

:: s21 ? ff1;

:: s12 ! ff1;

:: s11 ! ff1;

od;

}

active proctype f2() {

byte ff2 = noot;

do

:: s12 ? ff2;

:: s32 ? ff2;

:: s23 ! ff2;	

:: s21 ! ff2;	

od;

}

active proctype f3() {

byte ff3 = wim;

do

:: s23 ? ff3;

:: s33 ? ff3;

:: s33 ! ff3;

:: s32 ! ff3;

od;

}

init{

skip;

}

…

Submitted by Kees Pronk on 26 August 2011 at 23:23

The output is now printed in a separate Java thread, so EpiSpin does not hang anymore when a long verification run is started. Also, the output is shown in real-time now instead of when the verification is finished. Both improvements are also applied on simulation runs.

The stop button is working now, although not with the same functionality as iSpin has. iSpin still gives the result of a verification run when it is stopped, while EpiSpin does not.

In version 1.0.4, the Stop button will behave the same as in iSpin, meaning that if a verification run is stopped, the result of the verification is still shown in the output.