Подход, основанный на инвариантных ограничениях генерации

Я прочитал статью «Анализ линейных отношений на основе ограничений» от «Шрирама Санкаранараянана, Хенни Б. Сипмы и Зохара Манна», чтобы проверить уравнения с фиксированной точкой, возникающие в результате абстрактной интерпретации, путем применения леммы Фаркаша в заданном неравенстве шаблона с неизвестными коэффициентами, который вычисляет ограничения на значения коэффициентов, так что подстановка любого решения обратно в шаблон дает допустимое инвариантное отношение.

Я следовал примеру 1 (на этой бумаге) Let V = {x, y} и L = { 0 }. Рассмотрим систему перехода, показанную ниже. Каждый переход моделирует параллельный процесс, который автоматически обновляет переменные x, y.

Θ = (x = 0 ∧ y = 0)
T = {τ1 , τ2 }
τ1 = <l0 , l0 , [x' = x + 2y ∧ y' = 1 − y]>
τ2 = <l0, l0 , [x' = x + 1 ∧ y' = y + 2]>

Я закодировал инициацию, используя лемму Фаркаша (пример 2 в этой статье), а также последовательность (через переходы τ1 и τ2).

Авторы говорят:

Мы фиксируем систему линейных переходов Π с переменными {x1 , . . . , xn }, которые вместе обозначаются как x. Предполагается, что система имеет одно местоположение для упрощения презентации. Утверждение шаблона в расположении α(c) = c1 x1 + · · · + cn xn + d ≥ 0. Переменные-коэффициенты {c1 , . . . , cn , d} вместе обозначаются как c. Переходы системы {τ1 , . . . , τm }, где τi : , , ρi. Начальное условие обозначается Θ. Система в Примере 1 будет использоваться в качестве рабочего примера для иллюстрации представленных идей.

Я достиг общего ограничения, полученного путем объединения ограничений, полученных от инициации и выполнения для каждого перехода (пример 4 в этой статье).

В этот момент я думаю, что можно решить ограничение, закодировав все это в решении, таком как Z3. На самом деле я сделал это, закодировав линейную арифметику непосредственно в Z3:

(define-sort MyType () Int)
(declare-const myzero MyType)
(declare-const mi1 MyType)
(declare-const mi2 MyType)
(declare-const c1 MyType)
(declare-const c2 MyType)
(declare-const d MyType)
(assert (= myzero 0))
;initiation
    (assert (>= d 0) )
;transition 1
(assert (and 
    (= (- (* mi1 c1) c1) 0)
    (= (- (+ (* mi1 c2) c2) (* 2 c1) ) 0)
    (<= (- (- (* mi1 d) d) c2) 0)
    (>= mi1 0)
))
;transition 2
(assert (and 
    (= (- (* mi2 c1) c1) 0)
    (= (- (* mi2 c2) c2) 0)
    (<= (- (- (- (* mi2 d) d) c1) (* 2 c2) ) 0)
    (>= mi2 0)
))
(check-sat)
(get-model)

Я предполагаю, что у меня не все хорошо, так как я не выяснил ни одного индуктивного инварианта в местоположении l0 через c1, c2, ..., cn, d как отдельные значения (диапазон o).

Z3 ответил мне ноль по всем коэффициентам:

sat
(model 
    (define-fun mi2 () Int 0)
    (define-fun c2 () Int 0)
    (define-fun mi1 () Int 0)
    (define-fun c1 () Int 0)
    (define-fun d () Int 4)
    (define-fun myzero () Int 0)
)

Я пытался найти примеры, связанные с , но до сих пор не повезло.