model checking support

[coolya]

Implements #21 and is based on #25 hence #25 needs to be merged first.

This pull request adds support to run the model checker directly from gradle on a project or subset of models from a project. It's configuration is closely aligned with the generator from command line part that we already have in the project.

In general the gradle part is not much different, a simple plugin with extensions for configuration and the a command line backend that does the real work. Some of the decisions why to use certain classes are documented in the code directly but my main goal was to stay away from anything the uses the ModelCheckerSetting from MPS to avoid any interferences with the settings of the user.

Currently there is no way to configure which checks are executed and how the errors are reported. Everything is sent to log4j. In theory users could use the log.xml file in the MPS installation to customise the logging. Users could also use log4j configuration via properties of env variables to redirect the log out put somewhere else.

Customisation can be done by changing properties of the checkmodels task which is a JavaExec task.

Future Work

• Integrate with testing infrastructure (Report model checking results as tests #30)
• Better usage documentation with advanced examples

[arimer]

Is there a way how I can run the modelcheck test? After deploying the modelchecker locally with modelcheck:publishPluginMavenPublicationToMavenLocal I'll get an artifact with the version: modelcheck-2018.2.5.2-SNAPSHOT.

However, the build.gradle file for the /test/modelcheck project tries to use a modelcheck plugin with the following version:
id("modelcheck") version "1.0-SNAPSHOT" which it obviously can't find under the local repos.

Am I doing something wrong, or do we need to adapt the required migrationcheck version in the /test/modelcheck project?

[coolya]

It looks like you are confusing the version of the modelcheck artefact that used at runtime with the plugin version. The modelcheck artefact is only used at execution time of the headless MPS. It is not used in the build script execution. The version of plugin always matches the version of the mps-gradle-plugin artefact while the runtime artefact is specific to a MPS version.

The version of the plugin is calculated here: https://github.com/mbeddr/mps-gradle-plugin/pull/31/files#diff-392475fdf2bc320d17762ed97109a121R23

The decision about which runtime artefact should be used is taken here: https://github.com/mbeddr/mps-gradle-plugin/pull/31/files#diff-6a674476dac875501fa72a159331f169R31

And is based on the actual MPS dependency version. This way we can support different MPS specific implementations.

I guess the problem you are having is something different and is caused by the fact that #25 is bumping the version from 1.0 to 1.1.

[sergej-koscejev]

I can't say much about the rest of the code, it looks fine and I assume it's working :)

EDIT: ok I was wrong to assume it's working. I can't run it:

Unable to find a gradle build file named build.gradle.
Using gradle at '/Users/sergej/Projects/mps-gradle-plugin/test/modelcheck/gradlew' to run buildfile '':

> Task :checkmodels FAILED

FAILURE: Build failed with an exception.

* What went wrong:
Execution failed for task ':checkmodels'.
> Could not resolve all files for configuration ':detachedConfiguration1'.
   > Could not find any version that matches de.itemis.mps:modelcheck:2018.2.4+.
     Versions that do not match:
       - 2018.2.5.2-SNAPSHOT
       - maven-metadata-local.xml
     Searched in the following locations:
       - https://projects.itemis.de/nexus/content/repositories/mbeddr/de/itemis/mps/modelcheck/maven-metadata.xml
       - https://projects.itemis.de/nexus/content/repositories/mbeddr/de/itemis/mps/modelcheck/
       - file:/Users/sergej/.m2/repository/de/itemis/mps/modelcheck/maven-metadata.xml
       - file:/Users/sergej/.m2/repository/de/itemis/mps/modelcheck/
       - https://repo.maven.apache.org/maven2/de/itemis/mps/modelcheck/maven-metadata.xml
       - https://repo.maven.apache.org/maven2/de/itemis/mps/modelcheck/
     Required by:
         project :

* Try:
Run with --stacktrace option to get the stack trace. Run with --info or --debug option to get more log output. Run with --scan to get full insights.

* Get more help at https://help.gradle.org

BUILD FAILED in 13s
2 actionable tasks: 2 executed

[sergej-koscejev]

Doesn't work - see my previous review comment