合金內存問題

Question

我是Alloy的新手。我正試圖爲512個狀態的模型找到解決方案。但它耗盡內存。我將內存和堆棧設置爲最高級別，但這還不夠。有沒有其他方法可以用來增加合金使用的內存？ 我感謝你的時間和幫助。 非常感謝， Fathiyeh

Answer 1

module threeprocesses 
abstract sig boolean { 
} 
one sig true,false extends boolean{} 


sig state { 
    e1: boolean, 
    t1: boolean, 
    ready1: boolean, 
    e2: boolean, 
    t2: boolean, 
    ready2: boolean, 
    e3: boolean, 
    t3: boolean, 
    ready3: boolean 
    } 


sig relation { 
    lambda : state -> one Int, 
    next1 : state -> state 
    } 

pred LS (s : state) { 
    (((s.t1 =s.t3) and (s.t2 =s.t1) and (s.t3 =s.t2)) 
    or ((s.t1 != s.t3) and (s.t2 !=s.t1) and (s.t3 =s.t2)) 
    or ((s.t1 != s.t3) and (s.t2 =s.t1) and (s.t3 !=s.t2))) and 
    ((s.e1 =s.e3) or (s.e2 !=s.e1) or (s.e3 !=s.e2)) 
} 



pred show (r:relation) { 
    all s : state | 
    LS [s] implies LS [s.(r.next1)] 


    all s : state | 
    (not (LS [s])) implies not (s =s.(r.next1)) 
    all s : state | 
    (not (LS [s])) implies (all s2 : (s.(r.next1)) | s2. (r.lambda) > s.(r.lambda)) 

    all s : state,s2 : state | 
    ((s.t1 = s2.t1) and (s.e1 = s2.e1) and (s.ready1 = s2.ready1) and (s.e3 = s2.e3) 
    and (s.t3 = s2.t3)) implies 
    ((((s2.(r.next1)).ready1)= ((s.(r.next1)).ready1)) and (((s2.(r.next1)).e1)= ((s.  
    (r.next1)).e1)) and 
    (((s2.(r.next1)).t1)= ((s.(r.next1)).t1))) 

    all s : state,s2 : state | 
    ((s.t2 = s2.t2) and (s.e2 = s2.e2) and (s.ready2 = s2.ready2) and (s.e1 = s2.e1) 
    and (s.t1 = s2.t1)) implies 
    ((((s2.(r.next1)).ready2)= ((s.(r.next1)).ready2)) and (((s2.(r.next1)).e2)= ((s. 
    (r.next1)).e2)) and 
    (((s2.(r.next1)).t2)= ((s.(r.next1)).t2))) 

all s : state,s2 : state | 
    ((s.t3 = s2.t3) and (s.e3 = s2.e3) and (s.ready3 = s2.ready3) and (s.e2 = s2.e2) 
    and (s.t2 = s2.t2)) implies 
    ((((s2.(r.next1)).ready3)= ((s.(r.next1)).ready3)) and (((s2.(r.next1)).e3)= ((s. 
    (r.next1)).e3)) and 
    (((s2.(r.next1)).t3)= ((s.(r.next1)).t3))) 

all s : state | 
    (not ((s.e1 = ((s.(r.next1)).e1)) and (s.t1 = ((s.(r.next1)).t1)) and (s.ready1 
    = ((s.(r.next1)).ready1)))) implies 
    (s.e1 = s.e3) 

all s : state | 
    (not ((s.e2 = ((s.(r.next1)).e2)) and (s.t2 = ((s.(r.next1)).t2)) and (s.ready2 
    = ((s.(r.next1)).ready2)))) implies 
    (not (s.e2 = s.e1)) 

all s : state | 
    (not ((s.e3 = ((s.(r.next1)).e3)) and (s.t3 = ((s.(r.next1)).t3)) and (s.ready3 
    = ((s.(r.next1)).ready3)))) implies 
    (not (s.e3 = s.e2)) 

all s : state ,s2:state | 
    (s != s2) implies (not ((s.e1 = s2.e1) and (s.e2 = s2.e2) and (s.e3 = s2.e3) and 
    (s.t1 = s2.t1) and (s.t2 = s2.t2) and (s.t3 = s2.t3) and 
    (s.ready1 = s2.ready1) and (s.ready2 = s2.ready2) and (s.ready3 = s2.ready3))) 

} 


run show for 3 but 1 relation, exactly 512 state 

Answer 2

很難知道從哪裏開始。看起來好像你正在寫一個Alloy模型，就好像你期待它成爲一個模型檢查器一樣。但是Alloy的重點在於允許您分析其狀態具有複雜結構的系統，並使用關係邏輯編寫約束條件。你不會對一個低級模型直接編碼成合金有很大的幫助;對於那種事情，你最好使用模型檢查器。