How to create Rodin projects programmatically

The code snippets on this page are derived from the UML-B plugin 'ac.soton.umlb.eventB', package 'generator'. You can find this package in the Rodin projects sourceforge SVN repository : https://sourceforge.net/p/rodin-b-sharp/svn/HEAD/tree/trunk/UML-B/ac.soton.umlb.eventB/src/ac/soton/umlb/eventB/generator/

[Some of the code could be improved wrt the use of monitors. An explanation of some of the parameters in the Rodin API could be added]

How to create a Rodin Project

Here is a method to create a Rodin project of a given name. (This method overwrites any existing Rodin project of that name). The project handle is retrieved from the rodin database. if the project does not exist, it is created using the handle. The project is opened. The project is given the Rodin 'nature' (if not already). The project is set to derived (this is not strictly necessary but it can be used to distinguish projects that the user has created from ones that have been created programmatically).

      public static IRodinProject createRodinProject(final String projectName) {
		final IWorkspace workspace = ResourcesPlugin.getWorkspace(); 
		try {
			final IRodinDB rodinDB = RodinCore.valueOf(workspace.getRoot());
			final IRodinProject rodinProject = rodinDB.getRodinProject(projectName);
			final IProject project = rodinProject.getProject();
			if (!project.exists()) project.create(null);
			project.open(null);

			// add the rodin nature if it isn't already there
			final IProjectDescription description = project.getDescription();
			final String[] natures = description.getNatureIds();
			boolean alreadyRodin = false;
			for (int i = 0; i < natures.length; ++i)
				if (RodinCore.NATURE_ID.equals(natures[i])) {
					alreadyRodin = true;
					break;
				}
			if (!alreadyRodin) {     // Add the Rodin nature
				final String[] newNatures = new String[natures.length + 1];
				System.arraycopy(natures, 0, newNatures, 0, natures.length);
				newNatures[natures.length] = RodinCore.NATURE_ID;
				description.setNatureIds(newNatures);
				project.setDescription(description, null);
			}
			project.setDerived(true);  // mark the project as derived (this could be used to distinguish user editable projects
			return rodinProject;
		} catch (final CoreException e) {
                       .... exception code ....
		}
	}

Once you have created a Rodin Project you may want to call its save method to save it. Since this method makes changes to the workspace, you need to call it from a WorkspaceRunnable. For Example:-

	RodinCore.run(new IWorkspaceRunnable() {
		public void run(final IProgressMonitor monitor) throws CoreException{
			monitor.beginTask("",10);
 			rodinProject=createRodinProject(projectName);
			rodinProject.save(null, true);
			monitor.done();
		}
	},null);

How to create a Rodin File construct (e.g. Machine, Context)

Here is a method to create a new Rodin File construct of a given filename in the given Rodin project and with a given comment. Note that the filename should include the correct extension (e.g. ".bum" for a Machine). The handle is retrieved from the Rodin project and used to create the new Rodin file. The corresponding resource is set to derived to indicate that it was generated programmatically. The comment is added to the Rodin File.

	public static IRodinFile createRodinConstruct(final String filename, final IRodinProject rProject, final String comment) {
		if (rProject == null)
			return null;
		try {
			final IRodinFile rodinFile = rProject.getRodinFile(filename);
			rodinFile.create(true, null);
			rodinFile.getResource().setDerived(true);    // mark the file as derived
			if (rodinFile instanceof ICommentedElement)
 				if (comment != null && !comment.trim().equals(""))
					((ICommentedElement) rodinFile).setComment(comment, null);
			return rodinFile;
		} catch (final Exception e) {
                       .... exception code ....
		}
	}

As with the Rodin project above, if you want to save the created construct, you should do this from a WorkspaceRunnable.

How to create a Rodin element

Here is a method to create a new Rodin element of a given type and name in the given Rodin element and Rodin File and with a given comment. The handle is retrieved from the parent element and used to create the new Rodin element. Depending on the type of the new Rodin element, the name is used as the label, identifier, or abstract event label. The comment is set if the element type owns a comment.

	public static IInternalElement createRodinElement(
			final IInternalElementType type,
                       final String name,
                       final IInternalElement parent,
		        final IRodinFile rodinFile,
                       final String comment) {
		if (parent == null) return null;
		try {
			final IInternalElement rodinEl = parent.getInternalElement(type, name)
			rodinEl.create(null, null);
			if (rodinEl instanceof ILabeledElement)
				((ILabeledElement) rodinEl).setLabel(name, null);
			if (rodinEl instanceof IIdentifierElement)
				((IIdentifierElement) rodinEl).setIdentifierString(name, null);
			if (rodinEl instanceof ICommentedElement)
				if (comment != null)
					((ICommentedElement) rodinEl).setComment(comment,null);
			if (rodinEl instanceof IRefinesEvent)
				((IRefinesEvent) rodinEl).setAbstractEventLabel(name, null);
			return rodinEl;
		} catch (final Exception e) {
                       .... exception code ....
		}
	}

This method is called passing the appropriate element type which can be obtained from the Rodin element class. For example an Invariant can be created like this:-

      	IInvariant invariant = (IInvariant) createRodinElement(IInvariant.ELEMENT_TYPE, invariantName, rodinFile, rodinFile, comment);

How to set attributes of a Rodin Element

To set attributes of a Rodin Element, use the appropriate methods of the element (depending on the element type). For example:-

	invariant.setPredicateString(myPredicateString,null);