Difference between revisions of "Rodin File Types"

From Event-B
Jump to navigationJump to search
imported>Andy
imported>Colin
(update uml-b/coda file extensions inc. XText)
 
(7 intermediate revisions by 2 users not shown)
Line 5: Line 5:
 
{{SimpleHeader}}
 
{{SimpleHeader}}
 
|-
 
|-
|File Extension  || Root Element Type || Contents ||  Plug-in
+
|File Extension  || Root Element Type || Contents ||  Plug-in || Notes
 
|-
 
|-
 
|<tt>.bum</tt> || {{class|IMachineRoot}} || Event-B Machine || Event-B Core
 
|<tt>.bum</tt> || {{class|IMachineRoot}} || Event-B Machine || Event-B Core
Line 20: Line 20:
 
|-
 
|-
 
|<tt>.bps</tt> || {{class|IPSRoot}} || Event-B Proof Statuses || Event-B Core
 
|<tt>.bps</tt> || {{class|IPSRoot}} || Event-B Proof Statuses || Event-B Core
 +
|-
 +
|<tt>.bcp</tt> || {{class|IComposedMachineRoot}} || Composition Definition  || Shared-Event Composition
 +
|-
 +
|<tt>.bcs</tt> || {{class|ISCComposedMachineRoot}} || Statically checked Composition Definition  || Shared-Event Composition
 +
|-
 +
|<tt>.dcp</tt> || {{class|IDecompositionRoot}} || Decomposition Record || Decomposition
 +
|-
 +
|<tt>.dcc</tt> || {{class|ISCDecompositionRoot}} || Statically checked Decomposition Record || Decomposition
 
|-
 
|-
 
|<tt>.xmb</tt> || N/A || Machine or Context stored in the standard EMF XMI format || Event-B EMF Framework
 
|<tt>.xmb</tt> || N/A || Machine or Context stored in the standard EMF XMI format || Event-B EMF Framework
 +
|-
 +
|<tt>.xmc</tt> || N/A || Composite Machine (using includes) stored in the standard EMF XMI format || Event-B EMF Framework + Inclusion
 +
|-
 +
|<tt>.cls</tt> || N/A || Class Diagram || iUML-B Class Diagrams
 +
|-
 +
|<tt>.clsx</tt> || N/A || Class Diagram XText || xUML-B Class Diagrams
 +
|-
 +
|<tt>.cd</tt> || N/A || Class Diagram Layout || iUML-B Class Diagrams
 +
|-
 +
|<tt>.stm</tt> || N/A || State-machine Diagram ||  iUML-B State-Machines
 +
|-
 +
|<tt>.stmx</tt> || N/A || State-machine Diagram XText || xUML-B State-Machines
 
|-
 
|-
 
|<tt>.smd</tt> || N/A || State-machine Diagram Layout || iUML-B State-Machines
 
|<tt>.smd</tt> || N/A || State-machine Diagram Layout || iUML-B State-Machines
 
|-
 
|-
|<tt>.cd</tt> || N/A || Class Diagram Layout || iUML-B Class Diagrams
+
|<tt>.cmp</tt> || N/A || CODA component Diagram ||  CODA component Diagram
 +
|-
 +
|<tt>.cmpx</tt> || N/A || CODA component Diagram XText || xCODA component Diagram
 +
|-
 +
|<tt>.cpd</tt> || N/A || CODA component Diagram Layout || CODA component Diagram
 
|-
 
|-
 
|<tt>.pjd</tt> || N/A || Project Diagram Layout || iUML-B Project Diagrams
 
|<tt>.pjd</tt> || N/A || Project Diagram Layout || iUML-B Project Diagrams
Line 41: Line 65:
 
|<tt>.contextDiag</tt> || N/A || UML-B Context Diagram || UML-B classic
 
|<tt>.contextDiag</tt> || N/A || UML-B Context Diagram || UML-B classic
 
|-
 
|-
|<tt>.mch</tt> || {{class|Machine}} || Event-B Machine || Text-Based Event-B
+
|<tt>.mch</tt> || N/A || Event-B Machine || Text-Based Event-B
 +
|-
 +
|<tt>.ctx</tt> || N/A || Event-B Context || Text-Based Event-B
 +
|-
 +
|<tt>.ins</tt> || {{class|InstRoot}} || Generic Instantiation Unchecked || Generic Instantiation
 +
|-
 +
|<tt>.insc</tt> || {{class|SCInstRoot}} || Generic Instantiation Checked || Generic Instantiation
 +
|-
 +
|<tt>.bumx</tt> || N/A || XMachine File || XEvent-B
 +
|-
 +
|<tt>.bucx</tt> || N/A || XContext file || XEvent-B
 
|-
 
|-
|<tt>.ctx</tt> || {{class|Context}} || Event-B Context || Text-Based Event-B
 
  
 
|}
 
|}

Latest revision as of 14:55, 12 March 2019

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
.clsx N/A Class Diagram XText xUML-B Class Diagrams
.cd N/A Class Diagram Layout iUML-B Class Diagrams
.stm N/A State-machine Diagram iUML-B State-Machines
.stmx N/A State-machine Diagram XText xUML-B State-Machines
.smd N/A State-machine Diagram Layout iUML-B State-Machines
.cmp N/A CODA component Diagram CODA component Diagram
.cmpx N/A CODA component Diagram XText xCODA component Diagram
.cpd N/A CODA component Diagram Layout CODA component Diagram
.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