Re: [tlaplus] synchronization using a component

Dear Marko,

I suggest defining a constant named "Threads" to represent the two threads:
CONSTANT Threads

I do not quite understand the purpose of the variables in this spec, but I suggest defining the variables "threadWaiting", "threadVars" and "threadActions":

(******************************************************************)
VARIABLES
threadWaiting,  \* threadWaiting[t] is the same as threadTWaiting.
threadVars,   \* threadVars[t] is the same as threadTVars.
threadActions,   \* threadActions[t] is the same as threadTAction.
(******************************************************************)  

Then you can define your next state relation in the following form:

(******************************************************************)  
SyncThreadNext ==
\/ \E t \in Threads :
/\ waitingForThread(t)
/\ thread(t)
(******************************************************************)  

Adding clear and concise comments to a spec is important and necessary, because it will make the future readers of the spec (including the writer herself) very much grateful!

I also assume you are trying to specify the module "Synchronizer" for future use in other specs. A good spec needs to have everything required to understand it inside itself. Hence, perhaps parameterizing specs is not very useful in practice.

Best Regards,
AmirHossein

On Fri, Jun 14, 2019 at 5:30 PM 'Marko Schuetz-Schmuck' via tlaplus <tlaplus@xxxxxxxxxxxxxxxx> wrote:

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.