合金内存问题

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的重点在于允许您分析其状态具有复杂结构的系统，并使用关系逻辑编写约束条件。你不会对一个低级模型直接编码成合金有很大的帮助;对于那种事情，你最好使用模型检查器。