[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Re: Temporal property


On Nov 2, 2016, at 6:13 PM, vit...@xxxxxxxxxx wrote:

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,

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.