promela - как я могу инициализировать массив за один раз?

Question

Я бы идеально, как что-то вроде этого:

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

Но, насколько я могу сказать, что не работает. Есть ли способ сделать это, это не так?

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

Answer 1

Это часть языка Promela:

// 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 и проверить

# 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