Недетерминированные автоматы в проектировании систем параллельной обработки. Вашкевич Н.П. - 173 стр.

        Перейдем теперь к определению формального описания основных
событий, реализуемых в рассматриваемом алгоритме управления процессами
и представляемых в дальнейшем в виде системы канонических уравнений НД
    СКУ. В начале рассмотрим формализацию самых главных событий,
определяющих входы процессов в свои критические участки и обозначенные
       в предыдущих разделах символом S ik (где i - номер процесса).
           Для нашего варианта задачи «производители-потребители»
 используются только два взаимодействующих процесса. Для них указанные
   события, для удобства дальнейшего анализа, представим, на основании
            системы уравнений (6.9), в следующем общем виде:
                              1                 1    1           1       1
                            S k (t  1)  S вз S кo  S k S n ,
                                                                               (6.17)
                                                                      2
                            S k2 (t    1)      2 2
                                               S вз S кo      S 2k S n ,
  где S 1n и S 2n - сокращенные обозначения событий, свидетельствующих о
                     факте окончания процедуры записи и чтения из буфера и
                        обеспечивающих выход процессов производителя и
                    потребителя из своих критических участков соответственно.
      Выражения для событий S 1вз и S вз
                                      2
                                         определятся, исходя из соотношения
                      (6.10), следующим образом:
                                       1        2          2         1
                                      S вз  S k , S вз  S k .                (6.18)
         Представление условий зарождения событий S 1k и S 2k в (6.17), в
      отличие от представления их в системе уравнений (6.18), в виде
  объединенных событий S 1кo  ( S1 S 1пр ) и S кo
                                                2           2
                                                    (S 2 S пр ) объясняется тем, что
     события S 1пр и S пр
                       2
                          , входящие в них, зависят не только от состояния
          согласующего буфера, но также и от событий S1 и S 2 .
       Для получения описаний событий S 1кo и S кo
                                                2
                                                   воспользуемся прямой
  таблицей переходов (ПТП), определяющей эти события. ПТП (табл.6.1)
      строится на основе требований к рассматриваемому алгоритму
                     взаимодействия двух процессов.




                                                                                    173