Toggle navigation
Toggle navigation
This project
Loading...
Sign in
mirela
/
scp
Go to a project
Toggle navigation
Toggle navigation pinning
Projects
Groups
Snippets
Help
Project
Activity
Repository
Pipelines
Graphs
Issues
0
Merge Requests
0
Wiki
Network
Create a new issue
Builds
Commits
Authored by
Johan ARCILE
2017-06-02 15:59:45 +0000
Browse Files
Options
Browse Files
Download
Email Patches
Plain Diff
Commit
b8f216ecb36924205d5ab87dcede21c2e9695da5
b8f216ec
1 parent
97fa24c0
Upload new file
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
499 additions
and
0 deletions
Ex3/Uppaal/Ex3.xml
Ex3/Uppaal/Ex3.xml
0 → 100644
View file @
b8f216e
<?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
&
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
<
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
<
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
>
=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
>
=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
&
k_O_Pr, urgent chan
&
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
>
=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
&
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
<
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
<
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
>
=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
>
=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
&
k_C_Pr, urgent chan
&
k_O_Pr, urgent chan
&
lock_M1, urgent chan
&
unlock_M1
</parameter>
<declaration>
clock x;
</declaration>
<location
id=
"id9"
x=
"0"
y=
"0"
>
<name
x=
"-20"
y=
"-25"
>
W
</name>
</location>
<location
id=
"id10"
x=
"150"
y=
"0"
>
<name
x=
"130"
y=
"-25"
>
P
</name>
<label
kind=
"invariant"
x=
"100"
y=
"20"
>
x
<
3000
</label>
</location>
<location
id=
"id11"
x=
"0"
y=
"-100"
>
<name
x=
"-20"
y=
"-125"
>
W2
</name>
</location>
<location
id=
"id12"
x=
"150"
y=
"-100"
>
<name
x=
"130"
y=
"-125"
>
P2
</name>
<label
kind=
"invariant"
x=
"100"
y=
"-80"
>
x
<
3000
</label>
</location>
<location
id=
"id13"
x=
"300"
y=
"0"
>
</location>
<location
id=
"id14"
x=
"300"
y=
"100"
>
<label
kind=
"invariant"
x=
"250"
y=
"120"
>
x
<
300
</label>
</location>
<location
id=
"id15"
x=
"150"
y=
"100"
>
</location>
<init
ref=
"id9"
/>
<transition>
<source
ref=
"id9"
/>
<target
ref=
"id10"
/>
<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=
"id9"
/>
<target
ref=
"id11"
/>
<label
kind=
"synchronisation"
x=
"-50"
y=
"-60"
>
k_O_Pr?
</label>
</transition>
<transition>
<source
ref=
"id11"
/>
<target
ref=
"id12"
/>
<label
kind=
"synchronisation"
x=
"50"
y=
"-120"
>
k_C_Pr?
</label>
<label
kind=
"assignment"
x=
"50"
y=
"-90"
>
x=0
</label>
</transition>
<transition>
<source
ref=
"id10"
/>
<target
ref=
"id13"
/>
<label
kind=
"guard"
x=
"200"
y=
"-20"
>
x
>
=2000
</label>
</transition>
<transition>
<source
ref=
"id12"
/>
<target
ref=
"id13"
/>
<label
kind=
"guard"
x=
"200"
y=
"-120"
>
x
>
=2000
</label>
<nail
x=
"300"
y=
"-100"
/>
</transition>
<transition>
<source
ref=
"id13"
/>
<target
ref=
"id14"
/>
<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=
"id14"
/>
<target
ref=
"id15"
/>
<label
kind=
"guard"
x=
"200"
y=
"80"
>
x
>
=200
</label>
</transition>
<transition>
<source
ref=
"id15"
/>
<target
ref=
"id9"
/>
<label
kind=
"synchronisation"
x=
"50"
y=
"80"
>
unlock_M1!
</label>
<nail
x=
"0"
y=
"100"
/>
</transition>
</template>
<template>
<name>
F_t
</name>
<parameter>
urgent chan
&
k_O_F, urgent chan
&
k_P_F, urgent chan
&
lock_M2, urgent chan
&
unlock_M2, urgent chan
&
lock_M3, urgent chan
&
unlock_M3
</parameter>
<declaration>
clock x;
</declaration>
<location
id=
"id16"
x=
"0"
y=
"0"
>
<name
x=
"-20"
y=
"-25"
>
W
</name>
</location>
<location
id=
"id17"
x=
"150"
y=
"0"
>
<name
x=
"130"
y=
"-25"
>
P0
</name>
<label
kind=
"invariant"
x=
"100"
y=
"20"
>
x
<
75
</label>
</location>
<location
id=
"id18"
x=
"150"
y=
"-100"
>
<name
x=
"130"
y=
"-125"
>
P1
</name>
<label
kind=
"invariant"
x=
"100"
y=
"-80"
>
x
<
75
</label>
</location>
<location
id=
"id19"
x=
"300"
y=
"0"
>
</location>
<location
id=
"id20"
x=
"750"
y=
"100"
>
<label
kind=
"invariant"
x=
"700"
y=
"120"
>
x
<
30
</label>
</location>
<location
id=
"id21"
x=
"600"
y=
"100"
>
</location>
<location
id=
"id22"
x=
"450"
y=
"100"
>
</location>
<location
id=
"id23"
x=
"300"
y=
"100"
>
<label
kind=
"invariant"
x=
"250"
y=
"120"
>
x
<
20
</label>
</location>
<location
id=
"id24"
x=
"150"
y=
"100"
>
</location>
<init
ref=
"id16"
/>
<transition>
<source
ref=
"id16"
/>
<target
ref=
"id17"
/>
<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=
"id16"
/>
<target
ref=
"id18"
/>
<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"
/>
</transition>
<transition>
<source
ref=
"id17"
/>
<target
ref=
"id19"
/>
<label
kind=
"guard"
x=
"200"
y=
"-20"
>
x
>
=50
</label>
</transition>
<transition>
<source
ref=
"id18"
/>
<target
ref=
"id19"
/>
<label
kind=
"guard"
x=
"200"
y=
"-120"
>
x
>
=50
</label>
<nail
x=
"300"
y=
"-100"
/>
</transition>
<transition>
<source
ref=
"id19"
/>
<target
ref=
"id20"
/>
<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=
"id20"
/>
<target
ref=
"id21"
/>
<label
kind=
"guard"
x=
"650"
y=
"80"
>
x
>
=20
</label>
</transition>
<transition>
<source
ref=
"id21"
/>
<target
ref=
"id22"
/>
<label
kind=
"synchronisation"
x=
"500"
y=
"80"
>
unlock_M2!
</label>
</transition>
<transition>
<source
ref=
"id22"
/>
<target
ref=
"id23"
/>
<label
kind=
"synchronisation"
x=
"350"
y=
"80"
>
lock_M3!
</label>
<label
kind=
"assignment"
x=
"350"
y=
"110"
>
x=0
</label>
</transition>
<transition>
<source
ref=
"id23"
/>
<target
ref=
"id24"
/>
<label
kind=
"guard"
x=
"200"
y=
"80"
>
x
>
=10
</label>
</transition>
<transition>
<source
ref=
"id24"
/>
<target
ref=
"id16"
/>
<label
kind=
"synchronisation"
x=
"50"
y=
"80"
>
unlock_M3!
</label>
<nail
x=
"0"
y=
"100"
/>
</transition>
</template>
<template>
<name>
M1_t
</name>
<parameter>
urgent chan
&
lock_M1, urgent chan
&
unlock_M1
</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_M1?
</label>
</transition>
<transition>
<source
ref=
"id26"
/>
<target
ref=
"id25"
/>
<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
&
lock_M2, urgent chan
&
unlock_M2
</parameter>
<location
id=
"id27"
x=
"0"
y=
"0"
>
<name
x=
"-20"
y=
"-25"
>
W
</name>
</location>
<location
id=
"id28"
x=
"150"
y=
"0"
>
</location>
<init
ref=
"id27"
/>
<transition>
<source
ref=
"id27"
/>
<target
ref=
"id28"
/>
<label
kind=
"synchronisation"
x=
"50"
y=
"-20"
>
lock_M2?
</label>
</transition>
<transition>
<source
ref=
"id28"
/>
<target
ref=
"id27"
/>
<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
&
lock_M3, urgent chan
&
unlock_M3
</parameter>
<location
id=
"id29"
x=
"0"
y=
"0"
>
<name
x=
"-20"
y=
"-25"
>
W
</name>
</location>
<location
id=
"id30"
x=
"150"
y=
"0"
>
</location>
<init
ref=
"id29"
/>
<transition>
<source
ref=
"id29"
/>
<target
ref=
"id30"
/>
<label
kind=
"synchronisation"
x=
"50"
y=
"-20"
>
lock_M3?
</label>
</transition>
<transition>
<source
ref=
"id30"
/>
<target
ref=
"id29"
/>
<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
&
lock_M1, urgent chan
&
unlock_M1
</parameter>
<declaration>
clock x,y;
</declaration>
<location
id=
"id31"
x=
"0"
y=
"0"
>
<name
x=
"-20"
y=
"-25"
>
W
</name>
</location>
<location
id=
"id32"
x=
"150"
y=
"0"
>
<name
x=
"130"
y=
"-25"
>
M
</name>
<label
kind=
"invariant"
x=
"100"
y=
"20"
>
x
<
310
</label>
</location>
<location
id=
"id33"
x=
"300"
y=
"0"
>
</location>
<location
id=
"id34"
x=
"450"
y=
"0"
>
<name
x=
"430"
y=
"-25"
>
S
</name>
<label
kind=
"invariant"
x=
"400"
y=
"20"
>
x
<
500
</label>
</location>
<init
ref=
"id31"
/>
<transition>
<source
ref=
"id31"
/>
<target
ref=
"id32"
/>
<label
kind=
"synchronisation"
x=
"50"
y=
"-20"
>
lock_M1!
</label>
<label
kind=
"assignment"
x=
"50"
y=
"10"
>
x=0
</label>
</transition>
<transition>
<source
ref=
"id32"
/>
<target
ref=
"id33"
/>
<label
kind=
"guard"
x=
"200"
y=
"-20"
>
x
>
=210
</label>
</transition>
<transition>
<source
ref=
"id33"
/>
<target
ref=
"id34"
/>
<label
kind=
"synchronisation"
x=
"350"
y=
"-20"
>
unlock_M1!
</label>
<label
kind=
"assignment"
x=
"350"
y=
"10"
>
x=0
</label>
</transition>
<transition>
<source
ref=
"id34"
/>
<target
ref=
"id31"
/>
<label
kind=
"guard"
x=
"200"
y=
"80"
>
x
>
=400
</label>
<label
kind=
"assignment"
x=
"204"
y=
"102"
>
y=0
</label>
<nail
x=
"450"
y=
"100"
/>
<nail
x=
"0"
y=
"100"
/>
</transition>
</template>
<template>
<name>
H_t
</name>
<parameter>
urgent chan
&
lock_M2, urgent chan
&
unlock_M2
</parameter>
<declaration>
clock x,y;
</declaration>
<location
id=
"id35"
x=
"0"
y=
"0"
>
<name
x=
"-20"
y=
"-25"
>
W
</name>
</location>
<location
id=
"id36"
x=
"150"
y=
"0"
>
<name
x=
"130"
y=
"-25"
>
M
</name>
<label
kind=
"invariant"
x=
"100"
y=
"20"
>
x
<
30
</label>
</location>
<location
id=
"id37"
x=
"300"
y=
"0"
>
</location>
<location
id=
"id38"
x=
"450"
y=
"0"
>
<name
x=
"430"
y=
"-25"
>
S
</name>
<label
kind=
"invariant"
x=
"400"
y=
"20"
>
x
<
20
</label>
</location>
<init
ref=
"id35"
/>
<transition>
<source
ref=
"id35"
/>
<target
ref=
"id36"
/>
<label
kind=
"synchronisation"
x=
"50"
y=
"-20"
>
lock_M2!
</label>
<label
kind=
"assignment"
x=
"50"
y=
"10"
>
x=0
</label>
</transition>
<transition>
<source
ref=
"id36"
/>
<target
ref=
"id37"
/>
<label
kind=
"guard"
x=
"200"
y=
"-20"
>
x
>
=20
</label>
</transition>
<transition>
<source
ref=
"id37"
/>
<target
ref=
"id38"
/>
<label
kind=
"synchronisation"
x=
"350"
y=
"-20"
>
unlock_M2!
</label>
<label
kind=
"assignment"
x=
"350"
y=
"10"
>
x=0
</label>
</transition>
<transition>
<source
ref=
"id38"
/>
<target
ref=
"id35"
/>
<label
kind=
"guard"
x=
"200"
y=
"80"
>
x
>
=10
</label>
<label
kind=
"assignment"
x=
"204"
y=
"102"
>
y=0
</label>
<nail
x=
"450"
y=
"100"
/>
<nail
x=
"0"
y=
"100"
/>
</transition>
</template>
<template>
<name>
M_t
</name>
<parameter>
urgent chan
&
lock_M3, urgent chan
&
unlock_M3
</parameter>
<declaration>
clock x,y;
</declaration>
<location
id=
"id39"
x=
"0"
y=
"0"
>
<name
x=
"-20"
y=
"-25"
>
W
</name>
</location>
<location
id=
"id40"
x=
"150"
y=
"0"
>
<name
x=
"130"
y=
"-25"
>
M
</name>
<label
kind=
"invariant"
x=
"100"
y=
"20"
>
x
<
20
</label>
</location>
<location
id=
"id41"
x=
"300"
y=
"0"
>
</location>
<location
id=
"id42"
x=
"450"
y=
"0"
>
<name
x=
"430"
y=
"-25"
>
S
</name>
<label
kind=
"invariant"
x=
"400"
y=
"20"
>
x
<
20
</label>
</location>
<init
ref=
"id39"
/>
<transition>
<source
ref=
"id39"
/>
<target
ref=
"id40"
/>
<label
kind=
"synchronisation"
x=
"50"
y=
"-20"
>
lock_M3!
</label>
<label
kind=
"assignment"
x=
"50"
y=
"10"
>
x=0
</label>
</transition>
<transition>
<source
ref=
"id40"
/>
<target
ref=
"id41"
/>
<label
kind=
"guard"
x=
"200"
y=
"-20"
>
x
>
=10
</label>
</transition>
<transition>
<source
ref=
"id41"
/>
<target
ref=
"id42"
/>
<label
kind=
"synchronisation"
x=
"350"
y=
"-20"
>
unlock_M3!
</label>
<label
kind=
"assignment"
x=
"350"
y=
"10"
>
x=0
</label>
</transition>
<transition>
<source
ref=
"id42"
/>
<target
ref=
"id39"
/>
<label
kind=
"guard"
x=
"200"
y=
"80"
>
x
>
=10
</label>
<label
kind=
"assignment"
x=
"204"
y=
"102"
>
y=0
</label>
<nail
x=
"450"
y=
"100"
/>
<nail
x=
"0"
y=
"100"
/>
</transition>
</template>
<system>
urgent chan k_C_Pr;
urgent chan k_O_Pr;
urgent chan k_O_F;
urgent chan k_P_F;
urgent chan lock_M1;
urgent chan unlock_M1;
urgent chan lock_M2;
urgent chan unlock_M2;
urgent chan lock_M3;
urgent chan unlock_M3;
C = C_t(k_C_Pr);
O = O_t(k_O_Pr, k_O_F);
P = P_t(k_P_F);
Pr = Pr_t(k_C_Pr, k_O_Pr, lock_M1, unlock_M1);
F = F_t(k_O_F, k_P_F, lock_M2, unlock_M2, lock_M3, unlock_M3);
M1 = M1_t(lock_M1, unlock_M1);
M2 = M2_t(lock_M2, unlock_M2);
M3 = M3_t(lock_M3, unlock_M3);
G = G_t(lock_M1, unlock_M1);
H = H_t(lock_M2, unlock_M2);
M = M_t(lock_M3, unlock_M3);
system C, O, P, Pr, F, M1, M2, M3, G, H, M;
</system>
</nta>
Please
register
or
login
to post a comment