The TlaDocumentSymbolsProvider stumbles on operators while parsing constants and doesn't report them as model symbols. As a result, const operator names don't appear in the outline panel and in completion suggestions. Such operators also prevent parsing of the following constants.
A simple case:
CONSTANT Foo(_), Bar
Neither Foo nor Bar makes it to the model symbols list
Checking nondeterministic models under an arbitrary scheduler allows us to use the (faster) algorithms for DTMCs/CTMCs. This might be useful, e.g., when the nondeterminism is known to be spurious.
In some sense, this would be the reverse operation of --transformation:to-nondet.
Note that for MAs it might be necessary to also invoke --[transformation:]eliminate-chains to get a CTMC (this
The
TlaDocumentSymbolsProviderstumbles on operators while parsing constants and doesn't report them as model symbols. As a result, const operator names don't appear in the outline panel and in completion suggestions. Such operators also prevent parsing of the following constants.A simple case:
CONSTANT Foo(_), BarNeither
FoonorBarmakes it to the model symbols list