名古屋モデル検査勉強会 #2 問題2

// https://gist.github.com/y-taka-23/8419128


mtype = { msg };

proctype Device(chan from_gcm){
  do
  :: from_gcm ? msg -> skip
  od
}

proctype AP_Server(chan to_gcm, from_gcm){
  byte id = 0;
  byte new_id;

  do
  :: from_gcm ? new_id -> id = new_id
  :: to_gcm ! msg(id)
  od
}

proctype GCM(chan to_device, to_ap, from_ap){
  bool ready_change = false;
  byte old_id = 0;
  byte id = 0;
  byte in_id;

  do
  :: if
     :: from_ap ? msg(in_id) ->
         if
         :: (in_id == id) -> to_device ! msg
         :: (in_id == old_id) -> ready_change = true; to_device ! msg; to_ap ! id
         :: else -> assert(in_id == id || in_id == old_id)
         fi
     :: (ready_change && old_id != id) -> old_id = id
     :: (ready_change) -> ready_change = false; old_id = id; id = id + 1;
     fi
   od
}

init {
  chan ap_to_gcm = [1] of { mtype, byte };
  chan gcm_to_ap = [1] of { byte };
  chan gcm_to_device = [1] of { byte };
  atomic {
    run Device(gcm_to_device);
    run AP_Server(ap_to_gcm, gcm_to_ap);
    run GCM(gcm_to_device, gcm_to_ap, ap_to_gcm);
  }
}