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

[Stephan Merz <stepha...@xxxxxxxxx>]

Hello Richard,

thanks for your compliments.

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 # <<>>
>         /\ 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?
> 
> 
> 
> 
> 
> 
> -- 
> 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.