Difference between pages "Extension Proof Rules" and "How to read Rodin projects and elements programmatically"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Nicolas
m
 
imported>Maria
 
Line 1: Line 1:
Rules that are marked with a <tt>*</tt> in the first column are implemented in the latest version of Rodin.
+
==How to read a Rodin Project==
Rules without a <tt>*</tt> are planned to be implemented in future versions.
+
You can access an existing Rodin project using <code>RodinCore.getRodinDB().getRodinProject("your_project_name")</code>. This returns a handle to an <code>IRodinProject</code>. This project may or may not exist. Call <code>exists</code> on the resulting project to be sure.
Other conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Rewrite_Rules]].
 
  
== Rewrite Rules ==
+
An other option is calling <code>RodinCore.getRodinDB().getRodinProjects</code>, which returns an array with of all existing <code>IRodinProject</code>s.
  
{{RRHeader}}
+
==How to read a Machine or a Context==
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_COND_BTRUE}}||<math> \operatorname{COND}(\btrue, E_1, E_2)  \;\;\defi\;\;  E_1 </math>||  ||  A
+
Machines and Contexts are accessed through <code>IMachineRoot</code> and <code>IContextRoot</code> respectively. Those roots are stored in <code>IRodinFile</code>s.
{{RRRow}}|*||{{Rulename|SIMP_SPECIAL_COND_BFALSE}}||<math> \operatorname{COND}(\bfalse, E_1, E_2)  \;\;\defi\;\;  E_2 </math>||  ||  A
 
|}
 
  
 +
The following method returns all existing <code>IMachineRoot</code>s of a project:
  
== Inference Rules ==
 
{{RRHeader}}
 
  
|}
+
[[Category:Developer documentation]]
 
+
[[Category:Rodin Platform]]
[[Category:User documentation|The Proving Perspective]]
 
[[Category:Rodin Platform|The Proving Perspective]]
 
[[Category:User manual|The Proving Perspective]]
 

Revision as of 13:58, 28 October 2008

How to read a Rodin Project

You can access an existing Rodin project using RodinCore.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 IRodinProjects.

How to read a Machine or a Context

Machines and Contexts are accessed through IMachineRoot and IContextRoot respectively. Those roots are stored in IRodinFiles.

The following method returns all existing IMachineRoots of a project: