Supported ConstructionsTranslator 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
- 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.