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



         

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


Определение 20.

Алгоритмом движения ndfsm мы будем называть функцию αndfsm, которая по неизбыточному описанию ориентированного графа G = ( VG, XG, π ), текущей вершине v

isin.gif VG и пройденному маршруту e = ( e1, e2, …, en ) вычисляет действие a
isin.gif XG
{ τ } следующим образом:

  • Если текущая вершина не является завершенной, то функция возвращает минимальный стимул из π(v), который не является пройденным в текущей вершине;
  • Иначе, если в детерминированном пройденном подграфе существует маршрут, ведущий из текущей вершины в какую-либо из незавершенных пройденных вершин, то функция возвращает стимул, приписанный к дуге ei пройденного маршрута, которая обладает минимальным индексом среди всех дуг, являющихся первыми дугами в кратчайших маршрутах детерминированного пройденного подграфа, ведущих из текущей вершины в какую-либо из незавершенных пройденных вершин;
  • В противном случае функция возвращает τ.

Корректность определения следует из фундированности множества стимулов и конечности пройденного подграфа.

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

Обходом по стимулам [] конечного ориентированного графа G = ( VG, XG, EG ) называется маршрут v1

image025.gif
v2
image027.gif
image029.gif
vn, в котором для каждой дуги ( v, x, v' )
isin.gif EG существует i
isin.gif { 1, … , n-1 }, такое что v = vi и x = xi.

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




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