[SAL-HELP] Parametric SAL models

[Pinter Norbert]

I'm a student at Budapest University of Technology. I'm using the SAL model
checkers, and recently I've encountered a problem.

I tried to implement the Byzantine Generals algorithm (with oral messages)
in the general case: I want to choose the different parameters, such as
round number and number of faulty nodes parametric.

One solution is to maintain an M dimension matrix (for storing the
messages), where M is the number of the rounds. I can't create an M
dimension matrix though, if the M is a parameter.

As a workaround, I'm currently using scripts to generate different instances
of the algorithm, but this is not a nice solution :)

Please help me to solve this problem!

Best regards,
Norbert Pintér