Может ли кто-нибудь здесь объяснить, как оператор транзитивного замыкания работает в Alloy с точки зрения матрицы. Я имею в виду, какое правило перевода для перевода оператора закрытия в реальную операцию с матрицей.
переходная крышка из сплава
Ответы (1)
Для вычисления транзитивного замыкания Кодкод использует итеративное возведение в квадрат.
В двух словах, если у вас есть бинарное отношение r (которое напрямую преобразуется в двумерную логическую матрицу), транзитивное замыкание r можно вычислить итеративно как
- r1 = r или (r . r)
- r2 = r1 или (r1 . r1)
- r3 = r1 или (r2 . r2)
- ...
- ^r = rn = rn-1 или (rn-1 . rn-1)
Вопрос в том, когда мы остановимся, т. е. каким должно быть n. Поскольку все ограничено, Kodkod статически знает максимальное количество строк в r, и должно быть интуитивно понятно, что если n установлено равным этому количеству строк, алгоритм произведет семантически правильный перевод. Однако достаточно даже n/2 (поскольку мы каждый раз возводим матрицу в квадрат), что является фактическим числом, используемым Кодкодом.
person
Aleksandar Milicevic
schedule
23.01.2013
Еще один вопрос: если у меня есть c^.contents, какая входная матрица для вычисления транзитивного замыкания? Предположим, что c — это тип подписи C. Тогда что такое входная матрица?
- person user1197891; 24.01.2013
я имею в виду, что если я скажу c в c^.contents, как тогда вы можете убедиться, что c будет присутствовать в матрице транзитивного замыкания?
- person user1197891; 24.01.2013
c не имеет значения при вычислении транзитивного замыкания contents. Требуется, чтобы contents было бинарным отношением, затем ^contents вычислялось, как я описал ранее, и, наконец, вычислялось простое соединение между c и ^contents.
- person Aleksandar Milicevic; 25.01.2013
На самом деле, даже
ceiling(log_2(n)) достаточно.
- person Grayswandyr; 29.06.2017
