问题标签 [ctl]

我想知道下面的 CTL 公式是否等价，如果是，你能帮助我说服自己它们是等价的吗？A(p U ( A(q U r) )) = A(A(p U q) U r)

我想不出任何与之相矛盾的模型，我的直觉告诉我这些公式是等价的，但我找不到任何支持该陈述的等价物。我试图将等价性 A(p U q) == not(E ((not q) U not(p or q)) 或 EG (not q)) 改写成有用但多次失败的东西。

我浏览了我的课程资料以及谷歌，但我找不到任何东西。但是，我确实在这里找到了另一个具有相同等价问题但没有答案的问题，因此我正在尝试进行第二次尝试。

我想将 csv 文件导入到 oracle 数据库。我的 csv 看起来像这样：

表 A：有时包含 2 行或 3 行或为空。我想导入开始表 B。所以我的 control.ctl 是：

xyz 表是：

为什么没有存储数据？

我想导入 csv 文件。我的脚本是：

我的桌子是：

我的 control.ctl 是：

错误是：

请让我知道哪一个是错的。谢谢大家

我正在使用 kubernetes 进行容器编排，kubectl get rc在主节点上运行时我没有得到任何输出，而在使用他们的 REST API 时我得到一个复制控制器列表

我错过了什么

我用谷歌搜索了一段时间，发现一些论文提出了 CTL 或 CTL* 模型检查 SPIN。但是，根据 Promela 手册页，没有办法在 Promela 模型中表达 CTL。现在只是提案级别吗？

我是 NuSMV 的新手，并尝试为这个简单的回合制游戏建模。10块积木，每个玩家每回合可以拿1-3块积木，谁拿走最后一块积木获胜。假设玩家 A 先走，这是我的尝试。我想表达“最终会有赢家”，但我的代码不起作用，因为它不会阻止玩家在brick = 0之后拿砖，所以最终玩家a，b都会成为赢家。

这是我的代码：

这是我在 SPEC AF 上的输出（获胜者 = a | 获胜者 = 无）来说明我的观点。

如您所见，模型仍然提供了一个反例，其中玩家 b 在玩 a 已经获胜后赢得了游戏。

我的表数据包含从 sql loader ctl 文件加载的换行符，名为“IPADDRESS”的一列正在加载换行符：

我的 ctl 文件：

表存储中的数据为 Ex：

示例输入文件数据：

我收到此代码的编译时错误。不明白是什么意思，请帮忙。这是关于 codechef 的一些练习题。

试图在网上找到，但无法找到类似的答案。

代码是-

错误是-

我需要帮助编写这些 CTL。我还不太了解如何以 NuSMV 格式编写代码，希望我的代码对您有意义，因为它是不完整的 atm。

2）如果一个进程正在等待，它最终会到达它的临界区

3）两个进程必须“轮流”进入临界区

4）一个进程有可能连续两次进入临界区（在另一个进程之前）。

5) 进程 1 连续进入临界区将至少间隔 n 个周期，其中 n 是某个常数。你应该为n选择一个合适的值，并且这个值应该被验证（即，不被证明）。

6）您选择的更多非平凡属性

如果网站正在使用中央证书存储，有谁知道您是否可以将 CTL 绑定到网站？

通常我会使用 netsh http 命令绑定 CTL，但它似乎不接受 sslctlidentifier 开关