EFSM Traversal » History » Revision 3
Revision 2 (Alexander Kamkin, 02/27/2014 07:47 PM) → Revision 3/13 (Alexander Kamkin, 02/27/2014 08:18 PM)
h1. EFSM Traversal h2. Веронский алгоритм Алгоритм в целом состоит из трёх фаз: # Обучение (learning); learning; # Случайный обход (random walk); random walk; # Поиск с возвратами (backjumping). backjumping. h3. Обучение 1) В ходе первой фазы анализируются зависимости они анализируют взаимозависимости переходов по данным и по управлению. Зависимость по данным: один переход устанавливает значение переменной, которую другой переход использует при вычислении значения выхода или другой переменной (внутренней или выходной). внутренней переменной. Зависимость по управлению: один переход устанавливает значение переменной, которая входит в условие срабатывания другого перехода. Эти зависимости можно представить в виде ориентированного направленного графа, в котором вершины узлы — это переходы EFSM, а дуги рёбра представляют зависимости по данным/управлению. Тут же происходит выявление счётчиков и зависимых от них переходов. Переменная _x_ x считается счётчиком, если существует цикл, такой циклический путь, в который входит переход с условием срабатывания, гардом зависящим от _x_, x, а также переход, в действии action''е которого меняется значение _x_, x, причём значение _x_ x прямо или косвенно зависит от предыдущего значения _x_. x. h3. Случайный обход 2) На вход случайного обходчика подаётся два параметра: количество тестовых последовательностей и длина каждой одной последовательности. В цикле, пока количество тестовых последовательностей не достигнет максимального числа или пока не будут покрыты все переходы выполняются следующие действия: # сброс состояния EFSM; # генерация входных векторов в цикле, пока не будет достигнута максимальная длина текущей последовательности. Входной вектор генерируется следующим образом: # случайным образом выбирается один из переходов, исходящих из текущего состояния; # делается попытка разрешить его условие срабатывания; гард; # если условие срабатывания разрешено: ## гард разрешён, невовлечённым в него входным переменным присваиваются случайные значения; ## применяется действие перехода и значения, в соответствии с этими значениями обновляется состояние EFSM; ## выполненному EFSM, сохраняется информация о "достижимости" (выполненному переходу ставится в соответствие номер номера текущей последовательности и номер текущего её элемента. ### *TODO: Переходу или состоянию?* # если условие срабатывания не разрешено: ## *TODO: Что делается в этом случае?* h3. Поиск с возвратами Составляется 3) составляется упорядоченный список непокрытых переходов, причём переходы, исходящие из уже посещённых на предыдущем этапе состояний, состояний помещаются в начало списка. Затем циклически выполняются следующие действия: # выбирается переход из начала списка; # если его условие срабатывания гард зависит только от входных переменных: ## входов EFSM, извлекается сохранённая на предыдущем шаге информация о достижимости начального состояния этого перехода; ## на перехода. На основе этой информации к EFSM применяется соответствующая входная последовательность, и EFSM оказывается в начальном состоянии состоянии-источнике для обрабатываемого перехода; ## разрешается условие срабатывания перехода. Разрешается гард этого перехода; ### *TODO: А если условие неразрешимо?* ## перехода, переход удаляется из списка; # если его условие срабатывания гард зависит не только от входных переменных: ## входов, извлекается сохранённая на предыдущем шаге информация о достижимости начального состояния этого перехода; ## на перехода. На основе этой информации к EFSM применяется соответствующая входная последовательность, и EFSM оказывается в начальном состоянии состоянии-источнике для обрабатываемого перехода; ## делается перехода. Делается попытка разрешить условие срабатывания гард этого перехода: ### если перехода. Если она успешна, переход удаляется из списка; ### списка, если нет — обработка продолжается; продолжается. # на основании информации о зависимостях по данным извлекаются извлечь переходы, которые определяют значение переменных, входящих в условие срабатывания гард обрабатываемого перехода; # для перехода. Для каждого из них (пусть это будет _t_) выполняются t) выполнить следующие действия: ## получить информацию о достижимости начального состояния _t_, t, выполнить соответствующую тестовую цепочку; ### *TODO: что делать, если начальное состояние _t_ недостижимо?* ## если Если переход _t_ t не обновляет значение счётчика, при помощи алгоритма Дейкстры найти путь от _t_ t к целевому переходу; ## если переходу. Если в _t_ t обновляется значение счётчика, алгоритм Дейкстры применяется два раза: сначала, чтобы найти путь от конечного состояния _t_ t до целевого перехода, а затем - чтобы найти путь из начального состояния _t_ t в самого себя через _t_; ## t. После этого при помощи решателя ограничений constraint solver''а определяется, сколько раз необходимо пройти по второму пути (то есть по циклу), чтобы начать двигаться по первому; ### *TODO: как это делается?* ## построить ограничение constraint в виде композиции действия action''а перехода _t_ t и условие срабатывания _t_ guard''ов t и целевого перехода; ## если это ограничение неразрешимо: ### этот constraint неразрешим, перейти к следующему _t_; ## если это ограничение разрешимо: ### t. Если разрешим, подать полученные значения входных переменных входов в EFSM; ### EFSM, а затем последовательно пройти пройтись по каждому переходу из найденного алгоритмом Дейкстры пути; ### если условие срабатывания пути. Если guard какого-либо из переходов неразрешимо: #### оказался невыполнимым, перейти к следующему _t_. t.