Rodin File Types

The Rodin platform manipulates several kind of files which are usually distinguished by their extension.

The purpose of this page is to inventory all file types used by the Rodin platform and plug-ins.

File Extension	Root Element Type	Contents	Plug-in	Notes
.bum	IMachineRoot	Event-B Machine	Event-B Core
.buc	IContextRoot	Event-B Context	Event-B Core
.bcm	ISCMachineRoot	Event-B Statically Checked Machine	Event-B Core
.bcc	ISCContextRoot	Event-B Statically Checked Context	Event-B Core
.bpo	IPORoot	Event-B Proof Obligations	Event-B Core
.bpr	IPRRoot	Event-B Proofs	Event-B Core
.bps	IPSRoot	Event-B Proof Statuses	Event-B Core
.bcp	IComposedMachineRoot	Composition Definition	Shared-Event Composition
.bcs	ISCComposedMachineRoot	Statically checked Composition Definition	Shared-Event Composition
.dcp	IDecompositionRoot	Decomposition Record	Decomposition
.dcc	ISCDecompositionRoot	Statically checked Decomposition Record	Decomposition
.xmb	N/A	Machine or Context stored in the standard EMF XMI format	Event-B EMF Framework
.xmc	N/A	Composite Machine (using includes) stored in the standard EMF XMI format	Event-B EMF Framework + Inclusion
.cls	N/A	Class Diagram	iUML-B Class Diagrams
.cd	N/A	Class Diagram Layout	iUML-B Class Diagrams
.stm	N/A	State-machine Diagram	iUML-B State-Machines
.smd	N/A	State-machine Diagram Layout	iUML-B State-Machines
.pjd	N/A	Project Diagram Layout	iUML-B Project Diagrams
.prj_diag	N/A	Project Diagram Viewer (older version)	Event-B Project Diagram Plugin
.umlb	N/A	UML-B model	UML-B classic
.packageDiag	N/A	UML-B Package Diagram	UML-B classic
.classDiag	N/A	UML-B Class Diagram	UML-B classic
.stateDiag	N/A	UML-B State Diagram	UML-B classic
.contextDiag	N/A	UML-B Context Diagram	UML-B classic
.mch	N/A	Event-B Machine	Text-Based Event-B
.ctx	N/A	Event-B Context	Text-Based Event-B
.ins	InstRoot	Generic Instantiation Unchecked	Generic Instantiation
.insc	SCInstRoot	Generic Instantiation Checked	Generic Instantiation
.bumx	N/A	XMachine File	XEvent-B
.bucx	N/A	XContext file	XEvent-B