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



         

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


Лемма.

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

Доказательство.

Предположим, что это не так. Тогда существует конечный граф G = ( VG, XG, EG ), обладающий детерминированным сильносвязным полным остовным подграфом, и функционирование e = ( e1, e2, …, en, … ) алгоритма ndfsm на этом графе такие, что e не является конечным обходом по стимулам графа G. Такое может быть в двух случаях: если функционирование e является конечным, но не является обходом по стимулам графа G, и если функционирование e является бесконечным.

1. Предположим, что функционирование e = ( e1, e2, …, en ) является конечным, но не является обходом по стимулам графа G. Тогда из определения функционирования следует, что αndfsm( A, v'n, e ) = τ . Следовательно вершина v'n является завершенной и в детерминированном пройденном подграфе G''e не существует маршрута, ведущего из вершины v'n в какую-либо из незавершенных пройденных вершин.

С другой стороны e не является обходом по стимулам графа G, то есть в графе G существует такая дуга ( v, x, v' )

isin.gif EG, что не существует такого i
isin.gif { 1, … , n }, что v = vi и x = xi.

Рассмотрим детерминированный сильносвязный полный остовный подграф G' = ( VG', XG', EG' ) графа G. Так как подграф является остовным, то обе вершины v и v'n принадлежат VG'. Так как граф G конечный, а его подграф G' - сильносвязный, то существует конечный маршрут f = ( f1, f2, …, fk ), ведущий из v'n в v. Пусть fi = ( wi, yi, w'i ). Тогда для всех i

isin.gif { 1, … , k } из вершины wi в графе G выходит одна единственная дуга fi, помеченная стимулом yi. Предположим, что существует вторая такая дуга: ( wi, yi, w''i )
isin.gif EG. Тогда эта дуга также принадлежит и подграфу G' ( ( wi, yi, w''i )
isin.gif EG' ), так как подграф G' является полным остовным подграфом. А это противоречит тому, что подграф G' является детерминированным.


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