Логический анализ корректности конфигурирования межсетевых экранов
5
ствие каждой нити
*
*
? ?
a A
внешнюю реакцию из множества
! .
A
Процесс
P
, выполняющий множество нитей
* *
*
? (? ) ,
a a S
будем
обозначать
( )
P S
. Значение функции
*
на тех нитях множества
*
?
A
, на которых эта функция не определена и на тех нитях, кото-
рые этому множеству не принадлежат, считается равным
!
e
. Мно-
жество нитей
*
?
a
таких, что
*
*
* *
*
{? ? | ? (? ) }
a A a a S
будем обо-
значать
?
S
.
Популярным языком представления процессов является язык
графов переходов. Для построения графа переходов процесса счита-
ется, что после каждого его восприятия, в том числе пустого, процесс
осуществляет внутреннюю реакцию или, как говорят, переходит во
внутреннее состояние ожидания следующего восприятия. Находясь в
этом внутреннем состоянии, процесс может порождать внешнюю ре-
акцию, в том числе пустую. В графе переходов каждое состояние
процесса изображается кружком, внутрь которого помещается сим-
вол этого состояния; каждому восприятию соответствует стрелка, со-
единяющая состояния этого перехода. Начальное состояние выделя-
ется двойным кружком. На рис. 1 показан граф переходов некоторого
процесса
P
.
b !a
1 1
,
b ,!a
2 2
b ,!a
3 3
?a
1
b
4
,!a
3
?a
2
?a , ?a
1
2
?a
1
?a
2
?a ,?a
1 2
Рис. 1.
Граф переходов процесса
P
Граф переходов процесса позволяет компактно описывать не-
большое множество нитей, в том числе бесконечных. В этих усло-
виях естественным кажется описывать процесс непосредственно
его графом переходов. Но при большой размерности графа такое
описание становится громоздким и ненаглядным. Альтернативой
этому является использование адекватных графу канонических
