Skip to content
Snippets Groups Projects
Commit d5b8b14a authored by dgelessus's avatar dgelessus
Browse files

Remove JavaFX section whose content can be found on the wiki

parent 727fbd96
Branches
No related tags found
No related merge requests found
[[prob-2.0-javafx-ui]]
= ProB 2.0 JavaFX UI
:leveloffset: +1
[[beta-version-download]]
= Beta Version Download
* A beta version of this new UI is available at
https://www3.hhu.de/stups/downloads/prob2/[https://www3.hhu.de/stups/downloads/prob2/].
[[the-prob2-javafx-main-window]]
== The ProB2 JavaFX Main Window
By default the main window is split into three vertical panes (see
below).
* 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:
** <<javafx-history-view,The History of operations leading to this state (History)>>
** <<javafx-project-view,The Project view>>
** <<javafx-verification-view,The Verification view>>
** <<javafx-statistics-view,The Statistics view>>
image::ProB2JavaFX_UI_Overview.png[]
[[the-prob2-javafx-main-menu-bar]]
== The ProB2 JavaFX Main Menu Bar
The menu bar contains the various commands to access the features of
ProB. It includes the following menus:
=== File
image::File.png[]
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
JavaFX UI, save your project or reload the currently running machine.
=== Edit
image::Edit.png[]
The Edit submenu provides two ways to edit the
current machine (either in the editor provided by the ProB2 JavaFX UI or
in the your operating systems standard editor) and allows to edit your
general and global preferences by opening a seperate window.
=== Formula
image::Formula.png[]
Here you can add formulas for visualization and
open the history chart window.
=== Consoles
image::Consoles.png[]
This submenu leads to two consoles, one Groovy, one B.
=== Perspectives
image::Perspectives.png[]
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.
=== View
image::View.png[]
This submenu allows you to adjust font and button size in the ProB2 JavaFX UI.
=== Help
image::Help.png[]
The Help submenu provides you with help about the
ProB2 JavaFX UI, information about the ProB2 UI, ProB2 kernel, ProB CLI
and Java version used here and a way to report issues regarding the
ProB2 JavaFX UI.
[[javafx-history-view]]
= History View
image::History.png[]
History View shows a list of already executed operations.
The items contained in this list are linked to the State View:
When selecting one of these items, State View shows the current and the previous state of the chosen machine.
The chrevron buttons on the left allow to go back and forth in history by one step. The two buttons on the right provide sorting and help.
Note that if you choose to go back in history and execute an operation
the previously following one will be lost.
[[javafx-project-view]]
= Project View
If no machine or no project has been opened, the Project View will allow
you to create a project. If you choose to open a machine without having
a project, a default project will be created.
The Project View contains several tabs:
* *Project*, containing name and description
* *Machines*, containing machines added to this project
* *Verifications*, containing the verification status of each machine
* *Preferences*, containing custom preferences
* *Run Configurations*, containing machines paired with preferences
(each pair has its own entry)
[[javafx-project-tab]]
== Project Tab
image::Project_Tab.png[]
This tab shows the name and the description
of the current project. Both are either automatically generated by
opening a machine or chosen by the user who manually created the project
and can be changed by double clicking on each respectively.
[[javafx-machines-tab]]
== Machines Tab
image::Machines_Tab.png[]
This tab shows the machines belonging to
the project. By using the plus button several machines can be added to
the project. By clicking right on a specific machine this machine can be
edited or removed from the project.
[[javafx-verifications-tab]]
== Verifications Tab
image::Verifications_Tab.png[] This tab shows the status of each type
of verification run on the machines contained by the project. If no test
of a specific verification type has been run, a blue questionmark sign
is shown. If the verification type could not recognize any failures, a
green check will be displayed. If a test failed, a red x sign will be
shown.
[[javafx-preferences-tab]]
== Preferences Tab
image::Preferences_Tab.png[]
This tab allows to add, edit and remove
preference settings and shows a list of these preference settings by the
names chosen by the user. By pressing the plus button you can add and by
right clicking on a specific preference setting you can edit and remove.
image::Add_Preference.png[]
The screenshot above shows the window for adding and editing preferences.
[[javafx-run-configurations-tab]]
== Run Configurations Tab
image::Runconfigurations_Tab.png[]
This tab allows to pair up
machines and preferences. The machine running with default preferences
will be displayed just by name. Run configurations combining a machine
with a custom preference setting are shown as
_machinename.preferencename_.
[[javafx-verification-view]]
= Verification View
The Verification View provides 3 different methods to test a machine:
* Modelchecking
* LTL Verifications and
* Constraint Based Checking
In each tab you can add multiple tests to check you currently selected
machine and interrupt the checking process by pressing the "Cancel"
button.
[[javafx-modelchecking]]
== Modelchecking
image::Modelchecking.png[]
By pressing the plus button you can add
several model checking variants. The following view will be shown:
image::Modelchecking_Stage.png[]
Select one of the search strategies
(breadth first, depth first or a mix of both) and the checkboxes
containing different possible errors like deadlocks to be checked for.
By pushing the `Model Check` button your selected variant will be
added to the list shown at the top of the Modelchecking Tab.
[[javafx-ltl-verifications]]
== LTL Verifications
image::LTL.png[]
By pressing the `Add LTL Formula` or `Add LTL
Pattern` buttons an editor for each respectively will be opened and you
can add LTL formulas or patterns to the lists to be checked for.
[[javafx-constraint-based-checking]]
== Constraint Based Checking
image::CBC.png[]
image::Add_CBC.png[]
[[javafx-statistics-view]]
= Statistics View
The Statistics View provides some state and transition data: The main
view shows the quantity of processed states and total transitions, the
extended view shows additional state and transition statistics
image::Statistics.png[]
:leveloffset: -1
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment