ProB Documentation - User contributions [en]

Verification View

2017-10-11T07:49:02Z

Yumiko Takahashi: /* Modelchecking */

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.
==Modelchecking==
[[File:Modelchecking.png|left]]
By pressing the plus button you can add several model checking variants. The following view will be shown:
[[File:Modelchecking Stage.png|left]]
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.

==LTL Verifications==
[[File:LTL.png|left]]
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.
==Constraint Based Checking==
[[File:CBC.png|left]]
[[File:Add CBC.png|left]]

File:Statistics.png

2017-10-11T07:18:46Z

Yumiko Takahashi: Yumiko Takahashi uploaded a new version of File:Statistics.png

Verification View

2017-10-11T07:14:13Z

Yumiko Takahashi: /* Constraint Based Checking */

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.
==Modelchecking==
[[File:Modelchecking.png|left]]
By pressing the plus button you can add several model checking variants. The following view will be shown:
[[File:Modelchecking Stage.png|left]]
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.

==LTL Verifications==
[[File:LTL.png|left]]
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.
==Constraint Based Checking==
[[File:CBC.png|left]]
[[File:Add CBC.png|left]]

File:Add CBC.png

2017-10-11T07:13:30Z

Yumiko Takahashi:

File:CBC.png

2017-10-11T07:10:23Z

Yumiko Takahashi: Yumiko Takahashi uploaded a new version of File:CBC.png

File:LTL.png

2017-10-11T07:10:00Z

Yumiko Takahashi: Yumiko Takahashi uploaded a new version of File:LTL.png

File:Modelchecking Stage.png

2017-10-11T07:09:32Z

Yumiko Takahashi: Yumiko Takahashi uploaded a new version of File:Modelchecking Stage.png

File:Modelchecking.png

2017-10-11T07:09:04Z

Yumiko Takahashi: Yumiko Takahashi uploaded a new version of File:Modelchecking.png

File:Runconfigurations Tab.png

2017-10-11T06:49:31Z

Yumiko Takahashi: Yumiko Takahashi uploaded a new version of File:Runconfigurations Tab.png

File:Add Preference.png

2017-10-11T06:48:44Z

Yumiko Takahashi: Yumiko Takahashi uploaded a new version of File:Add Preference.png

File:Preferences Tab.png

2017-10-11T06:48:22Z

Yumiko Takahashi: Yumiko Takahashi uploaded a new version of File:Preferences Tab.png

File:Verifications Tab.png

2017-10-11T06:47:18Z

Yumiko Takahashi: Yumiko Takahashi uploaded a new version of File:Verifications Tab.png

File:Machines Tab.png

2017-10-11T06:46:19Z

Yumiko Takahashi: Yumiko Takahashi uploaded a new version of File:Machines Tab.png

File:Project Tab.png

2017-10-11T06:45:22Z

Yumiko Takahashi: Yumiko Takahashi uploaded a new version of File:Project Tab.png

Verification View

2017-10-11T06:35:11Z

Yumiko Takahashi:

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.
==Modelchecking==
[[File:Modelchecking.png|left]]
By pressing the plus button you can add several model checking variants. The following view will be shown:
[[File:Modelchecking Stage.png|left]]
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.

==LTL Verifications==
[[File:LTL.png|left]]
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.
==Constraint Based Checking==
[[File:CBC.png|left]]

History View

2017-10-11T06:25:40Z

Yumiko Takahashi:

[[File:History.png|center]]The 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.

File:History.png

2017-10-11T06:20:45Z

Yumiko Takahashi: Yumiko Takahashi uploaded a new version of File:History.png

ProB2-UI

2017-10-04T09:29:00Z

Yumiko Takahashi:

== 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:
** [[History_View|The History of operations leading to this state (History)]]
** [[Project_View|The Project view]]
** [[Verification_View|The Verification view]]
** [[Statistics_View|The Statistics view]]

[[File:ProB2JavaFX_UI_Overview.png||900px]]

== The ProB2 JavaFX Main Menu Bar ==
The menu bar contains the various commands to access the features of ProB. It includes the menus
*File,
*Edit,
*Formula,
*Consoles,
*Perspectives,
*View,
*Window and
*Help
[[File:File.png|left]]
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.
[[File:Edit.png|left]]
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.
[[File:Formula.png|left]]
Here you can add formulas for visualization and open the history chart window.
[[File:Consoles.png|left]]
This submenu leads to two consoles, one Groovy, one B.
[[File:Perspectives.png|left]]
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|left]]
This submenu allows you to adjust font and button size in the ProB2 JavaFX UI.
[[File:Help.png|left]]
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.

ProB2-UI

2017-10-04T09:27:24Z

Yumiko Takahashi: /* The Submenus */

== 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:
** [[History_View|The History of operations leading to this state (History)]]
** [[Project_View|The Project view]]
** [[Verification_View|The Verification view]]
** [[Statistics_View|The Statistics view]]

[[File:ProB2JavaFX_UI_Overview.png||900px]]

== The ProB2 JavaFX Main Menu Bar ==
The menu bar contains the various commands to access the features of ProB. It includes the menus
*File,
*Edit,
*Formula,
*Consoles,
*Perspectives,
*View,
*Window and
*Help
===The Submenus===
[[File:File.png|left]]
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.
[[File:Edit.png|left]]
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.
[[File:Formula.png|left]]
Here you can add formulas for visualization and open the history chart window.
[[File:Consoles.png|left]]
This submenu leads to two consoles, one Groovy, one B.
[[File:Perspectives.png|left]]
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|left]]
This submenu allows you to adjust font and button size in the ProB2 JavaFX UI.
[[File:Help.png|left]]
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.

File:Help.png

2017-10-04T08:57:20Z

Yumiko Takahashi:

File:View.png

2017-10-04T08:57:06Z

Yumiko Takahashi:

File:Perspectives.png

2017-10-04T08:56:49Z

Yumiko Takahashi:

File:Consoles.png

2017-10-04T08:56:32Z

Yumiko Takahashi:

File:Formula.png

2017-10-04T08:56:15Z

Yumiko Takahashi:

File:Edit.png

2017-10-04T08:55:42Z

Yumiko Takahashi:

File:File.png

2017-10-04T08:55:20Z

Yumiko Takahashi:

ProB2-UI

2017-10-04T08:50:59Z

Yumiko Takahashi: /* The ProB2 JavaFX Main Menu Bar */

ProB2-UI

2017-10-04T08:40:50Z

Yumiko Takahashi: /* The ProB2 JavaFX Main Menu Bar */

Verification View

2017-10-04T07:10:08Z

Yumiko Takahashi: /* Modelchecking */

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.
==Modelchecking==
[[File:Modelchecking.png|left]]
By pressing the plus button you can add several model checking variants. The following view will be shown:
[[File:Modelchecking Stage.png|left]]
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.

==LTL Verifications==
[[File:LTL.png|left]]
==Constraint Based Checking==
[[File:CBC.png|left]]

File:Modelchecking Stage.png

2017-10-04T06:57:30Z

Yumiko Takahashi:

File:Modelchecking.png

2017-10-04T06:56:14Z

Yumiko Takahashi: Yumiko Takahashi uploaded a new version of File:Modelchecking.png

File:CBC.png

2017-10-04T06:51:51Z

Yumiko Takahashi:

File:LTL.png

2017-10-04T06:51:29Z

Yumiko Takahashi:

Verification View

2017-10-04T06:51:08Z

Yumiko Takahashi:

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.
==Modelchecking==
[[File:Modelchecking.png|left]]
==LTL Verifications==
[[File:LTL.png|left]]
==Constraint Based Checking==
[[File:CBC.png|left]]

File:Modelchecking.png

2017-10-04T06:48:38Z

Yumiko Takahashi: Yumiko Takahashi uploaded a new version of File:Modelchecking.png

File:Modelchecking.png

2017-10-04T06:47:16Z

Yumiko Takahashi: Yumiko Takahashi uploaded a new version of File:Modelchecking.png

Project View

2017-09-28T10:43:48Z

Yumiko Takahashi:

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)
==Project Tab==
[[File:Project Tab.png|left]]
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.
==Machines Tab==
[[File:Machines Tab.png|left]]
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.
==Verifications Tab==
[[File:Verifications Tab.png|left]]
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.
==Preferences Tab==
[[File:Preferences Tab.png|left]]
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.
[[File:Add Preference.png|left]]
The screenshot above shows the window for adding and editing preferences.
==Run Configurations Tab==
[[File:Runconfigurations Tab.png|left]]
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''.

File:Runconfigurations Tab.png

2017-09-28T10:43:06Z

Yumiko Takahashi:

Project View

2017-09-28T10:35:03Z

Yumiko Takahashi:

File:Add Preference.png

2017-09-28T10:25:48Z

Yumiko Takahashi:

File:Preferences Tab.png

2017-09-28T10:20:36Z

Yumiko Takahashi:

Project View

2017-09-28T10:17:30Z

Yumiko Takahashi:

File:Verifications Tab.png

2017-09-28T10:10:03Z

Yumiko Takahashi: Yumiko Takahashi uploaded a new version of File:Verifications Tab.png

File:Verifications Tab.png

2017-09-28T10:08:47Z

Yumiko Takahashi:

Project View

2017-09-28T10:06:17Z

Yumiko Takahashi:

File:Machines Tab.png

2017-09-28T10:00:35Z

Yumiko Takahashi:

File:Project Tab.png

2017-09-28T09:53:15Z

Yumiko Takahashi:

History View

2017-09-28T09:52:06Z

Yumiko Takahashi:

File:Modelchecking.png

2017-09-27T09:11:58Z

Yumiko Takahashi:

Verification View

2017-09-27T09:11:38Z

Yumiko Takahashi: