为什么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？

回答

相关问题