[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
incorporating modules into other modules when model checking
Stephen Merz provided some nice examples of communication primitives a while back: LossyQueue, AsyncInterleavingQueue, SyncInterleavingQueue. For example, the LossyQueue looked like this:
----------------------------- MODULE LossyQueue ---------------------------
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?