CSP-подобные синхронизации

Question

Я пытаюсь использовать механизм синхронизации, подобный CSP, и я не понимаю, почему начальное состояние следующей модели является тупиком:

const int N = 2;
chan a;

process Processes(int [1,N] pid) {
    state A, B;
    init A;
    trans A -> B { sync a; };
}

system Processes;

На мой взгляд, 2 процесса синхронизированы по каналу «а» и должны сделать хотя бы один шаг, нет?

Answer 1

Системное объявление должно включать объявление IO:

P1=Processes(1);
P2=Processes(2);

system P1, P2;

IO P1 {a}
IO P2 {a}

К сожалению, объявление IO не понимает параметров шаблона, поэтому я использовал полное создание экземпляра с конкретными именами.

Существует также опция «Скромный» для включения различной семантики обновления, например:

x=y+z

использует старое значение y и z (до синхронизации) в случае одновременного изменения y и z.