Spinroot

Artemis

Member

Registered: 2015-01-20

Posts: 1

Enhancement: Output current status also if transitions change a lot

Hi,

even though this is no bug I though it might well fit here.

I have a model that does not have many states but an huge amount of possible transitions.

My problem is that I cannot see any progress when watching the pan output as the states never reach the marker of 1 million stored states but have transitions in the area of 70 million and above. At first I just thought that the verifier somehow hung and only after killing it at different times I saw a difference in the number of transitions explored.

Currently I have made to following changes to pangen1.h. I guess it could be implemented in a better way but it does the job for me. Maybe you can think about including this/a similar functionality, maybe not ;-)

I changed the following lines (2829-2838)

	"			if (!kk)",
	"			{	static long sdone = (long) 0; long ndone;",
	"				nstates++;",
	"#if defined(ZAPH) && defined(BITSTATE)",
	"				zstates += (double) hfns;",
	"#endif",
	"				ndone = (ulong) (nstates/(freq));",
	"				if (ndone != sdone)",
	"				{	snapshot();",
	"					sdone = ndone;",

to:

	"			if (!kk)",
	"			{	static long sdone = (long) 0; long ndone;",
	"				static long sdone2 = (long) 0; long ndone2;",
	"				nstates++;",
	"#if defined(ZAPH) && defined(BITSTATE)",
	"				zstates += (double) hfns;",
	"#endif",
	"				ndone = (ulong) (nstates/(freq));",
	"				ndone2 = (ulong) ((nstates+truncs)/(10*freq));",
	"				if (ndone != sdone || ndone2 != sdone2)",
	"				{	snapshot();",
	"					sdone = ndone;",
	"					sdone2 = ndone2;",

This is the diff:

@@ -2828,14 +2828,17 @@
    "           }",
    "           if (!kk)",
    "           {   static long sdone = (long) 0; long ndone;",
+   "               static long sdone2 = (long) 0; long ndone2;",
    "               nstates++;",
    "#if defined(ZAPH) && defined(BITSTATE)",
    "               zstates += (double) hfns;",
    "#endif",
    "               ndone = (ulong) (nstates/(freq));",
-   "               if (ndone != sdone)",
+   "               ndone2 = (ulong) ((nstates+truncs)/(10*freq));",
+   "               if (ndone != sdone || ndone2 != sdone2)",
    "               {   snapshot();",
    "                   sdone = ndone;",
+   "                   sdone2 = ndone2;",
    "#if defined(AUTO_RESIZE) && !defined(BITSTATE) && !defined(MA)",
    "                   if (nstates > ((double)(ONE_L<<(ssize+1))))",
    "                   {   void resize_hashtable(void);",

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: Enhancement: Output current status also if transitions change a lot

interesting, will consider this