1 | # |
---|
2 | # Specification for the ProductionCell |
---|
3 | # |
---|
4 | # WARNING: All the formulas are included here, but only a few of them are used |
---|
5 | # for the check_script |
---|
6 | # |
---|
7 | # Author: Abelardo Pardo <abel@vlsi.colorado.edu> |
---|
8 | # |
---|
9 | # Limitation of Mobility for the Travelling Crane |
---|
10 | # |
---|
11 | AG(!((TC.Crane.HorizontalPos = OverFB) * |
---|
12 | (TC.CraneCNTR.HorizontalMove = GoLeft))); # 1 |
---|
13 | AG(!((TC.Crane.HorizontalPos = OverDB) * |
---|
14 | (TC.CraneCNTR.HorizontalMove = GoRight))); # 2 |
---|
15 | AG(!((TC.Crane.HorizontalPos = Middle) * |
---|
16 | (!(TC.Crane.VerticalPos = UpMost)))); # 3 |
---|
17 | AG(!((TC.Crane.HorizontalPos = OverDB) * |
---|
18 | (TC.Crane.VerticalPos = FBHight))); # 4 |
---|
19 | AG(!(TC.Crane.VerticalPos = UpMost * |
---|
20 | TC.CraneCNTR.VerticalMove = GoUp)); # 5 |
---|
21 | AG(!(TC.Crane.VerticalPos = FBHight * |
---|
22 | TC.CraneCNTR.VerticalMove = GoDown)); # 6 |
---|
23 | AG(!TC.Crane.HorizontalMove = Stop -> |
---|
24 | TC.CraneCNTR.VerticalPos = UpMost); # 7 |
---|
25 | # |
---|
26 | # Limitation of Mobility of the Rotary Table |
---|
27 | # |
---|
28 | #AG(!(RT.RTable.RTAngle = S * |
---|
29 | # RT.RTableCNTR.RTRotaryMotor = CWise)); # 8 |
---|
30 | #AG(!(RT.RTable.RTAngle = SE * |
---|
31 | # RT.RTableCNTR.RTRotaryMotor = CCWise)); # 9 |
---|
32 | #AG(!(RT.RTable.RTHight = Top * |
---|
33 | # RT.RTableCNTR.RTVerticalMotor = GoUp)); # 10 |
---|
34 | #AG(!(RT.RTable.RTHight = Bot * |
---|
35 | # RT.RTableCNTR.RTVerticalMotor = GoDown)); # 11 |
---|
36 | # |
---|
37 | # Limitation of Mobility of the Rotary Arm |
---|
38 | # |
---|
39 | #AG(!(AR.Arm.RAAnglePos = OverRT * |
---|
40 | # AR.ACNTR.RARotaryMotor = CWise)); # 12 |
---|
41 | #AG(!(AR.Arm.RAAnglePos = OverLoadedPress * |
---|
42 | # AR.ACNTR.RARotaryMotor = CCWise)); # 13 |
---|
43 | #AG(!(AR.Arm.RALoadArm = Retracted * |
---|
44 | # AR.ACNTR.RAExtendLoadArm = Retract)); # 14 |
---|
45 | #AG(!(AR.Arm.RALoadArm = Extended * |
---|
46 | # AR.ACNTR.RAExtendLoadArm = Extend)); # 15 |
---|
47 | #AG(!(AR.Arm.RAUnLoadArm = Retracted * |
---|
48 | # AR.ACNTR.RAExtendUnLoadArm = Retract)); # 16 |
---|
49 | #AG(!(AR.Arm.RAUnLoadArm = Extended * |
---|
50 | # AR.ACNTR.RAExtendUnLoadArm = Extend)); # 17 |
---|
51 | #AG(!((!AR.Arm.RALoadArm = Retracted) * |
---|
52 | # (!AR.Arm.RAUnLoadArm = Retracted))); # 18 |
---|
53 | #AG(!AR.ACNTR.RARotaryMotor = Stop -> |
---|
54 | # (AR.Arm.RALoadArm = Retracted * AR.Arm.RAUnLoadArm = Retracted)); # 19 |
---|
55 | # |
---|
56 | # Limitation of Mobility for the Press |
---|
57 | # |
---|
58 | #AG(!(PR.Pr.PressPosition = Top * PR.PrCNTR.PressMotor = GoUp)); # 20 |
---|
59 | #AG(!(PR.Pr.PressPosition = Bot * PR.PrCNTR.PressMotor = GoDown)); # 21 |
---|
60 | #AG((AR.Arm.RAAnglePos = OverLoadedPress * !AR.Arm.RALoadArm = Retracted) |
---|
61 | # -> PR.Pr.PressPosition = Mid); # 22 |
---|
62 | AG(!(PR.Pr.PressPosition = Mid * AR.Arm.RALoadArm = Extended * |
---|
63 | AR.Arm.RAAnglePos = OverLoadedPress)); # 23 |
---|
64 | AG(!(PR.Pr.PressPosition = Top * AR.Arm.RAUnLoadArm = Extended * |
---|
65 | AR.Arm.RAAnglePos = OverUnLoadedPress)); # 24 |
---|
66 | # |
---|
67 | # Correctness of the communication protocol DB -> Crane |
---|
68 | # |
---|
69 | AG(DB.DBeltCNTR.PieceOutDB = Y -> |
---|
70 | AF(TC.CraneCNTR.PieceGrabbedFromDB = Y)); # 25 |
---|
71 | #AG(DB.DBeltCNTR.PieceOutDB = Y -> |
---|
72 | # A(DB.DBeltCNTR.PieceOutDB = Y U TC.CraneCNTR.PieceGrabbedFromDB = Y)); # 26 |
---|
73 | # |
---|
74 | # Correctness of the communication protocol ARM -> DB |
---|
75 | # |
---|
76 | #AG(DB.DBeltCNTR.DBReady = Y -> AF(AR.ACNTR.PieceOutArm = Y)); # 27 |
---|
77 | #AG(DB.DBeltCNTR.DBReady = Y -> |
---|
78 | # A(DB.DBeltCNTR.DBReady = Y U AR.ACNTR.PieceOutArm = Y)); # 28 |
---|
79 | # |
---|
80 | # Correctness of the communication protocol RT -> Arm |
---|
81 | # |
---|
82 | #AG(RT.RTableCNTR.RTOutReady = Y -> |
---|
83 | # (AF(AR.ACNTR.PieceGrabbedFromRT = Y))); # 29 |
---|
84 | #AG(RT.RTableCNTR.RTOutReady = Y -> |
---|
85 | # A(RT.RTableCNTR.RTOutReady = Y U AR.ACNTR.PieceGrabbedFromRT = Y)); # 30 |
---|
86 | # |
---|
87 | # Correctness of the communication protocol FB -> Crane |
---|
88 | # |
---|
89 | #AG(FB.FBeltCNTR.FBReady = Y -> AF(TC.CraneCNTR.PieceReleasedOnFB = Y)); # 31 |
---|
90 | #AG(FB.FBeltCNTR.FBReady = Y -> |
---|
91 | # A(FB.FBeltCNTR.FBReady = Y U TC.CraneCNTR.PieceReleasedOnFB = Y)); # 32 |
---|
92 | # |
---|
93 | # Correctness of the communication protocol FB -> RT (2358 seconds) |
---|
94 | # |
---|
95 | #AG(FB.FBeltCNTR.PieceOutFB = Y -> |
---|
96 | # AF(RT.RTableCNTR.PieceGrabbedFromFB = Y)); # 33 |
---|
97 | #AG(FB.FBeltCNTR.PieceOutFB = Y -> |
---|
98 | # A(FB.FBeltCNTR.PieceOutFB = Y U RT.RTableCNTR.PieceGrabbedFromFB = Y)); # 34 |
---|
99 | # |
---|
100 | # Correctness of the communication protocol ARM -> LOAD PRESS |
---|
101 | # |
---|
102 | #AG( PR.PrCNTR.PressReadyToBeLoaded = Y -> |
---|
103 | # AF(AR.ACNTR.ArmLoadedPress = Y)); # 35 |
---|
104 | #AG(PR.PrCNTR.PressReadyToBeLoaded = Y -> |
---|
105 | # A(PR.PrCNTR.PressReadyToBeLoaded = Y U AR.ACNTR.ArmLoadedPress = Y)); # 36 |
---|
106 | # |
---|
107 | # Correctness of the communication protocol ARM -> UNLOAD PRESS |
---|
108 | # |
---|
109 | #AG( PR.PrCNTR.PressReadyToBeUnLoaded = Y -> |
---|
110 | # AF(AR.ACNTR.ArmUnLoadedPress = Y)); # 37 |
---|
111 | #AG(PR.PrCNTR.PressReadyToBeUnLoaded = Y -> |
---|
112 | # A(PR.PrCNTR.PressReadyToBeUnLoaded = Y U |
---|
113 | # AR.ACNTR.ArmUnLoadedPress = Y)); # 38 |
---|