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



         

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


То есть существуют такие i и j, что pi
isin.gif { p1, p2, …, pk }
pj
pi
pj
{ p1, p2, …, pk }.

Отсюда, i ≤ k < j

pj
pi. Следовательно, последовательность ( p1, p2, …, pn ) не является линеаризацией, что противоречит нашему предположению.

Если не дублировать проверку существования путей, соответствующих общему началу линеаризаций, то число необходимых вычислений функции &#x03b3; будет совпадать с числом дуг в дереве возможных линеаризаций. Число дуг в дереве для множества размерностью n составляет:

n + n&#x0387;(n-1) + … + n&#x0387;(n-1)&#x0387; … &#x0387;1 =

image104.gif
=
image106.gif
image108.gif
≤ e&#x0387;n!, где e - число Эйлера.

Основной сложностью в реализации этого алгоритма является организация перебора возможных линеаризаций асинхронной модели поведения ( P,

). Наиболее простой подход, основанный на переборе всех перестановок в лексикографическом порядке, требует O(n&#x0387;n!) операций, так как для проверки того, является ли очередная перестановка линеаризацией, в этом случае требуется ∼n операций.

С другой стороны, существуют другие алгоритмы перебора перестановок, которые позволяют сократить затраты на проверку того, является ли очередная перестановка линеаризацией или нет. Но применение нетривиального перебора линеаризаций должно обеспечивать не только сложность O(n!), но и избегать перебора k! заведомо неподходящих перестановок, в тех случаях, когда известно, что (n-k)-ый элемент в какой-то перестановке нарушает условия линеаризации.

Алгоритм перебора линеаризаций, удовлетворяющий всем этим требованиям, был построен на основе алгоритма перебора перестановок 1.11, описанного в []. Этот алгоритм обеспечивает перебор перестановок таким образом, что каждая последующая перестановка отличается от предыдущей транспозицией одной пары элементов. В результате, проверка соответствия очередной перестановки условиям линеаризации требует в большинстве случаев константного времени. И в то же время, данный алгоритм позволяет избежать перебора k! заведомо неподходящих перестановок.




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