CommunityModules icon indicating copy to clipboard operation
CommunityModules copied to clipboard

annotate operators with the @supportedBy tag

Open konnov opened this issue 3 years ago • 1 comments

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.

konnov avatar Apr 01 '22 12:04 konnov

@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").

lemmy avatar Apr 01 '22 16:04 lemmy