[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] synchronization using a component



had meant to reply to the list, but replied to the author only:

-- 
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+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8736kc1g6n.fsf%40tpad-m.i-did-not-set--mail-host-address--so-tickle-me.
For more options, visit https://groups.google.com/d/optout.
Dear Amir,

"Amir A.H.S.A" <amir.ahsa.2011@xxxxxxxxx> writes:

> Dear Marko,
>
> May I suggest you make the following modifications to the Synchronizer spec?

thank you very much for taking the time to consider the spec and to
provide your feedback. I share some thoughts on which I would appreciate
further comment. 

> 1- Change the name "Init" to a more specific name, such as "TSInit" which
> stands for ThreadSyncInit.

I am not fond of names that heavily abbreviate (magical number 7 plus or
minus 2) and so for this reason I would prefer your suggestion
ThreadSyncInit. To bring it in line with the other prominent name maybe
SyncThreadInit.

> 2- Define a next state relation.

Of course, SyncThreadActions(...) is the next state action. From the way
you suggest using TSNext below I assume you are suggesting hiding the
parameters. I tried parameterization of the Synchronizer in other ways
than with operator parameters, but e.g. substituting CONSTANTS or
VARIABLES:

SYNC == INSTANCE Synchronizer WITH threadAAction <- \E d \in Message: CH!Send(d), threadBAction <- CH!Rcv

results in level errors: CH!Send(...) has level 2.

Any suggestions here in particular?

> 3- Define the complete spec in the following form:
> TSSpec ==
> /\ TSInit
> /\ [][TSNext]_<<threadAWaiting, threadBWaiting>>

Yes, although my SyncThreadNext still has parameters.

> 4- Define an invariant of the new spec, after all we need to know what is
> the correctness condition of this specification!
> Adding this invariant will allow you to check the correctness of your
> specification by running the TLC model checker.

Of course. I am thinking about the correctness and/or liveness
conditions...

> 5- Add descriptive comments to each part of the spec, for example:
> (***************************************************************************)
> (* An explanation of the action
> *)
> (***************************************************************************)
> waitingForB(threadAVars) ==
>   threadAWaiting
>     => UNCHANGED threadAVars

I added some such comments, but they seem to me somewhat redundant,
because to me the definitions (choice of names, ...) seemed
self-documenting, but maybe that comes from being immersed in the
topic...

Thanks again for your feedback,

Marko

> Best Regards,
> AmirHossein
>
>
> On Wed, Jun 12, 2019 at 10:38 PM 'Marko Schuetz-Schmuck' via tlaplus <
> tlaplus@xxxxxxxxxxxxxxxx> wrote:
>
>> Dear All,
>>
>> I found it interesting that with TLA+ I can have a component that is
>> responsible of synchronizing the representations of two
>> threads. https://github.com/MarkoSchuetz/synchronizer
>>
>> Best regards,
>>
>> Marko
>>
>> --
>> 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+unsubscribe@xxxxxxxxxxxxxxxx.
>> To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
>> Visit this group at https://groups.google.com/group/tlaplus.
>> To view this discussion on the web visit
>> https://groups.google.com/d/msgid/tlaplus/87ef3y1xsk.fsf%40tpad-m.i-did-not-set--mail-host-address--so-tickle-me
>> .
>> For more options, visit https://groups.google.com/d/optout.
>>
>
> -- 
> 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+unsubscribe@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
> Visit this group at https://groups.google.com/group/tlaplus.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAKxfy0t93-T8dAs1omWT%3DmeKeJ5XYk5eHQVMweAxNA%3DKU2ZDRQ%40mail.gmail.com.
> For more options, visit https://groups.google.com/d/optout.

-- 
Prof. Dr. Marko Schütz-Schmuck
Department of Mathematical Sciences
University of Puerto Rico at Mayagüez
Mayagüez, PR 00681

-- 
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+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8736kc1g6n.fsf%40tpad-m.i-did-not-set--mail-host-address--so-tickle-me.
For more options, visit https://groups.google.com/d/optout.

Attachment: signature.asc
Description: PGP signature