How to read Rodin projects and elements programmatically
From Event-B
Contents |
How to read a Rodin Project
You can access an existing Rodin project usingRodinCore.getRodinDB().getRodinProject("your_project_name"). This returns a handle to an IRodinProject
. This project may or may not exist. Call exists
on the resulting project to be sure.
An other option is calling RodinCore.getRodinDB().getRodinProjects, which returns an array with of all existing IRodinProject
s.
How to read a Machine or a Context
Machines and Contexts are accessed throughIMachineRoot
and IContextRoot
respectively. Those roots are stored in IRodinFile
s.
The following method returns all existing IMachineRoot
s of a project:
public static IMachineRoot[] getMachineRootChildren(IRodinProject project) throws RodinDBException {
ArrayList<IMachineRoot> result = new ArrayList<IMachineRoot>();
for (IRodinElement element : project.getChildren()) {
if (element instanceof IRodinFile) {
IInternalElement root = ((IRodinFile) element).getRoot();
if (root instanceof IMachineRoot) {
result.add((IMachineRoot) root);
}
}
}
return result.toArray(new IMachineRoot[result.size()]);
}
And this method returns all existing
IContextRoot
s of a project:
public static IContextRoot[] getContextRootChildren(IRodinProject project) throws RodinDBException {
ArrayList<IContextRoot> result = new ArrayList<IContextRoot>();
for (IRodinElement element : project.getChildren()) {
if (element instanceof IRodinFile) {
IInternalElement root = ((IRodinFile) element).getRoot();
if (root instanceof IContextRoot) {
result.add((IContextRoot) root);
}
}
}
return result.toArray(new IContextRoot[result.size()]);
}
How to read Invariants, Events, Theorems etc.
Once you have obtained anIMachineRoot
or an IContextRoot
it is very easy to access its child elements. There exist functions such as getInvariants() to obtain an array of all existing IInvariants
. If you just want a specific element call a function of the form getInvariant("your_invariant_name"). Again this only returns a handle and does not guarantee that the element exists.
How to read Proof Obligations
For information on reading proof obligations, have a look at Accessing Proof Obligations.
