| OK, one half is easy because F => <>F is valid for any temporal formula F.
The other half needs some index reasoning:
sigma |= <>[]<>P means that sigma[n ..] |= []<>P for some n \in Nat. [1] Thus, for any m >= n, there is some k >=m such that sigma[k ..] |= P. (*)
You want to prove that sigma |= []<>P, i.e., for any i \in Nat there is some j >= i such that sigma[j ..] |= P.
If i >= n, this follows from (*). If i < n, find a suitable j by applying (*) to n.
Stephan
[1] I write sigma[n ..] to denote the suffix of behavior sigma from index n.
On 21 May 2024, at 16:05, Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:
I do think intuitively <>[]<>P is equivalent to []<>P although I tried for about an hour to prove so without success. A good sign that I really need to work on my proof skills!
Andrew
On Monday, May 20, 2024 at 1:53:12 PM UTC-4 Hillel Wayne wrote:
Expert mode: find a use-case for <>[]<>P (or prove
it's just []<>P or something) H
On 5/19/2024 8:47 AM, Andrew Helwer
wrote:
Oh I figured out the difference myself. []<>P can of
course be true or false of a specific behavior. <>P is
true if P is true at least once at any point in the behavior.
[]<>P is only true when, if P becomes false after becoming
true, it eventually becomes true again.
Andrew
On Sunday, May 19, 2024 at
9:36:27 AM UTC-4 Andrew Helwer wrote:
Examples of constant-level expressions:
- 5 + 15
- 0 .. 10
- {1, 2, 3, 4, 5}
- "foobar"
- op, where op was declared as op == (constant
_expression_)
- x, where x was declared as CONSTANT x
Examples of state-level expressions:
- n + 5, where n was declared as VARIABLE n
- op, where op was declared as op == (state-level
_expression_)
Examples of action-level expressions:
- z' = z + 5, where z was declared as VARIABLE z
- op, where op was declared as op == (action-level
_expression_)
Examples of temporal-level expressions:
- <>[](x > 5), where x was declared as VARIABLE
x
- P ~> Q, where P and Q are action-level expressions
or below (I believe)
There is additional related terminology outside of this:
- State: an assignment of values to variables; variables
are accessed with no prime, like x
- Step: A pair of successive states, where variables are
addressed by being primed or not, like x' or x
- Behavior: An infinite sequence of states
- Spec: A set of behaviors comprising the possible
executions of the system you are modeling
- Formula: a bit of an imprecise term but is usually
used to refer to temporal formulas, so either specs or
temporal-level expressions
Constant-level expressions are just that, they can be
evaluated without reference to any state or anything by just
looking at them. State-level expressions can only be
evaluated within the context of a specific state.
Action-level expressions can only be evaluated within the
context of a specific step. Temporal-level expressions can
only be evaluated within the context of a specific behavior,
or spec.
Actually I'm a bit confused about the last one. It would
seem to me that <>P and []<>P are two different
levels of formulas, since <>P can be true or false of
a specific behavior whereas []<>P seems to be a
statement over multiple behaviors. Can anybody help me out
here?
Anyway how this all helped.
Andrew Helwer
On Sunday, May 19, 2024
at 9:18:13 AM UTC-4 marta zhango wrote:
Systems
are specified as formulas. I also see functions described
using logical connectives such as
implication (=>), conjunction (∧), disjunction
(V) and quantification (\A, \E).
Is TLA+ specified as formulas or functions ? Or
something else ?
On Sunday, May 19,
2024 at 11:08:42 PM UTC+12 marta zhango wrote:
Actually, it is for TLA+ itself. You have
mentioned: constant, state, action, temporal. Any
important
others? Would you be so kind to show a general
syntax for each ?
On Sunday, May 19, 2024 at
11:01:36 PM UTC+12 Stephan Merz wrote:
I don’t know documentation you looked at.
From a user’s perspective, Leslie Lamport’s
video lectures [1] and/or Hillel Wayne’s Web
site and book [2] are probably the best
introduction (with the latter focusing on
PlusCal, but this includes TLA+ expressions).
If you are looking for more mathematical
descriptions covering the language and its
semantics, Specifying Systems [3], the
original paper introducing TLA (but not the
specification language TLA+) [4] or an old
paper of mine [5] may be helpful.
Hope this helps,
Stephan
I actually need some nitpicking.
TLA is a scheme for precise and clear
description,
whereas the documentation is not.
What are the basic constructs then
? As this is what I would like to
neatly summarise.
On Sunday, May 19,
2024 at 9:38:51 PM UTC+12 Stephan
Merz wrote:
In fact, there is no such thing
as "statements" in TLA+, only
formulas of different levels
(constant, state, action,
temporal). This is not nitpicking,
but quite a fundamental
distinction.
Have seen that
statements in TLA are of
the form [A]_p, where A
is an action and p is a
property.
But what are things
without action formalism
like
Cardinality(assignments[t])
and expressions such
as
/\
assignments
\in [Tasks
-> SUBSET
CPUs]
and
IsSorted(seq)
== \A
i,
j \in
1..Len(seq):
i <
j =>
seq[i]
<= seq[j]
What are the latter
? Because they do
not look like TLA
statements
in the form of [A]_p.
--
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.
--
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.
--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/3e3e996b-e96b-432e-bdc1-80c3af1da0afn%40googlegroups.com.
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/34EDA0F0-BE4C-4F65-AF7D-002F31428451%40gmail.com.
|