[tlaplus] state and step predicate and variable types?

[ns <nedsri1988@xxxxxxxxx>]

Suppose I wanted to define a generic way of making a spec from components

mk(si) == si.init /\ [][si.next]_si.vars

so i could say something like

Init1 == x=0
Next1 == x'>x

vars1 == <<x>>
si == [init |-> Init1, next |-> Next1, vars |-> vars1]
Spec == mk(si)

If I wanted to declare the Record Type call it SpecInfo, what should the "types" of the various fields of SpecInfo be?

SpecInfo == [init:?, next:?, vars:?]

I can sort of see how I might be able to make the init and next fields be functions, but i'm not sure what to do with the vars field.

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/c160a340-aab7-4ec4-96f1-44192fabc21fn%40googlegroups.com.