Spinroot

A forum for Spin users

You are not logged in.

#1 2014-03-11 15:51:58

Mara
Member
Registered: 2012-05-30
Posts: 24

Help in understanding a timeout behaviour.

Dear Spin Gurus,
I wrote a Promela program in which I placed into an atomic instruction some variable modification. Since I wanted to generate as much counterexamples as possible for the invariant (LC00007 <= 2)  I  placed, as I usually do, an assert clause right after the variable modifications.
If I execute the program I obtain 658 traces.

After I wanted to check the same invariant at timeout. I (erroneously)  placed the timeout clause just before the assert, as shown in the code below. I know that the best way to do it is placing it as an alternative choice in the do clause, but I decided to see what was coming out from this.

I was expecting to find nothing: since each timeout is in a guarded sequence that will not be executable at timeout I expected  that the timeout should never be fired.
At my surprise, this program generates exactly the same traces of the one without the timeout.
How is it possible? What I'm missing? Why the sequence
timeout -> assert (LC00007 <= 2)
is executed also when the timeout clause is false?

Please help me in understanding what I'm missing.
Mara

/* THE (GLOBAL) VARIABLES*/
 byte LC00001 = 2;
 byte LC00002 = 0;
 byte LC00003 = 2;
 byte LC00004 = 2;
 byte LC00005 = 2;
 byte LC00006 = 2;
 byte LC00007 = 2;

/* */

proctype R_proc()
	{
	do
	:: atomic{((LC00001 > 0))  -> (LC00001=LC00001-1; LC00002=LC00002+1; timeout -> assert (LC00007 <= 2))} /* REACTION NUMBER 1: 1 LC00001-->1 LC00002*/
	:: atomic{((LC00002 > 0))  -> (LC00002=LC00002-1; LC00003=LC00003+1; timeout -> assert (LC00007 <= 2))} /* REACTION NUMBER 2: 1 LC00002-->1 LC00003*/
	:: atomic{((LC00003 > 0) && (LC00004 > 0))  -> (LC00003=LC00003-1; LC00004=LC00004-1; LC00005=LC00005+1; LC00006=LC00006+1; timeout -> assert (LC00007 <= 2))} /* REACTION NUMBER 3: 1 LC00003 + 1 LC00004-->1 LC00005+1 LC00006*/
	:: atomic{((LC00005 > 0))  -> (LC00005=LC00005-1; LC00003=LC00003+1; timeout -> assert (LC00007 <= 2))} /* REACTION NUMBER 4: 1 LC00005-->1 LC00003*/
	:: atomic{((LC00003 > 0))  -> (LC00003=LC00003-1; LC00007=LC00007+1; timeout -> assert (LC00007 <= 2))} /* REACTION NUMBER 5: 1 LC00003-->1 LC00007*/

	od
	}

	
/* start the process*/
	init{
			run R_proc()
	}
	

Offline

#2 2014-03-13 03:04:19

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Help in understanding a timeout behaviour.

there is only one process here (R_proc)
if it chooses any of the options with the timeout in the middle, it will get stuck at that point.
then timeout will be enabled to relieve the system out of the hang state, and it can then continue executing

Offline

#3 2014-03-13 14:56:43

Mara
Member
Registered: 2012-05-30
Posts: 24

Re: Help in understanding a timeout behaviour.

Ok, and this explains why the timeout is fired also inside the  atomic sequence, even if it is blocked.

However it is still not clear to me why it generates as many counterexample as if the timeout was not there.
I mean, if you remove the timeout, you obtain 658 counterexamples, that are generated in the intermediate states between the initial and the final (i.e. timeout) ones.
And if you put the timeout clause directly into the do cycle, you obtain only the 3 counterexamples corresponding to the final, timeout states.

So, why the assert is executed also in all the intermediate states if there is the timeout guard before?

Sorry if I insist, but reasoning in Promela is quite different than reasoning in a "normal" imperative language.

Thank you, very much

Mara

Offline

#4 2014-03-13 16:17:24

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Help in understanding a timeout behaviour.

because there is no other option to continue executing at that point....
if the timeout wasn't enabled, the system would be deadlocked....

Offline

#5 2014-03-18 10:31:25

Mara
Member
Registered: 2012-05-30
Posts: 24

Re: Help in understanding a timeout behaviour.

Sorry if I insist, but the generated counterexamples are not in the final states. Only three counterexamples are generated at timeout, since in this model only three deadlock (final) states exist.

However, the assert is fired also in non-deadlock conditions, and this is really strange, since the instruction
timeout -> assert(..)
in my understanding should be fired ONLY at timeout not ALSO at timeout. Indeed, if you run the program searching for assert violations you obtain also the errors that are not corresponding to the timeout condition, i.e.  the assert is fired also when the system is not in the deadlock state, and generates counterexample in all the intermediate states that lead to the deadlock ones.

I hope that I have been more clear on what I would like to know. I don't want to know why the assert is fired at timeout, I understand that the surrounding atomic clause is ignored at timeout, to avoid the deadlock. But I do not understand why the assert is executed also when timeout is false and the instruction  timeout -> assert(..) should not be executed.

Thank you very much for your patience,

Mara

Offline

#6 2014-03-18 17:01:32

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Help in understanding a timeout behaviour.

Atomic sequences are only atomic until they block.
So if a blocking statement is executed, the atomicity is lost.
So in this case, when the execution stops at the timeout (which initially will be false)
then atomicity is lost.  It can be regained once Spin determines that the system as a whole
is blocked (which it is in this case since there is only one process), and timeout is set to 'true.'
At this point any process can start executing -- including the blocked one (but in this case that
is still the only process of course).
Does that clarify anything?

Offline

Board footer

Powered by FluxBB