tla+ - 检查 TLA+ 中的变量值

Question

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

Res_Word == {"_","N"}

变量 my_variable = "Some_valueONE"

检查 == my_variable \in Res_Word

* 表示检查变量是否包含集合中所需的某些特定值。

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>>