UPPAAL例子-维京人过河

介绍
全局变量
全局声明
模板-solidier
- 声明
- 状态转化图
模板-Torch
- 声明
- 状态转化图
性质验证

uppaal

介绍

Four vikings are about to cross a damaged bridge in the middle of the
night. The bridge can only carry two of the vikings at the time and to
find the way over the bridge the vikings need to bring a torch. The
vikings need 5, 10, 20 and 25 minutes (one-way) respectively to cross
the bridge.
Does a schedule exist which gets all four vikings over the bridge
within 60 minutes?
*/

四名维京人将要穿过一座受损的桥夜晚。这座桥当时只能载两个维京人去
在桥上找到维京人需要带火炬的路。这个维京人需要5分钟、10分钟、20分钟和25分钟（单程）才能穿越这座桥。
有没有把四个维京人都送到桥上的时间表？
60分钟内？

全局变量

chan take, release;      // Take and release chan通道的意思
int[0,1] L;     // The side the torch is on
clock time;     // Global time

全局声明

const int fastest = 5;
const int fast    = 10;
const int slow    = 20;
const int slowest = 25;Viking1 = Soldier(fastest);
Viking2 = Soldier(fast);
Viking3 = Soldier(slow);
Viking4 = Soldier(slowest);system Viking1, Viking2, Viking3, Viking4, Torch;

模板-solidier

声明

clock y;

状态转化图

开始维京人未过河，处于不安全状态

如果可以拿起火把且L ==0，此时y初始化，进入下一个状态，此时y一直增加

当y = _delay这个临界点时候，维京人已经到达，处于安全状态，释放火把，此时火把状态为1

维京人此刻在对岸

火把可以被拿地且L ==1，此时此时说明要回去。过程类似。

模板-Torch

声明

无

状态转化图

火把初始状态为free
接受到take时候，进入紧急状态，要么马上走人（一个人），要不然可以马上接受到第二个take信号走人（两个人，最多情况下）。
double_men走完之后，只能得realse。一次realse操作变成一个人，接着再realse一次，到达free状态，且更新L

个人理解：这部分只是考虑火把状态，不考虑从一个状态迁移到另一个状态考虑，人经历了什么。人和火把的状态通过通道保持同步。不可否认，形式化验证本身同样是可能存在问题的

性质验证

E<> Solidier1.safe and Solidier2.safe and Solidier3.safe and Solidier4.safe and time<=60

UPPAAL例子-维京人过河相关推荐

【游戏建模】Zbrush建模详细教程——维京人
今天跟大家分享一篇ZBrush雕刻维京人角色模型图文教程,感兴趣的朋友可以看下! 在这个维京人的作品中,我将向你展示我是如何使用zbrush制作"FlokiVikingsFanArt&quo ...
《NFL橄榄球》：明尼苏达维京人·橄榄1号位
明尼苏达维京人(英语:Minnesota Vikings)是一支职业美式足球球队,位于明尼苏达州的明尼阿波利斯.他们现时在国家橄榄球联合会北区参与国家美式足球联盟比赛.该球队本为美国美式足球联盟(AF ...
【Zbrush教程】怎样用ZBrush去雕刻制作一个维京人，详细讲解教程
第1步:概念在我们开始用ZBrush建模作品之前,你首先要知道,选择一个能提升我们技能的新项目非常重要:比如建模.拓扑结构.纹理等等.在这个项目中,因为我想熟悉衣服和配饰的制作过程,所以我选择了一个 ...
维京人的秘密：残暴背后的真相，敬畏神灵死后进入英灵殿
维京人,一个充满神秘色彩的名字,勾起了人们对于古代北欧残暴战士的想象.然而,维京人究竟是如何形成这样的形象,他们的传统和习俗又是如何塑造了他们的一生呢? 首先,我们要了解维京人的生活背景.维京人生活在 ...
维京猎人博客_7款维京游戏将您等到刺客信条瓦尔哈拉
维京猎人博客 Ah, Vikings. The mention of the word probably generates a similar image for most people: big ...
金沙艺廊于澳门四季名荟正式开幕；招商维京游轮深耕“文游”助力中国旅游业高质量发展 | 全球旅报...
Nikolaos Lekkas被任命为深圳柏悦酒店行政总厨.Nikolaos Lekkas于2022年1月被任命为深圳柏悦酒店行政总厨.来自希腊的Nikolaos先生是一位有着丰富管理经验的烹饪专家, ...
3D建模教程，使用ZBrush和MAYA制作超酷维京猫
在本教程中,Carlos Gonzalez Villagomez将向您展示如何创建一只维京海盗猫,还包括猫的造型,纹理,修饰,渲染和合成.因为他真的很喜欢<疯狂动物城>和<功夫熊猫& ...
八人过河思考策略_在思考云时平衡策略与战略
八人过河思考策略这一直是一个问题-那些将IT体系结构视为可以为单个应用程序或小型系统域提供服务的事物. 如今,许多组织无法选择一种云技术来为整个企业IT服务. 他们处理一系列具有一次性云架构的战术应 ...
精华帖——八人过河的程序实现
题目: 一家六口,一个爸爸,一个妈妈,俩儿子,俩女儿,还有一个警察,一个坏蛋,过一条河. 爸爸不在妈妈伤害儿子,妈妈不在爸爸伤害女儿,警察不在坏蛋伤害一家六口. 只有妈妈爸爸警察会开船,一次只能过两个 ...

UPPAAL例子-维京人过河

UPPAAL例子-维京人过河

介绍

全局变量

全局声明

模板-solidier

声明

状态转化图

模板-Torch

声明

状态转化图

性质验证

UPPAAL例子-维京人过河相关推荐

最新文章

热门文章