model-checking

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

Requested feature: Create an attribute that allow users to mark their proof harness functions.
Use case: The same way users can tag their test functions using the #[test] attribute, users should be able to tag their proof harness with an attribute such as #[proof]

Sparsepp triggers a warning:

/Users/tim/storm/build-debug/include/resources/3rdparty/sparsepp/sparsepp/spp.h:942:33: warning: definition of implicit copy constructor for 'Two_d_destructive_iterator<std::__1::pair<const DdNode *const, bool>, spp::sparsegroup<std::__1::pair<const DdNode *const, bool>, spp::libc_allocator<std::__1::pair<const DdNode *const, bool>>> *, std::__1::pair<const DdNod