(of the MSD-to-SMV for Product Lines Tool)

Our tool requires first to install and configure an eclipse environment for editing the scenario-based product line specifications and for transforming them into NuSMV models. Second, it requires to patch and compile NuSMV for checking feature-enriched SMV models. The latter procedure is described here.

Due to dependency problems, we currently have difficulties of bundling our tool into an easily installable package. Thus, our tool has to be installed by setting up a development environment as described below. For this setup, it is necessary that a Java JDK is installed (JDK 6 (1.6) is recommended).

New: MAC users can download an pre-configured eclipse set-up and a readily patched NuSMV version in this ZIP archive. (So there is no need to go through the steps below.)

Please do not hesitate to contact me in case you run into problems.

Setting up the eclipse environment

  1. Download and install a the eclipse modeling tools from here (version 3.7.2 is recommended).
  2. Start the workbench and install Xtext 2.2.1. To do this, go to Help->Install new Software… Then enter the following update site URL:

    Select the feature group Xtext 2.2.1 as shown in the screenshot below.

    Xtext installation via the update site

    Then click Next and acknowledge the license agreements. After the installation is completed, acknowledge the restart of the workbench (“Restart Now”).

  3. Import the projects archived in the file Download and save the file on your local drive. In your eclipse workbench, go to File->Import and select General->Existing projects into workspace. Then hit Next, choose to select an archive file, and browse to the location of In the projects list, there should now be a number of projects visible. Hit finish.
    (There may be problems if you have Java 1.7 installed. Then you can set the Java compiler compliance level back to 1.6: Go to Window->Preferences and then select Java->Compiler in the tree left. On the right, set the Compiler Compliance level to 1.6.)
    Now there should be no compile errors in you workspace.
  4. Now you need to set up a runtime workspace. To do this select Run->Run Configurations… Then in the tree on the right select “Eclipse Application” and in the toolbar above hit “New launch configuration”. Select the “Arguments” tab and make sure that you specify the following VM arguments:
    • -Xms40m -Xmx512m -XX:PermSize=256m -XX:MaxPermSize=256m

    The settings for the respective parameter can be higher, but should not be lower. You can leave all other settings on default. Start the runtime workbench by clicking in “Run”. This opens a new eclipse workbench window.

  5. In your runtime workbench, import the projects archived in Download the file and import the archived projects as explained above.There will now be the following two projects in your workspace:
    • it.polimi.elet.deepse.msdtonusmv
    • it.polimi.elet.deepse.msdtonusmv.examples

You can now continue to the following page on using the tool.