ProB Documentation - User contributions [en]

Rodin User and Developer Workshop 2013 - Tutorial

2015-05-05T08:20:08Z

Joy Clark:

[[Category:ProB Java API]]

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 [[media:Scheduler_tutorial2013.zip|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.

== 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 '''<code>upgrade "latest"</code>''' 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.

== Preparation ==

# Import the Scheduler project.
# Start an animation for Scheduler0
# Perform some random animation steps
# Type <code>trace = animations.getCurrentTrace()</code> into the Groovy console. This accesses the current animation and saves it in the <code>trace</code> variable.
# Type <code>s = trace.getStateSpace()</code> to save a reference to the state space that is associated with <code>trace</code>

== 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()

== 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 <code>massakr</code> 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")

== 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.

== 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., <code>"1<4" & "x>y"</code> evaluates to <code>"(1<4) & (x>y)"</code>. 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. <code>"1<2".implies("3<4")</code> results in <code>"(1<2) => (3<4)"</code>. The last line converts a list of predicates into a conjunction. In Groovy collect means map and inject means reduce.

== 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))

== 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, <code>animations</code> and <code>api</code>.

<code>animations</code> is an Instance of <code>AnimationSelector</code>, <code>api</code> is an instance of <code>Api</code>. 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)

==Additional Resources==

Further information can be found in the [[Developer_Manual|developer manual]].

{{Feedback}}

Rodin User and Developer Workshop 2013 - Tutorial

2015-05-05T08:18:47Z

Joy Clark: /* Evaluation */

[[Category:ProB Java API]]

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 [[media:Scheduler_tutorial2013.zip|simple scheduler example]]. Maybe you have to clean the project after importing.

== 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 '''<code>upgrade "latest"</code>''' 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.

== Preparation ==

# Import the Scheduler project.
# Start an animation for Scheduler0
# Perform some random animation steps
# Type <code>trace = animations.getCurrentTrace()</code> into the Groovy console. This accesses the current animation and saves it in the <code>trace</code> variable.
# Type <code>s = trace.getStateSpace()</code> to save a reference to the state space that is associated with <code>trace</code>

== 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()

== 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 <code>massakr</code> 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")

== 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.

== 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., <code>"1<4" & "x>y"</code> evaluates to <code>"(1<4) & (x>y)"</code>. 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. <code>"1<2".implies("3<4")</code> results in <code>"(1<2) => (3<4)"</code>. The last line converts a list of predicates into a conjunction. In Groovy collect means map and inject means reduce.

== 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))

== 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, <code>animations</code> and <code>api</code>.

<code>animations</code> is an Instance of <code>AnimationSelector</code>, <code>api</code> is an instance of <code>Api</code>. 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)

==Additional Resources==

Further information can be found in the [[Developer_Manual|developer manual]].

{{Feedback}}

Rodin User and Developer Workshop 2013 - Tutorial

2015-05-05T08:14:12Z

Joy Clark: /* Traces */

[[Category:ProB Java API]]

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 [[media:Scheduler_tutorial2013.zip|simple scheduler example]]. Maybe you have to clean the project after importing.

== 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 '''<code>upgrade "latest"</code>''' 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.

== Preparation ==

# Import the Scheduler project.
# Start an animation for Scheduler0
# Perform some random animation steps
# Type <code>trace = animations.getCurrentTrace()</code> into the Groovy console. This accesses the current animation and saves it in the <code>trace</code> variable.
# Type <code>s = trace.getStateSpace()</code> to save a reference to the state space that is associated with <code>trace</code>

== 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()

== 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 <code>massakr</code> 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")

== 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.

== 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.evaluateForEveryState([f1, "waiting" as EventB])

evaluateForEveryState takes a list of formulas and evaluates them for each state of the statespace. This method is not called eval to prevent accidental evaluation. To evaluate a list of formulas for a subset, there is another method evaluateForGivenStates.

'''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., <code>"1<4" & "x>y"</code> evaluates to <code>"(1<4) & (x>y)"</code>. 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. <code>"1<2".implies("3<4")</code> results in <code>"(1<2) => (3<4)"</code>. The last line converts a list of predicates into a conjunction. In Groovy collect means map and inject means reduce.

== 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))

== 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, <code>animations</code> and <code>api</code>.

<code>animations</code> is an Instance of <code>AnimationSelector</code>, <code>api</code> is an instance of <code>Api</code>. 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)

==Additional Resources==

Further information can be found in the [[Developer_Manual|developer manual]].

{{Feedback}}

Rodin User and Developer Workshop 2013 - Tutorial

2015-05-05T08:13:16Z

Joy Clark: /* The State Space */

[[Category:ProB Java API]]

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 [[media:Scheduler_tutorial2013.zip|simple scheduler example]]. Maybe you have to clean the project after importing.

== 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 '''<code>upgrade "latest"</code>''' 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.

== Preparation ==

# Import the Scheduler project.
# Start an animation for Scheduler0
# Perform some random animation steps
# Type <code>trace = animations.getCurrentTrace()</code> into the Groovy console. This accesses the current animation and saves it in the <code>trace</code> variable.
# Type <code>s = trace.getStateSpace()</code> to save a reference to the state space that is associated with <code>trace</code>

== 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()

== 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 <code>massakr</code> 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")

== 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().getId())

'''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 ==
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.evaluateForEveryState([f1, "waiting" as EventB])

evaluateForEveryState takes a list of formulas and evaluates them for each state of the statespace. This method is not called eval to prevent accidental evaluation. To evaluate a list of formulas for a subset, there is another method evaluateForGivenStates.

'''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., <code>"1<4" & "x>y"</code> evaluates to <code>"(1<4) & (x>y)"</code>. 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. <code>"1<2".implies("3<4")</code> results in <code>"(1<2) => (3<4)"</code>. The last line converts a list of predicates into a conjunction. In Groovy collect means map and inject means reduce.

== 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))

== 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, <code>animations</code> and <code>api</code>.

<code>animations</code> is an Instance of <code>AnimationSelector</code>, <code>api</code> is an instance of <code>Api</code>. 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)

==Additional Resources==

Further information can be found in the [[Developer_Manual|developer manual]].

{{Feedback}}

Rodin User and Developer Workshop 2013 - Tutorial

2015-05-05T08:01:24Z

Joy Clark: /* Preparation */

[[Category:ProB Java API]]

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 [[media:Scheduler_tutorial2013.zip|simple scheduler example]]. Maybe you have to clean the project after importing.

== 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 '''<code>upgrade "latest"</code>''' 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.

== Preparation ==

# Import the Scheduler project.
# Start an animation for Scheduler0
# Perform some random animation steps
# Type <code>trace = animations.getCurrentTrace()</code> into the Groovy console. This accesses the current animation and saves it in the <code>trace</code> variable.
# Type <code>s = trace.getStateSpace()</code> to save a reference to the state space that is associated with <code>trace</code>

== 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()

== 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 <code>massakr</code> event. This event breaks the invariant of the system. Otherwise the next command will return an empty set.

'''Are there some states that violate the invariant?'''
s.getInvariantKo()

'''Are there some states where the invariant holds?'''
s.getInvariantOk()

'''What kind of object is the result? '''
s.getInvariantOk().getClass()

'''What kind of objects are contained in the set? '''
s.getInvariantOk().first().getClass()

'''Let's explore StateIds.'''
x = s.getInvariantOk().first()

'''Can we get the value of a variable in that state?'''
x.value("active")

'''Can we randomly "execute" events?'''
y = x.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?'''
s.getOutEdges(x)

'''What are the elements of the hashset?'''
s.getOutEdges(x).first().getClass()

'''Now let's get one of these OpInfo objects'''
o = (s.getOutEdges(x) as List)[1]

Groovy allows us to transform a Set into a list using the Groovy [http://silvanolte.com/blog/2011/03/11/the-groovy-as-keyword/ as] keyword.

'''What is the name of the operation?'''
n = o.getName()

'''What are the actual parameters?'''
n = o.getParams()

'''What is the formal parameter name?'''
e = mch.getEvent(o.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

'''x.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 space, and the detail information from the OpInfo 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,x,name,params) {
formal_params = mch.getEvent(name).getParameters()
pred = [formal_params,params].transpose()
.collect { a,b -> a.toString() + "=" + b.toString() }
x.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")

== 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().getId())

'''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 ==
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.evaluateForEveryState([f1, "waiting" as EventB])

evaluateForEveryState takes a list of formulas and evaluates them for each state of the statespace. This method is not called eval to prevent accidental evaluation. To evaluate a list of formulas for a subset, there is another method evaluateForGivenStates.

'''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., <code>"1<4" & "x>y"</code> evaluates to <code>"(1<4) & (x>y)"</code>. 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. <code>"1<2".implies("3<4")</code> results in <code>"(1<2) => (3<4)"</code>. The last line converts a list of predicates into a conjunction. In Groovy collect means map and inject means reduce.

== 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))

== 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, <code>animations</code> and <code>api</code>.

<code>animations</code> is an Instance of <code>AnimationSelector</code>, <code>api</code> is an instance of <code>Api</code>. 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)

==Additional Resources==

Further information can be found in the [[Developer_Manual|developer manual]].

{{Feedback}}

Rodin User and Developer Workshop 2013 - Tutorial

2015-05-05T07:59:52Z

Joy Clark: /* The State Space */

[[Category:ProB Java API]]

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 [[media:Scheduler_tutorial2013.zip|simple scheduler example]]. Maybe you have to clean the project after importing.

== 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 '''<code>upgrade "latest"</code>''' 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.

== Preparation ==

# Import the Scheduler project.
# Start an animation for Scheduler0
# Perform some random animation steps
# Type <code>s = animations.getCurrentTrace() as StateSpace</code> into the Groovy console. <code>animations.getCurrentTrace()</code> accesses the current animation and <code>as StateSpace</code> accesses the current state space associated with the current animation.

== 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()

== 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 <code>massakr</code> event. This event breaks the invariant of the system. Otherwise the next command will return an empty set.

'''Are there some states that violate the invariant?'''
s.getInvariantKo()

'''Are there some states where the invariant holds?'''
s.getInvariantOk()

'''What kind of object is the result? '''
s.getInvariantOk().getClass()

'''What kind of objects are contained in the set? '''
s.getInvariantOk().first().getClass()

'''Let's explore StateIds.'''
x = s.getInvariantOk().first()

'''Can we get the value of a variable in that state?'''
x.value("active")

'''Can we randomly "execute" events?'''
y = x.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?'''
s.getOutEdges(x)

'''What are the elements of the hashset?'''
s.getOutEdges(x).first().getClass()

'''Now let's get one of these OpInfo objects'''
o = (s.getOutEdges(x) as List)[1]

Groovy allows us to transform a Set into a list using the Groovy [http://silvanolte.com/blog/2011/03/11/the-groovy-as-keyword/ as] keyword.

'''What is the name of the operation?'''
n = o.getName()

'''What are the actual parameters?'''
n = o.getParams()

'''What is the formal parameter name?'''
e = mch.getEvent(o.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

'''x.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 space, and the detail information from the OpInfo 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,x,name,params) {
formal_params = mch.getEvent(name).getParameters()
pred = [formal_params,params].transpose()
.collect { a,b -> a.toString() + "=" + b.toString() }
x.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")

== 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().getId())

'''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 ==
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.evaluateForEveryState([f1, "waiting" as EventB])

evaluateForEveryState takes a list of formulas and evaluates them for each state of the statespace. This method is not called eval to prevent accidental evaluation. To evaluate a list of formulas for a subset, there is another method evaluateForGivenStates.

'''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., <code>"1<4" & "x>y"</code> evaluates to <code>"(1<4) & (x>y)"</code>. 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. <code>"1<2".implies("3<4")</code> results in <code>"(1<2) => (3<4)"</code>. The last line converts a list of predicates into a conjunction. In Groovy collect means map and inject means reduce.

== 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))

== 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, <code>animations</code> and <code>api</code>.

<code>animations</code> is an Instance of <code>AnimationSelector</code>, <code>api</code> is an instance of <code>Api</code>. 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)

==Additional Resources==

Further information can be found in the [[Developer_Manual|developer manual]].

{{Feedback}}

Rodin User and Developer Workshop 2013 - Tutorial

2015-05-05T07:48:54Z

Joy Clark: /* Preparation */

[[Category:ProB Java API]]

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 [[media:Scheduler_tutorial2013.zip|simple scheduler example]]. Maybe you have to clean the project after importing.

== 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 '''<code>upgrade "latest"</code>''' 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.

== Preparation ==

# Import the Scheduler project.
# Start an animation for Scheduler0
# Perform some random animation steps
# Type <code>s = animations.getCurrentTrace() as StateSpace</code> into the Groovy console. <code>animations.getCurrentTrace()</code> accesses the current animation and <code>as StateSpace</code> accesses the current state space associated with the current animation.

== 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()

== The State Space ==
The state space represents the whole currently known world for an animation. It is lazily explored, i.e., the knowledge always increases. The class is based on a Graph from the [http://jung.sourceforge.net/ JUNG] framework. However, we hide methods that can remove information from the graph. The StateSpace class also provides notification mechanism to inform clients about important changes, such as the exploration of new states.

'''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 <code>massakr</code> event. This event breaks the invariant of the system. Otherwise the next command will return an empty set.

'''Are there some states that violate the invariant?'''
s.getInvariantKo()

'''Are there some states where the invariant holds?'''
s.getInvariantOk()

'''What kind of object is the result? '''
s.getInvariantOk().getClass()

'''What kind of objects are contained in the set? '''
s.getInvariantOk().first().getClass()

'''Let's explore StateIds.'''
x = s.getInvariantOk().first()

'''Can we get the value of a variable in that state?'''
x.value("active")

'''Can we randomly "execute" events?'''
y = x.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?'''
s.getOutEdges(x)

'''What are the elements of the hashset?'''
s.getOutEdges(x).first().getClass()

'''Now let's get one of these OpInfo objects'''
o = (s.getOutEdges(x) as List)[1]

Groovy allows us to transform a Set into a list using the Groovy [http://silvanolte.com/blog/2011/03/11/the-groovy-as-keyword/ as] keyword.

'''What is the name of the operation?'''
n = o.getName()

'''What are the actual parameters?'''
n = o.getParams()

'''What is the formal parameter name?'''
e = mch.getEvent(o.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

'''x.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 space, and the detail information from the OpInfo 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,x,name,params) {
formal_params = mch.getEvent(name).getParameters()
pred = [formal_params,params].transpose()
.collect { a,b -> a.toString() + "=" + b.toString() }
x.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")

== 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().getId())

'''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 ==
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.evaluateForEveryState([f1, "waiting" as EventB])

evaluateForEveryState takes a list of formulas and evaluates them for each state of the statespace. This method is not called eval to prevent accidental evaluation. To evaluate a list of formulas for a subset, there is another method evaluateForGivenStates.

'''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., <code>"1<4" & "x>y"</code> evaluates to <code>"(1<4) & (x>y)"</code>. 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. <code>"1<2".implies("3<4")</code> results in <code>"(1<2) => (3<4)"</code>. The last line converts a list of predicates into a conjunction. In Groovy collect means map and inject means reduce.

== 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))

== 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, <code>animations</code> and <code>api</code>.

<code>animations</code> is an Instance of <code>AnimationSelector</code>, <code>api</code> is an instance of <code>Api</code>. 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)

==Additional Resources==

Further information can be found in the [[Developer_Manual|developer manual]].

{{Feedback}}

ProB Java API Tutorial

2014-11-05T15:08:58Z

Joy Clark: /* How to run a groovy script */

[[Category:ProB Java API]]

ProB 2.0 is currently experimental. This means that the implementation may change during the course of development. However, we have reached the point in development where some of the features have reached a certain level of stability. Therefore, we are writing this tutorial to explain what those features are.

== How to get started developing with ProB 2.0 ==

The source code for ProB 2.0 is available via GitHub. Click [https://github.com/bendisposto/prob2 here] to view the prob2 repository. There is also a short guide available there which will help getting Eclipse set up so that you can get started with the development. Our bugtracker is available [http://jira.cobra.cs.uni-duesseldorf.de/browse/PROBCORE here]. There you can view the features that we are currently working on and can submit new feature requests.

== How to open the Groovy Shell ==

The ProB Groovy shell is available in the Eclipse application. To open it, select

<tt> Window > Show View > Other.. </tt>

Then select

<tt> ProB > Groovy Console </tt>

and hit <tt> ok</tt>.

== Open the ProB API from Source/JAR file ==

In order to access the console from source or from a JAR file, start the application with the parameters -s (short for --shell) and -local (which specifies that you are running the application from a local computer). This will start a web server at a given port (the default is 8080, but it increments the port number if a port is already active). The shell can then be accessed at the following address:

localhost:PORTNR/sessions/GroovyConsoleSession

== How to load a model ==

=== Classical B ===

You can load a Classical B model into the groovy console using the <tt> api </tt> variable that is available. There is a method <tt> b_load </tt> that is available to load Classical B models. For example:

<tt> m = api.b_load("/home/pathToFile/example.mch") </tt>

will load example.mch into the variable <tt>m</tt>.

=== Event B ===

To load an Event B model into ProB, right click on the model and select

<tt> Start Animation / Model Checking </tt>

from the context menu that drops down.

You can also load Event B models into the API via the eventb_load command in the Api object. The eventb_load command accepts .bcm and .bcc files.

== How to animate models ==

The Trace abstraction is available to carry out animations.

=== In The Console ===

There are several different ways that a new transition can be added to the current trace. The most important thing to remember is that each Trace object is completely immutable. This means that when you change a trace, you are actually getting a new Trace back. This means that when you carry out an animation step, you always have to make sure that you save the Trace object that is returned.

The simplest way to add a transition is to specify it with the name of the event to be executed and predicates to specify how the parameters for the event are to be allocated. Specifying no predicate will assume a predicate of "TRUE=TRUE" for the given event.

<tt> t = t.execute("new","pp=PID1") </tt>

If executing the event in a groovy environment (console or script), the event will be recognized as a method on the Trace class. This means that you can execute the event "new" as follows:

<tt> t = t.new("pp=PID1") </tt>

If you know the id that has been allocated by the ProB kernel to a given transition, this can be added via the "add" method. This will search the outgoing transitions from the current state and attempts to find one with a matching id. For instance, if operation 0 is among the enabled operations for the current state, then

<tt> t = t.add(0) </tt>

will add operation 0 to the current trace, create a new trace, and return it.

If you know the name and parameters combination for a specific transition, you can also add operations via operation name and a list of the parameters. For instance

<tt> t = t.addTransitionWith("new",["PID3"]) </tt>

will add the transition new(PID3) to the trace.

It is also possible to execute any event by executing

<tt> t = t.anyEvent() </tt>

and it is also possible to execute any event with name "name". For instance,

<tt> t = t.anyEvent("name") </tt>

will execute any event with the name "name".

It also possible to move backwards and forwards within a trace.

Move backwards:

<tt> t = t.back() </tt>

Move forwards:

<tt> t = t.forward() </tt>

=== In The UI ===

In order to animate a loaded model in the UI, double-click on an enabled event in the <tt>Events</tt> view. Then, the resulting trace will automatically be loaded into the different views and it can be further animated. To move backwards and forwards in the trace, use the buttons in the upper right hand corner of the <tt>Events</tt> view.

== How to switch from UI to groovy console ==

There is an easy way to switch from the UI to the groovy console and back. It all happens using the "animations" global variable in the groovy console. What is important to remember, is that in this case, there is no distinction between an animation and a trace.

=== From UI to Console ===

In the UI, switch to the <tt>Current Animations</tt> view. Here you can view the different animations that are available. If the desired animation is not available, double click on it in this view and it will be set as the current animation. Now, to move this animation from the UI to the groovy console, simply type

<tt> x = animations.getCurrentTrace() </tt>

into the groovy console and the current animation will be loaded into the variable <tt>x</tt>.

=== From the Console to the UI ===

If you have a trace saved into variable <tt>trace_0</tt> in the groovy console, you can easily add it to the UI. Simply type

<tt> animations.addNewAnimation(trace_0) </tt>

into the groovy console and the trace will automatically be added to the list of current animations and all of the views will be updated.

== How to carry out evaluations ==

It is very simple to evaluate strings in the groovy console. There is a build in eval method in both the Trace and the StateSpace. In the trace, you just need to specify a string and the parser that is needed to parse the string. The two parsers currently available are <tt>ClassicalB</tt> and <tt>EventB</tt>.For instance,

<tt> t.evalCurrent("x:NAT" as EventB) </tt>

will parse "x:NAT" using the Event B parser and then will evaluate it at the current state. The following code

<tt> t.evalCurrent("x:NAT" as ClassicalB) </tt>

will parse "x:NAT" using the Classical B parser and then will evaluate it at the current state.

The Trace class can also attempt to identify the correct parser for the formula in question. This means that for an EventBModel the EventB parser will be used, and for a ClassicalBModel, the ClassicalB parser will be used. In this case, calling the evalCurrent method with a String parameter will parse the String formula with the parser associated with the current formalism being animated. In this case

<tt> t.eval("x:NAT")</tt>.

will identify which model type is being animated and choose the appropriate parser.

It is also possible to evaluate formulas on the SpaceSpace level. For instance, if <tt>space_0</tt> is a StateSpace, you can evaluate a list of formulas by typing

<tt> space_0.eval(space_0[5],["x:NAT" as EventB,"y:NAT" as ClassicalB]) </tt>

into the console. This will parse "x:NAT" with the Event B parser and "y:NAT" with the Classical B parser and then will evaluate them at the state with id 5. The parser is not implicit in the StateSpace, so it is important to specify it here. In order to evaluate a formula, you need to specify the StateId object that is associated with the desired id. To extract a StateId from a StateSpace, you can use the notation <tt>space[ID]</tt> where ID is either a String or an integer representing the StateId that you want to view.

== How to convert between the main abstractions ==

There is a connection between all of the main abstractions. You can easily convert between them by using the <tt>as</tt> operator.

To convert between a Model and a StateSpace, use:

<tt> eventb = statespace_0 as EventBModel </tt> (if you are animating an Event B model)

or

<tt> classicalb = statespace_0 as ClassicalBModel </tt> (if you are animating ClassicalB).

The reverse translation is just as easy:

<tt> space = model as StateSpace </tt>

will return the StateSpace associated with model.

Conversion between a Trace and a StateSpace and between a Trace and Model are also simple. The following conversions are valid:

<tt> space = trace as StateSpace </tt>

<tt> trace = StateSpace as Trace </tt>

<tt> trace = model as Trace </tt>

<tt> model = trace as EventBModel </tt> or <tt> model = trace as ClassicalBModel </tt>

The only thing to mention is that every time you convert from a StateSpace or Model to a Trace, a new trace from the root state is created.

== How to save a trace ==

ProB currently supports a mechanism to save a trace in a script so that the same trace can be recreated. We are currently working on some improvements to this mechanism, so expect it to change over the next period of time. Currently, it is possible to save a Trace as an XML trace by typing

<tt>TraceConverter.save(trace_0,"/pathToFile/fileName.xml")</tt>

into the console. This will create the XML file <tt>fileName.xml</tt>.

If you want to load this trace back into the console, there are two options available. You can convert the XML file to a Groovy closure that will then take a Model object and return a Trace with all of the operations specified in the XML file. This can be triggered by calling the method

<tt>TraceConverter.xmlToGroovy("/pathToFile/fileName.xml","/pathToFile/groovyScript.groovy")</tt>

You can then run the produced Groovy script and execute the resulting closure to restore your Trace

<tt>run /pathToFile/groovyScript.groovy</tt>

A script <tt>script_NUM</tt> will be produced. Then enter

<tt> trace = script_NUM(modelForThisTrace) </tt>

into the console, where modelForThisTrace is the model for which the trace should be executed.

Another option is to simply restore the Trace directly from the TraceConverter

<tt> trace = TraceConverter.restore(modelForThisTrace,"/pathToFile/fileName.xml")</tt>

== How to run a groovy script ==

You can use the build in <tt>run</tt> command to run a groovy script. Simply type

<tt> run new File(pathToScript/script.groovy) </tt>

into the console.

== How to animate with only the StateSpace abstraction ==

It is also possible to carry out animations without using a trace object.

To get the root vertex from StateSpace space_0, type:

<tt> st = space_0.root </tt>

from there, you can execute a chain of events. For instance,

<tt> st = st.anyEvent("new").anyEvent().new("pp=PID1").new() </tt>

So you can execute anyEvent with the method anyEvent(filter), where filter can be a String name, or a List of names. You can also execute an event with name "name", with the method name(predicate), where predicate is the predicate string intended to filter the solutions for the event. If there are no parameters, the predicate "TRUE = TRUE" will automatically be added.

ProB Java API Tutorial

2014-11-05T15:08:28Z

Joy Clark: /* How to convert between the main abstractions */

[[Category:ProB Java API]]

ProB 2.0 is currently experimental. This means that the implementation may change during the course of development. However, we have reached the point in development where some of the features have reached a certain level of stability. Therefore, we are writing this tutorial to explain what those features are.

== How to get started developing with ProB 2.0 ==

The source code for ProB 2.0 is available via GitHub. Click [https://github.com/bendisposto/prob2 here] to view the prob2 repository. There is also a short guide available there which will help getting Eclipse set up so that you can get started with the development. Our bugtracker is available [http://jira.cobra.cs.uni-duesseldorf.de/browse/PROBCORE here]. There you can view the features that we are currently working on and can submit new feature requests.

== How to open the Groovy Shell ==

The ProB Groovy shell is available in the Eclipse application. To open it, select

<tt> Window > Show View > Other.. </tt>

Then select

<tt> ProB > Groovy Console </tt>

and hit <tt> ok</tt>.

== Open the ProB API from Source/JAR file ==

In order to access the console from source or from a JAR file, start the application with the parameters -s (short for --shell) and -local (which specifies that you are running the application from a local computer). This will start a web server at a given port (the default is 8080, but it increments the port number if a port is already active). The shell can then be accessed at the following address:

localhost:PORTNR/sessions/GroovyConsoleSession

== How to load a model ==

=== Classical B ===

You can load a Classical B model into the groovy console using the <tt> api </tt> variable that is available. There is a method <tt> b_load </tt> that is available to load Classical B models. For example:

<tt> m = api.b_load("/home/pathToFile/example.mch") </tt>

will load example.mch into the variable <tt>m</tt>.

=== Event B ===

To load an Event B model into ProB, right click on the model and select

<tt> Start Animation / Model Checking </tt>

from the context menu that drops down.

You can also load Event B models into the API via the eventb_load command in the Api object. The eventb_load command accepts .bcm and .bcc files.

== How to animate models ==

The Trace abstraction is available to carry out animations.

=== In The Console ===

There are several different ways that a new transition can be added to the current trace. The most important thing to remember is that each Trace object is completely immutable. This means that when you change a trace, you are actually getting a new Trace back. This means that when you carry out an animation step, you always have to make sure that you save the Trace object that is returned.

The simplest way to add a transition is to specify it with the name of the event to be executed and predicates to specify how the parameters for the event are to be allocated. Specifying no predicate will assume a predicate of "TRUE=TRUE" for the given event.

<tt> t = t.execute("new","pp=PID1") </tt>

If executing the event in a groovy environment (console or script), the event will be recognized as a method on the Trace class. This means that you can execute the event "new" as follows:

<tt> t = t.new("pp=PID1") </tt>

If you know the id that has been allocated by the ProB kernel to a given transition, this can be added via the "add" method. This will search the outgoing transitions from the current state and attempts to find one with a matching id. For instance, if operation 0 is among the enabled operations for the current state, then

<tt> t = t.add(0) </tt>

will add operation 0 to the current trace, create a new trace, and return it.

If you know the name and parameters combination for a specific transition, you can also add operations via operation name and a list of the parameters. For instance

<tt> t = t.addTransitionWith("new",["PID3"]) </tt>

will add the transition new(PID3) to the trace.

It is also possible to execute any event by executing

<tt> t = t.anyEvent() </tt>

and it is also possible to execute any event with name "name". For instance,

<tt> t = t.anyEvent("name") </tt>

will execute any event with the name "name".

It also possible to move backwards and forwards within a trace.

Move backwards:

<tt> t = t.back() </tt>

Move forwards:

<tt> t = t.forward() </tt>

=== In The UI ===

In order to animate a loaded model in the UI, double-click on an enabled event in the <tt>Events</tt> view. Then, the resulting trace will automatically be loaded into the different views and it can be further animated. To move backwards and forwards in the trace, use the buttons in the upper right hand corner of the <tt>Events</tt> view.

== How to switch from UI to groovy console ==

There is an easy way to switch from the UI to the groovy console and back. It all happens using the "animations" global variable in the groovy console. What is important to remember, is that in this case, there is no distinction between an animation and a trace.

=== From UI to Console ===

In the UI, switch to the <tt>Current Animations</tt> view. Here you can view the different animations that are available. If the desired animation is not available, double click on it in this view and it will be set as the current animation. Now, to move this animation from the UI to the groovy console, simply type

<tt> x = animations.getCurrentTrace() </tt>

into the groovy console and the current animation will be loaded into the variable <tt>x</tt>.

=== From the Console to the UI ===

If you have a trace saved into variable <tt>trace_0</tt> in the groovy console, you can easily add it to the UI. Simply type

<tt> animations.addNewAnimation(trace_0) </tt>

into the groovy console and the trace will automatically be added to the list of current animations and all of the views will be updated.

== How to carry out evaluations ==

It is very simple to evaluate strings in the groovy console. There is a build in eval method in both the Trace and the StateSpace. In the trace, you just need to specify a string and the parser that is needed to parse the string. The two parsers currently available are <tt>ClassicalB</tt> and <tt>EventB</tt>.For instance,

<tt> t.evalCurrent("x:NAT" as EventB) </tt>

will parse "x:NAT" using the Event B parser and then will evaluate it at the current state. The following code

<tt> t.evalCurrent("x:NAT" as ClassicalB) </tt>

will parse "x:NAT" using the Classical B parser and then will evaluate it at the current state.

The Trace class can also attempt to identify the correct parser for the formula in question. This means that for an EventBModel the EventB parser will be used, and for a ClassicalBModel, the ClassicalB parser will be used. In this case, calling the evalCurrent method with a String parameter will parse the String formula with the parser associated with the current formalism being animated. In this case

<tt> t.eval("x:NAT")</tt>.

will identify which model type is being animated and choose the appropriate parser.

It is also possible to evaluate formulas on the SpaceSpace level. For instance, if <tt>space_0</tt> is a StateSpace, you can evaluate a list of formulas by typing

<tt> space_0.eval(space_0[5],["x:NAT" as EventB,"y:NAT" as ClassicalB]) </tt>

into the console. This will parse "x:NAT" with the Event B parser and "y:NAT" with the Classical B parser and then will evaluate them at the state with id 5. The parser is not implicit in the StateSpace, so it is important to specify it here. In order to evaluate a formula, you need to specify the StateId object that is associated with the desired id. To extract a StateId from a StateSpace, you can use the notation <tt>space[ID]</tt> where ID is either a String or an integer representing the StateId that you want to view.

== How to convert between the main abstractions ==

There is a connection between all of the main abstractions. You can easily convert between them by using the <tt>as</tt> operator.

To convert between a Model and a StateSpace, use:

<tt> eventb = statespace_0 as EventBModel </tt> (if you are animating an Event B model)

or

<tt> classicalb = statespace_0 as ClassicalBModel </tt> (if you are animating ClassicalB).

The reverse translation is just as easy:

<tt> space = model as StateSpace </tt>

will return the StateSpace associated with model.

Conversion between a Trace and a StateSpace and between a Trace and Model are also simple. The following conversions are valid:

<tt> space = trace as StateSpace </tt>

<tt> trace = StateSpace as Trace </tt>

<tt> trace = model as Trace </tt>

<tt> model = trace as EventBModel </tt> or <tt> model = trace as ClassicalBModel </tt>

The only thing to mention is that every time you convert from a StateSpace or Model to a Trace, a new trace from the root state is created.

== How to save a trace ==

ProB currently supports a mechanism to save a trace in a script so that the same trace can be recreated. We are currently working on some improvements to this mechanism, so expect it to change over the next period of time. Currently, it is possible to save a Trace as an XML trace by typing

<tt>TraceConverter.save(trace_0,"/pathToFile/fileName.xml")</tt>

into the console. This will create the XML file <tt>fileName.xml</tt>.

If you want to load this trace back into the console, there are two options available. You can convert the XML file to a Groovy closure that will then take a Model object and return a Trace with all of the operations specified in the XML file. This can be triggered by calling the method

<tt>TraceConverter.xmlToGroovy("/pathToFile/fileName.xml","/pathToFile/groovyScript.groovy")</tt>

You can then run the produced Groovy script and execute the resulting closure to restore your Trace

<tt>run /pathToFile/groovyScript.groovy</tt>

A script <tt>script_NUM</tt> will be produced. Then enter

<tt> trace = script_NUM(modelForThisTrace) </tt>

into the console, where modelForThisTrace is the model for which the trace should be executed.

Another option is to simply restore the Trace directly from the TraceConverter

<tt> trace = TraceConverter.restore(modelForThisTrace,"/pathToFile/fileName.xml")</tt>

== How to run a groovy script ==

You can use the build in <tt>run</tt> command to run a groovy script. Simply type

<tt> run pathToScript/script.groovy </tt>

into the console. Code completion is available for the run command.

== How to animate with only the StateSpace abstraction ==

It is also possible to carry out animations without using a trace object.

To get the root vertex from StateSpace space_0, type:

<tt> st = space_0.root </tt>

from there, you can execute a chain of events. For instance,

<tt> st = st.anyEvent("new").anyEvent().new("pp=PID1").new() </tt>

So you can execute anyEvent with the method anyEvent(filter), where filter can be a String name, or a List of names. You can also execute an event with name "name", with the method name(predicate), where predicate is the predicate string intended to filter the solutions for the event. If there are no parameters, the predicate "TRUE = TRUE" will automatically be added.

ProB Java API Tutorial

2014-11-05T15:08:03Z

Joy Clark: /* How to carry out evaluations */

[[Category:ProB Java API]]

ProB 2.0 is currently experimental. This means that the implementation may change during the course of development. However, we have reached the point in development where some of the features have reached a certain level of stability. Therefore, we are writing this tutorial to explain what those features are.

== How to get started developing with ProB 2.0 ==

The source code for ProB 2.0 is available via GitHub. Click [https://github.com/bendisposto/prob2 here] to view the prob2 repository. There is also a short guide available there which will help getting Eclipse set up so that you can get started with the development. Our bugtracker is available [http://jira.cobra.cs.uni-duesseldorf.de/browse/PROBCORE here]. There you can view the features that we are currently working on and can submit new feature requests.

== How to open the Groovy Shell ==

The ProB Groovy shell is available in the Eclipse application. To open it, select

<tt> Window > Show View > Other.. </tt>

Then select

<tt> ProB > Groovy Console </tt>

and hit <tt> ok</tt>.

== Open the ProB API from Source/JAR file ==

In order to access the console from source or from a JAR file, start the application with the parameters -s (short for --shell) and -local (which specifies that you are running the application from a local computer). This will start a web server at a given port (the default is 8080, but it increments the port number if a port is already active). The shell can then be accessed at the following address:

localhost:PORTNR/sessions/GroovyConsoleSession

== How to load a model ==

=== Classical B ===

You can load a Classical B model into the groovy console using the <tt> api </tt> variable that is available. There is a method <tt> b_load </tt> that is available to load Classical B models. For example:

<tt> m = api.b_load("/home/pathToFile/example.mch") </tt>

will load example.mch into the variable <tt>m</tt>.

=== Event B ===

To load an Event B model into ProB, right click on the model and select

<tt> Start Animation / Model Checking </tt>

from the context menu that drops down.

You can also load Event B models into the API via the eventb_load command in the Api object. The eventb_load command accepts .bcm and .bcc files.

== How to animate models ==

The Trace abstraction is available to carry out animations.

=== In The Console ===

There are several different ways that a new transition can be added to the current trace. The most important thing to remember is that each Trace object is completely immutable. This means that when you change a trace, you are actually getting a new Trace back. This means that when you carry out an animation step, you always have to make sure that you save the Trace object that is returned.

The simplest way to add a transition is to specify it with the name of the event to be executed and predicates to specify how the parameters for the event are to be allocated. Specifying no predicate will assume a predicate of "TRUE=TRUE" for the given event.

<tt> t = t.execute("new","pp=PID1") </tt>

If executing the event in a groovy environment (console or script), the event will be recognized as a method on the Trace class. This means that you can execute the event "new" as follows:

<tt> t = t.new("pp=PID1") </tt>

If you know the id that has been allocated by the ProB kernel to a given transition, this can be added via the "add" method. This will search the outgoing transitions from the current state and attempts to find one with a matching id. For instance, if operation 0 is among the enabled operations for the current state, then

<tt> t = t.add(0) </tt>

will add operation 0 to the current trace, create a new trace, and return it.

If you know the name and parameters combination for a specific transition, you can also add operations via operation name and a list of the parameters. For instance

<tt> t = t.addTransitionWith("new",["PID3"]) </tt>

will add the transition new(PID3) to the trace.

It is also possible to execute any event by executing

<tt> t = t.anyEvent() </tt>

and it is also possible to execute any event with name "name". For instance,

<tt> t = t.anyEvent("name") </tt>

will execute any event with the name "name".

It also possible to move backwards and forwards within a trace.

Move backwards:

<tt> t = t.back() </tt>

Move forwards:

<tt> t = t.forward() </tt>

=== In The UI ===

In order to animate a loaded model in the UI, double-click on an enabled event in the <tt>Events</tt> view. Then, the resulting trace will automatically be loaded into the different views and it can be further animated. To move backwards and forwards in the trace, use the buttons in the upper right hand corner of the <tt>Events</tt> view.

== How to switch from UI to groovy console ==

There is an easy way to switch from the UI to the groovy console and back. It all happens using the "animations" global variable in the groovy console. What is important to remember, is that in this case, there is no distinction between an animation and a trace.

=== From UI to Console ===

In the UI, switch to the <tt>Current Animations</tt> view. Here you can view the different animations that are available. If the desired animation is not available, double click on it in this view and it will be set as the current animation. Now, to move this animation from the UI to the groovy console, simply type

<tt> x = animations.getCurrentTrace() </tt>

into the groovy console and the current animation will be loaded into the variable <tt>x</tt>.

=== From the Console to the UI ===

If you have a trace saved into variable <tt>trace_0</tt> in the groovy console, you can easily add it to the UI. Simply type

<tt> animations.addNewAnimation(trace_0) </tt>

into the groovy console and the trace will automatically be added to the list of current animations and all of the views will be updated.

== How to carry out evaluations ==

It is very simple to evaluate strings in the groovy console. There is a build in eval method in both the Trace and the StateSpace. In the trace, you just need to specify a string and the parser that is needed to parse the string. The two parsers currently available are <tt>ClassicalB</tt> and <tt>EventB</tt>.For instance,

<tt> t.evalCurrent("x:NAT" as EventB) </tt>

will parse "x:NAT" using the Event B parser and then will evaluate it at the current state. The following code

<tt> t.evalCurrent("x:NAT" as ClassicalB) </tt>

will parse "x:NAT" using the Classical B parser and then will evaluate it at the current state.

The Trace class can also attempt to identify the correct parser for the formula in question. This means that for an EventBModel the EventB parser will be used, and for a ClassicalBModel, the ClassicalB parser will be used. In this case, calling the evalCurrent method with a String parameter will parse the String formula with the parser associated with the current formalism being animated. In this case

<tt> t.eval("x:NAT")</tt>.

will identify which model type is being animated and choose the appropriate parser.

It is also possible to evaluate formulas on the SpaceSpace level. For instance, if <tt>space_0</tt> is a StateSpace, you can evaluate a list of formulas by typing

<tt> space_0.eval(space_0[5],["x:NAT" as EventB,"y:NAT" as ClassicalB]) </tt>

into the console. This will parse "x:NAT" with the Event B parser and "y:NAT" with the Classical B parser and then will evaluate them at the state with id 5. The parser is not implicit in the StateSpace, so it is important to specify it here. In order to evaluate a formula, you need to specify the StateId object that is associated with the desired id. To extract a StateId from a StateSpace, you can use the notation <tt>space[ID]</tt> where ID is either a String or an integer representing the StateId that you want to view.

== How to convert between the main abstractions ==

There is a connection between all of the main abstractions. You can easily convert between them by using the <tt>as</tt> operator.

To convert between a Model and a StateSpace, use:

<tt> eventb = statespace_0 as EventBModel </tt> (if you are animating an Event B model)

or

<tt> classicalb = statespace_0 as ClassicalBModel </tt> (if you are animating ClassicalB).

The reverse translation is just as easy:

<tt> space = model as StateSpace </tt>

will return the StateSpace associated with model.

Conversion between a Trace and a StateSpace and between a Trace and Model are also simple. The following conversions are valid:

<tt> space = trace as StateSpace </tt>

<tt> trace = StateSpace as Trace </tt>

<tt> trace = model as Trace </tt>

<tt> model = trace as EventBModel </tt> or <tt> model = trace as ClassicalBModel </tt>

The only thing to mention is that every time you convert from a StateSpace or Model to a Trace, a new trace is created.

== How to save a trace ==

ProB currently supports a mechanism to save a trace in a script so that the same trace can be recreated. We are currently working on some improvements to this mechanism, so expect it to change over the next period of time. Currently, it is possible to save a Trace as an XML trace by typing

<tt>TraceConverter.save(trace_0,"/pathToFile/fileName.xml")</tt>

into the console. This will create the XML file <tt>fileName.xml</tt>.

If you want to load this trace back into the console, there are two options available. You can convert the XML file to a Groovy closure that will then take a Model object and return a Trace with all of the operations specified in the XML file. This can be triggered by calling the method

<tt>TraceConverter.xmlToGroovy("/pathToFile/fileName.xml","/pathToFile/groovyScript.groovy")</tt>

You can then run the produced Groovy script and execute the resulting closure to restore your Trace

<tt>run /pathToFile/groovyScript.groovy</tt>

A script <tt>script_NUM</tt> will be produced. Then enter

<tt> trace = script_NUM(modelForThisTrace) </tt>

into the console, where modelForThisTrace is the model for which the trace should be executed.

Another option is to simply restore the Trace directly from the TraceConverter

<tt> trace = TraceConverter.restore(modelForThisTrace,"/pathToFile/fileName.xml")</tt>

== How to run a groovy script ==

You can use the build in <tt>run</tt> command to run a groovy script. Simply type

<tt> run pathToScript/script.groovy </tt>

into the console. Code completion is available for the run command.

== How to animate with only the StateSpace abstraction ==

It is also possible to carry out animations without using a trace object.

To get the root vertex from StateSpace space_0, type:

<tt> st = space_0.root </tt>

from there, you can execute a chain of events. For instance,

<tt> st = st.anyEvent("new").anyEvent().new("pp=PID1").new() </tt>

So you can execute anyEvent with the method anyEvent(filter), where filter can be a String name, or a List of names. You can also execute an event with name "name", with the method name(predicate), where predicate is the predicate string intended to filter the solutions for the event. If there are no parameters, the predicate "TRUE = TRUE" will automatically be added.

ProB Java API Tutorial

2014-11-05T15:04:08Z

Joy Clark: /* In The Console */

[[Category:ProB Java API]]

ProB 2.0 is currently experimental. This means that the implementation may change during the course of development. However, we have reached the point in development where some of the features have reached a certain level of stability. Therefore, we are writing this tutorial to explain what those features are.

== How to get started developing with ProB 2.0 ==

The source code for ProB 2.0 is available via GitHub. Click [https://github.com/bendisposto/prob2 here] to view the prob2 repository. There is also a short guide available there which will help getting Eclipse set up so that you can get started with the development. Our bugtracker is available [http://jira.cobra.cs.uni-duesseldorf.de/browse/PROBCORE here]. There you can view the features that we are currently working on and can submit new feature requests.

== How to open the Groovy Shell ==

The ProB Groovy shell is available in the Eclipse application. To open it, select

<tt> Window > Show View > Other.. </tt>

Then select

<tt> ProB > Groovy Console </tt>

and hit <tt> ok</tt>.

== Open the ProB API from Source/JAR file ==

In order to access the console from source or from a JAR file, start the application with the parameters -s (short for --shell) and -local (which specifies that you are running the application from a local computer). This will start a web server at a given port (the default is 8080, but it increments the port number if a port is already active). The shell can then be accessed at the following address:

localhost:PORTNR/sessions/GroovyConsoleSession

== How to load a model ==

=== Classical B ===

You can load a Classical B model into the groovy console using the <tt> api </tt> variable that is available. There is a method <tt> b_load </tt> that is available to load Classical B models. For example:

<tt> m = api.b_load("/home/pathToFile/example.mch") </tt>

will load example.mch into the variable <tt>m</tt>.

=== Event B ===

To load an Event B model into ProB, right click on the model and select

<tt> Start Animation / Model Checking </tt>

from the context menu that drops down.

You can also load Event B models into the API via the eventb_load command in the Api object. The eventb_load command accepts .bcm and .bcc files.

== How to animate models ==

The Trace abstraction is available to carry out animations.

=== In The Console ===

There are several different ways that a new transition can be added to the current trace. The most important thing to remember is that each Trace object is completely immutable. This means that when you change a trace, you are actually getting a new Trace back. This means that when you carry out an animation step, you always have to make sure that you save the Trace object that is returned.

The simplest way to add a transition is to specify it with the name of the event to be executed and predicates to specify how the parameters for the event are to be allocated. Specifying no predicate will assume a predicate of "TRUE=TRUE" for the given event.

<tt> t = t.execute("new","pp=PID1") </tt>

If executing the event in a groovy environment (console or script), the event will be recognized as a method on the Trace class. This means that you can execute the event "new" as follows:

<tt> t = t.new("pp=PID1") </tt>

If you know the id that has been allocated by the ProB kernel to a given transition, this can be added via the "add" method. This will search the outgoing transitions from the current state and attempts to find one with a matching id. For instance, if operation 0 is among the enabled operations for the current state, then

<tt> t = t.add(0) </tt>

will add operation 0 to the current trace, create a new trace, and return it.

If you know the name and parameters combination for a specific transition, you can also add operations via operation name and a list of the parameters. For instance

<tt> t = t.addTransitionWith("new",["PID3"]) </tt>

will add the transition new(PID3) to the trace.

It is also possible to execute any event by executing

<tt> t = t.anyEvent() </tt>

and it is also possible to execute any event with name "name". For instance,

<tt> t = t.anyEvent("name") </tt>

will execute any event with the name "name".

It also possible to move backwards and forwards within a trace.

Move backwards:

<tt> t = t.back() </tt>

Move forwards:

<tt> t = t.forward() </tt>

=== In The UI ===

In order to animate a loaded model in the UI, double-click on an enabled event in the <tt>Events</tt> view. Then, the resulting trace will automatically be loaded into the different views and it can be further animated. To move backwards and forwards in the trace, use the buttons in the upper right hand corner of the <tt>Events</tt> view.

== How to switch from UI to groovy console ==

There is an easy way to switch from the UI to the groovy console and back. It all happens using the "animations" global variable in the groovy console. What is important to remember, is that in this case, there is no distinction between an animation and a trace.

=== From UI to Console ===

In the UI, switch to the <tt>Current Animations</tt> view. Here you can view the different animations that are available. If the desired animation is not available, double click on it in this view and it will be set as the current animation. Now, to move this animation from the UI to the groovy console, simply type

<tt> x = animations.getCurrentTrace() </tt>

into the groovy console and the current animation will be loaded into the variable <tt>x</tt>.

=== From the Console to the UI ===

If you have a trace saved into variable <tt>trace_0</tt> in the groovy console, you can easily add it to the UI. Simply type

<tt> animations.addNewAnimation(trace_0) </tt>

into the groovy console and the trace will automatically be added to the list of current animations and all of the views will be updated.

== How to carry out evaluations ==

It is very simple to evaluate strings in the groovy console. There is a build in eval method in both the Trace and the StateSpace. In the trace, you just need to specify a string and the parser that is needed to parse the string. The two parsers currently available are <tt>ClassicalB</tt> and <tt>EventB</tt>.For instance,

<tt> t.eval("x:NAT" as EventB) </tt>

will parse "x:NAT" using the Event B parser and then will evaluate it at the current state. The following code

<tt> t.eval("x:NAT" as ClassicalB) </tt>

will parse "x:NAT" using the Classical B parser and then will evaluate it at the current state.

Classical B is actually the default parser, so it would also be sufficient to write

<tt> t.eval("x:NAT")</tt>.

It is also possible to evaluate formulas on the SpaceSpace level. For instance, if <tt>space_0</tt> is a StateSpace, you can evaluate a list of formulas by typing

<tt> space_0.eval(space_0[5],["x:NAT" as EventB,"y:NAT" as ClassicalB]) </tt>

into the console. This will parse "x:NAT" with the Event B parser and "y:NAT" with the Classical B parser and then will evaluate them at the state with id 5. The parser is not implicit in the StateSpace, so it is important to specify it here. In order to evaluate a formula, you need to specify the StateId object that is associated with the desired id. To extract a StateId from a StateSpace, you can use the notation <tt>space[ID]</tt> where ID is either a String or an integer representing the StateId that you want to view.

== How to convert between the main abstractions ==

There is a connection between all of the main abstractions. You can easily convert between them by using the <tt>as</tt> operator.

To convert between a Model and a StateSpace, use:

<tt> eventb = statespace_0 as EventBModel </tt> (if you are animating an Event B model)

or

<tt> classicalb = statespace_0 as ClassicalBModel </tt> (if you are animating ClassicalB).

The reverse translation is just as easy:

<tt> space = model as StateSpace </tt>

will return the StateSpace associated with model.

Conversion between a Trace and a StateSpace and between a Trace and Model are also simple. The following conversions are valid:

<tt> space = trace as StateSpace </tt>

<tt> trace = StateSpace as Trace </tt>

<tt> trace = model as Trace </tt>

<tt> model = trace as EventBModel </tt> or <tt> model = trace as ClassicalBModel </tt>

The only thing to mention is that every time you convert from a StateSpace or Model to a Trace, a new trace is created.

== How to save a trace ==

ProB currently supports a mechanism to save a trace in a script so that the same trace can be recreated. We are currently working on some improvements to this mechanism, so expect it to change over the next period of time. Currently, it is possible to save a Trace as an XML trace by typing

<tt>TraceConverter.save(trace_0,"/pathToFile/fileName.xml")</tt>

into the console. This will create the XML file <tt>fileName.xml</tt>.

If you want to load this trace back into the console, there are two options available. You can convert the XML file to a Groovy closure that will then take a Model object and return a Trace with all of the operations specified in the XML file. This can be triggered by calling the method

<tt>TraceConverter.xmlToGroovy("/pathToFile/fileName.xml","/pathToFile/groovyScript.groovy")</tt>

You can then run the produced Groovy script and execute the resulting closure to restore your Trace

<tt>run /pathToFile/groovyScript.groovy</tt>

A script <tt>script_NUM</tt> will be produced. Then enter

<tt> trace = script_NUM(modelForThisTrace) </tt>

into the console, where modelForThisTrace is the model for which the trace should be executed.

Another option is to simply restore the Trace directly from the TraceConverter

<tt> trace = TraceConverter.restore(modelForThisTrace,"/pathToFile/fileName.xml")</tt>

== How to run a groovy script ==

You can use the build in <tt>run</tt> command to run a groovy script. Simply type

<tt> run pathToScript/script.groovy </tt>

into the console. Code completion is available for the run command.

== How to animate with only the StateSpace abstraction ==

It is also possible to carry out animations without using a trace object.

To get the root vertex from StateSpace space_0, type:

<tt> st = space_0.root </tt>

from there, you can execute a chain of events. For instance,

<tt> st = st.anyEvent("new").anyEvent().new("pp=PID1").new() </tt>

So you can execute anyEvent with the method anyEvent(filter), where filter can be a String name, or a List of names. You can also execute an event with name "name", with the method name(predicate), where predicate is the predicate string intended to filter the solutions for the event. If there are no parameters, the predicate "TRUE = TRUE" will automatically be added.

ProB Java API Tutorial

2014-11-05T14:56:37Z

Joy Clark: /* Event B */

[[Category:ProB Java API]]

ProB 2.0 is currently experimental. This means that the implementation may change during the course of development. However, we have reached the point in development where some of the features have reached a certain level of stability. Therefore, we are writing this tutorial to explain what those features are.

== How to get started developing with ProB 2.0 ==

The source code for ProB 2.0 is available via GitHub. Click [https://github.com/bendisposto/prob2 here] to view the prob2 repository. There is also a short guide available there which will help getting Eclipse set up so that you can get started with the development. Our bugtracker is available [http://jira.cobra.cs.uni-duesseldorf.de/browse/PROBCORE here]. There you can view the features that we are currently working on and can submit new feature requests.

== How to open the Groovy Shell ==

The ProB Groovy shell is available in the Eclipse application. To open it, select

<tt> Window > Show View > Other.. </tt>

Then select

<tt> ProB > Groovy Console </tt>

and hit <tt> ok</tt>.

== Open the ProB API from Source/JAR file ==

In order to access the console from source or from a JAR file, start the application with the parameters -s (short for --shell) and -local (which specifies that you are running the application from a local computer). This will start a web server at a given port (the default is 8080, but it increments the port number if a port is already active). The shell can then be accessed at the following address:

localhost:PORTNR/sessions/GroovyConsoleSession

== How to load a model ==

=== Classical B ===

You can load a Classical B model into the groovy console using the <tt> api </tt> variable that is available. There is a method <tt> b_load </tt> that is available to load Classical B models. For example:

<tt> m = api.b_load("/home/pathToFile/example.mch") </tt>

will load example.mch into the variable <tt>m</tt>.

=== Event B ===

To load an Event B model into ProB, right click on the model and select

<tt> Start Animation / Model Checking </tt>

from the context menu that drops down.

You can also load Event B models into the API via the eventb_load command in the Api object. The eventb_load command accepts .bcm and .bcc files.

== How to animate models ==

The Trace abstraction is available to carry out animations.

=== In The Console ===

There are several different ways that a new transition can be added to the current trace. The most important thing to remember is that each Trace object is completely immutable. This means that when you change a trace, you are actually getting a new Trace back. This means that when you carry out an animation step, you always have to make sure that you save the Trace object that is returned.

The simplest way to add a transition is to add it via operation id. For instance, if operation 0 is among the enabled operations for the current state, then

<tt> t = t.add(0) </tt>

will add operation 0 to the current trace, create a new trace, and return it.

You can also add operations via operation name and a list of the parameters. For instance

<tt> t = t.add("new",["PID3"]) </tt>

will add the transition new(PID3) to the trace.

It is also possible to execute any event by executing

<tt> t = t.anyEvent() </tt>

and it is also possible to execute any event with name "name". For instance,

<tt> t = t.anyEvent("name") </tt>

will execute any event with the name "name".

Lastly, it is also possible to execute an event by treating it as if it were a method in the Trace class. For instance,

<tt> t = t.new() </tt>

will execute the event new (by default, the first solution for "new" is chosen). It is also possible to add a predicate as a parameter to filter for a particular solution. For instance,

<tt> t = t.new("pp=PID1") </tt>

will execute new(PID1) as long as pp is the name of the parameter for new.

It also possible to move backwards and forwards within a trace.

Move backwards:

<tt> t = t.back() </tt>

Move forwards:

<tt> t = t.forward() </tt>

=== In The UI ===

In order to animate a loaded model in the UI, double-click on an enabled event in the <tt>Events</tt> view. Then, the resulting trace will automatically be loaded into the different views and it can be further animated. To move backwards and forwards in the trace, use the buttons in the upper right hand corner of the <tt>Events</tt> view.

== How to switch from UI to groovy console ==

There is an easy way to switch from the UI to the groovy console and back. It all happens using the "animations" global variable in the groovy console. What is important to remember, is that in this case, there is no distinction between an animation and a trace.

=== From UI to Console ===

In the UI, switch to the <tt>Current Animations</tt> view. Here you can view the different animations that are available. If the desired animation is not available, double click on it in this view and it will be set as the current animation. Now, to move this animation from the UI to the groovy console, simply type

<tt> x = animations.getCurrentTrace() </tt>

into the groovy console and the current animation will be loaded into the variable <tt>x</tt>.

=== From the Console to the UI ===

If you have a trace saved into variable <tt>trace_0</tt> in the groovy console, you can easily add it to the UI. Simply type

<tt> animations.addNewAnimation(trace_0) </tt>

into the groovy console and the trace will automatically be added to the list of current animations and all of the views will be updated.

== How to carry out evaluations ==

It is very simple to evaluate strings in the groovy console. There is a build in eval method in both the Trace and the StateSpace. In the trace, you just need to specify a string and the parser that is needed to parse the string. The two parsers currently available are <tt>ClassicalB</tt> and <tt>EventB</tt>.For instance,

<tt> t.eval("x:NAT" as EventB) </tt>

will parse "x:NAT" using the Event B parser and then will evaluate it at the current state. The following code

<tt> t.eval("x:NAT" as ClassicalB) </tt>

will parse "x:NAT" using the Classical B parser and then will evaluate it at the current state.

Classical B is actually the default parser, so it would also be sufficient to write

<tt> t.eval("x:NAT")</tt>.

It is also possible to evaluate formulas on the SpaceSpace level. For instance, if <tt>space_0</tt> is a StateSpace, you can evaluate a list of formulas by typing

<tt> space_0.eval(space_0[5],["x:NAT" as EventB,"y:NAT" as ClassicalB]) </tt>

into the console. This will parse "x:NAT" with the Event B parser and "y:NAT" with the Classical B parser and then will evaluate them at the state with id 5. The parser is not implicit in the StateSpace, so it is important to specify it here. In order to evaluate a formula, you need to specify the StateId object that is associated with the desired id. To extract a StateId from a StateSpace, you can use the notation <tt>space[ID]</tt> where ID is either a String or an integer representing the StateId that you want to view.

== How to convert between the main abstractions ==

There is a connection between all of the main abstractions. You can easily convert between them by using the <tt>as</tt> operator.

To convert between a Model and a StateSpace, use:

<tt> eventb = statespace_0 as EventBModel </tt> (if you are animating an Event B model)

or

<tt> classicalb = statespace_0 as ClassicalBModel </tt> (if you are animating ClassicalB).

The reverse translation is just as easy:

<tt> space = model as StateSpace </tt>

will return the StateSpace associated with model.

Conversion between a Trace and a StateSpace and between a Trace and Model are also simple. The following conversions are valid:

<tt> space = trace as StateSpace </tt>

<tt> trace = StateSpace as Trace </tt>

<tt> trace = model as Trace </tt>

<tt> model = trace as EventBModel </tt> or <tt> model = trace as ClassicalBModel </tt>

The only thing to mention is that every time you convert from a StateSpace or Model to a Trace, a new trace is created.

== How to save a trace ==

ProB currently supports a mechanism to save a trace in a script so that the same trace can be recreated. We are currently working on some improvements to this mechanism, so expect it to change over the next period of time. Currently, it is possible to save a Trace as an XML trace by typing

<tt>TraceConverter.save(trace_0,"/pathToFile/fileName.xml")</tt>

into the console. This will create the XML file <tt>fileName.xml</tt>.

If you want to load this trace back into the console, there are two options available. You can convert the XML file to a Groovy closure that will then take a Model object and return a Trace with all of the operations specified in the XML file. This can be triggered by calling the method

<tt>TraceConverter.xmlToGroovy("/pathToFile/fileName.xml","/pathToFile/groovyScript.groovy")</tt>

You can then run the produced Groovy script and execute the resulting closure to restore your Trace

<tt>run /pathToFile/groovyScript.groovy</tt>

A script <tt>script_NUM</tt> will be produced. Then enter

<tt> trace = script_NUM(modelForThisTrace) </tt>

into the console, where modelForThisTrace is the model for which the trace should be executed.

Another option is to simply restore the Trace directly from the TraceConverter

<tt> trace = TraceConverter.restore(modelForThisTrace,"/pathToFile/fileName.xml")</tt>

== How to run a groovy script ==

You can use the build in <tt>run</tt> command to run a groovy script. Simply type

<tt> run pathToScript/script.groovy </tt>

into the console. Code completion is available for the run command.

== How to animate with only the StateSpace abstraction ==

It is also possible to carry out animations without using a trace object.

To get the root vertex from StateSpace space_0, type:

<tt> st = space_0.root </tt>

from there, you can execute a chain of events. For instance,

<tt> st = st.anyEvent("new").anyEvent().new("pp=PID1").new() </tt>

So you can execute anyEvent with the method anyEvent(filter), where filter can be a String name, or a List of names. You can also execute an event with name "name", with the method name(predicate), where predicate is the predicate string intended to filter the solutions for the event. If there are no parameters, the predicate "TRUE = TRUE" will automatically be added.

ProB Java API Tutorial

2014-11-05T14:55:30Z

Joy Clark: /* Open the ProB API from Source/JAR file */

[[Category:ProB Java API]]

ProB 2.0 is currently experimental. This means that the implementation may change during the course of development. However, we have reached the point in development where some of the features have reached a certain level of stability. Therefore, we are writing this tutorial to explain what those features are.

== How to get started developing with ProB 2.0 ==

The source code for ProB 2.0 is available via GitHub. Click [https://github.com/bendisposto/prob2 here] to view the prob2 repository. There is also a short guide available there which will help getting Eclipse set up so that you can get started with the development. Our bugtracker is available [http://jira.cobra.cs.uni-duesseldorf.de/browse/PROBCORE here]. There you can view the features that we are currently working on and can submit new feature requests.

== How to open the Groovy Shell ==

The ProB Groovy shell is available in the Eclipse application. To open it, select

<tt> Window > Show View > Other.. </tt>

Then select

<tt> ProB > Groovy Console </tt>

and hit <tt> ok</tt>.

== Open the ProB API from Source/JAR file ==

In order to access the console from source or from a JAR file, start the application with the parameters -s (short for --shell) and -local (which specifies that you are running the application from a local computer). This will start a web server at a given port (the default is 8080, but it increments the port number if a port is already active). The shell can then be accessed at the following address:

localhost:PORTNR/sessions/GroovyConsoleSession

== How to load a model ==

=== Classical B ===

You can load a Classical B model into the groovy console using the <tt> api </tt> variable that is available. There is a method <tt> b_load </tt> that is available to load Classical B models. For example:

<tt> m = api.b_load("/home/pathToFile/example.mch") </tt>

will load example.mch into the variable <tt>m</tt>.

=== Event B ===

To load an Event B model into ProB, right click on the model and select

<tt> Start Animation / Model Checking </tt>

from the context menu that drops down.

== How to animate models ==

The Trace abstraction is available to carry out animations.

=== In The Console ===

There are several different ways that a new transition can be added to the current trace. The most important thing to remember is that each Trace object is completely immutable. This means that when you change a trace, you are actually getting a new Trace back. This means that when you carry out an animation step, you always have to make sure that you save the Trace object that is returned.

The simplest way to add a transition is to add it via operation id. For instance, if operation 0 is among the enabled operations for the current state, then

<tt> t = t.add(0) </tt>

will add operation 0 to the current trace, create a new trace, and return it.

You can also add operations via operation name and a list of the parameters. For instance

<tt> t = t.add("new",["PID3"]) </tt>

will add the transition new(PID3) to the trace.

It is also possible to execute any event by executing

<tt> t = t.anyEvent() </tt>

and it is also possible to execute any event with name "name". For instance,

<tt> t = t.anyEvent("name") </tt>

will execute any event with the name "name".

Lastly, it is also possible to execute an event by treating it as if it were a method in the Trace class. For instance,

<tt> t = t.new() </tt>

will execute the event new (by default, the first solution for "new" is chosen). It is also possible to add a predicate as a parameter to filter for a particular solution. For instance,

<tt> t = t.new("pp=PID1") </tt>

will execute new(PID1) as long as pp is the name of the parameter for new.

It also possible to move backwards and forwards within a trace.

Move backwards:

<tt> t = t.back() </tt>

Move forwards:

<tt> t = t.forward() </tt>

=== In The UI ===

In order to animate a loaded model in the UI, double-click on an enabled event in the <tt>Events</tt> view. Then, the resulting trace will automatically be loaded into the different views and it can be further animated. To move backwards and forwards in the trace, use the buttons in the upper right hand corner of the <tt>Events</tt> view.

== How to switch from UI to groovy console ==

There is an easy way to switch from the UI to the groovy console and back. It all happens using the "animations" global variable in the groovy console. What is important to remember, is that in this case, there is no distinction between an animation and a trace.

=== From UI to Console ===

In the UI, switch to the <tt>Current Animations</tt> view. Here you can view the different animations that are available. If the desired animation is not available, double click on it in this view and it will be set as the current animation. Now, to move this animation from the UI to the groovy console, simply type

<tt> x = animations.getCurrentTrace() </tt>

into the groovy console and the current animation will be loaded into the variable <tt>x</tt>.

=== From the Console to the UI ===

If you have a trace saved into variable <tt>trace_0</tt> in the groovy console, you can easily add it to the UI. Simply type

<tt> animations.addNewAnimation(trace_0) </tt>

into the groovy console and the trace will automatically be added to the list of current animations and all of the views will be updated.

== How to carry out evaluations ==

It is very simple to evaluate strings in the groovy console. There is a build in eval method in both the Trace and the StateSpace. In the trace, you just need to specify a string and the parser that is needed to parse the string. The two parsers currently available are <tt>ClassicalB</tt> and <tt>EventB</tt>.For instance,

<tt> t.eval("x:NAT" as EventB) </tt>

will parse "x:NAT" using the Event B parser and then will evaluate it at the current state. The following code

<tt> t.eval("x:NAT" as ClassicalB) </tt>

will parse "x:NAT" using the Classical B parser and then will evaluate it at the current state.

Classical B is actually the default parser, so it would also be sufficient to write

<tt> t.eval("x:NAT")</tt>.

It is also possible to evaluate formulas on the SpaceSpace level. For instance, if <tt>space_0</tt> is a StateSpace, you can evaluate a list of formulas by typing

<tt> space_0.eval(space_0[5],["x:NAT" as EventB,"y:NAT" as ClassicalB]) </tt>

into the console. This will parse "x:NAT" with the Event B parser and "y:NAT" with the Classical B parser and then will evaluate them at the state with id 5. The parser is not implicit in the StateSpace, so it is important to specify it here. In order to evaluate a formula, you need to specify the StateId object that is associated with the desired id. To extract a StateId from a StateSpace, you can use the notation <tt>space[ID]</tt> where ID is either a String or an integer representing the StateId that you want to view.

== How to convert between the main abstractions ==

There is a connection between all of the main abstractions. You can easily convert between them by using the <tt>as</tt> operator.

To convert between a Model and a StateSpace, use:

<tt> eventb = statespace_0 as EventBModel </tt> (if you are animating an Event B model)

or

<tt> classicalb = statespace_0 as ClassicalBModel </tt> (if you are animating ClassicalB).

The reverse translation is just as easy:

<tt> space = model as StateSpace </tt>

will return the StateSpace associated with model.

Conversion between a Trace and a StateSpace and between a Trace and Model are also simple. The following conversions are valid:

<tt> space = trace as StateSpace </tt>

<tt> trace = StateSpace as Trace </tt>

<tt> trace = model as Trace </tt>

<tt> model = trace as EventBModel </tt> or <tt> model = trace as ClassicalBModel </tt>

The only thing to mention is that every time you convert from a StateSpace or Model to a Trace, a new trace is created.

== How to save a trace ==

ProB currently supports a mechanism to save a trace in a script so that the same trace can be recreated. We are currently working on some improvements to this mechanism, so expect it to change over the next period of time. Currently, it is possible to save a Trace as an XML trace by typing

<tt>TraceConverter.save(trace_0,"/pathToFile/fileName.xml")</tt>

into the console. This will create the XML file <tt>fileName.xml</tt>.

If you want to load this trace back into the console, there are two options available. You can convert the XML file to a Groovy closure that will then take a Model object and return a Trace with all of the operations specified in the XML file. This can be triggered by calling the method

<tt>TraceConverter.xmlToGroovy("/pathToFile/fileName.xml","/pathToFile/groovyScript.groovy")</tt>

You can then run the produced Groovy script and execute the resulting closure to restore your Trace

<tt>run /pathToFile/groovyScript.groovy</tt>

A script <tt>script_NUM</tt> will be produced. Then enter

<tt> trace = script_NUM(modelForThisTrace) </tt>

into the console, where modelForThisTrace is the model for which the trace should be executed.

Another option is to simply restore the Trace directly from the TraceConverter

<tt> trace = TraceConverter.restore(modelForThisTrace,"/pathToFile/fileName.xml")</tt>

== How to run a groovy script ==

You can use the build in <tt>run</tt> command to run a groovy script. Simply type

<tt> run pathToScript/script.groovy </tt>

into the console. Code completion is available for the run command.

== How to animate with only the StateSpace abstraction ==

It is also possible to carry out animations without using a trace object.

To get the root vertex from StateSpace space_0, type:

<tt> st = space_0.root </tt>

from there, you can execute a chain of events. For instance,

<tt> st = st.anyEvent("new").anyEvent().new("pp=PID1").new() </tt>

So you can execute anyEvent with the method anyEvent(filter), where filter can be a String name, or a List of names. You can also execute an event with name "name", with the method name(predicate), where predicate is the predicate string intended to filter the solutions for the event. If there are no parameters, the predicate "TRUE = TRUE" will automatically be added.

ProB Java API Tutorial

2014-11-05T14:54:23Z

Joy Clark: /* How to open the Groovy Shell */

[[Category:ProB Java API]]

ProB 2.0 is currently experimental. This means that the implementation may change during the course of development. However, we have reached the point in development where some of the features have reached a certain level of stability. Therefore, we are writing this tutorial to explain what those features are.

== How to get started developing with ProB 2.0 ==

The source code for ProB 2.0 is available via GitHub. Click [https://github.com/bendisposto/prob2 here] to view the prob2 repository. There is also a short guide available there which will help getting Eclipse set up so that you can get started with the development. Our bugtracker is available [http://jira.cobra.cs.uni-duesseldorf.de/browse/PROBCORE here]. There you can view the features that we are currently working on and can submit new feature requests.

== How to open the Groovy Shell ==

The ProB Groovy shell is available in the Eclipse application. To open it, select

<tt> Window > Show View > Other.. </tt>

Then select

<tt> ProB > Groovy Console </tt>

and hit <tt> ok</tt>.

== Open the ProB API from Source/JAR file ==

In order to access the console from source or from a JAR file, start the application with the parameters -s (short for --shell) and -local (which specifies that you are running the application from a local computer). This will start a web server at a given port (the default is 8080, but it increments the port number if a port is already active). The shell can then be accessed at the following address:

http://localhost:8080/sessions/GroovyConsoleSession

== How to load a model ==

=== Classical B ===

You can load a Classical B model into the groovy console using the <tt> api </tt> variable that is available. There is a method <tt> b_load </tt> that is available to load Classical B models. For example:

<tt> m = api.b_load("/home/pathToFile/example.mch") </tt>

will load example.mch into the variable <tt>m</tt>.

=== Event B ===

To load an Event B model into ProB, right click on the model and select

<tt> Start Animation / Model Checking </tt>

from the context menu that drops down.

== How to animate models ==

The Trace abstraction is available to carry out animations.

=== In The Console ===

There are several different ways that a new transition can be added to the current trace. The most important thing to remember is that each Trace object is completely immutable. This means that when you change a trace, you are actually getting a new Trace back. This means that when you carry out an animation step, you always have to make sure that you save the Trace object that is returned.

The simplest way to add a transition is to add it via operation id. For instance, if operation 0 is among the enabled operations for the current state, then

<tt> t = t.add(0) </tt>

will add operation 0 to the current trace, create a new trace, and return it.

You can also add operations via operation name and a list of the parameters. For instance

<tt> t = t.add("new",["PID3"]) </tt>

will add the transition new(PID3) to the trace.

It is also possible to execute any event by executing

<tt> t = t.anyEvent() </tt>

and it is also possible to execute any event with name "name". For instance,

<tt> t = t.anyEvent("name") </tt>

will execute any event with the name "name".

Lastly, it is also possible to execute an event by treating it as if it were a method in the Trace class. For instance,

<tt> t = t.new() </tt>

will execute the event new (by default, the first solution for "new" is chosen). It is also possible to add a predicate as a parameter to filter for a particular solution. For instance,

<tt> t = t.new("pp=PID1") </tt>

will execute new(PID1) as long as pp is the name of the parameter for new.

It also possible to move backwards and forwards within a trace.

Move backwards:

<tt> t = t.back() </tt>

Move forwards:

<tt> t = t.forward() </tt>

=== In The UI ===

In order to animate a loaded model in the UI, double-click on an enabled event in the <tt>Events</tt> view. Then, the resulting trace will automatically be loaded into the different views and it can be further animated. To move backwards and forwards in the trace, use the buttons in the upper right hand corner of the <tt>Events</tt> view.

== How to switch from UI to groovy console ==

There is an easy way to switch from the UI to the groovy console and back. It all happens using the "animations" global variable in the groovy console. What is important to remember, is that in this case, there is no distinction between an animation and a trace.

=== From UI to Console ===

In the UI, switch to the <tt>Current Animations</tt> view. Here you can view the different animations that are available. If the desired animation is not available, double click on it in this view and it will be set as the current animation. Now, to move this animation from the UI to the groovy console, simply type

<tt> x = animations.getCurrentTrace() </tt>

into the groovy console and the current animation will be loaded into the variable <tt>x</tt>.

=== From the Console to the UI ===

If you have a trace saved into variable <tt>trace_0</tt> in the groovy console, you can easily add it to the UI. Simply type

<tt> animations.addNewAnimation(trace_0) </tt>

into the groovy console and the trace will automatically be added to the list of current animations and all of the views will be updated.

== How to carry out evaluations ==

It is very simple to evaluate strings in the groovy console. There is a build in eval method in both the Trace and the StateSpace. In the trace, you just need to specify a string and the parser that is needed to parse the string. The two parsers currently available are <tt>ClassicalB</tt> and <tt>EventB</tt>.For instance,

<tt> t.eval("x:NAT" as EventB) </tt>

will parse "x:NAT" using the Event B parser and then will evaluate it at the current state. The following code

<tt> t.eval("x:NAT" as ClassicalB) </tt>

will parse "x:NAT" using the Classical B parser and then will evaluate it at the current state.

Classical B is actually the default parser, so it would also be sufficient to write

<tt> t.eval("x:NAT")</tt>.

It is also possible to evaluate formulas on the SpaceSpace level. For instance, if <tt>space_0</tt> is a StateSpace, you can evaluate a list of formulas by typing

<tt> space_0.eval(space_0[5],["x:NAT" as EventB,"y:NAT" as ClassicalB]) </tt>

into the console. This will parse "x:NAT" with the Event B parser and "y:NAT" with the Classical B parser and then will evaluate them at the state with id 5. The parser is not implicit in the StateSpace, so it is important to specify it here. In order to evaluate a formula, you need to specify the StateId object that is associated with the desired id. To extract a StateId from a StateSpace, you can use the notation <tt>space[ID]</tt> where ID is either a String or an integer representing the StateId that you want to view.

== How to convert between the main abstractions ==

There is a connection between all of the main abstractions. You can easily convert between them by using the <tt>as</tt> operator.

To convert between a Model and a StateSpace, use:

<tt> eventb = statespace_0 as EventBModel </tt> (if you are animating an Event B model)

or

<tt> classicalb = statespace_0 as ClassicalBModel </tt> (if you are animating ClassicalB).

The reverse translation is just as easy:

<tt> space = model as StateSpace </tt>

will return the StateSpace associated with model.

Conversion between a Trace and a StateSpace and between a Trace and Model are also simple. The following conversions are valid:

<tt> space = trace as StateSpace </tt>

<tt> trace = StateSpace as Trace </tt>

<tt> trace = model as Trace </tt>

<tt> model = trace as EventBModel </tt> or <tt> model = trace as ClassicalBModel </tt>

The only thing to mention is that every time you convert from a StateSpace or Model to a Trace, a new trace is created.

== How to save a trace ==

ProB currently supports a mechanism to save a trace in a script so that the same trace can be recreated. We are currently working on some improvements to this mechanism, so expect it to change over the next period of time. Currently, it is possible to save a Trace as an XML trace by typing

<tt>TraceConverter.save(trace_0,"/pathToFile/fileName.xml")</tt>

into the console. This will create the XML file <tt>fileName.xml</tt>.

If you want to load this trace back into the console, there are two options available. You can convert the XML file to a Groovy closure that will then take a Model object and return a Trace with all of the operations specified in the XML file. This can be triggered by calling the method

<tt>TraceConverter.xmlToGroovy("/pathToFile/fileName.xml","/pathToFile/groovyScript.groovy")</tt>

You can then run the produced Groovy script and execute the resulting closure to restore your Trace

<tt>run /pathToFile/groovyScript.groovy</tt>

A script <tt>script_NUM</tt> will be produced. Then enter

<tt> trace = script_NUM(modelForThisTrace) </tt>

into the console, where modelForThisTrace is the model for which the trace should be executed.

Another option is to simply restore the Trace directly from the TraceConverter

<tt> trace = TraceConverter.restore(modelForThisTrace,"/pathToFile/fileName.xml")</tt>

== How to run a groovy script ==

You can use the build in <tt>run</tt> command to run a groovy script. Simply type

<tt> run pathToScript/script.groovy </tt>

into the console. Code completion is available for the run command.

== How to animate with only the StateSpace abstraction ==

It is also possible to carry out animations without using a trace object.

To get the root vertex from StateSpace space_0, type:

<tt> st = space_0.root </tt>

from there, you can execute a chain of events. For instance,

<tt> st = st.anyEvent("new").anyEvent().new("pp=PID1").new() </tt>

So you can execute anyEvent with the method anyEvent(filter), where filter can be a String name, or a List of names. You can also execute an event with name "name", with the method name(predicate), where predicate is the predicate string intended to filter the solutions for the event. If there are no parameters, the predicate "TRUE = TRUE" will automatically be added.

Programmatic Abstractions in the ProB 2.0 API

2014-11-05T14:47:58Z

Joy Clark: /* StateSpace */

[[Category:ProB Java API]]

== Overview ==

=== 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 ===
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.

== 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.

== 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.

== 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.

Programmatic Abstractions in the ProB 2.0 API

2014-11-05T14:40:15Z

Joy Clark: /* Model */

[[Category:ProB Java API]]

== Overview ==

=== 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 ===
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.

== 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.

== 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.
It is actually implemented as a graph (using the JGraphT library), so there are built in graph functions and support for graphical representations. In the graph, the vertices are states and the edges are events (including solutions and choices for local variables and non-deterministic assignments).

Conceptually, the state space is completely there and completely evaluated. When you access a state within the StateSpace that has not yet been explored, 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.

The StateSpace object is actually mutable, but it is always growing. No data ever gets replaced by any new data.

== 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.

Programmatic Abstractions in the ProB 2.0 API

2014-11-05T14:38:21Z

Joy Clark: /* Overview */

[[Category:ProB Java API]]

== Overview ==

=== 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 ===
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.

== 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.

== 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.
It is actually implemented as a graph (using the JGraphT library), so there are built in graph functions and support for graphical representations. In the graph, the vertices are states and the edges are events (including solutions and choices for local variables and non-deterministic assignments).

Conceptually, the state space is completely there and completely evaluated. When you access a state within the StateSpace that has not yet been explored, 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.

The StateSpace object is actually mutable, but it is always growing. No data ever gets replaced by any new data.

== 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.

Programmatic Abstractions in the ProB 2.0 API

2014-11-05T14:34:09Z

Joy Clark: /* Background */

[[Category:ProB Java API]]

== Overview ==

=== 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 ===
The developer is still able to use commands in order to get information from the prolog kernel. But 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.

== 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.

== 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.
It is actually implemented as a graph (using the JGraphT library), so there are built in graph functions and support for graphical representations. In the graph, the vertices are states and the edges are events (including solutions and choices for local variables and non-deterministic assignments).

Conceptually, the state space is completely there and completely evaluated. When you access a state within the StateSpace that has not yet been explored, 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.

The StateSpace object is actually mutable, but it is always growing. No data ever gets replaced by any new data.

== 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.

ProB 2.0 Development

2014-11-05T14:31:35Z

Joy Clark: /* Basic Design Principles */

[[Category:ProB Java API]]
[[Category:Developer Manual]]
__TOC__

== 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? ===

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 ==

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 ==

A tutorial for the current features of ProB 2.0 is available [[ProB 2.0 Tutorial|here]].

Rodin User and Developer Workshop 2013 - Tutorial

2013-06-26T20:55:33Z

Joy Clark: /* The model */ specify line as code

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 [[media:Scheduler_tutorial2013.zip|simple scheduler example]]. Maybe you have to clean the project after importing.

== 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 '''<code>upgrade latest</code>''' 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.

== Preparation ==

# Import the Scheduler project.
# Start an animation for Scheduler0
# Perform some random animation steps
# Type <code>s = space_0</code> into the Groovy console. space_0 has been created automatically when you loaded the scheduler. Subsequent loading wil result in space_1, space_2, etc.

== 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()

The stae space represents the whole currently known world for an animation. It is lazily explored, i.e., the knowledge always increases. The class is based on a Graph from the [http://jung.sourceforge.net/ JUNG] framework. However, we hide methods that can remove information from the graph. The StateSpace class also provides notification mechanism to inform clients about important changes, such as the exploration of new states.

'''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 <code>massakr</code> event. This event breaks the invariant of the system. Otherwise the next command will return an empty set.

'''Are there some states that violate the invariant?'''
s.getInvariantKo()

'''Are there some states where the invariant holds?'''
s.getInvariantOk()

'''What kind of object is the result? '''
s.getInvariantOk().getClass()

'''What kind of objects are contained in the set? '''
s.getInvariantOk().first().getClass()

'''Let's explore StateIds.'''
x = s.getInvariantOk().first()

'''Can we get the value of a variable in that state?'''
x.value("active")

'''Can we randomly "execute" events?'''
y = x.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?'''
s.getOutEdges(x)

'''What are the elements of the hashset?'''
s.getOutEdges(x).first().getClass()

'''Now let's get one of these OpInfo objects'''
o = (s.getOutEdges(x) as List)[1]

Groovy allows us to transform a Set into a list using the Groovy [http://silvanolte.com/blog/2011/03/11/the-groovy-as-keyword/ as] keyword.

'''What is the name of the operation?'''
n = o.getName()

'''What are the actual parameters?'''
n = o.getParams()

'''What is the formal parameter name?'''
e = mch.getEvent(o.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

'''x.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 space, and the detail information from the OpInfo 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,x,name,params) {
formal_params = mch.getEvent(name).getParameters()
pred = [formal_params,params].transpose()
.collect { a,b -> a.toString() + "=" + b.toString() }
x.perform(name,pred)
}

You can write your own set of convenience functions in a groovy file and run it at the beginning.
run ~/myAwesomeScript.groovy

'''How can we track a trace of events?'''
t = new Trace(s)

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.

'''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().getId())

'''How can we produce a random trace?'''
def randTrace(t,n) {
nt = t;
for(int i=0; i < n; i++) {
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.evaluateForEveryState([f1, "waiting" as EventB])

evaluateForEveryState takes a list of formulas and evaluates them for each state of the statespace. This method is not called eval to prevent accidental evaluation. To evaluate a list of formulas for a subset, there is another method evaluateForGivenStates.

'''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., <code>"1<4" & "x>y"</code> evaluates to <code>"(1<4) & (x>y)"</code>. 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. <code>"1<2".implies("3<4")</code> results in <code>"(1<2) => (3<4)"</code>. 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.getResult()

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.getResult()

'''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.getResult()
}

'''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, <code>animations</code> and <code>api</code>.

<code>animations</code> is an Instance of <code>AnimationSelector</code>, <code>api</code> is an instance of <code>Api</code>. 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)

==Additional Resources==

Further information can be found in the [[Developer_Manual|developer manual]].

{{Feedback}}

ProB Java API Tutorial

2013-06-26T20:51:57Z

Joy Clark: /* How to get started developing with ProB 2.0 */ fix broken links

ProB 2.0 is currently experimental. This means that the implementation may change during the course of development. However, we have reached the point in development where some of the features have reached a certain level of stability. Therefore, we are writing this tutorial to explain what those features are.

== How to get started developing with ProB 2.0 ==

The source code for ProB 2.0 is available via GitHub. Click [https://github.com/bendisposto/prob2 here] to view the prob2 repository. There is also a short guide available there which will help getting Eclipse set up so that you can get started with the development. Our bugtracker is available [http://jira.cobra.cs.uni-duesseldorf.de/browse/PROBCORE here]. There you can view the features that we are currently working on and can submit new feature requests.

== How to open the Groovy Shell ==

The ProB Groovy shell is available in the Eclipse application. To open it, select

<tt> Window > Show View > Other.. </tt>

Then select

<tt> ProB > Groovy Console </tt>

and hit <tt> ok</tt>.

== How to load a model ==

=== Classical B ===

You can load a Classical B model into the groovy console in two ways. There is a built in <tt>load</tt>. For example:

<tt> load /home/pathToFile/example.mch </tt>

would load example.mch into the console (it will automatically save it into a variable named <tt>model_NUM</tt>, where <tt>NUM</tt> is a unique identifier). The nice thing about the load command is that it allows code completion. Code completion works the same as in a normal console. Hit <tt> <TAB> </tt> to see the code completions that are available.

If you are writing a script that you want to run in the console, you will want to use the <tt> api </tt> variable that is available. There is a method <tt> b_load </tt> that is available to load Classical B models. For example:

<tt> m = api.b_load("/home/pathToFile/example.mch") </tt>

will load example.mch into the variable <tt>m</tt>.

=== Event B ===

To load an Event B model into ProB, right click on the model and select

<tt> Start Animation / Model Checking </tt>

from the context menu that drops down.

== How to animate models ==

The Trace abstraction is available to carry out animations.

=== In The Console ===

There are several different ways that a new transition can be added to the current trace. The most important thing to remember is that each Trace object is completely immutable. This means that when you change a trace, you are actually getting a new Trace back. This means that when you carry out an animation step, you always have to make sure that you save the Trace object that is returned.

The simplest way to add a transition is to add it via operation id. For instance, if operation 0 is among the enabled operations for the current state, then

<tt> t = t.add(0) </tt>

will add operation 0 to the current trace, create a new trace, and return it.

You can also add operations via operation name and a list of the parameters. For instance

<tt> t = t.add("new",["PID3"]) </tt>

will add the transition new(PID3) to the trace.

It is also possible to execute any event by executing

<tt> t = t.anyEvent() </tt>

and it is also possible to execute any event with name "name". For instance,

<tt> t = t.anyEvent("name") </tt>

will execute any event with the name "name".

Lastly, it is also possible to execute an event by treating it as if it were a method in the Trace class. For instance,

<tt> t = t.new() </tt>

will execute the event new (by default, the first solution for "new" is chosen). It is also possible to add a predicate as a parameter to filter for a particular solution. For instance,

<tt> t = t.new("pp=PID1") </tt>

will execute new(PID1) as long as pp is the name of the parameter for new.

It also possible to move backwards and forwards within a trace.

Move backwards:

<tt> t = t.back() </tt>

Move forwards:

<tt> t = t.forward() </tt>

=== In The UI ===

In order to animate a loaded model in the UI, double-click on an enabled event in the <tt>Events</tt> view. Then, the resulting trace will automatically be loaded into the different views and it can be further animated. To move backwards and forwards in the trace, use the buttons in the upper right hand corner of the <tt>Events</tt> view.

== How to switch from UI to groovy console ==

There is an easy way to switch from the UI to the groovy console and back. It all happens using the "animations" global variable in the groovy console. What is important to remember, is that in this case, there is no distinction between an animation and a trace.

=== From UI to Console ===

In the UI, switch to the <tt>Current Animations</tt> view. Here you can view the different animations that are available. If the desired animation is not available, double click on it in this view and it will be set as the current animation. Now, to move this animation from the UI to the groovy console, simply type

<tt> x = animations.getCurrentTrace() </tt>

into the groovy console and the current animation will be loaded into the variable <tt>x</tt>.

=== From the Console to the UI ===

If you have a trace saved into variable <tt>trace_0</tt> in the groovy console, you can easily add it to the UI. Simply type

<tt> animations.addNewAnimation(trace_0) </tt>

into the groovy console and the trace will automatically be added to the list of current animations and all of the views will be updated.

== How to carry out evaluations ==

It is very simple to evaluate strings in the groovy console. There is a build in eval method in both the Trace and the StateSpace. In the trace, you just need to specify a string and the parser that is needed to parse the string. The two parsers currently available are <tt>ClassicalB</tt> and <tt>EventB</tt>.For instance,

<tt> t.eval("x:NAT" as EventB) </tt>

will parse "x:NAT" using the Event B parser and then will evaluate it at the current state. The following code

<tt> t.eval("x:NAT" as ClassicalB) </tt>

will parse "x:NAT" using the Classical B parser and then will evaluate it at the current state.

Classical B is actually the default parser, so it would also be sufficient to write

<tt> t.eval("x:NAT")</tt>.

It is also possible to evaluate formulas on the SpaceSpace level. For instance, if <tt>space_0</tt> is a StateSpace, you can evaluate a list of formulas by typing

<tt> space_0.eval(space_0[5],["x:NAT" as EventB,"y:NAT" as ClassicalB]) </tt>

into the console. This will parse "x:NAT" with the Event B parser and "y:NAT" with the Classical B parser and then will evaluate them at the state with id 5. The parser is not implicit in the StateSpace, so it is important to specify it here. In order to evaluate a formula, you need to specify the StateId object that is associated with the desired id. To extract a StateId from a StateSpace, you can use the notation <tt>space[ID]</tt> where ID is either a String or an integer representing the StateId that you want to view.

== How to convert between the main abstractions ==

There is a connection between all of the main abstractions. You can easily convert between them by using the <tt>as</tt> operator.

To convert between a Model and a StateSpace, use:

<tt> eventb = statespace_0 as EventBModel </tt> (if you are animating an Event B model)

or

<tt> classicalb = statespace_0 as ClassicalBModel </tt> (if you are animating ClassicalB).

The reverse translation is just as easy:

<tt> space = model as StateSpace </tt>

will return the StateSpace associated with model.

Conversion between a Trace and a StateSpace and between a Trace and Model are also simple. The following conversions are valid:

<tt> space = trace as StateSpace </tt>

<tt> trace = StateSpace as Trace </tt>

<tt> trace = model as Trace </tt>

<tt> model = trace as EventBModel </tt> or <tt> model = trace as ClassicalBModel </tt>

The only thing to mention is that every time you convert from a StateSpace or Model to a Trace, a new trace is created.

== How to save a trace ==

ProB currently supports a mechanism to save a trace in a script so that the same trace can be recreated. We are currently working on some improvements to this mechanism, so expect it to change over the next period of time. Currently, it is possible to save a Trace as an XML trace by typing

<tt>TraceConverter.save(trace_0,"/pathToFile/fileName.xml")</tt>

into the console. This will create the XML file <tt>fileName.xml</tt>.

If you want to load this trace back into the console, there are two options available. You can convert the XML file to a Groovy closure that will then take a Model object and return a Trace with all of the operations specified in the XML file. This can be triggered by calling the method

<tt>TraceConverter.xmlToGroovy("/pathToFile/fileName.xml","/pathToFile/groovyScript.groovy")</tt>

You can then run the produced Groovy script and execute the resulting closure to restore your Trace

<tt>run /pathToFile/groovyScript.groovy</tt>

A script <tt>script_NUM</tt> will be produced. Then enter

<tt> trace = script_NUM(modelForThisTrace) </tt>

into the console, where modelForThisTrace is the model for which the trace should be executed.

Another option is to simply restore the Trace directly from the TraceConverter

<tt> trace = TraceConverter.restore(modelForThisTrace,"/pathToFile/fileName.xml")</tt>

== How to run a groovy script ==

You can use the build in <tt>run</tt> command to run a groovy script. Simply type

<tt> run pathToScript/script.groovy </tt>

into the console. Code completion is available for the run command.

== How to animate with only the StateSpace abstraction ==

It is also possible to carry out animations without using a trace object.

To get the root vertex from StateSpace space_0, type:

<tt> st = space_0.root </tt>

from there, you can execute a chain of events. For instance,

<tt> st = st.anyEvent("new").anyEvent().new("pp=PID1").new() </tt>

So you can execute anyEvent with the method anyEvent(filter), where filter can be a String name, or a List of names. You can also execute an event with name "name", with the method name(predicate), where predicate is the predicate string intended to filter the solutions for the event. If there are no parameters, the predicate "TRUE = TRUE" will automatically be added.

ProB Java API Tutorial

2013-06-04T12:14:55Z

Joy Clark: /* How to carry out evaluations */

ProB 2.0 is currently experimental. This means that the implementation may change during the course of development. However, we have reached the point in development where some of the features have reached a certain level of stability. Therefore, we are writing this tutorial to explain what those features are.

== How to get started developing with ProB 2.0 ==

The source code for ProB 2.0 is available via GitHub. Click [[https://github.com/bendisposto/prob2|here]] to view the prob2 repository. There is also a short guide available there which will help getting Eclipse set up so that you can get started with the development. Our bugtracker is available [[http://jira.cobra.cs.uni-duesseldorf.de/browse/PROBCORE|here]]. There you can view the features that we are currently working on and can submit new feature requests.

== How to open the Groovy Shell ==

The ProB Groovy shell is available in the Eclipse application. To open it, select

<tt> Window > Show View > Other.. </tt>

Then select

<tt> ProB > Groovy Console </tt>

and hit <tt> ok</tt>.

== How to load a model ==

=== Classical B ===

You can load a Classical B model into the groovy console in two ways. There is a built in <tt>load</tt>. For example:

<tt> load /home/pathToFile/example.mch </tt>

would load example.mch into the console (it will automatically save it into a variable named <tt>model_NUM</tt>, where <tt>NUM</tt> is a unique identifier). The nice thing about the load command is that it allows code completion. Code completion works the same as in a normal console. Hit <tt> <TAB> </tt> to see the code completions that are available.

If you are writing a script that you want to run in the console, you will want to use the <tt> api </tt> variable that is available. There is a method <tt> b_load </tt> that is available to load Classical B models. For example:

<tt> m = api.b_load("/home/pathToFile/example.mch") </tt>

will load example.mch into the variable <tt>m</tt>.

=== Event B ===

To load an Event B model into ProB, right click on the model and select

<tt> Start Animation / Model Checking </tt>

from the context menu that drops down.

== How to animate models ==

The Trace abstraction is available to carry out animations.

=== In The Console ===

There are several different ways that a new transition can be added to the current trace. The most important thing to remember is that each Trace object is completely immutable. This means that when you change a trace, you are actually getting a new Trace back. This means that when you carry out an animation step, you always have to make sure that you save the Trace object that is returned.

The simplest way to add a transition is to add it via operation id. For instance, if operation 0 is among the enabled operations for the current state, then

<tt> t = t.add(0) </tt>

will add operation 0 to the current trace, create a new trace, and return it.

You can also add operations via operation name and a list of the parameters. For instance

<tt> t = t.add("new",["PID3"]) </tt>

will add the transition new(PID3) to the trace.

It is also possible to execute any event by executing

<tt> t = t.anyEvent() </tt>

and it is also possible to execute any event with name "name". For instance,

<tt> t = t.anyEvent("name") </tt>

will execute any event with the name "name".

Lastly, it is also possible to execute an event by treating it as if it were a method in the Trace class. For instance,

<tt> t = t.new() </tt>

will execute the event new (by default, the first solution for "new" is chosen). It is also possible to add a predicate as a parameter to filter for a particular solution. For instance,

<tt> t = t.new("pp=PID1") </tt>

will execute new(PID1) as long as pp is the name of the parameter for new.

It also possible to move backwards and forwards within a trace.

Move backwards:

<tt> t = t.back() </tt>

Move forwards:

<tt> t = t.forward() </tt>

=== In The UI ===

In order to animate a loaded model in the UI, double-click on an enabled event in the <tt>Events</tt> view. Then, the resulting trace will automatically be loaded into the different views and it can be further animated. To move backwards and forwards in the trace, use the buttons in the upper right hand corner of the <tt>Events</tt> view.

== How to switch from UI to groovy console ==

There is an easy way to switch from the UI to the groovy console and back. It all happens using the "animations" global variable in the groovy console. What is important to remember, is that in this case, there is no distinction between an animation and a trace.

=== From UI to Console ===

In the UI, switch to the <tt>Current Animations</tt> view. Here you can view the different animations that are available. If the desired animation is not available, double click on it in this view and it will be set as the current animation. Now, to move this animation from the UI to the groovy console, simply type

<tt> x = animations.getCurrentTrace() </tt>

into the groovy console and the current animation will be loaded into the variable <tt>x</tt>.

=== From the Console to the UI ===

If you have a trace saved into variable <tt>trace_0</tt> in the groovy console, you can easily add it to the UI. Simply type

<tt> animations.addNewAnimation(trace_0) </tt>

into the groovy console and the trace will automatically be added to the list of current animations and all of the views will be updated.

== How to carry out evaluations ==

It is very simple to evaluate strings in the groovy console. There is a build in eval method in both the Trace and the StateSpace. In the trace, you just need to specify a string and the parser that is needed to parse the string. The two parsers currently available are <tt>ClassicalB</tt> and <tt>EventB</tt>.For instance,

<tt> t.eval("x:NAT" as EventB) </tt>

will parse "x:NAT" using the Event B parser and then will evaluate it at the current state. The following code

<tt> t.eval("x:NAT" as ClassicalB) </tt>

will parse "x:NAT" using the Classical B parser and then will evaluate it at the current state.

Classical B is actually the default parser, so it would also be sufficient to write

<tt> t.eval("x:NAT")</tt>.

It is also possible to evaluate formulas on the SpaceSpace level. For instance, if <tt>space_0</tt> is a StateSpace, you can evaluate a list of formulas by typing

<tt> space_0.eval(space_0[5],["x:NAT" as EventB,"y:NAT" as ClassicalB]) </tt>

into the console. This will parse "x:NAT" with the Event B parser and "y:NAT" with the Classical B parser and then will evaluate them at the state with id 5. The parser is not implicit in the StateSpace, so it is important to specify it here. In order to evaluate a formula, you need to specify the StateId object that is associated with the desired id. To extract a StateId from a StateSpace, you can use the notation <tt>space[ID]</tt> where ID is either a String or an integer representing the StateId that you want to view.

== How to convert between the main abstractions ==

There is a connection between all of the main abstractions. You can easily convert between them by using the <tt>as</tt> operator.

To convert between a Model and a StateSpace, use:

<tt> eventb = statespace_0 as EventBModel </tt> (if you are animating an Event B model)

or

<tt> classicalb = statespace_0 as ClassicalBModel </tt> (if you are animating ClassicalB).

The reverse translation is just as easy:

<tt> space = model as StateSpace </tt>

will return the StateSpace associated with model.

Conversion between a Trace and a StateSpace and between a Trace and Model are also simple. The following conversions are valid:

<tt> space = trace as StateSpace </tt>

<tt> trace = StateSpace as Trace </tt>

<tt> trace = model as Trace </tt>

<tt> model = trace as EventBModel </tt> or <tt> model = trace as ClassicalBModel </tt>

The only thing to mention is that every time you convert from a StateSpace or Model to a Trace, a new trace is created.

== How to save a trace ==

ProB currently supports a mechanism to save a trace in a script so that the same trace can be recreated. We are currently working on some improvements to this mechanism, so expect it to change over the next period of time. Currently, it is possible to save a Trace as an XML trace by typing

<tt>TraceConverter.save(trace_0,"/pathToFile/fileName.xml")</tt>

into the console. This will create the XML file <tt>fileName.xml</tt>.

If you want to load this trace back into the console, there are two options available. You can convert the XML file to a Groovy closure that will then take a Model object and return a Trace with all of the operations specified in the XML file. This can be triggered by calling the method

<tt>TraceConverter.xmlToGroovy("/pathToFile/fileName.xml","/pathToFile/groovyScript.groovy")</tt>

You can then run the produced Groovy script and execute the resulting closure to restore your Trace

<tt>run /pathToFile/groovyScript.groovy</tt>

A script <tt>script_NUM</tt> will be produced. Then enter

<tt> trace = script_NUM(modelForThisTrace) </tt>

into the console, where modelForThisTrace is the model for which the trace should be executed.

Another option is to simply restore the Trace directly from the TraceConverter

<tt> trace = TraceConverter.restore(modelForThisTrace,"/pathToFile/fileName.xml")</tt>

== How to run a groovy script ==

You can use the build in <tt>run</tt> command to run a groovy script. Simply type

<tt> run pathToScript/script.groovy </tt>

into the console. Code completion is available for the run command.

== How to animate with only the StateSpace abstraction ==

It is also possible to carry out animations without using a trace object.

To get the root vertex from StateSpace space_0, type:

<tt> st = space_0.root </tt>

from there, you can execute a chain of events. For instance,

<tt> st = st.anyEvent("new").anyEvent().new("pp=PID1").new() </tt>

So you can execute anyEvent with the method anyEvent(filter), where filter can be a String name, or a List of names. You can also execute an event with name "name", with the method name(predicate), where predicate is the predicate string intended to filter the solutions for the event. If there are no parameters, the predicate "TRUE = TRUE" will automatically be added.

ProB Java API Tutorial

2013-06-04T12:14:40Z

Joy Clark: /* In The Console */

ProB 2.0 is currently experimental. This means that the implementation may change during the course of development. However, we have reached the point in development where some of the features have reached a certain level of stability. Therefore, we are writing this tutorial to explain what those features are.

== How to get started developing with ProB 2.0 ==

The source code for ProB 2.0 is available via GitHub. Click [[https://github.com/bendisposto/prob2|here]] to view the prob2 repository. There is also a short guide available there which will help getting Eclipse set up so that you can get started with the development. Our bugtracker is available [[http://jira.cobra.cs.uni-duesseldorf.de/browse/PROBCORE|here]]. There you can view the features that we are currently working on and can submit new feature requests.

== How to open the Groovy Shell ==

The ProB Groovy shell is available in the Eclipse application. To open it, select

<tt> Window > Show View > Other.. </tt>

Then select

<tt> ProB > Groovy Console </tt>

and hit <tt> ok</tt>.

== How to load a model ==

=== Classical B ===

You can load a Classical B model into the groovy console in two ways. There is a built in <tt>load</tt>. For example:

<tt> load /home/pathToFile/example.mch </tt>

would load example.mch into the console (it will automatically save it into a variable named <tt>model_NUM</tt>, where <tt>NUM</tt> is a unique identifier). The nice thing about the load command is that it allows code completion. Code completion works the same as in a normal console. Hit <tt> <TAB> </tt> to see the code completions that are available.

If you are writing a script that you want to run in the console, you will want to use the <tt> api </tt> variable that is available. There is a method <tt> b_load </tt> that is available to load Classical B models. For example:

<tt> m = api.b_load("/home/pathToFile/example.mch") </tt>

will load example.mch into the variable <tt>m</tt>.

=== Event B ===

To load an Event B model into ProB, right click on the model and select

<tt> Start Animation / Model Checking </tt>

from the context menu that drops down.

== How to animate models ==

The Trace abstraction is available to carry out animations.

=== In The Console ===

There are several different ways that a new transition can be added to the current trace. The most important thing to remember is that each Trace object is completely immutable. This means that when you change a trace, you are actually getting a new Trace back. This means that when you carry out an animation step, you always have to make sure that you save the Trace object that is returned.

The simplest way to add a transition is to add it via operation id. For instance, if operation 0 is among the enabled operations for the current state, then

<tt> t = t.add(0) </tt>

will add operation 0 to the current trace, create a new trace, and return it.

You can also add operations via operation name and a list of the parameters. For instance

<tt> t = t.add("new",["PID3"]) </tt>

will add the transition new(PID3) to the trace.

It is also possible to execute any event by executing

<tt> t = t.anyEvent() </tt>

and it is also possible to execute any event with name "name". For instance,

<tt> t = t.anyEvent("name") </tt>

will execute any event with the name "name".

Lastly, it is also possible to execute an event by treating it as if it were a method in the Trace class. For instance,

<tt> t = t.new() </tt>

will execute the event new (by default, the first solution for "new" is chosen). It is also possible to add a predicate as a parameter to filter for a particular solution. For instance,

<tt> t = t.new("pp=PID1") </tt>

will execute new(PID1) as long as pp is the name of the parameter for new.

It also possible to move backwards and forwards within a trace.

Move backwards:

<tt> t = t.back() </tt>

Move forwards:

<tt> t = t.forward() </tt>

=== In The UI ===

In order to animate a loaded model in the UI, double-click on an enabled event in the <tt>Events</tt> view. Then, the resulting trace will automatically be loaded into the different views and it can be further animated. To move backwards and forwards in the trace, use the buttons in the upper right hand corner of the <tt>Events</tt> view.

== How to switch from UI to groovy console ==

There is an easy way to switch from the UI to the groovy console and back. It all happens using the "animations" global variable in the groovy console. What is important to remember, is that in this case, there is no distinction between an animation and a trace.

=== From UI to Console ===

In the UI, switch to the <tt>Current Animations</tt> view. Here you can view the different animations that are available. If the desired animation is not available, double click on it in this view and it will be set as the current animation. Now, to move this animation from the UI to the groovy console, simply type

<tt> x = animations.getCurrentTrace() </tt>

into the groovy console and the current animation will be loaded into the variable <tt>x</tt>.

=== From the Console to the UI ===

If you have a trace saved into variable <tt>trace_0</tt> in the groovy console, you can easily add it to the UI. Simply type

<tt> animations.addNewAnimation(trace_0) </tt>

into the groovy console and the trace will automatically be added to the list of current animations and all of the views will be updated.

== How to carry out evaluations ==

It is very simple to evaluate strings in the groovy console. There is a build in eval method in both the Trace and the StateSpace. In the history, you just need to specify a string and the parser that is needed to parse the string. The two parsers currently available are <tt>ClassicalB</tt> and <tt>EventB</tt>.For instance,

<tt> t.eval("x:NAT" as EventB) </tt>

will parse "x:NAT" using the Event B parser and then will evaluate it at the current state. The following code

<tt> t.eval("x:NAT" as ClassicalB) </tt>

will parse "x:NAT" using the Classical B parser and then will evaluate it at the current state.

Classical B is actually the default parser, so it would also be sufficient to write

<tt> t.eval("x:NAT")</tt>.

It is also possible to evaluate formulas on the SpaceSpace level. For instance, if <tt>space_0</tt> is a StateSpace, you can evaluate a list of formulas by typing

<tt> space_0.eval(space_0[5],["x:NAT" as EventB,"y:NAT" as ClassicalB]) </tt>

into the console. This will parse "x:NAT" with the Event B parser and "y:NAT" with the Classical B parser and then will evaluate them at the state with id 5. The parser is not implicit in the StateSpace, so it is important to specify it here. In order to evaluate a formula, you need to specify the StateId object that is associated with the desired id. To extract a StateId from a StateSpace, you can use the notation <tt>space[ID]</tt> where ID is either a String or an integer representing the StateId that you want to view.

== How to convert between the main abstractions ==

There is a connection between all of the main abstractions. You can easily convert between them by using the <tt>as</tt> operator.

To convert between a Model and a StateSpace, use:

<tt> eventb = statespace_0 as EventBModel </tt> (if you are animating an Event B model)

or

<tt> classicalb = statespace_0 as ClassicalBModel </tt> (if you are animating ClassicalB).

The reverse translation is just as easy:

<tt> space = model as StateSpace </tt>

will return the StateSpace associated with model.

Conversion between a Trace and a StateSpace and between a Trace and Model are also simple. The following conversions are valid:

<tt> space = trace as StateSpace </tt>

<tt> trace = StateSpace as Trace </tt>

<tt> trace = model as Trace </tt>

<tt> model = trace as EventBModel </tt> or <tt> model = trace as ClassicalBModel </tt>

The only thing to mention is that every time you convert from a StateSpace or Model to a Trace, a new trace is created.

== How to save a trace ==

ProB currently supports a mechanism to save a trace in a script so that the same trace can be recreated. We are currently working on some improvements to this mechanism, so expect it to change over the next period of time. Currently, it is possible to save a Trace as an XML trace by typing

<tt>TraceConverter.save(trace_0,"/pathToFile/fileName.xml")</tt>

into the console. This will create the XML file <tt>fileName.xml</tt>.

If you want to load this trace back into the console, there are two options available. You can convert the XML file to a Groovy closure that will then take a Model object and return a Trace with all of the operations specified in the XML file. This can be triggered by calling the method

<tt>TraceConverter.xmlToGroovy("/pathToFile/fileName.xml","/pathToFile/groovyScript.groovy")</tt>

You can then run the produced Groovy script and execute the resulting closure to restore your Trace

<tt>run /pathToFile/groovyScript.groovy</tt>

A script <tt>script_NUM</tt> will be produced. Then enter

<tt> trace = script_NUM(modelForThisTrace) </tt>

into the console, where modelForThisTrace is the model for which the trace should be executed.

Another option is to simply restore the Trace directly from the TraceConverter

<tt> trace = TraceConverter.restore(modelForThisTrace,"/pathToFile/fileName.xml")</tt>

== How to run a groovy script ==

You can use the build in <tt>run</tt> command to run a groovy script. Simply type

<tt> run pathToScript/script.groovy </tt>

into the console. Code completion is available for the run command.

== How to animate with only the StateSpace abstraction ==

It is also possible to carry out animations without using a trace object.

To get the root vertex from StateSpace space_0, type:

<tt> st = space_0.root </tt>

from there, you can execute a chain of events. For instance,

<tt> st = st.anyEvent("new").anyEvent().new("pp=PID1").new() </tt>

So you can execute anyEvent with the method anyEvent(filter), where filter can be a String name, or a List of names. You can also execute an event with name "name", with the method name(predicate), where predicate is the predicate string intended to filter the solutions for the event. If there are no parameters, the predicate "TRUE = TRUE" will automatically be added.

ProB Java API Tutorial

2013-06-04T12:14:27Z

Joy Clark:

ProB 2.0 is currently experimental. This means that the implementation may change during the course of development. However, we have reached the point in development where some of the features have reached a certain level of stability. Therefore, we are writing this tutorial to explain what those features are.

== How to get started developing with ProB 2.0 ==

The source code for ProB 2.0 is available via GitHub. Click [[https://github.com/bendisposto/prob2|here]] to view the prob2 repository. There is also a short guide available there which will help getting Eclipse set up so that you can get started with the development. Our bugtracker is available [[http://jira.cobra.cs.uni-duesseldorf.de/browse/PROBCORE|here]]. There you can view the features that we are currently working on and can submit new feature requests.

== How to open the Groovy Shell ==

The ProB Groovy shell is available in the Eclipse application. To open it, select

<tt> Window > Show View > Other.. </tt>

Then select

<tt> ProB > Groovy Console </tt>

and hit <tt> ok</tt>.

== How to load a model ==

=== Classical B ===

You can load a Classical B model into the groovy console in two ways. There is a built in <tt>load</tt>. For example:

<tt> load /home/pathToFile/example.mch </tt>

would load example.mch into the console (it will automatically save it into a variable named <tt>model_NUM</tt>, where <tt>NUM</tt> is a unique identifier). The nice thing about the load command is that it allows code completion. Code completion works the same as in a normal console. Hit <tt> <TAB> </tt> to see the code completions that are available.

If you are writing a script that you want to run in the console, you will want to use the <tt> api </tt> variable that is available. There is a method <tt> b_load </tt> that is available to load Classical B models. For example:

<tt> m = api.b_load("/home/pathToFile/example.mch") </tt>

will load example.mch into the variable <tt>m</tt>.

=== Event B ===

To load an Event B model into ProB, right click on the model and select

<tt> Start Animation / Model Checking </tt>

from the context menu that drops down.

== How to animate models ==

The Trace abstraction is available to carry out animations.

=== In The Console ===

There are several different ways that a new transition can be added to the current history. The most important thing to remember is that each Trace object is completely immutable. This means that when you change a trace, you are actually getting a new Trace back. This means that when you carry out an animation step, you always have to make sure that you save the Trace object that is returned.

The simplest way to add a transition is to add it via operation id. For instance, if operation 0 is among the enabled operations for the current state, then

<tt> t = t.add(0) </tt>

will add operation 0 to the current trace, create a new trace, and return it.

You can also add operations via operation name and a list of the parameters. For instance

<tt> t = t.add("new",["PID3"]) </tt>

will add the transition new(PID3) to the trace.

It is also possible to execute any event by executing

<tt> t = t.anyEvent() </tt>

and it is also possible to execute any event with name "name". For instance,

<tt> t = t.anyEvent("name") </tt>

will execute any event with the name "name".

Lastly, it is also possible to execute an event by treating it as if it were a method in the Trace class. For instance,

<tt> t = t.new() </tt>

will execute the event new (by default, the first solution for "new" is chosen). It is also possible to add a predicate as a parameter to filter for a particular solution. For instance,

<tt> t = t.new("pp=PID1") </tt>

will execute new(PID1) as long as pp is the name of the parameter for new.

It also possible to move backwards and forwards within a trace.

Move backwards:

<tt> t = t.back() </tt>

Move forwards:

<tt> t = t.forward() </tt>

=== In The UI ===

In order to animate a loaded model in the UI, double-click on an enabled event in the <tt>Events</tt> view. Then, the resulting trace will automatically be loaded into the different views and it can be further animated. To move backwards and forwards in the trace, use the buttons in the upper right hand corner of the <tt>Events</tt> view.

== How to switch from UI to groovy console ==

There is an easy way to switch from the UI to the groovy console and back. It all happens using the "animations" global variable in the groovy console. What is important to remember, is that in this case, there is no distinction between an animation and a trace.

=== From UI to Console ===

In the UI, switch to the <tt>Current Animations</tt> view. Here you can view the different animations that are available. If the desired animation is not available, double click on it in this view and it will be set as the current animation. Now, to move this animation from the UI to the groovy console, simply type

<tt> x = animations.getCurrentTrace() </tt>

into the groovy console and the current animation will be loaded into the variable <tt>x</tt>.

=== From the Console to the UI ===

If you have a trace saved into variable <tt>trace_0</tt> in the groovy console, you can easily add it to the UI. Simply type

<tt> animations.addNewAnimation(trace_0) </tt>

into the groovy console and the trace will automatically be added to the list of current animations and all of the views will be updated.

== How to carry out evaluations ==

It is very simple to evaluate strings in the groovy console. There is a build in eval method in both the Trace and the StateSpace. In the history, you just need to specify a string and the parser that is needed to parse the string. The two parsers currently available are <tt>ClassicalB</tt> and <tt>EventB</tt>.For instance,

<tt> t.eval("x:NAT" as EventB) </tt>

will parse "x:NAT" using the Event B parser and then will evaluate it at the current state. The following code

<tt> t.eval("x:NAT" as ClassicalB) </tt>

will parse "x:NAT" using the Classical B parser and then will evaluate it at the current state.

Classical B is actually the default parser, so it would also be sufficient to write

<tt> t.eval("x:NAT")</tt>.

It is also possible to evaluate formulas on the SpaceSpace level. For instance, if <tt>space_0</tt> is a StateSpace, you can evaluate a list of formulas by typing

<tt> space_0.eval(space_0[5],["x:NAT" as EventB,"y:NAT" as ClassicalB]) </tt>

into the console. This will parse "x:NAT" with the Event B parser and "y:NAT" with the Classical B parser and then will evaluate them at the state with id 5. The parser is not implicit in the StateSpace, so it is important to specify it here. In order to evaluate a formula, you need to specify the StateId object that is associated with the desired id. To extract a StateId from a StateSpace, you can use the notation <tt>space[ID]</tt> where ID is either a String or an integer representing the StateId that you want to view.

== How to convert between the main abstractions ==

There is a connection between all of the main abstractions. You can easily convert between them by using the <tt>as</tt> operator.

To convert between a Model and a StateSpace, use:

<tt> eventb = statespace_0 as EventBModel </tt> (if you are animating an Event B model)

or

<tt> classicalb = statespace_0 as ClassicalBModel </tt> (if you are animating ClassicalB).

The reverse translation is just as easy:

<tt> space = model as StateSpace </tt>

will return the StateSpace associated with model.

Conversion between a Trace and a StateSpace and between a Trace and Model are also simple. The following conversions are valid:

<tt> space = trace as StateSpace </tt>

<tt> trace = StateSpace as Trace </tt>

<tt> trace = model as Trace </tt>

<tt> model = trace as EventBModel </tt> or <tt> model = trace as ClassicalBModel </tt>

The only thing to mention is that every time you convert from a StateSpace or Model to a Trace, a new trace is created.

== How to save a trace ==

ProB currently supports a mechanism to save a trace in a script so that the same trace can be recreated. We are currently working on some improvements to this mechanism, so expect it to change over the next period of time. Currently, it is possible to save a Trace as an XML trace by typing

<tt>TraceConverter.save(trace_0,"/pathToFile/fileName.xml")</tt>

into the console. This will create the XML file <tt>fileName.xml</tt>.

If you want to load this trace back into the console, there are two options available. You can convert the XML file to a Groovy closure that will then take a Model object and return a Trace with all of the operations specified in the XML file. This can be triggered by calling the method

<tt>TraceConverter.xmlToGroovy("/pathToFile/fileName.xml","/pathToFile/groovyScript.groovy")</tt>

You can then run the produced Groovy script and execute the resulting closure to restore your Trace

<tt>run /pathToFile/groovyScript.groovy</tt>

A script <tt>script_NUM</tt> will be produced. Then enter

<tt> trace = script_NUM(modelForThisTrace) </tt>

into the console, where modelForThisTrace is the model for which the trace should be executed.

Another option is to simply restore the Trace directly from the TraceConverter

<tt> trace = TraceConverter.restore(modelForThisTrace,"/pathToFile/fileName.xml")</tt>

== How to run a groovy script ==

You can use the build in <tt>run</tt> command to run a groovy script. Simply type

<tt> run pathToScript/script.groovy </tt>

into the console. Code completion is available for the run command.

== How to animate with only the StateSpace abstraction ==

It is also possible to carry out animations without using a trace object.

To get the root vertex from StateSpace space_0, type:

<tt> st = space_0.root </tt>

from there, you can execute a chain of events. For instance,

<tt> st = st.anyEvent("new").anyEvent().new("pp=PID1").new() </tt>

So you can execute anyEvent with the method anyEvent(filter), where filter can be a String name, or a List of names. You can also execute an event with name "name", with the method name(predicate), where predicate is the predicate string intended to filter the solutions for the event. If there are no parameters, the predicate "TRUE = TRUE" will automatically be added.

ProB Java API Tutorial

2013-06-04T12:13:39Z

Joy Clark:

ProB 2.0 is currently experimental. This means that the implementation may change during the course of development. However, we have reached the point in development where some of the features have reached a certain level of stability. Therefore, we are writing this tutorial to explain what those features are.

== How to get started developing with ProB 2.0 ==

The source code for ProB 2.0 is available via GitHub. Click [[https://github.com/bendisposto/prob2|here]] to view the prob2 repository. There is also a short guide available there which will help getting Eclipse set up so that you can get started with the development. Our bugtracker is available [[http://jira.cobra.cs.uni-duesseldorf.de/browse/PROBCORE|here]]. There you can view the features that we are currently working on and can submit new feature requests.

== How to open the Groovy Shell ==

The ProB Groovy shell is available in the Eclipse application. To open it, select

<tt> Window > Show View > Other.. </tt>

Then select

<tt> ProB > Groovy Console </tt>

and hit <tt> ok</tt>.

== How to load a model ==

=== Classical B ===

You can load a Classical B model into the groovy console in two ways. There is a built in <tt>load</tt>. For example:

<tt> load /home/pathToFile/example.mch </tt>

would load example.mch into the console (it will automatically save it into a variable named <tt>model_NUM</tt>, where <tt>NUM</tt> is a unique identifier). The nice thing about the load command is that it allows code completion. Code completion works the same as in a normal console. Hit <tt> <TAB> </tt> to see the code completions that are available.

If you are writing a script that you want to run in the console, you will want to use the <tt> api </tt> variable that is available. There is a method <tt> b_load </tt> that is available to load Classical B models. For example:

<tt> m = api.b_load("/home/pathToFile/example.mch") </tt>

will load example.mch into the variable <tt>m</tt>.

=== Event B ===

To load an Event B model into ProB, right click on the model and select

<tt> Start Animation / Model Checking </tt>

from the context menu that drops down.

== How to animate models ==

The Trace abstraction is available to carry out animations.

=== In The Console ===

There are several different ways that a new transition can be added to the current history. The most important thing to remember is that each Trace object is completely immutable. This means that when you change a trace, you are actually getting a new Trace back. This means that when you carry out an animation step, you always have to make sure that you save the Trace object that is returned.

The simplest way to add a transition is to add it via operation id. For instance, if operation 0 is among the enabled operations for the current state, then

<tt> t = t.add(0) </tt>

will add operation 0 to the current trace, create a new trace, and return it.

You can also add operations via operation name and a list of the parameters. For instance

<tt> t = t.add("new",["PID3"]) </tt>

will add the transition new(PID3) to the trace.

It is also possible to execute any event by executing

<tt> t = t.anyEvent() </tt>

and it is also possible to execute any event with name "name". For instance,

<tt> t = t.anyEvent("name") </tt>

will execute any event with the name "name".

Lastly, it is also possible to execute an event by treating it as if it were a method in the Trace class. For instance,

<tt> t = t.new() </tt>

will execute the event new (by default, the first solution for "new" is chosen). It is also possible to add a predicate as a parameter to filter for a particular solution. For instance,

<tt> t = t.new("pp=PID1") </tt>

will execute new(PID1) as long as pp is the name of the parameter for new.

It also possible to move backwards and forwards within a trace.

Move backwards:

<tt> t = t.back() </tt>

Move forwards:

<tt> t = t.forward() </tt>

=== In The UI ===

In order to animate a loaded model in the UI, double-click on an enabled event in the <tt>Events</tt> view. Then, the resulting trace will automatically be loaded into the different views and it can be further animated. To move backwards and forwards in the trace, use the buttons in the upper right hand corner of the <tt>Events</tt> view.

== How to switch from UI to groovy console ==

There is an easy way to switch from the UI to the groovy console and back. It all happens using the "animations" global variable in the groovy console. What is important to remember, is that in this case, there is no distinction between an animation and a trace.

=== From UI to Console ===

In the UI, switch to the <tt>Current Animations</tt> view. Here you can view the different animations that are available. If the desired animation is not available, double click on it in this view and it will be set as the current animation. Now, to move this animation from the UI to the groovy console, simply type

<tt> x = animations.getCurrentTrace() </tt>

into the groovy console and the current animation will be loaded into the variable <tt>x</tt>.

=== From the Console to the UI ===

If you have a trace saved into variable <tt>trace_0</tt> in the groovy console, you can easily add it to the UI. Simply type

<tt> animations.addNewAnimation(trace_0) </tt>

into the groovy console and the trace will automatically be added to the list of current animations and all of the views will be updated.

== How to carry out evaluations ==

It is very simple to evaluate strings in the groovy console. There is a build in eval method in both the Trace and the StateSpace. In the history, you just need to specify a string and the parser that is needed to parse the string. The two parsers currently available are <tt>ClassicalB</tt> and <tt>EventB</tt>.For instance,

<tt> t.eval("x:NAT" as EventB) </tt>

will parse "x:NAT" using the Event B parser and then will evaluate it at the current state. The following code

<tt> t.eval("x:NAT" as ClassicalB) </tt>

will parse "x:NAT" using the Classical B parser and then will evaluate it at the current state.

Classical B is actually the default parser, so it would also be sufficient to write

<tt> t.eval("x:NAT")</tt>.

It is also possible to evaluate formulas on the SpaceSpace level. For instance, if <tt>space_0</tt> is a StateSpace, you can evaluate a list of formulas by typing

<tt> space_0.eval(space_0[5],["x:NAT" as EventB,"y:NAT" as ClassicalB]) </tt>

into the console. This will parse "x:NAT" with the Event B parser and "y:NAT" with the Classical B parser and then will evaluate them at the state with id 5. The parser is not implicit in the StateSpace, so it is important to specify it here. In order to evaluate a formula, you need to specify the StateId object that is associated with the desired id. To extract a StateId from a StateSpace, you can use the notation <tt>space[ID]</tt> where ID is either a String or an integer representing the StateId that you want to view.

== How to convert between the main abstractions ==

There is a connection between all of the main abstractions. You can easily convert between them by using the <tt>as</tt> operator.

To convert between a Model and a StateSpace, use:

<tt> eventb = statespace_0 as EventBModel </tt> (if you are animating an Event B model)

or

<tt> classicalb = statespace_0 as ClassicalBModel </tt> (if you are animating ClassicalB).

The reverse translation is just as easy:

<tt> space = model as StateSpace </tt>

will return the StateSpace associated with model.

Conversion between a Trace and a StateSpace and between a Trace and Model are also simple. The following conversions are valid:

<tt> space = trace as StateSpace </tt>

<tt> trace = StateSpace as Trace </tt>

<tt> trace = model as Trace </tt>

<tt> model = trace as EventBModel </tt> or <tt> model = trace as ClassicalBModel </tt>

The only thing to mention is that every time you convert from a StateSpace or Model to a Trace, a new trace is created.

== How to save a trace ==

ProB currently supports a mechanism to save a trace in a script so that the same trace can be recreated. We are currently working on some improvements to this mechanism, so expect it to change over the next period of time. Currently, it is possible to save a Trace as an XML trace by typing

<tt>TraceConverter.save(trace_0,"/pathToFile/fileName.xml")</tt>

into the console. This will create the XML file <tt>fileName.xml</tt>.

If you want to load this trace back into the console, there are two options available. You can convert the XML file to a Groovy closure that will then take a Model object and return a Trace with all of the operations specified in the XML file. This can be triggered by calling the method

<tt>TraceConverter.xmlToGroovy("/pathToFile/fileName.xml","/pathToFile/groovyScript.groovy")</tt>

You can then run the produced Groovy script and execute the resulting closure to restore your Trace

<tt>run /pathToFile/groovyScript.groovy</tt>

A script <tt>script_NUM</tt> will be produced. Then enter

<tt> trace = script_NUM(modelForThisTrace) </tt>

into the console, where modelForThisTrace is the model for which the history should be executed.

Another option is to simply restore the Trace directly from the TraceConverter

<tt> trace = TraceConverter.restore(modelForThisTrace,"/pathToFile/fileName.xml")</tt>

== How to run a groovy script ==

You can use the build in <tt>run</tt> command to run a groovy script. Simply type

<tt> run pathToScript/script.groovy </tt>

into the console. Code completion is available for the run command.

== How to animate with only the StateSpace abstraction ==

It is also possible to carry out animations without using a trace object.

To get the root vertex from StateSpace space_0, type:

<tt> st = space_0.root </tt>

from there, you can execute a chain of events. For instance,

<tt> st = st.anyEvent("new").anyEvent().new("pp=PID1").new() </tt>

So you can execute anyEvent with the method anyEvent(filter), where filter can be a String name, or a List of names. You can also execute an event with name "name", with the method name(predicate), where predicate is the predicate string intended to filter the solutions for the event. If there are no parameters, the predicate "TRUE = TRUE" will automatically be added.

Programmatic Abstractions in the ProB 2.0 API

2013-06-04T11:57:19Z

Joy Clark:

== Overview ==

=== Background ===
The ProB 1.0 API takes advantage of one basic abstraction: developers can create Java commands that can be sent to the prolog kernel where something will be calculated. The result can then be used by the developer. Each Java command corresponds to one prolog command in the ProB kernel.

=== Current Implementation ===
The developer is still able to use commands in order to get information from the prolog kernel. But 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.

== 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.

== 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.
It is actually implemented as a graph (using the JGraphT library), so there are built in graph functions and support for graphical representations. In the graph, the vertices are states and the edges are events (including solutions and choices for local variables and non-deterministic assignments).

Conceptually, the state space is completely there and completely evaluated. When you access a state within the StateSpace that has not yet been explored, 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.

The StateSpace object is actually mutable, but it is always growing. No data ever gets replaced by any new data.

== 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.

ProB 2.0 Development

2013-06-04T11:55:11Z

Joy Clark: /* Explanation of the basic programmatic abstractions */

[[Category:Developer Manual]]
__TOC__

== Basic Design Principles ==

One of the main goals 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? ===

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 ==

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 ==

A tutorial for the current features of ProB 2.0 is available [[ProB 2.0 Tutorial|here]].

ProB 2.0 Development

2013-06-04T11:54:53Z

Joy Clark: /* Explanation of the basic programmatic abstractions */

[[Category:Developer Manual]]
__TOC__

== Basic Design Principles ==

One of the main goals 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? ===

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 ==

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 in [[Programmatic Abstractions in the ProB 2.0 API|here]].

== Tutorial of the Current Features of ProB 2.0 ==

A tutorial for the current features of ProB 2.0 is available [[ProB 2.0 Tutorial|here]].

ProB Java API Tutorial

2012-11-30T14:07:16Z

Joy Clark: /* How to animate with only the StateSpace abstraction */

ProB 2.0 is currently experimental. This means that the implementation may change during the course of development. However, we have reached the point in development where some of the features have reached a certain level of stability. Therefore, we are writing this tutorial to explain what those features are.

== How to get started developing with ProB 2.0 ==

The source code for ProB 2.0 is available via GitHub. Click [[https://github.com/bendisposto/prob2|here]] to view the prob2 repository. There is also a short guide available there which will help getting Eclipse set up so that you can get started with the development. Our bugtracker is available [[http://jira.cobra.cs.uni-duesseldorf.de/browse/PROBCORE|here]]. There you can view the features that we are currently working on and can submit new feature requests.

== How to open the Groovy Shell ==

The ProB Groovy shell is available in the Eclipse application. To open it, select

<tt> Window > Show View > Other.. </tt>

Then select

<tt> ProB > Groovy Console </tt>

and hit <tt> ok</tt>.

== How to load a model ==

=== Classical B ===

You can load a Classical B model into the groovy console in two ways. There is a built in <tt>load</tt>. For example:

<tt> load /home/pathToFile/example.mch </tt>

would load example.mch into the console (it will automatically save it into a variable named <tt>model_NUM</tt>, where <tt>NUM</tt> is a unique identifier). The nice thing about the load command is that it allows code completion. Code completion works the same as in a normal console. Hit <tt> <TAB> </tt> to see the code completions that are available.

If you are writing a script that you want to run in the console, you will want to use the <tt> api </tt> variable that is available. There is a method <tt> b_load </tt> that is available to load Classical B models. For example:

<tt> m = api.b_load("/home/pathToFile/example.mch") </tt>

will load example.mch into the variable <tt>m</tt>.

=== Event B ===

To load an Event B model into ProB, right click on the model and select

<tt> Start Animation / Model Checking </tt>

from the context menu that drops down.

== How to animate models ==

The History abstraction is available to carry out animations.

=== In The Console ===

There are several different ways that a new transition can be added to the current history. The most important thing to remember is that each History object is completely immutable. This means that when you change a history, you are actually getting a new History back. This means that when you carry out an animation step, you always have to make sure that you save the history object that is returned.

The simplest way to add a transition is to add it via operation id. For instance, if operation 0 is among the enabled operations for the current state, then

<tt> h = h.add(0) </tt>

will add operation 0 to the current history, create a new history, and return it.

You can also add operations via operation name and a list of the parameters. For instance

<tt> h = h.add("new",["PID3"]) </tt>

will add the transition new(PID3) to the trace.

It is also possible to execute any event by executing

<tt> h = h.anyEvent() </tt>

and it is also possible to execute any event with name "name". For instance,

<tt> h = h.anyEvent("name") </tt>

will execute any event with the name "name".

Lastly, it is also possible to execute an event by treating it as if it were a method in the history class. For instance,

<tt> h = h.new() </tt>

will execute the event new (by default, the first solution for "new" is chosen). It is also possible to add a predicate as a parameter to filter for a particular solution. For instance,

<tt> h = h.new("pp=PID1") </tt>

will execute new(PID1) as long as pp is the name of the parameter for new.

It also possible to move backwards and forwards within a history.

Move backwards:

<tt> h = h.back() </tt>

Move forwards:

<tt> h = h.forward() </tt>

=== In The UI ===

In order to animate a loaded model in the UI, double-click on an enabled event in the <tt>Events</tt> view. Then, the resulting history will automatically be loaded into the different views and it can be further animated. To move backwards and forwards in the history, use the buttons in the upper right hand corner of the <tt>Events</tt> view.

== How to switch from UI to groovy console ==

There is an easy way to switch from the UI to the groovy console and back. It all happens using the "animations" global variable in the groovy console. What is important to remember, is that in this case, there is no distinction between an animation and a history.

=== From UI to Console ===

In the UI, switch to the <tt>Current Animations</tt> view. Here you can view the different animations that are available. If the desired animation is not available, double click on it in this view and it will be set as the current animation. Now, to move this animation from the UI to the groovy console, simply type

<tt> x = animations.getCurrentHistory() </tt>

into the groovy console and the current animation will be loaded into the variable <tt>x</tt>.

=== From the Console to the UI ===

If you have a history saved into variable <tt>history_0</tt> in the groovy console, you can easily add it to the UI. Simply type

<tt> animations.addNewHistory(history_0) </tt>

into the groovy console and the history will automatically be added to the list of current animations and all of the views will be updated.

== How to carry out evaluations ==

It is very simple to evaluate strings in the groovy console. There is a build in eval method in both the History and the StateSpace. In the history, you just need to specify a string and the parser that is needed to parse the string. The two parsers currently available are <tt>ClassicalB</tt> and <tt>EventB</tt>.For instance,

<tt> h.eval("x:NAT" as EventB) </tt>

will parse "x:NAT" using the Event B parser and then will evaluate it at the current state. The following code

<tt> h.eval("x:NAT" as ClassicalB) </tt>

will parse "x:NAT" using the Classical B parser and then will evaluate it at the current state.

Classical B is actually the default parser, so it would also be sufficient to write

<tt> h.eval("x:NAT")</tt>.

It is also possible to evaluate formulas on the SpaceSpace level. For instance, if <tt>space_0</tt> is a StateSpace, you can evaluate a list of formulas by typing

<tt> space_0.eval("5",["x:NAT" as EventB,"y:NAT" as ClassicalB]) </tt>

into the console. This will parse "x:NAT" with the Event B parser and "y:NAT" with the Classical B parser and then will evaluate them at the state with id 5. The parser is not implicit in the StateSpace, so it is important to specify it here.

== How to convert between the main abstractions ==

There is a connection between all of the main abstractions. You can easily convert between them by using the <tt>as</tt> operator.

To convert between a Model and a StateSpace, use:

<tt> eventb = statespace_0 as EventBModel </tt> (if you are animating an Event B model)

or

<tt> classicalb = statespace_0 as ClassicalBModel </tt> (if you are animating ClassicalB).

The reverse translation is just as easy:

<tt> space = model as StateSpace </tt>

will return the StateSpace associated with model.

Conversion between a History and a StateSpace and between a History and Model are also simple. The following conversions are valid:

<tt> space = history as StateSpace </tt>

<tt> history = StateSpace as History </tt>

<tt> history = model as History </tt>

<tt> model = history as EventBModel </tt> or <tt> model = history as ClassicalBModel </tt>

The only thing to mention is that every time you convert from a StateSpace or Model to a History, a new history is created.

== How to save a history ==

ProB currently supports a mechanism to save a history in a script so that the same history can be create. We are currently working on some improvements to this mechanism, so expect it to change over the next period of time. Currently, it is possible to save a History as a script by typing

<tt>HistoryConverter.save(history_0,"/pathToFile/scriptName.groovy")</tt>

into the console. This will create the script <tt>scriptName.groovy</tt>.

To load this history back into the console, type

<tt> run /pathToFile/scriptName.groovy </tt>

A script <tt>script_NUM</tt> will be produced. Then enter

<tt> history_1 = script_NUM(modelForThisHistory) </tt>

into the console, where modelForThisHistory is the model for which the history should be executed.

== How to run a groovy script ==

You can use the build in <tt>run</tt> command to run a groovy script. Simply type

<tt> run pathToScript/script.groovy </tt>

into the console. Code completion is available for the run command.

== How to animate with only the StateSpace abstraction ==

It is also possible to carry out animations without using a history object.

To get the root vertex from StateSpace space_0, type:

<tt> st = space_0.root </tt>

from there, you can execute a chain of events. For instance,

<tt> st = st.anyEvent("new").anyEvent().new("pp=PID1").new() </tt>

So you can execute anyEvent with the method anyEvent(filter), where filter can be a String name, or a List of names. You can also execute an event with name "name", with the method name(predicate), where predicate is the predicate string intended to filter the solutions for the event. If there are no parameters, the predicate "TRUE = TRUE" will automatically be added.

ProB Java API Tutorial

2012-11-30T13:53:39Z

Joy Clark: /* How to run a groovy script */

ProB 2.0 is currently experimental. This means that the implementation may change during the course of development. However, we have reached the point in development where some of the features have reached a certain level of stability. Therefore, we are writing this tutorial to explain what those features are.

== How to get started developing with ProB 2.0 ==

The source code for ProB 2.0 is available via GitHub. Click [[https://github.com/bendisposto/prob2|here]] to view the prob2 repository. There is also a short guide available there which will help getting Eclipse set up so that you can get started with the development. Our bugtracker is available [[http://jira.cobra.cs.uni-duesseldorf.de/browse/PROBCORE|here]]. There you can view the features that we are currently working on and can submit new feature requests.

== How to open the Groovy Shell ==

The ProB Groovy shell is available in the Eclipse application. To open it, select

<tt> Window > Show View > Other.. </tt>

Then select

<tt> ProB > Groovy Console </tt>

and hit <tt> ok</tt>.

== How to load a model ==

=== Classical B ===

You can load a Classical B model into the groovy console in two ways. There is a built in <tt>load</tt>. For example:

<tt> load /home/pathToFile/example.mch </tt>

would load example.mch into the console (it will automatically save it into a variable named <tt>model_NUM</tt>, where <tt>NUM</tt> is a unique identifier). The nice thing about the load command is that it allows code completion. Code completion works the same as in a normal console. Hit <tt> <TAB> </tt> to see the code completions that are available.

If you are writing a script that you want to run in the console, you will want to use the <tt> api </tt> variable that is available. There is a method <tt> b_load </tt> that is available to load Classical B models. For example:

<tt> m = api.b_load("/home/pathToFile/example.mch") </tt>

will load example.mch into the variable <tt>m</tt>.

=== Event B ===

To load an Event B model into ProB, right click on the model and select

<tt> Start Animation / Model Checking </tt>

from the context menu that drops down.

== How to animate models ==

The History abstraction is available to carry out animations.

=== In The Console ===

There are several different ways that a new transition can be added to the current history. The most important thing to remember is that each History object is completely immutable. This means that when you change a history, you are actually getting a new History back. This means that when you carry out an animation step, you always have to make sure that you save the history object that is returned.

The simplest way to add a transition is to add it via operation id. For instance, if operation 0 is among the enabled operations for the current state, then

<tt> h = h.add(0) </tt>

will add operation 0 to the current history, create a new history, and return it.

You can also add operations via operation name and a list of the parameters. For instance

<tt> h = h.add("new",["PID3"]) </tt>

will add the transition new(PID3) to the trace.

It is also possible to execute any event by executing

<tt> h = h.anyEvent() </tt>

and it is also possible to execute any event with name "name". For instance,

<tt> h = h.anyEvent("name") </tt>

will execute any event with the name "name".

Lastly, it is also possible to execute an event by treating it as if it were a method in the history class. For instance,

<tt> h = h.new() </tt>

will execute the event new (by default, the first solution for "new" is chosen). It is also possible to add a predicate as a parameter to filter for a particular solution. For instance,

<tt> h = h.new("pp=PID1") </tt>

will execute new(PID1) as long as pp is the name of the parameter for new.

It also possible to move backwards and forwards within a history.

Move backwards:

<tt> h = h.back() </tt>

Move forwards:

<tt> h = h.forward() </tt>

=== In The UI ===

In order to animate a loaded model in the UI, double-click on an enabled event in the <tt>Events</tt> view. Then, the resulting history will automatically be loaded into the different views and it can be further animated. To move backwards and forwards in the history, use the buttons in the upper right hand corner of the <tt>Events</tt> view.

== How to switch from UI to groovy console ==

There is an easy way to switch from the UI to the groovy console and back. It all happens using the "animations" global variable in the groovy console. What is important to remember, is that in this case, there is no distinction between an animation and a history.

=== From UI to Console ===

In the UI, switch to the <tt>Current Animations</tt> view. Here you can view the different animations that are available. If the desired animation is not available, double click on it in this view and it will be set as the current animation. Now, to move this animation from the UI to the groovy console, simply type

<tt> x = animations.getCurrentHistory() </tt>

into the groovy console and the current animation will be loaded into the variable <tt>x</tt>.

=== From the Console to the UI ===

If you have a history saved into variable <tt>history_0</tt> in the groovy console, you can easily add it to the UI. Simply type

<tt> animations.addNewHistory(history_0) </tt>

into the groovy console and the history will automatically be added to the list of current animations and all of the views will be updated.

== How to carry out evaluations ==

It is very simple to evaluate strings in the groovy console. There is a build in eval method in both the History and the StateSpace. In the history, you just need to specify a string and the parser that is needed to parse the string. The two parsers currently available are <tt>ClassicalB</tt> and <tt>EventB</tt>.For instance,

<tt> h.eval("x:NAT" as EventB) </tt>

will parse "x:NAT" using the Event B parser and then will evaluate it at the current state. The following code

<tt> h.eval("x:NAT" as ClassicalB) </tt>

will parse "x:NAT" using the Classical B parser and then will evaluate it at the current state.

Classical B is actually the default parser, so it would also be sufficient to write

<tt> h.eval("x:NAT")</tt>.

It is also possible to evaluate formulas on the SpaceSpace level. For instance, if <tt>space_0</tt> is a StateSpace, you can evaluate a list of formulas by typing

<tt> space_0.eval("5",["x:NAT" as EventB,"y:NAT" as ClassicalB]) </tt>

into the console. This will parse "x:NAT" with the Event B parser and "y:NAT" with the Classical B parser and then will evaluate them at the state with id 5. The parser is not implicit in the StateSpace, so it is important to specify it here.

== How to convert between the main abstractions ==

There is a connection between all of the main abstractions. You can easily convert between them by using the <tt>as</tt> operator.

To convert between a Model and a StateSpace, use:

<tt> eventb = statespace_0 as EventBModel </tt> (if you are animating an Event B model)

or

<tt> classicalb = statespace_0 as ClassicalBModel </tt> (if you are animating ClassicalB).

The reverse translation is just as easy:

<tt> space = model as StateSpace </tt>

will return the StateSpace associated with model.

Conversion between a History and a StateSpace and between a History and Model are also simple. The following conversions are valid:

<tt> space = history as StateSpace </tt>

<tt> history = StateSpace as History </tt>

<tt> history = model as History </tt>

<tt> model = history as EventBModel </tt> or <tt> model = history as ClassicalBModel </tt>

The only thing to mention is that every time you convert from a StateSpace or Model to a History, a new history is created.

== How to save a history ==

ProB currently supports a mechanism to save a history in a script so that the same history can be create. We are currently working on some improvements to this mechanism, so expect it to change over the next period of time. Currently, it is possible to save a History as a script by typing

<tt>HistoryConverter.save(history_0,"/pathToFile/scriptName.groovy")</tt>

into the console. This will create the script <tt>scriptName.groovy</tt>.

To load this history back into the console, type

<tt> run /pathToFile/scriptName.groovy </tt>

A script <tt>script_NUM</tt> will be produced. Then enter

<tt> history_1 = script_NUM(modelForThisHistory) </tt>

into the console, where modelForThisHistory is the model for which the history should be executed.

== How to run a groovy script ==

You can use the build in <tt>run</tt> command to run a groovy script. Simply type

<tt> run pathToScript/script.groovy </tt>

into the console. Code completion is available for the run command.

== How to animate with only the StateSpace abstraction ==

ProB Java API Tutorial

2012-11-30T13:48:26Z

Joy Clark: /* How to save a history */

ProB 2.0 is currently experimental. This means that the implementation may change during the course of development. However, we have reached the point in development where some of the features have reached a certain level of stability. Therefore, we are writing this tutorial to explain what those features are.

== How to get started developing with ProB 2.0 ==

The source code for ProB 2.0 is available via GitHub. Click [[https://github.com/bendisposto/prob2|here]] to view the prob2 repository. There is also a short guide available there which will help getting Eclipse set up so that you can get started with the development. Our bugtracker is available [[http://jira.cobra.cs.uni-duesseldorf.de/browse/PROBCORE|here]]. There you can view the features that we are currently working on and can submit new feature requests.

== How to open the Groovy Shell ==

The ProB Groovy shell is available in the Eclipse application. To open it, select

<tt> Window > Show View > Other.. </tt>

Then select

<tt> ProB > Groovy Console </tt>

and hit <tt> ok</tt>.

== How to load a model ==

=== Classical B ===

You can load a Classical B model into the groovy console in two ways. There is a built in <tt>load</tt>. For example:

<tt> load /home/pathToFile/example.mch </tt>

would load example.mch into the console (it will automatically save it into a variable named <tt>model_NUM</tt>, where <tt>NUM</tt> is a unique identifier). The nice thing about the load command is that it allows code completion. Code completion works the same as in a normal console. Hit <tt> <TAB> </tt> to see the code completions that are available.

If you are writing a script that you want to run in the console, you will want to use the <tt> api </tt> variable that is available. There is a method <tt> b_load </tt> that is available to load Classical B models. For example:

<tt> m = api.b_load("/home/pathToFile/example.mch") </tt>

will load example.mch into the variable <tt>m</tt>.

=== Event B ===

To load an Event B model into ProB, right click on the model and select

<tt> Start Animation / Model Checking </tt>

from the context menu that drops down.

== How to animate models ==

The History abstraction is available to carry out animations.

=== In The Console ===

There are several different ways that a new transition can be added to the current history. The most important thing to remember is that each History object is completely immutable. This means that when you change a history, you are actually getting a new History back. This means that when you carry out an animation step, you always have to make sure that you save the history object that is returned.

The simplest way to add a transition is to add it via operation id. For instance, if operation 0 is among the enabled operations for the current state, then

<tt> h = h.add(0) </tt>

will add operation 0 to the current history, create a new history, and return it.

You can also add operations via operation name and a list of the parameters. For instance

<tt> h = h.add("new",["PID3"]) </tt>

will add the transition new(PID3) to the trace.

It is also possible to execute any event by executing

<tt> h = h.anyEvent() </tt>

and it is also possible to execute any event with name "name". For instance,

<tt> h = h.anyEvent("name") </tt>

will execute any event with the name "name".

Lastly, it is also possible to execute an event by treating it as if it were a method in the history class. For instance,

<tt> h = h.new() </tt>

will execute the event new (by default, the first solution for "new" is chosen). It is also possible to add a predicate as a parameter to filter for a particular solution. For instance,

<tt> h = h.new("pp=PID1") </tt>

will execute new(PID1) as long as pp is the name of the parameter for new.

It also possible to move backwards and forwards within a history.

Move backwards:

<tt> h = h.back() </tt>

Move forwards:

<tt> h = h.forward() </tt>

=== In The UI ===

In order to animate a loaded model in the UI, double-click on an enabled event in the <tt>Events</tt> view. Then, the resulting history will automatically be loaded into the different views and it can be further animated. To move backwards and forwards in the history, use the buttons in the upper right hand corner of the <tt>Events</tt> view.

== How to switch from UI to groovy console ==

There is an easy way to switch from the UI to the groovy console and back. It all happens using the "animations" global variable in the groovy console. What is important to remember, is that in this case, there is no distinction between an animation and a history.

=== From UI to Console ===

In the UI, switch to the <tt>Current Animations</tt> view. Here you can view the different animations that are available. If the desired animation is not available, double click on it in this view and it will be set as the current animation. Now, to move this animation from the UI to the groovy console, simply type

<tt> x = animations.getCurrentHistory() </tt>

into the groovy console and the current animation will be loaded into the variable <tt>x</tt>.

=== From the Console to the UI ===

If you have a history saved into variable <tt>history_0</tt> in the groovy console, you can easily add it to the UI. Simply type

<tt> animations.addNewHistory(history_0) </tt>

into the groovy console and the history will automatically be added to the list of current animations and all of the views will be updated.

== How to carry out evaluations ==

It is very simple to evaluate strings in the groovy console. There is a build in eval method in both the History and the StateSpace. In the history, you just need to specify a string and the parser that is needed to parse the string. The two parsers currently available are <tt>ClassicalB</tt> and <tt>EventB</tt>.For instance,

<tt> h.eval("x:NAT" as EventB) </tt>

will parse "x:NAT" using the Event B parser and then will evaluate it at the current state. The following code

<tt> h.eval("x:NAT" as ClassicalB) </tt>

will parse "x:NAT" using the Classical B parser and then will evaluate it at the current state.

Classical B is actually the default parser, so it would also be sufficient to write

<tt> h.eval("x:NAT")</tt>.

It is also possible to evaluate formulas on the SpaceSpace level. For instance, if <tt>space_0</tt> is a StateSpace, you can evaluate a list of formulas by typing

<tt> space_0.eval("5",["x:NAT" as EventB,"y:NAT" as ClassicalB]) </tt>

into the console. This will parse "x:NAT" with the Event B parser and "y:NAT" with the Classical B parser and then will evaluate them at the state with id 5. The parser is not implicit in the StateSpace, so it is important to specify it here.

== How to convert between the main abstractions ==

There is a connection between all of the main abstractions. You can easily convert between them by using the <tt>as</tt> operator.

To convert between a Model and a StateSpace, use:

<tt> eventb = statespace_0 as EventBModel </tt> (if you are animating an Event B model)

or

<tt> classicalb = statespace_0 as ClassicalBModel </tt> (if you are animating ClassicalB).

The reverse translation is just as easy:

<tt> space = model as StateSpace </tt>

will return the StateSpace associated with model.

Conversion between a History and a StateSpace and between a History and Model are also simple. The following conversions are valid:

<tt> space = history as StateSpace </tt>

<tt> history = StateSpace as History </tt>

<tt> history = model as History </tt>

<tt> model = history as EventBModel </tt> or <tt> model = history as ClassicalBModel </tt>

The only thing to mention is that every time you convert from a StateSpace or Model to a History, a new history is created.

== How to save a history ==

ProB currently supports a mechanism to save a history in a script so that the same history can be create. We are currently working on some improvements to this mechanism, so expect it to change over the next period of time. Currently, it is possible to save a History as a script by typing

<tt>HistoryConverter.save(history_0,"/pathToFile/scriptName.groovy")</tt>

into the console. This will create the script <tt>scriptName.groovy</tt>.

To load this history back into the console, type

<tt> run /pathToFile/scriptName.groovy </tt>

A script <tt>script_NUM</tt> will be produced. Then enter

<tt> history_1 = script_NUM(modelForThisHistory) </tt>

into the console, where modelForThisHistory is the model for which the history should be executed.

== How to run a groovy script ==

== How to animate with only the StateSpace abstraction ==

ProB Java API Tutorial

2012-11-30T13:45:29Z

Joy Clark: /* How to save a history */

ProB 2.0 is currently experimental. This means that the implementation may change during the course of development. However, we have reached the point in development where some of the features have reached a certain level of stability. Therefore, we are writing this tutorial to explain what those features are.

== How to get started developing with ProB 2.0 ==

The source code for ProB 2.0 is available via GitHub. Click [[https://github.com/bendisposto/prob2|here]] to view the prob2 repository. There is also a short guide available there which will help getting Eclipse set up so that you can get started with the development. Our bugtracker is available [[http://jira.cobra.cs.uni-duesseldorf.de/browse/PROBCORE|here]]. There you can view the features that we are currently working on and can submit new feature requests.

== How to open the Groovy Shell ==

The ProB Groovy shell is available in the Eclipse application. To open it, select

<tt> Window > Show View > Other.. </tt>

Then select

<tt> ProB > Groovy Console </tt>

and hit <tt> ok</tt>.

== How to load a model ==

=== Classical B ===

You can load a Classical B model into the groovy console in two ways. There is a built in <tt>load</tt>. For example:

<tt> load /home/pathToFile/example.mch </tt>

would load example.mch into the console (it will automatically save it into a variable named <tt>model_NUM</tt>, where <tt>NUM</tt> is a unique identifier). The nice thing about the load command is that it allows code completion. Code completion works the same as in a normal console. Hit <tt> <TAB> </tt> to see the code completions that are available.

If you are writing a script that you want to run in the console, you will want to use the <tt> api </tt> variable that is available. There is a method <tt> b_load </tt> that is available to load Classical B models. For example:

<tt> m = api.b_load("/home/pathToFile/example.mch") </tt>

will load example.mch into the variable <tt>m</tt>.

=== Event B ===

To load an Event B model into ProB, right click on the model and select

<tt> Start Animation / Model Checking </tt>

from the context menu that drops down.

== How to animate models ==

The History abstraction is available to carry out animations.

=== In The Console ===

There are several different ways that a new transition can be added to the current history. The most important thing to remember is that each History object is completely immutable. This means that when you change a history, you are actually getting a new History back. This means that when you carry out an animation step, you always have to make sure that you save the history object that is returned.

The simplest way to add a transition is to add it via operation id. For instance, if operation 0 is among the enabled operations for the current state, then

<tt> h = h.add(0) </tt>

will add operation 0 to the current history, create a new history, and return it.

You can also add operations via operation name and a list of the parameters. For instance

<tt> h = h.add("new",["PID3"]) </tt>

will add the transition new(PID3) to the trace.

It is also possible to execute any event by executing

<tt> h = h.anyEvent() </tt>

and it is also possible to execute any event with name "name". For instance,

<tt> h = h.anyEvent("name") </tt>

will execute any event with the name "name".

Lastly, it is also possible to execute an event by treating it as if it were a method in the history class. For instance,

<tt> h = h.new() </tt>

will execute the event new (by default, the first solution for "new" is chosen). It is also possible to add a predicate as a parameter to filter for a particular solution. For instance,

<tt> h = h.new("pp=PID1") </tt>

will execute new(PID1) as long as pp is the name of the parameter for new.

It also possible to move backwards and forwards within a history.

Move backwards:

<tt> h = h.back() </tt>

Move forwards:

<tt> h = h.forward() </tt>

=== In The UI ===

In order to animate a loaded model in the UI, double-click on an enabled event in the <tt>Events</tt> view. Then, the resulting history will automatically be loaded into the different views and it can be further animated. To move backwards and forwards in the history, use the buttons in the upper right hand corner of the <tt>Events</tt> view.

== How to switch from UI to groovy console ==

There is an easy way to switch from the UI to the groovy console and back. It all happens using the "animations" global variable in the groovy console. What is important to remember, is that in this case, there is no distinction between an animation and a history.

=== From UI to Console ===

In the UI, switch to the <tt>Current Animations</tt> view. Here you can view the different animations that are available. If the desired animation is not available, double click on it in this view and it will be set as the current animation. Now, to move this animation from the UI to the groovy console, simply type

<tt> x = animations.getCurrentHistory() </tt>

into the groovy console and the current animation will be loaded into the variable <tt>x</tt>.

=== From the Console to the UI ===

If you have a history saved into variable <tt>history_0</tt> in the groovy console, you can easily add it to the UI. Simply type

<tt> animations.addNewHistory(history_0) </tt>

into the groovy console and the history will automatically be added to the list of current animations and all of the views will be updated.

== How to carry out evaluations ==

It is very simple to evaluate strings in the groovy console. There is a build in eval method in both the History and the StateSpace. In the history, you just need to specify a string and the parser that is needed to parse the string. The two parsers currently available are <tt>ClassicalB</tt> and <tt>EventB</tt>.For instance,

<tt> h.eval("x:NAT" as EventB) </tt>

will parse "x:NAT" using the Event B parser and then will evaluate it at the current state. The following code

<tt> h.eval("x:NAT" as ClassicalB) </tt>

will parse "x:NAT" using the Classical B parser and then will evaluate it at the current state.

Classical B is actually the default parser, so it would also be sufficient to write

<tt> h.eval("x:NAT")</tt>.

It is also possible to evaluate formulas on the SpaceSpace level. For instance, if <tt>space_0</tt> is a StateSpace, you can evaluate a list of formulas by typing

<tt> space_0.eval("5",["x:NAT" as EventB,"y:NAT" as ClassicalB]) </tt>

into the console. This will parse "x:NAT" with the Event B parser and "y:NAT" with the Classical B parser and then will evaluate them at the state with id 5. The parser is not implicit in the StateSpace, so it is important to specify it here.

== How to convert between the main abstractions ==

There is a connection between all of the main abstractions. You can easily convert between them by using the <tt>as</tt> operator.

To convert between a Model and a StateSpace, use:

<tt> eventb = statespace_0 as EventBModel </tt> (if you are animating an Event B model)

or

<tt> classicalb = statespace_0 as ClassicalBModel </tt> (if you are animating ClassicalB).

The reverse translation is just as easy:

<tt> space = model as StateSpace </tt>

will return the StateSpace associated with model.

Conversion between a History and a StateSpace and between a History and Model are also simple. The following conversions are valid:

<tt> space = history as StateSpace </tt>

<tt> history = StateSpace as History </tt>

<tt> history = model as History </tt>

<tt> model = history as EventBModel </tt> or <tt> model = history as ClassicalBModel </tt>

The only thing to mention is that every time you convert from a StateSpace or Model to a History, a new history is created.

== How to save a history ==

ProB currently supports a mechanism to save a history in a script so that the same history can be create. We are currently working on some improvements to this mechanism, so expect it to change over the next period of time. Currently, it is possible to save a History as a script by typing

<tt>HistoryConverter.save(history_0,"/pathToFile/scriptName.groovy")</tt>

into the console. This will create the script <tt>scriptName.groovy</tt>.

== How to run a groovy script ==

== How to animate with only the StateSpace abstraction ==

ProB Java API Tutorial

2012-11-30T13:42:17Z

Joy Clark: /* How to convert between the main abstractions */

ProB 2.0 is currently experimental. This means that the implementation may change during the course of development. However, we have reached the point in development where some of the features have reached a certain level of stability. Therefore, we are writing this tutorial to explain what those features are.

== How to get started developing with ProB 2.0 ==

The source code for ProB 2.0 is available via GitHub. Click [[https://github.com/bendisposto/prob2|here]] to view the prob2 repository. There is also a short guide available there which will help getting Eclipse set up so that you can get started with the development. Our bugtracker is available [[http://jira.cobra.cs.uni-duesseldorf.de/browse/PROBCORE|here]]. There you can view the features that we are currently working on and can submit new feature requests.

== How to open the Groovy Shell ==

The ProB Groovy shell is available in the Eclipse application. To open it, select

<tt> Window > Show View > Other.. </tt>

Then select

<tt> ProB > Groovy Console </tt>

and hit <tt> ok</tt>.

== How to load a model ==

=== Classical B ===

You can load a Classical B model into the groovy console in two ways. There is a built in <tt>load</tt>. For example:

<tt> load /home/pathToFile/example.mch </tt>

would load example.mch into the console (it will automatically save it into a variable named <tt>model_NUM</tt>, where <tt>NUM</tt> is a unique identifier). The nice thing about the load command is that it allows code completion. Code completion works the same as in a normal console. Hit <tt> <TAB> </tt> to see the code completions that are available.

If you are writing a script that you want to run in the console, you will want to use the <tt> api </tt> variable that is available. There is a method <tt> b_load </tt> that is available to load Classical B models. For example:

<tt> m = api.b_load("/home/pathToFile/example.mch") </tt>

will load example.mch into the variable <tt>m</tt>.

=== Event B ===

To load an Event B model into ProB, right click on the model and select

<tt> Start Animation / Model Checking </tt>

from the context menu that drops down.

== How to animate models ==

The History abstraction is available to carry out animations.

=== In The Console ===

There are several different ways that a new transition can be added to the current history. The most important thing to remember is that each History object is completely immutable. This means that when you change a history, you are actually getting a new History back. This means that when you carry out an animation step, you always have to make sure that you save the history object that is returned.

The simplest way to add a transition is to add it via operation id. For instance, if operation 0 is among the enabled operations for the current state, then

<tt> h = h.add(0) </tt>

will add operation 0 to the current history, create a new history, and return it.

You can also add operations via operation name and a list of the parameters. For instance

<tt> h = h.add("new",["PID3"]) </tt>

will add the transition new(PID3) to the trace.

It is also possible to execute any event by executing

<tt> h = h.anyEvent() </tt>

and it is also possible to execute any event with name "name". For instance,

<tt> h = h.anyEvent("name") </tt>

will execute any event with the name "name".

Lastly, it is also possible to execute an event by treating it as if it were a method in the history class. For instance,

<tt> h = h.new() </tt>

will execute the event new (by default, the first solution for "new" is chosen). It is also possible to add a predicate as a parameter to filter for a particular solution. For instance,

<tt> h = h.new("pp=PID1") </tt>

will execute new(PID1) as long as pp is the name of the parameter for new.

It also possible to move backwards and forwards within a history.

Move backwards:

<tt> h = h.back() </tt>

Move forwards:

<tt> h = h.forward() </tt>

=== In The UI ===

In order to animate a loaded model in the UI, double-click on an enabled event in the <tt>Events</tt> view. Then, the resulting history will automatically be loaded into the different views and it can be further animated. To move backwards and forwards in the history, use the buttons in the upper right hand corner of the <tt>Events</tt> view.

== How to switch from UI to groovy console ==

There is an easy way to switch from the UI to the groovy console and back. It all happens using the "animations" global variable in the groovy console. What is important to remember, is that in this case, there is no distinction between an animation and a history.

=== From UI to Console ===

In the UI, switch to the <tt>Current Animations</tt> view. Here you can view the different animations that are available. If the desired animation is not available, double click on it in this view and it will be set as the current animation. Now, to move this animation from the UI to the groovy console, simply type

<tt> x = animations.getCurrentHistory() </tt>

into the groovy console and the current animation will be loaded into the variable <tt>x</tt>.

=== From the Console to the UI ===

If you have a history saved into variable <tt>history_0</tt> in the groovy console, you can easily add it to the UI. Simply type

<tt> animations.addNewHistory(history_0) </tt>

into the groovy console and the history will automatically be added to the list of current animations and all of the views will be updated.

== How to carry out evaluations ==

It is very simple to evaluate strings in the groovy console. There is a build in eval method in both the History and the StateSpace. In the history, you just need to specify a string and the parser that is needed to parse the string. The two parsers currently available are <tt>ClassicalB</tt> and <tt>EventB</tt>.For instance,

<tt> h.eval("x:NAT" as EventB) </tt>

will parse "x:NAT" using the Event B parser and then will evaluate it at the current state. The following code

<tt> h.eval("x:NAT" as ClassicalB) </tt>

will parse "x:NAT" using the Classical B parser and then will evaluate it at the current state.

Classical B is actually the default parser, so it would also be sufficient to write

<tt> h.eval("x:NAT")</tt>.

It is also possible to evaluate formulas on the SpaceSpace level. For instance, if <tt>space_0</tt> is a StateSpace, you can evaluate a list of formulas by typing

<tt> space_0.eval("5",["x:NAT" as EventB,"y:NAT" as ClassicalB]) </tt>

into the console. This will parse "x:NAT" with the Event B parser and "y:NAT" with the Classical B parser and then will evaluate them at the state with id 5. The parser is not implicit in the StateSpace, so it is important to specify it here.

== How to convert between the main abstractions ==

There is a connection between all of the main abstractions. You can easily convert between them by using the <tt>as</tt> operator.

To convert between a Model and a StateSpace, use:

<tt> eventb = statespace_0 as EventBModel </tt> (if you are animating an Event B model)

or

<tt> classicalb = statespace_0 as ClassicalBModel </tt> (if you are animating ClassicalB).

The reverse translation is just as easy:

<tt> space = model as StateSpace </tt>

will return the StateSpace associated with model.

Conversion between a History and a StateSpace and between a History and Model are also simple. The following conversions are valid:

<tt> space = history as StateSpace </tt>

<tt> history = StateSpace as History </tt>

<tt> history = model as History </tt>

<tt> model = history as EventBModel </tt> or <tt> model = history as ClassicalBModel </tt>

The only thing to mention is that every time you convert from a StateSpace or Model to a History, a new history is created.

== How to save a history ==

== How to run a groovy script ==

== How to animate with only the StateSpace abstraction ==

ProB Java API Tutorial

2012-11-30T13:34:52Z

Joy Clark: /* How to carry out evaluations */

ProB Java API Tutorial

2012-11-30T13:23:24Z

Joy Clark: /* How to switch from UI to groovy console */

ProB Java API Tutorial

2012-11-30T13:12:57Z

Joy Clark:

ProB Java API Tutorial

2012-11-30T13:12:21Z

Joy Clark: /* How to animate models */

ProB Java API Tutorial

2012-11-30T12:44:07Z

Joy Clark:

ProB Java API Tutorial

2012-11-30T12:40:37Z

Joy Clark: /* How to load a model */

ProB Java API Tutorial

2012-11-30T12:30:34Z

Joy Clark: Created page with 'ProB 2.0 is currently experimental. This means that the implementation may change during the course of development. However, we have reached the point in development where some o…'

ProB 2.0 Development

2012-11-30T10:32:35Z

Joy Clark: /* Explanation of the basic programmatic abstractions */

[[Category:Developer Manual]]
__TOC__

== Basic Design Principles ==

One of the main goals 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? ===

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 ==

The basic programmatic abstractions that are available in the ProB 2.0 API are the Model, History, 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 History corresponds to exactly one trace throughout the StateSpace. A more detailed description of the different is available in [[Programmatic Abstractions in the ProB 2.0 API|here]].

== Tutorial of the Current Features of ProB 2.0 ==

A tutorial for the current features of ProB 2.0 is available [[ProB 2.0 Tutorial|here]].

ProB 2.0 Development

2012-11-30T10:32:16Z

Joy Clark: /* Tutorial of the Current Features of ProB 2.0 */

[[Category:Developer Manual]]
__TOC__

== Basic Design Principles ==

One of the main goals 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? ===

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 ==

The basic programmatic abstractions that are available in the ProB 2.0 API are the Model, History, 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 History corresponds to exactly one trace throughout the StateSpace. A more detailed description of the different is available in the [[Programmatic Abstractions in the ProB 2.0 API]].

== Tutorial of the Current Features of ProB 2.0 ==

A tutorial for the current features of ProB 2.0 is available [[ProB 2.0 Tutorial|here]].

Programmatic Abstractions in the ProB 2.0 API

2012-11-30T10:23:12Z

Joy Clark: /* History */

== Overview ==

=== Background ===
The ProB 1.0 API takes advantage of one basic abstraction: developers can create Java commands that can be sent to the prolog kernel where something will be calculated. The result can then be used by the developer. Each Java command corresponds to one prolog command in the ProB kernel.

=== Current Implementation ===
The developer is still able to use commands in order to get information from the prolog kernel. But 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.

== 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.

== 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.
It is actually implemented as a graph (using the JGraphT library), so there are built in graph functions and support for graphical representations. In the graph, the vertices are states and the edges are events (including solutions and choices for local variables and non-deterministic assignments).

Conceptually, the state space is completely there and completely evaluated. When you access a state within the StateSpace that has not yet been explored, 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.

The StateSpace object is actually mutable, but it is always growing. No data ever gets replaced by any new data.

== History ==

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 History provides this abstraction.

The History 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 History behaves like a browser history; it is possible to move forward and backward within the current trace.

And important concept to understand when considering the History is that the idea of a "history" is in this sense equivalent with the concept of an "animation". A History corresponds to exactly one animation trace. Each History is associated with exactly one StateSpace, but we can have many different History objects on top of a single StateSpace.

The History is immutable. This means that whenever an animation step is performed (forward, backward, or simply adding a transition to the trace) a new History is returned.

Programmatic Abstractions in the ProB 2.0 API

2012-11-30T10:10:30Z

Joy Clark: /* StateSpace */

Programmatic Abstractions in the ProB 2.0 API

2012-11-30T10:05:05Z

Joy Clark: /* Model */

Programmatic Abstractions in the ProB 2.0 API

2012-11-30T09:48:41Z

Joy Clark: /* Overview */

Programmatic Abstractions in the ProB 2.0 API

2012-11-30T09:45:04Z

Joy Clark:

Programmatic Abstractions in the ProB 2.0 API

2012-11-30T09:33:20Z

Joy Clark: Created page with '__TOC__ == Model == == StateSpace == == History =='

__TOC__

== Model ==

== StateSpace ==

== History ==

ProB 2.0 Development

2012-11-30T09:32:50Z

Joy Clark: /* Explanation of the basic programmatic abstractions */

[[Category:Developer Manual]]
__TOC__

== Basic Design Principles ==

One of the main goals 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? ===

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 ==

The basic programmatic abstractions that are available in the ProB 2.0 API are the Model, History, 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 History corresponds to exactly one trace throughout the StateSpace. A more detailed description of the different is available in the [[Programmatic Abstractions in the ProB 2.0 API]].

== Tutorial of the Current Features of ProB 2.0 ==

Something.

ProB 2.0 Development

2012-11-30T09:07:03Z

Joy Clark: /* Why Groovy? */

[[Category:Developer Manual]]
__TOC__

== Basic Design Principles ==

One of the main goals 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? ===

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 ==

Something.

== Tutorial of the Current Features of ProB 2.0 ==

Something.