EFSM Traversal » History » Revision 4
Revision 3 (Alexander Kamkin, 02/27/2014 08:18 PM) → Revision 4/13 (Alexander Kamkin, 02/28/2014 06:03 AM)
h1. Обход расширенного конечного автомата (EFSM, Extended Finite State Machine) EFSM Traversal h2. Веронский метод (Franco Fummi et al.) алгоритм Метод обхода EFSM Алгоритм в целом состоит из трёх фаз: # обучение Обучение (learning); # случайный Случайный обход (random walk); # поиск Поиск с возвратами (backjumping). h3. Обучение В ходе первой фазы анализируются _зависимости_ зависимости переходов EFSM по _данным_ данным и по _управлению_, и строится граф зависимостей — ориентированный граф, вершинами которого являются переходы заданного EFSM, а дуги представляют зависимости. # *TODO: в одном графе представляются как зависимости управлению. Зависимость по данным, так и зависимости по управлению?* # *TODO: зависимости по разным переменным представляются разными дугами?* Переход _t_ ~2~ _зависит по данным_ от перехода _t_ ~1~, если _t_ ~1~ данным: один переход устанавливает значение некоторой переменной _x_ (действие перехода содержит присваивание в _x_), а _t_ ~2~ переменной, которую другой переход использует _x_ при вычислении значения другой переменной (внутренней или выходной). Переход _t_ ~2~ _зависит Зависимость по управлению_ от перехода _t_ ~1~, если _t_ ~1~ управлению: один переход устанавливает значение некоторой переменной _x_, переменной, которая входит в условие срабатывания _t_ ~2~. другого перехода. На этой Эти зависимости можно представить в виде ориентированного графа, в котором вершины — это переходы EFSM, а дуги представляют зависимости по данным/управлению. Тут же фазе происходит выявление счётчиков и зависимых от них переходов. Переменная _x_ считается _счётчиком_, счётчиком, если существует цикл цикл, в графе состояний EFSM, в который входит переход с условием срабатывания, зависящим от _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_. h2. Литература *TODO: Дать ссылку на статью.*