When a user repeatedly checks a model, the current model should indicate a trend for the state space statistics compared to the previous run (snapshot). I.e. has the number of distinct states gone up, down, or remained the same...

I have issue with model explamation lime() try demo in lime/demo/text_classification_explanation.R it game me error:

`results <- lime(sentences_to_explain, bst, get.features.matrix, keep_word_position = false)(cases = sentences_to_explain, n_labels = 1, n_features = 5)

Error in eval(lhs, parent, parent) : attempt to apply non-function
`
Can you please suggest? Thanks.

Having #45 closed, we should update the Apalache manual. Perhaps we should add a new section on integration with TLA Toolbox and explain how one gets an Apalache counterexample imported in the toolbox.

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

We want to auto-generate a website that documents all the supported patterns of ReqAnalyzer and their countertrace formulas.

It would be even better if we would generate pictures of automata and/or timing diagrams.

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

We should mark clauses with information about the corresponding assertion in code (say, NullPointerException in line X), and then generate output like "Could not verify absence of NullPointerException in line X".

With the framework for labelling clauses that Teme introduced, that should be fairly simple?

More documentation about the input format / syntax is needed.

Ideally, this should be auto-generated from https://github.com/jrclogic/SMCDEL/blob/master/src/SMCDEL/Internal/Parse.y and https://github.com/jrclogic/SMCDEL/blob/master/src/SMCDEL/Internal/Lex.x.

@danielbyler can you take a look here and possibly set us up for this? It's the automated documentation that you see across projects. We should also configure the webhook into our project so that the docs continuously update as changes are made.

A quick rundown of current issues that hinder productive use of ModelPolisher:

• There was a logic error when using AnnotateDB: a check in one place was inverted and ADB was used when it should not have been and vice versa. This should be fixed in master after pulling in changes from the refactoring branch today
• Both COBRAparser and JSONParser currently error on some models from bigg_models da