Theta
Theta verifies the XSTS translation of a case with unbounded integers, and its verdicts are exact. 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 and its source line.
nuXmv
nuXmv verifies the SMV translation of a case with unbounded integers, and its verdicts are exact; its bdd-invar configuration needs bounded integers. 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 and its source line.
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.
Uppaal
Uppaal verifies the timed-automaton translation of a case and is the only backend that honours @Clock, which the other backends treat as an ordinary variable. It havocs an integer only among candidate values, so its configurations are under-approximating, except over-approximation, which over-approximates the clock zones. It declares every integer with its static bound, or with a 31-bit range when it has none within 32 bits, and stops a run as Not supported, naming the variable, when a value leaves the declared range; a proof over a counter without a guard such as if (counter < 10) { counter := counter + 1 } counts through that whole range and does not finish in practice. 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.