UPPAAL死锁不清楚
UPPAAL deadlock unclear
我正在使用 UPPAAL，我正在尝试为鞋厂建模，其中 5 个系统 运行 并联。如果有人需要，我可以写得更详细，但我不想通过描述模型来浪费任何人的时间。
所以直奔问题：UPPAAL deadlock state
在link中的图片上，自动机无法进行红色转换。转换的唯一标准是 p >= 4，但正如我所标记的，这应该没问题，因为 p=21。
那么为什么它不能进行过渡呢？
您可以在下面 link 找到来源：
https://drive.google.com/open?id=1zuige_JBTPA7kZJPwE5cocWCzY6eh8UL
非常感谢任何帮助！
我特别感兴趣的是死锁的原因，以及为什么无法进行转换，即使我试图强制转换
(不好意思，我没有上传图片的水平:()
编辑1：
由于有些人声称代码不可访问，所以我将粘贴 UPPAAL 的 2 个文件，如下所示：
hf_elso_1.xml:
<?xml version="1.0" encoding="utf-8"?><!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_1.dtd'><nta><declaration>// Place global declarations here.
chan ontoindul, talpontkesz, talpakkeszen, felsoreszkesz;
clock t1,t2,t3,globalClock;
int p, to, talp, fr,cipo;</declaration><template><name x="5" y="5">talponto</name><declaration>// Place local declarations here.
</declaration><location id="id0" x="-24" y="-216"></location><location id="id1" x="-464" y="240"><committed/></location><location id="id2" x="-464" y="-24"><label kind="invariant" x="-536" y="-48">t1<=500</label></location><location id="id3" x="-24" y="-80"><committed/></location><location id="id4" x="-24" y="-152"><label kind="invariant" x="0" y="-160">t1<=800</label></location><location id="id5" x="-24" y="64"><label kind="invariant" x="-32" y="80">t1<1</label></location><location id="id6" x="-24" y="-288"><name x="-34" y="-318">start</name></location><init ref="id6"/><transition><source ref="id0"/><target ref="id4"/><label kind="synchronisation" x="-96" y="-192">ontoindul!</label></transition><transition><source ref="id6"/><target ref="id0"/><label kind="assignment" x="-80" y="-264">p:=40</label></transition><transition><source ref="id2"/><target ref="id1"/><label kind="assignment" x="-528" y="112">p=p-4</label></transition><transition><source ref="id1"/><target ref="id5"/><label kind="assignment" x="-384" y="216">to:=to+1</label></transition><transition><source ref="id5"/><target ref="id2"/><label kind="guard" x="-352" y="-48">p>=4</label><label kind="synchronisation" x="-352" y="-32">ontoindul!</label><label kind="assignment" x="-352" y="-16">t1:=0</label></transition><transition><source ref="id3"/><target ref="id5"/><label kind="assignment" x="-124" y="-40">to:=to+1,p:=p-4</label><nail x="-24" y="8"/><nail x="-24" y="16"/></transition><transition><source ref="id4"/><target ref="id3"/><label kind="assignment" x="-96" y="-120">t1:=0</label></transition></template><template><name>talpkeszito</name><location id="id7" x="88" y="120"><committed/></location><location id="id8" x="-208" y="120"><label kind="invariant" x="-256" y="136">t1<=100</label></location><location id="id9" x="-72" y="-80"></location><init ref="id9"/><transition><source ref="id7"/><target ref="id9"/><label kind="assignment" x="-52" y="20">to=to-3</label></transition><transition><source ref="id8"/><target ref="id7"/><label kind="assignment" x="-120" y="144">talp=talp+5</label></transition><transition><source ref="id9"/><target ref="id8"/><label kind="guard" x="-200" y="-10">to>2</label><label kind="synchronisation" x="-200" y="5">ontoindul?</label></transition></template><template><name>felsvag</name><location id="id10" x="112" y="-168"><label kind="invariant" x="102" y="-153">t1<=200</label></location><location id="id11" x="368" y="-176"><label kind="invariant" x="352" y="-224">t1<=100</label></location><location id="id12" x="-80" y="16"></location><location id="id13" x="-80" y="-168"></location><init ref="id13"/><transition><source ref="id10"/><target ref="id12"/><label kind="guard" x="-40" y="-144">p>0</label><label kind="assignment" x="-40" y="-128">p=p-1, fr=fr+5</label></transition><transition><source ref="id11"/><target ref="id10"/><label kind="guard" x="200" y="-208">p>0</label><label kind="assignment" x="180" y="-172">p=p-1, fr=fr+5</label></transition><transition><source ref="id12"/><target ref="id11"/><label kind="guard" x="224" y="96">fr<20</label><label kind="synchronisation" x="216" y="112">ontoindul?</label><nail x="196" y="110"/></transition><transition><source ref="id13"/><target ref="id12"/><label kind="guard" x="-152" y="-144">p>0</label><label kind="synchronisation" x="-152" y="-128">ontoindul?</label><label kind="assignment" x="-152" y="-112">p=p-1</label></transition></template><template><name>Varras</name><declaration>int osszcipo;</declaration><location id="id14" x="232" y="-216"><label kind="invariant" x="232" y="-192">t2<=10</label></location><location id="id15" x="-24" y="-208"></location><init ref="id15"/><transition><source ref="id14"/><target ref="id15"/><nail x="104" y="-328"/></transition><transition><source ref="id15"/><target ref="id14"/><label kind="guard" x="40" y="-88">talp>0 and fr>1</label><label kind="assignment" x="40" y="-72">cipo=cipo+1, talp=talp-1, fr=fr-2, t2=0,osszcipo=osszcipo+1</label><nail x="104" y="-104"/></transition></template><template><name>Kereskedo</name><location id="id16" x="16" y="-104"><label kind="invariant" x="32" y="-96">t3<=100</label></location><location id="id17" x="-184" y="-104"></location><init ref="id17"/><transition><source ref="id16"/><target ref="id17"/><nail x="-80" y="-200"/></transition><transition><source ref="id17"/><target ref="id16"/><label kind="guard" x="-48" y="16">cipo>2</label><label kind="assignment" x="-80" y="48">cipo=cipo-2,p=p+4,t3=0</label><nail x="-88" y="16"/></transition></template><system>// Place template instantiations here.
To = talponto();
Tk = talpkeszito();
Fv = felsvag();
V = Varras();
K = Kereskedo();
// List one or more processes to be composed into a system.
system To,Tk,Fv,V,K;</system></nta>
您可以在下面找到我为系统检查创建的查询：
hf_elso_1.q:
//This file was generated from (Commercial) UPPAAL 4.0.14 (rev. 5615), May 2014
/*
*/
A[] !deadlock
/*
*/
E<> p>=41
/*
*/
E<> (cipo==1 and p>=26)
/*
*/
E<> (p==0 and talp==0 and fr==0 and to==0)
/*
*/
E<> p>=0 imply V.osszcipo>=5
/*
*/
E<> (V.osszcipo>=10)
所以我发现了我的问题所在，以下是uppaal频道同步的一些经验法则：
1。如果你使用普通的通道声明，那么如果接收方的守卫（标记为？）没有完成，发送方（标记为！）将无法继续前进。
2. 为了避免第一个异常，将频道声明为广播，这样即使接收者守卫没有完成，发送者也总是能够继续前进。
我希望这对 UPPAAL 的未来用户有用。
我正在使用 UPPAAL，我正在尝试为鞋厂建模，其中 5 个系统 运行 并联。如果有人需要，我可以写得更详细，但我不想通过描述模型来浪费任何人的时间。 所以直奔问题：UPPAAL deadlock state
在link中的图片上，自动机无法进行红色转换。转换的唯一标准是 p >= 4，但正如我所标记的，这应该没问题，因为 p=21。 那么为什么它不能进行过渡呢？ 您可以在下面 link 找到来源： https://drive.google.com/open?id=1zuige_JBTPA7kZJPwE5cocWCzY6eh8UL 非常感谢任何帮助！
我特别感兴趣的是死锁的原因，以及为什么无法进行转换，即使我试图强制转换 (不好意思，我没有上传图片的水平:()
编辑1： 由于有些人声称代码不可访问，所以我将粘贴 UPPAAL 的 2 个文件，如下所示： hf_elso_1.xml:
<?xml version="1.0" encoding="utf-8"?><!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_1.dtd'><nta><declaration>// Place global declarations here.
chan ontoindul, talpontkesz, talpakkeszen, felsoreszkesz;
clock t1,t2,t3,globalClock;
int p, to, talp, fr,cipo;</declaration><template><name x="5" y="5">talponto</name><declaration>// Place local declarations here.
</declaration><location id="id0" x="-24" y="-216"></location><location id="id1" x="-464" y="240"><committed/></location><location id="id2" x="-464" y="-24"><label kind="invariant" x="-536" y="-48">t1<=500</label></location><location id="id3" x="-24" y="-80"><committed/></location><location id="id4" x="-24" y="-152"><label kind="invariant" x="0" y="-160">t1<=800</label></location><location id="id5" x="-24" y="64"><label kind="invariant" x="-32" y="80">t1<1</label></location><location id="id6" x="-24" y="-288"><name x="-34" y="-318">start</name></location><init ref="id6"/><transition><source ref="id0"/><target ref="id4"/><label kind="synchronisation" x="-96" y="-192">ontoindul!</label></transition><transition><source ref="id6"/><target ref="id0"/><label kind="assignment" x="-80" y="-264">p:=40</label></transition><transition><source ref="id2"/><target ref="id1"/><label kind="assignment" x="-528" y="112">p=p-4</label></transition><transition><source ref="id1"/><target ref="id5"/><label kind="assignment" x="-384" y="216">to:=to+1</label></transition><transition><source ref="id5"/><target ref="id2"/><label kind="guard" x="-352" y="-48">p>=4</label><label kind="synchronisation" x="-352" y="-32">ontoindul!</label><label kind="assignment" x="-352" y="-16">t1:=0</label></transition><transition><source ref="id3"/><target ref="id5"/><label kind="assignment" x="-124" y="-40">to:=to+1,p:=p-4</label><nail x="-24" y="8"/><nail x="-24" y="16"/></transition><transition><source ref="id4"/><target ref="id3"/><label kind="assignment" x="-96" y="-120">t1:=0</label></transition></template><template><name>talpkeszito</name><location id="id7" x="88" y="120"><committed/></location><location id="id8" x="-208" y="120"><label kind="invariant" x="-256" y="136">t1<=100</label></location><location id="id9" x="-72" y="-80"></location><init ref="id9"/><transition><source ref="id7"/><target ref="id9"/><label kind="assignment" x="-52" y="20">to=to-3</label></transition><transition><source ref="id8"/><target ref="id7"/><label kind="assignment" x="-120" y="144">talp=talp+5</label></transition><transition><source ref="id9"/><target ref="id8"/><label kind="guard" x="-200" y="-10">to>2</label><label kind="synchronisation" x="-200" y="5">ontoindul?</label></transition></template><template><name>felsvag</name><location id="id10" x="112" y="-168"><label kind="invariant" x="102" y="-153">t1<=200</label></location><location id="id11" x="368" y="-176"><label kind="invariant" x="352" y="-224">t1<=100</label></location><location id="id12" x="-80" y="16"></location><location id="id13" x="-80" y="-168"></location><init ref="id13"/><transition><source ref="id10"/><target ref="id12"/><label kind="guard" x="-40" y="-144">p>0</label><label kind="assignment" x="-40" y="-128">p=p-1, fr=fr+5</label></transition><transition><source ref="id11"/><target ref="id10"/><label kind="guard" x="200" y="-208">p>0</label><label kind="assignment" x="180" y="-172">p=p-1, fr=fr+5</label></transition><transition><source ref="id12"/><target ref="id11"/><label kind="guard" x="224" y="96">fr<20</label><label kind="synchronisation" x="216" y="112">ontoindul?</label><nail x="196" y="110"/></transition><transition><source ref="id13"/><target ref="id12"/><label kind="guard" x="-152" y="-144">p>0</label><label kind="synchronisation" x="-152" y="-128">ontoindul?</label><label kind="assignment" x="-152" y="-112">p=p-1</label></transition></template><template><name>Varras</name><declaration>int osszcipo;</declaration><location id="id14" x="232" y="-216"><label kind="invariant" x="232" y="-192">t2<=10</label></location><location id="id15" x="-24" y="-208"></location><init ref="id15"/><transition><source ref="id14"/><target ref="id15"/><nail x="104" y="-328"/></transition><transition><source ref="id15"/><target ref="id14"/><label kind="guard" x="40" y="-88">talp>0 and fr>1</label><label kind="assignment" x="40" y="-72">cipo=cipo+1, talp=talp-1, fr=fr-2, t2=0,osszcipo=osszcipo+1</label><nail x="104" y="-104"/></transition></template><template><name>Kereskedo</name><location id="id16" x="16" y="-104"><label kind="invariant" x="32" y="-96">t3<=100</label></location><location id="id17" x="-184" y="-104"></location><init ref="id17"/><transition><source ref="id16"/><target ref="id17"/><nail x="-80" y="-200"/></transition><transition><source ref="id17"/><target ref="id16"/><label kind="guard" x="-48" y="16">cipo>2</label><label kind="assignment" x="-80" y="48">cipo=cipo-2,p=p+4,t3=0</label><nail x="-88" y="16"/></transition></template><system>// Place template instantiations here.
To = talponto();
Tk = talpkeszito();
Fv = felsvag();
V = Varras();
K = Kereskedo();
// List one or more processes to be composed into a system.
system To,Tk,Fv,V,K;</system></nta>
您可以在下面找到我为系统检查创建的查询：
hf_elso_1.q:
//This file was generated from (Commercial) UPPAAL 4.0.14 (rev. 5615), May 2014
/*
*/
A[] !deadlock
/*
*/
E<> p>=41
/*
*/
E<> (cipo==1 and p>=26)
/*
*/
E<> (p==0 and talp==0 and fr==0 and to==0)
/*
*/
E<> p>=0 imply V.osszcipo>=5
/*
*/
E<> (V.osszcipo>=10)
所以我发现了我的问题所在，以下是uppaal频道同步的一些经验法则：
1。如果你使用普通的通道声明，那么如果接收方的守卫（标记为？）没有完成，发送方（标记为！）将无法继续前进。
2. 为了避免第一个异常，将频道声明为广播，这样即使接收者守卫没有完成，发送者也总是能够继续前进。
我希望这对 UPPAAL 的未来用户有用。