как объявить Размер сообщения в PROMELA?

Синтаксис для объявления канала, например:

chan ab = [16] of { short }

ab — идентификатор, привязанный к каналу. 16 — количество сообщений в канале. short — это тип данных каждого сообщения.

Когда вы указываете тип сообщения, у вас есть ряд дополнительных опций:

char ab = [16] of { byte, short, bit }

который создает канал с каждым сообщением: byte, short и bit. В таком случае часто лучше создать новый тип с:

typedef message {
  byte operator;
  short data;
  bit what;
};

а потом

chan ab = [16] of { message }