Dear Zheng Tan,
Sorry for the late reply.
Note that the traffic light controller has a particularity: the timer is
not guaranteed to advance. It stays in START for a
(nondeterministically chosen) while before advancing, but it may also
stay in START forever. Obviously, we don't want a timer that is stuck
in its START STATE!
To remedy this, we use a "fairness constraint". If you read in a
fairness constraint, you restrict the model checker to only look at
paths on which the constraint is true infinitely often. The constraint
that we read here is !(timer.state=START), which asserts that we are not
interested in paths on which from some point on the timer is stuck in
the start state. Reading in a fairness constraint is done with the
read_fairness command.
The reason things are done this way is not just because now we can use a
timer with very little state. The main reason is that now the timer can
decide when it switches from START to SHORT. Hence, we are really doing
a model check for timers of any length, and not just for a timer of a
specific length. If we now implement a timer that always goes from
START to SHORT in, say, 10 ticks, we know that the model is correct,
because that is just one bahavior of the nondeterministic timer that we
have in tlc. The only "timer" that would be wrong is the one that
always stays in the START state, and we excluded that.
Hope that helps.
Roderick.
Zheng Tan wrote:
>
> Hi,
>
> In VIS user's Manual (page33) 4.5.2 (Debugging for Model Checking) mention a traffic light
> model_check debugging example. I am not quite understand how they revise the program
> according to the an error debug trace. ( There are two properties fail during model
> checking.)
> The situation is "the timer is stuck in its initial state, by forcing the timer to progress
> in finite time to the next state". How they do this to guarantee the correctness of next
> model checking. Thanks,
>
> Zheng Tan
This archive was generated by hypermail 2b29 : Thu Mar 01 2001 - 11:39:16 MST