Model-Check checker set in MPS and IDEA modes

[tomb50]

I'd like to use model-checker invocation whilst in MPS environment mode.

It seems however that some of the checkers that one would be expected to be standard (typeSystem and nonTypeSystem checkers) are registered with the CheckerRegistry through an EditorCheckerComponent. This is only initialised if MPS is run as an Idea environment.

If running as an MPS environment, these checkers are not registered with the CheckerRegistry and therefore not found by the mode-check goal of this plugin.

Would it be possible to add the ability to include these checkers (either configurable or not) within the set of checkers to be used for the mode-check goal.

I have attached two screenshots that show the state of the CheckerRegistry on both MPS and IDEA env versions of the model-checker goal from the plugin.

I don't want to run in IDEA mode since for me it increases the execution time by quite a lot.