Re: [tlaplus] Parse error was expecting "==== or more module body"

• Date: Wed, 5 Jan 2022 05:43:05 -0800 (PST)
• Ironport-hdrordr: A9a23:9hpwOK1ROKBXN4tx2VVeywqjBKckLtp133Aq2lEZdPU1SK2lfq+V98jzuSWftN9zYh8dcLK7VJVoKEm0naKdirN/AV7WZniFhILeFvAG0WKN+VDd8lXFh41gPPBbE5RDNA==

Thank you so much for the detailed explaination. I understood a great deal. And this is my final spec

-------------------------------- MODULE nuke --------------------------------
EXTENDS Reals,Naturals
CONSTANTS m,k
VARIABLES c,E,r

ASSUME (m \in Real) /\ (m > 0)
ASSUME k \in Nat /\ ( ( ((2*k-1)^2 - 1) > 4/m ) /\ ( ((2*k-3)^2 -1) < 4/m ) )

Init ==  (c=0) /\ (r=0) /\ (E=0)

Next ==    /\ (c' = c+1)
/\ E' = IF c' >= k THEN m*(c'^2) ELSE 0
/\ r' = IF c' >= k THEN m+(1/c') ELSE 0

Spec == Init /\ [][Next]_<<c,E,r>>
=============================================================================

But it failed nevertheless
Evaluating assumption line 22, col 8 to line 22, col 30 of module nuke failed.
Attempted to check if the value:
m
is an element of the string "Reals"

I guess this means there is a bug in my model afterall.
On Wednesday, January 5, 2022 at 12:49:32 PM UTC+3 Stephan Merz wrote:
Hello,

concerning the syntax errors:

1. Your _expression_ "CHOOSE k \in Nat : P(k)" appears where TLA+ expects a definition, an axiom / assumption or a theorem. Since m and k are declared as constants, I believe what you really mean is

ASSUME k \in Nat /\ (k > (1+(1+4/m)^0.5) / 2) /\ (k < (2+(1+4/m)^0.5) / 2)

Alternatively, you could remove the constant parameter k and write the definition

k == CHOOSE k \in Nat : ( (k > (1+(1+4/m)^0.5) / 2) /\ (k < (2+(1+4/m)^0.5) / 2) )

but presumably you'd like to check your spec for all possible values of k rather than a fixed one.

2. The final conjunct of your next-state relation is incomplete because the ELSE branch is missing. Perhaps you meant to write

c' >= k => E' >= r' * c'

in order to restrict transitions to those that satisfy this implication, but perhaps you rather meant to assert the invariant

c >= k => E >= r * c

and verify that this implication is true for every state along every run of the system? In that case, you should write a definition like

Inv == c >= k => E >= r * c

and use the TLA+ tools to verify that it holds (but see below).

3. [][Next] is not a well-formed formula of TLA+, you should write

Spec == Init /\ [][Next]_<<c,E,r>>

4. Although not an error, it is a bit strange that your definitions of the initial predicate and the next-state relation are written as disjunctions with a single disjunct. You may want to remove the leading "\/" (but perhaps this is a simplified version and you have other disjuncts in mind).

–––

More fundamentally, while TLA+ has a standard module representing the real numbers, the currently available TLA+ tools (the model checkers TLC and Apalache as well as the interactive proof system TLAPS) do not support real numbers. I am therefore afraid that TLA+ is not the most appropriate formalism for what you are trying to do.

Best regards,

Stephan

I am a novice to formal verification, please forgive my begginer doubts.

-------------------------------- MODULE nuke --------------------------------
EXTENDS Reals,Naturals
CONSTANTS m,k
VARIABLES c,E,r

ASSUME (m \in Real) /\ (m > 0)
CHOOSE k \in Nat : ( (k > (1+(1+4/m)^0.5) / 2) /\ (k < (2+(1+4/m)^0.5) / 2) )

Init == \/ /\ c=0
/\ r=0
/\ E=0

Next == \/ /\ c' = c+1
/\ E' = IF c' >= k THEN m*(c'^2) ELSE 0
/\ r' = IF c' >= k THEN m+(1/c') ELSE 0
/\ IF c'>=k THEN E'>r'*c'

Spec == Init /\ [][Next]
====================================================================

Errors
1. CHOOSE is not allowing brackets
2. TLC is not allowing real values (0.5) , how am I supposed to get root then ?
3. My final assertion is this IF c'>=k THEN E'>r'*c' , where/how can I specify this ?
4. Does TLA+ support ceiling function ?

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