Reading ....
Richard
On Thursday, October 29, 2015 at 4:13:18 AM UTC-4, Stephan Merz wrote:
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...@googlemail.com 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...@googlegroups.com.
> 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.