GEAR jETI HowTo

From JETI FMICS Wiki
Jump to: navigation, search

This page describes the integration of the GEAR model checker into the jETI tool server and the subsequent usage of the deployed tools in a Java ABC SIB graph.

GEAR's current jETI implementation is still in its early stages. Please report any bugs or odd behaviour you may find using our bug tracker.


Necessary files

To deploy GEAR as a jETI tool, you will of course first need a working jETI tool server and the required permissions to edit the tools.

The tools are provided as part of the GEAR CLI (command-line interface) package that contains several different CLI implementations. The corresponding JAR file (usually called something like GEAR-CLI.jar) has to be placed inside the lib directory of the tool server.


Adding the tools to the jETI tool server

Then, you need to add the jETI services (either via the web configurator or directly in the file config/tools.xml). The services provided are

  • The remote model-checking process itself, taking an existing SIB Graph, along with a property to check. The result (a set of satisfying nodes) can be displayed afterwards.
  • The generation of a game graph that displays extensive information about the underlying model-checking process. The graph can be displayed afterwards.


Via the web frontend

Add new services with the following parameters:

For the model checking tool
Type Name Class Class Argument Value
static N/A String leave empty java
static N/A String leave empty -cp
static N/A String leave empty lib/GEAR-CLI.jar
static N/A String leave empty de.metaframe.plugin.gear.cli.ModelcheckingCLI
required formula Input File N/A N/A
required model Input File N/A N/A
required nodelist Output File N/A N/A


For the game graph generation tool
Type Name Class Class Argument Value
static N/A String leave empty java
static N/A String leave empty -cp
static N/A String leave empty lib/GEAR-CLI.jar
static N/A String leave empty de.metaframe.plugin.gear.cli.GameGraphCLI
required formula Input File N/A N/A
required model Input File N/A N/A
required gamegraph Output File N/A N/A


Via config/tools.xml

Alternatively, you can add the tool descriptions directly in the config/tools.xml tool description file. The following XML snippets should help.

For the model checking tool:

<tool name='GEARMC' active='true' class='de.unido.ls5.eti.toolserver.RuntimeUnix' method='exec'>
  <description>Returns satisfying nodes for formula and model.</description>
  <array class='java.lang.Object'>
    <parameter class='java.lang.String' value='java' />
    <parameter class='java.lang.String' value='-cp' />
    <parameter class='java.lang.String' value='lib/gear/gear-CLI.jar' />
    <parameter class='java.lang.String' value='de.metaframe.plugin.gear.cli.ModelcheckingCLI' />
    <parameter name='formula' class='de.unido.ls5.eti.toolserver.InputFileReference' required='true' description='Formula' />
    <parameter name='model' class='de.unido.ls5.eti.toolserver.InputFileReference' required='true' description='The model to check.' />
    <parameter name='nodelist' class='de.unido.ls5.eti.toolserver.OutputFileReference' required='true' description='List of satisfying nodes.' />
  </array>
</tool>

For the game graph generation tool:

<tool name='GEARGameGraph' active='true' class='de.unido.ls5.eti.toolserver.RuntimeUnix' method='exec'>
  <description>Returns GameGraph for formula and model.</description>
  <array class='java.lang.Object'>
    <parameter class='java.lang.String' value='java' />
    <parameter class='java.lang.String' value='-cp' />
    <parameter class='java.lang.String' value='lib/gear/gear-CLI.jar' />
    <parameter class='java.lang.String' value='de.metaframe.plugin.gear.cli.GameGraphCLI' />
    <parameter name='formula' class='de.unido.ls5.eti.toolserver.InputFileReference' required='true' description='Formula' />
    <parameter name='model' class='de.unido.ls5.eti.toolserver.InputFileReference' required='true' description='The model to check.' />
    <parameter name='gamegraph' class='de.unido.ls5.eti.toolserver.OutputFileReference' required='true' description='The resulting GameGraph.' />
  </array>
</tool>


Generate the required SIBs

Let the jETI web configurator generate the required SIBs for you. The resulting ZIP file should contain one SIB for every tool you have selected in the tool editor. Place that ZIP file somewhere where your Java ABC installation can find and use them.


Build SIB graphs to make use of GEAR remotely

Now you need to integrate the remote usage of GEAR into an existing SIB graph. The example graphs contained in the ZIP file below should give you an idea of how this is done.

The two ReadFile SIBs in the beginning of these SIB graphs load the required model and formula into an execution context so that the tools can use them. The model is just a SIB graph you have saved somewhere and the expression is a text file containing a parseable symbolic expression that may make use of the standard built-in operators and macros.


Any questions? Try the GEAR home page, the GEAR mailing list or our bug tracker.