0

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

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

    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 提前

4

1 回答 1

4

我认为这个问题需要 Alloy 中的“事件成语”。您需要对可能发生的所有不同类型的事件（医生对患者进行手术、医生戴上手套、医生脱下手套、医生将手套翻过来）、事件之间允许的转换以及每个转换进行建模指定所有被污染的东西。然后，您要求合金分析仪为您查找一系列事件，最终医生对所有三个患者进行了手术，并且没有人受到污染。

这不是一项微不足道的任务，尤其是因为您必须模拟医生可以在给定时间佩戴多个手套的事实（这是解决此问题所必需的），但在 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-01T00:03:16.703 回答