「Sriram Sankaranarayanan、Henny B. Sipma、および Zohar Mann」の論文「Constraint-Based Linear-Relations Analysis」を読んで、未知の係数を持つ与えられたテンプレート不等式に Farkas Lemma を適用することにより、抽象的な解釈から生じる不動点方程式をチェックしました。これは、係数の値に対する制約を計算し、任意の解をテンプレートに代入すると、有効な不変関係が得られます。
私は例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]>
Farkas Lemma (その論文の例 2) と consecution (遷移 τ1 および τ2 による) を使用して、開始をエンコードしました。
著者は次のように述べています。
まとめて x と呼ばれる
Π変数 を使用して、線形遷移システムを修正します。{x1 , . . . , xn }プレゼンテーションを簡略化するために、システムには単一の場所があると想定されています。場所 のテンプレート アサーションは ですα(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を介して場所での誘導不変量を把握していないと、うまくいかないと思います。c1c2cndo
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)
)
私は関連する例を見つけようとしましたが、今までそれを手に入れることができませんでした.