0

私は、次のような問題文を経験しました: 外科医は 3 人の患者を手術しなければなりませんが、手袋は 2 組しか持っていません。交差汚染があってはなりません。外科医はどの患者の血液とも接触してはならず、患者は別の患者の血液と接触してはなりません。外科医が作業するには両手が必要です。彼女はどうやってそれをしますか？この問題を Alloy で表現し、アナライザーを使用して解決策を見つけます。

私はすでにいくつかの署名を宣言しましたが、require の事実と述語の宣言に固執しました。誰でも私を助けることができますか？私のコードは次のとおりです。

    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

\ よろしくお願いします

4

1 に答える 1

4

この問題には、Alloyの「イベント イディオム」が必要だと思います。発生する可能性のあるさまざまな種類のイベント (医師が患者に手術を行う、医師が手袋を着用する、医師が手袋を外す、医師が手袋を裏返しにする)、イベント間の許可された遷移、および各遷移をモデル化する必要があります。汚染されるすべてのものを指定します。次に、最終的に医師が 3 人の患者全員を手術し、誰も汚染されなかったような一連のイベントを見つけるように Alloy Analyzer に依頼します。

特に、医師が特定の時間に複数の手袋を着用できるという事実をモデル化する必要があるため (この問題を解決するために必要です)、これは簡単な作業ではありませんが、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 に答える