source: vis_dev/vis-2.1/examples/production_cell/prodcell.ctl @ 11

Last change on this file since 11 was 11, checked in by cecile, 13 years ago

Add vis
File size: 5.2 KB
Line 
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#
11AG(!((TC.Crane.HorizontalPos = OverFB) *
12     (TC.CraneCNTR.HorizontalMove = GoLeft)));                            # 1
13AG(!((TC.Crane.HorizontalPos = OverDB) *
14     (TC.CraneCNTR.HorizontalMove = GoRight)));                           # 2
15AG(!((TC.Crane.HorizontalPos = Middle) *
16    (!(TC.Crane.VerticalPos = UpMost))));                                 # 3
17AG(!((TC.Crane.HorizontalPos = OverDB) *
18     (TC.Crane.VerticalPos = FBHight)));                                  # 4
19AG(!(TC.Crane.VerticalPos = UpMost *
20     TC.CraneCNTR.VerticalMove = GoUp));                                  # 5
21AG(!(TC.Crane.VerticalPos = FBHight *
22    TC.CraneCNTR.VerticalMove = GoDown));                                 # 6
23AG(!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
62AG(!(PR.Pr.PressPosition = Mid * AR.Arm.RALoadArm = Extended *
63     AR.Arm.RAAnglePos = OverLoadedPress));                               # 23
64AG(!(PR.Pr.PressPosition = Top * AR.Arm.RAUnLoadArm = Extended *
65     AR.Arm.RAAnglePos = OverUnLoadedPress));                             # 24
66#
67# Correctness of the communication protocol DB -> Crane
68#
69AG(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
Note: See TracBrowser for help on using the repository browser.