CommunityModules
CommunityModules copied to clipboard
annotate operators with the @supportedBy tag
This PR introduces the annotation @supportedBy("TLC") or @supportedBy("TLC,Apalache") in front of all operators, to document which operators are supported only by TLC and which operators are supported by TLC and Apalache.
@muenchnerkindl Would it be useful to include TLAPS in the @supportedBy annotation? For example, annotate operators for which we have lemmas? We could revert @supportedBy into @unsupportedBy to make it less noisy. If a complete module is unsupported by a tool (e.g. IOUtils, CSV, ...), an ASSUME could be used that evaluates to FALSE with that tool: ASSUME IsTool("Apalache").