Каналы в Promela

Каналы в языке Promela являются объектами первого порядка, то есть они могут быть переданы через канал как и любое другое значение. Это позволяет формировать динамическую структуру связей.

proctype A ( chan ptr )
{
   chan dest;  /* Объявляем канал */
   ptr ? dest; /* Считываем канал передачи из канала-параметра */ 
   dest ! 1;   /* Записываем в канал число 1 */
}

init {
   chan a = [ 1 ] of { chan }; /* Создаем канал для передачи канала */
   run A(a);                   /* Запускаем процесс с параметром-каналом */
   chan dest = [1] of {int};   /* Создаем канал назначения */
   a ! dest;                   /* Записываем в канал назначения канал передачи */
   int res;
   dest ? res;                 /* Считываем из канала передачи число */
   if
   :: res == 1 -> printf("OK") /* Убеждаемся, что считалась единица */
   fi
}

Каналы Promela можно использовать для моделирования указателей произвольной вложенности.