[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[certi-cvs] certi/doc CERTI-tickHandling.xml
From: |
certi-cvs |
Subject: |
[certi-cvs] certi/doc CERTI-tickHandling.xml |
Date: |
Mon, 16 Aug 2010 06:17:19 +0000 |
CVSROOT: /sources/certi
Module name: certi
Changes by: Eric NOULARD <erk> 10/08/16 06:17:19
Added files:
doc : CERTI-tickHandling.xml
Log message:
Beginning (unfinished) UPPAAL model for investigating tick handling
CVSWeb URLs:
http://cvs.savannah.gnu.org/viewcvs/certi/doc/CERTI-tickHandling.xml?cvsroot=certi&rev=1.1
Patches:
Index: CERTI-tickHandling.xml
===================================================================
RCS file: CERTI-tickHandling.xml
diff -N CERTI-tickHandling.xml
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ CERTI-tickHandling.xml 16 Aug 2010 06:17:19 -0000 1.1
@@ -0,0 +1,21 @@
+<?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>//
Place global declarations here.
+const int nbFederate = 2;
+typedef int[0,nbFederate-1] RangeFederate;
+
+chan rq[RangeFederate];
+chan rqNext[RangeFederate];
+chan rqStop[RangeFederate];</declaration><template><name x="5"
y="5">RTIA_Tick</name><parameter>int FedRank</parameter><declaration>// Place
local declarations here.
+bool multiple=false;
+bool result=false;
+
+int timeout =0; // 0 means timeout is not used
+int maxTicks=0; // 0 means maxTicks is not used
+
+</declaration><location id="id0" x="0" y="-464"><name x="-42"
y="-494">TICK_NEXT</name></location><location id="id1" x="-352" y="-160"><name
x="-408" y="-136">TICK_CALLBACK</name></location><location id="id2" x="-320"
y="-480"><name x="-376" y="-512">TICK_BLOCKING</name></location><location
id="id3" x="8" y="-168"><name x="-30"
y="-130">TICK_RETURN</name></location><location id="id4" x="-600"
y="-296"><name x="-632" y="-328">NO_TICK</name></location><init
ref="id4"/><transition><source ref="id0"/><target ref="id3"/><label
kind="guard" x="8"
y="-336">!(result==true)</label></transition><transition><source
ref="id0"/><target ref="id1"/><label kind="guard" x="-168"
y="-416">result==true</label></transition><transition><source
ref="id2"/><target ref="id3"/></transition><transition><source
ref="id1"/><target ref="id3"/></transition><transition><source
ref="id4"/><target ref="id1"/><label kind="synchronisation" x="-552"
y="-232">rq[FedRank]?</label><label kind="assignment" x="-544"
y="-208">result=false</label></transition><transition><source
ref="id4"/><target ref="id2"/><label kind="synchronisation" x="-552"
y="-416">rq[FedRank]?</label><label kind="assignment" x="-552"
y="-432">result=false</label></transition></template><template><name>Request</name><declaration>bool
multiple;
+int minTickTime;
+int maxTickTime;</declaration><location id="id5" x="0" y="0"></location><init
ref="id5"/></template><template><name>RequestNext</name><location id="id6"
x="0" y="0"></location><init
ref="id6"/></template><template><name>RequestStop</name><location id="id7"
x="0" y="0"></location><init ref="id7"/></template><system>// Place template
instantiations here.
+RTIA_Tick1 = RTIA_Tick(1);
+RTIA_Tick2 = RTIA_Tick(2);
+
+// List one or more processes to be composed into a system.
+system RTIA_Tick1, RTIA_Tick2, Request, RequestNext,
RequestStop;</system></nta>
\ No newline at end of file
[Prev in Thread] |
Current Thread |
[Next in Thread] |
- [certi-cvs] certi/doc CERTI-tickHandling.xml,
certi-cvs <=