Реализовать поддержку верификации индексированных ФД, содержащих в себе другие ФД.
На данный момент отсутствует поддержка верификации индексированных ФД, которые содержат в себе другие ФД. Примеры таких ФД:
a[b]
a[b[1]]
a[b[b[1]]
a[b[1][c[3]]][d]Возможное решение:
Для каждого уровня вложенности необходимо обрабатывать ФД следующим образом:
ФД, содержащий вложенные индексированные ФД, преобразовать в Promela-код use(<<varN>>), где N соответствует порядковому номеру ФД, и повторить алгоритм для каждого вложенного ФД.
Реализовать поддержку верификации индексированных ФД, содержащих в себе другие ФД.
На данный момент отсутствует поддержка верификации индексированных ФД, которые содержат в себе другие ФД. Примеры таких ФД:
a[b]a[b[1]]a[b[b[1]]a[b[1][c[3]]][d]Возможное решение: Для каждого уровня вложенности необходимо обрабатывать ФД следующим образом: ФД, содержащий вложенные индексированные ФД, преобразовать в Promela-кодuse(<<varN>>), где N соответствует порядковому номеру ФД, и повторить алгоритм для каждого вложенного ФД.