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 simple scheduler example. 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.
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.
trace = animations.getCurrentTrace() into the Groovy console. This accesses the current animation and saves it in the trace variable.s = trace.getStateSpace() to save a reference to the state space that is associated with traceA 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()
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 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")
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.
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.
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))
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)
Further information can be found in the developer manual.
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.