MPS Model Checker for External JAR Files

Technical Problem:

Your MPS-based application imports various Functionalities from external JAR files, the functionality of which is no longer guaranteed after importing into MPS? 

A validation of the "MPS-Solution"in your imported JAR file can be made sure with a “Right Click/Check Solution" and it does not find any problems or errors? 


In order to explain this, one must understand that MPS does not, by default, perform any checking of such "Stub-Models" (Java stubs of imported JAR files). 

You must first activate the checking of these stub models in the "Settings" under "Tools / Model Checker" ("Check stub models" checkbox) and configure the required "Model checking level". 

In the Model Checker you will now find the actual view of the inconsistencies found, as well as errors and warnings, when this configuration setting has been changed when a test is carried out again using "Check Solution": 

A detailed debugging of the correctness and completeness of the imported JAR files is now possible without any problems. 

MPS-Error: ASMClassType (classifier is out of search scope)