Single View Design: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Maria No edit summary |
imported>Maria No edit summary |
||
Line 11: | Line 11: | ||
There's a number of content providers to choose from: | There's a number of content providers to choose from: | ||
*Projects: This content provider shows all open rodin projects. Closed projects are currently not shown. If this content provider is not selected the navigator is empty. | *Projects: This content provider shows all open rodin projects. Closed projects are currently not shown. If this content provider is not selected the navigator is empty. | ||
*Simple Machine and Context Structure: This shows all machines and contexts in a simple way. | *Simple Machine and Context Structure: This content provider shows all machines and contexts in a simple way. | ||
*Complex Machine and Context Structure: This shows all machines and contexts in a complex way (dependencies made visible). | *Complex Machine and Context Structure: This content provider shows all machines and contexts in a complex way (dependencies made visible). | ||
*Invariants, Events etc: There's a content provider for each of those elements. It shows all invariants (or any other chosen type) of a machine. | *Invariants, Events etc: There's a content provider for each of those elements. It shows all invariants (or any other chosen type) of a machine. | ||
*Proof Obligations: This content provider shows all Proof Obligations. | *Proof Obligations: This content provider shows all Proof Obligations. |
Revision as of 15:57, 22 September 2008
Purpose
The Purpose of the Single View Design is to present everything in a single view in Rodin.
Specification
The navigator presents all projects and their contents. The users can choose between to 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 Content Providers
There's a number of content providers to choose from:
- Projects: This content provider shows all open rodin projects. Closed projects are currently not shown. If this content provider is not selected the navigator is empty.
- Simple Machine and Context Structure: This content provider shows all machines and contexts in a simple way.
- Complex Machine and Context Structure: This content provider shows all machines and contexts in a complex way (dependencies made visible).
- Invariants, Events etc: There's a content provider for each of those elements. It shows all invariants (or any other chosen type) of a machine.
- Proof Obligations: This content provider shows all Proof Obligations.
The Actions
The following actions are available in the navigator:
- Projects: Delete, Rename, Copy
- Machines: Delete, Rename, Refine, Prove interactively
- Contexts: Delete, Extend, Prove interactively
- Proof Obligations: Retry Auto Provers, Recalculate Auto Status
- Globally: New Project, New Component
On double click each element is opened in an editor.
The Filters
The following filters are available in the navigator:
- A filter that hides discharged proof obligations.
- A filter that hides all proof obligations that don't contain a given string in their name.