24小时热门版块排行榜    

Znn3bq.jpeg
汕头大学海洋科学接受调剂
查看: 358  |  回复: 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

新虫 (初入文坛)

这个只是整个模型的一部分,但是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 的主题更新
普通表情 高级回复 (可上传附件)
最具人气热帖推荐 [查看全部] 作者 回/看 最后发表
[考研] 22408 312求调剂 +15 门路摸摸 2026-04-14 16/800 2026-04-14 17:15 by zs92450
[考研] 一志愿鲁东大学071000生物学学硕初试分数276求调剂 +25 慕绝cc 2026-04-09 29/1450 2026-04-14 16:45 by zhouxiaoyu
[考研] 材料专业344求调剂 +17 hualkop 2026-04-10 22/1100 2026-04-14 16:21 by sxdj2
[考研] 药学305求调剂 +10 玛卡巴卡boom 2026-04-10 10/500 2026-04-14 15:55 by zs92450
[考研] 284求调剂 +17 让我上岸吧阿西 2026-04-09 17/850 2026-04-14 14:44 by 不我拉绿卡
[考研] 272分材料子求调剂 +41 Loy0361 2026-04-10 53/2650 2026-04-13 14:20 by 张zhihao
[考研] 材料考研调剂 +29 云木达达 2026-04-11 31/1550 2026-04-13 13:32 by lyh鲁老师
[考研] 280求调剂 +7 兮兮夜夜 2026-04-09 10/500 2026-04-12 00:33 by 蓝云思雨
[考研] 331求调剂 +5 王国帅 2026-04-11 5/250 2026-04-11 22:56 by 溪涧流水
[考研] 0860004 求调剂 309分 +9 Yin DY 2026-04-08 9/450 2026-04-11 22:55 by dongdian1
[考研] 085400 328分 求调剂 +10 喂你一个大橙子 2026-04-09 14/700 2026-04-11 19:53 by lqspecial
[考研] 22408 352分求调剂0854类 +4 努力的夏末 2026-04-09 4/200 2026-04-11 09:57 by zhq0425
[考研] 083200 305分 求二轮调剂 不接受跨专业 +9 Claireyyyy 2026-04-09 10/500 2026-04-10 21:21 by Claireyyyy
[考研] 289 分105500药学专硕求调剂(找B区学校) +6 白云123456789 2026-04-09 8/400 2026-04-10 21:13 by zhouxiaoyu
[论文投稿] mdpi小修rvr时间四五天了 20+3 哈哈high 2026-04-08 5/250 2026-04-10 16:02 by 北京莱茵润色
[考研] 085800 能源动力求调剂 +6 阿biu啊啊啊啊啊 2026-04-10 6/300 2026-04-10 15:03 by hemengdong
[考研] 一志愿中科大070300化学,314分求调剂 +12 wakeluofu 2026-04-09 12/600 2026-04-10 09:57 by liuhuiying09
[考博] 博士自荐 +7 可可小胖 2026-04-08 7/350 2026-04-10 08:28 by kimhero
[考研] 083200 初试305分 求调剂 暂不考虑跨专业 +15 Claireyyyy 2026-04-09 15/750 2026-04-09 16:11 by zhuimr
[考研] 软件工程求调剂22软工296分求调剂,接受跨调 +4 yangchen2017 2026-04-08 5/250 2026-04-08 21:56 by 土木硕士招生
信息提示
请填处理意见