Using TTM's

The complete model will be composed of the following TTM's: , the TTM for the robot, and , (i=1,2,3), the TTM's for Machines 1, 2, and 3, respectively. The state machines are exactly as they were in the R&W model. We now present each of the TTM's below.

TTM for Robot:

  
Figure 19: TTM for Robot in 3-Machine Example

TTM for Machine 1:

  
Figure 20: TTMs for M1 and M2 in 3-Machine Example

TTM for Machine 2:

TTM for Machine 3:

  
Figure 21: TTM for M3 in 3-Machine Example

Then, the composed TTM for the Three-Machine Example is given by:

where:



where i=1,2 and .

with ``shared transitions'' = , , , .
Graphically, this composed TTM model looks just like the Petri Net in the next section (Figure 22), except that the data variables , are represented by the non-safe places , respectively.

Specifications in Temporal Logic

• Safety 1:
  The robot only loads a machine i if machine i is idle (i=1,2).
  
  
• Safety 2:
  The robot does not load machine i unless the capacity of its respective buffer allows for another piece (i=1,2).
  
  
• Mutual Exclusion:
  If the robot is loading one machine, then it is not available to load the other machine.
  
• Priority: Whenever both machines 1 and 2 are available, machine 1 is to be given priority when being loaded by the robot.
  
• Fair Use of Resource:
  The robot is to load machines 1 and 2 alternatively, starting, say, with machine 1.
  
• Different Types for M3:
  Machine 3 is to load itself only with two parts of different color (so the parts must come from different buffers).
  
• Same Types for M3:
  Machine 3 is to load itself with any two parts of the same color (so both parts must come from the same buffer at any one time).
  

The first three specifications above are already satisfied by the TTM model. This can be verified by checking the enabling conditions and transformation functions of the transitions in the composed model. The Priority specification, although a sequential specification, can be enforced by making sure that . All other specifications are also sequential specifications for which we do not have a controller synthesis procedure.