mirela / scp

Go to a project
Toggle navigation Toggle navigation pinning
Johan ARCILE
20b01a40 1 parent d944b920

Upload new file

Inline Side-by-side
Showing 1 changed file with 411 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>S1_t</name>
<parameter>urgent chan &amp;k_S1_F1</parameter>
<declaration>clock x;</declaration>
<location id="id0" x="0" y="0">
<name x="-25" y="-25">E</name>
<label kind="invariant" x="-50" y="20">x&lt;75</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;100</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;=50</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;=75</label>
</transition>
<transition>
<source ref="id2"/>
<target ref="id1"/>
<label kind="synchronisation" x="200" y="80">k_S1_F1!</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>S2_t</name>
<parameter>urgent chan &amp;k_S2_F2, urgent chan &amp;k_S2_F1</parameter>
<declaration>clock x;</declaration>
<location id="id3" x="0" y="0">
<name x="-20" y="-25">E</name>
<label kind="invariant" x="-50" y="20">x&lt;300</label>
</location>
<location id="id4" x="150" y="0">
<name x="130" y="-25">T</name>
<label kind="invariant" x="100" y="20">x&lt;400</label>
</location>
<location id="id5" x="300" y="0">
<name x="280" y="-25">S</name>
</location>
<location id="id6" x="300" y="100">
<name x="290" y="66">U</name>
</location>
<init ref="id3"/>
<transition>
<source ref="id3"/>
<target ref="id4"/>
<label kind="guard" x="50" y="-20">x&gt;=200</label>
<label kind="assignment" x="50" y="10">x=0</label>
</transition>
<transition>
<source ref="id4"/>
<target ref="id5"/>
<label kind="guard" x="200" y="-20">x&gt;=350</label>
</transition>
<transition>
<source ref="id5"/>
<target ref="id6"/>
<label kind="synchronisation" x="350" y="80">k_S2_F2!</label>
<nail x="450" y="0"/>
<nail x="450" y="100"/>
</transition>
<transition>
<source ref="id6"/>
<target ref="id4"/>
<label kind="synchronisation" x="200" y="80">k_S2_F1!</label>
<label kind="assignment" x="200" y="110">x=0</label>
<nail x="150" y="100"/>
</transition>
</template>
<template>
<name>S3_t</name>
<parameter>urgent chan &amp;k_S3_F2, urgent chan &amp;k_S3_B</parameter>
<declaration>clock x;</declaration>
<location id="id7" x="0" y="0">
<name x="-20" y="-25">E</name>
<label kind="invariant" x="-50" y="20">x&lt;300</label>
</location>
<location id="id8" x="150" y="0">
<name x="130" y="-25">T</name>
<label kind="invariant" x="100" y="20">x&lt;400</label>
</location>
<location id="id9" x="300" y="0">
<name x="280" y="-25">S</name>
</location>
<location id="id10" x="300" y="100">
<name x="290" y="66">U</name>
</location>
<init ref="id7"/>
<transition>
<source ref="id7"/>
<target ref="id8"/>
<label kind="guard" x="50" y="-20">x&gt;=200</label>
<label kind="assignment" x="50" y="10">x=0</label>
</transition>
<transition>
<source ref="id8"/>
<target ref="id9"/>
<label kind="guard" x="200" y="-20">x&gt;=350</label>
</transition>
<transition>
<source ref="id9"/>
<target ref="id10"/>
<label kind="synchronisation" x="350" y="80">k_S3_F2!</label>
<nail x="450" y="0"/>
<nail x="450" y="100"/>
</transition>
<transition>
<source ref="id10"/>
<target ref="id8"/>
<label kind="synchronisation" x="200" y="80">k_S3_B!</label>
<label kind="assignment" x="200" y="110">x=0</label>
<nail x="150" y="100"/>
</transition>
</template>
<template>
<name>F1_t</name>
<parameter>urgent chan &amp;k_S1_F1, urgent chan &amp;k_S2_F1, urgent chan &amp;lock_M, urgent chan &amp;unlock_M</parameter>
<declaration>clock x;</declaration>
<location id="id11" x="0" y="0">
<name x="-20" y="-25">W</name>
</location>
<location id="id12" x="150" y="0">
<name x="130" y="-25">P0</name>
<label kind="invariant" x="100" y="20">x&lt;75</label>
</location>
<location id="id13" x="150" y="-100">
<name x="130" y="-125">P1</name>
<label kind="invariant" x="100" y="-80">x&lt;75</label>
</location>
<location id="id14" x="300" y="0">
<name x="280" y="-25">S</name>
</location>
<location id="id15" x="300" y="100">
<label kind="invariant" x="250" y="120">x&lt;50</label>
</location>
<location id="id16" x="150" y="100">
</location>
<init ref="id11"/>
<transition>
<source ref="id11"/>
<target ref="id12"/>
<label kind="synchronisation" x="50" y="-20">k_S1_F1?</label>
<label kind="assignment" x="50" y="10">x=0</label>
</transition>
<transition>
<source ref="id11"/>
<target ref="id13"/>
<label kind="synchronisation" x="50" y="-120">k_S2_F1?</label>
<label kind="assignment" x="50" y="-90">x=0</label>
<nail x="0" y="-100"/>
</transition>
<transition>
<source ref="id12"/>
<target ref="id14"/>
<label kind="guard" x="200" y="-20">x&gt;=50</label>
</transition>
<transition>
<source ref="id13"/>
<target ref="id14"/>
<label kind="guard" x="200" y="-120">x&gt;=50</label>
<nail x="300" y="-100"/>
</transition>
<transition>
<source ref="id14"/>
<target ref="id15"/>
<label kind="synchronisation" x="350" y="80">lock_M!</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="id15"/>
<target ref="id16"/>
<label kind="guard" x="200" y="80">x&gt;=25</label>
</transition>
<transition>
<source ref="id16"/>
<target ref="id11"/>
<label kind="synchronisation" x="50" y="80">unlock_M!</label>
<nail x="0" y="100"/>
</transition>
</template>
<template>
<name>F2_t</name>
<parameter>urgent chan &amp;k_S2_F2, urgent chan &amp;k_S3_F2, urgent chan &amp;k_F2_B</parameter>
<declaration>clock x;</declaration>
<location id="id17" x="0" y="0">
<name x="-20" y="-25">W</name>
</location>
<location id="id18" x="150" y="0">
<name x="130" y="-25">P0</name>
<label kind="invariant" x="100" y="20">x&lt;100</label>
</location>
<location id="id19" x="150" y="-100">
<name x="130" y="-125">P1</name>
<label kind="invariant" x="100" y="-80">x&lt;100</label>
</location>
<location id="id20" x="300" y="0">
<name x="280" y="-25">S</name>
</location>
<init ref="id17"/>
<transition>
<source ref="id17"/>
<target ref="id18"/>
<label kind="synchronisation" x="50" y="-20">k_S2_F2?</label>
<label kind="assignment" x="50" y="10">x=0</label>
</transition>
<transition>
<source ref="id17"/>
<target ref="id19"/>
<label kind="synchronisation" x="50" y="-120">k_S3_F2?</label>
<label kind="assignment" x="50" y="-90">x=0</label>
<nail x="0" y="-100"/>
</transition>
<transition>
<source ref="id18"/>
<target ref="id20"/>
<label kind="guard" x="200" y="-20">x&gt;=75</label>
</transition>
<transition>
<source ref="id19"/>
<target ref="id20"/>
<label kind="guard" x="200" y="-120">x&gt;=75</label>
<nail x="300" y="-100"/>
</transition>
<transition>
<source ref="id20"/>
<target ref="id17"/>
<label kind="synchronisation" x="50" y="80">k_F2_B!</label>
<nail x="300" y="100"/>
<nail x="0" y="100"/>
</transition>
</template>
<template>
<name>B_t</name>
<parameter>urgent chan &amp;k_S3_B, urgent chan &amp;k_F2_B, urgent chan &amp;lock_M, urgent chan &amp;unlock_M</parameter>
<declaration>clock x;</declaration>
<location id="id21" x="0" y="0">
<name x="-20" y="-25">W</name>
</location>
<location id="id22" x="300" y="0">
<name x="280" y="-25">P</name>
<label kind="invariant" x="250" y="20">x&lt;50</label>
</location>
<location id="id23" x="150" y="0">
<name x="136" y="-34">B</name>
</location>
<location id="id24" x="150" y="-100">
<name x="140" y="-134">A</name>
</location>
<location id="id25" x="450" y="0">
<name x="430" y="-25">S</name>
</location>
<location id="id26" x="300" y="100">
<label kind="invariant" x="250" y="120">x&lt;50</label>
</location>
<location id="id27" x="150" y="100">
</location>
<init ref="id21"/>
<transition>
<source ref="id21"/>
<target ref="id23"/>
<label kind="synchronisation" x="50" y="-20">k_S3_B?</label>
</transition>
<transition>
<source ref="id21"/>
<target ref="id24"/>
<label kind="synchronisation" x="50" y="-120">k_F2_B?</label>
<nail x="0" y="-100"/>
</transition>
<transition>
<source ref="id23"/>
<target ref="id22"/>
<label kind="synchronisation" x="200" y="-20">k_F2_B?</label>
<label kind="assignment" x="200" y="10">x=0</label>
</transition>
<transition>
<source ref="id24"/>
<target ref="id22"/>
<label kind="synchronisation" x="200" y="-120">k_S3_B?</label>
<label kind="assignment" x="200" y="-90">x=0</label>
<nail x="300" y="-100"/>
</transition>
<transition>
<source ref="id22"/>
<target ref="id25"/>
<label kind="guard" x="350" y="-20">x&gt;=25</label>
</transition>
<transition>
<source ref="id25"/>
<target ref="id26"/>
<label kind="synchronisation" x="350" y="80">lock_M!</label>
<label kind="assignment" x="350" y="110">x=0</label>
<nail x="450" y="100"/>
</transition>
<transition>
<source ref="id26"/>
<target ref="id27"/>
<label kind="guard" x="200" y="80">x&gt;=25</label>
</transition>
<transition>
<source ref="id27"/>
<target ref="id21"/>
<label kind="synchronisation" x="50" y="80">unlock_M!</label>
<nail x="0" y="100"/>
</transition>
</template>
<template>
<name>M_t</name>
<parameter>urgent chan &amp;lock_M, urgent chan &amp;unlock_M</parameter>
<location id="id28" x="0" y="0">
<name x="-20" y="-25">W</name>
</location>
<location id="id29" x="150" y="0">
</location>
<init ref="id28"/>
<transition>
<source ref="id28"/>
<target ref="id29"/>
<label kind="synchronisation" x="50" y="-20">lock_M?</label>
</transition>
<transition>
<source ref="id29"/>
<target ref="id28"/>
<label kind="synchronisation" x="50" y="80">unlock_M?</label>
<nail x="150" y="100"/>
<nail x="0" y="100"/>
</transition>
</template>
<template>
<name>R_t</name>
<parameter>urgent chan &amp;lock_M, urgent chan &amp;unlock_M</parameter>
<declaration>clock x;</declaration>
<location id="id30" x="0" y="0">
<name x="-20" y="-25">W</name>
</location>
<location id="id31" x="150" y="0">
<name x="130" y="-25">M</name>
<label kind="invariant" x="100" y="20">x&lt;50</label>
</location>
<location id="id32" x="300" y="0">
</location>
<location id="id33" x="450" y="0">
<name x="430" y="-25">S</name>
<label kind="invariant" x="400" y="20">x&lt;75</label>
</location>
<init ref="id30"/>
<transition>
<source ref="id30"/>
<target ref="id31"/>
<label kind="synchronisation" x="50" y="-20">lock_M!</label>
<label kind="assignment" x="50" y="10">x=0</label>
</transition>
<transition>
<source ref="id31"/>
<target ref="id32"/>
<label kind="guard" x="200" y="-20">x&gt;=25</label>
</transition>
<transition>
<source ref="id32"/>
<target ref="id33"/>
<label kind="synchronisation" x="350" y="-20">unlock_M!</label>
<label kind="assignment" x="350" y="10">x=0</label>
</transition>
<transition>
<source ref="id33"/>
<target ref="id30"/>
<label kind="guard" x="200" y="80">x&gt;=50</label>
<nail x="450" y="100"/>
<nail x="0" y="100"/>
</transition>
</template>
<system>
urgent chan k_S1_F1;
urgent chan k_S2_F2;
urgent chan k_S2_F1;
urgent chan k_S3_F2;
urgent chan k_S3_B;
urgent chan k_F2_B;
urgent chan lock_M;
urgent chan unlock_M;
S1 = S1_t(k_S1_F1);
S2 = S2_t(k_S2_F2, k_S2_F1);
S3 = S3_t(k_S3_F2, k_S3_B);
F1 = F1_t(k_S1_F1, k_S2_F1, lock_M, unlock_M);
F2 = F2_t(k_S2_F2, k_S3_F2, k_F2_B);
B = B_t(k_S3_B, k_F2_B, lock_M, unlock_M);
M = M_t(lock_M, unlock_M);
R = R_t(lock_M, unlock_M);
system S1, S2, S3, F1, F2, B, M, R;
</system>
</nta>