Temporal property

[vit...@ump.edu.my]

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.*
*Universiti Malaysia Pahang <http://www.ump.edu.my>*

[Stephan Merz]

Hello,

I believe that you want to write

  Prop == [][x=1 => y'=2]_<<x,y>>

and check this as a temporal logic property. It asserts that whenever x or y change their values during a transition and x equals 1 in the first state, then y equals 2 in the second state.

Regards,

Stephan

[vit...@ump.edu.my]

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?

 

- what is necessity of if-then-else operator if conditionality can be naturally expressed with FOL?

 

- 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?

 

- how TLA+ supports modelling of concurrent systems - parallelism, synchronisation, atomic operations? There are no corresponding keywords in TLA+.

Thanks again,

Vitaliy.

[Leslie Lamport]

Your questions seem to indicate that you have just seen a little bit about TLA+.  Please tell us what you have read so far about TLA+ so we can suggest what you should do to learn more about it.

Leslie Lamport

[Steve Glaser]

Steveg

On Nov 2, 2016, at 6:13 PM, vit...@ump.edu.my 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,

Vitaliy.

On Wednesday, November 2, 2016 at 3:40:51 PM UTC+8, vit...@ump.edu.my 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.

Universiti Malaysia Pahang

--
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.
For more options, visit https://groups.google.com/d/optout.

[VITALIY MEZHUYEV .]

Dear Leslie,

thank you for your response.

I start with your book "Specifying Systems".

Actually my questions not about syntax of TLA, this is matter of choice.

E.g. for the print function - how it can be used for analyses of TLA model if its work significantly depends on internal structure of TLC algorithm?

Best regards,

Vitaliy.

On Thu, Nov 3, 2016 at 9:45 AM, Leslie Lamport <tlapl...@gmail.com> wrote:

Your questions seem to indicate that you have just seen a little bit about TLA+.  Please tell us what you have read so far about TLA+ so we can suggest what you should do to learn more about it.

Leslie Lamport

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/29WumfrZedo/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@googlegroups.com.

To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

--

Best regards,

Prof. Vitaliy

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.

Universiti Malaysia Pahang

[vit...@ump.edu.my]

Dear Steve, thank you! Very helpful.

[Leslie Lamport]

I start with your book "Specifying Systems".

 

How much of that book have you read?

 

E.g. for the print function - how it can be used for analyses of TLA model if its work significantly depends on internal structure of TLC algorithm?

 

Print(a, b) is defined to equal b.  As far as the meaning of a TLA+ specification goes, you can simply replace every instance of Print(a, b) with b.  When you run TLC on a model of a specification, it prints out lots of things.  What it prints out can depend on whether you write Print(a, b) rather than the equivalent expression b.  If you want to understand the output of TLC, you’ll have to learn about TLC—for example, by reading Chapter 14 of Specifying Systems.

 

Leslie

 

[vit...@ump.edu.my]

Dear Leslie,

 

thank you for your comments. Yes, my reading includes chapter 14.

 

TLA+toolbox is a blackbox, if not provide possibility to explore their internal mechanisms. And this is what users typically expect from Print operator.

 

In chapter 14 you said "TLC usually evaluates an expression many times, so inserting a Print expression in the specification can produce a lot of output." This exactly means that structure of output reflects parsing procedure, but not structure of the model or its behaviour.

 

Print becomes useful if we not only get values, but know points / rules / structure of the output.

And this looks like a problem, especially if we compare parser of a mathematical language with a parser of a programming language, where structure of output is strictly defined.

 

Yes, to implement output in a language composed from formulas Print also should be a formula.

I use Print only as true formula, and try to avoid all possible optimisation issues, but not always may predict / explain structure of Print output. Another point that seems to be the output depends on the TLC version as well.

 

Best regards,

Vitaliy.

[Leslie Lamport]

Dear Vitaliy,

   In chapter 14 you said "TLC usually evaluates an expression many
   times, so inserting a Print expression in the specification can
   produce a lot of output." This exactly means that structure of
   output reflects parsing procedure, but not structure of the model
   or its behaviour.

TLC prints the value when it evaluates the Print statement.
Evaluation is not a mathematical concept; it is something that TLC
does when checking a specification.  It makes no sense to implement
output in a language for writing formulas.  Since printing is
something that's done by TLC, you need to understand TLC to try to
make sense of what gets printed.  Section 14.2 explains in detail how
TLC works; in particular, it explains when TLC evaluates an
expression.  It should explain the output TLC produces for Print
expressions. 

How TLC evaluates expressions depends on the syntactic structure of
the expression (its "parsing") not just on the semantics of the
expression.  I don't know how any program can evaluate an expression
independently of the syntax in which the expression is written.

   Another point that seems to be the output depends on the TLC
   version as well.

I find that surprising, and I would appreciate any example in which
different versions of TLC produce different output from evaluating
Print statements.

Leslie