External Tools Integration

Integrating external tools in Atelier B 4

This page describes the extensibility features found in Atelier B 4. Atelier B 4 allows running « external tools » from within the GUI. For now those kinds of external tools can be integrated:

  • project external tools. Those tools are running on a project, and appears in the « Project » menu of the GUI. For instance, they can be used to provide metrics on a project
  • component. Those tools are running on a component, and appears in the « Component » menu of the GUI. They are launched on the selected component(s)
  • po. Those tools are running on a selected proof obligation in the interactive prover
  • goal. Those tools are running on the current goal of the interactive prover

Integrating an external tool is done by writing a « .etool » xml file. This file describes the type of tool, as well as the command that will be started. This file should be located in the « extensions » subdirectory of the Atelier B installation, and is loaded when the Atelier B GUI start. For each « etool » file, a corresponding menu entry is created within the « Project » or « Component » menu of the GUI. When the menu is clicked, the tool is launched, and the corresponding task appears in the « Tasks » window of Atelier B. Double-clicking on the task displays a windows showing the output of the tool. First, the main feature is illustrated on a simple example. The complete syntax of the « .etool » files is then described.

Two examples are available:

 

A simple example

Here is a simple example of tool for windows, that open the project database file (bdp) in an explorer window. The text should be saved in a file « openbdp.etool » located in the « extensions » subdirectory of the Atelier B installation directory (this directory may have to be created).

<externalTool name="openbdp"
       category="project"
       label="Open bdp"
       shortcut="Ctrl+Y"
       tooltip="Opens the project database directory in an explorer window"
       icon="openbdp.png"
       >
       <command>c:windowsexplorer.exe</command>
       <param>${projectBdp}</param>
</externalTool>

The file starts with the externalTool tag, which contains the required information as attributes (name, menu label, icon, etc…). Within the external tool, the following tags are used to describe the command:

  • command: the path to the executable file that will be started (here c:windowsexplorer.exe)
  • param: describes one parameter of the command. Here the command takes only one parameter, but for more complex commands with multiple parameters, there should be as many <param> as parameters.

The variable elements of the command (here the path to the bdp directory) are expressed using the ${variableName} notation. Here ${projectBdp} is replaced by the path to the bdp directory of the project.

A more complex example

The previous example had one major shortcoming: the path to the « explorer » executable is hardcoded. A better solution would be to allow the user to configure the path to the « explorer » executable. This can be done by using the toolParameter tag, that allows defining a new variable for using within the command. In that case, the corresponding etool file would be the following:

<externalTool name="openbdp"
      category="project"
      label="Open bdp"
      shortcut="Ctrl+Y"
      tooltip="Opens the project database directory in an explorer window"
      icon="openbdp.png"
      >
      <toolParameter name="explorer" type="exefile" default="c:windowsexplorer.exe" />

      <command>${explorer}</command>
      <param>${projectBdp}</param>
</externalTool>

Here, the toolParameter tag define a new variable that can be set by the user: a new tab is created in the « Preferences » dialog, that allows setting the path to the « explorer » executable (linux users could also provide a more suitable file manager).

Integration of ProB model-checker

ProB model-checker is now self generating the etool file for Atelier B (see Detailed procedure).

A sample file is provided below:

<externalTool category="component"   name="ProBTclTk" label="&Animate with ProB (Tcl/Tk)">
   <toolParameter name="editor" type="tool" configure="yes"
   default="c:/program files/prob/ProBWin.exe" />
   <command>${editor}</command>
   <param>${componentPath}</param>
   </externalTool>

List of recognised tags

Here is the current list of recognized tags as well as their allowed attributes.

  • externalTool: The enclosing tag of the etool file. Defines an external tool
  • toolParameter: Used to define parameters for running the command
  • temporaryFile: Used to create temporary files before running the command
  • command: The command that should be run
  • param: a parameter to the command
  • componentList: the list of components that are parts of the project. Used to specify parameters to the command

The allowed attributes are listed in the next sections.

externalTool

The externalTool tag is the main tag of the etool file. It is required, and can contain the following attributes:

  • name: the internal name of the tool (required)
  • category: the category of the tool. Can be « component« , « project« , « po » or « goal » (required)
  • label: the text that is displayed in the corresponding menu entry (required)
  • menu: if set, the menu entry will be placed in the given submenu. This can be used to group different related external tools.
  • shortcut: an optional keyboard shortcut for calling the tool
  • tooltip: information that is displayed about the tool
  • icon: the icon that will be used in the corresponding menu entry. This must be the name of a .png file located in the same directory as the etool file.
  • outputType: the type of output of the tool. If this tag is not present, the output is assumed to be text. Valid values are text and html

toolParameter

The toolParameter tag is used to define a variable that will be expansed when running the tool. The allowed attributes are the following:

  • name (required): the name of the parameter. The name correspond to the name of the variable
  • type (required): the type of the parameter. Can be one of « ressource« , « exefile« , « file » and « tool« 
  • default: a default value for the parameter if no other value is available
  • optional: can be « yes » or « no » to indicate that the parameter is optional. If the parameter is not optional, the tool will not be executed in the case where no value is found for the parameter
  • description: a textual description of the parameter. This field is used when creating a preference page for configuring the tool

Depending on the type of the tool, the textual content of the tag can be required or not, and can have different meanings. The requirement depends on the type of the attribute:

  • ressource: in that case the text field correspond to an Atelier B ressource, and the variable will be expanded into the value of the ressource. For instance:
  <toolParameter name="refinerFile" type="ressource">ATB*BART*RefinerFile</toolParameter>
  • exefile: in that case, the text field is not used. The variable will be expanded to the path of a file configured by the user in the « Preferences » dialog.
  <toolParameter name="editor" type="exefile" description="The editor" default="/usr/bin/xemacs" />
  • file: the text field is not used, and the variable will be expansed to the path of a file configured by the user in the « Preferences » dialog.
   <toolParameter name="myFile" type="file" description="tool configuration file" />
  • tool: This type correspond to a tool, either provided by Atelier B, either provided by the extension. The text field is optional, and correspond to an Atelier B ressource. The variable is expansed into the full path to the corresponding tool. The tool can be an executable or a logic-solver file (*.kin). Example:
 <toolParameter name="krt" type="tool" description="Logic Solver" default="krt">ATB*ATB*Logic_Solver_Command</toolParameter>

The tool is searched as follows: first, the content of the provided ressource (if any) is looked up. If it is empty or if no ressource is provided, the default value is taken. Then, the corresponding file is searched in the following directories

  • The os-dependant directory of Atelier B (bbin/win32 on windows, bbin/linux on linux, etc…)
  • The external tool directory. If the tool is named « mytool », this directory will be extensions/mytool
  • The os-dependant subdirectories of the external tool: extensions/mytool/win32 on windows, extensions/mytool/linux on linux, etc…

temporaryFile

The temporaryFile tag is used to write a temporary file before running the command. This can be used in the case where the command takes an input file. The textual content of the temporaryFile tag correspond to a template file, where all the variables are replaced by their values. There can be as many temporaryFile tags as needed in the etool file.

The following attributes are recognised:

  • name (required): the name of the variable that will hold the path to the created temporary file
  • directory (optional): the directory where the temporary file should be created. If no directory is specified, the system temporary directory will be used. Variables can be used to express this directory.
  • template (optional): A template for the name of the file. If provided, the name of the temporary file will be based on template

command

The command tag specifies the executable that should be started. One and only one command tag should be present in the extension file.

List of attributes:

  • workingDirectory (optional): The working directory of the started tool. Variables can be used to specify this directory

param

The param tag specifies one and only one argument to the <command> tag. There should be as many param tags as there are arguments to the command. This is required to correctly handle spaces in directories. This following attributes can be used with this tag:

  • fileExists this tag indicates that the corresponding parameter will be added only if the file referenced in the attribute exists. For example, the following will only add the PatchProver file if it exists:
  <param fileExists="${projectBdp}/PatchProver">${projectBdp}/PatchProver</param>
  • option this tag will add the parameter given by « option » before the parameter. It can be used when two parameters are « linked » together. For instance, the two following examples are equivalent:
  <param option="-I">${includeFile}</param>

  <param>-I</param>
  <param>${includeFile}</param>

componentList

The componentList tag is expansed into the list of filenames of the components present in the selected project. Each component will correspond to one parameter. It is used to specify the parameters to the command tag, and can be used with other param tags.

This behaviour can be modified by using the following attributes:

* option this attribute adds the parameter given by option before each component parameter.
* ext this attribute replaces the extension of the component by the given extension, and adds the resulting file only if it exists

To clarify, lets assume that the current project holds four components: test.mchtest_i.impctx.mch and ctx_i.imp. In the simplest case,

<componentList/>

will expand into

test.mch test_i.imp ctx.mch ctx_i.imp

Using the option attribute will add the prefix to each of the expanded component

<componentList option="-m" />

will expand into

-m test.mch -m test_i.imp -m ctx.mch -m ctx_i.imp

The ext attribute can be used to filter the type of the components:

<componentList ext="mch" />

will expand into the list of abstract machines of the project:

test.mch ctx.mch

The ext can also be used to obtain files with the same name as the component, but a different extension. For instance:

<componentList ext="pmm" />

will expand into the list of pmm files of the project (the pmm files that do not exists are not added to the list). Assuming that test_i.pmm and ctx_i.pmm are present in the same directory than the components, but that no pmm files are provided for test.mch and test_i.imp, the resulting arguments will be

test_i.pmm ctx_i.pmm

List of predefined variables

The following table shows all the predefined variables as well as their content:

Variable Tool type Description Min Atelierb version
${projectName} All The name of the currently selected project, or the project to which the selected component belongs 4.0
${projectBdp} All The absolute path to the « bdp » directory of the project 4.0
${projectTrad} All The absolute path to the translation (« lang ») directory of the project 4.0.2
${extensionsDir} All The path to the extension directory 4.0
${componentName} Component, Po, Goal The name of the selected component 4.0
${componentPath} Component, Po, Goal The absolute path to the selected component file 4.0
${componentDir} Component, Po, Goal The absolute path to the directory where the component is located 4.0
${componentExt} Component, Po, Goal The extension of the component 4.0
${poName} Po, Goal The name of the current proof obligation 4.0
${poGoal} Goal The current goal (as text) 4.0
${poHypothesis} Goal The current list of hypothesis (as text) 4.0