|
We designed a specification
of an 8-floor lift. Two modules are defined: One representing a door at floor i,
and one for the cabin. The main module puts all the pieces together, by defining 8 "doors"
(door0 to door7) and one cabin.
Under the fairness assumption that the lift will go up or down infinitely often, we proved the (untimed) property that any request is eventually granted, as well as several other safety properties. However, we saw that the number of transitions between a request and a grant is not bounded, since someone could open and close the door infinitely at some floor. With TSMV, we were able to count only the cabin's moves, and got the result that the maximum waiting "time" is 8 cabin's moves when calling the cabin at floor 4. The maximum waiting time is only 10 cabin's moves when calling the lift at floor 2 (since the cabin could be just leaving floor 2 when it is called, go up to floor 7, and come back).
|