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
    ...
endif
  • Bad states reachability: 
    if (isEmpty(reach && region_expression)) then
    ...
endif
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.