Difference between pages "UML-B Tutorial" and "Rodin Platform 3.6 Release Notes"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Colin
 
 
Line 1: Line 1:
Return to [[UML-B]]
+
{{TOCright}}
  
The tutorial assumes you have downloaded and installed the Rodin platform and then installed the UML-B plug-in extension feature.  
+
== What's New in Rodin 3.6? ==
  
See http://www.event-b.org/platform.html and  http://www.event-b.org/plugins.html for installation instructions
+
Rodin 3.6 brings several bug fixes. It also upgrades the underlying Eclipse to 2020-12, which can be run by Java 11 Runtimes.
  
 +
Please note that we only provide 64-bit binary versions of the Rodin platform.
  
Getting Started
+
=== Changes for plug-in developers ===
  
1. Start Rodin by clicking on rodin.exe and selecting a suitable workspace.
+
Rodin 3.6 is built on top of Eclipse 4.18 (2020-12), which requires Java 11.
  
2. '''Open the UML-B perspective'''
+
There is no API change within Rodin Core.
        a. Click on: Window → Open Perspective → Other…
 
        b. Select UML-B and click OK
 
  
3. '''Open a new UMLB project'''
+
== Installing ==
        a. File → New → Project
 
        b. Select UML-B Project → Next
 
[[Image:UMLBSelectNewProjectType.jpg]]
 
        c. Enter a name for your project and click Finish
 
        d. The UML-B new project wizard, automatically creates and opens a package diagram ready for you to start modelling
 
[[Image:UMLBBlankPackageDiagram.jpg]]
 
  
''Note that the icon, top right, shows that you are in the UML-B perspective''
+
=== Downloading ===
  
 +
[http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.6/ Download Rodin 3.6 now !]
  
Specification:  A person can go to bed and sleep. After at least one hour, an alarm can be sounded which is waking the person. The person should then get up. A person has a maximum number of hours of sleep after which the person will get up without the alarm being sounded.
+
=== Upgrading from a previous version of Rodin 3.x ===
  
'''Package Diagram'''
+
If you run Rodin 3.1, 3.2, 3.3, 3.4 or 3.5, then you can upgrade your Rodin Platform by clicking Help > Check for Updates, then select Rodin 3.6 in the popup window and accept the licence terms. Note that the upgrading process can take quite a long time.
  
In the package diagram editor, '''create a machine that sees a context'''.
+
Take care that Rodin 3.6 brings a new version of Eclipse. This means that once you have opened a workspace with Rodin 3.6, you will not be able to open it with a prior version of Rodin anymore. Please consider copying your workspace for Rodin 3.6 to avoid any disaster.
        a. Create a machine: click on “machine” in the palette and click in the package diagram space, then name your machine.
 
                (You can enter the name on the text field of the diagram element. Alternatively you can edit any element properties in the Properties tab).
 
        b. Create a context: click on “context” in the palette and click in the package diagram space, then name your context
 
        c. Click on “Sees” in the palette and create a link from your machine to the context
 
        d. Click save
 
[[Image:UMLBSleepyPackageDiagram.jpg]]
 
  
 +
If you run Rodin 3.0 or prior, you cannot upgrade to 3.6. You need to download the platform from SourceForge and reinstall your external plugins.
  
'''Context Diagram'''
+
== Requirements - Compatibility ==
 
'''Open the context diagram'''
 
        a. Highlight  the context diagram box in your package diagram
 
        b. In the properties tab click on “open context diagram…”
 
  
'''Create an enumerated type.''' We need three states: awake, asleep and waking. These are elements of an enumerated set WAKE_STATE.
+
=== Supported operating systems ===
        a. Click on “class type” in the palette and click into the context diagram space
 
        b. In the properties tab, type a name “WAKE_STATE” for your class type → press enter
 
              ''(DO NOT enter the name of the class type in the diagram, use the properties tab to enter all data)''
 
        c. In the properties tab, click “add new type” in order to define the enumerated set
 
[[Image:UMLBAwakeStateEnumeratedSet.jpg]]
 
        d. Type “{awake, asleep, waking}” into the Name field of the type expression dialog → OK
 
        e. In the properties tab, select the type {awake, asleep, waking} from the “instances” drop-down menu
 
  
'''Create a constant'''  which holds the maximum number of hours a person may sleep.
+
Rodin will work on the following operating systems
        a. Select “constant” from the palette and click into the context diagram space
+
* macOS 64-bit
        b. In the properties tab, type a name “maxHours” for your constant and give it the type “N” (where “N” = NAT is the symbol representing natural numbers).
+
* Linux 64-bit
        c. Save the context diagram
+
* Windows 64-bit
[[Image:MaxhoursConstant.jpg]]
 
  
'''Create/Open a Class Diagram''' for the machine
+
=== Java Runtime requirement ===
  
''The class diagram models the dynamic behaviour of the system.''
+
You need to have a 64-bit Java JRE (version 11 or later) installed on your computer. The Rodin application will not work with a previous version or with a 32-bit JRE.
        a. Open the package diagram (either select the tab, or find it in the navigator)
 
        b. Highlight the machine in the package diagram
 
        c. In the properties tab, click “open class diagram…”
 
  
''The model only requires one class in the class diagram. This class, person, will require two variables, “hoursOfSleep”, which tracks the amount of hours a person has slept, and “wakeState”, which records the current state of that person. The model also needs several events to manipulate the state. These are;  “goToBed” (to set the wakeState of a person to asleep), “addMoreSleep” (to add another hour of sleep to the person’s hoursOfSleep count), “soundAlarm” (to wake up a person and set the wakeState of that person to waking) and “getUp” (to set the person’s wakeState to awake).''
+
=== macOS specific requirements ===
  
'''Create a class.'''
+
The Rodin application is not notarized. This means that when you download it from SourceForge, macOS will quarantine the application and tell you that it is brokenJust run the command <code>xattr -rc Rodin.app</code> in a Terminal to remove the quarantine tag.
        a. Select “class” in the palette and click into the class diagram space
 
        b. In the properties tab, enter a name for your class “person”
 
[[Image:UMLBPersonClass_creating.jpg]]
 
        c. Move your mouse over the class in the class diagram, and select “add attribute” from the menu that pops up. (You could also use the tool palette).
 
[[Image:UMLBaddAttributeFromPopUp.jpg]]
 
        d. In the properties tab, enter the name “hoursOfSleep”, the type “N” and the initial value “0” of your attribute.
 
[[Image:UMLBHoursOfSleepAttribute_settingProperties.jpg]]
 
        e. Add another attribute to the class, and name it “wakeState”, type “Class Type WAKE_STATE” (this will use the enumerated set you created in the context diagram) and initial value “awake”.
 
[[Image:UMLBWakeStateAttribute.jpg]]
 
   
 
'''Add a constructor event to the class''', (this will add and initialise instances of the class).
 
        a. Add an event to the class “person” (either use the pop-up menu or the palette).
 
        b. In the properties tab, enter a name for the person “CreatePerson”
 
        c.    Select “constructor” in the “kind” drop-down menu.
 
[[Image:CreatePersonConstructor.jpg]]
 
 
'''Add an event''' to the class.
 
        a. Add another event to the class person
 
        b. Enter the name “goToBed” in the properties tab
 
        c. Select “guards” in the properties tab and “add guard…”
 
        d. In the guard field enter “wakeState(self) = awake” (we only want to put persons into bed that are awake) → OK.
 
''Note that you could also enter “self,.wakeState = awake” (the character pair ,. is converted to a special dot symbol). This gives a more object oriented style for guards and actions but is not as easy to relate to proof goals in the Event-B prover.''
 
  
[[Image:UMLBGoToBed.jpg]]
+
=== Linux specific requirements ===
        e. Select “actions” in the properties tab and “add action…”
 
        f. In the action field enter “wakeState(self) := asleep”  → OK
 
        g. Add another action and enter: “hoursOfSleep(self) := 0”
 
        h. Save your class diagram
 
  
Add the next three events to complete the model.
+
Package <code>libc6-amd64:i386</code> must be installed, in particular in order to run external prover binaries depending on the distribution, you could instead need these packages: <code>lib32z1</code>, <code>lib32ncurses5</code>, <code>lib32bz2-1.0</code>.
  
The event “addMoreSleep” adds another hour of sleep to the person’s sleep count. The person may, however, not sleep more than the maximum hours of sleep allowed.
+
=== Windows specific requirements ===
        a. Add another event to class person
+
Atelier B provers may work more slowly; it can cause ML to not automatically discharge some sequents that it discharges on windows 32-bit, due to its timeout. A workaround is to download a custom profile: [http://sourceforge.net/projects/rodin-b-sharp/files/DefaultAuto_ML800 DefaultAuto_ML800], then Window > Preferences > Event-B > Sequent Prover > Auto/Post Tactic > Profiles (tab) > Import..., point to the downloaded file, 'Select All' profiles (there are 2), OK. Then in 'Auto/Post Tactic' tab, select 'Default Auto Tactic Profile (ML 800)' profile for auto-tactics. It is the same as the 'Default Auto Tactic Profile', except ML has a longer timeout (800 ms). You can of course change this timeout by editing the 'ML (800)' profile.
        b. In the properties tab, enter the name “addMoreSleep” → press enter
 
        c. Add two guards: “wakeState(self) = asleep” and “hoursOfSleep(self) < maxHours”
 
        d. Add one action: “hoursOfSleep(self) := hoursOfSleep(self) + 1”
 
The event “soundAlarm” is used to wake up a person who has slept for at least one hour, and has not slept the maximum amount of hours.
 
        a. Add another event to class person
 
        b. Enter name: “soundAlarm”
 
        c. Add guards: “wakeState(self) = asleep”, “hoursOfSleep(self) > 0” and “hoursOfSleep(self) < maxHours”
 
        d. Add action: “wakeState(self) := waking”
 
The event “getUp”, will set the person’s wakeState to awake. It should be enabled when the person was woken by the alarm, i.e. is in a waking state or if the maximum hours of sleep have been reached.
 
        a. Add another event to class person
 
        b. Enter name: “getup”
 
        c. Add guard: (wakeState(self) = waking) or (wakeState(self) = asleep & hoursOfSleep(self) ≥ maxHours)
 
        d.   Add actions: "wakeState(self) := awake"  and  "hoursOfSleep(self) :=0"
 
        e. Save the class diagram.
 
  
''An alternative way to model this same specification using statemachines is given below.''
+
We have not noticed this problem for Linux 64-bit, nor for other platforms; however if you do, the same workaround applies.
 
'''View the generated Event-B'''
 
  
To view the generated Event-B context and machine, open the xxx.eventB folder (where xxx stands for the name of your project). You will see a long list of files. (You could switch to the Event-B perspective, which will filter the files in the Navigator to show the ones you can open). In order to view your context, double click on xxx.buc; for the machine click on xxx.bum. You will see several tabs at the bottom, select “Pretty Print” to view the generated eventB.
+
=== Math fonts ===
  
''If you want to experiment with the Event-B tools, you can edit the Event-B model in this view. However, any changes you make will not be fed back to the UML-B source models, so if you alter the UML-B model your Event-B edits will be overwritten and lost.''
+
To enhance your proving experience, the eclipse font settings (size, aspect...) are available from the preferences (General > Appearance > Colors and Fonts > Rodin). These settings allow you to modify the properties set on the Event-B Keyboard Text Font which is used in many views of the Proving UI. However, to enjoy these functionalities, you need to install the Brave Sans Mono font on your system. You can download this font from the link [http://sourceforge.net/projects/rodin-b-sharp/files/Font_%20Brave%20Sans%20Mono/0.12/ here].
  
[[Image:UMLBViewEventB.jpg]]
+
== 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 ensure 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].
'''Creating the Sleepy Model using Statemachines'''
 
  
''Statemachines provide an alternative way to model behaviour. This section shows how a statemachine could be used to replace some of the data, state variables and events of the previous model. If you use a different UML-B project name you can compare the generated Event-B from the two models.''
+
== About ==
  
'''Context Diagram.'''
+
Rodin Platform with git commit: <code>77c3449</code><br/>
 +
User Release date : 2021/05/17.
  
''The context of this model does not contain the enumerated set WAKE_STATE, because those states are generated by UML-B automatically from the statemachine.''
+
[[Category:Rodin Platform Release Notes]]
 
 
The context consists of only one constant maxHours.
 
        a. In the context diagram, create one constant (name: maxHours; type: N)
 
 
'''Class Diagram'''
 
 
 
''The class diagram consists of one class, “person”, which has one attribute “hoursOfSleep” to track the amount of hours a person has slept.''
 
 
 
Add a class, 'person' with attribute, 'hoursOfSleep'
 
        a. In the class diagram, create a class (name: person)
 
        b. Add an attribute to the class (name: hoursOfSleep; type: N; initial value: 0)
 
 
 
''This time, the events will be created using a statemachine.''
 
 
 
'''Add a class statemachine'''
 
        a. Select C Statemachine from the palette and click in the 'statemachines' compartment of class “person”
 
        b.    Name the statemachine, "wakeState"
 
[[Image:UMLBWakeStateStatemachine_creating.jpg]]
 
 
 
''Note: Two alternative translations of statemachines are provided. To change to the other translation,  change the 'Translation' property in the properties view.''
 
        c. Click “Open StateDiagram…”
 
 
'''Add states to the statemachine'''
 
        a. From the palette select state and create a state (name: awakeState)
 
        b. Do the same for the other two states: asleepState, wakingState
 
        c. Create an initial state (it doesn't need a name).
 
 
 
'''Add transitions between states.'''
 
 
 
''State transitions represents events''
 
        a. Create transitions to match the diagram  below
 
[[Image:UMLBWakeStateStatemachine_detail.jpg]]
 
        b. Add the following detail to the  different transitions.
 
[[Image:UMLBWakeUpByYourselfTransition_details.jpg]]
 
[[Image:UMLBAddMoreSleepTransition_details.jpg]]
 
[[Image:UMLBSoundAlarmTransition_details.jpg]]
 
        c.    Save the model and view the Event-B as before.
 
 
 
''Note: Two alternative translations of statemachines are provided. To change to the other translation, select the statemachine (either click on the canvas of the statemachine diagram or click on the statemachine in the class diagram) and change the 'Translation' property in the properties view.''
 
 
 
[[Category:User documentation]]
 
[[Category:UML-B]]
 
[[Category:Tutorial]]
 

Latest revision as of 14:09, 25 May 2021

What's New in Rodin 3.6?

Rodin 3.6 brings several bug fixes. It also upgrades the underlying Eclipse to 2020-12, which can be run by Java 11 Runtimes.

Please note that we only provide 64-bit binary versions of the Rodin platform.

Changes for plug-in developers

Rodin 3.6 is built on top of Eclipse 4.18 (2020-12), which requires Java 11.

There is no API change within Rodin Core.

Installing

Downloading

Download Rodin 3.6 now !

Upgrading from a previous version of Rodin 3.x

If you run Rodin 3.1, 3.2, 3.3, 3.4 or 3.5, then you can upgrade your Rodin Platform by clicking Help > Check for Updates, then select Rodin 3.6 in the popup window and accept the licence terms. Note that the upgrading process can take quite a long time.

Take care that Rodin 3.6 brings a new version of Eclipse. This means that once you have opened a workspace with Rodin 3.6, you will not be able to open it with a prior version of Rodin anymore. Please consider copying your workspace for Rodin 3.6 to avoid any disaster.

If you run Rodin 3.0 or prior, you cannot upgrade to 3.6. You need to download the platform from SourceForge and reinstall your external plugins.

Requirements - Compatibility

Supported operating systems

Rodin will work on the following operating systems

  • macOS 64-bit
  • Linux 64-bit
  • Windows 64-bit

Java Runtime requirement

You need to have a 64-bit Java JRE (version 11 or later) installed on your computer. The Rodin application will not work with a previous version or with a 32-bit JRE.

macOS specific requirements

The Rodin application is not notarized. This means that when you download it from SourceForge, macOS will quarantine the application and tell you that it is broken. Just run the command xattr -rc Rodin.app in a Terminal to remove the quarantine tag.

Linux specific requirements

Package libc6-amd64:i386 must be installed, in particular in order to run external prover binaries depending on the distribution, you could instead need these packages: lib32z1, lib32ncurses5, lib32bz2-1.0.

Windows specific requirements

Atelier B provers may work more slowly; it can cause ML to not automatically discharge some sequents that it discharges on windows 32-bit, due to its timeout. A workaround is to download a custom profile: DefaultAuto_ML800, then Window > Preferences > Event-B > Sequent Prover > Auto/Post Tactic > Profiles (tab) > Import..., point to the downloaded file, 'Select All' profiles (there are 2), OK. Then in 'Auto/Post Tactic' tab, select 'Default Auto Tactic Profile (ML 800)' profile for auto-tactics. It is the same as the 'Default Auto Tactic Profile', except ML has a longer timeout (800 ms). You can of course change this timeout by editing the 'ML (800)' profile.

We have not noticed this problem for Linux 64-bit, nor for other platforms; however if you do, the same workaround applies.

Math fonts

To enhance your proving experience, the eclipse font settings (size, aspect...) are available from the preferences (General > Appearance > Colors and Fonts > Rodin). These settings allow you to modify the properties set on the Event-B Keyboard Text Font which is used in many views of the Proving UI. However, to enjoy these functionalities, you need to install the Brave Sans Mono font on your system. You can download this font from the link here.

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 ensure 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 with git commit: 77c3449
User Release date : 2021/05/17.