Worked on PROMELA transformation

9 files changed, 454 insertions, 0 deletions

diff --git a/test/uscxml/promela/test-complete.scxml b/test/uscxml/promela/test-complete.scxml
new file mode 100644
index 0000000..a96152b
--- /dev/null
+++ b/test/uscxml/promela/test-complete.scxml
@@ -0,0 +1,154 @@
+<scxml datamodel="promela">
+
+  <datamodel>
+    <data id="foreachArray1" type="int[3]">[1,2,3]</data>
+    <data id="parallelVar1" type="int" expr="0"/>
+    <data id="ifVar1">{ foo: 1, bar: 'baz' }</data>
+    <data id="counter">{ itemSum: 0, indexSum: 0 }</data>
+    <data id="sendVar1" type="int" expr="4"/>
+    <data id="histVar1" type="int">0</data>
+    <data id="finalizeVar1" type="int">0</data>
+  </datamodel>
+
+  <state id="s0">
+    <history id="s0.h0" type="deep" />
+    <parallel id="p0">
+      <state id="p0.s0">
+        <state id="p0.s0.s0">
+          <onentry>
+            <if cond="ifVar1.foo == 3">
+              <log label="if choosen" />
+              <log label="ifVar1.bar is" expr="ifVar1.bar" />
+              <foreach array="foreachArray1" 
+                       item="foreachItem1" 
+                       index="foreachIndex1">
+                <script>
+                  counter.indexSum = counter.indexSum + foreachIndex1;
+                  counter.itemSum = counter.itemSum + foreachItem1;
+                </script>
+                <log label="foreach counter.indexSum is" 
+                     expr="counter.indexSum" />
+                <log label="foreach counter.itemSum is" 
+                     expr="counter.itemSum" />
+              </foreach>
+              <raise event="if.choosen" />
+            <elseif cond="ifVar1.bar == 'baz'" />
+              <log label="elseif choosen" />
+              <log label="ifVar1.bar is" expr="ifVar1.bar" />
+              <assign location="ifVar1.foo" expr="3" />
+              <send event="elseif.choosen" namelist="sendVar1">
+                <param name="foo" expr="sendVar1 + 16" />
+                <param name="bar" expr="'a string literal'" />
+              </send>
+            <else />
+              <log label="else choosen" />
+              <log label="ifVar1.foo is" expr="ifVar1.foo" />
+              <log label="ifVar1.bar is" expr="ifVar1.bar" />
+              <raise event="else.choosen" />
+            </if>
+            <script>parallelVar1++</script>
+          </onentry>
+          <transition event="else.choosen" target="p0">
+            <assign location="ifVar1.bar" expr="'baz'" />
+          </transition>
+          <transition event="elseif.choosen" target="p0"
+                      cond="_event.data.foo == 20 &amp;&amp; 
+                            _event.data.sendVar1 == 4 &amp;&amp; 
+                            _event.data.bar == 'a string literal'" 
+          />
+        </state>
+        <state id="p0.s0.s1">
+          <onentry>
+            <if cond="_x.states['p0'] &amp;&amp; histVar1 == 1">
+              <raise event="to.s2" />
+            <else />
+              <raise event="to.s1" />
+            </if>
+          </onentry>
+          <transition event="to.s2" target="s2" />
+          <transition event="to.s1" target="s1" />
+        </state>
+      </state>
+      <state id="p0.s1">
+        <onexit>
+          <script>parallelVar1++</script>
+        </onexit>
+      </state>
+      <transition event="if.choosen" 
+                  cond="counter.itemSum == 6 &amp;&amp; 
+                        counter.indexSum == 3" 
+                  target="p0.s0.s1" />
+    </parallel>
+  </state>
+  
+  <state id="s1">
+    <invoke type="scxml" autoforward="true">
+      <content>
+        <scxml datamodel="promela">
+          <state id="waitForEvent">
+            <transition event="trigger.child">
+              <send target="#_parent" event="back.to.history" />
+            </transition>
+          </state>
+        </scxml>
+      </content>
+      <finalize>
+        <script>finalizeVar1++;</script>
+      </finalize>
+    </invoke>
+    <onentry>
+      <send event="trigger.child" delay="1000" />
+    </onentry>
+    <transition event="back.to.history" 
+                cond="finalizeVar1 == 1" 
+                target="s0.h0">
+      <assign location="histVar1" expr="4-3" />
+    </transition>
+  </state>
+  
+  <state id="s2" initial="s2.s0">
+    <onentry>
+      <send event="cancel.delayed" delay="3000" sendid="cancel.delayed" />
+      <cancel sendid="cancel.delayed" />
+    </onentry>
+    <transition event="done.state.s2" 
+                cond="_event.data.Var1 == 'foo'" 
+                target="s3.h0">
+      <assign location="histVar1" expr="8" />
+    </transition>
+    <transition event="done.state.s2" target="fail" />
+    <transition event="cancel.delayed" target="fail" />
+    <transition target="pass" cond="histVar1 == 8" />
+    <state id="s2.s0">
+      <transition target="s2.s1"/>
+    </state>
+    <final id="s2.s1">
+      <donedata>
+        <param name="Var1" expr="'foo'"/>
+      </donedata>
+    </final>
+  </state>
+  
+  <state id="s3">
+    <history id="s3.h0" type="shallow">
+      <transition target="s3.s1">
+        <log label="history transition" />
+        <assign location="histVar1" expr="4" />
+      </transition>
+    </history>
+    <state id="s3.s1">
+      <transition target="s2" />
+    </state>
+  </state>
+  
+  <final id="pass">
+    <onentry>
+      <log label="Outcome" expr="'pass'"/>
+    </onentry>
+  </final>
+  <final id="fail">
+    <onentry>
+      <log label="Outcome" expr="'fail'"/>
+    </onentry>
+  </final>
+</scxml>
\ No newline at end of file
diff --git a/test/uscxml/promela/test-event-source-auto.scxml b/test/uscxml/promela/test-event-source-auto.scxml
new file mode 100644
index 0000000..cb33636
--- /dev/null
+++ b/test/uscxml/promela/test-event-source-auto.scxml
@@ -0,0 +1,45 @@
+<scxml datamodel="promela">
+  <!--
+    An auto event source will raise all events that enable transitions. If a 
+    transition depends on a data field, these will have to be specified explicitly.
+
+    promela-event-all-but
+    [ "error.bar" ]
+    -->
+    <!-- this will become a PROMELA_NIL -->
+  <state id="s0">
+    <!--
+      if _x.states[s0]
+      
+      These specialized events will only be dispatched in s0
+      promela-event
+      [ {"name": "e1", 
+         "data": { "foo": "some string" }},
+        {"name": "e1", 
+         "data": { "bar": 12 }} 
+      ]
+      -->
+    <transition event="e1" cond="_event.data.foo == 'some string'" />
+    <transition event="error.foo" cond="_event.data.foo == 'some string'" />
+    <transition event="error.bar.*" />
+    <transition event="error.baz.*" target="s1" />
+    <transition event="e1" cond="_event.data.bar == 12" />
+    <invoke type="foo">
+      <!-- 
+      promela-event
+      [ {"name": "inv1", 
+         "data": { "foo": "something else" }},
+        {"name": "inv2", 
+         "data": { "baz": 23 }} 
+      ]
+      -->
+    </invoke>
+  </state>
+  <state id="s1">
+    <!-- This transition will never be enabled -->
+    <transition event="e1" cond="_event.data.bar == 23" />
+    <transition event="e3" cond="bar == 23" />
+    <transition event="e1" />
+    <transition event="e2" />
+  </state>
+</scxml>
diff --git a/test/uscxml/promela/test-event-source.scxml b/test/uscxml/promela/test-event-source.scxml
new file mode 100644
index 0000000..3816bd0
--- /dev/null
+++ b/test/uscxml/promela/test-event-source.scxml
@@ -0,0 +1,39 @@
+<scxml datamodel="promela">
+  <state id="s0">
+    <invoke type="scxml">
+      <!-- Sends a single event and exits -->
+      <!--
+      #promela-event-source-custom:
+        if
+        :: 1 -> eQ!#to.s1#; goto #DONE#; // end this invoker
+        fi;
+      -->
+      <content>
+        <scxml>
+          <state id="s0">
+            <onentry>
+              <send target="#_parent" event="to.s1" />
+            </onentry>
+          </state>
+        </scxml>
+      </content>
+    </invoke>
+    <transition event="to.s1" target="s1" />
+  </state>
+  <state id="s1">
+    <onentry>
+      <!-- Send event to our external queue -->
+      <send event="to.s2" />
+    </onentry>
+    <transition event="to.s2" target="s2" />
+  </state>
+  <state id="s2">
+    <onentry>
+      <!-- Send event to our internal queue -->
+      <raise event="to.s3" />
+    </onentry>
+    <transition event="to.s3" target="s3" />
+  </state>
+
+  <state id="s3" final="true" />
+</scxml>
\ No newline at end of file
diff --git a/test/uscxml/promela/test-history.scxml b/test/uscxml/promela/test-history.scxml
new file mode 100644
index 0000000..ef48f6a
--- /dev/null
+++ b/test/uscxml/promela/test-history.scxml
@@ -0,0 +1,16 @@
+<scxml datamodel="promela">
+	<state id="s0">
+		<history id="h01" type="deep" />
+		<state id="s01">
+			<transition target="s02" event="foo" />
+			<transition target="s1" event="bar" />
+		</state>
+		<state id="s02">
+			<script>printf("In S02");</script>
+			<transition target="s1" />
+		</state>
+	</state>
+	<state id="s1">
+		<transition target="h01" />
+	</state>
+</scxml>
\ No newline at end of file
diff --git a/test/uscxml/promela/test-ltl.scxml b/test/uscxml/promela/test-ltl.scxml
new file mode 100644
index 0000000..23079d9
--- /dev/null
+++ b/test/uscxml/promela/test-ltl.scxml
@@ -0,0 +1,16 @@
+<scxml datamodel="promela">
+  <!--
+		#promela-event-source:
+			toggle.foo
+	-->
+	<datamodel>
+		<data id="foo" expr="0" type="bit" />
+	</datamodel>
+	<parallel id="main">
+		<state id="toggleFoo">
+			<transition event="toggle.foo">
+				<script>foo = !foo;</script>
+			</transition>
+		</state>
+	</parallel>
+</scxml>
\ No newline at end of file
diff --git a/test/uscxml/promela/test-non-progress.scxml b/test/uscxml/promela/test-non-progress.scxml
new file mode 100644
index 0000000..2301bd6
--- /dev/null
+++ b/test/uscxml/promela/test-non-progress.scxml
@@ -0,0 +1,17 @@
+<!-- 
+  Check for no-progress cycles
+
+  $ uscxml-transform -s -i this_file.scxml > test.pml
+  $ spin -a test.pml
+  $ gcc -DNP pan.c
+  $ ./a.out -l
+-->
+<scxml datamodel="promela">
+  <state id="s0">
+    <onentry>
+      <raise event="foo" />
+    </onentry>
+    <transition event="foo" target="s0" />
+  </state>
+  <state id="s1" final="true" />
+</scxml>
\ No newline at end of file
diff --git a/test/uscxml/promela/test-progress-label.scxml b/test/uscxml/promela/test-progress-label.scxml
new file mode 100644
index 0000000..8e27345
--- /dev/null
+++ b/test/uscxml/promela/test-progress-label.scxml
@@ -0,0 +1,20 @@
+<!-- 
+
+  Check for no-progress cycles
+
+  $ uscxml-transform -s -i this_file.scxml > test.pml
+  $ spin -a test.pml
+  $ gcc -DNP pan.c
+  $ ./a.out -l
+
+-->
+<scxml datamodel="promela">
+  <state id="s0">
+    <onentry>
+      <!-- promela-progress -->
+      <raise event="foo" />
+    </onentry>
+    <transition event="foo" target="s0" />
+  </state>
+  <state id="s1" final="true" />
+</scxml>
\ No newline at end of file
diff --git a/test/uscxml/promela/test-simple.scxml b/test/uscxml/promela/test-simple.scxml
new file mode 100644
index 0000000..61c8022
--- /dev/null
+++ b/test/uscxml/promela/test-simple.scxml
@@ -0,0 +1,15 @@
+<!-- 
+  Simple example
+  
+  $ uscxml-transform -s -i this_file.scxml > test.pml
+  $ spin -p -l -h test.pml
+-->
+<scxml datamodel="promela">
+  <state id="s0">
+    <onentry>
+      <raise event="foo" />
+    </onentry>
+    <transition event="foo" target="s1" />
+  </state>
+  <state id="s1" final="true" />
+</scxml>
\ No newline at end of file
diff --git a/test/uscxml/promela/test-syntax.scxml b/test/uscxml/promela/test-syntax.scxml
new file mode 100644
index 0000000..101c97a
--- /dev/null
+++ b/test/uscxml/promela/test-syntax.scxml
@@ -0,0 +1,132 @@
+<scxml datamodel="promela" binding="early" >
+  <!--
+    promela-event-source:
+      foo.bar
+      foo.baz foo.foo
+      error.communication 
+      error.platform 
+      err.foo
+  -->
+  <datamodel>
+    <data>
+      bool b1;
+    </data>
+    <data>
+      int fooSum = 0;
+      int fooIndex = 0;
+      int fooItem;
+      int foos[10];
+    </data>
+    <data>
+      bool b2, b3, b4;
+    </data>
+    <data>
+      bool b5, b6 = 3 + 4, b7, b8, b9;
+    </data>
+    <data>
+      bool c1; bool c2; bool c3; bool c4;
+      bool c5; bool c6; bool c7, c8 = 4 + 6, c9;
+    </data>
+    <data>
+      byte state = 1;
+      mtype = {
+        FATAL, NON_FATAL, COMPLETE, INCOMPLETE,
+        red, white, blue
+      }
+    </data>
+    <data>
+      bool busy[3];
+      bool lazy[4];
+    </data>
+    <data>
+      bool v3, v2 = 1;
+    </data>
+    
+  </datamodel>
+  <state id="init">
+		<invoke type="xhtml" id="xhtml1" src="resources/gui.xhtml">
+		  <!-- #promela-event-source:
+		    foo.bar
+		    foo.baz foo.foo
+		    error.communication 
+		    error.platform 
+		    err.foo
+		  -->
+		</invoke>
+		
+    <invoke type="scxml">
+      <!--
+        promela-event-source:
+        innerFoo
+      -->
+      
+      <final id="stop">
+        <onentry>
+          <send target="#_parent" event="innerFoo" />
+        </onentry>
+      </final>
+    </invoke>
+    <onentry>
+      <!--
+        #promela-inline:
+        progress: skip;
+      -->
+      <raise event="foo.bar" />
+      <script>
+        busy[4 - 3] = 1;
+      </script>
+      <log label="foos" expr="foos" />
+      <foreach item="fooItem" array="foos" index="fooIndex">
+        <script>
+          foos[fooIndex] = fooIndex;
+        </script>
+      </foreach>
+      <log label="foos" expr="foos" />
+      <foreach item="fooItem" array="foos" index="fooIndex">
+        <log label="fooItem" expr="fooItem" />
+        <script>
+          fooSum = fooSum + fooItem;
+        </script>
+      </foreach>
+      <log label="fooSum" expr="fooSum" />
+      <if cond="b1==0">
+        <script>
+          b2=1; b3=1;
+        </script>
+      <elseif cond="b1==1" />
+        <script>
+          b2=1; b3=1;
+        </script>
+      <else />
+        <script>
+          b2=1; b3=1;
+        </script>
+      </if>
+      <script>
+        v2=1; v3=1;
+      </script>
+    </onentry>
+    <transition target="pass" cond="v2==v3 &amp;&amp; busy[1] == 1" event="foo.bar">
+      <!--
+        promela-inline:
+        progress: skip;
+      -->
+    </transition>
+    <transition target="fail" event="*">
+      <!--
+        promela-inline:
+        progress: skip;
+      -->
+    </transition>
+  </state>
+  <final id="pass">
+    <onentry>
+      <log label="Outcome" expr="'pass'"/>
+    </onentry>
+  </final>
+  <final id="fail">
+    <onentry>
+      <log label="Outcome" expr="'fail'"/>
+    </onentry>
+  </final>
+</scxml>
\ No newline at end of file