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

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



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


On 5 Jan 2022, at 09:57, Adeeb Abdul Salam <adeebnabdulsalam@xxxxxxxxx> wrote:

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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/5e5b0ddf-7bc3-49a7-b9f8-51955b513dc2n%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/7E53DB11-052B-49D1-9E87-7F61180186BF%40gmail.com.