The TLA+ definition of records as functions makes it possible to manipulate records in ways that have no counterparts in programming languages. For example, we can define an operator S such that S(r, s) is a record obtained from r by removing each field that is also a field of the record s:
S(r, s) == [ x \in (DOMAIN r \ DOMAIN s) |-> r[x] ]
Now, if we have a set of records defined as
Rec1 == [a : Nat, b : Nat, c : Nat, d : Nat]
we then can define another set of records that have all fields of records in the set Rec1, except the field b, as
Rec2 == { S(r, [b |-> {}]) : r \in Rec1 }
This is quite handy when records in Rec1 have many fields.
S(r, s) == [ x \in (DOMAIN r \ DOMAIN s) |-> r[x] ]
Now, if we have a set of records defined as
Rec1 == [a : Nat, b : Nat, c : Nat, d : Nat]
we then can define another set of records that have all fields of records in the set Rec1, except the field b, as
Rec2 == { S(r, [b |-> {}]) : r \in Rec1 }
This is quite handy when records in Rec1 have many fields.
No comments:
Post a Comment