Difference between revisions of "Single View Design"

From Event-B
Jump to navigationJump to search
imported>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 projects will be presented:
+
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

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.