- html - 出于某种原因,IE8 对我的 Sass 文件中继承的 html5 CSS 不友好?
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景?
程序可以从 START 分支到 LEFT 或 RIGHT 分支。如何检查 LEFT 分支的执行路径和 RIGHT 分支的另一个执行路径?
------------------------------ MODULE WFBranch ------------------------------
VARIABLE state
START == "start"
LEFT == "left"
RIGHT == "right"
Init == state = START
Next ==
\/ /\ state = START
/\ \/ state' = LEFT
\/ state' = RIGHT
\/ /\ state \in {LEFT, RIGHT}
/\ state' = START
Spec ==
/\ Init
/\ [][Next]_<<state>>
/\ WF_<<state>>(Next) \* Avoid stuttering at start
(*
This passes, but it does not ensure that there exist different paths covering both
branches - e.g. state might never be LEFT.
*)
CheckEventualStates == \/ (state = START) ~> (state = RIGHT)
\/ (state = START) ~> (state = LEFT)
=============================================================================
最佳答案
在完全一般的情况下,没有办法检查每个状态,至少有一个行为最终达到它。这是因为 TLA+ 基于 线性时序逻辑 ,它没有表达在多种不同行为之间存在的属性的方法。
根据具体情况,有时您可以制作替代品。例如,我们可以写
Left ==
/\ state = START
/\ state' = LEFT
Right ==
/\ state = START
/\ state' = RIGHT
Next ==
\/ /\ state = START
/\ \/ Left
\/ Right
\/ /\ state \in {LEFT, RIGHT}
/\ state' = START
CheckEventualStates ==
/\ <>(ENABLED Left)
/\ <>(ENABLED Right)
关于formal-verification - 检查分支是否被执行,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/47743891/
我正在构建一个带有登录和注册系统的网站,用户的信息将存储在数据库中。我在创建帐户后实现标准电子邮件验证步骤。该过程如下:创建一个帐户,但将“已验证”标志设置为 False。然后,系统会向用户发送一封电
给定一个系统及其完整的状态空间,我可以说该状态空间是该系统行为的正式规范吗? 最佳答案 除非您正式定义了进出每个状态的所有可能转换,并且您的状态空间包含系统可能处于的所有可能状态。 在计算机系统的正式
有哪些代码示例可以证明KeY的优势? 细节 有了这么多的正式方法工具,我想知道KeY在哪些方面比其竞争对手更好,以及如何?一些可读的代码示例对于比较和理解非常有帮助。 更新 搜索the KeY web
我一直在写类似于 Stream 的东西。我能够证明每个仿函数定律,但我无法想出一种方法来证明它是完整的: module Stream import Classes.Verified %default
传统上,大多数使用计算逻辑的工作要么是命题式的(在这种情况下,您使用SAT( bool(boolean) 可满足性)求解器),要么是一阶的(在这种情况下,您使用一阶定理证明器)。 近年来,在SMT(可
我目前正在注册 MapR Academy 的免费在线学习计划 ADM200。我正在使用 2015 年 11 月 25 日修订的“设置虚拟集群”说明。我正在使用 Windows 8.1 计算机,并尝试在
在下面的程序中,循环的最后一个不变量验证失败。但是如果我把它作为断言放在 while 循环之前,条件就会验证。如果我添加字段 ia 没有改变,它也会验证。为什么需要这个?读取权限不应该暗示这一点吗?我
程序可以从 START 分支到 LEFT 或 RIGHT 分支。如何检查 LEFT 分支的执行路径和 RIGHT 分支的另一个执行路径? ------------------------------
我正在尝试使用 Dafny 证明以下程序的正确性/不正确性。 datatype List = Nil | Cons(T, List) function tail(l:List):List {
我对交易收据验证有一些疑问: 为什么需要外部服务器?为什么我不能直接联系 http://buy.itunes.apple.com直接从 iPhone 上? 如果此外部服务器出现故障或收据无效怎么办?如
我有一些类似于以下的伪代码: for (lets say 10 iterations) begin // Do some configuration changes fork
我已在设备设置中从商店注销。我仅在我的应用程序中输入了用户凭据。我已经设置了一个全新的(实际上大约 4 次)测试用户。 为什么这条消息不断弹出? 它是否连接到 iOS 5、自动应用程序同步或 iClo
我想向用户展示他们刚刚在点击“提交”进行验证后弹出的模式中填写的表单。我将其视为表格的副本,但每个字段均被禁用或变灰,以便他们可以查看并确认一切正确。要在此阶段对表单进行更改,需要从模式中取消并返回到
当我模拟Endian Swapper时,我得到了不同的时钟周期。使用 QuestaSim 在 VHDL 和 Verilog 模式下的 Cocotb 示例。 provided example code
我正在计划使用现成的 SMT 求解器对 C 代码的符号执行进行一些实验,并且想知道使用哪个求解器;看着例如SMT 竞赛参赛者只选择开源系统,将范围缩小到 Beaver、Boolector、CVC3、O
我在达夫尼(Dafny)得到警告,说我的量词有 No terms found to trigger on. 我要为代码执行的操作是找到平方值小于或等于给定自然数'n'的最大数字。这是到目前为止我想出的
我已在设备设置中退出商店。我只在我的应用程序中输入了用户凭据。我设置了一个全新的(实际上大约 4 次)测试用户。 为什么这条消息不断弹出? 它是否连接到 iOS 5、自动应用同步或 iCloud? 最
将未经验证的用户放入 users_table 是一个不错的选择,还是我应该创建一个 temp_users_table 来添加未经验证的用户? 第一个选项是在 users_table 上创建包含一列的行
我已经尝试了几天来解决这个问题,使用SDK附带的Dungeons演示代码。我已经尝试谷歌寻找答案,但找不到答案。 在地下城演示中,我从开发控制台传递了我的公钥。 签署apk并上传到控制台而不发布。 测
我必须在 fabric 上安装一个 bna 文件。我正在关注链接 https://hyperledger.github.io/composer/tutorials/deploy-to-fabric-s
我是一名优秀的程序员,十分优秀!