mirela / scp

Go to a project
Toggle navigation Toggle navigation pinning
Johan ARCILE
7f7605bb 1 parent 8020a5ef

Upload new file

Inline Side-by-side
Showing 1 changed file with 258 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,y;</declaration>
<location id="id0" x="144" y="102">
<name x="127" y="68">Q</name>
<urgent/>
</location>
<location id="id1" 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="id2" x="144" y="0">
<name x="124" y="-25">T</name>
<label kind="invariant" x="94" y="20">x&lt;4500</label>
</location>
<location id="id3" x="300" y="0">
<name x="280" y="-25">S</name>
</location>
<init ref="id1"/>
<transition>
<source ref="id0"/>
<target ref="id2"/>
<label kind="assignment" x="153" y="42">y=0</label>
</transition>
<transition>
<source ref="id1"/>
<target ref="id2"/>
<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="id2"/>
<target ref="id3"/>
<label kind="guard" x="200" y="-20">x&gt;=3500</label>
</transition>
<transition>
<source ref="id3"/>
<target ref="id0"/>
<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"/>
</transition>
</template>
<template>
<name>O_t</name>
<parameter>urgent chan &amp;k_O_Pr, urgent chan &amp;k_O_F</parameter>
<declaration>clock x,y;</declaration>
<location id="id4" x="0" y="102">
<name x="-10" y="68">Q</name>
<urgent/>
</location>
<location id="id5" x="0" y="0">
<name x="-20" y="-25">S</name>
</location>
<location id="id6" x="150" y="0">
<name x="130" y="-25">T</name>
</location>
<location id="id7" x="150" y="100">
</location>
<init ref="id5"/>
<transition>
<source ref="id4"/>
<target ref="id5"/>
<label kind="assignment" x="8" y="42">y=0</label>
</transition>
<transition>
<source ref="id5"/>
<target ref="id6"/>
<label kind="guard" x="50" y="-20">x&gt;=50</label>
</transition>
<transition>
<source ref="id6"/>
<target ref="id7"/>
<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="id7"/>
<target ref="id4"/>
<label kind="synchronisation" x="50" y="80">k_O_F!</label>
<label kind="assignment" x="50" y="110">x=0</label>
</transition>
</template>
<template>
<name>P_t</name>
<parameter>urgent chan &amp;k_P_F</parameter>
<declaration>clock x,y;</declaration>
<location id="id8" x="144" y="102">
<name x="127" y="68">Q</name>
<urgent/>
</location>
<location id="id9" 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="id10" x="144" y="0">
<name x="124" y="-25">T</name>
<label kind="invariant" x="94" y="20">x&lt;3600</label>
</location>
<location id="id11" x="300" y="0">
<name x="280" y="-25">S</name>
</location>
<init ref="id9"/>
<transition>
<source ref="id8"/>
<target ref="id10"/>
<label kind="assignment" x="153" y="42">y=0</label>
</transition>
<transition>
<source ref="id9"/>
<target ref="id10"/>
<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="id10"/>
<target ref="id11"/>
<label kind="guard" x="200" y="-20">x&gt;=2600</label>
</transition>
<transition>
<source ref="id11"/>
<target ref="id8"/>
<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"/>
</transition>
</template>
<template>
<name>Pr_t</name>
<parameter>urgent chan &amp;k_C_Pr, urgent chan &amp;k_O_Pr</parameter>
<declaration>clock x,y;</declaration>
<location id="id12" x="289" y="119">
<label kind="invariant" x="279" y="136">x&lt;610</label>
</location>
<location id="id13" x="289" y="0">
<name x="272" y="-34">Q</name>
<urgent/>
</location>
<location id="id14" x="0" y="0">
<name x="-20" y="-25">W</name>
</location>
<location id="id15" x="153" y="0">
<name x="133" y="-25">P</name>
<label kind="invariant" x="103" y="20">x&lt;3000</label>
</location>
<location id="id16" x="0" y="-100">
<name x="-20" y="-125">W2</name>
</location>
<init ref="id14"/>
<transition>
<source ref="id13"/>
<target ref="id12"/>
<label kind="assignment" x="297" y="51">x=0</label>
</transition>
<transition>
<source ref="id12"/>
<target ref="id14"/>
<label kind="guard" x="119" y="93">x&gt;=200</label>
<label kind="assignment" x="110" y="127">y=0</label>
<nail x="0" y="119"/>
</transition>
<transition>
<source ref="id14"/>
<target ref="id15"/>
<label kind="synchronisation" x="50" y="-20">k_C_Pr?</label>
<label kind="assignment" x="50" y="10">x=0</label>
</transition>
<transition>
<source ref="id14"/>
<target ref="id16"/>
<label kind="synchronisation" x="-50" y="-60">k_O_Pr?</label>
</transition>
<transition>
<source ref="id16"/>
<target ref="id15"/>
<label kind="synchronisation" x="50" y="-120">k_C_Pr?</label>
<label kind="assignment" x="50" y="-90">x=0</label>
<nail x="153" y="-102"/>
</transition>
<transition>
<source ref="id15"/>
<target ref="id13"/>
<label kind="guard" x="200" y="-20">x&gt;=2000</label>
</transition>
</template>
<template>
<name>F_t</name>
<parameter>urgent chan &amp;k_O_F, urgent chan &amp;k_P_F</parameter>
<declaration>clock x,y;</declaration>
<location id="id17" x="306" y="127">
<label kind="invariant" x="296" y="144">x&lt;100</label>
</location>
<location id="id18" x="306" y="0">
<name x="280" y="-26">Q</name>
<urgent/>
</location>
<location id="id19" x="0" y="0">
<name x="-20" y="-25">W</name>
</location>
<location id="id20" x="153" y="0">
<name x="133" y="-25">P</name>
<label kind="invariant" x="103" y="20">x&lt;75</label>
</location>
<init ref="id19"/>
<transition>
<source ref="id18"/>
<target ref="id17"/>
<label kind="assignment" x="314" y="59">x=0</label>
</transition>
<transition>
<source ref="id17"/>
<target ref="id19"/>
<label kind="guard" x="127" y="102">x&gt;=30</label>
<label kind="assignment" x="119" y="136">y=0</label>
<nail x="0" y="127"/>
</transition>
<transition>
<source ref="id19"/>
<target ref="id20"/>
<label kind="synchronisation" x="50" y="-20">k_O_F?</label>
<label kind="assignment" x="50" y="10">x=0</label>
</transition>
<transition>
<source ref="id19"/>
<target ref="id20"/>
<label kind="synchronisation" x="50" y="-120">k_P_F?</label>
<label kind="assignment" x="50" y="-90">x=0</label>
<nail x="0" y="-100"/>
<nail x="153" y="-102"/>
</transition>
<transition>
<source ref="id20"/>
<target ref="id18"/>
<label kind="guard" x="200" y="-20">x&gt;=50</label>
</transition>
</template>
<system>
urgent chan k_C_Pr;
urgent chan k_O_Pr;
urgent chan k_O_F;
urgent chan k_P_F;
C = C_t(k_C_Pr);
O = O_t(k_O_Pr, k_O_F);
P = P_t(k_P_F);
Q = Pr_t(k_C_Pr, k_O_Pr);
F = F_t(k_O_F, k_P_F);
system C, O, P, Q, F;
</system>
</nta>