Steveg
Dear Stefan, thank you for quick answer! If possible, some more
questions (should I create new topics for it?):
- how TLC distinguish between
assignment and comparison? E.g. use of x` = 1 in the action definition will be
considered as assignment, but as comparison in a temporal property? Can primed
variables be used in condition statements in the definition of actions?
x' = 1 is a comparison. There is no assignment in TLA+. You are free to use primed variables in lots of unusual places (unusual if you're thinking assignment).
- what is necessity of
if-then-else operator if conditionality can be naturally expressed with FOL?
All paths through an _expression_ must determine the value of all primed variables (or mark them UNCHANGED). If-then-else is no different than implication in that some expressions are conditional. You can rewrite if-then-else as two implications ( IF x THEN y ELSE z is x => y /\ ~x => z ). If y defines a' and z doesn't the _expression_ is likely invalid (it would be valid if some other path defined a' but that coding style is ugly and hard to maintain).
- work of print function is
quite confusing. I understand that output depends on internal TLC algorithm, so
please advise where I may read more about print?
It's ugly and I haven't figures it out either.
- how TLA+ supports modelling
of concurrent systems - parallelism, synchronisation, atomic operations? There
are no corresponding keywords in TLA+.
Exactly one transition happens at a time. That guarantees atomicity. Parallelism happens when one thread does something and the other threads stutter.
Thanks again, Vitaliy. On Wednesday, November 2, 2016 at 3:40:51 PM UTC+8, vit...@xxxxxxxxxx wrote: Hi, is it possible in TLA to specify and check the property linking values of current and next states, like Prop == (x = 1) => (y` = 2). Seems to be the operation "=" for primed variables (as e.g. y') will be considered as assignement, but not comparison? Tq.
The information contained in this e-mail message and any accompanying files is or may be confidential. If you are not the intended recipient, any use, dissemination, reliance, forwarding, printing or copying of this e-mail or any attached files is unauthorised. This e-mail is subject to copyright. No part of it should be reproduced, adapted or communicated without the written consent of the copyright owner. If you have received this e-mail in error please advise the sender immediately by return e-mail or telephone and delete all copies. UMP does not guarantee the accuracy or completeness of any information contained in this e-mail or attached files. Internet communications are not secure, therefore UMP does not accept legal responsibility for the contents of this message or attached files.
--
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...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
|