promela - how do i initialize an array at one time?

Question

I'd ideally like something like this:

byte things[10] = {1,4,5,6,13,14,15,16,10,12};

But as far as I can tell that doesn't work. Is there a way to do this that's not like this?

things[0] = 1
things[1] = 4
things[2] = 5
...

Answer 1

This is part of the Promela language:

// foo.pml
byte bar[5] = { 1,2,3,4,5 }

init {
  printf ("bar[0]: %d\n", bar[0]);
  printf ("bar[4]: %d\n", bar[4]);

  assert (1 == bar[0]);
  assert (5 == bar[4])
}

Simulate and verify

# Simulate
$ spin foo.pml
      bar[0]: 1
      bar[4]: 5
1 process created

# Verify
$ spin -a foo.pml
$ gcc -o foo pan.c
$ ./foo
hint: this search is more efficient if pan.c is compiled -DSAFETY

(Spin Version 6.3.2 -- 17 May 2014)
    + Partial Order Reduction

Full statespace search for:
    never claim             - (none specified)
    assertion violations    +
    acceptance   cycles     - (not selected)
    invalid end states  +

State-vector 20 byte, depth reached 5, errors: 0
        6 states, stored
        0 states, matched
        6 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

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


unreached in init
    (0 of 5 states)

pan: elapsed time 0 seconds