This example illustrates how TSMV is efficient at dealing with long durations. The problemThe bridge-crossing problem is a famous mathematical puzzle with time critical aspects [Rot02]. A group of four persons, called P1, P2, P3 and P4, have to cross a bridge at night. It is dark and they can only cross the bridge if they carry a lamp. Only one lamp is available and at most two persons can cross at the same time. Therefore any solution requires that, after the first two persons cross the bridge, one of them returns, bringing back the lamp with him for the remaining people. The four persons have different maximal speeds: here P1 crosses in 5 time units (t.u.), P2 in 10 t.u., P3 in 20 t.u. and P4 in 25 t.u. When a pair crosses the bridge, they move at the speed of the slowest person in the pair. Now, how much time is required before the whole group is on the other side? A person is described as an SMV module with his crossing time as a parameter. His possible steps are to stay where he is, or move to the other side. He can only cross when the lamp is on his side (and then the lamp crosses with him). When he crosses, the transition takes at least his crossing time. This way, when four persons are synchronized, the crossing time is any integer greater or equal to the maximum crossing time of the crossing persons. The complete system is obtained by combining four persons (four instances of the same person module, with different crossing times) with a Boolean lamp value keeping track of the position of the lamp, and adding a further constraint (an INVAR in SMV) telling that at most two persons cross in one move. The system is further labeled with two propositions: initial for the initial configuration, and safe for the configurations where everyone is on the other side of the bridge. We can ask how much time is required for crossing: COMPUTE MIN[initial, safe]The answer (60 t.u.) is obtained in a few milliseconds. The bridge example readily gives rise to many variants with more than four persons, with different crossing times, and where a larger number of persons can cross in the same step. We ask SPEC AG EF<=60 safeand get a negative answer: in some reachable configurations, more than 60 t.u. are required. Indeed, if we start after just one person has crossed, that person will have to come back before we can implement the 60 t.u. solution. Hence 85 t.u. (=25+60) are sometimes required. We check that this is indeed the worst case with SPEC (AG EF<=85 safe) & !(AG EF<=84 safe)
Comparison with NuSMVThe same example can be treated with NuSMV. This is easy since the example does not use zero-length steps. For long steps, we use the method advocated in [CC01] and introduce a counter forcing several t.u. between actual system moves. It can be argued that this model is slightly more cumbersome.The answer 60 t.u. for COMPUTE MIN[initial, safe] is obtained a little less quickly than with TSMV (see table below). When verifying SPEC (AG EF<=85 safe) & !(AG EF<=84 safe) we obtain a negative answer! This is because the models are different. In fact, the NuSMV encoding describes a different TKS, where all intermediate positions exists along what should be long steps. The AG modality quantifies over these intermediate positions too. The intended semantics can be recovered by adapting the TCTL formula. The new formula relies on a new inbetween proposition that has to be added: it labels the intermediate configurations that should not exist in the TKS. The resulting formula SPEC AG (!inbetween -> EBF 0..85 (safe & !inbetween))is satisfied.
TSMV and sensitivity to scaling up the durationsThe bridge problem is an example of a system where durations are mostly ``long'' (greater than 1). The algorithms used in TSMV are designed in such a way that only useful durations are considered [MS03] (we were influenced by the complexity analysis in [LMS02]). As a result, TSMV is mostly insensitive to scaling up the durations. Assume that we define a model ``bridge x 10'' by replacing 5, 10, 20 and 25 with (resp.) 50, 100, 200, and 250, TSMV computes the minimum delay of 600 t.u. in more or less the same time it needed for the initial problemThis must be contrasted with nuSMV behavior. When we scale up the durations, the computation time increases dramatically. In fact, there is no way to avoid this: nuSMV does not know about TKS's and is bound to compute all sets associated with different values of the counter for intermediate states. Computing these sets is a tedious and mostly repetitive task that cannot be avoided unless a notion of TKS is introduced. The following table shows how running time and memory requirements (for the COMPUTE MIN statement only) grow when we scale up the timing parameters of the bridge problem of TSMV. Observe that the TKS defined with bridge x 10 is not exactly a scaling up of bridge since we use conditions of the form ``duration >= 100'' that allow all values 100, 101, 102, ...
In order to be really closer to a scale up of the initial model, we can specify that the time step can be the gcd of all crossing times (for instance, in "bridge x 20", crossing times are 100, 200, 400 and 500, and their gcd is 100). In the case of NuSMV, when using timing requirements, we must then multiply the result by the gcd of all crossing times in order to find the real result. We then get the following time and memory usage when computing the minimum total crossing time:
Download model files
Bibliography
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||