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

*From*: Alex <vstrength@xxxxxxxxx>*Date*: Tue, 1 Jun 2021 19:02:41 -0700 (PDT)*References*: <d7826de2-40f7-4224-9c84-2dd3c38bec70n@googlegroups.com> <96f53a07-fec9-4790-a1b1-850334fcdfbdn@googlegroups.com> <250ce0dc-872a-4b2f-860b-0cc6cf44c98cn@googlegroups.com> <ddd9445f-7ffd-4bb2-8f59-6987f51a9731n@googlegroups.com> <6FCE6ED0-924D-456E-9087-0DE15122DECA@gmail.com>

Thanks a lot guys! For someone who interested here is the complete spec that verifies successor function behavior:

```

EXTENDS Integers, TLC

CONSTANT Limit \* Upper bound limit, that model will be testing

ASSUME Limit \in Nat

IntRange == 0..Limit

FPlusOne == [x \in IntRange |-> IF x >= Limit THEN Limit ELSE x + 1] \* Helper function to convert Church numerals to integers

ReducerFunctions == {FPlusOne} \* this functions must all have the same domain and image set (T -> T)

ReducerArguments == IntRange \* must be in the domain of T

ChurchNumbers == [ReducerFunctions -> [ReducerArguments -> ReducerArguments]]

LZero == [f \in ReducerFunctions |-> [x \in ReducerArguments |-> x]] \* Zero numeral

LSucc == \* Successor function for generating next Church numeral

[n \in ChurchNumbers |->

[f \in ReducerFunctions |-> [x \in ReducerArguments |-> f[n[f][x]]] ]

]

VARIABLE

step, \* Execution step, ranging from 0 to Limit

numeral \* Church numeral, produced on each step

TypeOK == \* At every step we'll verify that current Church numeral could be correctly converted to an integer

/\ step = numeral[FPlusOne][0]

/\ PrintT(<<"Reduced Church Numeral", numeral[FPlusOne][0]>>)

Init == \* Start with zero numeral

/\ step = 0

/\ numeral = LZero

SetNext == \* Try up to a "Limit" numbers

/\ step < Limit

/\ numeral' = LSucc[numeral]

/\ step' = step + 1

ComputationComplete == \* Stop, when we tried "Limit" worth of numerals

/\ step = Limit

/\ UNCHANGED<<step, numeral>>

Next ==

\/ SetNext

\/ ComputationComplete

-------------------------------------------------------------------------------

Spec == Init /\ [][Next]_<<step, numeral>>

```

On Monday, May 31, 2021 at 7:06:19 AM UTC-7 leuschel wrote:

Hi,

>

> On 31 May 2021, at 01:41, Alex <vstr...@xxxxxxxxx> wrote:

>

>

> ```

> The first argument of >= should be an integer, but instead it is:

>

I think in your spec it should be

MyNat == 0..Limit

instead of

MyNat == {0..Limit}

In CSP/FDR you write {a..b} for the interval from a to b, but in TLA+/B this is a singleton set containing an interval.

However, even after that correction there is a type error in your construction (s[n[s][z]]).

Greetings,

Michael

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/34f7cb78-889d-48bc-8454-bcf19d380a6bn%40googlegroups.com.

**References**:**[tlaplus] How to pass a function as an argument to the other function?***From:*Alex

**[tlaplus] Re: How to pass a function as an argument to the other function?***From:*Andrew Helwer

**[tlaplus] Re: How to pass a function as an argument to the other function?***From:*Afonso Fernandes

**[tlaplus] Re: How to pass a function as an argument to the other function?***From:*Alex

**Re: [tlaplus] How to pass a function as an argument to the other function?***From:*Michael Leuschel

- Prev by Date:
**[tlaplus] Two translation and annotations work** - Next by Date:
**[tlaplus] Re: Two translation and annotations work** - Previous by thread:
**Re: [tlaplus] How to pass a function as an argument to the other function?** - Next by thread:
**[tlaplus] Two translation and annotations work** - Index(es):