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

[tlaplus] state and step predicate and variable types?

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.

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.