ProB Tcl/Tk Architecture

TheProB Tcl/Tk cross-language architecture

The ProB Tcl/Tk contains a mixture of Prolog and Tcl/Tk source code. The core (i.e., the constraint solver, the animation engine, the model checker, ...) are all written in Prolog (which in turn may call some C external functions, e.g., for LTL model checking).

We use the SICStus library(tcltk) (see chapter 10.40 of SICStus manual)

Overall, the communication works as follows:

• on startup ProB launches Tcl/Tk
• from then on Tcl/Tk controls the GUI and calls Prolog predicates
• Tcl/Tk code calls Prolog using 
prolog PRED(…X…Y…)
• Tcl/Tk then gets result values using
 $prolog_variables(X) or $prolog_variables(Y). There are only limited Prolog datatypes that can be transferred from Prolog to Tcl/Tk in this way; see below.
• Tcl/Tk code can also check if a Prolog call was successful, e.g.: 
if [prolog tcltk_backtrack] { … }
• Tcl/Tk code usually calls predicates with tcltk in their name; but there are exception (evaluation_view.tcl calls bvisual2 predicates)

The library(tcltk) puts restrictions on what can be transferred from Prolog to Tcl/Tk and then extracted using $prolog_variables(VAR):

• integer
• atoms (which get translated to Tcl strings)
• lists of integer or atoms
• nested lists of the above; in this case the Prolog code should not return the list but wrap the list result inside a list(.) constructor