24小时热门版块排行榜    

查看: 331  |  回复: 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的回帖
普通表情 高级回复 (可上传附件)
最具人气热帖推荐 [查看全部] 作者 回/看 最后发表
[考研] 0856材料求调剂 +10 hyf hyf hyf 2026-02-28 11/550 2026-02-28 18:50 by 无际的草原
[考研] 298求调剂 +6 人间唯你是清欢 2026-02-28 7/350 2026-02-28 18:48 by 无际的草原
[考研] 311求调剂 +7 南迦720 2026-02-28 7/350 2026-02-28 18:28 by leonnulll
[基金申请] 面上模板改不了页边距吧? +3 ieewxg 2026-02-25 3/150 2026-02-28 18:25 by addressing
[教师之家] 版面费该交吗 +15 苹果在哪里 2026-02-22 18/900 2026-02-28 18:20 by mibaomingg
[考研] 285求调剂 +5 满头大汗的学生 2026-02-28 5/250 2026-02-28 18:10 by 材料专硕调剂;
[考研] 276求调剂 +3 路lyh123 2026-02-28 3/150 2026-02-28 18:02 by houyaoxu
[考研] 求调剂 +3 repeatt?t 2026-02-28 3/150 2026-02-28 18:00 by houyaoxu
[考研] 化工专硕348,一志愿985求调剂 +3 弗格个 2026-02-28 5/250 2026-02-28 17:04 by sandychj
[考博] 博士自荐 +3 kkluvs 2026-02-28 3/150 2026-02-28 16:59 by StarAura
[高分子] 求环氧树脂研发1名 +3 孙xc 2026-02-25 11/550 2026-02-28 16:57 by ichall
[考博] 博士推荐 +4 花儿笑? 2026-02-21 5/250 2026-02-28 16:55 by mumin1990
[考研] 265分求调剂不调专业和学校有行学上就 +4 礼堂丁真258 2026-02-28 6/300 2026-02-28 16:18 by 求调剂zz
[考博] 26申博 +3 想申博! 2026-02-26 3/150 2026-02-28 16:07 by nxgogo
[考研] 295求调剂 +4 19171856320 2026-02-28 4/200 2026-02-28 13:39 by ms629
[考研] 290求调剂 +4 材料专硕调剂; 2026-02-28 5/250 2026-02-28 13:32 by houyaoxu
[考研] 0856调剂 +3 刘梦微 2026-02-28 3/150 2026-02-28 13:22 by houyaoxu
[考研] 304求调剂 +5 曼殊2266 2026-02-28 6/300 2026-02-28 12:44 by 迷糊CCPs
[基金申请] 什么是人一生最重要的? +10 瞬息宇宙 2026-02-21 10/500 2026-02-27 08:46 by tfang
[硕博家园] 【博士招生】太原理工大学2026化工博士 +4 N1ce_try 2026-02-24 8/400 2026-02-26 08:40 by N1ce_try
信息提示
请填处理意见