Is there any way to make a timeout diagnostic “legitimate”? Hide it if certain conditions are met? Note the end states are valid. Like this one:

$ spin -c ./_timeout.promela
proc 0 = :init:
proc 1 = region_r19
proc 2 = region_r36
      timeout
-------------
final state:
-------------
#processes: 3
                queue 1 (_channels[0]):
                queue 2 (_channels[1]):
  2:    proc  2 (region_r36:1) ./_timeout.promela:32 (state 1) <valid end state>
  2:    proc  1 (region_r19:1) ./_timeout.promela:19 (state 1) <valid end state>
  2:    proc  0 (:init::1) ./_timeout.promela:44 (state 4) <valid end state>
3 processes created

Background info: I am trying to model a state machine. Some of the states are valid as shown (waiting for some event). I still get a timeout diagnostic and I am afraid this will foil the verification step (I am not there yet with the coding).

The code for the above:

#define idx_region_r19 0
#define idx_region_r36 1

mtype = { event_StateChange, }

typedef event {mtype evId; short fromState; short toState};

chan _channels[2] = [1] of {event};


proctype region_r19()
{
    local short myIdx = idx_region_r19;
    local event evtRecv;

loop_r19:
end_r19:
    _channels[myIdx]?evtRecv;

    goto loop_r19;
} // region_r19


proctype region_r36()
{
    local short myIdx = idx_region_r36;
    local event evtRecv;

loop_r36:
end_r36:
    _channels[myIdx]?evtRecv;

    goto loop_r36;
} // region_r36



init {
    atomic {
        run region_r19();
        run region_r36();
    }
}