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

Remove ProB2 section whose content can be found on the wiki

parent d5b8b14a
Branches
No related tags found
No related merge requests found
[[prob2.0]]
= ProB 2.0
:leveloffset: +1
[[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>>.
[[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.
[[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[]
:leveloffset: -1
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment