Subject: Comments on LRM pp 29-66
From: Anthony McIsaac (anthony.mcisaac@st.com)
Date: Mon Oct 07 2002 - 08:28:37 PDT
p 32 line 47
Should be A[->n:inf]
p 40 line 3
General comment on style of these definitions: "The ..... that is the operand" works OK for
short definitions, but gets very cumbersome in later more complex ones.
Perhaps a later version of the manual could considern definitions along the lines
"always P holds if P holds at the given cycle and all subsequent cycles"?
p 41 informal semantics of next
Can i in next[i] be 0. It looks as ifit can; in which case make it clear explicitly tht next[0]P
holds if P holds in the current cycle
p 42 informal semantics of next_a
Again, can lower bound of range be 0?
Say explicitly what bthis means if so.
p 43 informal semantics of next_e
Same again
p 44 informal semantics of next_event
Slightly different point:
Make it clear that you start looking for the "next cycle where the Boolean expression holds"
at the current cycle.
Perhaps change the first 2) to
either the Boolean expression and the FL property both hold at the current cycle, or .....
Similarly throughout.
Also for other variants of next_event
p 47 informal semantics of before.
make it clear that it doesn't matter whether the right-hand operand ever holds.
Perhaps change the first 2) to
either the either the FL property that is the right operand never holds, or .......
Similarly throughout
p 48 informal semantics of until, line 33
What is "that cycle"? Not just any cycle where the FL property holds, but the first occasion
where it does. To be accurate, "either the FL property that is the right operand holds at the current cycle,
or the FL property that is the left operand holds at all cycles up to, but not necessarily including,
the first cycle after the current cycle at which the FL property that is the right operand holds".
Similarly throughout
p49 line 29
nice easy one for a change: should be "all cycles up to and including that cycle"
p 56 line 23
[Restrictions] "Match those of the corresponding non-LTL operators
Anthony
-- Anthony McIsaacSTMicroelectronics Limited 1000 Aztec West Almondsbury Bristol BS32 4SQ
Tel: ++44 (0)1454 462466 Fax: ++44 (0)1454 617910
Email: Anthony.McIsaac@st.com
This archive was generated by hypermail 2b28 : Mon Oct 07 2002 - 08:31:19 PDT