Skip to main content

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.

What the backend refuses​

  • Variables of type real, string or any: the SMV translation declares integer, boolean and enumeration variables only.
  • For-operations: the SMV translation has no loop.
  • String literals: SMV 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.
  • Integer variables, in the bdd-invar configuration only: the translation declares every integer unbounded, and the BDD engine cannot build its state machine over unbounded integers.