24. Семантика языка И-ЛИБО систем

24.1. Поведение автомата

Семантика языка И-ЛИБО систем - это применение правил традиционной семантики к языку И-ЛИБО СИСТЕМ.

То есть, формуле согласованной системы непосредственно ставится в соответствие её значение - конструкция автомата, а ей, в свою очередь - поведение (функционирование), заключающееся в определении рабочего профиля данного автомата.

	согласованная система	произвольная система ВС
корректное испытание	рабочеее состояние совпадает с одним из состояний, образующих корневую ВС
ошибочное испытание	НЕ принадлежит рабочему профилю

Надо только учесть, что для систем, хоть сколько-нибудь приближенных к реальности, к техническим системам, обычно не бывает никакого сигнала об ошибке, а просто поведение становится непредсказуемым, с чем, собственно, и стоит задача побороться.

Поскольку основу автомата образует дерево разбиения, поведение можно определить рекурсивно согласно тому, как распространяется активность от корня до листьев, образованных операторами:

•	испытание (автомата, построенного на текущем поддереве) начинается с того, что считаются уже установленными значения внешних переменных и только на его головной блок пеоступает сигнал активности, все прочие его блоки находятся в пассивном состоянии
•	дальнейшее распространение активности в сторону листьев зависит от установленных значений внешних переменных и от типа головноой вершины:
	a.	оператор, описываемый формулой атома, при поступлении сигнала активности либо подтверждает значение внешней переменной, либо выдаёт ошибку при несовпадении значений: Вход Выход активность значения внешней переменной/собственное подтверждение ошибка + совпадают + - + НЕ совпадают - ERROR - совпадают - - - НЕ совпадают - -
	b.	блок состояния, описываемый формулой состояния, при поступлении сигнала активности транслирует его ко всем образующим его операторам
	c.	базовый блок, описываемый формулой ВС, при поступлении сигнала активности проверяет, с каким ключом ассоциировано текущее распределение значений внешних переменных, а затем транслирует сигнал активности соответствующему блоку состояния
	d.	узел типа И-, описываемый соответствующей формулой:
		•	при отсутствии коммутатора просто транслирует сигнал активности всем непосредственно подчинённым блокам
		•	при наличии коммутатора вычисляет проекцию текущего внешнего состояния на базис коммутатора и сравнивает полученное состояние со всеми ключами
			•	если совпадение имеет место ровно с одним ключом, то сигнал активности транслируется всем непосредственно подчинённым блокам
			•	в противном случае фиксируется ошибка
	e.	узел типа ЛИБО-, описываемый соответствующей формулой, вычисляет проекцию текущего внешнего состояния на базис селектора и сравнивает полученное состояние со всеми ключами
		•	если совпадение имеет место ровно с одним ключом, то сигнал активности транслируется соответствующему непосредственно подчинённому блоку
		•	в противном случае фиксируется ошибка
•	для пунктов b,c,d определены новые вершины, получившие сигнал активности, а потому являющиеся корнями поддеревьев, для которых рекурсивно применяется данный алгоритм
•	блоки, оставшиеся в пассивном состоянии, на ход испытания не влияют

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

• "мгновенно" работает каждый блок
• "мгновенно" срабатывает связка "СЛЕДУЕТ" между разными блоками автомата - это и конструктивная и функциональная связка;

Как видно, информацию о поведении сложного автомата в конкретном испытании можно разделить на перечисление активных блоков (поток управления) и на поток данных, образованным состоянием того набора внешних переменных, которые ипользуются при этом в его активных:

• операторах
• ключах его коммутаторов
• ключах его селекторов

Объединение всевозможных потоков управления совпадает множеством всех блоков (см. Теорема 24.7), а объединение потоков данных - с ВС головного блока, получаемой алгоритм синтеза(см. Теорема 24.8).

Алгоритм синтеза в качестве дополнительного положительного результата определяет ВС головного блока.

Любое рабочее состояние профиля оказываетсяё прообразом одного из состояний этой ВС, и наоборот - для каждого состояния этой ВС найдётся его прообраз в профиле (см. Теорема 24.4).

Назад Вперёд