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

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

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]
/\ PrintT(<<"Reduced Church Numeral", numeral[FPlusOne]>>)

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: