Retrascope

h1. EFSM Traversal

Алгоритм в целом состоит из трёх фаз:

# learning;

# random walk;

# backjumping.

1) В ходе первой фазы они анализируют взаимозависимости переходов по данным и по управлению. Зависимость по данным: один переход устанавливает значение переменной, которую другой переход использует при вычислении значения выхода или другой внутренней переменной. Зависимость по управлению: один переход устанавливает значение переменной, которая входит в условие срабатывания другого перехода.

Эти зависимости можно представить в виде направленного графа, в котором узлы — это переходы EFSM, а рёбра представляют зависимости по данным/управлению.

Тут же происходит выявление счётчиков и зависимых от них переходов. Переменная x считается счётчиком, если существует такой циклический путь, в который входит переход с гардом зависящим от x, а также переход, в action''е которого меняется значение x, причём значение x прямо или косвенно зависит от предыдущего значения x.

2) На вход случайного обходчика подаётся два параметра: количество тестовых последовательностей и длина одной последовательности.

В цикле, пока количество тестовых последовательностей не достигнет максимального числа или пока не будут покрыты все переходы выполняются следующие действия:

# сброс состояния EFSM;

# генерация входных векторов в цикле, пока не будет достигнута максимальная длина текущей последовательности.

Входной вектор генерируется следующим образом:

# случайным образом выбирается один из переходов, исходящих из текущего состояния;

# делается попытка разрешить его гард;

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

3) составляется упорядоченный список непокрытых переходов, причём переходы, исходящие из уже посещённых на предыдущем этапе состояний помещаются в начало списка. Затем циклически выполняются следующие действия:

# выбирается переход из начала списка;

# если его гард зависит только от входов EFSM, извлекается сохранённая на предыдущем шаге информация о достижимости начального состояния этого перехода. На основе этой информации к EFSM применяется соответствующая входная последовательность, и EFSM оказывается в состоянии-источнике для обрабатываемого перехода. Разрешается гард этого перехода, переход удаляется из списка;

# если его гард зависит не только от входов, извлекается сохранённая на предыдущем шаге информация о достижимости начального состояния этого перехода. На основе этой информации к EFSM применяется соответствующая входная последовательность, и EFSM оказывается в состоянии-источнике для обрабатываемого перехода. Делается попытка разрешить гард этого перехода. Если она успешна, переход удаляется из списка, если нет — обработка продолжается.

# на основании информации о зависимостях по данным извлечь переходы, которые определяют значение переменных, входящих в гард обрабатываемого перехода. Для каждого из них (пусть это будет t) выполнить следующие действия:

## получить информацию о достижимости t, выполнить соответствующую тестовую цепочку;

## Если переход t не обновляет значение счётчика, при помощи алгоритма Дейкстры найти путь от t к целевому переходу. Если в t обновляется значение счётчика, алгоритм Дейкстры применяется два раза: сначала, чтобы найти путь от конечного состояния t до целевого перехода, а затем - чтобы найти путь из начального состояния t в самого себя через t. После этого при помощи constraint solver''а определяется, сколько раз необходимо пройти по второму пути (то есть по циклу), чтобы начать двигаться по первому;

## построить constraint в виде композиции action''а перехода t и guard''ов t и целевого перехода;

## если этот constraint неразрешим, перейти к следующему t. Если разрешим, подать полученные значения входов в EFSM, а затем последовательно пройтись по каждому переходу из найденного алгоритмом Дейкстры пути. Если guard какого-либо из переходов оказался невыполнимым, перейти к следующему t.