初识形式化验证工具——CPN tools

安装链接:https://cpntools.org/category/downloads/

学习链接:https://cs.au.dk/cpnets/industrial-use

成功安装软件:

右键新建/打开项目:

导入项目:

交互工具:

仿真运行:也是拖拽出来后,要进行的操作在命名处左键即可。

换颜色应该是在style里面。

层次petri网的概念

1.目的

创建大型的、复杂的 Petri网是一个很麻烦的任务。但是类似于模块化编程思想,通过在CPNTools工具内利用替代变迁的概念可以将CPN网络结构拆分为多个小块。一般概念上,具有替代变迁的网络是有多个层次的网络一你可以先创建一个有点简化的网络,以此来从广义上定义你正在建模的系统的全貌;然后利用高层网中的替代变迁,将其关联到更为详细的页面中去,从而你可以逐步地、越来越细化你的模型。

2.替代变迁

用变迁表征网结构中的某一整块是层次网中常用的一种方法,利用这种方法使得包含上述变迁网络从逻辑上得到简化。这样一种变迁就叫做替代变迁。

替代变迁根本上没有增加任何新的东西。利用替代变迁可以做的操作同样也可以利用融合库所fusion places 的方式来实现。但是类比于融合库所,替代变迁显得更方便、有用,它可以区分出建模上的可行性和整体不可行性上的不同。3.子页和父页

包含有替代变迁的页面叫做父页,上图中的Top页面就是一个父页。

当CPN 网使用替代变迁的时候,替代变迁所表达的逻辑必须得在某一位置得到实现。实现替代变迁逻辑的页面叫做子页,从逻辑的角度来看子页也可以被称呼为子网或者子模块。

下图中的Reverse页面就是一个子页,它与替代变迁Reverse关联。  每个替代变迁都是对应子页的父节点。层次网结构中子页和父页之间的关系,在索引区网的总视图 overview中得以显现。子页的名称通常位于父页的下面,而且子页的名称比父页的名称稍有缩进。如果在索引中没有看到子页,可以单击父页旁边的蓝色箭头来展开子页列表。

4.端口库所和槽库所

        父页和子页的关联是通过两个页面上有特殊目的的融合集 fusion sets 中的库所来实现的。这些特殊的融合集包含两种库所。其中子页中的库所叫做端口库所,而父页上的叫做槽库所。

 

 5.端口库所/槽库所的关联

        端口库所/槽库所的关联被用来定义子页是如何粘合到它的父节点中去的。每一个槽库所都必须关联一个对应子页的端口库所。而具有In标签的端口库所也必须得关联一个槽库所,而且这个槽库所还得是替代变迁的输入(不是输出)节点。类似地,有Out标签的端口库所也必须得关联一个槽库所,而且这个槽库所还得是替代变迁的输出(不是输入)节点;有I/O标签的端口库所所关联的槽库所则可以既是替代变迁的输入节点又可以是替代变迁的输出节点。

        注意:端口库所周围的弧与端口类型标签没有对应关系。例如:假定有一个具有 In标签的端口库所,可以有弧从子页中的变迁流向这个库所,也可以有弧从这个库所(作为输出节点)流向子页中的某个变迁。

 6.端口库所和槽库所的标识

        父页槽库所中具有的标识在子页对应端口库所中也同样应该具有,反之亦然。

例如:父页面Top中 Begin库所中的初始标识与子页面Reverse中 Begin库所的初始标识相同。

7.对子页面的多次使用

        替代变迁的最大作用在于子页面并不仅仅只是唯一一个替代变迁的值:子页面可以被重复使用,效果就如同于多个父页面上多个替代变迁的值。

        如果子页面表示超过一个替代变迁的值,那么这就叫做子页面的多重实例。类似地,也存在子页面上库所和变迁地多重实例的现象。每个子页面的实例都是完全独立的,与同一子页面的其他实例的标识无关。

CPN工具各功能

1.net

新建/关闭,鼠标拖住窗口下面边缘,可以改变形状大小

修改名称:

合并工具窗口,拖在一起就可以了。

保存:

2 create

利用磁性参考线,帮助对齐绘制:

红色×可以选中元素进行删除,删了没办法复原???没有Ctrl+Z,慎重!

3 style

改变颜色、粗细等样式,其他后面再学。

4 view

本文来自互联网用户投稿,该文观点仅代表作者本人,不代表本站立场。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如若转载,请注明出处:/a/724865.html

如若内容造成侵权/违法违规/事实不符,请联系我们进行投诉反馈qq邮箱809451989@qq.com,一经查实,立即删除!

相关文章

探索Web Components

title: 探索Web Components date: 2024/6/16 updated: 2024/6/16 author: cmdragon excerpt: 这篇文章介绍了Web Components技术,它允许开发者创建可复用、封装良好的自定义HTML元素,并直接在浏览器中运行,无需依赖外部库。通过组合HTML模…

CNAS软件测试报告全国通用吗?如何获取CNAS软件测试报告?

CNAS是中国合格评定国家认可委员会的英文缩写,是我国负责认可和监管合格评定机构的国家级组织。CNAS软件测试报告是经过CNAS认可的软件测试机构出具的报告,它详细记录了被测试软件的测试结果、缺陷情况以及整体质量评估。 企业和用户通过查看CNAS软件测…

多环境镜像晋级/复用最佳实践

作者:木烟 本文主要介绍镜像构建部署场景,多环境镜像晋级/复用最佳实践,保证“所发即所测”。 场景介绍 应用研发场景有效地管理镜像产物是确保软件快速、安全、可靠部署的关键环节。通常一个应用研发需要经过测试、预发、生产各个阶段&am…

地图上绘制地铁线路

需求背景 不管是之前的pms 地铁还是location都会有需求涉及到地图上绘制地铁线路,来查看当前位置是否靠近地铁口,常规的交互可以看下高德地图,如图所示: 需求分析 不管是高德地图还是百度地图都提供了简易版的地铁线路图&#x…

【AI】通义千问使用指南:让你快速上手,成为问题解决高手!

大家好,我是木头左。 近日,继文心一言和讯飞星火之后,阿里虽迟但到,直接宣布开源两款“通义千问”大模型。作为国内首个开源且可商用的人工智能大模型,这会给我们带来哪些变化呢? 如何申请阿里通义千问&am…

RK3568技术笔记十二 Android编译方法

Android源码说明 Android源码在SAIL-RK3568开发板光盘->Android->源代码中,由于android源码太大,在进行压缩时,进行分包压缩,因此有4部分,如图所示: 进行解压时,需将4部分压缩包放置同一…

Redis的安装及详解

1.Redis介绍? 1.1 Redis是什么? Redis(Remote Dictionary Server,远程字典服务器)是一个开源免费的,用C语言编写的一个高性能的分布式内存数据库,基于内存运行并支持持久化的NoSQL数据库。是当前最热门的…

若依RuoYi-Vue分离版—富文本Quill的图片支持伸缩大小及布局

若依RuoYi-Vue分离版—富文本Quill的图片支持伸缩大小及布局、工具栏带中文提示 1.在vue.config.js 文件中添加 一下内容2.下载安装插件3.在Editor组件中引入插件4.使用Editor组件(特别注意要的加 v-if )5.bug 之 imageResize的 img的style丢失1.先创建一…

山东大学软件学院创新项目实训开发日志——收尾篇

山东大学软件学院创新项目实训开发日志——收尾篇 项目名称:ModuFusion Visionary:实现跨模态文本与视觉的相关推荐 -------项目目标: 本项目旨在开发一款跨模态交互式应用,用户可以上传图片或视频,并使用文本、点、…

Canonical Juju 的一个奇怪编排部署

一周前的一个项目扩容出现了异常,进行了操作回滚,未对线上业务造成损失。 现象是这样的: 通过基于 Canonical Juju-GUI 在一组节点上部署了某个组件,在把这组节点添加到集群后,有4个节点上出现了同一组件的2个instanc…

WDF驱动开发-计时器

WDF可以使用框架的内置计时器支持。 它适用于 Kernel-Mode Driver Framework (KMDF) 驱动程序,以及从版本 2 开始的 User-Mode Driver Framework (UMDF) 驱动程序。 框架提供了一个 计时器对象 ,使驱动程序能够创建计时器。 在驱动程序创建计时器对象并…

Scala语言:大数据开发的未来之星 - 零基础到精通入门指南

前言 随着大数据时代的到来,数据量的急剧增长为软件开发带来了新的挑战和机遇。Scala语言因其函数式编程和面向对象的特性,以及与Apache Spark的完美协作,在大数据开发领域迅速崛起,成为该领域的新兴宠儿。本篇将从零基础开始&…

Vue59-全局事件总线:任意组件间通信

一、原理图 只是总结出的经验,不是新的API! 二、x的要求: 1、保证x被所有组件看见; 2、x可以调用的到$on,才能绑定事件,还能调用到:$of, $emit; 三、x的创建&#xff…

手把手教你创建并启动一个Vue3项目(Windows版)

一、Node安装 1、下载地址:Node.js — Run JavaScript Everywhere 2、安装Node,双击启动一直Next 3、验证安装Node是否成功,打开CMD命令窗口,输入node -v,显示版本就表示成功 4、验证安装npm是否成功,npm是…

sqlite3指令操作-linux

1.查看当前数据库位置 2.查看当前数据库文件下有哪些表 3.显示 某表创建时的SQL语句 4.打开、关闭显示列标题; 5.列对齐显示 6.列以‘,’分隔显示 .separator 7.查询表信息 8.插入消息 9.删除某一行内容 10.修改某行某列内容 11.修改表名字 alter tab…

开发者黑板报#65

第65期 AI 谷歌Gemini 终于,GPT-4独霸时代终结了! 过去一个月里,四款大模型横空出世,在各项关键基准测试中与GPT-4相匹敌,甚至更胜一筹。 谷歌Gemini 1.5突破100万个tokens,是GPT-4的近8倍&#xff0c…

办公楼导航系统:设计要点、功能实现与效益评估

随着现代办公楼的日益复杂化和规模化,如何高效、便捷地在楼宇内部进行定位和导航,已成为众多企业和员工关注的焦点。维小帮办公楼定位导航系统通过精准的定位和智能的导航功能,能够显著提升办公环境的智能化水平和办公效率。 一、维小帮办公…

嵌入式实验---实验一 通用GPIO实验

一、实验目的 1、掌握STM32F103 GPIO程序设计流程; 2、熟悉STM32固件库的基本使用。 二、实验原理 1、通过按键实现:按键按下,LED点亮;按键释放,LED熄灭。 三、实验设备和器材 电脑、Keil uVision5软件、Proteus…

Top10在线音频剪辑软件,你了解几款?(免费分享)

多年来,随着音乐制作人和音频工程师的需求不断增长,音频剪辑软件领域经历了巨大的发展。最新的音频剪辑软件提供了从基本录制到最终发布所需的一切功能。其中一些软件专为播客设计,一些软件是免费的,并且一些软件提供了出色的音效…

【Win】双系统新体验:Hyper-V上macOS安装攻略

在虚拟化的世界里,Hyper-V是探索不同操作系统的一扇大门。尽管macOS并不是Hyper-V官方支持的来宾操作系统,但这并未阻挡技术探索者的脚步。他们通过不懈努力,开辟出了一条条通往macOS的非官方路径。这些路径或许曲折,却为那些渴望…