Wrong arguments passed to generated command

[michalwski]

I've created this [1] proper_statem which tests sending messages between XMPP users connected over BOSH or WS. In some cases the generated commands look like this:

[{set,{var,1},{call,bosh_interleave_reqs,connect_carol,[]}},
 {set,{var,2},{call,bosh_interleave_reqs,connect_geralt,[]}},
 {set,{var,3},
  {call,bosh_interleave_reqs,send_from_geralt, [{var,2},{var,1}]}},
 {set,{var,18},
  {call,bosh_interleave_reqs,send_from_geralt, [{var,2},{var,1}]}},
 {set,{var,19},
  {call,bosh_interleave_reqs,wait_for_msgs_carol,
   [{var,1},[{var,18}]]}}]

The error is in the wait_for_msgs_carol function. It should take [{var 18}, {var, 3}] as the second arg, but somehow it takes [{var 18}].

{var, 18} and {var, 3} are results of send_from_geralt function, and they are added to the statem's state. When I traced the state changes, it looked ok, both results where on the correct list but somehow in the end the wait_for_msgs_carol function was invoked with wrong list.

Am I doing sth wrong in my statem's implementation?

[1]. bosh_interleave_reqs.erl

[kostis]

If you want some help to debug this, please provide some self-contained module that shows the problem. I do not even know where to find escalus/include/escalus.hrland have no intention of finding out how to compile and install MongooseIM and all the infrastructure that it may require.

[michalwski]

OK, I'm shrinking the problem to sth more generic.

[michalwski]

Ok, I've created smaller example [1].

This reproduces the real problem I've found with MongooseIM. There is indeed a bug in MongooseIM which delivers the same message twice under some circumstances.

This fails given PropEr tests which is expected. Now PropEr tries to shrink the commands' sequence and generates wrong sequence when not every arguments from state are passed to the wait_for_msgs_* function.

In the smaller example, I'm generating a wrong message after 10th read. And the minimal example found by PropEr looks like this (for me):

[{set,{var,1},
      {call,send_messages_command_generator,connect_carol,[]}},
 {set,{var,2},
      {call,send_messages_command_generator,connect_geralt,[]}},
 {set,{var,3},
      {call,send_messages_command_generator,send_from_carol,
            [{var,1},{var,2}]}},
 {set,{var,25},
      {call,send_messages_command_generator,send_from_carol,
            [{var,1},{var,2}]}},
 {set,{var,26},
      {call,send_messages_command_generator,send_from_carol,
            [{var,1},{var,2}]}},
 {set,{var,27},
      {call,send_messages_command_generator,wait_for_msgs_geralt,
            [{var,2},[{var,26},{var,25}]]}}]

The last function wait_for_msgs_geralt should get [{var, 3},{var,26},{var,25}] as input.

Also, curious fact to me is the var sequence in the minimal example. We can see that after {var, 3} the next var is {var 25}.

[1]. send_messages_command_generator

[kostis]

I do not fully understand all the gory details of your program but your commands look like:

[{call, ?MODULE, connect_carol, []} || not Carol] ++
[{call, ?MODULE, connect_geralt, []} || not Geralt] ++
[{call, ?MODULE, send_from_carol, [S#state.carol, S#state.geralt]} || Users] ++
[{call, ?MODULE, send_from_geralt, [S#state.geralt, S#state.carol]} || Users] ++
[{call, ?MODULE, wait_for_msgs_carol, [S#state.carol, S#state.msgs_to_carol]}
     || MsgsToCarol] ++
[{call, ?MODULE, wait_for_msgs_geralt, [S#state.geralt, S#state.msgs_to_geralt]}
     || MsgsToGeralt].

The carol and geralt fields of the state are presumably booleans while the msgs_to_carol and msgs_to_geralt fields are presumably lists. (By the way, why don't you use typed records?? You should!).

Anyway, if you want the following that you write:

The last function wait_for_msgs_geralt should get [{var, 3},{var,26},{var,25}] as input.

shouldn't the commands you have defined look like this instead?

[{call, ?MODULE, connect_carol, []} || not Carol] ++
[{call, ?MODULE, connect_geralt, []} || not Geralt] ++
[{call, ?MODULE, send_from_carol, [S#state.carol, S#state.geralt]} || Users] ++
[{call, ?MODULE, send_from_geralt, [S#state.geralt, S#state.carol]} || Users] ++
[{call, ?MODULE, wait_for_msgs_carol, [S#state.carol | S#state.msgs_to_carol]}
     || MsgsToCarol] ++
[{call, ?MODULE, wait_for_msgs_geralt, [S#state.geralt | S#state.msgs_to_geralt]}
     || MsgsToGeralt].

Note the | instead of the , in the last two list comprehensions.

[kostis]

Rethinking my answer/suggestion above, I actually do not see what the problem with the original code is.
Your wait_for_msgs_geralt function has arity 2 so it should take an element and a list of messages as input, i.e., something of the form [{var,X}, [{var,N},{var,M}]] and not something of the form [{var,X},{var,N},{var,M}] as you write.

Bottomline: either there is no problem in PropEr, or you have not explained well/precisely what the problem is.

[michalwski]

Thanks for looking at my issue @kostis.

I probably could describe the problem better. Let me try again.

Big picture: this test generates commands for sending messages from carol to geralt (and the other way around) and reading these messages by these users.

The main issue I've found is the last generated command which looks like this:

{set,{var,27},
      {call,send_messages_command_generator,wait_for_msgs_geralt,
            [{var,2},[{var,26},{var,25}]]}}]

It looks fine, 2 arguments are passed, the second being the list of messages sent form carol to geralt. But if you look at all the commands generated by PropEr (in the shrunk sequence), the second argument should be list of 3 elements and not 2. The reason why is that function send_from_carol (send message from carol to geralt) was generated 3 times, and produced messages {var, 3}, {var, 25}, {var, 26}.

My question is: why message {var, 3} was omitted while generating the function wait_for_msgs_geralt.

Please note that, this wrong list of messages is generated only when proper tries to shrink commands to find minimal case.

[michalwski]

@kostis, is my latest explanation clear enough or do you have other questions?