User Manual: Difference between revisions

(Link to single-page handbook)
 
(14 intermediate revisions by 2 users not shown)
Line 1: Line 1:
[[Category:User_Manual]]
[[Category:User_Manual]]
__NOTOC__
__NOTOC__
ProB is a graphical animator and model checker for the B method. The ProB homepage is at [http://www.stups.uni-duesseldorf.de/ProB http://www.stups.uni-duesseldorf.de/ProB], where precompiled binaries, installation instructions and documentation are available.  
ProB is a graphical animator and model checker for the B method. The ProB homepage is at https://prob.hhu.de/, where precompiled binaries, installation instructions and documentation are available.  


== Important notice ==
== Important notice ==
If you find a problem with ProB or this documentation please let us know. We are happy to receive suggestions for improvements to ProB or the documentation.
If you find a problem with ProB or this documentation please let us know. We are happy to receive suggestions for improvements to ProB or the documentation.
More information about submitting bug reports is available in the [[Bugs|"bugs" section]] or directly in our  [http://jira.cobra.cs.uni-duesseldorf.de/ bug tracker].
More information about submitting bug reports is available in the [[Bugs|"bugs" section]].
You can also post a question in our [https://groups.google.com/d/forum/prob-users prob-users group] or  send an email to [mailto:Michael.Leuschel@hhu.de Michael Leuschel].
You can also post a question in our [https://groups.google.com/d/forum/prob-users prob-users group] or  send an email to [mailto:Michael.Leuschel@hhu.de Michael Leuschel].


== New version of ProB user manuals ==
== Single-page handbook ==


We are redesigning the user manual and developer handbook.
For those who prefer to read a single long page instead of many small pages, we also have a [[Full Handbook|single-page "handbook"]] version of the manual. '''Warning: the page is large and may take a few seconds to load.'''


* [https://www3.hhu.de/stups/handbook/prob2/prob_tcltk.html ProB Tcl/Tk User Manual] ([https://www3.hhu.de/stups/handbook/prob2/prob_tcltk.pdf PDF version of manual])
== Content of this manual ==
 
== Content of this handbook ==
{{User_Manual_Index}}
{{User_Manual_Index}}


Line 22: Line 20:


== Sample Models ==
== Sample Models ==
Some of the examples below are now [https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-notebooks available as Jupyter notebooks] and can be [https://mybinder.org/v2/git/https%3A%2F%2Fgitlab.cs.uni-duesseldorf.de%2Fgeneral%2Fstups%2Fprob2-jupyter-notebooks.git/master launched using binder].  Another [https://gitlab.cs.uni-duesseldorf.de/general/stups/prob-teaching-notebooks repository contains notebooks for teaching].
An extensive [https://github.com/hhu-stups/specifications collection of models for benchmarking is maintained in a Github repository].


* [[TrainSwitchingPuzzle]]
* [[TrainSwitchingPuzzle]]
* [[Gilbreath_Card_Trick|Model for Card Trick by Gilbreath]]
* [[Gilbreath_Card_Trick|Model for Card Trick by Gilbreath]]
* [[Rush Hour Puzzle]]
* [[Rush Hour Puzzle]]
* [[Game of Life]]
* [[Game of Life]] ([https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-notebooks/-/blob/master/puzzles/Game_of_Life.ipynb Jupyter notebook])
* [[N-Queens]]
* [[N-Queens]]
* [[Peaceable Armies of Queens]]
* [[Peaceable Armies of Queens]]
* [[Die Hard Jugs Puzzle]]
* [[Die Hard Jugs Puzzle]] ([https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-notebooks/-/blob/master/puzzles/Die_Hard_Jugs.ipynb Jupyter notebook])
* [[ABZ14|ABZ 2014 Landing Gear Case Study]]
* [[ABZ14|ABZ 2014 Landing Gear Case Study]]
* [[Sudoku Solved in the ProB REPL]]
* [[Sudoku Solved in the ProB REPL]]
* [https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-notebooks/-/blob/master/puzzles/Sudoku_Miracle.ipynb Miracle Sudoku (Jupyter notebook)]
* [[Euler Problem 67 - Maximum Path Sum II]]
* [[Euler Problem 67 - Maximum Path Sum II]]
* [[Mutual Exclusion (Fairness)]]
* [[Mutual Exclusion (Fairness)]]
Line 37: Line 38:
* [[Blocks World (Directed Model Checking)]]
* [[Blocks World (Directed Model Checking)]]
* [[Nine Prisoners|Nine Prisoners Puzzle by Dudeney and Gardner]]
* [[Nine Prisoners|Nine Prisoners Puzzle by Dudeney and Gardner]]
* [[Apples and Oranges (Apple Interview Question)]]
* [[Apples and Oranges (Apple Interview Question)]] ([https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-notebooks/-/blob/master/puzzles/Apples_and_Oranges.ipynb Jupyter Notebook])
* [[Bridges Puzzle (Hashiwokakero)]]
* [[Bridges Puzzle (Hashiwokakero)]] ([https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-notebooks/-/blob/master/puzzles/Bridges_Puzzle.ipynb Jupyter notebook])
* [[Argumentation Theory]]
* [[Argumentation Theory]]
* [[State_space_visualization_examples]]
* [[State_space_visualization_examples]]
Line 45: Line 46:
*[[ABZ16|ABZ 2016 Medical Case Study]]
*[[ABZ16|ABZ 2016 Medical Case Study]]
* [[Proving Theorems in the ProB REPL]]
* [[Proving Theorems in the ProB REPL]]
* [[SEND-MORE-MONEY]]
* [[SEND-MORE-MONEY]] ([https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-notebooks/-/blob/master/puzzles/SEND-MORE-MONEY.ipynb Jupyter notebook])
* [[Induction Proofs in B]]


== Sample Graphics ==
== Sample Graphics ==

Latest revision as of 15:19, 18 November 2022


ProB is a graphical animator and model checker for the B method. The ProB homepage is at https://prob.hhu.de/, where precompiled binaries, installation instructions and documentation are available.

Important notice

If you find a problem with ProB or this documentation please let us know. We are happy to receive suggestions for improvements to ProB or the documentation. More information about submitting bug reports is available in the "bugs" section. You can also post a question in our prob-users group or send an email to Michael Leuschel.

Single-page handbook

For those who prefer to read a single long page instead of many small pages, we also have a single-page "handbook" version of the manual. Warning: the page is large and may take a few seconds to load.

Content of this manual

Animation and Visualisation with ProB:

Validation with ProB:

Other Interfaces to ProB:

ProB and Other Tools:

ProB for Other Languages:

Advanced Features of ProB:

Advanced Visualization Features of ProB:

FAQ, Tips and Troubleshootings:


(Also have a look at the tutorial; in particular Starting ProB and first animation steps).

Sample Models

Some of the examples below are now available as Jupyter notebooks and can be launched using binder. Another repository contains notebooks for teaching. An extensive collection of models for benchmarking is maintained in a Github repository.

Sample Graphics


Feedback

Please help us to improve this documentation by providing feedback in our bug tracker, asking questions in our prob-users group or sending an email to Michael Leuschel.