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

*From*: Adeeb Abdul Salam <adeebnabdulsalam@xxxxxxxxx>*Date*: Wed, 5 Jan 2022 05:43:05 -0800 (PST)*References*: <5e5b0ddf-7bc3-49a7-b9f8-51955b513dc2n@googlegroups.com> <7E53DB11-052B-49D1-9E87-7F61180186BF@gmail.com>

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

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"

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 isASSUME 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 definitionk == 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 writec' >= k => E' >= r' * c'in order to restrict transitions to those that satisfy this implication, but perhaps you rather meant to assert the invariantc >= k => E >= r * cand verify that this implication is true for every state along every run of the system? In that case, you should write a definition likeInv == c >= k => E >= r * cand use the TLA+ tools to verify that it holds (but see below).3. [][Next] is not a well-formed formula of TLA+, you should writeSpec == 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,StephanOn 5 Jan 2022, at 09:57, Adeeb Abdul Salam <adeebnab...@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]====================================================================Errors1. CHOOSE is not allowing brackets2. 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.

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/2a207acd-703d-499f-9320-0ee29898a923n%40googlegroups.com.

**References**:**[tlaplus] Parse error was expecting "==== or more module body"***From:*Adeeb Abdul Salam

**Re: [tlaplus] Parse error was expecting "==== or more module body"***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Parse error was expecting "==== or more module body"** - Next by Date:
**Re: [tlaplus] Guarantee message passing** - Previous by thread:
**Re: [tlaplus] Parse error was expecting "==== or more module body"** - Next by thread:
**[tlaplus] Implementing a simple 'proof of work' algorithm in tla+** - Index(es):