(The MSD-to-SMV for Product Lines Tool)
If you’ve followed the installation instructions, there will now be the following two projects in your (runtime) workspace:
The first project contains the transformation rules for transforming the UML scenario product line specifications to NuSMV models. The second contains a few examples specifications as well as their resulting NuSMV models. In the subfolders of the example project, you find the following files:
Now you can do the following:
Inspect or edit the UML scenario product line specifications
Open the *.umldi files with the TOPCASED UML editor that is extended with a special MSD editor. To open an MSD diagram, navigate to the interactions in the outline view and open the MSD diagram.
Inspect or edit the NuSMV models
Open *.smv (or *.nusmv) files with a syntax-highlighting MSD editor.
Check the consistency of the MSD product line specification
Call “NuSMV -fbdd <specification-name>.smv”.
Perform a MSD-to-SMV transformation
To perform a transformation of a UML scenario product line specification, the following steps are necessary. We distinguish between (1) changing an existing UML scenario product line specification and re-running an already configured transformation the transformation and (2) configuring a new transformation for a new UML scenario product line specification.
- Re-running a transformation: delete the .smv and.corr.xmi file and then right-click on the .interpreterconfiguration file->TGG-Interpreter->perform configured transformation. This should start a transformation. Hit “OK” on the two dialog windows that open after the transformation is finished to save the models. A new .smv file and another .corr.xmi file will be created.
- Creating a new transformation configuration: Select the .uml model and the it.polimi.elet.deepse.msdtonusmv\tgg\msdtonusmv.tgg file in your project explorer, right-click->TGG-Interpreter->create forward transformation interpreter configuration. This will create a .interpreterconfiguration file. The transformation can now be executed as described above. By default, however, the transformation will create a .NuSMV file, which will not be editable using the NuSMV text editor. To create a .smv text file, open the .interpreterconfiguration file with the TGG Interpreter configuration tree editor and navigate to the “Domain Model NuSMV”. Right-click and select “Show in Properties View” and then in the properties view change the appendix of the resource URI to be .smv instead of .NuSMV.