Spinroot

A forum for Spin users

You are not logged in.

#1 2019-03-07 18:31:24

maryam
Member
Registered: 2012-03-27
Posts: 16

Model is too large

Hi,

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

Offline

#2 2019-03-08 01:19:47

spinroot
forum
Registered: 2010-11-18
Posts: 654
Website

Re: Model is too large

How large are the channels?  The size of channels can have a significant impact on verification complexity.
You're not showing the complete model, so it's hard to tell what the main cause is. Are there counters that could be given a smaller range? How many processes? etc.

Offline

#3 2019-03-08 02:24:43

maryam
Member
Registered: 2012-03-27
Posts: 16

Re: Model is too large

I see, so probably it is the channels. I have 5 processes and 10 channels, four of which has size 7, two has size 3, and four has size 1. There is only one counter that is either 0 or 1.

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?

Last edited by maryam (2019-03-08 02:38:25)

Offline

#4 2019-03-08 19:41:42

spinroot
forum
Registered: 2010-11-18
Posts: 654
Website

Re: Model is too large

I would recommend trying to reduce the number of channels and/or the size of the channels.
If you can replace a buffered channel with a rendezvous channel, that will also have a big effect.

Offline

Board footer

Powered by FluxBB