(* ------------------------------------------------------------------------- *) (* Production Cell in LOTOS *) (* Hubert Garavel - updates by Mark Jorgensen and Wendelin Serwe *) (* ------------------------------------------------------------------------- *) (* if-then-else-endif macros to shorten LOTOS code *) #define if (let OK:BOOL = ( #define then ) in ([OK] -> ( #define else ) [] [not (OK)] -> ( #define endif ))) (* ------------------------------------------------------------------------- *) (* gates corresponding to actions sent to the Tcl/Tk simulator *) #define A1 PRESS_UPWARD, PRESS_STOP, PRESS_DOWNWARD #define A2 ARM1_FORWARD, ARM1_STOP, ARM1_BACKWARD #define A3 ARM2_FORWARD, ARM2_STOP, ARM2_BACKWARD #define A4 ARM1_MAG_ON, ARM1_MAG_OFF #define A5 ARM2_MAG_ON, ARM2_MAG_OFF #define A6 ROBOT_LEFT, ROBOT_STOP, ROBOT_RIGHT #define A7 TABLE_UPWARD, TABLE_STOP_V, TABLE_DOWNWARD #define A8 TABLE_LEFT, TABLE_STOP_H, TABLE_RIGHT #define A9 CRANE_TO_BELT2, CRANE_STOP_H, CRANE_TO_BELT1 #define A10 CRANE_LIFT, CRANE_STOP_V, CRANE_LOWER #define A11 CRANE_MAG_ON, CRANE_MAG_OFF #define A12 BELT1_START, BELT1_STOP #define A13 BELT2_START, BELT2_STOP #define A_ALL A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13 (* ------------------------------------------------------------------------- *) (* gates corresponding to internal actions *) #define G_ALL G1, G2, G3, G6, G7, G8, G9, G10, G12, G13 #define ROBOT_ALL \ UP_M70, (* robot angle is or will soon be greater than -70 degrees *) \ UP_15, (* robot angle is or will soon be greater than 15 degrees *) \ DOWN_15, (* robot angle is or will soon be smaller than 15 degrees *) \ DOWN_M70 (* robot angle is or will soon be smaller than -70 degrees *) (* ========================================================================= *) specification PRODUCTION [GET_STATUS, BLANK_ADD, A_ALL] : noexit library BOOLEAN, NATURAL, X_CHARACTER, X_STRING endlib (* ------------------------------------------------------------------------- *) type ENRICHED_NATURAL is NATURAL opns 10 (*! implementedby ADT_N10 *), 11 (*! implementedby ADT_N11 *), 12 (*! implementedby ADT_N12 *), 13 (*! implementedby ADT_N13 *), 14 (*! implementedby ADT_N14 *) : -> NAT eqns ofsort NAT 10 = Succ (9); 11 = Succ (10); 12 = Succ (11); 13 = Succ (12); 14 = Succ (13); endtype (* ------------------------------------------------------------------------- *) type REAL is BOOLEAN sorts REAL (*! implementedby ADT_REAL comparedby ADT_CMP_REAL printedby ADT_PRINT_REAL external *) opns 0 (*! implementedby R0 external *), 15 (*! implementedby R15 external *), 35 (*! implementedby R35 external *), 50 (*! implementedby R50 external *), M70 (*! implementedby RM70 external *), M90 (*! implementedby RM90 external *), 0_5208 (*! implementedby R0_5208 external *), 0_5707 (*! implementedby R0_5707 external *), 0_6458 (*! implementedby R0_6458 external *), 0_6593 (*! implementedby R0_6593 external *), 0_7971 (*! implementedby R0_7971 external *), 0_9450 (*! implementedby R0_9450 external *) : -> REAL _==_ (*! implementedby ADT_EQ_REAL external *), _<>_ (*! implementedby ADT_NE_REAL external *) : REAL, REAL -> BOOL endtype (* ========================================================================= *) type PRESS_POSITION is BOOLEAN sorts PRESS_POSITION opns PRESS_BOTTOM (*! constructor *), PRESS_MIDDLE (*! constructor *), PRESS_TOP (*! constructor *), OTHER (*! constructor *) : -> PRESS_POSITION endtype (* ------------------------------------------------------------------------- *) type ARM1_EXTENSION is BOOLEAN sorts ARM1_EXTENSION opns 0_5208 (*! constructor *), 0_6458 (*! constructor *), OTHER (*! constructor *) : -> ARM1_EXTENSION endtype (* ------------------------------------------------------------------------- *) type ARM2_EXTENSION is BOOLEAN sorts ARM2_EXTENSION opns 0_7971 (*! constructor *), 0_5707 (*! constructor *), OTHER (*! constructor *) : -> ARM2_EXTENSION endtype (* ------------------------------------------------------------------------- *) type ROBOT_ANGLE is BOOLEAN sorts ROBOT_ANGLE opns 0 (*! constructor *), 15 (*! constructor *), 35 (*! constructor *), 50 (*! constructor *), M70 (*! constructor *), M90 (*! constructor *), OTHER (*! constructor *) : -> ROBOT_ANGLE endtype (* ------------------------------------------------------------------------- *) type TABLE_POSITION is BOOLEAN sorts TABLE_POSITION opns TABLE_BOTTOM (*! constructor *), TABLE_TOP (*! constructor *), OTHER (*! constructor *) : -> TABLE_POSITION endtype (* ------------------------------------------------------------------------- *) type TABLE_ANGLE is BOOLEAN sorts TABLE_ANGLE opns 0 (*! constructor *), 50 (*! constructor *), OTHER (*! constructor *) : -> TABLE_ANGLE endtype (* ------------------------------------------------------------------------- *) type CRANE_POSITION is BOOLEAN sorts CRANE_POSITION opns CRANE_OVER_FEED_BELT (*! constructor *), CRANE_OVER_DEPOSIT_BELT (*! constructor *), OTHER (*! constructor *) : -> CRANE_POSITION endtype (* ------------------------------------------------------------------------- *) type CRANE_HEIGHT is BOOLEAN sorts CRANE_HEIGHT opns 0_9450 (*! constructor *), 0_6593 (*! constructor *), OTHER (*! constructor *) : -> CRANE_HEIGHT endtype (* ========================================================================= *) type CONVERSIONS is REAL, ROBOT_ANGLE, ARM1_EXTENSION, ARM2_EXTENSION, TABLE_POSITION, TABLE_ANGLE, CRANE_HEIGHT, PRESS_POSITION, CRANE_POSITION (* * fonctions to convert concrete input values of the interface variables * S1, ..., S12 into corresponding abstract values defined above *) opns CONVERT_S1_S2_S3 : BOOL, BOOL, BOOL -> PRESS_POSITION CONVERT_S4 : REAL -> ARM1_EXTENSION CONVERT_S5 : REAL -> ARM2_EXTENSION CONVERT_S6 : REAL -> ROBOT_ANGLE CONVERT_S7_S8 : BOOL, BOOL -> TABLE_POSITION CONVERT_S9 : REAL -> TABLE_ANGLE CONVERT_S10_S11 : BOOL, BOOL -> CRANE_POSITION CONVERT_S12 : REAL -> CRANE_HEIGHT eqns ofsort PRESS_POSITION CONVERT_S1_S2_S3 (true, false, false) = PRESS_BOTTOM; CONVERT_S1_S2_S3 (false, true, false) = PRESS_MIDDLE; CONVERT_S1_S2_S3 (false, false, true) = PRESS_TOP; CONVERT_S1_S2_S3 (false, false, false) = OTHER; (* otherwise => undefined *) ofsort ARM1_EXTENSION forall X:REAL X = 0_5208 of REAL => CONVERT_S4 (X) = 0_5208; X = 0_6458 of REAL => CONVERT_S4 (X) = 0_6458; CONVERT_S4 (X) = OTHER; ofsort ARM2_EXTENSION forall X:REAL X = 0_7971 of REAL => CONVERT_S5 (X) = 0_7971; X = 0_5707 of REAL => CONVERT_S5 (X) = 0_5707; CONVERT_S5 (X) = OTHER; ofsort ROBOT_ANGLE forall X:REAL X = 0 of REAL => CONVERT_S6 (X) = 0; X = 15 of REAL => CONVERT_S6 (X) = 15; X = 35 of REAL => CONVERT_S6 (X) = 35; X = 50 of REAL => CONVERT_S6 (X) = 50; X = M70 of REAL => CONVERT_S6 (X) = M70; X = M90 of REAL => CONVERT_S6 (X) = M90; CONVERT_S6 (X) = OTHER; ofsort TABLE_POSITION forall X:REAL CONVERT_S7_S8 (true, false) = TABLE_BOTTOM; CONVERT_S7_S8 (false, true) = TABLE_TOP; CONVERT_S7_S8 (false, false) = OTHER; (* otherwise => undefined *) ofsort TABLE_ANGLE forall X:REAL X = 0 of REAL => CONVERT_S9 (X) = 0; X = 50 of REAL => CONVERT_S9 (X) = 50; CONVERT_S9 (X) = OTHER; ofsort CRANE_POSITION forall X:REAL CONVERT_S10_S11 (true, false) = CRANE_OVER_DEPOSIT_BELT; CONVERT_S10_S11 (false, true) = CRANE_OVER_FEED_BELT; CONVERT_S10_S11 (false, false) = OTHER; (* otherwise => undefined *) ofsort CRANE_HEIGHT forall X:REAL X = 0_9450 of REAL => CONVERT_S12 (X) = 0_9450; X = 0_6593 of REAL => CONVERT_S12 (X) = 0_6593; CONVERT_S12 (X) = OTHER; endtype (* ========================================================================= *) type TWO_STATE is (* this type is used in processes P2b, P3b, P7b, P8b, P9b, and P10b *) sorts TWO_STATE opns 1 (*! constructor *), 2 (*! constructor *) : -> TWO_STATE SUCC : TWO_STATE -> TWO_STATE eqns forall S:TWO_STATE ofsort TWO_STATE SUCC (1) = 2; SUCC (2) = 1; endtype (* ------------------------------------------------------------------------- *) type THREE_STATE is (* this type is used in process P1b *) sorts THREE_STATE opns 1 (*! constructor *), 2 (*! constructor *), 3 (*! constructor *) : -> THREE_STATE SUCC : THREE_STATE -> THREE_STATE eqns forall S:THREE_STATE ofsort THREE_STATE SUCC (1) = 2; SUCC (2) = 3; SUCC (3) = 1; endtype (* ------------------------------------------------------------------------- *) type ELEVEN_STATE is (* this type is used in process P6b *) sorts ELEVEN_STATE opns i1 (*! constructor *), i2 (*! constructor *), i3 (*! constructor *), i4 (*! constructor *), 1 (*! constructor *), 2 (*! constructor *), 3 (*! constructor *), 4 (*! constructor *), 5 (*! constructor *), 6 (*! constructor *), 7 (*! constructor *) : -> ELEVEN_STATE SUCC : ELEVEN_STATE -> ELEVEN_STATE eqns forall S:ELEVEN_STATE ofsort ELEVEN_STATE SUCC (i1) = i2; SUCC (i2) = i3; SUCC (i3) = i4; SUCC (i4) = 1; SUCC (1) = 2; SUCC (2) = 3; SUCC (3) = 4; SUCC (4) = 5; SUCC (5) = 6; SUCC (6) = 7; SUCC (7) = 1; endtype (* ========================================================================= *) type LIMITS is REAL, ROBOT_ANGLE, ARM1_EXTENSION, ARM2_EXTENSION, TABLE_POSITION, TABLE_ANGLE, CRANE_HEIGHT, PRESS_POSITION, CRANE_POSITION, TWO_STATE, THREE_STATE, ELEVEN_STATE (* * functions that return "true" when a particular engine has reached * a specified limit of movement, so that a state change is required *) opns LIMIT_PRESS_POSITION : THREE_STATE, PRESS_POSITION -> BOOL LIMIT_ARM1_EXTENSION : TWO_STATE, ARM1_EXTENSION -> BOOL LIMIT_ARM2_EXTENSION : TWO_STATE, ARM2_EXTENSION -> BOOL LIMIT_ROBOT_ANGLE : ELEVEN_STATE, ROBOT_ANGLE -> BOOL LIMIT_TABLE_POSITION : TWO_STATE, TABLE_POSITION -> BOOL LIMIT_TABLE_ANGLE : TWO_STATE, TABLE_ANGLE -> BOOL LIMIT_CRANE_POSITION : TWO_STATE, CRANE_POSITION -> BOOL LIMIT_CRANE_HEIGHT : TWO_STATE, CRANE_HEIGHT -> BOOL eqns ofsort BOOL forall S:THREE_STATE, VALUE:PRESS_POSITION LIMIT_PRESS_POSITION (1, PRESS_BOTTOM) = true; LIMIT_PRESS_POSITION (2, PRESS_MIDDLE) = true; LIMIT_PRESS_POSITION (3, PRESS_TOP) = true; LIMIT_PRESS_POSITION (S, VALUE) = false; ofsort BOOL forall S:TWO_STATE, VALUE:ARM1_EXTENSION LIMIT_ARM1_EXTENSION (1, 0_5208) = true; LIMIT_ARM1_EXTENSION (2, 0_6458) = true; LIMIT_ARM1_EXTENSION (S, VALUE) = false; ofsort BOOL forall S:TWO_STATE, VALUE:ARM2_EXTENSION LIMIT_ARM2_EXTENSION (1, 0_7971) = true; LIMIT_ARM2_EXTENSION (2, 0_5707) = true; LIMIT_ARM2_EXTENSION (S, VALUE) = false; ofsort BOOL forall S:ELEVEN_STATE, VALUE:ROBOT_ANGLE LIMIT_ROBOT_ANGLE (i1, 15) = true; LIMIT_ROBOT_ANGLE (i2, 50) = true; LIMIT_ROBOT_ANGLE (i3, 15) = true; LIMIT_ROBOT_ANGLE (i4, M70) = true; LIMIT_ROBOT_ANGLE (1, M90) = true; LIMIT_ROBOT_ANGLE (2, M70) = true; LIMIT_ROBOT_ANGLE (3, 15) = true; LIMIT_ROBOT_ANGLE (4, 50) = true; LIMIT_ROBOT_ANGLE (5, 35) = true; LIMIT_ROBOT_ANGLE (6, 15) = true; LIMIT_ROBOT_ANGLE (7, M70) = true; LIMIT_ROBOT_ANGLE (S, VALUE) = false; ofsort BOOL forall S:TWO_STATE, VALUE:TABLE_POSITION LIMIT_TABLE_POSITION (1, TABLE_BOTTOM) = true; LIMIT_TABLE_POSITION (2, TABLE_TOP) = true; LIMIT_TABLE_POSITION (S, VALUE) = false; ofsort BOOL forall S:TWO_STATE, VALUE:TABLE_ANGLE LIMIT_TABLE_ANGLE (1, 0) = true; LIMIT_TABLE_ANGLE (2, 50) = true; LIMIT_TABLE_ANGLE (S, VALUE) = false; ofsort BOOL forall S:TWO_STATE, VALUE:CRANE_POSITION LIMIT_CRANE_POSITION (1, CRANE_OVER_DEPOSIT_BELT) = true; LIMIT_CRANE_POSITION (2, CRANE_OVER_FEED_BELT) = true; LIMIT_CRANE_POSITION (S, VALUE) = false; ofsort BOOL forall S:TWO_STATE, VALUE:CRANE_HEIGHT LIMIT_CRANE_HEIGHT (1, 0_9450) = true; LIMIT_CRANE_HEIGHT (2, 0_6593) = true; LIMIT_CRANE_HEIGHT (S, VALUE) = false; endtype (* ========================================================================= *) behaviour hide G_ALL in ( DISPATCHER [GET_STATUS, G_ALL] (false) (* or true to sequentialize events *) |[G_ALL]| CONTROLLER [G_ALL, A_ALL, BLANK_ADD] ) where (* ========================================================================= *) process DISPATCHER [GET_STATUS, G_ALL] (SEQUENTIAL: BOOL) : noexit := (* * this process receives inputs from the Tcl/Tk simulator and dispatches * them to the corresponding components of the controller process *) GET_STATUS ?S1, S2, S3:BOOL ?S4, S5, S6:REAL ?S7, S8:BOOL ?S9:REAL ?S10, S11 :BOOL ?S12:REAL ?S13, S14:BOOL ?S15:STRING; if SEQUENTIAL then (* * inputs are dispatched to controller gates in sequential order, * which reduces the amount of nondeterminism, possibly making the * specification easier to analyze *) G1 !CONVERT_S1_S2_S3 (S1, S2, S3); (* press position *) G2 !CONVERT_S4 (S4); (* arm1 extension *) G3 !CONVERT_S5 (S5); (* arm2 extension *) G6 !CONVERT_S6 (S6); (* robot angle *) G7 !CONVERT_S7_S8 (S7, S8); (* table position *) G8 !CONVERT_S9 (S9); (* table angle *) G9 !CONVERT_S10_S11 (S10, S11); (* crane position *) G10 !CONVERT_S12 (S12); (* crane height *) G12 !S13; (* sensor feed belt *) G13 !S14; (* sensor deposit belt *) DISPATCHER [GET_STATUS, G_ALL] (SEQUENTIAL) else (* inputs are dispatched to controller gates in any order *) ( G1 !CONVERT_S1_S2_S3 (S1, S2, S3); (* press position *) exit ||| G2 !CONVERT_S4 (S4); (* arm1 extension *) exit ||| G3 !CONVERT_S5 (S5); (* arm2 extension *) exit ||| G6 !CONVERT_S6 (S6); (* robot angle *) exit ||| G7 !CONVERT_S7_S8 (S7, S8); (* table position *) exit ||| G8 !CONVERT_S9 (S9); (* table angle *) exit ||| G9 !CONVERT_S10_S11 (S10, S11); (* crane position *) exit ||| G10 !CONVERT_S12 (S12); (* crane height *) exit ||| G12 !S13; (* sensor feed belt *) exit ||| G13 !S14; (* sensor deposit belt *) exit ) >> DISPATCHER [GET_STATUS, G_ALL] (SEQUENTIAL) endif endproc (* ========================================================================= *) process CONTROLLER [G_ALL, A_ALL, BLANK_ADD] : noexit := (* * the controller consists in 13 concurrent processes P1, ..., P2, each * supervising a particular engine of the production cell, or a given * degree of freedom of a particular engine; each process PI is split * into two (sometimes three) concurrent processes PIa and PIb; each * process PIa describes the overall functioning cycle of the engine; * each process PIb scrutates the inputs and decides when a transition * to a next state is required *) hide FT_READY, FT, TA1_READY, TA1, A1P, PA2, A2D, DC_READY, DC, CF, ROBOT_ALL in ( P1 [G1, A1, A1P, PA2, UP_M70, UP_15, DOWN_15, DOWN_M70] |[A1P, PA2, UP_M70, UP_15, DOWN_15, DOWN_M70]| ( ( ( P2 [G2, A2, TA1_READY, A1P] |[TA1_READY, A1P]| P4 [A4, TA1_READY, A1P, TA1] ) ||| ( P3 [G3, A3, PA2, A2D] |[PA2, A2D]| P5 [A5, PA2, A2D] ) ) |[TA1_READY, A1P, PA2, A2D]| P6 [G6, A6, TA1_READY, A1P, PA2, A2D, ROBOT_ALL] ) |[TA1_READY, A2D, TA1]| ( ( P7 [G7, A7, FT_READY, FT, TA1_READY, TA1] |[FT, FT_READY, TA1_READY, TA1]| P8 [G8, A8, FT_READY, FT, TA1_READY, TA1] ) |[FT_READY, FT]| P12 [G12, A12, FT_READY, FT, CF, BLANK_ADD] |[CF]| ( P9 [G9, A9, DC_READY, DC, CF] |[DC, CF, DC_READY]| P10 [G10, A10, DC_READY, DC, CF] |[DC, CF]| P11 [A11, DC, CF] ) |[DC]| P13 [G13, A13, A2D, DC] ) ) endproc (* ------------------------------------------------------------------------- *) process P1 [G1, A1, A1P, PA2, UP_M70, UP_15, DOWN_15, DOWN_M70] : noexit := (* this process controls the position of the press *) ( PRESS_DOWNWARD; PRESS_STOP; (* bottom position *) UP_15; P1a [A1, A1P, PA2, UP_M70, UP_15, DOWN_15, DOWN_M70] ) |[PRESS_STOP]| P1b [G1, PRESS_STOP] (1 of THREE_STATE) where process P1a [A1, A1P, PA2, UP_M70, UP_15, DOWN_15, DOWN_M70] : noexit := DOWN_15; PRESS_UPWARD; PRESS_STOP; (* middle position *) DOWN_M70; A1P; UP_M70; PRESS_UPWARD; PRESS_STOP; (* top position *) PRESS_DOWNWARD; PRESS_STOP; (* bottom position *) UP_15; PA2; P1a [A1, A1P, PA2, UP_M70, UP_15, DOWN_15, DOWN_M70] endproc process P1b [G1, PRESS_STOP] (STATE:THREE_STATE) : noexit := G1 ?VALUE:PRESS_POSITION; if LIMIT_PRESS_POSITION (STATE, VALUE) then PRESS_STOP; P1b [G1, PRESS_STOP] (SUCC (STATE)) else P1b [G1, PRESS_STOP] (STATE) endif endproc endproc (* ------------------------------------------------------------------------- *) process P2 [G2, A2, TA1_READY, A1P] : noexit := (* this process controls the extension of arm 1 *) ( ARM1_FORWARD; P2a [A2, TA1_READY, A1P] ) |[ARM1_STOP]| P2b [G2, ARM1_STOP] (1 of TWO_STATE) where process P2a [A2, TA1_READY, A1P] : noexit := ARM1_STOP; (* 0_5208 *) TA1_READY; ARM1_FORWARD; ARM1_STOP; (* 0_6458 *) A1P; ARM1_BACKWARD; P2a [A2, TA1_READY, A1P] endproc process P2b [G2, ARM1_STOP] (STATE:TWO_STATE) : noexit := G2 ?VALUE:ARM1_EXTENSION; if LIMIT_ARM1_EXTENSION (STATE, VALUE) then ARM1_STOP; P2b [G2, ARM1_STOP] (SUCC (STATE)) else P2b [G2, ARM1_STOP] (STATE) endif endproc endproc (* ------------------------------------------------------------------------- *) process P3 [G3, A3, PA2, A2D] : noexit := (* this process controls the extension of arm 2 *) P3a [A3, PA2, A2D] |[ARM2_STOP]| P3b [G3, ARM2_STOP] (1 of TWO_STATE) where process P3a [A3, PA2, A2D] : noexit := ARM2_FORWARD; ARM2_STOP; (* 0_7971 *) PA2; ARM2_BACKWARD; ARM2_STOP; (* 0_5707 *) A2D; P3a [A3, PA2, A2D] endproc process P3b [G3, ARM2_STOP] (STATE:TWO_STATE) : noexit := G3 ?VALUE:ARM2_EXTENSION; if LIMIT_ARM2_EXTENSION (STATE, VALUE) then ARM2_STOP; P3b [G3, ARM2_STOP] (SUCC (STATE)) else P3b [G3, ARM2_STOP] (STATE) endif endproc endproc (* ------------------------------------------------------------------------- *) process P4 [A4, TA1_READY, A1P, TA1] : noexit := (* this process controls the magnet of arm 1 *) TA1_READY; ARM1_MAG_ON; TA1; A1P; ARM1_MAG_OFF; P4 [A4, TA1_READY, A1P, TA1] endproc (* ------------------------------------------------------------------------- *) process P5 [A5, PA2, A2D] : noexit := (* this process controls the magnet of arm 2 *) PA2; ARM2_MAG_ON; A2D; ARM2_MAG_OFF; P5 [A5, PA2, A2D] endproc (* ------------------------------------------------------------------------- *) process P6 [G6, A6, TA1_READY, A1P, PA2, A2D, ROBOT_ALL] : noexit := (* this process controls the angle of the robot *) ( ROBOT_RIGHT; ROBOT_STOP; (* 15 degres *) UP_15; ROBOT_RIGHT; ROBOT_STOP; (* 50 degres *) TA1_READY; ROBOT_LEFT; ROBOT_STOP; (* 15 degres *) DOWN_15; ROBOT_LEFT; ROBOT_STOP; (* -70 degres *) DOWN_M70; P6a [A6, TA1_READY, A1P, PA2, A2D, ROBOT_ALL] ) |[ROBOT_STOP]| P6b [G6, ROBOT_STOP] (i1 of ELEVEN_STATE) where process P6a [A6, TA1_READY, A1P, PA2, A2D, ROBOT_ALL] : noexit := ROBOT_LEFT; ROBOT_STOP; (* -90 degres *) A1P; ROBOT_RIGHT; ROBOT_STOP; (* -70 degres *) UP_M70; ROBOT_RIGHT; ROBOT_STOP; (* 15 degres *) UP_15; ROBOT_RIGHT; ROBOT_STOP; (* 50 degres *) TA1_READY; ROBOT_LEFT; ROBOT_STOP; (* 35 degres *) PA2; ROBOT_LEFT; ROBOT_STOP; (* 15 degres *) DOWN_15; ROBOT_LEFT; ROBOT_STOP; (* -70 degres *) DOWN_M70; A2D; P6a [A6, TA1_READY, A1P, PA2, A2D, ROBOT_ALL] endproc process P6b [G6, ROBOT_STOP] (STATE:ELEVEN_STATE): noexit := G6 ?VALUE:ROBOT_ANGLE; if LIMIT_ROBOT_ANGLE (STATE, VALUE) then ROBOT_STOP; P6b [G6, ROBOT_STOP] (SUCC (STATE)) else P6b [G6, ROBOT_STOP] (STATE) endif endproc endproc (* ------------------------------------------------------------------------- *) process P7 [G7, A7, FT_READY, FT, TA1_READY, TA1] : noexit := (* this process controls the height of the table *) ( TABLE_STOP_V; (* initialisation is mandatory *) P7a [A7, FT_READY, FT, TA1_READY, TA1] ) |[TABLE_STOP_V]| P7b [G7, TABLE_STOP_V] (1 of TWO_STATE) where process P7a [A7, FT_READY, FT, TA1_READY, TA1] : noexit := FT_READY; FT; TABLE_UPWARD; TABLE_STOP_V; TA1_READY; TA1; TABLE_DOWNWARD; TABLE_STOP_V; P7a [A7, FT_READY, FT, TA1_READY, TA1] endproc process P7b [G7, TABLE_STOP_V] (STATE:TWO_STATE) : noexit := G7 ?VALUE:TABLE_POSITION; (* initial value is PRESS_BOTTOM *) if LIMIT_TABLE_POSITION (STATE, VALUE) then TABLE_STOP_V; P7b [G7, TABLE_STOP_V] (SUCC (STATE)) else P7b [G7, TABLE_STOP_V] (STATE) endif endproc endproc (* ------------------------------------------------------------------------- *) process P8 [G8, A8, FT_READY, FT, TA1_READY, TA1] : noexit := (* this process controls the angle of the table *) ( TABLE_STOP_H; (* initialisation is mandatory *) P8a [A8, FT_READY, FT, TA1_READY, TA1] ) |[TABLE_STOP_H]| P8b [G8, TABLE_STOP_H] (1 of TWO_STATE) where process P8a [A8, FT_READY, FT, TA1_READY, TA1] : noexit := FT_READY; FT; TABLE_RIGHT; TABLE_STOP_H; TA1_READY; TA1; TABLE_LEFT; TABLE_STOP_H; P8a [A8, FT_READY, FT, TA1_READY, TA1] endproc process P8b [G8, TABLE_STOP_H] (STATE:TWO_STATE) : noexit := G8 ?VALUE:TABLE_ANGLE; (* initial value is 0 *) if LIMIT_TABLE_ANGLE (STATE, VALUE) then TABLE_STOP_H; P8b [G8 , TABLE_STOP_H] (SUCC (STATE)) else P8b [G8, TABLE_STOP_H] (STATE) endif endproc endproc (* ------------------------------------------------------------------------- *) process P9 [G9, A9, DC_READY, DC, CF] : noexit := (* this process controls the position of the crane *) P9a [A9, DC_READY, DC, CF] |[CRANE_STOP_H]| P9b [G9, CRANE_STOP_H] (1 of TWO_STATE) where process P9a [A9, DC_READY, DC, CF] : noexit := CRANE_TO_BELT2; CRANE_STOP_H; DC_READY; DC; CRANE_TO_BELT1; CRANE_STOP_H; CF; P9a [A9, DC_READY, DC, CF] endproc process P9b [G9, CRANE_STOP_H] (STATE:TWO_STATE) : noexit := G9 ?VALUE:CRANE_POSITION; (* initial value is OTHER *) if LIMIT_CRANE_POSITION (STATE, VALUE) then CRANE_STOP_H; P9b [G9, CRANE_STOP_H] (SUCC (STATE)) else P9b [G9, CRANE_STOP_H] (STATE) endif endproc endproc (* ------------------------------------------------------------------------- *) process P10 [G10, A10, DC_READY, DC, CF] : noexit := (* this process controls the height of the crane *) P10a [A10, DC_READY, DC, CF] |[CRANE_STOP_V]| P10b [G10, CRANE_STOP_V] (1 of TWO_STATE) where process P10a [A10, DC_READY, DC, CF] : noexit := DC_READY; CRANE_LOWER; CRANE_STOP_V; DC; CRANE_LIFT; CRANE_STOP_V; CF; P10a [A10, DC_READY, DC, CF] endproc process P10b [G10, CRANE_STOP_V] (STATE:TWO_STATE) : noexit := G10 ?VALUE:CRANE_HEIGHT; if LIMIT_CRANE_HEIGHT (STATE, VALUE) then CRANE_STOP_V; P10b [G10, CRANE_STOP_V] (SUCC (STATE)) else P10b [G10, CRANE_STOP_V] (STATE) endif endproc endproc (* ------------------------------------------------------------------------- *) process P11 [A11, DC, CF] : noexit := (* this process controls the magnet of the crane *) DC; CRANE_MAG_ON; CF; CRANE_MAG_OFF; P11 [A11, DC, CF] endproc (* ------------------------------------------------------------------------- *) process P12 [G12, A12, FT_READY, FT, CF, BLANK_ADD] : noexit := (* this process controls belt 1 and adds the five blanks *) BLANK_ADD; BLANK_ADD; BLANK_ADD; BLANK_ADD; BLANK_ADD; stop |[BLANK_ADD]| ( BLANK_ADD; BELT1_START; P12a [A12, FT_READY, FT, CF, BLANK_ADD] ) |[BELT1_STOP, FT]| P12b [G12, BELT1_STOP, FT] (false) where process P12a [A12, FT_READY, FT, CF, BLANK_ADD] : noexit := BELT1_STOP; FT_READY; BELT1_START; FT; ( CF; P12a [A12, FT_READY, FT, CF, BLANK_ADD] [] BLANK_ADD; P12a [A12, FT_READY, FT, CF, BLANK_ADD] ) endproc process P12b [G12, BELT1_STOP, FT] (PREVIOUS_S13:BOOL) : noexit := G12 ?S13:BOOL; ( [PREVIOUS_S13 = S13] -> P12b [G12, BELT1_STOP, FT] (PREVIOUS_S13) [] [not (PREVIOUS_S13) and S13] -> BELT1_STOP; P12b [G12, BELT1_STOP, FT] (S13) [] [PREVIOUS_S13 and not (S13)] -> FT; P12b [G12, BELT1_STOP, FT] (S13) ) endproc endproc (* ------------------------------------------------------------------------- *) process P13 [G13, A13, A2D, DC] : noexit := (* this process controls belt 2 *) ( A2D; P13a [A13, A2D, DC] ) |[BELT2_STOP]| P13b [G13, BELT2_STOP] (false) where process P13a [A13, A2D, DC] : noexit := BELT2_START; BELT2_STOP; ( DC; A2D; P13a [A13, A2D, DC] [] A2D; DC; P13a [A13, A2D, DC] ) endproc process P13b [G13, BELT2_STOP] (PREVIOUS_S14:BOOL) : noexit := G13 ?S14:BOOL; ( [not (PREVIOUS_S14) or S14] -> P13b [G13, BELT2_STOP] (S14) [] [PREVIOUS_S14 and not (S14)] -> BELT2_STOP; P13b [G13, BELT2_STOP] (S14) ) endproc endproc (* ------------------------------------------------------------------------- *) endspec