Rodin User and Developer Workshop 2013 - Tutorial: Difference between revisions

Here are the information we have shown you at the tutorial. If you want to follow this tutorial on your computer you will have to install ProB 2.0 and start an animation. For this tutorial we use a simple scheduler example. Maybe you have to clean the project after importing.

Setup

You will need a fresh copy of ProB 2.0 installed to your Rodin or the sourcecode.

The update site for our builds is: http://nightly.cobra.cs.uni-duesseldorf.de/experimental/updatesite/

The sourcecode repository and a description how to setup your Eclipse: https://github.com/bendisposto/prob2

Please note that no matter which installation method you chose, you need to fetch the latest Prolog binaries. The easiest way is to type upgrade latest into the ProB 2.0 Groovy console.

In the following we will intermix some explanations with FAQ style code snippets. We assume that you execute all the code snippets. Some of the snippets rely on the previous execution of other snippets.

Preparation

1. Import the Scheduler project.
2. Start an animation for Scheduler0
3. Perform some random animation steps
4. Type s = space_0 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 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 massakr 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 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 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., "1<4" & "x>y" evaluates to "(1<4) & (x>y)". The second line implements a function not that wraps a predicate into a negation. The third line adds an implies method to the class String. "1<2".implies("3<4") results in "(1<2) => (3<4)". The last line converts a list of predicates into a conjunction. In Groovy collect means map and inject means reduce.

Evaluation is fine, but can I use ProB's solver?

f4 = new EventB("a = 1 & b = a - 1")
c4 = new CbcSolveCommand(f4)
s.execute(c4)
c4.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, animations and api.

animations is an Instance of AnimationSelector, api is an instance of Api. The selector maintains lists of Traces and State Spaces. The trace shown in the UI is marked as the current trace. The Api object is used to load models. Most likely we will rename this class and instance in the future to something more meaningful, e.g., loader.

Can I get the trace that is shown in the UI?

animations.getCurrentTrace() 

What traces are registered?

animations.getTraces() 

Can I add a trace to the UI?

animations.addNewAnimation(t) 

Additional Resources

Further information can be found in the developer manual.

Provide Feedback

Please help us improving the documentation by providing