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

Re: [tlaplus] Re: Temporal property

Dear Steve, thank you! Very helpful.

On Thursday, November 3, 2016 at 9:55:43 AM UTC+8, Steve Glaser wrote:


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.