Skip to main content

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.

What the backend refuses​

  • Variables of type real, string or any: XSTS has integer, boolean and enumeration variables only.
  • Real literals: XSTS has no real numbers.
  • String literals: XSTS has no strings.
  • Array literals: the backend receives arrays split into one variable per slot and has no form for an array value.
  • For-operations over anything but a range: an XSTS loop runs over an integer range.