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



         

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


КОНЕЦ (асинхронная модель поведения является корректной относительно данной асинхронной модели требований)

  • Если индекс текущего элемента перестановки больше либо равен n-2 или , то алгоритм переходит к шагу 9.

    if ((current ≥ n-2) || (bound[current] == 1)) goto 9;

  • Если индекс текущего элемента перестановки является нечетным при обратной нумерации элементов перестановки [n-1
    0, …, 0
    n-1], то алгоритм переходит к шагу 7.

    if ((n-current) % 2 == 0) goto 7;

  • Алгоритм осуществляет циклический сдвиг хвоста перестановки на единицу

    perm[current+2]

    perm[current+1] … perm[n-1]
    perm[n-2] perm[current+1]
    perm[n-1]

    tmp = perm[current+1]; for(j=current+1;j<n-1;j++) perm[j] = perm[j+1]; perm[n-1] = tmp;

  • Если предыдущая перестановка не противоречила частичному порядку
    , то алгоритм вычисляет не противоречит ли новая перестановка этому порядку, записывает результат в переменную order_failed и переходит к шагу 9.

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

    goto 9;

  • Алгоритм осуществляет транспозицию элементов перестановки с индексами current+1 и current+2.

    tmp = perm[current+1]; perm[current+1] = perm[current+2]; perm[current+2] = tmp;

  • Если предыдущая перестановка не противоречила частичному порядку
    , то алгоритм вычисляет не противоречит ли новая перестановка этому порядку и записывает результат в переменную order_failed.

    if (!order_failed) &#x007B;if (order[perm[current+2],perm[current+1]]) order_failed = true; &#x007D;

  • Если текущий счетчик числа точек ветвления равен 1, то алгоритм переходит к шагу 14.

    if (bound[current] == 1) goto 14;

  • Алгоритм осуществляет транспозицию элементов перестановки с индексами current и n-B(n-current,n-current-bound[current]+1), сохраняя индекс второго элемента в переменной current2.

    current2 = n-B(n-current,n-current-bound[current]+1); tmp = perm[current]; perm[current] = perm[current2]; perm[current2] = tmp;




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