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

# Re: [tlaplus] how to input an array constant in TLA+ toolbox?

 Hello,your syntax for specifying the function is not correct. Instead, try(0 :> 5) @@ (1 :> 8) @@ (2 :> 4)or [x \in 0 .. 2 |-> IF x = 0 THEN 5 ELSE IF x = 1 THEN 8 ELSE 4]If you choose to index your functions from 1, you can simply write <<5 ,8 4>> since a function with domain 1..N is a sequence in TLA+.StephanOn 30 May 2020, at 14:17, biao zhang wrote:Hi, I'm learning TLA+ recently. I'm trying to specify a simple program which find the max element in an array as below:-------------------------------- MODULE try --------------------------------EXTENDS IntegersCONSTANT numsCONSTANT lenVARIABLE idxVARIABLE maxInit == /\ idx = 0        /\ max = nums[0]       Next == /\ idx < len        /\ IF nums[idx] > max THEN max' = nums[idx] ELSE max' = max        /\ idx' = idx + 1        Invariant == /\ \A i \in {0..idx} : max >= nums[i]             /\ \E i \in {0..idx} : max = nums[i]      =============================================================================It seems to be correct, but I don't know how to specify the value for nums constant in Model Overview Page of TLA+ toolbox. I have tried this: nums <- [ 0 |-> 5, 1 |-> 8, 2 |-> 4 ]But TLA+ toolbox reports error for the input.Any ideas would be appreciated.Thanks! -- 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/f79f5661-f069-4921-9796-420006e2f517%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/997736BC-1D57-4044-ABF2-E48921171CE5%40gmail.com.