Search code examples
logicautomatanusmv

NuSMV getting stuck at a trivial deadlock

Suppose I code a model in NuSMV that starts in state S1. I want to check the condition in this model checker whether I eventually reach state S70 in all circumstances. Now visualize the NuSMV model that i coded as below:

enter image description here

From above it is obvious that eventually S70 will be reached but it may take much more than 70 time steps. Why? Because you may go to S2 then S3 then instead of progressing to S4 again back to S2 and this pattern repeats, say 100 times. Such possibilities are taken into account by NuSMV software also to confirm that S70 will definitely be reached.

The problem is that NuSMV said that S70 won't be reached and generated a counterexample which is precisely this:-

S1->S2->S3->S2

So the counter-example is just these 4 steps. But I am amazed that NuSMV cannot figure out that this deadlock will eventually get resolved over time. Why am I getting a non-intuitive result?

There may be a chance that the automata that I show in the figure is what I want my NuSMV code to represent but I coded one or two lines wrongly but I don't think so. Otherwise how come NuSMV could figure that it can go from S2 to S3. If it can figure that one can go from S2 to S3 then why terminate the counterexample above at S2?

Can someone explain?

Solution

  • But I am amazed that NuSMV cannot figure out that this deadlock will eventually get resolved over time

    I am not sure this situation corresponds to the definition of "deadlock". Anyway, NuSMV is correct in pointing out that there exists an execution in which the program will never reach state S70.

    A counter-example for a reachability problem (in a proper model without deadlock states) is always an infinite execution trace. The counter-example you get:

    S1->S2->S3->S2

    is composed by two parts:

    • a prefix part: the sequence of states, starting from the initial state, which reaches the infinite loop part. In this case, it is just S1.
    • a loop part: a self-looping sequence of state, which is easily identifiable because it ends with the same state it starts. In this case, it is S2 -> S3 -> S2

    This is a valid infinite execution path of your automaton, meaning that it is legitimate for the program to always jump from S3 to S2 and never go to S4, and since it never touches S70 it is also a counter-example for your property.

    I am not sure how I can further assist you in your problem, as you did not indicate whether you are using LTL or CTL, nor did you give any further information about your model. It might be necessary to change your model, your properties or both. If I may, I would advice you to take a look at the slides in the second part of this course on NuSMV/nuXmv to get a better understanding of the tool.

    EDIT

    Let's suppose that in the real world scenario that is being modeled it is technically impossible for such an infinite execution to ever occur, i.e. such possibility is the result of some simplifications introduced by the modeling phase, or that such a situation might actually occur but we are simply not interested in such extreme case for documented reasons.

    Then, the solution is to exclude such execution trace from the verification part, so that it cannot appear as a counter-example. The exact solution may depend on the model being verified, which it is not available to me, but an example could be:

     (! (G (F S2))) -> (F S70)

    This encoding assumes that there exists no loop-back going to S2 after S70. Otherwise, other approaches should be used.