|
@@ -0,0 +1,170 @@
|
|
|
+<?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_2.dtd'>
|
|
|
+<nta>
|
|
|
+ <declaration>/*
|
|
|
+OR - 2019
|
|
|
+ */
|
|
|
+
|
|
|
+const int NAB = 3; // # trains
|
|
|
+const int NBA = 3;
|
|
|
+const int N = 6;
|
|
|
+
|
|
|
+typedef int[0,NAB-1] id_tAB;
|
|
|
+typedef int[0,NBA-1] id_tBA;
|
|
|
+
|
|
|
+int ab=0, ba=0;
|
|
|
+
|
|
|
+chan accesAB[NAB], accesBA[NBA], libAB[NAB], libBA[NBA];
|
|
|
+
|
|
|
+</declaration>
|
|
|
+ <template>
|
|
|
+ <name>TrainBA</name>
|
|
|
+ <parameter>const id_tBA id</parameter>
|
|
|
+ <declaration>clock x;</declaration>
|
|
|
+ <location id="id0" x="-51" y="0">
|
|
|
+ <name x="-59" y="17">A</name>
|
|
|
+ </location>
|
|
|
+ <location id="id1" x="102" y="0">
|
|
|
+ <name x="102" y="17">BA</name>
|
|
|
+ <label kind="invariant" x="119" y="0">x<=10</label>
|
|
|
+ </location>
|
|
|
+ <location id="id2" x="102" y="-127">
|
|
|
+ <name x="92" y="-161">B</name>
|
|
|
+ </location>
|
|
|
+ <location id="id3" x="-51" y="-127">
|
|
|
+ <name x="-61" y="-161">Safe</name>
|
|
|
+ </location>
|
|
|
+ <init ref="id3"/>
|
|
|
+ <transition>
|
|
|
+ <source ref="id0"/>
|
|
|
+ <target ref="id3"/>
|
|
|
+ <label kind="synchronisation" x="-51" y="-80">libBA[id] !</label>
|
|
|
+ </transition>
|
|
|
+ <transition>
|
|
|
+ <source ref="id1"/>
|
|
|
+ <target ref="id0"/>
|
|
|
+ </transition>
|
|
|
+ <transition>
|
|
|
+ <source ref="id2"/>
|
|
|
+ <target ref="id1"/>
|
|
|
+ <label kind="synchronisation" x="102" y="-80">accesBA[id] ?</label>
|
|
|
+ <label kind="assignment" x="102" y="-63">x:=0</label>
|
|
|
+ </transition>
|
|
|
+ <transition>
|
|
|
+ <source ref="id3"/>
|
|
|
+ <target ref="id2"/>
|
|
|
+ </transition>
|
|
|
+ </template>
|
|
|
+ <template>
|
|
|
+ <name x="40" y="16">TrainAB</name>
|
|
|
+ <parameter>const id_tAB id</parameter>
|
|
|
+ <declaration>clock x;</declaration>
|
|
|
+ <location id="id4" x="96" y="96">
|
|
|
+ <name x="48" y="80">Safe</name>
|
|
|
+ </location>
|
|
|
+ <location id="id5" x="256" y="96">
|
|
|
+ <name x="272" y="80">A</name>
|
|
|
+ </location>
|
|
|
+ <location id="id6" x="96" y="232">
|
|
|
+ <name x="32" y="216">B</name>
|
|
|
+ </location>
|
|
|
+ <location id="id7" x="256" y="232">
|
|
|
+ <name x="272" y="216">AB</name>
|
|
|
+ <label kind="invariant" x="246" y="249">x<=10</label>
|
|
|
+ </location>
|
|
|
+ <init ref="id4"/>
|
|
|
+ <transition>
|
|
|
+ <source ref="id6"/>
|
|
|
+ <target ref="id4"/>
|
|
|
+ <label kind="synchronisation" x="96" y="147">libAB[id] !</label>
|
|
|
+ </transition>
|
|
|
+ <transition>
|
|
|
+ <source ref="id7"/>
|
|
|
+ <target ref="id6"/>
|
|
|
+ </transition>
|
|
|
+ <transition>
|
|
|
+ <source ref="id5"/>
|
|
|
+ <target ref="id7"/>
|
|
|
+ <label kind="synchronisation" x="256" y="147">accesAB[id] ?</label>
|
|
|
+ <label kind="assignment" x="256" y="164">x:=0</label>
|
|
|
+ </transition>
|
|
|
+ <transition>
|
|
|
+ <source ref="id4"/>
|
|
|
+ <target ref="id5"/>
|
|
|
+ </transition>
|
|
|
+ </template>
|
|
|
+ <template>
|
|
|
+ <name x="40" y="16">CTRL</name>
|
|
|
+ <declaration>id_tAB list[N+1];
|
|
|
+int[0,N] len;
|
|
|
+
|
|
|
+// Put an element at the end of the queue
|
|
|
+void enqueue(id_tAB element)
|
|
|
+{
|
|
|
+ list[len++] = element;
|
|
|
+}
|
|
|
+
|
|
|
+// Remove the front element of the queue
|
|
|
+void dequeue()
|
|
|
+{
|
|
|
+ int i = 0;
|
|
|
+ len -= 1;
|
|
|
+ while (i < len)
|
|
|
+ {
|
|
|
+ list[i] = list[i + 1];
|
|
|
+ i++;
|
|
|
+ }
|
|
|
+ list[i] = 0;
|
|
|
+}
|
|
|
+
|
|
|
+// Returns the front element of the queue
|
|
|
+id_tAB front()
|
|
|
+{
|
|
|
+ return list[0];
|
|
|
+}
|
|
|
+
|
|
|
+// Returns the last element of the queue
|
|
|
+id_tAB tail()
|
|
|
+{
|
|
|
+ return list[len - 1];
|
|
|
+}</declaration>
|
|
|
+ <location id="id8" x="246" y="127">
|
|
|
+ <name x="229" y="85">Free</name>
|
|
|
+ </location>
|
|
|
+ <init ref="id8"/>
|
|
|
+ </template>
|
|
|
+ <system>system TrainAB, TrainBA, CTRL;
|
|
|
+</system>
|
|
|
+ <queries>
|
|
|
+ <query>
|
|
|
+ <formula>E<> TrainBA(1).BA
|
|
|
+ </formula>
|
|
|
+ <comment>
|
|
|
+ </comment>
|
|
|
+ </query>
|
|
|
+ <query>
|
|
|
+ <formula>A[] forall (i : id_tBA) forall (j : id_tAB) TrainBA(i).BA && TrainAB(j).AB imply i == j
|
|
|
+ </formula>
|
|
|
+ <comment>
|
|
|
+ </comment>
|
|
|
+ </query>
|
|
|
+ <query>
|
|
|
+ <formula>TrainBA(1).B --> TrainBA(1).BA
|
|
|
+ </formula>
|
|
|
+ <comment>
|
|
|
+ </comment>
|
|
|
+ </query>
|
|
|
+ <query>
|
|
|
+ <formula>A<> TrainBA(1).BA
|
|
|
+ </formula>
|
|
|
+ <comment>
|
|
|
+ </comment>
|
|
|
+ </query>
|
|
|
+ <query>
|
|
|
+ <formula>E<> TrainBA(1).BA & TrainBA(2).BA
|
|
|
+ </formula>
|
|
|
+ <comment>
|
|
|
+ </comment>
|
|
|
+ </query>
|
|
|
+ </queries>
|
|
|
+</nta>
|