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

*From*: Abhishek Verma <vermaabhishekp@xxxxxxxxx>*Date*: Fri, 28 Jan 2022 09:48:03 -0800*References*: <5e95d1a9-a04c-4738-ab70-e74bdd320fbf@googlegroups.com> <A85FA054-FF3F-400B-B90C-41CA073E9AEC@lemmster.de>

Hi Markus,

Thank you for writing a clear spec for Huang's algorithm. I learned a few TLA+ features from it.

I tried executing the spec in TLA+ toolbox, but I got an error message that the DyadicRationals module could not be found. Where can I find the DyadicRationals module used in the spec? I could not find it on Google or in the Community modules: https://github.com/tlaplus/CommunityModules.

Thanks!

-Abhishek.

On Wed, Jan 26, 2022 at 10:50 AM <tlaplus-google-group@xxxxxxxxxxx> wrote:

https://github.com/tlaplus/Examples/tree/master/specifications/Huang is a spec of Huang’s weight-throwing algorithm.--MarkusOn Oct 5, 2018, at 2:58 PM, Nipun sehrawat <nipunse...@gmail.com> wrote:Hello,I am learning TLA+ and trying to write a spec for the weight-throwing algorithm described in: https://ieeexplore.ieee.org/document/37933.I wrote this simple spec for checking if TLC allows division in an action _expression_:----------------------------- MODULE WeightThrowing ----------------------------EXTENDS RealsVARIABLES countVARIABLES numInit == /\ num = 1/\ count = 0Next == /\ num' = num / 2/\ count' = count + 1================================================================================As expected, TLC didn't like this spec (perhaps because TLC doesn't support arbitrary precision arithmetic?). Here is the error I get:TLC threw an unexpected exception.This was probably caused by an error in the spec or model.See the User Output or TLC Console for clues to what happened.The exception was a java.lang.RuntimeException: Attempted to compute the value of an _expression_ ofform CHOOSE x \in S: P, but S was not enumerable.line 16, col 10 to line 16, col 38 of module RealsThe error occurred when TLC was evaluating the nestedexpressions at the following positions:0. Line 11, column 9 to line 12, column 29 in WeightThrowing1. Line 11, column 12 to line 11, column 25 in WeightThrowing2. Line 11, column 19 to line 11, column 25 in WeightThrowing3. Line 16, column 10 to line 16, column 38 in RealsAny suggestions around how to express a weight throwing algorithm in TLA+? I basically want the ability to split a weight, W, into two parts, W1 and W2, such that W1+W2=W. The splitting will happen multiple times as the system state evolves. Additionally, the initial value of W should be 1.Thank you,Nipun

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/A85FA054-FF3F-400B-B90C-41CA073E9AEC%40lemmster.de.

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/CABvW1%2BrM3e2eS8EP-V%3DTP1rppgyO51n0dWP3Wz7jjTytfkJQ9w%40mail.gmail.com.

**Follow-Ups**:**Re: [tlaplus] Division in action expression***From:*tlaplus-google-group

**References**:**Division in action expression***From:*Nipun sehrawat

**[tlaplus] Re: Division in action expression***From:*tlaplus-google-group

- Prev by Date:
**[tlaplus] Re: model value** - Next by Date:
**Re: [tlaplus] Division in action expression** - Previous by thread:
**[tlaplus] Re: Division in action expression** - Next by thread:
**Re: [tlaplus] Division in action expression** - Index(es):