repositories
/
mc1516the.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
53484c4
)
2.xml voor prop weight op RedCar
author
pimjager
<pim@pimjager.nl>
Thu, 16 Jun 2016 09:28:08 +0000
(11:28 +0200)
committer
pimjager
<pim@pimjager.nl>
Thu, 16 Jun 2016 09:28:08 +0000
(11:28 +0200)
uppaal/2.xml
patch
|
blob
|
history
diff --git
a/uppaal/2.xml
b/uppaal/2.xml
index
29e4e8f
..
e45b155
100644
(file)
--- a/
uppaal/2.xml
+++ b/
uppaal/2.xml
@@
-3,11
+3,13
@@
<nta>
\r
<declaration>// Place global declarations here.
// Intermediate
<nta>
\r
<declaration>// Place global declarations here.
// Intermediate
-
const int N =
13;
+
//const int N=
13;
// Advanced
// Advanced
-//const int N = 7
+//const int N = 7;
+//easy test puzzle
+const int N=3;
-typedef int[0,N-1] id_c;
+typedef int[0,
N-1] id_c;
broadcast chan up[N], down[N], left[N], right[N], start, leftRed, rightRed;
broadcast chan up[N], down[N], left[N], right[N], start, leftRed, rightRed;
@@
-48,7
+50,7
@@
void register() {
<source ref="id2"/>
\r
<target ref="id2"/>
\r
<label kind="guard" x="-280" y="8">x>0 && !grid[x-1][y]</label>
\r
<source ref="id2"/>
\r
<target ref="id2"/>
\r
<label kind="guard" x="-280" y="8">x>0 && !grid[x-1][y]</label>
\r
- <label kind="synchronisation" x="-246" y="102">
down
[id]!</label>
\r
+ <label kind="synchronisation" x="-246" y="102">
left
[id]!</label>
\r
<label kind="assignment" x="-340" y="34">grid[x+length-1][y]:=false,
grid[x-1][y]:=true,
x:=x-1</label>
\r
<label kind="assignment" x="-340" y="34">grid[x+length-1][y]:=false,
grid[x-1][y]:=true,
x:=x-1</label>
\r
@@
-59,7
+61,7
@@
x:=x-1</label>
<source ref="id2"/>
\r
<target ref="id2"/>
\r
<label kind="guard" x="-306" y="-263">x+length < 6 && !grid[x+length][y]</label>
\r
<source ref="id2"/>
\r
<target ref="id2"/>
\r
<label kind="guard" x="-306" y="-263">x+length < 6 && !grid[x+length][y]</label>
\r
- <label kind="synchronisation" x="-221" y="-204">
up
[id]!</label>
\r
+ <label kind="synchronisation" x="-221" y="-204">
right
[id]!</label>
\r
<label kind="assignment" x="-331" y="-229">grid[x][y]:=false,
grid[x+length][y]:=true,
x:=x+1</label>
\r
<label kind="assignment" x="-331" y="-229">grid[x][y]:=false,
grid[x+length][y]:=true,
x:=x+1</label>
\r
@@
-102,7
+104,7
@@
x:=x+1</label>
<source ref="id5"/>
\r
<target ref="id5"/>
\r
<label kind="guard" x="-170" y="153">y>0 && !grid[x][y-1]</label>
\r
<source ref="id5"/>
\r
<target ref="id5"/>
\r
<label kind="guard" x="-170" y="153">y>0 && !grid[x][y-1]</label>
\r
- <label kind="synchronisation" x="-119" y="119">
left
[id]!</label>
\r
+ <label kind="synchronisation" x="-119" y="119">
down
[id]!</label>
\r
<label kind="assignment" x="-221" y="51">grid[x][y-1]:=true,
grid[x][y+length-1]:=true,
y:=y-1</label>
\r
<label kind="assignment" x="-221" y="51">grid[x][y-1]:=true,
grid[x][y+length-1]:=true,
y:=y-1</label>
\r
@@
-113,7
+115,7
@@
y:=y-1</label>
<source ref="id5"/>
\r
<target ref="id5"/>
\r
<label kind="guard" x="-204" y="-221">y+length < 6 && !grid[x][y+length]</label>
\r
<source ref="id5"/>
\r
<target ref="id5"/>
\r
<label kind="guard" x="-204" y="-221">y+length < 6 && !grid[x][y+length]</label>
\r
- <label kind="synchronisation" x="-127" y="-195">
right
[id]!</label>
\r
+ <label kind="synchronisation" x="-127" y="-195">
up
[id]!</label>
\r
<label kind="assignment" x="-263" y="-161">grid[x][y+length]:=true,
grid[x][y]:=false,
y:=y+1</label>
\r
<label kind="assignment" x="-263" y="-161">grid[x][y+length]:=true,
grid[x][y]:=false,
y:=y+1</label>
\r
@@
-161,26
+163,56
@@
bool done = 0;</declaration>
grid[x][3] = true;
grid[x+1][3] = true;
}</declaration>
\r
grid[x][3] = true;
grid[x+1][3] = true;
}</declaration>
\r
- <location id="id9" x="493" y="-51">
\r
+ <location id="id9" x="238" y="34">
\r
+ <urgent/>
\r
+ </location>
\r
+ <location id="id10" x="221" y="-153">
\r
+ <urgent/>
\r
</location>
\r
</location>
\r
- <location id="id1
0" x="51" y="-59
">
\r
+ <location id="id1
1" x="493" y="-51
">
\r
</location>
\r
</location>
\r
- <location id="id1
1" x="-93" y="-68
">
\r
+ <location id="id1
2" x="51" y="-59
">
\r
</location>
\r
</location>
\r
- <location id="id12" x="-204" y="-68">
\r
+ <location id="id13" x="-93" y="-68">
\r
+ </location>
\r
+ <location id="id14" x="-204" y="-68">
\r
<urgent/>
\r
</location>
\r
<urgent/>
\r
</location>
\r
- <init ref="id12"/>
\r
+ <branchpoint id="id15" x="187" y="-85">
\r
+ </branchpoint>
\r
+ <init ref="id14"/>
\r
<transition>
\r
<source ref="id10"/>
\r
<transition>
\r
<source ref="id10"/>
\r
+ <target ref="id12"/>
\r
+ </transition>
\r
+ <transition>
\r
+ <source ref="id9"/>
\r
+ <target ref="id12"/>
\r
+ </transition>
\r
+ <transition>
\r
+ <source ref="id15"/>
\r
<target ref="id9"/>
\r
<target ref="id9"/>
\r
+ <label kind="probability" x="212" y="-25">1</label>
\r
+ </transition>
\r
+ <transition>
\r
+ <source ref="id15"/>
\r
+ <target ref="id10"/>
\r
+ <label kind="probability" x="204" y="-119">3</label>
\r
+ </transition>
\r
+ <transition>
\r
+ <source ref="id12"/>
\r
+ <target ref="id15"/>
\r
+ </transition>
\r
+ <transition>
\r
+ <source ref="id12"/>
\r
+ <target ref="id11"/>
\r
<label kind="guard" x="416" y="-93">x == 4</label>
\r
<label kind="synchronisation" x="416" y="-76">finish!</label>
\r
</transition>
\r
<transition>
\r
<label kind="guard" x="416" y="-93">x == 4</label>
\r
<label kind="synchronisation" x="416" y="-76">finish!</label>
\r
</transition>
\r
<transition>
\r
- <source ref="id1
0
"/>
\r
- <target ref="id1
0
"/>
\r
- <label kind="guard" x="0" y="161">x > 0 && grid[x-1][3]</label>
\r
+ <source ref="id1
2
"/>
\r
+ <target ref="id1
2
"/>
\r
+ <label kind="guard" x="0" y="161">x > 0 &&
!
grid[x-1][3]</label>
\r
<label kind="synchronisation" x="25" y="119">leftRed!</label>
\r
<label kind="assignment" x="-85" y="85">grid[x+1][3]:=false,
grid[x-1][3]:=true,
<label kind="synchronisation" x="25" y="119">leftRed!</label>
\r
<label kind="assignment" x="-85" y="85">grid[x+1][3]:=false,
grid[x-1][3]:=true,
@@
-189,31
+221,40
@@
x:=x-1</label>
<nail x="178" y="51"/>
\r
</transition>
\r
<transition>
\r
<nail x="178" y="51"/>
\r
</transition>
\r
<transition>
\r
- <source ref="id1
0
"/>
\r
- <target ref="id1
0
"/>
\r
- <label kind="guard" x="-17" y="-255">x+2 < 6 && grid[x+2][3]</label>
\r
+ <source ref="id1
2
"/>
\r
+ <target ref="id1
2
"/>
\r
+ <label kind="guard" x="-17" y="-255">x+2 < 6 &&
!
grid[x+2][3]</label>
\r
<label kind="synchronisation" x="25" y="-221">rightRed!</label>
\r
<label kind="synchronisation" x="25" y="-221">rightRed!</label>
\r
- <label kind="assignment" x="-85" y="-187">grid[x
-1
][3]:=false,
+ <label kind="assignment" x="-85" y="-187">grid[x][3]:=false,
grid[x+2][3]:=true,
x:=x+1</label>
\r
<nail x="-17" y="-144"/>
\r
<nail x="144" y="-136"/>
\r
</transition>
\r
<transition>
\r
grid[x+2][3]:=true,
x:=x+1</label>
\r
<nail x="-17" y="-144"/>
\r
<nail x="144" y="-136"/>
\r
</transition>
\r
<transition>
\r
- <source ref="id1
1
"/>
\r
- <target ref="id1
0
"/>
\r
+ <source ref="id1
3
"/>
\r
+ <target ref="id1
2
"/>
\r
<label kind="synchronisation" x="-75" y="-80">start?</label>
\r
</transition>
\r
<transition>
\r
<label kind="synchronisation" x="-75" y="-80">start?</label>
\r
</transition>
\r
<transition>
\r
- <source ref="id1
2
"/>
\r
- <target ref="id1
1
"/>
\r
+ <source ref="id1
4
"/>
\r
+ <target ref="id1
3
"/>
\r
<label kind="synchronisation" x="-186" y="-85">reg!</label>
\r
<label kind="assignment" x="-186" y="-68">register()</label>
\r
</transition>
\r
</template>
\r
<system>// Place template instantiations here.
<label kind="synchronisation" x="-186" y="-85">reg!</label>
\r
<label kind="assignment" x="-186" y="-68">register()</label>
\r
</transition>
\r
</template>
\r
<system>// Place template instantiations here.
+
+
+//easy test puzzle
+RED = RedCar(0,2);
+V1 = VertCar(2, 1, 4, 3);
+V2 = VertCar(3, 2, 5, 2);
+system RED, V1, V2, Player;
+
// Intermediate puzzle
// Intermediate puzzle
+/*
H1 = HorzCar(2, 0, 0, 5);
H2 = HorzCar(2, 1, 2, 5);
V3 = VertCar(2, 2, 4, 4);
H1 = HorzCar(2, 0, 0, 5);
H2 = HorzCar(2, 1, 2, 5);
V3 = VertCar(2, 2, 4, 4);
@@
-221,13
+262,14
@@
V4 = VertCar(2, 3, 2, 3);
V5 = VertCar(3, 4, 5, 2);
V6 = VertCar(2, 5, 1, 3);
H7 = HorzCar(2, 6, 3, 4);
V5 = VertCar(3, 4, 5, 2);
V6 = VertCar(2, 5, 1, 3);
H7 = HorzCar(2, 6, 3, 4);
-
H8
= RedCar(7, 2); //RED
+
RED
= RedCar(7, 2); //RED
V9 = VertCar(3, 8, 0, 0);
HA = HorzCar(2, 9, 1, 0);
VB = VertCar(2, 10, 3, 0);
HC = HorzCar(2, 11, 4, 1);
HD = HorzCar(2, 12, 4, 0);
V9 = VertCar(3, 8, 0, 0);
HA = HorzCar(2, 9, 1, 0);
VB = VertCar(2, 10, 3, 0);
HC = HorzCar(2, 11, 4, 1);
HD = HorzCar(2, 12, 4, 0);
-system H1, H2, V3, V4, V5, V6, H7, H8, V9, HA, VB, HC, HD, Player;
+system H1, H2, V3, V4, V5, V6, H7, RED, V9, HA, VB, HC, HD, Player;
+*/
// Advanced puzzle
/*
// Advanced puzzle
/*
@@
-240,9
+282,6
@@
H6 = HorzCar(3, 5, 1, 2);
H7 = HorzCar(3, 6, 3, 0);
system H1, V2, V3, V4, H5, H6, H7
*/
H7 = HorzCar(3, 6, 3, 0);
system H1, V2, V3, V4, H5, H6, H7
*/
-
-// List one or more processes to be composed into a system.
-
</system>
\r
<queries>
\r
<query>
\r
</system>
\r
<queries>
\r
<query>
\r