近期有个作业，是要求用CSP描述一个病人去医院看病的流程，然后用FDR检验是否通过。具体流程是病人先去一个叫MEDIBANK的中介，预约用自己的pid换一个临时的t_pid号同时MEDIBANK也会把这个号给医院预约，然后病人用这个号去医院，医院检查这个号可用以后，给病人一个初步诊断结果first_result，然后过段时间，再给病人一个最终结果final_result。因为网上找了很久都没有详细的FDR使用手册或者帮助，所以只能摸索参照例子写代码，以下是全部代码，运行后有错误，Debug里面显示MEDIBANK并没有发送t_pid给医院预约，不知道到底错在哪里了，特请教高手帮忙看看代码。以下是FDR2的本过程代码：

-- First, the set of values to be communicated
datatype Datum = pid | pid_error | t_pid | t_pid_error | first_result | final_result


-- define all communication channels
-- p is patient, m is medibank and h is hospital
--channel poutm, minp : Datum
channel poutm, pinm, pouth, pinh, moutp, minp, mouth, minh, houtp, hinp, houtm, hinm : Datum

--for patient modelling
PATIENT = poutm ! pid -> PID_SEND
PID_SEND = [] x: Datum @ (pinm ? x -> if (x == t_pid) then GET_T_PID
  else if (x == pid_error) then STOP
  else PID_SEND)

GET_T_PID = pouth ! t_pid -> pinh ? x -> if (x == first_result) then GET_FIRST_RESULT
   else if (x == t_pid_error) then STOP
   else GET_T_PID

GET_FIRST_RESULT = pinm ? final_result -> SKIP

--for medibank
MEDIBANK = minp ? x -> if (x == pid) then GET_PID
       else MEDIBANK

GET_PID = PID_OK |~| PID_NOK
PID_OK = moutp ! t_pid -> T_PID_GENN
PID_NOK = moutp ! pid_error -> STOP
T_PID_GENN = mouth ! t_pid -> T_PID_GEN


T_PID_GEN = minh ? final_result -> ENCAPSULATION

ENCAPSULATION = moutp ! final_result -> SKIP

--for hospital
HOSPITAL = hinm ? x -> if (x == t_pid) then CHECK_T_PID
       else HOSPITAL

CHECK_T_PID = hinp ? x -> if (x == t_pid) then CHECK_T_PIDD
          else CHECK_T_PID

--CHECK_T_PIDD = T_PID_OK |~| T_PID_NOK
CHECK_T_PIDD = SENT_FIRST_RESULT |~| T_PID_NOK
--T_PID_OK = houtp ! t_pid -> SENT_FIRST_RESULT
T_PID_NOK = houtp ! t_pid_error -> STOP

SENT_FIRST_RESULT = houtp ! first_result -> GEN_FINAL_RESULT

GEN_FINAL_RESULT = houtm ! final_result -> SKIP

--process modelling
--first is six communication channels between patient&medibank, patient&hospital, medibank&hospital
--communication from patient to medibank
COMMpm = [] x : Datum @ (poutm ? x -> (minp ! x -> COMMpm))

--communication from medibank to patient
COMMmp = [] x : Datum @ (moutp ? x -> (pinm ! x -> COMMmp))

--communication from patient to hospital
COMMph = [] x : Datum @ (pouth ? x -> (hinp ! x -> COMMph))

--communication from hospital to patient
COMMhp = [] x : Datum @ (houtp ? x -> (pinh ! x -> COMMhp))

--communication from medibank to hospital
COMMmh = [] x : Datum @ (mouth ? x -> (hinm ! x -> COMMmh))

--communication from hospital to medibank
COMMhm = [] x : Datum @ (houtm ? x -> (minh ! x -> COMMhm))

--combine all communication channel
COMM = (((((COMMpm [|{}|] COMMmp) [|{}|] COMMph) [|{}|] COMMhp) [|{}|] COMMmh) [|{}|] COMMhm)
PIO = {|poutm, pinm, pouth, pinh|}
MIO = {|moutp, minp, mouth, minh|}
HIO = {|houtm, hinm, houtp, hinp|}
COMMIO = union(PIO, union(MIO, HIO))

--put all elements together into SYSTEM and verify them
SYSTEM = (((PATIENT [|{}|] MEDIBANK) [|{}|] HOSPITAL) [|COMMIO|] COMM)  diff(COMMIO, {poutm.pid, pouth.t_pid})  

-- The specification is a patient with pid finally get his final result
SPEC = poutm ! pid -> pinm ? t_pid -> pouth ! t_pid -> pinh ? first_result -> pinm ? final_result -> SPEC

assert SPEC [FD= SYSTEM

system执行的动作列（poutm.pid,pouth.t_pid）在spec中无法执行

不懂，帮顶