Редактирование: ВПнМ/Теормин
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
ПРЕДУПРЕЖДЕНИЕ: Длина этой страницы составляет 90 килобайт. Страницы, размер которых приближается к 32 КБ или превышает это значение, могут неверно отображаться в некоторых браузерах. Пожалуйста, рассмотрите вариант разбиения страницы на меньшие части.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 1189: | Строка 1189: | ||
=== Язык Promela. Каналы сообщений. Операторы отправки и приёма сообщений. Тип mtype. синхронная и асинхронная передача сообщений. === | === Язык Promela. Каналы сообщений. Операторы отправки и приёма сообщений. Тип mtype. синхронная и асинхронная передача сообщений. === | ||
- | '''Каналы сообщений''' | ||
- | * сообщения передаются через каналы (очереди/буфера ограниченного объёма) | ||
- | * каналы бывают двух типов: | ||
- | ** буферизованные (асинхронные), | ||
- | ** небуферизованные (синхронные, рандеву); | ||
- | |||
- | chan x = [10] of {int, short, bit}; | ||
- | |||
- | '''Операторы отправки и приема сообщений''' | ||
- | Отправка: ch!expr1,...exprn | ||
- | * значения expri соответствуют типам в объявлении канала; | ||
- | * выполнимо, если заданный канал не полон; | ||
- | Приём: ch?const1 или var1,...constn или varn | ||
- | * значения vari становятся равны соотв. значениям полей сообщения; | ||
- | * значения consti ограничивают допустимые значения полей; | ||
- | * выполнимо, если заданный канал не пуст и первое сообщение в канале соответствует всем константным значениям в операторе приёма сообщения; | ||
- | |||
- | '''Объявление mtype''' | ||
- | * способ определить символьные константы (до 255) | ||
- | |||
- | Объявление mtype: | ||
- | mtype = {foo, bar}; | ||
- | mtype = {ack, msg, err, interrupt}; | ||
- | |||
- | Объявление переменных типа mtype: | ||
- | mtype a; | ||
- | mtype b = foo; | ||
- | |||
- | '''Cинхронная и асинхронная передача сообщений''' | ||
- | * Асинхронная передача | ||
- | ** асинхронные сообщения буферизуются для последующего приёма, пока канал не полон, | ||
- | ** отправитель блокируется, когда канал полон, | ||
- | ** получатель блокируется, когда канал пуст. | ||
- | * Синхронная передача | ||
- | ** ёмкость канала равна 0 - chan ch = [0] of {mtype}; | ||
- | ** передача сообщений методом “рандеву”, | ||
- | ** не хранит сообщения, | ||
- | ** отправитель блокируется в ожидании получателя, и наоборот, | ||
- | ** отправка и приём выполняются атомарно. | ||
- | |||
=== Язык Promela. Каналы сообщений. Вспомогательные операции с каналами сообщений. === | === Язык Promela. Каналы сообщений. Вспомогательные операции с каналами сообщений. === | ||
'''Другие операции с каналами''' | '''Другие операции с каналами''' |