24小时热门版块排行榜    

Znn3bq.jpeg
查看: 352  |  回复: 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 的主题更新
普通表情 高级回复 (可上传附件)
最具人气热帖推荐 [查看全部] 作者 回/看 最后发表
[考研] 296求调剂 +14 汪!?! 2026-04-10 16/800 2026-04-12 10:48 by zhouyuwinner
[考研] 一志愿华中农微生物,288分,三年实验经历 +11 代fish 2026-04-09 11/550 2026-04-12 10:21 by Hayaay
[考研] 326求调剂 +6 Shansyn 2026-04-10 6/300 2026-04-12 09:46 by hammer3
[考研] 一志愿郑州大学 22408 305分求调剂 +5 安小满zzz 2026-04-08 5/250 2026-04-12 00:41 by 蓝云思雨
[考研] 0860004 求调剂 309分 +9 Yin DY 2026-04-08 9/450 2026-04-11 22:55 by dongdian1
[考研] 求调剂 +11 月@163.com 2026-04-07 13/650 2026-04-11 22:55 by BruceLiu320
[考研] 一志愿厦大0856,306求调剂 +15 Bblinging 2026-04-11 15/750 2026-04-11 22:53 by 314126402
[考研] 药学专硕调剂 +8 ? 一路生?花? 2026-04-10 10/500 2026-04-11 21:21 by zhouxiaoyu
[考研] 283求调剂,工科! +12 苏打水7777 2026-04-08 12/600 2026-04-11 10:28 by 逆水乘风
[考研] 考研调剂 +26 硕星赴 2026-04-09 27/1350 2026-04-10 22:24 by 猪会飞
[考研] 298求调剂 +13 钉叮咚冬瓜 2026-04-09 13/650 2026-04-10 15:49 by jiajinhpu
[考研] 347材料专硕求调剂 +19 zj8215216 2026-04-06 19/950 2026-04-10 09:36 by 690616278
[考研] 08600生物与医药-327 +10 18755400796 2026-04-05 10/500 2026-04-10 08:14 by kangsm
[考研] 083200 初试305分 求调剂 暂不考虑跨专业 +15 Claireyyyy 2026-04-09 15/750 2026-04-09 16:11 by zhuimr
[考研] 材料工程322 +18 哈哈哈吼吼吼哈 2026-04-07 19/950 2026-04-09 10:44 by cymywx
[考研] 机械专硕273请求调剂 +6 庚申壬申 2026-04-07 6/300 2026-04-08 22:41 by bljnqdcc
[考研] 生物学328分求调剂 +9 闪电kkl 2026-04-08 10/500 2026-04-08 21:42 by liuhuiying09
[考研] 一志愿吉大化学327求调剂 +12 王王白石 2026-04-06 13/650 2026-04-08 16:05 by luoyongfeng
[考研] 材料工程专业日语生求调剂 +9 111623 2026-04-07 9/450 2026-04-07 23:31 by 一只好果子?
[考研] 331求调剂 +5 张元一 2026-04-07 6/300 2026-04-07 22:13 by hemengdong
信息提示
请填处理意见