UPPAAL死锁不清楚

Question

我正在使用UPPAAL，我试图模拟一个鞋厂，在那里5个系统并行运行。如果有人需要，我可以写得更详细，但我不想浪费任何人的时间来描述模型。所以直接到问题上来：UPPAAL死锁状态

在链接中的图片上，自动机无法进行红色转换。转换的唯一条件是p >= 4，但正如我所标记的，这应该可以作为p=21。那么，它为什么不做出转变呢？您可以在以下链接上找到源代码：JBTPA7kZJPwE5cocWCzY6eh8UL任何帮助都是非常感谢的！

我特别感兴趣的是死锁的原因，以及为什么转换是不可能的，即使我试图强制转换(对不起，但我没有上传图片的级别：())

Edit1: (一些人声称代码不可访问)，因此我将粘贴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&lt;=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&lt;=800</label></location><location id="id5" x="-24" y="64"><label kind="invariant" x="-32" y="80">t1&lt;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&gt;=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&lt;=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&gt;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&lt;=200</label></location><location id="id11" x="368" y="-176"><label kind="invariant" x="352" y="-224">t1&lt;=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&gt;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&gt;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&lt;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&gt;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&lt;=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&gt;0 and fr&gt;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&lt;=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&gt;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)

Answer 1

因此，我发现了我的问题所在，下面是一些用于uppaal信道同步的经验规则：

1.如果使用正常通道声明，则发送方(标记为!)如果接收方的护卫(标记为?)将无法继续前进。未实现。

2.为了避免第一次异常，请将频道声明为广播，这样即使接收方的保护没有得到满足，发送方也始终能够继续工作。

我希望这将对UPPAAL的未来用户有所帮助。