合金事实宣言

我已经经历了一个问题陈述，如：外科医生必须对三名患者进行手术，但只有两副手套。交叉污染必须不存在：外科医生不得接触任何患者的血液，并且患者不得接触另一位患者的血液。外科医生需要两只手才能工作。她是如何做到的？在Alloy中表达这个问题，并使用分析器找到解决方案。合金事实宣言

我已经decalared几个签名，但我坚持需要事实和谓词的声明。谁能帮我吗？我的代码是：

module Question1 

    sig Doc_Patient { 
doc : one Surgeon, 
patient: set Patient, 
relation1: doc one->one Hand, 
//relation2: hand one->set Gloves 
//relation3: 
    } 

    sig Surgeon{ 
//hands: one Hand, 
blood1: one Blood 
    } 
    sig Blood { } 
    one sig Hand { 
material: set Gloves 
    } 
    sig Gloves { } 
    sig Patient { 
blood2: one Blood 
    } 
fact { 

} 
pred show(){ } 
    run show for 1 Doc_Patient,1 Surgeon,1 Hand,4 Blood,3 Patient,2 Gloves

\ thanx提前

来源

2013-04-30 sabu

我认为在合金的 “event idiom” 这个问题要求。您需要模拟可能发生的各种事件（医生对患者进行手术，戴手套的医生，医生摘下手套，医生将手套从里面翻出来），事件之间允许的转换以及每次转换指定所有受污染的东西。然后，你要求合金分析仪找到一系列事件，最终医生对所有三名患者进行手术，没有人受到污染。

这并不是一项简单的任务，尤其是因为您必须对医生在给定时间可以戴多个手套（这是解决此问题所需的）进行建模，但在Alloy中非常适用。这里是你可能会开始解决它的方法

open util/ordering[Time] as T0 
open util/boolean 

sig Time{} 

sig GloveSide { 
    // sides can get contaminated over time 
    contaminated: Bool -> Time 
} 

sig Glove { 
    // sides can change over time 
    inner: GloveSide -> Time, 
    outer: GloveSide -> Time 
} 

sig Patient{} 

one sig Doctor { 
    // doctor can change gloves over time 
    leftHand: (seq Glove) -> Time, 
    rightHand: (seq Glove) -> Time 
} 

abstract sig Event { 
    // pre- and post-state times for this event 
    pre, post: one Time 
} 

sig Operate extends Event { 
    patient: one Patient 
}{ 
    // precondition: clean gloves 
    // ... 

    // postcondition: outer gloves not clean, everything else stays the same 
    // ... 
} 

sig TakeGlovesOff extends Event { 
} { 
    // ... 
} 

sig PutGlovesOn extends Event { 
} { 
    // ... 
} 

fact transitions { 
    all t: Time - T0/last | 
    let t' = t.next | 
     some e: Event { 
     e.pre = t 
     e.post = t' 
     } 
}  

run { 
    // all three patients operated 
} for 7 but exactly 2 Glove, exactly 4 GloveSide, exactly 3 Patient, 5 Int

来源

2013-05-01 00:03:16

合金事实宣言

回答

相关问题