Single View Design

From Event-B
Revision as of 15:57, 22 September 2008 by imported>Maria
Jump to navigationJump to search

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 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.