24小时热门版块排行榜    

Znn3bq.jpeg
查看: 355  |  回复: 3
当前主题已经存档。
当前只显示满足指定条件的回帖,点击这里查看本话题的所有回帖

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);
}
回复此楼

» 猜你喜欢

已阅   回复此楼   关注TA 给TA发消息 送TA红花 TA的回帖

tzcreative

新虫 (初入文坛)

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

tzcreative

新虫 (初入文坛)

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

gjliu

银虫 (小有名气)

欢迎高手跟帖,帮助解决问题有奖。
4楼2009-05-13 13:12:34
已阅   回复此楼   关注TA 给TA发消息 送TA红花 TA的回帖
普通表情 高级回复 (可上传附件)
最具人气热帖推荐 [查看全部] 作者 回/看 最后发表
[考研] 一志愿085802 323分求调剂 +9 drizzle_9 2026-04-12 10/500 2026-04-12 14:51 by drizzle_9
[考研] 一志愿华中农微生物,288分,三年实验经历 +11 代fish 2026-04-09 11/550 2026-04-12 10:21 by Hayaay
[考研] 化学工程调剂289 +44 yang婷 2026-04-07 50/2500 2026-04-12 02:36 by 秋豆菜芽
[硕博家园] 有没有学校材料专业收跨调(一志愿085410) +6 momo(上岸版) 2026-04-06 9/450 2026-04-11 22:38 by wj165256
[教师之家] 请问地理、遥感方面,可以做哪些横向项目啊,纵向完不成考核啊 +3 锦衣卫寒战 2026-04-07 5/250 2026-04-11 20:51 by 豫椒
[考研] 调剂求助 +6 果然有我 2026-04-11 7/350 2026-04-11 16:22 by 明月此时有
[考研] 22408 352分求调剂 +4 努力的夏末 2026-04-09 4/200 2026-04-11 10:42 by maddjdld
[考研] 283求调剂,工科! +12 苏打水7777 2026-04-08 12/600 2026-04-11 10:28 by 逆水乘风
[考研] 281求调剂 +11 觉得好的吧 2026-04-10 11/550 2026-04-11 09:35 by 逆水乘风
[考研] 本科211 工科085400 280分求调剂 可跨专业 +11 LZH(等待调剂中 2026-04-10 11/550 2026-04-11 08:39 by zhq0425
[考研] 302分求调剂 +9 凡语祈愿 2026-04-08 10/500 2026-04-10 23:26 by 314126402
[考研] 0858求调剂 5+5 Gky09300550, 2026-04-10 8/400 2026-04-10 19:13 by chemisry
[考研] 362求调剂 +10 我要考大 2026-04-06 14/700 2026-04-10 17:00 by luoyongfeng
[考研] 071000生物学调剂求助 +17 zzzzwww 2026-04-09 20/1000 2026-04-10 15:55 by 求调剂zz
[考研] 材料调剂 +5 hzhahg 2026-04-06 5/250 2026-04-10 10:10 by may_新宇
[考研] 一志愿哈工大,初试329,求环境科学与工程调剂! +11 余未辛 2026-04-06 11/550 2026-04-08 15:21 by screening
[考研] 338求调剂 +8 wxygxsaaaaa 2026-04-06 8/400 2026-04-08 06:58 by 无际的草原
[考研] 信工所11408 340分 本科西安交大自动化 +3 moontrek 2026-04-06 3/150 2026-04-07 09:56 by chongya
[考研] 081200-11408-367学硕求调剂 +4 1_2_3111 2026-04-06 4/200 2026-04-07 08:13 by jp9609
[考研] 308求调剂 +3 终不似从前 2026-04-05 3/150 2026-04-05 22:23 by hemengdong
信息提示
请填处理意见