--
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...@googlegroups.com.
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.
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+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
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.ah...@gmail.com> 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
> 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+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
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.