新书推介：《语义网技术体系》
作者：瞿裕忠，胡伟，程龚
   XML论坛     W3CHINA.ORG讨论区     计算机科学论坛     SOAChina论坛     Blog     开放翻译计划     新浪微博  
 
  • 首页
  • 登录
  • 注册
  • 软件下载
  • 资料下载
  • 核心成员
  • 帮助
    		•   Add to Google

    >> It is the theory that decides what can be observed. - Albert Einstein
    [返回] 计算机科学论坛 → 计算机理论与工程 → 『 理论计算机科学 』 → SMV--请求紧急帮助 ◇查看新帖 ◇ 用户列表 ◇

      发表一个新主题  发表一个新投票  回复主题  (订阅本版) 您是本帖的第 4544 个阅读者浏览上一篇主题  刷新本主题   树形显示贴子　浏览下一篇主题
     * 贴子主题： SMV--请求紧急帮助 举报  打印  推荐  IE收藏夹 
       本主题类别:     
     javaejb 帅哥哟，离线，有人找我吗？
      
      
      等级：大一新生
      文章：3
      积分：64
      门派：XML.ORG.CN
      注册：2007/10/19

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给javaejb发送一个短消息 把javaejb加入好友 查看javaejb的个人资料 搜索javaejb在『 理论计算机科学 』的所有贴子 引用回复这个贴子 回复这个贴子 查看javaejb的博客楼主
    发贴心情 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);
    }
    模型在附件中

    此主题相关图片如下：
    按此在新窗口浏览图片


       收藏   分享  
    顶(0)
      




    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2009/5/12 19:18:00
     
     javaejb 帅哥哟，离线，有人找我吗？
      
      
      等级：大一新生
      文章：3
      积分：64
      门派：XML.ORG.CN
      注册：2007/10/19

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给javaejb发送一个短消息 把javaejb加入好友 查看javaejb的个人资料 搜索javaejb在『 理论计算机科学 』的所有贴子 引用回复这个贴子 回复这个贴子 查看javaejb的博客第2楼
    发贴心情 
    这个只是整个模型的一部分，接下去部分是继续对p13的操作，但是Candence SMV提示语法错误，好像在两个不同的模块里也不能对同一个变量赋值。我在t12()这个模块中去掉对p12.marked和p12.data的赋值就没有问题。但是这样无法实现我的模型检测。
    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2009/5/12 21:17:00
     
     GoogleAdSense
      
      
      等级：大一新生
      文章：1
      积分：50
      门派：无门无派
      院校：未填写
      注册：2007-01-01
    给Google AdSense发送一个短消息 把Google AdSense加入好友 查看Google AdSense的个人资料 搜索Google AdSense在『 理论计算机科学 』的所有贴子 访问Google AdSense的主页 引用回复这个贴子 回复这个贴子 查看Google AdSense的博客广告
    2024/5/11 11:28:15

    本主题贴数2，分页： [1]

    管理选项： 修改tag | 锁定 | 解锁 | 提升 | 删除 | 移动 | 固顶 | 总固顶 | 奖励 | 惩罚 | 发布公告
    W3C Contributing Supporter! W 3 C h i n a ( since 2003 ) 旗 下 站 点
    苏ICP备05006046号《全国人大常委会关于维护互联网安全的决定》《计算机信息网络国际联网安全保护管理办法》
    		 109.375ms