Skip to content

Commit

Permalink
Do not rely on TLC's evaluation order.
Browse files Browse the repository at this point in the history 
Signed-off-by: Markus Alexander Kuppe <[email protected]>
  • Loading branch information
@lemmy
lemmy committed Feb 6, 2024
1 parent 448cc56 commit ea36000
Show file tree
Hide file tree
Showing 2 changed files with 21 additions and 18 deletions.
34 changes: 17 additions & 17 deletions modules/Functions.tla
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,23 @@ RestrictValues(f, Test(_)) ==
LET S == {x \in DOMAIN f : Test(f[x])}
IN Restrict(f, S)

(***************************************************************************)
(* Check if a function narrow is a restriction of a function wide, i.e. *)
(* Is the domain of narrow a subset of that of wide, and does the *)
(* projection of wide on the domain of narrow have the same image as *)
(* narrow does. *)
(* *)
(* Examples: *)
(* IsRestriction([one |-> 1], [one |-> 1, two |-> 2]) *)
(* IsRestriction([one |-> 1], [one |-> 1]) *)
(* ~IsRestriction([one |-> 1, two |-> 2], [one |-> 1, two |-> 3]) *)
(* ~IsRestriction([one |-> 1], [2 |-> two]) *)
(* ~IsRestriction([one |-> 1, two |-> 2], [two |-> 2]) *)
(***************************************************************************)
IsRestriction(narrow, wide) ==
/\ DOMAIN narrow \subseteq DOMAIN wide
/\ \A x \in DOMAIN narrow \intersect DOMAIN wide: narrow[x] = wide[x]

(***************************************************************************)
(* Range of a function. *)
(* Note: The image of a set under function f can be defined as *)
Expand Down Expand Up @@ -150,23 +167,6 @@ FoldFunctionOnSet(op(_,_), base, fun, indices) ==
(***************************************************************************)
MapThenFoldSet(op, base, LAMBDA i : fun[i], LAMBDA s: CHOOSE x \in s : TRUE, indices)

(***************************************************************************)
(* Check if a function narrow is a restriction of a function wide, i.e. *)
(* Is the domain of narrow a subset of that of wide, and does the *)
(* projection of wide on the domain of narrow have the same image as *)
(* narrow does. *)
(* *)
(* Examples: *)
(* IsRestriction([one |-> 1], [one |-> 1, two |-> 2]) *)
(* IsRestriction([one |-> 1], [one |-> 1]) *)
(* ~IsRestriction([one |-> 1, two |-> 2], [one |-> 1, two |-> 3]) *)
(* ~IsRestriction([one |-> 1], [2 |-> two]) *)
(* ~IsRestriction([one |-> 1, two |-> 2], [two |-> 2]) *)
(***************************************************************************)
IsRestriction(narrow, wide) ==
/\ DOMAIN narrow \subseteq DOMAIN wide
/\ \A x \in DOMAIN narrow: narrow[x] = wide[x]

=============================================================================
\* Modification History
\* Last modified Tue Nov 01 08:46:11 CET 2022 by merz
Expand Down
5 changes: 4 additions & 1 deletion tests/FunctionsTests.tla
View file
Original file line number Diff line number Diff line change
Expand Up @@ -107,10 +107,13 @@ ASSUME
g == ("a" :> 1 @@ "b" :> 1 @@ "c" :> 3)
IN Pointwise(f,g,-) = ("a" :> 0 @@ "b" :> 0 @@ "c" :> (-1) )

ASSUME IsRestriction(<<>>, <<>>)
ASSUME IsRestriction(<<>>, [one |-> 1])
ASSUME IsRestriction([one |-> 1], [one |-> 1, two |-> 2])
ASSUME IsRestriction([one |-> 1], [one |-> 1])
ASSUME ~IsRestriction([one |-> 1, two |-> 2], [one |-> 1, two |-> 3])
ASSUME ~IsRestriction([one |-> 1], <<>>)
ASSUME ~IsRestriction([one |-> 1], [two |-> 2])
ASSUME ~IsRestriction([one |-> 1, two |-> 2], [two |-> 2])
ASSUME ~IsRestriction([one |-> 1, two |-> 2], [one |-> 1, two |-> 3])

=============================================================================

0 comments on commit ea36000

Please sign in to comment.