UPPAAL тупик неясен
Я использую UPPAAL и пытаюсь смоделировать обувную фабрику, где 5 систем работают паралельно. Я могу написать об этом более подробно, если кому-то это нужно, но я не хочу тратить время на описание модели. Итак, прямо к проблеме: UPPAAL тупиковое состояние
На картинке в ссылке автомат не может сделать красный переход. Критерием только переходов является то, что p >= 4, но, как я отметил, это должно быть хорошо, так как p=21. Так почему же он не может сделать переход? Вы можете найти источник по ссылке ниже: https://drive.google.com/open?id=1zuige_JBTPA7kZJPwE5cocWCzY6eh8UL Любая помощь высоко ценится!
Меня интересует, в частности, причина тупика, и почему переход невозможен, хотя я пытался форсировать переход (извините, но у меня нет уровня для загрузки изображений:()
Edit1: как некоторые люди утверждали, что код недоступен, поэтому я вставлю 2 файла для UPPAAL, как показано ниже: 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)
1 ответ
Итак, я выяснил, в чем заключалась моя проблема, и ниже приведены некоторые практические правила для синхронизации каналов uppaal:
1. Если вы используете обычное объявление канала, то отправитель (отмеченный знаком!) Не сможет двигаться дальше, если защита на стороне получателя (отмечена знаком?) Не выполнена.
2. Чтобы избежать первой аномалии, объявите канал как широковещательный, чтобы отправитель всегда мог двигаться дальше, даже если защита получателя не выполнена.
Я надеюсь, что это будет полезно для будущих пользователей UPPAAL.