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; most of the GUI code can be found inside main_prob_tcltk_gui.tcl
- 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