Technische Problemstellung:

Ihre MPS-basierte Applikation importiert diverse Funktionalitäten aus externen JAR-Dateien, deren Funktionsfähigkeit nach dem Import in MPS jedoch nicht mehr sichergestellt ist?

Eine Überprüfung der "MPS-Solution" Ihrer importierten JAR-Datei mittels "Rechtsklick / Check Solution" findet jedoch auch keinerlei Probleme oder Fehler?

Problemlösung:

Um diesen Sachverhalt zu erklären, muss man verstehen, dass MPS defaultmäßig keinerlei Überprüfung solcher "Stub-Modelle" (Java-Stubs importierter JAR-Dateien) durchführt.

Sie müssen zuvor in den "Settings" unter "Tools / Model Checker" die Prüfung dieser Stub-Modelle aktivieren (Checkbox "Check stub models") sowie den benötigten "Model checking level" konfigurieren.

Im Model Checker finden Sie nun nach Änderung dieser Konfigurationseinstellung bei erneuter Durchführung einer Prüfung mittels "Check Solution" die eigentliche Ansicht der gefundenen Inkonstistenzen sowie Fehlern und Warnings:

Ein ausführliches Debugging der Korrektheit bzw. Vollständigkeit der importierten JAR-Dateien ist nun problemlos möglich.