EFSM Traversal¶

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

1. learning;
2. random walk;
3. backjumping.

1) В ходе первой фазы они анализируют взаимозависимости переходов по данным и по управлению. Зависимость по данным: один переход устанавливает значение переменной, которую другой переход использует при вычислении значения выхода или другой внутренней переменной. Зависимость по управлению: один переход устанавливает значение переменной, которая входит в условие срабатывания другого перехода.
Эти зависимости можно представить в виде направленного графа, в котором узлы — это переходы EFSM, а рёбра представляют зависимости по данным/управлению.
Тут же происходит выявление счётчиков и зависимых от них переходов. Переменная x считается счётчиком, если существует такой циклический путь, в который входит переход с гардом зависящим от x, а также переход, в action''е которого меняется значение x, причём значение x прямо или косвенно зависит от предыдущего значения x.

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

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

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

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

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

1. выбирается переход из начала списка;
2. если его гард зависит только от входов EFSM, извлекается сохранённая на предыдущем шаге информация о достижимости начального состояния этого перехода. На основе этой информации к EFSM применяется соответствующая входная последовательность, и EFSM оказывается в состоянии-источнике для обрабатываемого перехода. Разрешается гард этого перехода, переход удаляется из списка;
3. если его гард зависит не только от входов, извлекается сохранённая на предыдущем шаге информация о достижимости начального состояния этого перехода. На основе этой информации к EFSM применяется соответствующая входная последовательность, и EFSM оказывается в состоянии-источнике для обрабатываемого перехода. Делается попытка разрешить гард этого перехода. Если она успешна, переход удаляется из списка, если нет — обработка продолжается.
4. на основании информации о зависимостях по данным извлечь переходы, которые определяют значение переменных, входящих в гард обрабатываемого перехода. Для каждого из них (пусть это будет t) выполнить следующие действия:
   1. получить информацию о достижимости t, выполнить соответствующую тестовую цепочку;
   2. Если переход t не обновляет значение счётчика, при помощи алгоритма Дейкстры найти путь от t к целевому переходу. Если в t обновляется значение счётчика, алгоритм Дейкстры применяется два раза: сначала, чтобы найти путь от конечного состояния t до целевого перехода, а затем - чтобы найти путь из начального состояния t в самого себя через t. После этого при помощи constraint solver''а определяется, сколько раз необходимо пройти по второму пути (то есть по циклу), чтобы начать двигаться по первому;
   3. построить constraint в виде композиции action''а перехода t и guard''ов t и целевого перехода;
   4. если этот constraint неразрешим, перейти к следующему t. Если разрешим, подать полученные значения входов в EFSM, а затем последовательно пройтись по каждому переходу из найденного алгоритмом Дейкстры пути. Если guard какого-либо из переходов оказался невыполнимым, перейти к следующему t.