Can we have terminal states in NuSMV?

Is it possible to have a state in NuSMV that does not have transitions to any other states? For example is it valid that in my code l3 does not have any transitions? When I run this NuSMV gives me the error that "case conditions are not exhaustive". Thanks!

MODULE main

VAR

location: {l1,l2,l3};


ASSIGN

init(location):=l1;

next(location):= case
             (location = l1): l2;
             (location = l2): l1;
             (location = l2): l3;
             esac;

Solution

By construction, in the so-called assignment-style [used in your model]:

there is always at least one initial state
all states have at least one next state
non-determinism is apparent

Alternatively, one can use the so-called constraint-style, which allows for:

inconsistent INIT constraints, which result in no initial state
inconsistent TRANS constraints, which result in deadlock states (i.e. a state without any outgoing transition to some next state)
non-determinism is hidden

For more info, see the second part of this course, which applies also to NuSMV for the most part.

An example of a FSM wherein some state has no future state is:

MODULE main
VAR b : boolean;
TRANS b -> FALSE;

The state in which b is true has no future state. Conversely, the state in which b is false can loop in itself or go to the state in which b = true.

You can use the command check_fsm to detect deadlock states.

Please note that the presence of deadlock states can hinder the correctness of model checking in some situations. For instance:

FAQ #007: CTL specification with top level existential path quantifier is wrongly reported as being violated. For example, for the model below both specifications are reported to be false though one is just the negation of the other! I know such problems can arise with deadlock states, but running it with -ctt says that everything is fine.
MODULE main
VAR b : boolean;
TRANS next(b) = b;
CTLSPEC EF b
CTLSPEC !(EF b)

For other critical consequences of deadlock states in the transition relation, see this page.

Usually, when NuSMV says that "the case conditions are not exhaustive" one adds a default action with a TRUE condition at the end of the case construct, which is triggered when none of the previous conditions applies. The most common choice for the default action is a self-loop, which is encoded as follows:

MODULE main
VAR
  location: {l1,l2,l3};
ASSIGN
  init(location):= l1;
  next(location):=
    case
      (location = l1): l2;
      (location = l2): {l1, l3};
      TRUE           : location;
    esac;

NOTE: please notice that if there are multiple conditions with the same guard, only the first of these conditions is ever used. For this reason, when in your model location = l2 then the next value of location can only be l1 and never l3. To fix this, and have some non-deterministic choice among l1 and l3, one must list all possible future values under the same condition as a set of values (i.e. {l1, l3}).