From 7c0989c296bad7fbf9808d71eb03faf367fc0c9f Mon Sep 17 00:00:00 2001 From: dgelessus <dgelessus@users.noreply.github.com> Date: Wed, 3 Feb 2021 17:58:08 +0100 Subject: [PATCH] Remove ProB2 section whose content can be found on the wiki --- .../user/50_ProB2/00_section_header.adoc | 4 -- .../50_ProB2/01_ProB_2.0_Development.adoc | 64 ----------------- ...odin_and_a_HTML_Visualization_Example.adoc | 68 ------------------- .../user/50_ProB2/Prob2-advance-release.adoc | 14 ---- .../user/50_ProB2/ZZ_section_footer.adoc | 2 - 5 files changed, 152 deletions(-) delete mode 100644 src/docs/chapter/user/50_ProB2/00_section_header.adoc delete mode 100644 src/docs/chapter/user/50_ProB2/01_ProB_2.0_Development.adoc delete mode 100644 src/docs/chapter/user/50_ProB2/02_ProB_2.0_within_Rodin_and_a_HTML_Visualization_Example.adoc delete mode 100644 src/docs/chapter/user/50_ProB2/Prob2-advance-release.adoc delete mode 100644 src/docs/chapter/user/50_ProB2/ZZ_section_footer.adoc diff --git a/src/docs/chapter/user/50_ProB2/00_section_header.adoc b/src/docs/chapter/user/50_ProB2/00_section_header.adoc deleted file mode 100644 index a26ea87..0000000 --- a/src/docs/chapter/user/50_ProB2/00_section_header.adoc +++ /dev/null @@ -1,4 +0,0 @@ - -[[prob2.0]] -= ProB 2.0 -:leveloffset: +1 diff --git a/src/docs/chapter/user/50_ProB2/01_ProB_2.0_Development.adoc b/src/docs/chapter/user/50_ProB2/01_ProB_2.0_Development.adoc deleted file mode 100644 index 20943a1..0000000 --- a/src/docs/chapter/user/50_ProB2/01_ProB_2.0_Development.adoc +++ /dev/null @@ -1,64 +0,0 @@ - -[[prob2.0_general]] -= General - -[[prob2.0-development]] -= ProB 2.0 Development - -[[basic-design-principles]] -== Basic Design Principles - -One of our main design goals was that we wanted to build our UI on top -of a programmatic API. Our goal was to bring the ProB 2.0 API into a -scripting language and not to bring the scripting language into the API. - -We also attempted to apply functional programming techniques to our -project wherever it was possible. This included trying to create small -abstractions that could be composed in different ways. For example, we -tried to avoid very large interfaces, but instead preferred to have -small functions and methods that accomplish one single task. For this -same reason, we tried to use immutable data structures wherever -possible. - -The ProB API needs to deal with many different formalisms (i.e. -Classical B, Event B, Z, CSP, etc.). For this reason, we constucted our -data structures so that they can be easily adapted for other formalisms. - -While developing a particular feature, it is very helpful to be able to -easily experiment and interact with the tool. For this reason, we have -spent quite a bit of energy developing a developer friendly console for -testing out features as they are being developed. - -[[why-groovy]] -== Why Groovy? - -The scripting language that we chose is Groovy. It is a dynamically -typed JVM language. Because of the seamless integration between Java and -Groovy libraries, we can easily integrate any jar library into the ProB -API, and the code that we produce can also be fully integrated into any -other Java project. - -Groovy also has many features that make it an ideal scripting language. -It provides closures which allow the definition of higher order -functions. It is also possible to perform meta programming and thereby -redefine or modify existing groovy or java class files. For example, in -ProB 2.0, we redefined the java.lang.String class so that we can specify -the correct Parser with which a string should be parsed. - -[[explanation-of-the-basic-programmatic-abstractions]] -== Explanation of the basic programmatic abstractions - -The basic programmatic abstractions that are available in the ProB 2.0 -API are the Model, Trace, and StateSpace abstractions. The Model -provides all the static information about the model that is currently -being checked or animated. The StateSpace provides the corresponding -label transition system for the Model. The Trace represents exactly one -trace throughout the StateSpace. A more detailed description of the -different is available -<<programmatic-abstractions-in-the-prob-2.0-api,here>>. - -[[tutorial-of-the-current-features-of-prob-2.0]] -== Tutorial of the Current Features of ProB 2.0 - -A tutorial for the current features of ProB 2.0 is available -<<prob2-tutorial,here>>. diff --git a/src/docs/chapter/user/50_ProB2/02_ProB_2.0_within_Rodin_and_a_HTML_Visualization_Example.adoc b/src/docs/chapter/user/50_ProB2/02_ProB_2.0_within_Rodin_and_a_HTML_Visualization_Example.adoc deleted file mode 100644 index f8e2ec4..0000000 --- a/src/docs/chapter/user/50_ProB2/02_ProB_2.0_within_Rodin_and_a_HTML_Visualization_Example.adoc +++ /dev/null @@ -1,68 +0,0 @@ - -[[prob2-within-rodin]] -= ProB 2.0 within Rodin - -[[installing-prob-2.0-from-rodin-2.7-or-later]] -== Installing ProB 2.0 from Rodin 2.7 or later - -ProB 2.0 for Rodin 3.1 can be installed from the update site, which is located -http://nightly.cobra.cs.uni-duesseldorf.de/prob2/updates/releases/advance-final/[here]. - -The installation follows the normal Eclipse installation procedure. -Choose 'Install New Software...' from Rodin's Help menu. - -Enter the update site into the textfield and hit enter. The result is -shown in the following screenshot: - -image::Install_prob2.png[] - -* Enter the http://nightly.cobra.cs.uni-duesseldorf.de/experimental/updatesite/[update site] -and install the ProB 2.0 plugin - -[[obtaining-the-latest-prob-binary]] -== Obtaining the latest ProB binary - -Open a Groovy Console and type `upgrade latest`. - -image::GroovyConsoleUpgradeLatest.png[] - -If you have trouble with this you can also manually download the latest -nightly version of ProB from our downloads area and put the probcli -binary and the lib directory into a `.prob` directory in your home -directory. - -[[import-the-lift-project]] -== Import the Lift Project - -Select the Rodin `Import…` menu command and import the - -#FIXME Lift.zip LINK. - -[[start-animating-the-lift]] -== Start Animating the Lift - -Right-click on the `MLift` model and select the `Start Animation` -command: - -image::MLiftAnimateWithProB.png[] - -Click on setup_constants and initialise in the Events view: - -image::MLiftEventsView.png[] - -[[open-html-visualization]] -== Open HTML Visualization - -Go into the BMotion Studio Menu at the top and select -`Open BMotion Studio Template`: - -image::MLiftOpenHTMLVisualization.png[] - -Navigate to the `lift.html` file that is included in the Lift.zip -archive. - -You can now see a graphical visualisation of the state of the model: - -image::MLiftHTMLVisualization.png[] - -You can also click on the buttons in the HTML page to control the model. diff --git a/src/docs/chapter/user/50_ProB2/Prob2-advance-release.adoc b/src/docs/chapter/user/50_ProB2/Prob2-advance-release.adoc deleted file mode 100644 index c91ac60..0000000 --- a/src/docs/chapter/user/50_ProB2/Prob2-advance-release.adoc +++ /dev/null @@ -1,14 +0,0 @@ - -[[prob2.0_advanced_release]] -= ProB 2.0 Advanced Release - -ProB 2.0 for Rodin 3.1 can be installed from the update site located at: -http://nightly.cobra.cs.uni-duesseldorf.de/prob2/updates/releases/advance-final/ - -The installation follows the normal Eclipse installation procedure. -Choose 'Install New Software...' from Rodin's Help menu. - -Enter the update site into the textfield and hit enter. The result is -shown in the following screenshot: - -image::Install_prob2.png[] diff --git a/src/docs/chapter/user/50_ProB2/ZZ_section_footer.adoc b/src/docs/chapter/user/50_ProB2/ZZ_section_footer.adoc deleted file mode 100644 index 909c09e..0000000 --- a/src/docs/chapter/user/50_ProB2/ZZ_section_footer.adoc +++ /dev/null @@ -1,2 +0,0 @@ - -:leveloffset: -1 -- GitLab