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.

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.