Is there a way to match on a tuple, that is part of a larger function?

Question

I'm trying to model an industrial process that has a 3-way switch in it. The 3-way switch is part of a larger IO array. I want to pattern match on the value of these two IO pins, S.T. They enumerate the modes "forward", "pause", "backward"

VARIABLES
    Input

inputSet == {"3way1", "3way2", ...} \* the rest of the values are unimportant

directions == {"forward","pause","backward"}

TypeOk ==
    Input \in [inputSet |-> BOOLEAN]

----
\* Invariants
ThreewaySwitchIsNeverInvalid == ~(Input.3way1 /\ Input.3way2)

The problem that I'm running into, is that I can't seem to pattern match in a sensible way on the Input function.

i.e.

getMode[x \in [inputSet |-> BOOLEAN]] ==
    [<<TRUE, FALSE>> |-> "forward",
    <<FALSE, FALSE>> |-> "pause",
    <<FALSE, TRUE>> |-> "backward"][<<x.3way1, x.3way2>>] 

Errors out with Encountered "|->" at line XX column yy in module Factory and token ">>""

I've also tried to remove the tuple/sequence brackets on the booleans, but then I get Encountered "|->" at line XX column yy in module Factory and token "FALSE"

Answer 1

A solution that I found is:

getPattern [x \in [inputSet -> BOOLEAN]] ==
    CASE x.3way1-> "forward"
    [] x.3way2  -> "pause"
    [] OTHER    -> "backward"

which I'm not a fan of, but it works.

The reason that I wanted a function, and not an operator was that I could compose functions later on with

g \bullet f == [x \in DOMAIN f |-> g[f[x]]]

And this solution works for me

EDIT: Some additional documentation - I found that if you don't want to include TLC, then you can do the following:

(***************************************************************************)
(* Range of a function.                                                    *)
(***************************************************************************)
Range(f) == { f[x] : x \in DOMAIN f }


(***************************************************************************)
(* The inverse of a function.                                             *)
(* Example:                                                                *)
(*    LET f == ("a" :> 0 @@ "b" :> 1 @@ "c" :> 2)                          *)
(*    IN Inverse(f, DOMAIN f, Range(f)) =                                  *)
(*                                 (0 :> "a" @@ 1 :> "b" @@ 2 :> "c")      *)
(* Example:                                                                *)
(*    LET f == ("a" :> 0 @@ "b" :> 1 @@ "c" :> 2)                          *)
(*    IN Inverse(f, DOMAIN f, {1,3}) =                                     *)
(*                                 1 :> "b" @@ 3 :> "a")                   *)
(***************************************************************************)
Inverse(f,S,T) == [t \in T |-> CHOOSE s \in S : t \in Range(f) => f[s] = t]


threeWaySwitch ==   [forward |-> <<TRUE, FALSE>>,
                    pause |-> <<FALSE, FALSE>>,
                    backware |-> <<FALSE, TRUE>>]

getPattern ==
    Inverse(threeWaySwitch , DOMAIN threeWaySwitch , Range(threeWaySwitch))[<<x.3way1, x.3way2>>] 

the definitions for Range and Inverse are in CommunityModules/modules/Functions.tla found here

Answer 2

If you EXTEND TLC, you can write:

getMode[x \in [inputSet -> BOOLEAN]] ==
    (<<TRUE, FALSE>> :> "forward" @@
    <<FALSE, FALSE>> :> "pause" @@
    <<FALSE, TRUE>> :> "backward")[<<x.3way1, x.3way2>>]