incorporating modules into other modules when model checking

[richard.a...@xxxxxxxxxxxxxx]

Hello

Stephen Merz provided some nice examples of communication primitives a while back: LossyQueue, AsyncInterleavingQueue, SyncInterleavingQueue. For example, the LossyQueue looked like this:

----------------------------- MODULE LossyQueue ---------------------------
EXTENDS Sequences
VARIABLES i,o,q

vars == <<o,q>>

LQInit == /\ q = <<>>
          /\ i = o
                    
LQEnq == /\ q' = Append(q,i')
         /\ o' = o

LQDeq == /\ q # <<>>
         /\ o' = Head(q) 
         /\ q' = Tail(q)
         /\ i' = i
                  
LQNext == LQEnq \/ LQDeq

LQLive == WF_vars(LQDeq)                               
LQSpec == LQInit /\ [][LQNext]_vars /\ LQLive

=======================================================================

I want to use a LossyQueue in a larger module to model a queue. And I also want to model check some correctness properties of the larger module which makes use of this LossyQueue. For example, let's say the larger module represents a system composed of a producer, a consumer and the lossy queue and I want to check whether or not messages enq'd by the producer are deq'd by the consumer. Let's say it's called ProducerConsumer.

I expect modules are there to provide reuse, but it isn't clear to me how this LossyQueue module could be reused in ProducerConsumer to model an instance of a lossy queue, nor is it clear to me how the LQSpec defined in this module could or would be incorporated into the model checking of ProducerConsumer. Am I way off track?

What I do at present is to define operations like Enq(q,i) and Deq(q) which operate on a sequence called q to append and remove elements and so behave like a queue. These macros can even be put in their own module, but any underlying sequences which the macros operate on appear in the large module. Is this the only approach I have for incorporating such data structures into my larger modules?