应《网络安全法》要求，自2017年10月1日起，未进行实名认证将不得使用互联网跟帖服务。为保障您的帐号能够正常使用，请尽快对帐号进行手机号验证，感谢您的理解与支持！

24小时热门版块排行榜    

小木虫论坛-学术科研互动平台 » 专业学科区 » 信息科学 » 控制工程 » 【求助】SMV--请求紧急帮助
41/1返回列表
查看: 324  |  回复: 3
只看楼主 @他人 存档 新回复提醒 (忽略) 收藏    在APP中查看
当前主题已经存档。

tzcreative

新虫 (初入文坛)

[交流] 【求助】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);
}
回复此楼

» 猜你喜欢
1楼 2009-05-12 20:51:47
已阅   回复此楼   关注TA 给TA发消息 送TA红花 TA的回帖

tzcreative

新虫 (初入文坛)
这个只是整个模型的一部分，但是Candence SMV提示语法错误，好像在两个不同的模块里也不能对同一个变量赋值。我在t12()这个模块中去掉对t12.marked和t12.data的赋值就没有问题。但是这样无法实现我的模型检测。
赞一下 回复此楼
2楼2009-05-12 21:15:39
已阅   回复此楼   关注TA 给TA发消息 送TA红花 TA的回帖

tzcreative

新虫 (初入文坛)
这个只是整个模型的一部分，接下去是对p13的继续操作，但是Candence SMV提示语法错误，好像在两个不同的模块里也不能对同一个变量赋值。我在t12()这个模块中去掉对p12.marked和p12.data的赋值就没有问题。但是这样无法实现我的模型检测。
赞一下 回复此楼
3楼2009-05-12 21:17:30
已阅   回复此楼   关注TA 给TA发消息 送TA红花 TA的回帖

gjliu

银虫 (小有名气)
欢迎高手跟帖，帮助解决问题有奖。
赞一下 回复此楼
4楼2009-05-13 13:12:34
已阅   回复此楼   关注TA 给TA发消息 送TA红花 TA的回帖
相关版块跳转 我要订阅楼主 tzcreative 的主题更新
41/1返回列表
普通表情 龙 兔 虎 猫 高级回复 (可上传附件)
最具人气热帖推荐 [查看全部] 作者 回/看 最后发表
[公派出国] 售SCI一区文章，我:8 O5 51O 54,科目齐全 +3 5lbyq5wrhb 2026-02-07 4/200 2026-02-08 08:47 by vs90ilomwc
[考博] 售SCI一区文章，我:8 O5 51O 54,科目齐全 +3 5lbyq5wrhb 2026-02-07 4/200 2026-02-08 08:46 by vs90ilomwc
[硕博家园] 售SCI一区文章，我:8 O5 51O 54,科目齐全 +3 3rkserf6qr 2026-02-07 4/200 2026-02-08 08:27 by vs90ilomwc
[硕博家园] 售SCI一区文章，我:8 O5 51O 54,科目齐全 +5 2h7du0nuhk 2026-02-07 6/300 2026-02-08 08:26 by vs90ilomwc
[考博] 售SCI一区文章，我:8 O5 51O 54,科目齐全 +5 2h7du0nuhk 2026-02-07 6/300 2026-02-08 08:12 by vs90ilomwc
[硕博家园] 售SCI一区文章，我:8 O5 51O 54,科目齐全 +4 2h7du0nuhk 2026-02-07 6/300 2026-02-08 08:07 by vs90ilomwc
[考博] 售SCI一区文章，我:8 O5 51O 54,科目齐全 +4 2h7du0nuhk 2026-02-07 7/350 2026-02-08 08:06 by vs90ilomwc
[教师之家] 售SCI一区文章，我:8 O5 51O 54,科目齐全 +4 2h7du0nuhk 2026-02-07 7/350 2026-02-08 07:52 by vs90ilomwc
[找工作] 售SCI一区文章，我:8 O5 51O 54,科目齐全 +4 2h7du0nuhk 2026-02-07 7/350 2026-02-08 07:46 by vs90ilomwc
[公派出国] 售SCI一区文章，我:8 O5 51O 54,科目齐全 +4 2h7du0nuhk 2026-02-07 8/400 2026-02-08 07:32 by vs90ilomwc
[考博] 售SCI一区文章，我:8 O5 51O 54,科目齐全 +4 2h7du0nuhk 2026-02-07 8/400 2026-02-08 07:27 by vs90ilomwc
[教师之家] 售SCI一区文章，我:8 O5 51O 54,科目齐全 +4 2h7du0nuhk 2026-02-07 8/400 2026-02-08 07:26 by vs90ilomwc
[硕博家园] 售SCI一区文章，我:8 O5 51O 54,科目齐全 +4 2h7du0nuhk 2026-02-07 8/400 2026-02-08 07:07 by vs90ilomwc
[硕博家园] 博士延得我，科研能力直往上蹿 +8 偏振片 2026-02-02 8/400 2026-02-08 06:52 by liyeqik
[有机交流] 酰胺脱乙酰基 10+5 chibby 2026-02-03 12/600 2026-02-07 19:29 by 江东闲人
[基金申请] 同年申请2项不同项目，第1个项目里不写第2个项目的信息，可以吗 +4 hitsdu 2026-02-06 4/200 2026-02-07 13:07 by jurkat.1640
[基金申请] 有时候真觉得大城市人没有县城人甚至个体户幸福 +9 苏东坡二世 2026-02-04 10/500 2026-02-07 12:37 by 小毛球
[考博] 天津大学招2026.09的博士生，欢迎大家推荐交流（博导是本人） +4 a793625982 2026-02-05 5/250 2026-02-07 10:57 by a793625982
[基金申请] 面上项目申报 +3 Tide man 2026-02-01 3/150 2026-02-05 22:56 by god_tian
[教师之家] 遇见不省心的家人很难过 +18 otani 2026-02-03 22/1100 2026-02-04 11:06 by tangmnt
信息提示
关闭
请填处理意见
关闭