Difference between revisions of "Single View Design"

From Event-B
Jump to navigationJump to search
imported>Maria
imported>Jrloria
 
(18 intermediate revisions by 5 users not shown)
Line 1: Line 1:
 
==Purpose==
 
==Purpose==
The purpose of the Single View Design is to present everything in a single view in Rodin.
+
 
 +
The Rodin platform, at the beginning of the Deploy project, provided two views for displaying models and proofs:
 +
* The ''Project Explorer'' displays the modelling elements stored in the Rodin database.
 +
* The ''Obligation Explorer'' displays the proof obligations together with their proof state.
 +
 
 +
The clean separation between modelling and proving looked good during paper design.  However, users reported that they were constantly switching between the two views. This is due to the fact that modelling and proving are not separate activities, one being performed after the other. In general practice, both activities are intertwined.
 +
 
 +
Independently, Eclipse has released a new framework called the ''Common Navigation Framework'' since these two views were designed and implemented. The purpose of this framework is to provide Eclipse plug-ins with basic blocks for easily implementing views like the ''Project Explorer''. Moreover, this framework allows various plug-ins to cooperate together in populating such views, thus reinforcing plug-in integration into the platform.
 +
 
 +
Therefore, it was decided in the Deploy project to combine the two original views into a single one that would display modelling elements and proof obligations together. This new single view should also take advantage of the ''Common Navigation Framework'', in order to improve its seamless integration within Eclipse.
  
 
==Specification==
 
==Specification==
 
The Single View Design uses the [http://wiki.eclipse.org/index.php/Common_Navigator_Framework Common Navigator Framework] that is provided by Eclipse.
 
The Single View Design uses the [http://wiki.eclipse.org/index.php/Common_Navigator_Framework Common Navigator Framework] that is provided by Eclipse.
 
[[Image:MasterDetails.jpg]]
 
  
 
===The Navigator===
 
===The Navigator===
The navigator is the part on the left that contains a tree. It presents all projects and their contents. The users can choose between to ways how the machines and contexts will be presented:
+
The navigator contains a tree of all projects and their contents. The users can choose between two ways how the machines and contexts will be presented:
 
*A simple structure where all machines and contexts are presented on the same level
 
*A simple structure where all machines and contexts are presented on the same level
 
*A complex structure where the machines and contexts are presented as a tree. Thus dependencies between machines and contexts (like ''refines'' or ''sees'') are made visible.
 
*A complex structure where the machines and contexts are presented as a tree. Thus dependencies between machines and contexts (like ''refines'' or ''sees'') are made visible.
  
 
+
===The Statistics===
===The Details===
+
The statistics view presents information about the state of the proof obligations of the selected node in the navigator.
The details part is situated on the right and may contain several tabs. The content of each tab may depend on the selection in the navigator. Currently the only tab that exists is the statistics tab. It is possible to add new custom tabs.
 
 
 
====Statistics====
 
The statistics tab presents information about the state of the proof obligations of the selected node in the navigator.
 
  
 
==User guide==
 
==User guide==
Line 38: Line 41:
 
*'''Axioms'''
 
*'''Axioms'''
 
*'''Invariants'''
 
*'''Invariants'''
*'''Theorems'''
 
 
*'''Events'''
 
*'''Events'''
*'''Proof Obligations''': All proof obligations of a machine, context, axiom, invariant, theorem or event.
+
*'''Proof Obligations''': All proof obligations of a machine, context, axiom, invariant, derived invariant or event.
  
Here's an example of what the same projects looks like once using the complex machine and context structure (left) and once using the simple version (right).
+
Here is an example of what the same project looks like when using the complex machine and context structure (left) and when using the simple version (right).
  
 
[[Image:Complex.jpg]][[Image:Simple.jpg]]
 
[[Image:Complex.jpg]][[Image:Simple.jpg]]
Line 48: Line 50:
 
====Filters====
 
====Filters====
 
The filters let you choose what to hide in the navigator.
 
The filters let you choose what to hide in the navigator.
*'''File extensions''': There are various filters to hide certain types of files.
+
*'''File types''': There are various filters to hide certain types of files.
 
*'''All files and folders''': Hides all files and subfolders.
 
*'''All files and folders''': Hides all files and subfolders.
 
*'''Non Rodin Projects''': Hides all non Rodin projects. Also hides closed Rodin Projects.
 
*'''Non Rodin Projects''': Hides all non Rodin projects. Also hides closed Rodin Projects.
Line 60: Line 62:
  
 
===Statistics===
 
===Statistics===
The content displayed in the statistics tab depends on the selection in the navigator. Generally it shows an overview of the status of all proof obligations of the selected elements and a more detailed view below (if available). If a project is selected this means that in the overview the statistics for all proof obligations of that project are shown. In the detailed viewed each machine and context is listed with their own statistics. If you double click on an element in the detailed view, the corresponding element will be selected in the navigator.
+
The content displayed in the statistics view depends on the selection in the navigator. Generally it shows an overview of the status of all proof obligations of the selected elements and a more detailed view below (if available). If a project is selected this means that in the overview the statistics for all proof obligations of that project are shown. In the detailed viewed each machine and context is listed with their own statistics. If you double click on an element in the detailed view, the corresponding element will be selected in the navigator.
  
 
It is possible to select multiple elements in the navigator and get a combined statistics. But the selected elements must be on the same level (e.g. projects, machines/contexts). This mean if you select both machines and projects at the same time, you won't get any statistics.
 
It is possible to select multiple elements in the navigator and get a combined statistics. But the selected elements must be on the same level (e.g. projects, machines/contexts). This mean if you select both machines and projects at the same time, you won't get any statistics.
  
==Developer guide==
+
===See Also===
===Extending Single View Design===
+
* [[Extending Single View Design]]
Single View Design uses the [http://wiki.eclipse.org/index.php/Common_Navigator_Framework Common Navigator Framework] and [http://help.eclipse.org/stable/index.jsp?topic=/org.eclipse.platform.doc.isv/guide/forms_master_details.htm the Master/Details pattern]. The part on the left (the navigator) is the master part. You can add custom filters, content providers and action providers in a plug-in of your own. Add the extension <code>org.eclipse.ui.navigator.viewer</code>. There you can add viewerContentBindings and viewerActionBindings with viewerId <code>fr.systerel.explorer.navigator.view</code>. This binds your custom content, actions and filters to the navigator. The part on the right is the details part. You can add tabs of your own by extending <code>fr.systerel.explorer.masterDetails</code>.
 
 
 
In the picture you can see what types the nodes in the navigator have.
 
 
 
[[Image:Tree.jpg]]
 
 
 
====Adding a content provider to the navigator====
 
To add a custom content provider you have to use the <code>org.eclipse.ui.navigator.navigatorContent</code> extension. There you add a new navigatorContent. Example: You want to add a new child under the IMachineFile nodes. Define a navigatorContent and add triggerPoints. There you add a new <code>instanceof</code> with value <code>org.eventb.core.IMachineFile</code>. The priority of the navigatorContent decides in what order the content is shown with respect to other content providers. (For example the content provider for the variables has a higher priority than the one for invariants, that's why the variables appear before the invariants in the tree.) You need to provide a contentProvider and a labelProvider class. For more information read the extension point description of [http://help.eclipse.org/help32/index.jsp?topic=/org.eclipse.platform.doc.isv/reference/extension-points/org_eclipse_ui_navigator_navigatorContent.html navigatorContent]. Finally include your navigatorContent in your viewerContentBindings.
 
 
 
<code>
 
  <extension
 
        point="org.eclipse.ui.navigator.navigatorContent">
 
      <navigatorContent
 
            contentProvider="example.ContentProvider"
 
            id="example.navigatorContent"
 
            labelProvider="example.LabelProvider"
 
            name="Example Content">
 
        <triggerPoints>
 
            <instanceof
 
                  value="org.eventb.core.IMachineFile">
 
            </instanceof>
 
        </triggerPoints>
 
      </navigatorContent>
 
  </extension>
 
</code>
 
 
 
<code>
 
  <extension
 
        point="org.eclipse.ui.navigator.viewer">
 
      <viewerContentBinding
 
            viewerId="fr.systerel.explorer.navigator.view">
 
        <includes>
 
            <contentExtension
 
                  pattern="example.navigatorContent">
 
            </contentExtension>
 
        </includes>
 
      </viewerContentBinding>
 
  </extension>
 
</code>
 
 
 
 
 
====Adding a filter to the navigator====
 
To add a custom filter you have to use the <code>org.eclipse.ui.navigator.navigatorContent</code> extension. There you add a new commonFilter. You can either provide an implementation for <code>ViewerFilter</code> or use xml filterExpressions. For more information read the extension point description of [http://help.eclipse.org/help32/index.jsp?topic=/org.eclipse.platform.doc.isv/reference/extension-points/org_eclipse_ui_navigator_navigatorContent.html navigatorContent]. Finally include your commonFilter in your viewerContentBindings.
 
 
 
====Adding an action provider to the navigator====
 
To add a custom filter you use again the <code>org.eclipse.ui.navigator.navigatorContent</code> extension. There you add a new actionProvider. You have to provide an implementation for <code>org.eclipse.ui.navigator.CommonActionProvider</code>. To decide on what nodes in the tree your action provider should be invoked, use the enablement expression. Finally include your commonFilter in your viewerActionBindings.
 
 
 
====Adding a tab with custom content to the details part====
 
To add a custom tab use  the <code>fr.systerel.explorer.masterDetails</code> extension. Add a new detailsTab and provide a class that implements <code>INavigatorDetailsTab</code>.
 
  
[[Category:Work in progress]]
+
[[Category:User documentation]]
 +
[[Category:Design]]

Latest revision as of 18:35, 26 March 2010

Purpose

The Rodin platform, at the beginning of the Deploy project, provided two views for displaying models and proofs:

  • The Project Explorer displays the modelling elements stored in the Rodin database.
  • The Obligation Explorer displays the proof obligations together with their proof state.

The clean separation between modelling and proving looked good during paper design. However, users reported that they were constantly switching between the two views. This is due to the fact that modelling and proving are not separate activities, one being performed after the other. In general practice, both activities are intertwined.

Independently, Eclipse has released a new framework called the Common Navigation Framework since these two views were designed and implemented. The purpose of this framework is to provide Eclipse plug-ins with basic blocks for easily implementing views like the Project Explorer. Moreover, this framework allows various plug-ins to cooperate together in populating such views, thus reinforcing plug-in integration into the platform.

Therefore, it was decided in the Deploy project to combine the two original views into a single one that would display modelling elements and proof obligations together. This new single view should also take advantage of the Common Navigation Framework, in order to improve its seamless integration within Eclipse.

Specification

The Single View Design uses the Common Navigator Framework that is provided by Eclipse.

The Navigator

The navigator contains a tree of all projects and their contents. The users can choose between two ways how the machines and contexts will be presented:

  • A simple structure where all machines and contexts are presented on the same level
  • A complex structure where the machines and contexts are presented as a tree. Thus dependencies between machines and contexts (like refines or sees) are made visible.

The Statistics

The statistics view presents information about the state of the proof obligations of the selected node in the navigator.

User guide

Customizing the Navigator

Click on the little triangle in the upper right corner of the navigator view and select Customize View. This opens a dialog that allows you to choose Filters and Content.

Customize.jpg

Content

Here you can choose what content should be shown in the navigator.

  • Resources: All projects, files and folder (keep this one checked!).
  • Working Sets: Allows you to see the working sets as top level elements. If you're not familiar with working sets, consult eclipse help.
  • Simple Context Structure: Lists all contexts of a project.
  • Complex Context Structure: Lists all contexts of a project. Contexts that extend another context are attached to it as children in the tree. Contexts that are seen by a machine are attached to the machine as children. Choose either the complex or the simple structure. It is not recommended to have both active at the same time.
  • Simple Machines Structure: Lists all machines of a project.
  • Complex Context Structure: Lists all machines of a project. Machines that refine another machine are attached to it as children in the tree. Choose either the complex or the simple structure. It is not recommended to have both active at the same time.
  • Carrier Sets
  • Constants
  • Variables
  • Axioms
  • Invariants
  • Events
  • Proof Obligations: All proof obligations of a machine, context, axiom, invariant, derived invariant or event.

Here is an example of what the same project looks like when using the complex machine and context structure (left) and when using the simple version (right).

Complex.jpgSimple.jpg

Filters

The filters let you choose what to hide in the navigator.

  • File types: There are various filters to hide certain types of files.
  • All files and folders: Hides all files and subfolders.
  • Non Rodin Projects: Hides all non Rodin projects. Also hides closed Rodin Projects.
  • Closed Projects: Hides all closed projects.

There are some additional filters that can be found on top of the navigator:

PoFilters.JPG

Enter a text into the field and only proof obligations containing the string will be shown. If you push the green button, all discharged proof obligations will be hidden.

Statistics

The content displayed in the statistics view depends on the selection in the navigator. Generally it shows an overview of the status of all proof obligations of the selected elements and a more detailed view below (if available). If a project is selected this means that in the overview the statistics for all proof obligations of that project are shown. In the detailed viewed each machine and context is listed with their own statistics. If you double click on an element in the detailed view, the corresponding element will be selected in the navigator.

It is possible to select multiple elements in the navigator and get a combined statistics. But the selected elements must be on the same level (e.g. projects, machines/contexts). This mean if you select both machines and projects at the same time, you won't get any statistics.

See Also