Other languages

XTL Prolog Format for Transition Systems

You can also use ProB to animate and model check other specification languages by writing your own Prolog interpreter. To do this you should create a Prolog file with the .P extension and which defines three predicates:

• trans/3: this predicate should compute for every state (second argument), the outgoing transitions (first argument), and the resulting new states (third argument)
• prop/2: this predicate should compute the properties for the states of your system
• start/1: this defines the initial states of your system

For example, the following defines a system with two states (a and b) and two transitions (lock and unlock):

start(a).
trans(lock,a,b).
trans(unlock,b,a).
prop(X,X).

These Prolog files can be loaded with ProB's open command (be sure to use the .P extension and to either choose "All files" or "Other Formalisms" in the file filtering menu).

All recognised Prolog Predicates

As of ProB 1.15.0, it is possible to specify symbolic transitions using the predicate symb_trans/3. Such transitions are only available via the execute by predicate dialog and are intended for transitions that require user input or have side effects. symb_trans_enabled(Name,State) can be optionally used to mark states in which a symbolic transition is potentially enabled (not guaranteed).

To provide dynamic transition properties, such as descriptions, the two predicates trans/4 and start/2 can be used, where the last parameter is a list of properties, e.g.

trans(toggle_button,button(A),button(B),[description(toggle_from_to(A,B))]) :- toggle(A,B).

Static properties, such as parameter names, can be provided using trans_prop(TransName,Prop), e.g.

trans_prop(set_button,param_names(['ButtonState'])).

For symbolic transitions it is required to provide parameter names.

The following can be used to set up an animation image matrix with corresponding actions:

• animation_image(Nr,Path)
• animation_function_result(State,List) where List is a list of terms of the form ((Row,Col),Img) where Img is either a declared animation_image number or another Prolog term
• animation_image_right_click_transition(Row,Col,TransitionTemplate)
• animation_image_click_transition(FromRow,FromCol,ToRow,ToCol,ListOfTransitionTemplates,ImageNr)

An example for visualisation can be found at an encoding of the Rush Hour puzzle.

Further recognised predicates are:

• prob_pragma_string(DefinionName,Value): a way to mimic B DEFINITION Strings in XTL mode
• nr_state_properties(Nr): number of state properties displayed in the state view
• heuristic_function_active
• heuristic_function_result(State,Res)

Examples

The following predicates specify a simple button:

start(button(on)).
trans(toggle_button,button(X),button(Y)) :- toggle(X,Y).
trans(set_button(X),_,button(X)) :- X=on ; X=off.
prop(button(X),'='(button,X)).
toggle(on,off).
toggle(off,on).

Another simple example for a very basic process algebra is as follows:

% start(PossibleInitialState)
start(choice(pref(a,stop),intl(pref(b,pref(c,stop)),pref(d,stop)))).

% trans(Event, StateBefore, StateAfter)
trans(A,pref(A,P),P). % action prefix
trans(A,intl(P,Q),intl(P2,Q)) :- trans(A,P,P2). % interleave
trans(A,intl(P,Q),intl(P,Q2)) :- trans(A,Q,Q2).
trans(A,par(P,Q),par(P2,Q2)) :- trans(A,P,P2), trans(A,Q,Q2). % parallel composition
trans(A,choice(P,Q),P2) :- trans(A,P,P2). % choice
trans(A,choice(P,Q),Q2) :- trans(A,Q,Q2).

% prop(State, PropertyOfState)
prop(pref(A,P),prefix).
prop(intl(P,Q),interleave).
prop(A,A).

If you have a working interpreter, you can also contact the ProB developers in order for your interpreter to be included in the standard ProB distribution (in the style of the CSP-M or Promela interpreters). With this you can add syntax highlighting, error highlighting in the source code, highlighting during animation, support for new LTL properties,...

Another, slightly more elaborate example, is the following interpreter for regular expressions:

/* A simple animator for regular expressions */

start('|'('.'('*'(a),b) ,  '.'('*'(b),a))). 

trans(_,[],_) :- !,fail.
trans(X,X,[]) :- atomic(X),!.
trans(X,'|'(R1,R2),R) :- 
 trans(X,R1,R) ; trans(X,R2,R).
trans(X,'.'(R1,B),R) :- trans(X,R1,R2),
 gen_concat(R2,B,R).
trans(X,'?'(R1),R) :-
 trans(X,R1,R) ; (X=epsilon,R=[]).
trans(epsilon,'*'(_R1),[]). 
trans(X,'*'(R1),R) :- 
 trans(X,R1,R2),
 gen_concat(R2,'*'(R1),R).
trans(X,'+'(R1),R) :- 
 trans(X,R1,R2),
 gen_concat(R2,'*'(R1),R).

gen_concat(R1,R2,R) :- 
 (R1=[] -> R = R2 ; R = '.'(R1,R2)).

prop(X,X).

Finally, a more complex example is an encoding of the Rush Hour puzzle which also includes a graphical visualisation (using the animation_function_result predicate recognised by ProB as of version 1.4.0-rc3).

Using VisB in XTL mode

Since ProB 1.15.0, it is possible to use VisB with XTL specifications. For this, a B (!) definition file (.def) must be used, as with B models, which enables the use of VisB DEFINITIONS. The B definition file can the be linked to the specification using

prob_pragma_string('VISB_DEFINITIONS_FILE',PathToFile).

(or via the VisB view in ProB2-UI). To access the value of state properties in the current state, e.g. for VisB updates, the external function STATE_PROPERTY(NameOfProp) can be used, where NameOfProp corresponds to a property of the special style '='(Name,Value) in prop/2.

Note that for event predicates the parameter values must be wrapped in STRING_TO_TERM, e.g.

rec(event: "set_button", predicate: "buttonState = STRING_TO_TERM(\"on\")")

Promela

Version 1.2.7 of ProB (July 2008) was able to open Promela files. This mode provided source-level highlighting during animation. The main purpose was to debug and animate Promela specifications in a user-friendly way. We do not plan to compete in terms of model checking speed with Spin (Spin compiles Promela to C code, ProB uses a Prolog interpreter). To animate a Promela model, simply open the file with the .pml or .prom extension with the "File->Open..." command. You will have to choose "Other Formalisms" or "All Files" in the filter pop-up-menu to be able to select the file.

This direct support of Promela files has been discontinued, but the Promela interpreter is still available as an XTL Prolog specification (see above) and can thus be used to animate Promela specifications with ProB.