Retrascope

h1. EFSM Traversal

h2. Веронский алгоритм

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

# Обучение (learning);

# Случайный обход (random walk);

# Поиск с возвратами (backjumping).

h3. Обучение

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

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

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

h3. Случайный обход

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

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

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

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

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

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

# если условие срабатывания разрешено:

## невовлечённым в него входным переменным присваиваются случайные значения;

## применяется действие перехода и обновляется состояние EFSM;

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

### *TODO: Переходу или состоянию?*

# если условие срабатывания не разрешено:

## *TODO: Что делается в этом случае?*

h3. Поиск с возвратами

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

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

# если его условие срабатывания зависит только от входных переменных:

## извлекается сохранённая на предыдущем шаге информация о достижимости начального состояния этого перехода;

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

## разрешается условие срабатывания этого перехода;

### *TODO: А если условие неразрешимо?*

## переход удаляется из списка;

# если его условие срабатывания зависит не только от входных переменных:

## извлекается сохранённая на предыдущем шаге информация о достижимости начального состояния этого перехода;

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

### если она успешна, переход удаляется из списка;

### если нет — обработка продолжается;

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

# для каждого из них (пусть это будет _t_) выполняются следующие действия:

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

### *TODO: что делать, если начальное состояние _t_ недостижимо?*

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

## если в _t_ обновляется значение счётчика, алгоритм Дейкстры применяется два раза: сначала, чтобы найти путь от конечного состояния _t_ до целевого перехода, а затем - чтобы найти путь из начального состояния _t_ в самого себя через _t_;

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

### *TODO: как это делается?*

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

## если это ограничение неразрешимо:

### перейти к следующему _t_;

## если это ограничение разрешимо:

### подать полученные значения входных переменных в EFSM;

### последовательно пройти по каждому переходу из найденного алгоритмом Дейкстры пути;

### если условие срабатывания какого-либо из переходов неразрешимо:

#### перейти к следующему _t_.