1. Whenever possible use rendezvous communication, i.e., use channels with size 0 instead of size > 0.
2. Minimize the number of channels even if this means increasing the number of possible symbols to be sent over a channel. For instance, if you have A and B processes, with A sending ack to B and B sending ack to A over two channels AtoB and BtoA, you could reduce this to one channel AandB and have messages ack_from_A and ack_from_B.
3. As much as possible encode logic using labels and goto statements instead of higher-level (more C-like) constructs. So, loosely, try to make the code look more like assembly, and less like C.
4. Use mtypes instead of shorts/integers/doubles/etc. as much as possible as they force you to clarify your ideas in as finite of a manner as you can.
Would you agree with all this advise? Are there any other general tips you would reccomend?
Thank you!
]]>I guess one solution to decrease the model size is using arrays instead of channels and implement send and receive for them as d_steps. I appreciate if you have a better suggestion?
]]>I am modeling a quasi-synchronous system, which consists of several processes, and processes communicate through channels. I have modeled each process similar to the controller process in the following. Every process is activated periodically, reads all messages in its inbox channels atomically, do local computation, and publishes messages. Publishing messages to different channels can be interleaved by other processes execution. To model the interleaving between a message publish and its delivery, I am using two separate channels. commchan_topicname maintains messages published but not delivered yet, and ch_topicname shows the inbox of a process for that topic. There is also a process called deliver, which nondeterministically delivers a message to a process inbox (removes a message from commchan_topicname and sends it to ch_topicname). The model has four such processes plus the deliver process, and it consumes a lot of memory, while it seems simpler than that, as I have wrapped most sequences in a d_step block. Any idea what is wrong in my model, which causes significant memory consumption?
proctype ControllerP()
{
bool indngr = false;
short pwr = 10;
do
:: len(ch_danger) >= cont_danger_min && len(ch_speed) >= cont_speed_min && len(ch_go) >= cont_go_min ->
d_step {
read_chan(ch_danger, local_bfr_danger, cont_danger_size);
read_chan(ch_speed, local_bfr_speed, cont_speed_size);
read_chan(ch_go, local_bfr_go, cont_go_size) };
d_step { step_controller(); };
len(ch_power) + len(commchan_power) < act_power_size ->
d_step { publish(tpcPowerId, pwr); };
len(ch_indanger) + len(commchan_indanger) < opt_indanger_size ->
d_step { publish(tpcIndangerId, indngr); };
od;
}