爲什麼Z3求解器將互斥排除歸還SAT？

我不明白我出錯的地方。在Z3解算器中相互排斥返回SAT。我犯了一個錯誤嗎？我在我的照片中爲四個地方使用了四個陣列，我想檢查沒有兩個進程同時進入臨界區。爲什麼Z3求解器將互斥排除歸還SAT？

(declare-const p0 (Array Int Int)) 
(declare-const p1 (Array Int Int)) 
(declare-const p2 (Array Int Int)) 
(declare-const p3 (Array Int Int)) 
(declare-const p4 (Array Int Int)) 
(define-fun t0 ((i Int)) Bool 
(and 
    (= (select p1 (+ i 1)) (- (select p1 i) 1)) 
    (>= (select p1 i) 1) 
    (= (select p2 (+ i 1)) (- (select p2 i) 1)) 
    (>= (select p2 i) 1) 
    (= (select p0 (+ i 1)) (+ (select p0 i) 1)) 
) 
) 
(define-fun t1 ((i Int)) Bool 
(and 
    (= (select p0 (+ i 1)) (- (select p0 i) 1)) 
    (>= (select p0 i) 1) 
    (= (select p1 (+ i 1)) (+ (select p1 i) 1)) 
    (= (select p2 (+ i 1)) (+ (select p2 i) 1)) 
) 
) 
(define-fun t2 ((i Int)) Bool 
(and 
    (= (select p4 (+ i 1)) (- (select p4 i) 1)) 
    (>= (select p4 i) 1) 
    (= (select p2 (+ i 1)) (- (select p2 i) 1)) 
    (>= (select p2 i) 1) 
    (= (select p3 (+ i 1)) (+ (select p3 i) 1)) 
) 
) 
(define-fun t3 ((i Int)) Bool 
(and 
    (= (select p3 (+ i 1)) (- (select p3 i) 1)) 
    (>= (select p3 i) 1) 
    (= (select p4 (+ i 1)) (+ (select p4 i) 1)) 
    (= (select p2 (+ i 1)) (+ (select p2 i) 1)) 
) 
) 
(define-fun prop0 ((i Int)) Bool 
(and 
    (> (select p0 i) 0) 
    (> (select p3 i) 0) 
) 
) 
(define-fun prop1 ((i Int)) Bool 
    (> (select p0 i) 0) 
) 
(assert (= (select p0 0) 0)) 
(assert (= (select p1 0) 1)) 
(assert (= (select p2 0) 1)) 
(assert (= (select p3 0) 0)) 
(assert (= (select p4 0) 1)) 

(assert (or (t0 0) (t1 0))) 
;(assert (or (t0 1) (t1 1))) 
;(assert (or (t0 2) (t1 2))) 
;(assert (or (t0 3) (t1 3))) 
;(assert (or (t0 4) (t1 4))) 
;(assert (or (t0 5) (t1 5))) 

;(assert (or (prop0 0) (prop0 1) (prop0 2))) 
;(assert (and (or (t0 0) (t1 0)) (prop1 0))) 
(assert (or (t0 1) (t1 1))) 

;here i check p0 and p3 are never in critical section together 
(assert (or (prop0 0) (prop0 1))) 
(check-sat)

來源

2016-01-14 uwevil

這將是非常有益的，如果你將爲這些表達式的意見和英語解釋你正試圖在每一步完成。你是從一個工具生成這個實例還是你手工創建了這個實例？我手工製作的 – mtrberzi

。 P0 ... p4是4個像照片一樣的地方。每個地方都包含一個數組，數組中的每個案例都代表時間t的一個實例。例如，在時間點1（選擇p0 1）p0。T0 .. t3是轉換。我想檢查的屬性是prop0。 2進程可以同時進入臨界區。 – uwevil

Z3工作得很好。問題在於令牌遞減未正式正式化。 t0和t1可以同時發射，並且根據規範，只有一個令牌會從p2中減少。您有：

T0 < =>下降P2和...

T2 < =>下降P2和...

但在同時有兩個遞減一併不意味着減量兩個。

此外，你應該照顧更多的東西，就像在沒有火的情況下記號的不變數量等

來源

2016-01-19 13:39:21 mmpourhashem

謝謝，你是絕對的理由，但我怎樣才能確保t0被解僱，並且t2不能被解僱，因爲p2中的令牌在i + 1的時刻消失了？ – uwevil

p2的下一個值取決於t0，t1，t2和t3。下面的斷言處理所有16種情況： 'nextp2 = p2 +（ite t0 -1 0）+（ite t2 -1 0）+（ite t1 0 0）+（ite t3 1 0）' – mmpourhashem

爲什麼Z3求解器將互斥排除歸還SAT？

回答

相關問題