mirela / scp

Go to a project
Toggle navigation Toggle navigation pinning
Johan ARCILE
43e44c67 1 parent fc796bca

Upload new file

Inline Side-by-side
Showing 1 changed file with 442 additions and 0 deletions
<?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>
</declaration>
<template>
<name>C_t</name>
<parameter>urgent chan &amp;k_C_Pr</parameter>
<declaration>clock x;</declaration>
<location id="id0" x="0" y="0">
<name x="-20" y="-25">E</name>
<label kind="invariant" x="-50" y="20">x&lt;3000</label>
</location>
<location id="id1" x="150" y="0">
<name x="130" y="-25">T</name>
<label kind="invariant" x="100" y="20">x&lt;4500</label>
</location>
<location id="id2" x="300" y="0">
<name x="280" y="-25">S</name>
</location>
<init ref="id0"/>
<transition>
<source ref="id0"/>
<target ref="id1"/>
<label kind="guard" x="50" y="-20">x&gt;=2000</label>
<label kind="assignment" x="50" y="10">x=0</label>
</transition>
<transition>
<source ref="id1"/>
<target ref="id2"/>
<label kind="guard" x="200" y="-20">x&gt;=3500</label>
</transition>
<transition>
<source ref="id2"/>
<target ref="id1"/>
<label kind="synchronisation" x="200" y="80">k_C_Pr!</label>
<label kind="assignment" x="200" y="110">x=0</label>
<nail x="300" y="100"/>
<nail x="150" y="100"/>
</transition>
</template>
<template>
<name>O_t</name>
<parameter>urgent chan &amp;k_O_Pr, urgent chan &amp;k_O_F</parameter>
<declaration>clock x;</declaration>
<location id="id3" x="0" y="0">
<name x="-20" y="-25">S</name>
</location>
<location id="id4" x="150" y="0">
<name x="130" y="-25">T</name>
</location>
<location id="id5" x="150" y="100">
</location>
<init ref="id3"/>
<transition>
<source ref="id3"/>
<target ref="id4"/>
<label kind="guard" x="50" y="-20">x&gt;=50</label>
</transition>
<transition>
<source ref="id4"/>
<target ref="id5"/>
<label kind="synchronisation" x="200" y="80">k_O_Pr!</label>
<nail x="300" y="0"/>
<nail x="300" y="100"/>
</transition>
<transition>
<source ref="id5"/>
<target ref="id3"/>
<label kind="synchronisation" x="50" y="80">k_O_F!</label>
<label kind="assignment" x="50" y="110">x=0</label>
<nail x="0" y="100"/>
</transition>
</template>
<template>
<name>P_t</name>
<parameter>urgent chan &amp;k_P_F</parameter>
<declaration>clock x;</declaration>
<location id="id6" x="0" y="0">
<name x="-20" y="-25">E</name>
<label kind="invariant" x="-50" y="20">x&lt;3600</label>
</location>
<location id="id7" x="150" y="0">
<name x="130" y="-25">T</name>
<label kind="invariant" x="100" y="20">x&lt;3600</label>
</location>
<location id="id8" x="300" y="0">
<name x="280" y="-25">S</name>
</location>
<init ref="id6"/>
<transition>
<source ref="id6"/>
<target ref="id7"/>
<label kind="guard" x="50" y="-20">x&gt;=2600</label>
<label kind="assignment" x="50" y="10">x=0</label>
</transition>
<transition>
<source ref="id7"/>
<target ref="id8"/>
<label kind="guard" x="200" y="-20">x&gt;=2600</label>
</transition>
<transition>
<source ref="id8"/>
<target ref="id7"/>
<label kind="synchronisation" x="200" y="80">k_P_F!</label>
<label kind="assignment" x="200" y="110">x=0</label>
<nail x="300" y="100"/>
<nail x="150" y="100"/>
</transition>
</template>
<template>
<name>Pr_t</name>
<parameter>urgent chan &amp;lock_M1, urgent chan &amp;unlock_M1</parameter>
<declaration>clock x,y;
</declaration>
<location id="id9" x="0" y="102">
<name x="-17" y="68">Q</name>
<urgent/>
</location>
<location id="id10" x="0" y="0">
<name x="-20" y="-25">W</name>
<label kind="invariant" x="-68" y="17">x&lt;5300</label>
</location>
<location id="id11" x="300" y="0">
</location>
<location id="id12" x="300" y="100">
<label kind="invariant" x="250" y="120">x&lt;300</label>
</location>
<location id="id13" x="150" y="100">
<name x="140" y="66">S</name>
</location>
<init ref="id10"/>
<transition>
<source ref="id9"/>
<target ref="id10"/>
</transition>
<transition>
<source ref="id10"/>
<target ref="id11"/>
<label kind="guard" x="119" y="-25">x&gt;=2000</label>
<label kind="assignment" x="136" y="0">y=0</label>
</transition>
<transition>
<source ref="id11"/>
<target ref="id12"/>
<label kind="synchronisation" x="350" y="80">lock_M1!</label>
<label kind="assignment" x="350" y="110">x=0</label>
<nail x="450" y="0"/>
<nail x="450" y="100"/>
</transition>
<transition>
<source ref="id12"/>
<target ref="id13"/>
<label kind="guard" x="200" y="80">x&gt;=200</label>
</transition>
<transition>
<source ref="id13"/>
<target ref="id9"/>
<label kind="synchronisation" x="50" y="80">unlock_M1!</label>
<label kind="assignment" x="51" y="102">x=0</label>
</transition>
</template>
<template>
<name>F_t</name>
<parameter>urgent chan &amp;lock_M2, urgent chan &amp;unlock_M2, urgent chan &amp;lock_M3, urgent chan &amp;unlock_M3</parameter>
<declaration>clock x;</declaration>
<location id="id14" x="0" y="0">
<name x="-20" y="-25">W</name>
<label kind="invariant" x="-68" y="8">x&lt;7275</label>
</location>
<location id="id15" x="300" y="0">
</location>
<location id="id16" x="750" y="100">
<label kind="invariant" x="700" y="120">x&lt;30</label>
</location>
<location id="id17" x="600" y="100">
</location>
<location id="id18" x="450" y="100">
</location>
<location id="id19" x="300" y="100">
<label kind="invariant" x="250" y="120">x&lt;20</label>
</location>
<location id="id20" x="150" y="100">
</location>
<init ref="id14"/>
<transition>
<source ref="id14"/>
<target ref="id15"/>
<label kind="guard" x="200" y="-20">x&gt;=50</label>
</transition>
<transition>
<source ref="id15"/>
<target ref="id16"/>
<label kind="synchronisation" x="800" y="80">lock_M2!</label>
<label kind="assignment" x="800" y="110">x=0</label>
<nail x="900" y="0"/>
<nail x="900" y="100"/>
</transition>
<transition>
<source ref="id16"/>
<target ref="id17"/>
<label kind="guard" x="650" y="80">x&gt;=20</label>
</transition>
<transition>
<source ref="id17"/>
<target ref="id18"/>
<label kind="synchronisation" x="500" y="80">unlock_M2!</label>
</transition>
<transition>
<source ref="id18"/>
<target ref="id19"/>
<label kind="synchronisation" x="350" y="80">lock_M3!</label>
<label kind="assignment" x="350" y="110">x=0</label>
</transition>
<transition>
<source ref="id19"/>
<target ref="id20"/>
<label kind="guard" x="200" y="80">x&gt;=10</label>
</transition>
<transition>
<source ref="id20"/>
<target ref="id14"/>
<label kind="synchronisation" x="50" y="80">unlock_M3!</label>
<label kind="assignment" x="18" y="100">x=0</label>
<nail x="0" y="100"/>
</transition>
</template>
<template>
<name>M1_t</name>
<parameter>urgent chan &amp;lock_M1, urgent chan &amp;unlock_M1</parameter>
<location id="id21" x="0" y="0">
<name x="-20" y="-25">W</name>
</location>
<location id="id22" x="150" y="0">
</location>
<init ref="id21"/>
<transition>
<source ref="id21"/>
<target ref="id22"/>
<label kind="synchronisation" x="50" y="-20">lock_M1?</label>
</transition>
<transition>
<source ref="id22"/>
<target ref="id21"/>
<label kind="synchronisation" x="50" y="80">unlock_M1?</label>
<nail x="150" y="100"/>
<nail x="0" y="100"/>
</transition>
</template>
<template>
<name>M2_t</name>
<parameter>urgent chan &amp;lock_M2, urgent chan &amp;unlock_M2</parameter>
<location id="id23" x="0" y="0">
<name x="-20" y="-25">W</name>
</location>
<location id="id24" x="150" y="0">
</location>
<init ref="id23"/>
<transition>
<source ref="id23"/>
<target ref="id24"/>
<label kind="synchronisation" x="50" y="-20">lock_M2?</label>
</transition>
<transition>
<source ref="id24"/>
<target ref="id23"/>
<label kind="synchronisation" x="50" y="80">unlock_M2?</label>
<nail x="150" y="100"/>
<nail x="0" y="100"/>
</transition>
</template>
<template>
<name>M3_t</name>
<parameter>urgent chan &amp;lock_M3, urgent chan &amp;unlock_M3</parameter>
<location id="id25" x="0" y="0">
<name x="-20" y="-25">W</name>
</location>
<location id="id26" x="150" y="0">
</location>
<init ref="id25"/>
<transition>
<source ref="id25"/>
<target ref="id26"/>
<label kind="synchronisation" x="50" y="-20">lock_M3?</label>
</transition>
<transition>
<source ref="id26"/>
<target ref="id25"/>
<label kind="synchronisation" x="50" y="80">unlock_M3?</label>
<nail x="150" y="100"/>
<nail x="0" y="100"/>
</transition>
</template>
<template>
<name>G_t</name>
<parameter>urgent chan &amp;lock_M1, urgent chan &amp;unlock_M1</parameter>
<declaration>clock x,y;</declaration>
<location id="id27" x="0" y="102">
<name x="-17" y="68">Q</name>
<urgent/>
</location>
<location id="id28" x="0" y="0">
<name x="-20" y="-25">W</name>
</location>
<location id="id29" x="150" y="0">
<name x="130" y="-25">M</name>
<label kind="invariant" x="100" y="20">x&lt;310</label>
</location>
<location id="id30" x="300" y="0">
</location>
<location id="id31" x="450" y="0">
<name x="430" y="-25">S</name>
<label kind="invariant" x="400" y="20">x&lt;500</label>
</location>
<init ref="id28"/>
<transition>
<source ref="id27"/>
<target ref="id28"/>
<label kind="assignment" x="8" y="42">y=0</label>
</transition>
<transition>
<source ref="id28"/>
<target ref="id29"/>
<label kind="synchronisation" x="50" y="-20">lock_M1!</label>
<label kind="assignment" x="50" y="10">x=0</label>
</transition>
<transition>
<source ref="id29"/>
<target ref="id30"/>
<label kind="guard" x="200" y="-20">x&gt;=210</label>
</transition>
<transition>
<source ref="id30"/>
<target ref="id31"/>
<label kind="synchronisation" x="350" y="-20">unlock_M1!</label>
<label kind="assignment" x="350" y="10">x=0</label>
</transition>
<transition>
<source ref="id31"/>
<target ref="id27"/>
<label kind="guard" x="200" y="80">x&gt;=400</label>
<nail x="450" y="100"/>
</transition>
</template>
<template>
<name>H_t</name>
<parameter>urgent chan &amp;lock_M2, urgent chan &amp;unlock_M2</parameter>
<declaration>clock x;</declaration>
<location id="id32" x="0" y="0">
<name x="-20" y="-25">W</name>
</location>
<location id="id33" x="150" y="0">
<name x="130" y="-25">M</name>
<label kind="invariant" x="100" y="20">x&lt;30</label>
</location>
<location id="id34" x="300" y="0">
</location>
<location id="id35" x="450" y="0">
<name x="430" y="-25">S</name>
<label kind="invariant" x="400" y="20">x&lt;20</label>
</location>
<init ref="id32"/>
<transition>
<source ref="id32"/>
<target ref="id33"/>
<label kind="synchronisation" x="50" y="-20">lock_M2!</label>
<label kind="assignment" x="50" y="10">x=0</label>
</transition>
<transition>
<source ref="id33"/>
<target ref="id34"/>
<label kind="guard" x="200" y="-20">x&gt;=20</label>
</transition>
<transition>
<source ref="id34"/>
<target ref="id35"/>
<label kind="synchronisation" x="350" y="-20">unlock_M2!</label>
<label kind="assignment" x="350" y="10">x=0</label>
</transition>
<transition>
<source ref="id35"/>
<target ref="id32"/>
<label kind="guard" x="200" y="80">x&gt;=10</label>
<nail x="450" y="100"/>
<nail x="0" y="100"/>
</transition>
</template>
<template>
<name>M_t</name>
<parameter>urgent chan &amp;lock_M3, urgent chan &amp;unlock_M3</parameter>
<declaration>clock x;</declaration>
<location id="id36" x="0" y="0">
<name x="-20" y="-25">W</name>
</location>
<location id="id37" x="150" y="0">
<name x="130" y="-25">M</name>
<label kind="invariant" x="100" y="20">x&lt;20</label>
</location>
<location id="id38" x="300" y="0">
</location>
<location id="id39" x="450" y="0">
<name x="430" y="-25">S</name>
<label kind="invariant" x="400" y="20">x&lt;20</label>
</location>
<init ref="id36"/>
<transition>
<source ref="id36"/>
<target ref="id37"/>
<label kind="synchronisation" x="50" y="-20">lock_M3!</label>
<label kind="assignment" x="50" y="10">x=0</label>
</transition>
<transition>
<source ref="id37"/>
<target ref="id38"/>
<label kind="guard" x="200" y="-20">x&gt;=10</label>
</transition>
<transition>
<source ref="id38"/>
<target ref="id39"/>
<label kind="synchronisation" x="350" y="-20">unlock_M3!</label>
<label kind="assignment" x="350" y="10">x=0</label>
</transition>
<transition>
<source ref="id39"/>
<target ref="id36"/>
<label kind="guard" x="200" y="80">x&gt;=10</label>
<nail x="450" y="100"/>
<nail x="0" y="100"/>
</transition>
</template>
<system>urgent chan lock_M1;
urgent chan unlock_M1;
Q = Pr_t(lock_M1, unlock_M1);
M1 = M1_t(lock_M1, unlock_M1);
G = G_t(lock_M1, unlock_M1);
system Q, M1, G;
</system>
</nta>