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



         

Алгоритм проверки корректности поведения - часть 8


current2 : Nat := 0
       вспомогательная переменная для хранения индекса второго взаимодействий, участвовавшего в последней транспозиции.

tmp : Nat := 0
       вспомогательная переменная.

j : Nat := 0
       вспомогательная переменная.

Алгоритм.

  1. Алгоритм вычисляет является ли текущая перестановка perm линеаризацией частичного порядка
    , записывает результат в переменную order_failed и переходит к шагу 2, если текущая перестановка не противоречит частичному порядку
    , или к шагу 3 - в противном случае. При этом предполагается, что упорядочение P[perm[0]], …, P[perm[current]] не противоречит частичному порядку
    и поэтому достаточно проверить элементы перестановки, начиная с current.

    for(;current<n-1;current++) &#x007B;for(j=current+1;j<n;j++) &#x007B;if (order[perm[j],perm[current]]) &#x007B;order_failed = true; goto 3; &#x007D; &#x007D; &#x007D;

    order_failed = false;

  2. Алгоритм строит пути в модели требований, соответствующие последовательности взаимодействий в текущей перестановке, заполняя массив path. При этом предполагается, что начальные отрезки пути path[0], …, path[processed] уже построены ранее. Если на одном из шагов множество состояний модели требований оказывается пустым, то алгоритм переходит к шагу problem, установив значение переменной current равное индексу элемента перестановки для которого было получено пустое множество. Если же path[n] ≠ Ø, то алгоритм завершает свою работу с положительным вердиктом. Найдена линеаризация ( P[perm[0]], P[perm[1]],…, P[perm[n-1]] ), для которой множество Г*( v0, ( P[perm[0]], P[perm[1]], …, P[perm[n-1]] ) ) = path[n] не пусто.

    for(;processed<n;processed++) &#x007B;path[processed+1] = Ø; foreach v : V in path[processed] path[processed+1] = path[processed+1]

    &#x03b3;( v, P[perm[processed]] ); if (path[processed+1] == Ø) &#x007B;current = processed; for(j=current+1;j<n;j++) bound[j] = n-j; goto 3; &#x007D; &#x007D;




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