Hi Brett,
And, thanks to Bill Torpey's reply, I should clarify I only had TCP
transport in my mind.
I also only had TCP in my mind. I should have said that.
Wow, that's some modeling! I don't at all grasp how this formal
modeling works but I guess in most practical applications a HWM of 1
would not be very,... well,... "practical".
I believe the large state space of my model comes from the data and
redundant processes I'm modelling. I have lots of buffering going on. Of
course, 0MQ and another protocol that I'm modelling are also
contributing factors. Model checking usually works best for
control-intensive and not data-intensive applications.
Hmm, actually I see zmq_socket_monitor() has[2] a ZMQ_EVENT_DISCONNECTED
event. It seems it would allow an app with a SUB to react directly to a
PUB death without the need to maintain an app-level timeout.
I have never used the socket monitor so don't know its subtleties. In
particular, I'd wonder if the "disconnected" event is generated after
some internal timeout and if so if that would need to be featured in
your modeling.
This socket monitor thing sounds like something I should look into if I
ever get to upgrade my system.
0MQ is a mere complication in my model, though. The main focus is in my
overall distributed system. I think that 0MQ PUB-SUB deserves a model in
its own right. I think it would be a great topic for a research paper to
build a formal model of 0MQ PUB-SUB...
Cheers,
John
_______________________________________________
zeromq-dev mailing list
zeromq-dev@lists.zeromq.org
https://lists.zeromq.org/mailman/listinfo/zeromq-dev
