Difference between pages "Event-B Statemachines" and "Rodin Platform 2.1.1 Release Notes"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Vitaly
(New page: frame|left ==Overview== Event-B Statemachines Plug-in is part of the iUML-B experimental tool that focuses on UML-B and Event-B integration. The plug-in provides ...)
 
imported>Nicolas
 
Line 1: Line 1:
−
[[Image:IUMLB_big.png|frame|left]]
+
{{TOCright}}
  
−
==Overview==
+
Rodin 2.1.1 is a maintenance release: as such, it contains only bug fixes. For more information, see [[Rodin_Platform_2.1_Release_Notes]].
  
−
Event-B Statemachines Plug-in is part of the iUML-B experimental tool that focuses on UML-B and Event-B integration. The plug-in provides a way of adding state machines directly to Event-B machines and is capable of translating former to Event-B language. It also offers a UML-like diagram editor for state machines, as well as state machine animation, which can be installed as additional plug-in that runs on top of ProB Animator.
+
== What's New in Rodin 2.1.1 ? ==
  
−
==Installation==
+
* Fixed bugs:
 +
** ArrayIndexOutOfBoundsException during a build
 +
** IndexOutOfBoundsException when building a theory (with [[Theory_Plug-in|Theory Plug-in]] installed)
 +
** Auto-tactic profile preference bugs
 +
** Various UI bugs (prover interface, rule details, tactic profiles) including, in particular, a fix for slow hypothesis search on Windows OS.
  
−
The Event-B Statemachines plug-in is available for installation from Rodin update site under Modelling Extensions category. Animation plug-in for it is available from Verification and Validation category. Both plug-ins require EMF and GMF frameworks, Event-B EMF framework, ProB, OCL and QVT - all of these dependencies will be installed automatically upon plug-in installation.
+
* Changes for plugin-developers
 +
:None
  
−
==Using the tool==
+
== Installing ==
  
−
The tool consists of a standard UML-like graphical editor for state machine diagrams, and integration to Event-B Explorer and a translator to Event-B language. Some of these may seem familiar to you if you have experience with UML editors or UML-B plug-in for Rodin.
+
Users who are already running Rodin 2.1 are encouraged to perform an upgrade, as described below. The upgrade is faster, smaller (the archive is about 6 MB) and simpler than downloading a whole new platform: no need to reinstall plug-ins or configure the platform from scratch.  
  
−
====Event-B Explorer====
+
=== Upgrading from Rodin 2.1 ===
  
−
[[Image:New_statemachine.png|thumbnail|State machine in Event-B Explorer]]
+
* download archive [http://sourceforge.net/projects/rodin-b-sharp/files/Core_%20Rodin%20Platform/2.1.1/rodin-2.1.1-repo.zip/download rodin-2.1.1-repo.zip]
 +
* launch Rodin 2.1
 +
* Help > Install New Software... > Add... > enter a name (for instance "Rodin 2.1.1") then
 +
: Archive... > select the rodin-2.1.1-repo.zip archive
 +
: Mac users may have to use Local... then point to archive root directory, in case the archive was automatically unzipped
 +
* set options in the bottom of the page:
 +
:* check
 +
:** "Show only the latest versions of available software"
 +
:** "Hide items that are already installed"
 +
:* uncheck
 +
:** "Group items by category"
 +
:** "Contact all update sites..."
 +
: the central area should now list 5 entries
 +
* select "Rodin Platform", click "Next"
 +
: a message informs "Your original request has been modified.  See the details."
 +
: "Rodin Platform" is already installed, so an update will be performed instead.
 +
* click Next, accept license, finish and restart
  
−
To start the modelling all you have to do is to select a machine in Event-B Explorer that you would like to extend with state machines and click on ''Create new statemachine'' from explorer's toolbar. An input dialog will appear asking you for name of a new state machine. After that you should be able to see a new state machine appearing as a child of machine in explorer.
+
=== Downloading ===
  
−
The explorer also shows the contents of state machines, including states, transitions and annotations. You can customise the amount if information you would like to see by going to explorer's menu (a small triangle at the top right-hand side) ''> Customize View.. > Filters'' tab. There are three filters defined for state machines: ''Annotation Filter, Transition Filter, State Filter'' - that hide corresponding elements in explorer (state filter hides simple states, like initial, final or ANY).
+
[http://sourceforge.net/projects/rodin-b-sharp/files/Core_%20Rodin%20Platform/2.1.1/ http://sourceforge.net/projects/rodin-b-sharp/files/Core_ Rodin Platform/2.1.1/]
  
−
In addition, there are ''Open'' and ''Delete'' actions available for state machine in context menu of explorer. These allow to open a state machine in editor (shortcut is double-click) and delete a state machine (shortcut is Delete key). In the machine context menu there are two more actions related to state machines: ''Refine with statemachines'' and ''Delete generated'' - which allow correspondingly to create a refinement of machine with state machine refinements (not available yet from standard ''Refine'' action of Rodin) and to delete all Event-B elements generated by state machines (required only for experimental purposes if generated things/diagrams get corrupted).
+
== Disclaimer ==
 +
Since Rodin is continuously maintained, several unsoundness bugs which have been encountered were investigated and fixed. However, despite the total commitment of our teams to insure the soundness of the platform, some unexpected and unknown soundness issues could remain. We would be grateful if you would report these issues to the [mailto:rodin-b-sharp-devel@lists.sourceforge.net development mailing list].
  
−
====Diagram Editor====
+
== About ==
 +
Rodin Platform from release branch: branches/RodinCore/2.1.1 r10985
  
−
[[Image:Statemachine editor.png|thumbnail|left|State machine diagram editor]]
+
Made of Rodin 2.1 plus following trunk revisions (change log available in SourceForge downloads):
 +
10768; 10800; 10801; 10806; 10807; 10860; 10861; 10863; 10870; 10872; 10876; 10877; 10880; 10879; 10915; 10916; 10940
  
−
To edit a state machine in diagram editor you simply double-click it. The tool creates a diagram file for you with the same name as root state machine.
 
  
−
Working with the editor is straightforward. The element creation tools are available from palette, divided into three categories: ''States'', ''State Features'' and ''State Links''. When a diagram element is selected on canvas the Properties View shows its available properties (if you cannot find it, please go to Rodin's menu ''Window > Show View > Properties''). After a state machine is complete it can be validated to make sure it has no semantic errors and translated to Event-B. When translated, it can be animated with ProB.
+
Developer Release date : 11/03/2011.
 +
User Release date : 15/03/2011.
  
−
 
+
[[Category:Rodin Platform Release Notes]]
−
 
 
−
 
 
−
 
 
−
 
 
−
 
 
−
 
 
−
 
 
−
 
 
−
=====Elements=====
 
−
 
 
−
The diagram allows to create the following ''State'' elements:
 
−
* State
 
−
* Refined State (shall not be used)
 
−
* Initial (state)
 
−
* Final (state)
 
−
* ANY (state)
 
−
 
 
−
A state can have nested state machines, added from ''State Features'', which correspond to UML parallel substates, also called parallel (or orthogonal) regions.
 
−
 
 
−
Finally, states can have transitions from one to another, created from ''State Links''. Transitions can also be created from popup arrows on states and link to either existing states or to ones created from the context menu.
 
−
 
 
−
=====Context Menu=====
 
−
 
 
−
The context menu of a diagram includes four specific actions:
 
−
* ''Validate'' - to run the validation check on state machine model
 
−
* ''Translate to Event-B'' - to run the translation of state machine to Event-B language
 
−
* ''Start Animation'' - to run ProB animation and animate the diagram
 
−
* ''Stop Animation'' - to stop the animation and return to Event-B perspective
 
−
 
 
−
[[Category:Plugin]] [[Category:User documentation]]
 

Revision as of 14:59, 17 March 2011

Rodin 2.1.1 is a maintenance release: as such, it contains only bug fixes. For more information, see Rodin_Platform_2.1_Release_Notes.

What's New in Rodin 2.1.1 ?

  • Fixed bugs:
    • ArrayIndexOutOfBoundsException during a build
    • IndexOutOfBoundsException when building a theory (with Theory Plug-in installed)
    • Auto-tactic profile preference bugs
    • Various UI bugs (prover interface, rule details, tactic profiles) including, in particular, a fix for slow hypothesis search on Windows OS.
  • Changes for plugin-developers
None

Installing

Users who are already running Rodin 2.1 are encouraged to perform an upgrade, as described below. The upgrade is faster, smaller (the archive is about 6 MB) and simpler than downloading a whole new platform: no need to reinstall plug-ins or configure the platform from scratch.

Upgrading from Rodin 2.1

  • download archive rodin-2.1.1-repo.zip
  • launch Rodin 2.1
  • Help > Install New Software... > Add... > enter a name (for instance "Rodin 2.1.1") then
Archive... > select the rodin-2.1.1-repo.zip archive
Mac users may have to use Local... then point to archive root directory, in case the archive was automatically unzipped
  • set options in the bottom of the page:
  • check
    • "Show only the latest versions of available software"
    • "Hide items that are already installed"
  • uncheck
    • "Group items by category"
    • "Contact all update sites..."
the central area should now list 5 entries
  • select "Rodin Platform", click "Next"
a message informs "Your original request has been modified. See the details."
"Rodin Platform" is already installed, so an update will be performed instead.
  • click Next, accept license, finish and restart

Downloading

http://sourceforge.net/projects/rodin-b-sharp/files/Core_ Rodin Platform/2.1.1/

Disclaimer

Since Rodin is continuously maintained, several unsoundness bugs which have been encountered were investigated and fixed. However, despite the total commitment of our teams to insure the soundness of the platform, some unexpected and unknown soundness issues could remain. We would be grateful if you would report these issues to the development mailing list.

About

Rodin Platform from release branch: branches/RodinCore/2.1.1 r10985

Made of Rodin 2.1 plus following trunk revisions (change log available in SourceForge downloads): 

10768; 10800; 10801; 10806; 10807; 10860; 10861; 10863; 10870; 10872; 10876; 10877; 10880; 10879; 10915; 10916; 10940


Developer Release date : 11/03/2011. User Release date : 15/03/2011.

Retrieved from ‘https://wiki.event-b.org/index.php?title=Event-B_Statemachines&oldid=7567’