如何在TLA+中对函数内的元组进行模式匹配？

问题场景 #

我正在建模一个包含三路开关的工业流程，该三路开关属于一个更大的IO数组。需要将两个IO引脚3way1和3way2的布尔值组合，映射为"forward"、"pause"、"backward"三种模式。现有基础代码如下：

VARIABLES
    Input

inputSet == {"3way1", "3way2", ...} \* 其余值无关紧要

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

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

----\* 不变式
ThreewaySwitchIsNeverInvalid == ~(Input.3way1 /\ Input.3way2)

遇到的问题 #

尝试用元组做模式匹配的方式实现映射函数时触发语法错误，错误代码如下：

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

报错信息：Encountered "|->" at line XX column yy in module Factory and token ">>"

移除元组括号后依旧报错：Encountered "|->" at line XX column yy in module Factory and token "FALSE"

解决方案 #

TLA+ 不支持直接用元组作为字面量函数的定义域键来构建映射，换用以下两种方式均可实现需求：

方式一：条件判断实现 #

getMode[x \in [inputSet |-> BOOLEAN]] ==
    IF x.3way1 /\ ~x.3way2 THEN "forward"
    ELSIF ~x.3way1 /\ ~x.3way2 THEN "pause"
    ELSIF ~x.3way1 /\ x.3way2 THEN "backward"
    ELSE \* 受不变式ThreewaySwitchIsNeverInvalid约束，此分支不会触发
        ASSERT FALSE

方式二：先定义合法集合再构建映射函数 #

validPairs == {<<TRUE, FALSE>>, <<FALSE, FALSE>>, <<FALSE, TRUE>>}
modeMap == [p \in validPairs |-> 
    CASE p = <<TRUE, FALSE>> -> "forward"
         p = <<FALSE, FALSE>> -> "pause"
         p = <<FALSE, TRUE>> -> "backward"]

getMode[x \in [inputSet |-> BOOLEAN]] == modeMap[<<x.3way1, x.3way2>>]

内容的提问来源于stack exchange，提问作者Alex Shirley