返回介绍

H.3.1 Rewrite rules for clocks

发布于 2020-09-09 22:56:16 字数 1206 浏览 960 评论 0 收藏 0

The semantics of clocked sequences and properties is defined in terms of the semantics of unclocked

sequences and properties. The following rewrite rules define the transformation of a clocked sequence or property

into an unclocked version that is equivalent for the purposes of defining the satisfaction relation. In this

transformation, it is required that the conditions in event controls not be dependent upon any local variables.

? @(c) b ( !c [*0:$] ##1 c & b ) .

? @(c)( 1, v = e ) ( @(c) 1 ##0 ( 1, v = e )) .

? @(c)( P ) ( @(c) P ).

? @(c)( R1 ##1 R2 ) ( @(c) R1 ##1 @(c) R2 ) .

? @(c)( R1 ##0 R2 ) ( @(c) R1 ##0 @(c) R2 ) .

? @(c)( R1 or R2 ) ( @(c) R1 or @(c) R2 ) .

? @(c)( R1 intersect R2 ) ( @(c) R1 intersect @(c) R2 ) .

? @(c) first_match ( R ) first_match ( @(c) R ) .

? @(c) R [*0] ( @(c) R )[*0] .

? @(c) R [*1:$] ( @(c) R )[*1:$] .

? @(c) disable iff ( b ) P disable iff ( b ) @(c) P .

? @(c) not P not @(c) P.

? @(c) ( R |-> P ) ( @(c) R |-> @(c) P ) .

? @(c) ( P1 or P2 ) ( @(c) P1 or @(c) P2 ).

? @(c) ( P1 and P2 ) ( @(c) P1 and @(c) P2 ).

如果你对这篇内容有疑问,欢迎到本站社区发帖提问 参与讨论,获取更多帮助,或者扫码二维码加入 Web 技术交流群。

扫码二维码加入Web技术交流群

发布评论

需要 登录 才能够评论, 你可以免费 注册 一个本站的账号。
列表为空,暂无数据
    我们使用 Cookies 和其他技术来定制您的体验包括您的登录状态等。通过阅读我们的 隐私政策 了解更多相关信息。 单击 接受 或继续使用网站,即表示您同意使用 Cookies 和您的相关数据。
    原文