summaryrefslogtreecommitdiffstats
path: root/test/w3c/promela/test242.scxml
diff options
context:
space:
mode:
authorStefan Radomski <radomski@tk.informatik.tu-darmstadt.de>2014-12-01 11:02:40 (GMT)
committerStefan Radomski <radomski@tk.informatik.tu-darmstadt.de>2014-12-01 11:02:40 (GMT)
commitaf6609592298c5e047e37e5ae2b47e6a8edbb677 (patch)
treee6e7da1cd34dccf3fb4f389e684b7c899b12987a /test/w3c/promela/test242.scxml
parentd2e90c02e5ad19a5857e7c7fb87f248182fdb32d (diff)
downloaduscxml-af6609592298c5e047e37e5ae2b47e6a8edbb677.zip
uscxml-af6609592298c5e047e37e5ae2b47e6a8edbb677.tar.gz
uscxml-af6609592298c5e047e37e5ae2b47e6a8edbb677.tar.bz2
Nested invokers and delayed events for PROMELA model checking
Diffstat (limited to 'test/w3c/promela/test242.scxml')
-rw-r--r--test/w3c/promela/test242.scxml97
1 files changed, 47 insertions, 50 deletions
diff --git a/test/w3c/promela/test242.scxml b/test/w3c/promela/test242.scxml
index 01ea8d0..c887bcf 100644
--- a/test/w3c/promela/test242.scxml
+++ b/test/w3c/promela/test242.scxml
@@ -1,56 +1,53 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<!-- test that markup specified by 'src' and by <content> is treated the same way. That means that
-either we get done.invoke in both cases or in neither case (in which case we timeout) -->
-<scxml xmlns="http://www.w3.org/2005/07/scxml" xmlns:conf="http://www.w3.org/2005/scxml-conformance" initial="s0" version="1.0" datamodel="promela">
- <state id="s0">
- <onentry>
- <send event="timeout1" delay="1s"/>
+<?xml version="1.0" encoding="UTF-8"?><!-- test that markup specified by 'src' and by <content> is treated the same way. That means that
+either we get done.invoke in both cases or in neither case (in which case we timeout) --><scxml xmlns="http://www.w3.org/2005/07/scxml" xmlns:conf="http://www.w3.org/2005/scxml-conformance" initial="s0" version="1.0" datamodel="promela">
+
+
+<state id="s0">
+ <onentry>
+ <send xmlns:scxml="http://www.w3.org/2005/07/scxml" delay="1000" event="timeout"/>
</onentry>
<transition event="timeout" target="fail"/>
- <invoke type="http://www.w3.org/TR/scxml/" src="file:test242sub1.scxml"/>
- <transition event="done.invoke" target="s02"/>
- <transition event="timeout1" target="s03"/>
- </state>
- <state id="s02">
- <onentry>
- <send event="timeout2" delay="1s"/>
- </onentry>
- <invoke type="http://www.w3.org/TR/scxml/">
- <!-- identical to test242sub1.scxml. -->
- <content>
- <scxml version="1.0" initial="subFinal1" datamodel="promela">
- <final id="subFinal1"/>
- </scxml>
- </content>
- </invoke>
- <!-- we got done.invoke last time, so we need it this time too -->
- <transition event="done.invoke" target="pass"/>
- <transition event="timeout2" target="fail"/>
- </state>
- <state id="s03">
- <onentry>
- <send event="timeout3" delay="1s"/>
- </onentry>
- <invoke type="http://www.w3.org/TR/scxml/">
- <!-- identical to test242sub1.scxml. -->
- <content>
- <scxml version="1.0" initial="subFinal2" datamodel="promela">
- <final id="subFinal2"/>
- </scxml>
- </content>
- </invoke>
- <!-- we got timeout last time, so we need it this time too -->
- <transition event="timeout3" target="pass"/>
- <transition event="done.invoke" target="fail"/>
- </state>
- <final xmlns:scxml="http://www.w3.org/2005/07/scxml" id="pass">
+
+ <invoke type="http://www.w3.org/TR/scxml/" src="file:test242sub1.scxml"/>
+ <transition event="done.invoke" target="s02"/>
+ <transition event="timeout1" target="s03"/>
+ </state>
+
+<state id="s02">
<onentry>
- <log label="Outcome" expr="'pass'"/>
+ <send xmlns:scxml="http://www.w3.org/2005/07/scxml" delay="1000" event="timeout"/>
</onentry>
- </final>
- <final xmlns:scxml="http://www.w3.org/2005/07/scxml" id="fail">
+ <invoke type="http://www.w3.org/TR/scxml/">
+ <!-- identical to test242sub1.scxml. -->
+ <content>
+ <scxml version="1.0" initial="subFinal1" datamodel="promela">
+ <final id="subFinal1"/>
+ </scxml>
+ </content>
+ </invoke>
+ <!-- we got done.invoke last time, so we need it this time too -->
+ <transition event="done.invoke" target="pass"/>
+ <transition event="timeout2" target="fail"/>
+ </state>
+
+<state id="s03">
<onentry>
- <log label="Outcome" expr="'fail'"/>
+ <send xmlns:scxml="http://www.w3.org/2005/07/scxml" delay="1000" event="timeout"/>
</onentry>
- </final>
-</scxml>
+ <invoke type="http://www.w3.org/TR/scxml/">
+ <!-- identical to test242sub1.scxml. -->
+ <content>
+ <scxml version="1.0" initial="subFinal2" datamodel="promela">
+ <final id="subFinal2"/>
+ </scxml>
+ </content>
+ </invoke>
+ <!-- we got timeout last time, so we need it this time too -->
+ <transition event="timeout3" target="pass"/>
+ <transition event="done.invoke" target="fail"/>
+ </state>
+
+
+<final xmlns:scxml="http://www.w3.org/2005/07/scxml" id="pass"><onentry><log label="Outcome" expr="'pass'"/></onentry></final>
+<final xmlns:scxml="http://www.w3.org/2005/07/scxml" id="fail"><onentry><log label="Outcome" expr="'fail'"/></onentry></final>
+</scxml> \ No newline at end of file