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



         

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


Следовательно, наше предположение относительно существования второй дуги ( wi, yi, w''i )
isin.gif EG неверно и дуга ( wi, yi, w'i ) является единственной дугой в графе G, выходящей из wi и помеченной стимулом yi.

Докажем индукцией по пути f = ( f1, f2, …, fk ), что все вершины w'i являются завершенными для i

isin.gif { 1, … , k }.

База индукции . Вершина w1 = v'n

isin.gif VGe является завершенной, по определению функционирования и функции αndfsm.

Предположение индукции . Пусть вершина w'i-1 = wi является завершенной.

Шаг индукции . Так как вершина wi является завершенной, стимул yi является допустимым в этой вершине и дуга ( wi, yi, w'i ) является единственной дугой, выходящей из wi и помеченной стимулом yi, то дуга ( wi, yi, w'i ) также является пройденной, то есть ( wi, yi, w'i )

isin.gif e. Отсюда следует, что дуга ( wi, yi, w'i ) принадлежит детерминированному пройденному подграфу G''e, так как эта дуга является пройденной и детерминированной. На этом основании можно сделать вывод, что вершина w'i является завершенной, так как в противном случае мы нашли маршрут ( f1, f2, …, fi ) в детерминированном пройденном подграфе G''e, ведущий из v'n в одну из незавершенных пройденных вершин.

Мы доказали, что все вершины w'i являются завершенными. Следовательно, и вершина w'k = v

isin.gif VGe также является завершенной, что противоречит нашему предположению о том, что e не является обходом по стимулам графа G. Следовательно, это предположение не верно и функционирование e не является конечным.

2. Предположим, что функционирование e = ( e1, e2, …, en, … ) является бесконечным. Тогда для всех i ≥ 0 αndfsm( A, v'i, ( e1, …, ei ) ) ≠ τ.

Определим функцию βG на графе G, устанавливающую соответствие между маршрутом ( e1, …, ei ) в графе G и парой натуральных чисел (b1,b2), следующим образом:

  • b1 равно числу дуг графа G, отсутствующих в маршруте ( e1, …, ei ), |EG \ { e1, …, ei }|;
  • b2 равно




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