Spinroot

Maxvonhippel

Member

Registered: 2019-09-13

Posts: 20

[SOLVED] What is my state size?

I have a model of TCP:

mtype = { SYN, ACK, FIN, SYN_ACK, FIN_ACK }

// Declare and run our test for 2 talking peers!
chan AtoB = [1] of { mtype };
chan BtoA = [1] of { mtype };

/* peer is a peer in a TCP connection conversation.
 * currently we model only 2 peers at once, in conversation.
 */
proctype peer(chan incoming, outgoing) 
{
CLOSED:
	do
	:: goto LISTEN; 				  // Listen
	:: outgoing ! SYN; goto SYN_SENT; // Connect
	od
LISTEN:
	if
	:: incoming ? SYN -> outgoing ! SYN_ACK; goto SYN_RECEIVED;
	fi
SYN_RECEIVED:
	if
	:: incoming ? ACK -> goto ESTABLISHED;
	fi
// etc.
}

init
{
	atomic { 
		run peer(AtoB, BtoA); 	// runs peerA
		run peer(BtoA, AtoB); 	// runs peerB
	}
}

When I run it, I get that there are only 4 states, which seems pretty unlikely to me:

spin -run TCP.pml
pan:1: invalid end state (at depth 3)
pan: wrote TCP.pml.trail

(Spin Version 6.5.0 -- 17 July 2019)
Warning: Search not completed
	+ Partial Order Reduction

Full statespace search for:
	never claim         	- (none specified)
	assertion violations	+
	cycle checks       	- (disabled by -DSAFETY)
	invalid end states	+

State-vector 48 byte, depth reached 4, errors: 1
        4 states, stored
        0 states, matched
        4 transitions (= stored+matched)
        1 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.000	equivalent memory usage for states (stored*(State-vector + overhead))
    0.287	actual memory usage for states
  128.000	memory used for hash table (-w24)
    0.534	memory used for DFS stack (-m10000)
  128.730	total actual memory usage

On the other hand, if I use the `-D` option, I see lots of states (quite a bit more than 4!) with what appear to be valid transitions:

spin -a TCP.pml && cc -o pan pan.c && ./pan -d -D
STEP 3 peer
	state   1 -(tr   1)-> state  10  [id   0 tp   2] [----L] TCP.pml:19 => goto LISTEN
	state   2 -(tr   6)-> state  19  [id   1 tp   6] [----G] TCP.pml:20 => outgoing!SYN
	state   3 -(tr   1)-> state  19  [id   2 tp   2] [----L] TCP.pml:20 => goto SYN_SENT
	state   4 -(tr   1)-> state  10  [id   0 tp   2] [----L] TCP.pml:19 => goto LISTEN
	state   4 -(tr   6)-> state  19  [id   1 tp   6] [----G] TCP.pml:19 => outgoing!SYN
	state   5 -(tr   1)-> state   4  [id   4 tp   2] [----L] TCP.pml:22 => .(goto)
	state   6 -(tr   1)-> state  10  [id   5 tp   2] [----L] TCP.pml:18 => break
	state   7 -(tr   7)-> state   8  [id   6 tp 505] [----G] TCP.pml:24 => incoming?SYN
	state   8 -(tr   8)-> state  14  [id   7 tp   6] [----G] TCP.pml:24 => outgoing!SYN_ACK
	state   9 -(tr   1)-> state  14  [id   8 tp   2] [----L] TCP.pml:24 => goto SYN_RECEIVED
	state  10 -(tr   7)-> state   8  [id   6 tp 505] [----G] TCP.pml:24 => incoming?SYN
	state  11 -(tr   1)-> state  14  [id  10 tp   2] [----L] TCP.pml:26 => .(goto)
	state  12 -(tr   9)-> state  27  [id  11 tp 505] [----G] TCP.pml:28 => incoming?ACK
	state  13 -(tr   1)-> state  27  [id  12 tp   2] [----L] TCP.pml:28 => goto ESTABLISHED
// etc

Am I misunderstanding one output or the other?  Presumably, there is a bug in my model - and I am happy to debug it.  But I'm having trouble doing so, without understanding what the `Spin` output means.

Thank you!

Last edited by Maxvonhippel (2019-09-23 16:02:53)

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: [SOLVED] What is my state size?

4 states explore until it found a deadlock
you can use ./pan -c0 to explore all states

Maxvonhippel

Member

Registered: 2019-09-13

Posts: 20

Re: [SOLVED] What is my state size?

This solved my problem, thank you!