Spinroot

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

Hi,

I have two following statements in the model (the program model is the self-composed model of a program with parallel composition):

   c_code{};
   (!lock);

The first statement is always followed by the second one. So, I wrapped these two statements as an atomic sequence as follows:

   atomic{
        c_code{};
        (!lock);
   }

As expected, the number of states were decreased for concurrent programs (when lock is zero, the sequence is executed indivisibly).
But, the result for sequential programs was surprising, where the number of states were increased a bit little! I cannot understand why?!

many thanks in advance

Can anyone tell me if there is a straightforward way to gain a trace of an execution or not?