问题标签 [pluscal]

我使用 PlusCal 来模拟一个接受与正则表达式匹配的字符串的普通状态机(X*)(Y)。

即使我已经标记了 algorithm fair，以下时间条件由于口吃而失败......模型检查器允许状态机吸收 anX然后简单地停止Loop而不再做任何其他事情的情况。

在这样一个简单过程的背景下，公平实际上意味着什么？有没有办法告诉模型检查器状态机永远不会用完输入，因此总是会终止？

给定集合，例如 {1, 2, 4, 10, 6} 我怎样才能将元素 4 获取到变量 var。我想要的是从集合中获取元素“4”到变量 var: var = 4 并从集合中删除元素 4：set = {1, 2, 10, 6}

我想写一个这样的（a）公式：

但每次我尝试运行模型时，我都会收到错误消息，«在评估中，标识符 x 要么未定义，要么不是运算符。»

到底是怎么回事？这样的公式真的不能写吗？为什么？我该如何解决这个问题？

谢谢。