Skip to main content

Spin

Spin verifies the Promela translation of a case. It computes with 32-bit integers and havocs an integer only among candidate values, so it is under-approximating: a trace it finds is trusted, a proof is not, and a Spin portfolio reports a proof as Inconclusive. It needs spin and gcc on PATH, since Spin compiles every search with gcc. It treats a @Clock variable as an ordinary variable. Before it runs, it reports a case Not supported when the case holds a construct listed below, naming each construct, or the variable it concerns, and its source line.

What the backend refuses​

  • Variables of type real, string or any: Promela has integer, boolean and mtype variables only.
  • For-operations: the Promela translation has no loop.
  • Real literals: Promela has no real numbers.
  • String literals: Promela has no strings.
  • Array literals: the backend receives arrays split into one variable per slot and has no form for an array value.
  • Array indexing: the backend receives arrays split into one variable per slot and has no form for indexing.
  • Non-boolean if-then-else inside a property: an LTL formula has no conditional expression, and only a boolean one can be rewritten into logic.
  • Unbounded integer variables: Spin computes with 32-bit integers that wrap without notice, so a value beyond them would make a trace wrong; the property depends on a variable without a static bound, such as a counter without a guard like if (counter < 10) { counter := counter + 1 }.
  • Integer variables beyond the 32-bit range: Spin computes with 32-bit integers that wrap without notice, so a value beyond them would make a trace wrong; the property depends on a variable whose static bound exceeds them.
  • Arithmetic that may leave the 32-bit range: Spin computes with 32-bit integers that wrap without notice, so a value beyond them would make a trace wrong; the property depends on the arithmetic.