# Re: [tlaplus] incorporating modules into other modules when model checking

Hello Richard,

First, note that LQSpec as it is written cannot be used with TLC: the initial condition only specifies that the values of i and o are equal but doesn't say what they are, and similarly LQEnq does not determine the value of i'. For TLC, you probably want to add something like

CONSTANT Data
null == CHOOSE x : x \notin Data

and change the definitions

LQInit ==
/\ q = << >>
/\ i = null
/\ o = null

LQEnq == \E d \in Data :
/\ i' = d
/\ q' = Append(q, i')
/\ o' = o

This being done, you could instantiate the module and use it in another one, like so

LQ == INSTANCE LossyQueue  \* possibly specify some substitutions for the parameters

ProducerConsumer ==
/\ ... \* specification of the producer and consumer processes
/\ LQ!LQSpec

However, while this is a fine TLA formula, you won't be able to give it as a specification to TLC because it expects to see specifications in standard form

Init /\ [][Next]_v /\ L

with a single next-state action. You need to apply some massaging to convert your composed specification to standard form, and you'll end up writing something like

PCNext ==
\/ ...  \* actions of producer and consumer processes
\/ LQ!LQNext /\ UNCHANGED ...  \* P/C variables different from the channels that synchronize with LQ

Chapter 10 of the TLA book discusses composition in more detail.

Best,
Stephan

> On 28 Oct 2015, at 22:34, richard.a...@xxxxxxxxxxxxxx wrote:
>
> 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 # <<>>
>         /\ 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?
>
>
>
>
>
>
> --
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at http://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.