Spinroot

A forum for Spin users

You are not logged in.

#1 Re: General » [SOLVED ... it is deterministic] Make Spin output deterministic » 2020-11-11 21:23:40

By the way, for anyone who has this issue and comes across this post in the future - this bug is caused when you write code that uses Spin as a backend, but you don't make sure that your code deletes whatever models it wrote (and any trail files or other files output by Spin) after each execution of Spin.  It's just a side-effect bug from extra files lying around.  (So, not Spin's fault, basically automated user error.)

#2 Re: General » Model is too large » 2020-08-23 22:20:27

My experience so far has been that the following techniques reduce model size:

1. Whenever possible use rendezvous communication, i.e., use channels with size 0 instead of size > 0.
2. Minimize the number of channels even if this means increasing the number of possible symbols to be sent over a channel.  For instance, if you have A and B processes, with A sending ack to B and B sending ack to A over two channels AtoB and BtoA, you could reduce this to one channel AandB and have messages ack_from_A and ack_from_B.
3. As much as possible encode logic using labels and goto statements instead of higher-level (more C-like) constructs.  So, loosely, try to make the code look more like assembly, and less like C.
4. Use mtypes instead of shorts/integers/doubles/etc. as much as possible as they force you to clarify your ideas in as finite of a manner as you can.

Would you agree with all this advise?  Are there any other general tips you would reccomend?

Thank you!

#3 Re: General » [SOLVED] Best practice for bounded signed integers? » 2020-08-14 00:22:22

Thank you for the quick response Gerard, I appreciate it.  Wiring my own arithmetic seems a bit ugly, although of course doable.  Is there some way I could alternatively just tell Spin to ignore states under some condition?  Then I could say, "ignore any states where such-and-such integers are out-of-bounds."  I know this is a feature in Alloy, which makes me think maybe it is available in Promela ... if not no worries, I can work out the arithmetic.  Thank you!

#4 General » [SOLVED] Best practice for bounded signed integers? » 2020-08-08 01:56:02

Maxvonhippel
Replies: 3

Suppose I want to deal with some bounded signed integers, such as, -30 through 30.  In particular, what I want is something like this:

chan example = [1] of { -30 ... 30 }

What is the best way to accomplish this?  If I didn't want negative numbers I think I could use an unsigned of only so-many bits, and I guess I could do that with a sign-bit to get what I want, but it seems kind of inelegent.

Thank you!

#5 Re: Bug Reports » Excessive warnings thrown for `spin -run` » 2020-08-01 04:14:01

Thank you Gerard, I appreciate it!  I made a tool that uses Spin as a back-end, and these warnings can be troublesome smile

#6 Bug Reports » Excessive warnings thrown for `spin -run` » 2020-07-30 19:00:38

Maxvonhippel
Replies: 3

When I run `spin` on a fairly simple model, I get tons of warnings:

````
pan.c: In function ‘make_trail’:
pan.c:2172:19: warning: ‘%d’ directive writing between 1 and 10 bytes into a region of size between 1 and 512 [-Wformat-overflow=]
2172 |   sprintf(fnm, "%s%d.%s",
      |                   ^~
pan.c:2172:16: note: directive argument in the range [1, 2147483647]
2172 |   sprintf(fnm, "%s%d.%s",
      |                ^~~~~~~~~
In file included from /usr/include/stdio.h:867,
                 from pan.c:7:
/usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 3 or more bytes (assuming 523) into a destination of size 512
   36 |   return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1,
      |          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
   37 |       __bos (__s), __fmt, __va_arg_pack ());
      |       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
pan.c:2180:22: warning: ‘__builtin___sprintf_chk’ may write a terminating nul past the end of the destination [-Wformat-overflow=]
2180 |   sprintf(fnm, "%s.%s", MyFile, tprefix);
      |                      ^
In file included from /usr/include/stdio.h:867,
                 from pan.c:7:
/usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 2 or more bytes (assuming 513) into a destination of size 512
   36 |   return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1,
      |          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
   37 |       __bos (__s), __fmt, __va_arg_pack ());
      |       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
pan.c:2187:21: warning: ‘%d’ directive writing between 1 and 10 bytes into a region of size between 1 and 512 [-Wformat-overflow=]
2187 |     sprintf(fnm, "%s%d.%s",
      |                     ^~
pan.c:2187:18: note: directive argument in the range [1, 2147483646]
2187 |     sprintf(fnm, "%s%d.%s",
      |                  ^~~~~~~~~
In file included from /usr/include/stdio.h:867,
                 from pan.c:7:
/usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 3 or more bytes (assuming 523) into a destination of size 512
   36 |   return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1,
      |          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
   37 |       __bos (__s), __fmt, __va_arg_pack ());
      |       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
pan.c:2190:24: warning: ‘__builtin___sprintf_chk’ may write a terminating nul past the end of the destination [-Wformat-overflow=]
2190 |     sprintf(fnm, "%s.%s", MyFile, tprefix);
      |                        ^
In file included from /usr/include/stdio.h:867,
                 from pan.c:7:
/usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 2 or more bytes (assuming 513) into a destination of size 512
   36 |   return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1,
      |          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
   37 |       __bos (__s), __fmt, __va_arg_pack ());
      |       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
pan.c: In function ‘findtrail’:
pan.c:1776:22: warning: ‘%s’ directive writing 5 bytes into a region of size between 0 and 511 [-Wformat-overflow=]
1748 |  tprefix = "trail";
      |            ~~~~~~~   
......
1776 |   { sprintf(fnm, "%s.%s", MyFile, tprefix);
      |                      ^~
In file included from /usr/include/stdio.h:867,
                 from pan.c:7:
/usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output between 7 and 518 bytes into a destination of size 512
   36 |   return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1,
      |          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
   37 |       __bos (__s), __fmt, __va_arg_pack ());
      |       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
pan.c:1787:24: warning: ‘__builtin___sprintf_chk’ may write a terminating nul past the end of the destination [-Wformat-overflow=]
1787 |     sprintf(fnm, "%s.%s", MyFile, tprefix);
      |                        ^
In file included from /usr/include/stdio.h:867,
                 from pan.c:7:
/usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 2 or more bytes (assuming 513) into a destination of size 512
   36 |   return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1,
      |          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
   37 |       __bos (__s), __fmt, __va_arg_pack ());
      |       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
pan.c:1752:23: warning: ‘.’ directive writing 1 byte into a region of size between 0 and 511 [-Wformat-overflow=]
1752 |   { sprintf(fnm, "%s%d.%s",
      |                       ^
In file included from /usr/include/stdio.h:867,
                 from pan.c:7:
/usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output between 8 and 529 bytes into a destination of size 512
   36 |   return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1,
      |          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
   37 |       __bos (__s), __fmt, __va_arg_pack ());
      |       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
pan.c:1764:23: warning: ‘.’ directive writing 1 byte into a region of size between 0 and 511 [-Wformat-overflow=]
1764 |     sprintf(fnm, "%s%d.%s",
      |                       ^
In file included from /usr/include/stdio.h:867,
                 from pan.c:7:
/usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 3 or more bytes (assuming 514) into a destination of size 512
   36 |   return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1,
      |          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
   37 |       __bos (__s), __fmt, __va_arg_pack ());
      |       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
pan.c:1826:21: warning: ‘%s’ directive writing 5 bytes into a region of size between 0 and 511 [-Wformat-overflow=]
1813 |  tprefix = "trail";
      |            ~~~~~~~   
......
1826 |  { sprintf(fnm, "%s.%s", MyFile, tprefix);
      |                     ^~
In file included from /usr/include/stdio.h:867,
                 from pan.c:7:
/usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output between 7 and 518 bytes into a destination of size 512
   36 |   return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1,
      |          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
   37 |       __bos (__s), __fmt, __va_arg_pack ());
      |       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
pan.c:1830:23: warning: ‘__builtin___sprintf_chk’ may write a terminating nul past the end of the destination [-Wformat-overflow=]
1830 |    sprintf(fnm, "%s.%s", MyFile, tprefix);
      |                       ^
In file included from /usr/include/stdio.h:867,
                 from pan.c:7:
/usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 2 or more bytes (assuming 513) into a destination of size 512
   36 |   return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1,
      |          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
   37 |       __bos (__s), __fmt, __va_arg_pack ());
      |       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
pan.c:1816:22: warning: ‘.’ directive writing 1 byte into a region of size between 0 and 511 [-Wformat-overflow=]
1816 |  { sprintf(fnm, "%s%d.%s", MyFile, whichtrail, tprefix);
      |                      ^
In file included from /usr/include/stdio.h:867,
                 from pan.c:7:
/usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output between 8 and 529 bytes into a destination of size 512
   36 |   return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1,
      |          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
   37 |       __bos (__s), __fmt, __va_arg_pack ());
      |       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
pan.c:1820:22: warning: ‘.’ directive writing 1 byte into a region of size between 0 and 511 [-Wformat-overflow=]
1820 |    sprintf(fnm, "%s%d.%s",
      |                      ^
In file included from /usr/include/stdio.h:867,
                 from pan.c:7:
/usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 3 or more bytes (assuming 514) into a destination of size 512
   36 |   return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1,
      |          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
   37 |       __bos (__s), __fmt, __va_arg_pack ());
      |       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
pan:1: invalid end state (at depth 2)
pan: wrote abs.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 148 byte, depth reached 3, errors: 1
        4 states, stored
        0 states, matched
        4 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.001    equivalent memory usage for states (stored*(State-vector + overhead))
    0.279    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



pan: elapsed time 0 seconds
````

Is there a way to make Spin not throw so many warnings?  I am on Linux Mint 20, on a 2018 XPS 13.  Thanks!

#7 Re: General » [SOLVED ... it is deterministic] Make Spin output deterministic » 2020-02-17 22:49:37

You're right, there was a bug elsewhere in my code, unrelated to Spin hmm

Thank you!

#8 Re: General » [SOLVED ... it is deterministic] Make Spin output deterministic » 2020-01-29 17:32:52

I suspect possibly the setting I want is this:

-RSN
Use N as a seed for the random number generator.
Can be used in combination with compilation directives -DT_RAND and -DP_RAND (defined under experimental options below) to randomize the search process. N can be any non-negative integer value.

I will test and see if this works.

To be clear, what I am looking for is an option XXX such that given some tmp.pml, running

spin -run -a XXX tmp.pml

... will create the same trail file every time, if the property is violated.

#9 General » [SOLVED ... it is deterministic] Make Spin output deterministic » 2020-01-29 16:56:26

Maxvonhippel
Replies: 4

I am working on a tool that invokes Spin.  Let's call my tool g3.  So, the user runs

$ g3 [input]

and then in turn g3 makes a new Promela file **tmp.pml**, the contents of which differ depending on the [input], and runs

$ spin -run -a tmp.pml

g3 then processes the piped output and prints a result.  I have unit tests for my code.  When I run my code, I can run it 4 times in a row, and have it pass, fail, fail, pass.  I am quite confident the reason has to do with Spin: I think Spin is finding a different trail file (a different path to the violation of the property in tmp.pml) each time I run it.  I tried making Spin find the shortest trail file using the -i option but this made my tool very slow for larger inputs.  I also tried manually setting the seed (I think the option was -nX where X is the seed) but this did not solve the problem.

How can I make Spin run deterministically, in order to make debugging my tool that invokes Spin easier?

#10 Re: General » [SOLVED] "While not timeout" option? » 2019-12-05 17:55:13

By the way, the -e flag is undocumented under -run when you do spin --.  I know it's documented under ./pan but it would be useful for new users to also include it under -run in the spin -- output.

I'm happy to cut a pull request on github to do this, if you'd like.  Is that the preferred way to contribute?  Or would you prefer to just add it yourself, or is there some other process I should go through?

#11 Re: General » [SOLVED] "While not timeout" option? » 2019-12-05 17:53:54

Fantastic, thank you!  I had totally forgotten about those.

#12 General » [SOLVED] "While not timeout" option? » 2019-12-04 20:20:37

Maxvonhippel
Replies: 4

Hi,

I have in the past written code much like this:

if
:: timeout -> skip;
:: someChan ! someMsg;
fi
if
:: timeout -> skip;
:: someChan ? someOtherMsg;
fi
... etc etc

Is there any way to do this with some sort of while-guard, like

while (! timeout) {
  send and receive stuff
} else {
   handle the fact that you've timed out / reached what would otherwise be a deadlock
}

?  Thank you!

#13 Re: General » [SOLVED] How to step through program? » 2019-10-05 03:59:33

Ok, I wrote a simple Python wrapper.  If anyone thinks they might find this functionality useful, the code is here:

https://gist.github.com/maxvonhippel/838ba96cf31944f4d03561bc0870697f

Best,

Max

#14 General » [SOLVED] How to step through program? » 2019-10-03 03:34:48

Maxvonhippel
Replies: 2

I love the interactive mode, but I would like it to ask me for a choice even when there is only one choice available.

The best option I've found is:

    spin -p -i -w my_great_model.pml

This prints everything, which is nice, but it prints it all at once, instead of stepping through the program.

Is there a way to make the interactive mode step through the program, for instance whenever I press enter?  (If not, I will likely write my own wrapper to do this and share it here.)

Thanks!

#16 General » [SOLVED] What is my state size? » 2019-09-20 22:46:13

Maxvonhippel
Replies: 2

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!

#17 Re: General » [Solved] Storing arbitrary channel message in a variable » 2019-09-17 04:00:54

I was a fool, the answer is obvious - I need to use receive, with < >; ie

byte msg;
myChan ? < msg >;

http://spinroot.com/spin/Man/receive.html

#18 General » [Solved] Storing arbitrary channel message in a variable » 2019-09-17 03:57:06

Maxvonhippel
Replies: 1

I would like to have some logic like:

IF the channel chan1 is not empty:
    Let X = chan1.pop()
    do some stuff with X

But the only way I know how to do this is to explicitly enumerate all possible values of X, ie, if X were of some mtype { BANANA, HOTDOG, MANGO, KOALA }, I would do

mtype tmp;
if
:: chan1 ? BANANA -> tmp = BANANA;
:: chan1 ? HOTDOG -> tmp = HOTDOG;
:: chan1 ? MANGO -> tmp = MANGO;
:: chan1 ? KOALA -> tmp = KOALA;
fi
do some stuff with tmp

Is this the best way to do it?  Or is there some method like the ".pop()" I want that I can use?

Thank you!

#19 General » [Solved] How are states labeled? » 2019-09-16 17:02:02

Maxvonhippel
Replies: 1

I know how variables are labeled: from right to left.  For example:

    mtype:cmdTypes = { Close, Connect, Listen, Timeout, Null }

yields Close = cmdTypes 5, Connect = cmdTypes 4, etc.  This is evident, for example, in the dot.out file produced when I click on the automota view in the GUI.

But how are states labeled?  For instance, if I have a model like this:

proctype awesomeModel(chan some great channel, some other fantastic channel, and yet another superb channel)
{
BANANA:
    if
    :: guard 1 -> goto MANGO;
    :: guard 2 -> do something; goto HOTDOG;
    fi
MANGO:
    if
    :: guard 3 -> do something else; goto BANANA;
    fi
HOTDOG:
    if
    :: guard 4 -> goto PEACH
    fi
... etc etc
}

... then how does Spin assign labels like S0, S1, S2, etc. to the various states?  It seems to me that these correspond monotonically with my labels (e.g., BANANA, MANGO, HOTDOG, PEACH, etc.) and with the "do something"s that happen within them, so I get some sort of partitioning like

Sa0 = BANANA
Sa1 = do something
Sa2 = MANGO
Sa3 = do something else
Sa4 = HOTDOG
Sa5 = PEACH
... etc

where a0 < a1 < s2 < a3 < a4 < a5 < ...

but I am not sure if that is correct, and I am also not sure where these numbers come from since many states don't show up at all (that is to say, { a0, a1, a2, a3, ... } != { 1, 2, 3, 4, ... }).

Any guidance on this front would be much appreciated!

Board footer

Powered by FluxBB