ProB2-UI: Difference between revisions

Latest revision as of 12:52, 7 May 2026

ProB2-UI is the new Java-based user interface for ProB.

Download

Download the latest version of ProB2-UI here. See also the release history.

The source code for ProB2-UI is available at https://github.com/hhu-stups/prob2_ui and can be built by following these instructions.

Features

Compared to the original UI based on Tcl/Tk, this new UI has some unique new features:

Projects which store formal models, ProB preferences, and verification settings
Load Rodin models from Rodin workspaces (without having to export them within Rodin)
Managing and storing multiple trace files for a model, being able to replay all traces
MC/DC test-case generation
A view for managing LTL formulas for a model
Visualisation of models using VisB and SVG graphics
An integrated view for all dot-based graph visualisations (state space, machine hierarchy, formulas, projection diagrams, enabling graphs, event refinement hierarchy, ....)
An integrated view to access all table based statistics (event coverage, MC/DC coverage, read-write matrices, WD POs, ...)
A multi-language interface, currently providing English, French, German and Russian

We have developed a small video highlighting the core features (also on YouTube) on a model the from visb-visualisation-examples:

<h2>Paper/Citing</h2> Paper: <a rel="nofollow" class="external text" href="https://link.springer.com/chapter/10.1007/978-3-030-85248-1_12">Springer Link</a>, <a rel="nofollow" class="external text" href="https://www.researchgate.net/publication/353989368_ProB2-UI_A_Java-Based_User_Interface_for_ProB">ResearchGate</a> BibTeX citation: <pre> @InProceedings{prob2ui, author="Bendisposto, Jens and Gele{\ss}us, David and Jansing, Yumiko and Leuschel, Michael and P{\"u}tz, Antonia and Vu, Fabian and Werth, Michelle", editor="Lluch Lafuente, Alberto and Mavridou, Anastasia", title="ProB2-UI: A Java-Based User Interface for ProB", booktitle="Formal Methods for Industrial Critical Systems", year="2021", publisher="Springer International Publishing", address="Cham", pages="193--201", abstract="ProB2-UI is a modern JavaFX-based user interface for the animator, constraint solver, and model checker ProB. We present the main features of the tool, especially compared to ProB's previous user interfaces and other available tools for B, Event-B, and other formalisms. We also present some of ProB2-UI's history as well as its uses in the industry since its release in 2019.", isbn="978-3-030-85248-1" } </pre> <h2>The ProB2-UI Main Window</h2> By default the main window is split into three vertical panes (see below). <ul><li>In the left pane, the Operations view , showing the operations whose preconditions and guards are true in this state (the view also uses a blue circular arrow icon when an operation does not change the state);</li> <li>In the middle the State View, containing the current state of the B machine, listing e.g., the current values of the machine variables;</li> <li>In the right pane there are a variety of subviews, which can be activated: <ul><li><a href="/w/index.php?title=History_View" title="History View">The History of operations leading to this state (History)</a></li> <li><a href="/w/index.php?title=Project_View" title="Project View">The Project view</a></li> <li><a href="/w/index.php?title=Verification_View" title="Verification View">The Verification view</a></li> <li><a href="/w/index.php?title=Statistics_View" title="Statistics View">The Statistics view</a></li></ul></li></ul> <a href="/w/index.php?title=File:ProB2JavaFX_UI_Overview_New.png" class="mw-file-description"><img src="/w/images/e/ee/ProB2JavaFX_UI_Overview_New.png" decoding="async" width="1000" height="502" class="mw-file-element" /></a> <h2>The ProB2-UI Main Menu Bar</h2> The menu bar contains the various commands to access the features of ProB. It includes the menus <ul><li>File,</li> <li>Edit,</li> <li>Formula,</li> <li>Consoles,</li> <li>Perspectives,</li> <li>View,</li> <li>Window and</li> <li>Help</li></ul> <figure class="mw-default-size mw-halign-none" typeof="mw:File"><a href="/w/index.php?title=File:File.png" class="mw-file-description"><img src="/w/images/b/b0/File.png" decoding="async" width="600" height="225" class="mw-file-element" /></a><figcaption></figcaption></figure> The File submenu allows you to create a new Project, open an existing project or a machine, open recent projects shown as list and/or clear the list of recent projects, close the ProB2-UI, save your project or reload the currently running machine. <figure class="mw-default-size mw-halign-none" typeof="mw:File"><a href="/w/index.php?title=File:Edit.png" class="mw-file-description"><img src="/w/images/d/d2/Edit.png" decoding="async" width="600" height="145" class="mw-file-element" /></a><figcaption></figcaption></figure> The Edit submenu provides two ways to edit the current machine (either in the editor provided by the ProB2-UI or in the your operating systems standard editor) and allows to edit your general and global preferences by opening a seperate window. <figure class="mw-default-size mw-halign-none" typeof="mw:File"><a href="/w/index.php?title=File:Formula.png" class="mw-file-description"><img src="/w/images/c/cf/Formula.png" decoding="async" width="600" height="145" class="mw-file-element" /></a><figcaption></figcaption></figure> Here you can add formulas for visualization and open the history chart window. <figure class="mw-default-size mw-halign-none" typeof="mw:File"><a href="/w/index.php?title=File:Consoles.png" class="mw-file-description"><img src="/w/images/3/37/Consoles.png" decoding="async" width="600" height="145" class="mw-file-element" /></a><figcaption></figcaption></figure> This submenu leads to two consoles, one Groovy, one B. <figure class="mw-default-size mw-halign-none" typeof="mw:File"><a href="/w/index.php?title=File:Perspectives.png" class="mw-file-description"><img src="/w/images/0/0f/Perspectives.png" decoding="async" width="600" height="145" class="mw-file-element" /></a><figcaption></figcaption></figure> The Perspectives submenu allows you to change the appearance of the main view. The default view is shown at the top and two additional perspectives (Seperated History and Seperated History and Statistics) are preset. By Detach Components the view can be shown in seperate windows. Load allows you to make your own perspective by providing an FXML file containing the views but be aware that this might ruin the ability to detach components. <figure class="mw-default-size mw-halign-none" typeof="mw:File"><a href="/w/index.php?title=File:View.png" class="mw-file-description"><img src="/w/images/9/98/View.png" decoding="async" width="600" height="145" class="mw-file-element" /></a><figcaption></figcaption></figure> This submenu allows you to adjust font and button size in the ProB2-UI. <figure class="mw-default-size mw-halign-none" typeof="mw:File"><a href="/w/index.php?title=File:Help.png" class="mw-file-description"><img src="/w/images/a/aa/Help.png" decoding="async" width="600" height="145" class="mw-file-element" /></a><figcaption></figcaption></figure> The Help submenu provides you with help about the ProB2-UI, information about the ProB2 UI, ProB2 kernel, ProB CLI and Java version used here and a way to report issues regarding the ProB2-UI.

@@ Line 1: / Line 1: @@
-== The ProB2 JavaFX Main Window ==
+'''ProB2-UI''' is the new Java-based user interface for ProB. __NOTOC__
+== Download ==
+'''[[Download#ProB2-UI|Download the latest version of ProB2-UI here]]'''. See also the [https://github.com/hhu-stups/prob2_ui/blob/develop/doc/prob2ui_release_history.md release history].
+The source code for ProB2-UI is available at https://github.com/hhu-stups/prob2_ui and can be built by following [https://github.com/hhu-stups/prob2_ui#running-from-source these instructions].
+== Features ==
+Compared to the original UI based on Tcl/Tk, this new UI has some unique new features:
+* Projects which store formal models, ProB preferences, and verification settings
+* Load Rodin models from Rodin workspaces (without having to export them within Rodin)
+* Managing and storing multiple trace files for a model, being able to replay all traces
+* MC/DC test-case generation
+* A view for managing LTL formulas for a model
+* Visualisation of models using [[VisB]] and SVG graphics
+* An integrated view for all dot-based graph visualisations (state space, machine hierarchy, formulas, projection diagrams, enabling graphs, event refinement hierarchy, ....)
+* An integrated view to access all table based statistics (event coverage, MC/DC coverage, read-write matrices, WD POs, ...)
+* A multi-language interface, currently providing English, French, German and Russian
+We have developed a small
+[https://media.hhu.de/video/prob2-ui-overview/732170cf5ca368239e104bb56e29d73a video highlighting the core features] (also on [https://youtu.be/HqTlr6y-hwk YouTube]) on a model the from [https://gitlab.cs.uni-duesseldorf.de/general/stups/visb-visualisation-examples visb-visualisation-examples]:
+<!-- Official embed URL, taken from the "twitter:player" meta tag on the video page. -->
+<!-- For some reason, the height parameter needs to be 10 pixels higher than the desired video height, and the iframe height needs to be 40 pixels higher still to prevent a vertical scrollbar in the iframe. -->
+<html>
+<iframe width="768" height="530" frameborder="0" allowfullscreen src="https://media.hhu.de/media/embed?key=732170cf5ca368239e104bb56e29d73a&width=768&height=490&autoplay=false&autolightsoff=false&loop=false&chapters=false&related=false&responsive=true"/>
+</html>
+<!-- Unofficial manual embed, with the URLs taken from the JS player on the video page. -->
+<!-- This seems to load much quicker than the official embed, and it has no size issues, but it doesn't allow changing the video resolution. -->
+<!--
+<html>
+<video controls width="768" height="480" preload="none" poster="https://media.hhu.de/cache/3d7afd0a1fbc75fe4fc76d0be294a852.png">
+<source src="https://media.hhu.de/getMedium/732170cf5ca368239e104bb56e29d73a.mp4?format=720p" type="video/mp4"/>
+</video>
+</html>
+-->
+== Paper/Citing ==
+Paper: [https://link.springer.com/chapter/10.1007/978-3-030-85248-1_12 Springer Link], [https://www.researchgate.net/publication/353989368_ProB2-UI_A_Java-Based_User_Interface_for_ProB ResearchGate]
+BibTeX citation:
+<pre>
+@InProceedings{prob2ui,
+author="Bendisposto, Jens
+and Gele{\ss}us, David
+and Jansing, Yumiko
+and Leuschel, Michael
+and P{\"u}tz, Antonia
+and Vu, Fabian
+and Werth, Michelle",
+editor="Lluch Lafuente, Alberto
+and Mavridou, Anastasia",
+title="ProB2-UI: A Java-Based User Interface for ProB",
+booktitle="Formal Methods for Industrial Critical Systems",
+year="2021",
+publisher="Springer International Publishing",
+address="Cham",
+pages="193--201",
+abstract="ProB2-UI is a modern JavaFX-based user interface for the animator, constraint solver, and model checker ProB. We present the main features of the tool, especially compared to ProB's previous user interfaces and other available tools for B, Event-B, and other formalisms. We also present some of ProB2-UI's history as well as its uses in the industry since its release in 2019.",
+isbn="978-3-030-85248-1"
+}
+</pre>
+== The ProB2-UI Main Window ==
@@ Line 6: / Line 75: @@
 * In the left pane, the Operations view , showing the operations whose preconditions and guards are true in this state (the view also uses a blue circular arrow icon when an operation does not change the state);
 * In the middle the State View, containing the current state of the B machine, listing e.g., the current values of the machine variables;
-* In the right pane there are a variety of subviews, which can be activate:
+* In the right pane there are a variety of subviews, which can be activated:
 ** [[History_View|The History of operations leading to this state (History)]]
 ** [[Project_View|The Project view]]
@@ Line 12: / Line 81: @@
 ** [[Statistics_View|The Statistics view]]
-[[File:ProB2JavaFX_UI_Overview.png||900px]]
+[[File:ProB2JavaFX_UI_Overview_New.png||1000px]]
-== The ProB2 JavaFX Main Menu Bar ==
+== The ProB2-UI Main Menu Bar ==
 The menu bar contains the various commands to access the features of ProB. It includes the menus
 *File,
@@ Line 24: / Line 93: @@
 *Window and
 *Help
+[[File:File.png|none]]
+The File submenu allows you to create a new Project, open an existing project or a machine, open recent projects shown as list and/or clear the list of recent projects, close the ProB2-UI, save your project or reload the currently running machine.
+[[File:Edit.png|none]]
+The Edit submenu provides two ways to edit the current machine (either in the editor provided by the ProB2-UI or in the your operating systems standard editor) and allows to edit your general and global preferences by opening a seperate window.
+[[File:Formula.png|none]]
+Here you can add formulas for visualization and open the history chart window.
+[[File:Consoles.png|none]]
+This submenu leads to two consoles, one Groovy, one B.
+[[File:Perspectives.png|none]]
+The Perspectives submenu allows you to change the appearance of the main view. The default view is shown at the top and two additional perspectives (Seperated History and Seperated History and Statistics) are preset. By ''Detach Components'' the view can be shown in seperate windows. ''Load'' allows you to make your own perspective by providing an FXML file containing the views but be aware that this might ruin the ability to detach components.
+[[File:View.png|none]]
+This submenu allows you to adjust font and button size in the ProB2-UI.
+[[File:Help.png|none]]
+The Help submenu provides you with help about the ProB2-UI, information about the ProB2 UI, ProB2 kernel, ProB CLI and Java version used here and a way to report issues regarding the ProB2-UI.