The example we use in PRTS module is a multi-lift system. The motivation is an
interesting phenomena: sometimes a user has requested a service in multi-lift
system, but a lift traveling in the same direction passes by that user and the
user must wait for another lift to serve it. This is actually because the
request assignment algorithm in the system and some other unpredictable
reasons such as a lift could be occupied arbitrary time because of other
users. We use PAT to model this complicated system which combines concurrency,
real-time and probability, and 2 methods of assigning the requests are
modeled: one is choosing the nearest lift and the other is choosing an
arbitrary one.

Because of the complexity of this system, now PAT could just handle 2 lifts,
otherwise there will be state explosion. But we could still get some
reasonable results from this table. Firstly, the more users are there, the
higher probability that some users will be passed by. Secondly, if we use
nearest lift assignment, we could expect a smaller probability that such bad
behavior could happen, which could be found in Lift_223_nearest and
Lift_223_random cases. There are many optimization could be implemented in
PAT, so we can expect better and better performance in this module. The experiment data is available here.