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