Программирование рекурсивных функций в сплаве

Я пытаюсь построить рекурсивную функцию в Alloy. Согласно грамматике, представленной в книге Дэниела Джексона, это возможно. Моя функция:

fun auxiliaryToAvoidCyclicRecursion[idTarget:MethodId, m:Method]: Method{
    (m.b.id = idTarget) => {
        m
    } else (m.b.id != idTarget) => {
        (m.b = LiteralValue) => {
           m 
        } else {
           some mRet:Method, c:Class | mRet in c.methods && m.b.id = mRet.id => auxiliaryToAvoidCyclicRecursion[idTarget, mRet]
        }       
    }
}

Но решатель утверждает о вызове auxiliaryToAvoidCyclicRecursion[idTarget, mRet], говоря, что:

"This must be a formula expression.
Instead, it has the following possible type(s):
{this/Method}"

recursion alloy
person Tarciana    schedule 20.09.2013    source источник
comment
Вы должны опубликовать остальную часть своей модели, чтобы мы могли ее запустить.   -  person Aleksandar Milicevic    schedule 21.09.2013

Ответы (1)


arrow_upward
4
arrow_downward

Проблема именно в том, о чем говорится в сообщении об ошибке: возвращаемый тип вашей функции auxiliaryToAvoidCyclicRecursion — Method, который вы пытаетесь использовать в логической импликации, где ожидается формула (т. е. что-то типа Boolean). Вы получите такую ​​же ошибку на любом другом языке со статической типизацией.

Вы можете переписать свою функцию как предикат, чтобы обойти эту проблему:

pred auxiliaryToAvoidCyclicRecursion[idTarget:MethodId, m:Method, ans: Method] {
    (m.b.id = idTarget) => {
        ans = m
    } else (m.b.id != idTarget) => {
        (m.b = LiteralValue) => {
           ans = m 
        } else {
           some mRet:Method, c:Class {
             (mRet in c.methods && m.b.id = mRet.id) => 
                auxiliaryToAvoidCyclicRecursion[idTarget, mRet, ans]
           }
        }       
    }
}

Это не должно привести к ошибке компиляции, но для запуска убедитесь, что вы включили рекурсию (Параметры -> Глубина рекурсии). Как вы увидите, максимальная глубина рекурсии равна 3, а это означает, что Alloy Analyzer может разворачивать ваши рекурсивные вызовы до 3 раз, независимо от объема вашего анализа. Когда этого недостаточно, у вас все еще есть возможность переписать модель так, чтобы рассматриваемый рекурсивный предикат моделировался как отношение. Вот простой пример, иллюстрирующий это.

Связанный список с рекурсивно определенной функцией для вычисления длины списка:

sig Node {
  next: lone Node
} {
  this !in this.^@next
}

fun len[n: Node]: Int {
  (no n.next) => 1 else plus[1, len[n.next]]
}

// instance found when recursion depth is set to 3
run { some n: Node | len[n] > 3 } for 5 but 4 Int

// can't find an instance because of too few recursion unrollings (3), 
// despite the scope being big enough
run { some n: Node | len[n] > 4 } for 5 but 4 Int

Теперь тот же список, где len моделируется как отношение (т. е. поле в Node)

sig Node {
  next: lone Node,
  len: one Int
} {
  this !in this.^@next
  (no this.@next) => this.@len = 1 else this.@len = plus[next.@len, 1]
}

// instance found
run { some n: Node | n.len > 4 } for 5 but 4 Int

Обратите внимание, что последний подход, который не использует рекурсию (и, следовательно, не зависит от значения параметра конфигурации «глубина рекурсии»), может быть (и обычно так и есть) значительно медленнее, чем первый.

person Aleksandar Milicevic    schedule 21.09.2013