24小时热门版块排行榜    

查看: 336  |  回复: 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 的主题更新
普通表情 高级回复 (可上传附件)
最具人气热帖推荐 [查看全部] 作者 回/看 最后发表
[考研] 招08考数学 +4 laoshidan 2026-03-20 8/400 2026-03-22 19:56 by 小皮蛋酱
[考研] 289材料与化工(085600)B区求调剂 +3 这么名字咋样 2026-03-22 4/200 2026-03-22 17:56 by 云民大李老师
[考研] 306求调剂 +5 来好运来来来 2026-03-22 5/250 2026-03-22 16:17 by BruceLiu320
[考研] 260求调剂 +3 朱芷琳 2026-03-20 4/200 2026-03-22 15:12 by 朱芷琳
[考研] 269专硕求调剂 +6 金恩贝 2026-03-21 6/300 2026-03-22 14:31 by ColorlessPI
[考研] 318求调剂 +4 plum李子 2026-03-21 7/350 2026-03-22 14:17 by ColorlessPI
[考研] 初试 317 +7 半拉月丙 2026-03-20 7/350 2026-03-21 22:26 by peike
[考研] 材料求调剂 +5 @taotao 2026-03-21 5/250 2026-03-21 20:55 by lbsjt
[考研] 求调剂 +3 白QF 2026-03-21 3/150 2026-03-21 13:12 by zhukairuo
[考研] 机械专硕299求调剂至材料 +3 kkcoco25 2026-03-16 4/200 2026-03-21 03:52 by JourneyLucky
[考研] 070300化学319求调剂 +7 锦鲤0909 2026-03-17 7/350 2026-03-21 03:46 by JourneyLucky
[考研] 083200学硕321分一志愿暨南大学求调剂 +3 innocenceF 2026-03-17 3/150 2026-03-21 02:35 by JourneyLucky
[考研] 一志愿南昌大学,327分,材料与化工085600 +9 Ncdx123456 2026-03-19 9/450 2026-03-20 23:41 by lovewei0727
[考研] 330求调剂 +4 小材化本科 2026-03-18 4/200 2026-03-20 23:13 by JourneyLucky
[考研] 317求调剂 +5 申子申申 2026-03-19 9/450 2026-03-20 22:26 by JourneyLucky
[考研] 一志愿 南京航空航天大学大学 ,080500材料科学与工程学硕 +5 @taotao 2026-03-20 5/250 2026-03-20 20:16 by JourneyLucky
[考研] 【同济软件】软件(085405)考研求调剂 +3 2026eternal 2026-03-18 3/150 2026-03-18 19:09 by 搏击518
[考研] 085601求调剂 +4 Du.11 2026-03-16 4/200 2026-03-17 17:08 by ruiyingmiao
[考研] 考研调剂 +3 淇ya_~ 2026-03-17 5/250 2026-03-17 09:25 by Winj1e
[考研] 283求调剂 +3 听风就是雨; 2026-03-16 3/150 2026-03-17 07:41 by 热情沙漠
信息提示
请填处理意见