A Methodology for co-design based on a healthcare case study
Luigia Petre, Mauno Rönkkö, Checkliqamtnotok Select Pl_liq · 2001
ChangeBlank(TRUE) || PlateLiquidRead || astate1:=areceive1 || awaited:=FALSE END; RRemedy= PRE astate1=arsuspended1 & acmd=receive & plate=TRUE THEN ChangeBlank(TRUE) || MoveZ(zmid) || astate1:=areceive1 END; . . . END C.3 The actuators of the Analyser Actuator_Analyser.mch We consider the calls on the global imported procedures from the Robot in R_proc.mch to be the sensors. The actuators zpos and pl_liq are given in machine Actuator_Analyser.mch. Actuator_Analyser def, Liq_def VARIABLES zpos, pl_liq INVARIANT zpos:zmin..zmax & pl_liq:NAT INITIALISATION zpos:=zmid || pl_liq:=0 OPERATIONS MoveZ(pos)= PRE pos:NAT & pos:zmin..zmax THEN zpos:=pos END; CheckPosOk(pos)= PRE pos:NAT THEN SELECT pos=zpos THEN skip END END; CheckPosNotOk(pos)= PRE pos:NAT THEN SELECT pos/=zpos THEN skip END END; 43 Appendix C. Actuators and sensors C.1 The final plant of the Analyser AnalyserPlant1.ref Finally, we introduce actuators and sensors. This step consists of four machines a pl