-- 发布时间：5/12/2009 7:18:00 PM
-- 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);
}
模型在附件中
此主题相关图片如下：