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