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

How to add a simple menu command

You need to add an entry in the ProB Tcl/Tk menu. The menus are defined at the top of the file main_prob_tcltk_gui.tcl

  .frmMenu.mnuAnalyse.mnuCoverage add command -label "Number of Values for all Variables" -command {procNrVariableValuesOverStatespace}

You also need to define the Tcl/Tk part of your command (probably inside main_prob_tcltk_gui.tcl):

proc procNrVariableValuesOverStatespace {} {
		if [prolog “tcltk_compute_nr_covered_values_for_all_variables(Res)"] {
			procShowErrors
			procShowTable $prolog_variables(Res) "Coverage Table" "Number of Covered Values for Variables" "CoverageVariablesTable" "" ""
		} else {
		    procShowErrors
		}
}

Observe the use of prolog to call Prolog predicates and $prolog_variables to extract return values obtained from Prolog (which should instantiate the corresponding variable/argument). Also observer that we call procShowErrors, a Tcl/Tk procedure, which extracts all pending error messages and displays them to the user. procShowTable is a utility to display a dialog box containing a table.

Finally, we need to define the called Prolog predicate somewhere in the Prolog code:

tcltk_compute_nr_covered_values_for_all_variables(list([list(['Variable', 'Number of Values'])|VL])) :-
    state_space:get_state_space_stats(NrNodes,_,_),
    format('Computing all values in ~w states for all variables~n',[NrNodes]),
    findall(list([ID,Count]),number_of_values_for_variable(ID,Count),VL),
    format('Finished computing all values for all variables~n',[]).

The use of format is more for debugging (the output will not be seen by ProB Tcl/Tk, just on the console (if any) used to launch ProB Tcl/Tk).

The command is now available and ready to use:

Some useful ProB Tcl/Tk procedures

• procShowErrors: collect all new errors and warnings from the Prolog error_manager and displays them in a dialog (in batch mode they are printed on the console only)
• procShowList, procShowTable: pops up dialog boxes to display lists or tables (lists of lists). Parameters are title of dialog box,…
• procInsertHistoryOptionsState: updates the State, History and Operations (Options) views by calling Prolog and getting information about the current state

Note: the Tcl/Tk code is mostly state-less, almost everything is stored inside Prolog:

• current animation state
• animation history and forward history
• state space (all visited states and transitions)
• all errors that have occurred (stored by the error_manager.pl)
• the current specification
• the state of all the preferences (inside preferences.pl)
• ...