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

[Adeeb Abdul Salam <adeebnabdulsalam@xxxxxxxxx>]

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.