I'm using UPPAAL, and I'm trying to model a shoe factory, where 5 systems run paralelly. I can write on this more detailed if someone needs it, but I do not want to waste anyones time by describing the model. So straight to the problem:UPPAAL deadlock state
On the picture in the link the automaton cannot make the red transition. The transitions only criteria is that p >= 4, but as I have marked, this should be fine, as p=21. So why cant it make the transition? You can find the source on the below link: https://drive.google.com/open?id=1zuige_JBTPA7kZJPwE5cocWCzY6eh8UL Any help is highly appreciated!
I am interested in the reason for the deadlock in particular, and why the transition is not possible, even though I was trying to force the transition (sorry, but I do not have the level to upload images:()
Edit1: As some people claimed the code is not accessible,so I will paste the 2 files for UPPAAL as below: 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>
And below you can find the queries I created for system checking:
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)
So I found out what was my problem, and below are some rules of thumb for uppaal channel synchronization:
1. If you use a normal channel declaration, then the sender (marked with !) will not be able to move on if the guard on the receiver side (marked with ?) is not fulfilled.
2. To avoid the first anomaly, declare the channel as broadcast, so the sender will always be able to move on even though the receiver guard is not fulfilled.
I hope this will be useful for future users of UPPAAL.