| 查看: 395 | 回复: 3 | |||
| 当前主题已经存档。 | |||
[交流]
【求助】SMV--请求紧急帮助
|
|||
|
我正在学习Candence-SMV,对一个简单的Petri网进行模拟验证，但是提示语法错误，不知道是什么原因，请各位高手指点。万分感谢！ typedef d_place struct { marked : boolean; data : 0..5; } --t11 MODULE t11(p11,p12){ --ASSIGN default{ next(p11.marked):=p11.marked; next(p11.data):=p11.data; next(p12.marked):=p12.marked; next(p12.data):=p12.data; } in case { p11.marked & !p12.marked & p11.data>0 : { next(p11.marked):=0; next(p12.marked):=1; next(p12.data):=p11.data; } } } --t12 MODULE t12(p12,p13){ --ASSIGN default { next(p12.data):=p12.data; next(p13.marked):=p13.marked; next(p13.data):=p13.data; } in case { p12.marked & !p13.marked & p12.data>0 : { next(p13.marked):=1; next(p13.data):=1; next(p12.data):=p12.data-1; } } next(p12.marked):=p12.marked; } MODULE main(){ p11,p12,p13 : d_place; init(p11.marked):=1; init(p11.data) := 5; init(p12.marked):=0; init(p13.marked):=0; pr_x1 : t11(p11,p12); pr_x2 : t12(p12,p13); SPEC AG((p11.marked & p11.data>0)-> AF p13.marked); } |
回复此楼» 猜你喜欢
售SCI一区文章，我:8.O.55.1.O.54,科目齐全,可伽急
已经有4人回复
-
售SCI一区文章，我:8.O.55.1.O.54,科目齐全,可伽急
已经有5人回复
-
售SCI文章，我:8O5.5.1.O.54,科目齐全,可+急
已经有3人回复
-
售SCI一区T0P文章，我:8O.55.1.O.54,科目全,可伽急
已经有3人回复
-
售SCI文章，我:8O5.5.1.O.54,科目齐全,可+急
已经有3人回复
-
售SCI一区T0P文章，我:8O.55.1.O.54,科目全,可伽急
已经有3人回复
-
售SCI一区文章，我:8.O.551.O.5.4,科目全,可伽急
已经有4人回复
-
售SCI-T0P文章，我:8O.5.5.1.O.54,科目齐全,可+急
已经有4人回复
-
售SCI一区T0P文章，我:8.O.55.1.O.54,科目齐全,可+急
已经有3人回复
-
售SCI一区T0P文章，我:8O.55.1.O.5.4,科目齐全,可+急
已经有6人回复
2楼2009-05-12 21:15:39
3楼2009-05-12 21:17:30
4楼2009-05-13 13:12:34
