ГОСТ Р ИСОМЭК ТО 10023-М
[dir-Request]
•—> t?ta : TAddress ?tcei : TCE1 ?tsp : TSP {IsTReq(tsp)J ;
TCEPHalf
t] (dir)
dir-Indication]
—> t?ta : TAddress ?tcei : TCEI ?tsp : TSP (IsTInd(tsp)] ;
TCEPHalf
It] (dir)
endproc (* TCEPHalf •)
12.3 М е ж о к о н е ч н ы йк е д е т е р м и н и з м
12.3.1
Общее описание
Как было сказано выше, TCReqToInd параметризуется исто
рией запросов rh. выполненных на одном конце, которые могут
влиять на возможные будущие индикации на другом конце. Зна
чения вида TRcqHistory являются основными последовательностя
ми. на которых определены некоторые операции, позволяющие
рассматривать только влияющие элементы истории(подробнее
см. 12.3.2).
Непосредственная форма определения TCReqToInd — это очень
простая праворекурснвная форма. В любой момент времени про
цесс TSPE%’ent специфицирует ограничения на следующее наблю
даемое событие; первый параметр TSPEvent — это основа пред
ставления недетерминиэма (операция Tops определена в12.3.2).
После выполнения этого события TCReqToInd выполняется с об
новленным значением параметра.
process TCReqToInd [t] (rh : TreqHistory) : noexit : —
TSPEvent [t] (Tops(rh), rh) > accept rh1 : TReqHistory in
TCReqToInd ft) (rhl)
endproc (* TCReqToInd •)
12.3.2
Определение данных
Первое определение обеспечивает основную конструкцию исто
рий примитивов запроса посредством операций NoTReqs (пустая
история) и OnTopOf (для расширения истории более ранним зап
росом). Также введены еще несколько булевых функций с обычной
интерпретацией.
П р и м е ч а н и е — Ради полноты OnTopOf нужно определять твкже и для
случая, когда ее первый аргумент — индикация; и атом случае история остает-
26