Update tntc manual with run and test
#342
Conversation
| tntc typecheck [--out=<out>.json] <spec>.tnt | ||
| ``` | ||
|
|
||
| This command infers types in the TNT specification, which is provided in the |
There was a problem hiding this comment.
Currently the typecheck command also infers effects. I think it makes sense to have type and effect checking at the same command, but I couldn't think of a good name for it, so I just kept typecheck until we get to review it, which I think it's right now. Any ideas on how to improve this? @konnov @shonfeder
There was a problem hiding this comment.
I would keep it typecheck. At some point, we were even thinking of integrating effects in the type system. So from the user's perspective, this distinction between types and effects is probably too fine-grained. We should probably even replace parse and typecheck with something like compile, so all stages are done at once and the output is saved in a file. Then we can introduce options to skip some of the stages. This is what compilers normally do. Even Python is producing a bytecode file.
There was a problem hiding this comment.
Factored out into a separate issue: #359
|
|
||
| *This command is not implemented yet.* | ||
|
|
||
| ```sh | ||
| tntc exec [--seed=<seed>] [--length=<len>] \ | ||
| [--timeout=sec] [--check=prop] [--out=<out>.json] <spec>.tnt | ||
| tntc run [--seed=<seed>] [--timeout=sec] [--out=<out>.json] <spec>.tnt <name> |
There was a problem hiding this comment.
What about calling these runnable definitions tasks? Ruby has something like this with rakes, where makefile-like tasks are defined in ruby instead of a new/different language. We could use the qualifier task for the runnable definitions in TNT syntax.
| tntc run [--seed=<seed>] [--timeout=sec] [--out=<out>.json] <spec>.tnt <name> | |
| tntc run [--seed=<seed>] [--timeout=sec] [--out=<out>.json] <spec>.tnt <task> |
There was a problem hiding this comment.
After the standup discussion, I realize runs are actually a different thing than tasks. I believe we should have the essential definition of the command with the run (i.e. the length parameter), and leave only low-level configs to the task (that is, things that are not relevant to a person reading the specification).
Elaborating a bit on the tasks: I already had some thoughts on this when planning the VSCode plugin (see this discussion entry). I believe we should have a format to define the commands for TNT that can:
- Be automatically identified as VSCode tasks as I suggested in the discussion
- Be run with something like
tntc taskfor all tasks ortntc task <group>for specific groups (i.e. heavy checks, sanity checks, unit tests). - Be used in CI. For instance,
npmcommands/scrips are used in CI instead of calling executables such asmochadirectly. TNT should mimic this by having a very simple standard CI config that callstntc task test, as opposed to specifying apalache commands and flags in the CI file.
There was a problem hiding this comment.
Great idea! Here is a follow-up issue on that: #360
| ``` | ||
|
|
||
| This command produces a random execution of a TNT specification, | ||
| whose name is given with `<spec>.tnt`. | ||
| whose name is given with `<spec>.tnt`. The random execution should follow | ||
| the run structure that is given in the definition called `<name>`. |
There was a problem hiding this comment.
| the run structure that is given in the definition called `<name>`. | |
| the run structure that is given in the task definition called `<task>`. |
This PR introduces two future commands in the
tntcmanual:runto perform a randomized execution of a TNT spec, andtestto run unit tests in a TNT spec.