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

Remove JavaAPI section whose content can be found on the wiki 

The other section about the ProB 2 API is *not* content from the wiki.
parent 59650dc3
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
Showing
with 0 additions and 513 deletions
src/docs/chapter/user/60_JavaAPI/00_section_header.adoc deleted 100644 → 0
+ 0
− 4
View file @ 59650dc3
[[prob2-java-api]]
= ProB 2.0 Java API
:leveloffset: +1
src/docs/chapter/user/60_JavaAPI/01_ProB_Java_API.adoc deleted 100644 → 0
+ 0
− 33
View file @ 59650dc3
[[general-java-api]]
= General
[[prob-java-api-documentation]]
== Documentation
* <<prob-java-api-tutorial,Tutorial>>
* <<developer-introduction, Documentation>>
== Additional Material
* <<prob2.0-development,ProB 2.0 Development>>
* https://github.com/bendisposto/prob2_tooling_template[ProB 2.0 Tooling
Template]
* <<programmatic-abstractions-in-prob-api,Programmatic_Abstractions_in_the_ProB_2.0_API>>
* https://docs.google.com/document/pub?id=109z3qG6_KBUqm0NC9FaEF1C6_NYCJl453wcXzbovj2Q[ProB
2.0 Requirements Document] +
(if you want to comment on the Document, please use goo.gl/KS2bh)
* <<user-and-developer-workshop,Rodin User and Developer Workshop 2013 -
Tutorial Presentation>>
* <<tutorial13,Rodin User and Developer Workshop 2013 - Tutorial>>
* <<prob-2.0-within-rodin-and-a-html-visualization-example,ProB 2.0
within Rodin and a HTML Visualization Example>>
== Download
Nightly builds of ProB 2 for Rodin 3 can be obtained from within Rodin
using the update site
http://nightly.cobra.cs.uni-duesseldorf.de/prob2/updates/nightly/[http://nightly.cobra.cs.uni-duesseldorf.de/prob2/updates/nightly/].
src/docs/chapter/user/60_JavaAPI/10_Programmatic_Abstractions_in_the_ProB_2.0_API.adoc deleted 100644 → 0
+ 0
− 86
View file @ 59650dc3
[[programmatic-abstractions-in-prob-api]]
= Programmatic Abstraction in the ProB 2.0 API
[[overview-programmatic-abstractions-in-prob-api]]
== Overview
[[background]]
=== Background
The original ProB plug-in for Rodin introduced one basic abstraction:
developers can create Java commands specifying calculations that are to
be made by the ProB CLI binary. The result that is calculated by ProB
can then be interpreted and manipulated by the developer. Each Java
command corresponds to one prolog instruction in the ProB kernel.
[[current-implementation]]
=== Current Implementation
We have maintained the abstractions of the commands in order to
communicate with the ProB kernel. However, as we were considering how
the ProB core should be structured, we realized that many commands may
be used over and over again in the same (or very similar) concepts.
Therefore, we created the programmatic abstractions that will be
described in the following sections.
[[java-api-model]]
== Model
The Model is an abstraction that provides static information about the
current model that is being animated or checked. For Classical B and
Event B, this includes all of the information about the refinement chain
and all of the different components (Machines, Contexts, Invariants,
Variables, etc.).
This abstraction is available so that it is possible to have access to
the static information about the model during an animation without
having to contact ProB directly.
Currently, the Model abstraction is implemented for the Classical B and
Event B formalisms. But because we have implemented the abstraction with
other formalisms in mind, it should not be difficult to implement new
formalisms. We have also implemented a Model abstraction for CSP-M
specifications, but it is currently not possible to access any static
information about the model. TLA+ specifications can be represented in
the API as Classical B models.
[[java-api-statespace]]
== StateSpace
There is a one-to-one relationship between a StateSpace and a model. The
StateSpace is the corresponding label transition system for a particular
model.
Conceptually, the state space is completely there and completely
evaluated. When you access a state within the StateSpace, ProB will
fetch the information from Prolog automatically and transparently. The
only observation that can be made is that the fetching of some states
takes longer than the ones that are already "cached" in the
StateSpace. For performance reasons, not all states in the state space
are saved indefinitely. The states in the StateSpace are saved as State
objects, which then hold the information about the outgoing transitions
and formulas of interest that have been evaluated for the given state.
In the StateSpace, these objects are cached in an LRU cache so that if
not accessed for a given period of time, the garbage collector can clean
them up.
[[java-api-trace]]
== Trace
For some tools, the StateSpace abstraction may be sufficient. But when
it comes to animation and the concept of a "current state", a further
abstraction becomes necessary. The Trace provides this abstraction.
A Trace consists of a linked list of states which correspond to a path
through the StateSpace. There is also a pointer in the list which
identifies the current state. The Trace behaves like a browser history;
it is possible to move forward and backward within the current trace.
A Trace corresponds to exactly one trace within the animation. Each
Trace is associated with exactly one StateSpace, but we can have many
different Trace objects on top of a single StateSpace.
The Trace is immutable. This means that whenever an animation step is
performed (forward, backward, or simply adding a transition to the
trace) a new Trace is returned.
src/docs/chapter/user/60_JavaAPI/20_Rodin_User_and_Developer_Workshop_2013_-_Tutorial.adoc deleted 100644 → 0
+ 0
− 388
View file @ 59650dc3
[[rodin-user-and-developer-workshop-2013]]
= Rodin User and Developer Workshop 2013
Here are the information we have shown you at the tutorial. If you want
to follow this tutorial on your computer you will have to install ProB
2.0 and start an animation. For this tutorial we use a
image::Scheduler_tutorial2013.zip[]. Maybe you
have to clean the project after importing.
This page was updated in May of 2015 to reflect changes made to the ProB
2.0 API.
[[java-api-setup]]
== Setup
You will need a fresh copy of ProB 2.0 installed to your Rodin or the
sourcecode.
The update site for our builds is:
http://nightly.cobra.cs.uni-duesseldorf.de/experimental/updatesite/
The sourcecode repository and a description how to setup your Eclipse:
https://github.com/bendisposto/prob2
Please note that no matter which installation method you chose, you need
to fetch the latest Prolog binaries. The easiest way is to type
'upgrade "latest"` into the ProB 2.0 Groovy console.
In the following we will intermix some explanations with FAQ style code
snippets. We assume that you execute all the code snippets. Some of the
snippets rely on the previous execution of other snippets.
[[java-api-preparation]]
== Preparation
1. Import the Scheduler project.
2. Start an animation for Scheduler0
3. Perform some random animation steps
4. Type `trace = animations.getCurrentTrace()` into the Groovy console.
This accesses the current animation and saves it in the `trace`
variable.
5. Type `s = trace.getStateSpace()` to save a reference to the state
space that is associated with `trace`
[[java-api-the-model]]
== The Model
A model gives you access to the static properties of a Rodin
development. Such as contexts, machines, constants, variables,
invariants, events, etc. A model is a graph of components and their
relationship. Except for Graph handling there are no shared methods
between formalisms. The main difference between EventBModel and
ClassicalBModel are the artifacts and relationships they can contain. An
EventB Model consists of Machines and Contexts and the only
relationships are refinement and sees.
*How can we get the model for a given state space?*
`m = s.getModel()`
*What is the Java type of m?*
`m.getClass()`
An EventB model consists of machines and contexts. Machines allow to
access variables, invariants, variants and events. Contexts give you
access to axioms, constants and sets. Let's explore machines.
*How do we get access to the Scheduler0 machine?*
`mch = m.getComponent("Scheduler0")`
*What are the invariants of Scheduler0?*
`mch.getInvariants()`
*What are the events of Scheduler0?*
`mch.getEvents()`
*How can we access the event named new?*
`ne = mch.getEvent("new")`
*What is the guard of new?*
`ne.getGuards()`
[[java-api-the-state-space]]
== The State Space
The state space represents the whole currently known world for an
animation. It is lazily explored. Information about the state space is
stored in State objects which can be queried to inspect information
about any given state. These State objects are cached and can be
accessed via their string identifier.
*How do we retrieve the state space for a given model?*
`s = m.getStateSpace()`
In Rodin, you should try to explore the state until your trace contains
the `massakr` event. This event breaks the invariant of the system.
Otherwise the next command will return an empty set.
*How can I access the current state from an animation?*
`state = trace.getCurrentState()`
*Does the state that violate the invariant?*
`state.getInvariantOk()`
*Can we get the value of a variable in that state?*
`state.eval("active")`
*Can we randomly "execute" events?*
`y = state.anyEvent()`
*Can we "execute" a specific event?*
Yes we can! We will figure out how it is done in a moment.
*How do we find out which events are enabled?*
`state.getOutTransitions()`
*What are the elements of this list?*
`state.getOutTransitions().first().getClass()`
*Now let's get one of these Transition objects*
`trans = state.getOutTransitions()[1]`
*What is the name of the transition?*
`n = trans.getName()`
*What are the actual parameters?*
`params = trans.getParams()`
*What is the formal parameter name?*
`e = mch.getEvent(trans.getName())`
Finally we can "execute" the Event using the perform method of the
StateId object. At this point you need to chose an event that you want
to execute. It has to be enabled in the state, but you can provide
additional guards to restrict the parameters. For instance if the event
del is enabled and we want to delete process P2 the command is
*state.perform("del",["r=P2"])*
We try not to intertwine different aspects of the system. That is why we
had to get the formal parameter from the model's representation, the
enabled operations from the state, and the detail information from the
Transition object. This design principle was taken from Rich Hickey's
http://www.infoq.com/presentations/Simple-Made-Easy[Simple made easy]
talk.
However, this doesn't prevent us (or you!) from adding convenience
functions!
*How do I execute an event?*
....
def exec(mch,state,name,params) {
formal_params = mch.getEvent(name).getParameters()
pred = [formal_params,params].transpose()
.collect { a,b -> a.toString() + "=" + b.toString() }
state.perform(name,pred)
}
....
You can write your own set of convenience functions in a groovy file and
run it at the beginning.
`run new File("myAwesomeScript.groovy")`
[[java-api-traces]]
== Traces
A trace represents a path through the state space. It can move forward
and backward through the Trace and can be extended with a new
transition. Traces are immutable, yet creating new traces is efficient
because of structural sharing.
*How can we track a trace of events?*
`t = new Trace(s)`
*What is the current state of the trace?*
`t.getCurrentState()`
*What are the enabled events in the current state?*
`t.getNextTransitions()`
*How can we "execute" an event?*
`t = t.add(t.getNextTransitions().first())`
*How can we produce a random trace?*
`def randTrace(t,n) {` +
` def nt = t;` +
` n.times { nt = nt.anyEvent() }` +
` nt` +
`}`
*Let's run it!*
`randTrace(t,20)`
'''How can go back in time? '''
`t = t.back()`
*How can we go forward in time?*
`t = t.forward()`
If we go back in time, the trace keeps future states. If we change a
decision in the past, the trace drops the future. It behaves in the same
way your browser history does.
[[java-api-evaluation]]
== Evaluation
Evaluation is done by passing an instance of the interface IEvalElement
to an evaluator. Each formalism has its own descendant of IEvalElement.
They apply a parser to a String
*How can we create an EventB formula?*
`f1 = "active \\/ waiting"` as EventB
The escaping of the backslash is unfortunatly required because the
formula is contained in a Java String.
*And how do we create a classical B formula?*
`f2 = "active \\/ waiting"` as ClassicalB
*How can we evaluate the formulas for state x?*
`x.eval(f1)`
*What have we received?*
`x.eval(f1).getClass()`
ProB's Prolog engine does not make a difference between EventB and
classical B. Only the parsers are different. Event B Formulas are parsed
by Rodin. Classical B formulas are parsed by ProB's parser.
*Ok, we can evaluate a formula for a state. Anything else that evaluates
formulas?*
`t.eval(f1)`
Traces evaluate a formula for each state of the trace. They return a
list of results.
*Anything else?*
`s.evaluateForGivenStates(t.getTransitionList().collect { it.getSource()},[f1, "waiting" as EventB])`
evaluateForGivenStates takes a list of states and a list of formulas and
evaluates them for each state of the statespace. This method is not
called eval to prevent accidental evaluation.
*Can we evaluate the guard of an event for a whole trace?*
....
g = mch.getEvent("del").getGuards()
g = g.collect {it.toString()}.join(" & ")
t.eval(g)
....
`"I want to have it extra sweet!"`
....
String.metaClass.and = {b -> "("+delegate+") & ("+b + ")" }
not = { "not("+it+")" }
String.metaClass.implies = {b -> "("+delegate +") => (" + b + ") "}
conj = { it.collect{it.toString()}.inject {a,b -> a & b}}
....
This piece of code introduces four functions to simplify handling of
formulas. The first line overrides the & operator for Strings and allows
us to conjoin two predicates as Strings, e.g., `"1<4" & "x>y"`
evaluates to `"(1<4) & (x>y)"`. The second line implements a
function not that wraps a predicate into a negation. The third line adds
an implies method to the class String. `"1<2".implies("3<4")`
results in `"(1<2) => (3<4)"`. The last line converts a list
of predicates into a conjunction. In Groovy collect means map and inject
means reduce.
[[java-api-constraint-solver]]
== Constraint solver
*Evaluation is fine, but can I use ProB's solver?*
....
f4 = new EventB("a = 1 & b = a - 1")
c4 = new CbcSolveCommand(f4)
s.execute(c4)
c4.getValue()
....
The state space in the example has two purposes. It is used to tell the
typechecker which constants and sets exist in the model. It also allows
us to send commands to the Prolog core of ProB.
'''What do we get if the predicate is not solvable? '''
....
f4 = new ClassicalB("a = a - 1")
c4 = new CbcSolveCommand(f4)
s.execute(c4)
c4.getValue()
....
*Can we get rid of that Java stuff please?*
....
def cbc_solve(space, formula) {
e = new EventB(formula)
c = new CbcSolveCommand(e)
space.execute(c)
c.getValue()
}
....
*Can we find out if one event can in principle be enabled, i.e., it is
not dead code?*
....
i = conj(mch.getInvariants())
g = conj(mch.getEvent("del").getGuards())
cbc_solve(s, i & i.implies(g))
....
[[java-api-notification-and-ui-access]]
== Notification and UI Access
Clients can register themself to receive a notification if an animation
step occured, new states were discovered or the model has changed. The
client has to implement one of the Listener interfaces from the
de.prob.statespace package.
ProB 2.0 was built on top of the same commands as ProB 1.0. Most of the
commands are usable with only minor changes. ProB 2.0 can be extended in
the same way as ProB 1.0.
To access the user interface, ProB 2.0 injects two special objects into
the console, `animations` and `api`.
`animations` is an Instance of `AnimationSelector`, `api` is an instance
of `Api`. The selector maintains lists of Traces and State Spaces. The
trace shown in the UI is marked as the current trace. The Api object is
used to load models. Most likely we will rename this class and instance
in the future to something more meaningful, e.g., loader.
*Can I get the trace that is shown in the UI?*
`animations.getCurrentTrace()`
*What traces are registered?*
`animations.getTraces()`
*Can I add a trace to the UI?*
`animations.addNewAnimation(t)`
[[java-api-additional-resources]]
== Additional Resources
Further information can be found in the ProB Developer_Manual.
src/docs/chapter/user/60_JavaAPI/ZZ_section_footer.adoc deleted 100644 → 0
+ 0
− 2
View file @ 59650dc3
:leveloffset: -1
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment