----
いつも確認したくなること
----
その1
初期化しないと0が入る
#highlight(linenumber,promela){{bit n1;
bool n2;
byte n3;
short n4;
int n5;
mtype n6;
active proctype P1(){
printf("bit:%d\n", n1);
printf("bool:%d\n", n2);
printf("byte:%d\n", n3);
printf("short:%d\n", n4);
printf("int:%d\n", n5);
printf("mtype:%d\n", n6);
} }}
結果($spinオプションなし)
#aa(blockquote){{ bit:0
bool:0
byte:0
short:0
int:0
mtype:0
1 process created }}
