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

         Перейти к выполнению пункта 2.
                              t  не содержит свободно анонимной переменной
                           i
         2. Учитывая, что q,
 и формулу
                                                   t &t  t,
записать выражение (4.49) в следующей эквивалентной форме:
                     j k1
   S i , (t )    V (τ) i ,,j  (τ) & ( τ1 )e( τ1 ) & S i,,j1 ( τ  1)  qi , (t ) &
                      j 1 t                     1 t
                                                                                                         (4.50)
                       j k1
                  & [ V (τ) i ,,j  (τ) & ( τ1 )qi , ( τ1 ) & S i,,j1 ( τ  1)].
                       j 1 t                      1 t

       Перейти к выполнению требований пункта 3.
       3. Выражение (4.50) путем применения к первому дизъюнктивному
члену аксиомы 1 (4.44) и сокращенного обозначения на основании (4.44)
соответствующей связной группы предикатов (обозначена квадратными
скобками) преобразовать к виду:
                               j  k1
          S i ,   t   V i ,,j  t  & S i,,j 1 (t  1)  qi , t  & Si , (t  1) .   (4.51)
                               j 1

         На этом работа алгоритма заканчивается.

     4.2.4. Пример синтеза абстрактного цифрового автомата с
использованием языка исчисления предикатов первого
порядка
      Требуется построить цифровой автомат Мура, заданный следующим
словесным алгоритмом.
      1. На вход автомата могут подаваться восемь элементарных входных
сигналов:
                       X   x0 , x1 , x2 , x3 , x4 , x5 , x6 , x7
       2. Цифровой автомат должен функционировать циклически. Начало
цикла должно определять событие S 0 , отмеченное выходным сигналом y0 .
       Событие S 0 должно иметь место при поступлении на вход автомата
элементарного входного сигнала x0 или x7 независимо от наличия в этот
момент времени других элементарных входных сигналов, а также в том
случае, если после зарождения события S 0 другие входные сигналы на вход
автомата еще не подавались.
       3. В цифровом автомате должно иметь место событие S1 , отмеченное
выходным сигналом y1 , если в интервале времени между поступлением,
соответственно, сигналов x5 и x6 (не включая моменты времени поступления
сигналов x5 и x6 ) на вход автомата было подано четное количество сигналов

                                                                                                                  84