24小时热门版块排行榜    

Znn3bq.jpeg
查看: 353  |  回复: 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 的主题更新
普通表情 高级回复 (可上传附件)
最具人气热帖推荐 [查看全部] 作者 回/看 最后发表
[考研] 344 材料专业 求调剂211 无地域要求 +6 hualkop 2026-04-11 6/300 2026-04-12 15:00 by seattle40
[考研] 0831一轮调剂失败求助 +9 小熊睿睿_s 2026-04-11 9/450 2026-04-12 14:18 by 昆工高欣
[考研] 本科南方医科大学 一志愿985 药学学硕284分 求调剂 +5 弱水听文 2026-04-09 5/250 2026-04-12 13:16 by shengxi123
[考研] 211本科材料化工求调剂 +15 YHLAH 2026-04-11 16/800 2026-04-12 12:44 by BruceLiu320
[考研] 化学工程调剂289 +44 yang婷 2026-04-07 50/2500 2026-04-12 02:36 by 秋豆菜芽
[考研] 计算机22408 281分,求调剂 +7 17715607211 2026-04-06 7/350 2026-04-12 00:43 by xuxiang
[考研] 求调剂 +6 小聂爱学习 2026-04-11 9/450 2026-04-11 21:20 by 蓝云思雨
[考研] 电子信息279求调剂,有书读就行 +8 wwwooden 2026-04-08 11/550 2026-04-11 20:22 by cq2548
[考研] 295求调剂 +6 ?要上岸? 2026-04-05 7/350 2026-04-11 19:02 by laoshidan
[考研] 346,工科求调剂 +3 moser233 2026-04-09 3/150 2026-04-11 10:04 by zhq0425
[考研] 368求调剂 +3 17385968172 2026-04-10 3/150 2026-04-10 20:12 by 电子奥德彪
[考研] 284求调剂 +9 让我上岸吧阿西 2026-04-09 11/550 2026-04-10 19:18 by 靖jing
[考研] 机械专368 有去处吗 +4 种大树 2026-04-10 4/200 2026-04-10 15:31 by jiajinhpu
[考研] 285求调剂 +9 AZMK 2026-04-07 11/550 2026-04-10 15:24 by AZMK
[考研] 求调剂 +11 翩翩一书生 2026-04-09 13/650 2026-04-10 10:27 by liuhuiying09
[考研] 070300化学 求调剂 +13 73372112 2026-04-08 13/650 2026-04-09 20:22 by maddjdld
[考研] 283电子信息求调剂 +4 三石WL 2026-04-08 4/200 2026-04-09 10:21 by wp06
[考研] 一志愿985初试354分生物调剂 +3 031001 2026-04-06 3/150 2026-04-09 00:30 by Evan_Liu
[考研] 一志愿南昌大学,085600,344分求调剂 +11 调剂上岸玘 2026-04-05 12/600 2026-04-08 16:17 by luoyongfeng
[考研] 专硕085403,291分,有两篇专利,一国一奖 +3 哈吉咪哈吉咪 2026-04-07 3/150 2026-04-07 18:21 by 蓝云思雨
信息提示
请填处理意见