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 16:04:03 +0000
Browse Files
Options
Browse Files
Download
Email Patches
Plain Diff
Commit
b49bb19c6029254be3e3bf0aa8f6ade08e77789d
b49bb19c
1 parent
e96a2df9
Upload new file
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
228 additions
and
0 deletions
Ex3/Uppaal/Ex3_1.1.xml
Ex3/Uppaal/Ex3_1.1.xml
0 → 100644
View file @
b49bb19
<?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
</parameter>
<declaration>
clock x,y;
</declaration>
<location
id=
"id9"
x=
"289"
y=
"119"
>
</location>
<location
id=
"id10"
x=
"289"
y=
"0"
>
<name
x=
"272"
y=
"-34"
>
Q
</name>
<urgent/>
</location>
<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"
>
P
</name>
<label
kind=
"invariant"
x=
"100"
y=
"20"
>
x
<
3000
</label>
</location>
<location
id=
"id13"
x=
"0"
y=
"-100"
>
<name
x=
"-20"
y=
"-125"
>
W2
</name>
</location>
<init
ref=
"id11"
/>
<transition>
<source
ref=
"id10"
/>
<target
ref=
"id9"
/>
</transition>
<transition>
<source
ref=
"id9"
/>
<target
ref=
"id11"
/>
<label
kind=
"assignment"
x=
"110"
y=
"127"
>
y=0
</label>
<nail
x=
"0"
y=
"119"
/>
</transition>
<transition>
<source
ref=
"id11"
/>
<target
ref=
"id12"
/>
<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=
"id11"
/>
<target
ref=
"id13"
/>
<label
kind=
"synchronisation"
x=
"-50"
y=
"-60"
>
k_O_Pr?
</label>
</transition>
<transition>
<source
ref=
"id13"
/>
<target
ref=
"id12"
/>
<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=
"id12"
/>
<target
ref=
"id10"
/>
<label
kind=
"guard"
x=
"200"
y=
"-20"
>
x
>
=2000
</label>
</transition>
</template>
<template>
<name>
F_t
</name>
<parameter>
urgent chan
&
k_O_F, urgent chan
&
k_P_F
</parameter>
<declaration>
clock x,y;
</declaration>
<location
id=
"id14"
x=
"306"
y=
"127"
>
</location>
<location
id=
"id15"
x=
"306"
y=
"0"
>
<name
x=
"280"
y=
"-26"
>
Q
</name>
<urgent/>
</location>
<location
id=
"id16"
x=
"0"
y=
"0"
>
<name
x=
"-20"
y=
"-25"
>
W
</name>
</location>
<location
id=
"id17"
x=
"153"
y=
"0"
>
<name
x=
"133"
y=
"-25"
>
P
</name>
<label
kind=
"invariant"
x=
"103"
y=
"20"
>
x
<
75
</label>
</location>
<init
ref=
"id16"
/>
<transition>
<source
ref=
"id15"
/>
<target
ref=
"id14"
/>
</transition>
<transition>
<source
ref=
"id14"
/>
<target
ref=
"id16"
/>
<label
kind=
"assignment"
x=
"119"
y=
"136"
>
y=0
</label>
<nail
x=
"0"
y=
"127"
/>
</transition>
<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=
"id17"
/>
<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=
"id17"
/>
<target
ref=
"id15"
/>
<label
kind=
"guard"
x=
"200"
y=
"-20"
>
x
>
=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>
Please
register
or
login
to post a comment