formal-methods

https://github.com/project-oak/oak/blob/4f2063aea9fc8afa123617d1bf9e518b58469562/oak_functions/examples/weather_lookup/module/src/tests.rs#L196

I think we should avoid using "real" randomness in tests, and especially in benchmarks, which are expected to converge. So perhaps we should consider a fixed-seed RNG (see https://docs.rs/rand/0.8.4/rand/trait.SeedableRng.html#tymethod.from_seed ).

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