Supported Constructions

Translator supports the whole model declaration syntax (wrt. FAST manual) and partially supports strategy implementation:
  • Set of reachable states post* (not pre*):
    Region reach := post*(region, transitions);
  • Good property specification:
    if (subSet(reach, region_expression)) then
  • Bad states reachability:
    if (isEmpty(reach && region_expression)) then
See for README file for a little more.

Unsupported Expressions

  • Quantifiers exists and forall.
  • Conditioned definition of a region definition:
    if (cond) then Region r := definition; endif
  • Any operations over pre*/post* sets, except supported.