Re: [tlaplus] synchronization using a component

• From: "'Marko Schuetz-Schmuck' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>
• Date: Fri, 14 Jun 2019 08:53:36 -0400

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.

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

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

> 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

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
> *)
> (***************************************************************************)

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...

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
>>
>> 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
>> .
>> 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.