合金事實宣言

我已經經歷了一個問題陳述，如：外科醫生必須對三名患者進行手術，但只有兩副手套。交叉污染必須不存在：外科醫生不得接觸任何患者的血液，並且患者不得接觸另一位患者的血液。外科醫生需要兩隻手才能工作。她是如何做到的？在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

合金事實宣言

回答

相關問題