Specification of a job shop scheduling simulation model and some properties of its internal transition function

We specify a job shop scheduling system according to DEVS formalism introduced by Zeigler. Our specification defines a set of state variables and an internal transition function that moves the system from state to state at event times. Some properties of the internal transition function are presented.