Difference between revisions of "Single View Design"
From Event-B
Jump to navigationJump to searchimported>Maria |
imported>Maria |
||
Line 4: | Line 4: | ||
==Specification== | ==Specification== | ||
===The Navigator=== | ===The Navigator=== | ||
− | The navigator presents all projects and their contents. The users can choose between to ways how the | + | 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 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 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. | ||
+ | |||
+ | |||
[[Category:Work in progress]] | [[Category:Work in progress]] |
Revision as of 13:24, 18 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 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.