Спецификация и тестирование систем с асинхронным интерфейсом



         

Алгоритм обхода ndfsm - часть 5


  • 0, если i = 0, вершина v'i является незавершенной или в детерминированном пройденном подграфе нет маршрута, ведущего из вершины v'i и в какую-либо из незавершенных пройденных вершин;
  • минимальной длине маршрута в детерминированном пройденном подграфе, начинающегося в вершине v'i и заканчивающегося в какой-либо из незавершенных пройденных вершин, в противном случае.

    Определим на множестве пар натуральных чисел линейный порядок:

    (b1,b2) < (b'1,b'2)

    b1 < b'1
    (b1 = b'1
    b2 < b'2)

    Отметим, что множество пар натуральных чисел с данным линейным порядком образуют фундированное множество, то есть множество, в котором отсутствует бесконечно убывающая последовательность элементов.

    Согласно определению βG( () ) = (|EG|,0).

    Покажем, что для любого префикса ( e1, …, ei ) функционирования e

    βG( ( e1, …, ei, ei+1 ) ) < βG( ( e1, …, ei ) )

    Для всех i ≥ 0 αndfsm( A, v'i, ( e1, …, ei ) ) ≠ τ. Следовательно, либо вершина v'i не является завершенной, либо в детерминированном пройденном подграфе существует маршрут, ведущий из вершины v'i в какую-либо из незавершенных пройденных вершин.

    Рассмотрим первый случай. Если вершина v'i не является завершенной, то αndfsm возвращает минимальный стимул из π(v), который не является пройденным в вершине v'i. На этом основании можно сделать вывод, что ei+1 является дугой, не принадлежащей &#x007B; e1, …, ei &#x007D;. Поэтому первый компонент βG( ( e1, …, ei+1 ) ) на единицу меньше первого компонента βG( ( e1, …, ei ) ), откуда следует, что βG( ( e1, …, ei, ei+1 ) ) < βG( ( e1, …, ei ) ).

    Рассмотрим второй случай. Если вершина v'i является завершенной и в детерминированном пройденном подграфе существует маршрут, ведущий из вершины v'i в какую-либо из незавершенных пройденных вершин, то αndfsm возвращает стимул, приписанный к дуге ej пройденного маршрута, которая обладает минимальным индексом среди всех дуг, являющихся первыми дугами в кратчайших маршрутах детерминированного пройденного подграфа, ведущих из текущей вершины в какую-либо из незавершенных пройденных вершин.


    Содержание  Назад  Вперед