EFSM Traversal¶

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

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

1. Обучение (learning);
2. Случайный обход (random walk);
3. Поиск с возвратами (backjumping).

Обучение¶

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

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

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

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

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

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

1. случайным образом выбирается один из переходов, исходящих из текущего состояния;
2. делается попытка разрешить его условие срабатывания;
3. если условие срабатывания разрешено:
   1. невовлечённым в него входным переменным присваиваются случайные значения;
   2. применяется действие перехода и обновляется состояние EFSM;
   3. выполненному переходу ставится в соответствие номер текущей последовательности и номер текущего её элемента.
      1. TODO: Переходу или состоянию?
4. если условие срабатывания не разрешено:
   1. TODO: Что делается в этом случае?

Поиск с возвратами¶

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

1. выбирается переход из начала списка;
2. если его условие срабатывания зависит только от входных переменных:
   1. извлекается сохранённая на предыдущем шаге информация о достижимости начального состояния этого перехода;
   2. на основе этой информации к EFSM применяется соответствующая входная последовательность, и EFSM оказывается в начальном состоянии обрабатываемого перехода;
   3. разрешается условие срабатывания этого перехода;
      1. TODO: А если условие неразрешимо?
   4. переход удаляется из списка;
3. если его условие срабатывания зависит не только от входных переменных:
   1. извлекается сохранённая на предыдущем шаге информация о достижимости начального состояния этого перехода;
   2. на основе этой информации к EFSM применяется соответствующая входная последовательность, и EFSM оказывается в начальном состоянии обрабатываемого перехода; ## делается попытка разрешить условие срабатывания этого перехода:
      1. если она успешна, переход удаляется из списка;
      2. если нет — обработка продолжается;
4. на основании информации о зависимостях по данным извлекаются переходы, которые определяют значение переменных, входящих в условие срабатывания обрабатываемого перехода;
5. для каждого из них (пусть это будет t) выполняются следующие действия:
   1. получить информацию о достижимости начального состояния t, выполнить соответствующую тестовую цепочку;
      1. TODO: что делать, если начальное состояние t недостижимо?
   2. если переход t не обновляет значение счётчика, при помощи алгоритма Дейкстры найти путь от t к целевому переходу;
   3. если в t обновляется значение счётчика, алгоритм Дейкстры применяется два раза: сначала, чтобы найти путь от конечного состояния t до целевого перехода, а затем - чтобы найти путь из начального состояния t в самого себя через t;
   4. при помощи решателя ограничений определяется, сколько раз необходимо пройти по второму пути (то есть по циклу), чтобы начать двигаться по первому;
      1. TODO: как это делается?
   5. построить ограничение в виде композиции действия перехода t и условие срабатывания t и целевого перехода;
   6. если это ограничение неразрешимо:
      1. перейти к следующему t;
   7. если это ограничение разрешимо:
      1. подать полученные значения входных переменных в EFSM;
      2. последовательно пройти по каждому переходу из найденного алгоритмом Дейкстры пути;
      3. если условие срабатывания какого-либо из переходов неразрешимо:
         1. перейти к следующему t.