Previous Page  12 / 18 Next Page
Information
Show Menu
Previous Page 12 / 18 Next Page
Page Background

В.С. Буренков, С.Р. Иванов

60

ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2017. № 1

 

: ?

1

0

0

, |

( ( ))

0 ( ) ... ,

, , , , , ,

, , , , , ,

g c x

i

i

k

i

i

n

i

n

l

l

g len c k

c v v

rrc

l

l

l

l

l

l

           

 

         

(5)

где

1

:

x v

   

и

2

:

.

k

c v v

     

В процессе исполнения запроса только одно правило

, 0

,

i

rrc

i n

 

может по-

рождать переходы. В этих случаях изменение пометки обусловлено изменением

значения переменной

x

. Определим, какие значения может принимать

x

вследствие

применения правила

, 0

.

i

rrc

i n

 

Для этого рассмотрим фрагмент вычисления

0 1 1 2

m m

s s

s

  

системы переходов

.

TS

В таком случае переход

1

m m

s

s

получен

вследствие применения правила

1

.

i

concrete

rrc Rulesr

В моделях либо

0

i

(сообще-

ние извлекает процесс, представляющий системный коммутатор

home

-процессора),

либо

0

i

(сообщение извлекает процесс-запросчик с номером

i

). Факт примене-

ния правила означает, что условие

 

0

len c

k

  

выполнено. В свою очередь,

это позволяет записать

 

1

.

k

c v v

  

Следовательно, из

1

, ,

m

  

находится

k

членов, каждый из которых имеет вид

.

i

  

Таким образом, после осуществления

перехода

1

,

m m

s

s

переменная

х

будет принимать одно из значений из множества

X

, всех ранее отправленных по каналу значений, причем

1

k

v v

является переста-

новкой этого множества.

Указанному множеству правил

1

concrete

Rulesr

в абстрактной модели соответ-

ствует множество правил

1

,

1

,

| 0 3,1

,

abstract

i

i j

Rulesr

rra raa

i

j S

   

где

 

1

abs

S dom c

— число различных отправляемых значений в операторах

отправки сообщения, соответствующих операторам приема сообщения из

1

.

c C

Выбор правила из этого множества недетерминирован, т.

е.

1

1

1

:

concrete

abstract

Transr Rulesr

Rulesr

— мультиотображение. Первый тип элемен-

тов этого множества имеет вид

: ?

1

0

3

0

3

,

|

( ( ))

0

( ) ...

,

, , , , ,

,

, , , , ,

,

abs

g c x

i

i

abs abs

abs

abs

abs

l

i

i

abs abs

i

abs abs

l

l

g

len c l

c v v

rra

l

l

l

l

l

l

      

    

          

где

1

:

abs

abs

x v

   

и

'

2

:

abs

abs

l

c v v

    

. Здесь

l

может принимать значе-

ния 1, 2.

Согласно абстрактным преобразованиям,

 

1

, 0 2,

i

i

Transr rrc rra i

 

 

1

3

, 2

.

i

Transr rrc rra i n

 

Определим, какие значения при этом может принимать переменная

x

в абстрактной модели в состоянии

1

.

m

f s

Рассмотрим фрагмент вычисле-

ния

 

 

 

0

1

1

2

( ) Α ( )Α Α ( )

m m

f s

f s

f s

  

системы переходов

.

abs

TS

Здесь

 

 

Α :

.

abs

Act

Act

  

Условие

 

0

abs

len

c

l

 

может быть выполнено

только, если из

 

 

1

Α ,

, Α

m

  

было

l

членов, каждый из которых порожден