检查TLA+中的变量值

Question

我必须在TLC中使用TLA+检查变量值。例如

Res_Word == {"_"，"N"}

变量my_variable = "Some_valueONE“

Check == my_variable \in Res_Word

*表示检查变量是否包含set中要求的某些特定值。

Answer 1

您所提供的方法的具体问题是什么？下面是一个PlusCal示例。

---- MODULE test ----
EXTENDS Integers, Sequences, TLC, FiniteSets
(* --algorithm test
variables res_positive_match = "N", res_negative_match = "Y";
define
    Res_Word == {"_","N","M"}
    NotInResWord == res_negative_match \in Res_Word
end define;

begin P:
  print <<"res_positive_match:", res_positive_match \in Res_Word>>;
  print <<"res_negative_match:", res_negative_match \in Res_Word, "NotInResWord:", NotInResWord>>;
  print <<"sets matching:", {"N","_"} \subseteq Res_Word>>;
end algorithm; *)
\* BEGIN TRANSLATION
\* END TRANSLATION
=====

它输出类似以下内容：

<<"res_positive_match:", TRUE>>
<<"res_negative_match:", FALSE, "NotInResWord:", FALSE>>
<<"sets matching:", TRUE>>