Actions
Feature #5573
closed[efsm] Включение инвариантов на переменные в EFSM
Start date:
01/23/2015
Due date:
% Done:
100%
Estimated time:
Published in build:
20150307
Actions
Added by Igor Melnichenko almost 10 years ago. Updated over 9 years ago.
100%
Реализован перенос инвариантов из CFG в CGAA.
Инварианты на переменные хранятся в EFSM-представлении в виде Map<String, Node> (ключ - имя переменной, значение - инвариант). CgaaEfsmTransformer в том числе добавляет инварианты из CGAA-представления. В классе Efsm присутствует метод добавления инварианта, но нет методов их получения извне, ввиду неясной политики именования таких функций в данном классе(только через приватные поля).