formal-verification - Uppaal - 当条件变为真时如何强制转换?
问题描述
我希望能够在条件变为真后立即强制转换。
例如,在此示例中,我想在全局变量a变为5时强制从下一个系统从状态S0转换到S1。守卫是不够的,因为在触发转换之前 a 达到 5 后仍然可以递增。我真的需要触发过渡,然后继续增加a。
有没有简单的方法来做到这一点?我尝试在状态中添加不变量,但它会造成死锁。
解决方案
使用频道同步。几种方法:
在进程上声明
chan message;
并添加message!
同步increment
,添加进程转换,并使用另一个带有保护的转换来检查值并相应地移动到另一个位置。message?
next
a
在边缘声明
urgent broadcast chan ASAP;
和使用,这将使该转换一旦启用(即满足防护)就变得紧急。紧急转换仅支持整数守卫。ASAP!
next
推荐阅读
- python - 如何修复 OpenSSL.SSL.WantReadError?
- java - 方法代码覆盖率不包括在 Spring Reactor 中调用 flatMap() 的情况
- java - Java 运行时环境内存不足,无法继续进行 elasticsearch
- sql - Exist query Oracle join syntax vs ANSI JOIN syntax
- hibernate - 新的 Spring Boot 应用程序启动失败 Error Creating bean with name 'entityManagerFactory'
- python - 在无头健身房 jupyter Python 2.7 中获取“ AttributeError:'ImageData'对象没有属性'data'”
- ios - 如何创建支持手写文本和在同一页面上键入文本的绘图视图,类似于 IOS Notes App
- html - 滚动棒/跳转第二个中途网站
- react-native - google-play-service 更新后无法在 react-native 中构建 android 应用程序
- python - 如何根据 python 中的条件从现有列表创建自定义列表?