Unreachable Default

Definition:

  • An alt statement contains an else branch while a default is active. The else branch of an alt statement is taken if no other branch is applicable. If a default is active at the same time, its branches come after all branches of the alt statement. Hence the default altstep can never be executed if an else branch is present.

Code Example:

testcase myTestcase() runs on MyComponent {
  var default myDefaultVar := activate(myAltstep(t))
  alt {
    [] p.receive(charstring:("foo1")) {
      p.send("ack")
    }
    [] p.receive(charstring:("bar1")) {
      p.send("nack")
    }
    [else] {
      setverdict(fail)
      log("unexpected behavior")
    }
  }
  deactivate(myDefaultVar)
}

References:

Quality attributes

  • - Code Example

  • - Cause and Effect

  • - Frequency

  • - Refactoring