diff --git a/src/docs/chapter/reference/02_ABZ16.adoc b/src/docs/chapter/reference/02_ABZ16.adoc index 20d441ced4e9c1b5fcbea2f936d20d765f438c32..ad5c43bd4e7c6fc7d8e8f97de6dbfafd294e2ac1 100644 --- a/src/docs/chapter/reference/02_ABZ16.adoc +++ b/src/docs/chapter/reference/02_ABZ16.adoc @@ -48,4 +48,4 @@ Ladenberger (ladenberger@cs.uni-duesseldorf.de) * https://www3.hhu.de/stups/prob/index.php/BMotion_Studio[BMotion Studio for ProB Homepage] * https://www3.hhu.de/stups/handbook/bmotion/current/html[BMotion Studio for ProB User Handbook] * http://wiki.event-b.org/index.php/IUML-B[iUML-B Homepage] -* http://handbook.event-b.org/[Rodin Handbook] +* https://www3.hhu.de/stups/handbook/rodin/[Rodin Handbook] diff --git a/src/docs/chapter/user/01_The_ProB_Animator_and_Model_Checker.adoc b/src/docs/chapter/user/01_The_ProB_Animator_and_Model_Checker.adoc index 7a8b5e15ab8286e18c4058d3392679545ebfd9b5..60a7985e509f7000cbfd543a666d35240b09f0b9 100644 --- a/src/docs/chapter/user/01_The_ProB_Animator_and_Model_Checker.adoc +++ b/src/docs/chapter/user/01_The_ProB_Animator_and_Model_Checker.adoc @@ -3,8 +3,8 @@ [width="100%",cols="60%,40%",] |======================================================================= | ProB is an animator, constraint solver and model checker for the -http://en.wikipedia.org/wiki/B-Method[B-Method] (see the -http://www.clearsy.com/en/our-specific-know-how/b-method/?lang=en[B-Method +https://en.wikipedia.org/wiki/B-Method[B-Method] (see the +https://www.clearsy.com/en/[B-Method site of Clearsy]). It allows fully automatic animation of B specifications, and can be used to systematically check a specification for a wide range of errors. The constraint-solving capabilities of ProB @@ -17,7 +17,7 @@ and provides support for data structures such as (higher-order) relations, functions and sequences. In addition to the B language, ProB also supports http://www.event-b.org/[Event-B], http://en.wikipedia.org/wiki/Communicating_sequential_processes[CSP-M], -http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html[TLA+], +http://lamport.azurewebsites.net/tla/tla.html[TLA+], and http://en.wikipedia.org/wiki/Z_notation[Z]. ProB can be installed within http://sourceforge.net/projects/rodin-b-sharp/[Rodin], where it comes with diff --git a/src/docs/chapter/user/10_General/01_Installation.adoc b/src/docs/chapter/user/10_General/01_Installation.adoc index 0897d679bd6fb5fcb21535b7d20415837ee2b89c..ee5c34e3e0db4dae3474b943bf9ab2dea706626b 100644 --- a/src/docs/chapter/user/10_General/01_Installation.adoc +++ b/src/docs/chapter/user/10_General/01_Installation.adoc @@ -17,9 +17,9 @@ Both the standalone ProB Tcl/Tk and probcli can be downloaded together installation; just type in predicates and expressions into the web page. There is also a -http://www.tools.clearsy.com/index.php5?title=ProB_etool_generation[plugin +https://tools.clearsy.com/index.php5?title=ProB_etool_generation[plugin for Atelier B], in order to use the standalone ProB Tcl/Tk Version on -http://www.atelierb.eu/[Atelier B] projects. It comes bundled with ProB +https://www.atelierb.eu/[Atelier B] projects. It comes bundled with ProB Tcl/Tk. ProB is used within a few other tools, such as diff --git a/src/docs/chapter/user/10_General/02_Windows_Installation_Instructions.adoc b/src/docs/chapter/user/10_General/02_Windows_Installation_Instructions.adoc index 329ec00be3b438b3210321d55632b6dd18b171b3..8c9d7b8a0b0bc4f0d5c374116022574e54b34e1e 100644 --- a/src/docs/chapter/user/10_General/02_Windows_Installation_Instructions.adoc +++ b/src/docs/chapter/user/10_General/02_Windows_Installation_Instructions.adoc @@ -38,7 +38,7 @@ newer)] link provided in the `Dependencies` column and the `Windows` row above [[download-the-prob-for-windows-zipfile]] === Download the ProB for Windows Zipfile -* Click on the http://nightly.cobra.cs.uni-duesseldorf.de/releases/1.4.1/ProB.windows.zip[Zipfile +* Click on the https://www3.hhu.de/stups/downloads/[Zipfile (with probcli)] link in the `Downloads` column and `Windows` row * Decompress and expand the ProB directory if necessary. Do not change the location and structure of the files and directories within ProB @@ -74,7 +74,7 @@ written in Java. * In case you cannot start neither ProBWin nor probcli, you should to install the -http://www.microsoft.com/en-us/download/details.aspx?id=3387[Microsoft +https://www.microsoft.com/en-us/download/details.aspx?id=3387[Microsoft Visual C++ 2005 Redistributable Package (x86)] for yourself (rather than rely on the ones we provide in the `Microsoft.VC80.CRT` folder mentioned above). diff --git a/src/docs/chapter/user/20_Validation/MC/Tutorial_Various_Optimizations.adoc b/src/docs/chapter/user/20_Validation/MC/Tutorial_Various_Optimizations.adoc index 5e54515ec05f7a57f0151e09beb8f2f8778fbdf8..a8333861ad5e730746d0aaac9a969ba0a4d9388c 100644 --- a/src/docs/chapter/user/20_Validation/MC/Tutorial_Various_Optimizations.adoc +++ b/src/docs/chapter/user/20_Validation/MC/Tutorial_Various_Optimizations.adoc @@ -217,7 +217,7 @@ state space will be performed using the reduced search algorithm. The reduction algorithm has been evaluated on various B and Event-B models. The evaluation can be obtained -http://nightly.cobra.cs.uni-duesseldorf.de/por/[here]. +https://www3.hhu.de/stups/downloads/[here]. [[partial-guard-evaluation]] === Partial Guard Evaluation @@ -532,6 +532,6 @@ evaluations could be saved up. These and various other benchmarks used for evaluating partial guard evaluation (PGE) can be viewed -http://nightly.cobra.cs.uni-duesseldorf.de/pge/[here]. +https://www3.hhu.de/stups/downloads/[here]. === References diff --git a/src/docs/chapter/user/30_OtherLanguages/EventB/ProB_for_Event-B.adoc b/src/docs/chapter/user/30_OtherLanguages/EventB/ProB_for_Event-B.adoc index 8a754c3cf416d532493ef197d2c821579de00839..d70712cdfbebfcdb53024e0283e61bc1fb9b192f 100644 --- a/src/docs/chapter/user/30_OtherLanguages/EventB/ProB_for_Event-B.adoc +++ b/src/docs/chapter/user/30_OtherLanguages/EventB/ProB_for_Event-B.adoc @@ -22,10 +22,5 @@ Classic>> * <<tutorial-ltl-counter-example-view,Visualization of LTL Counter-examples in Rodin>> -The http://handbook.event-b.org[Rodin handbook] also contains material -about ProB: - -* http://handbook.event-b.org/current/html/tut_building_the_model.html#tut:prob[Finding -Invariant Violations with ProB] -* http://handbook.event-b.org/current/html/tut_populate_context.html#a0000000094[Finding -Solutions to Axioms] +The https://www3.hhu.de/stups/handbook/rodin/[Rodin handbook], also contains material +about ProB.