Merge branch 'develop'

CHANGES.md

@@ -1,6 +1,11 @@
+# v0.12.0rc
+
+- [rules2ldl] natural numbers  
+  support all arithmetic (add/sub/mul/div) and comparison (eq/ne/gt/lt/ge/le) operations.
+
 # v0.11.0 (2018-12-03)
 
-- [rulespp] natural numbers  
+- [rules2ldl] natural numbers  
   natural numbers (literals and variables) are supported.
   `variable x : nat (n)` declares a variable `x` that ranges over 0, ..., n - 1.
   expressions such as `x = 1`, `x = y`, and `x + 1 = y + 2` are recognized as propositions.

README.md

@@ -1,70 +1,71 @@
 # Summary
 [*dsl4sc*](https://github.com/ldltools/dsl4sc) is a domain-specific language,
 based on [LDL<sub>f</sub>](https://www.cs.rice.edu/~vardi/),
-for defining, verifying, and running state transition models for event processing.
+for defining and verifying state transition models for event processing.
 
-Each model defined in dsl4sc has the following unique characteristics:
+Each model in dsl4sc has the following unique characteristics:
 
-- Its building blocks -- _protocols_, _properties_, and
-  [_ECA rules_](https://en.wikipedia.org/wiki/Event_condition_action) --
-  are independent of each other.  
-  You can regard each protocol, property, or rule as a separate model,
-  while the whole model as a conjunctive composition of these building-block models.
-- It has a clear semantics in LDL<sub>f</sub>.
+- It can be defined in terms of event _protocol_, _properties_, and ECA _rules_
+  - event protocol: _regular_ pattern of acceptable event sequences
+  - propery: LDL<sub>f</sub> formula that globally holds as an invariant condition.
+  - [_ECA rule_](https://en.wikipedia.org/wiki/Event_condition_action):
+    relation between an event and its impact on internal states
+- It has a clear semantics in terms of LDL<sub>f</sub>.
 - it can be verified statically and formally against arbitrary requirements
   that are also defined in dsl4sc
 - It can derive an executable statechart in [SCXML](https://www.w3.org/TR/scxml/)
 
 # Example: [ping\_pong](examples/ping\_pong/README.md) -- You say "ping" and I say "pong"
 
-Let us consider 2 sorts of events, _ping_ and _pong_, which are emitted in an
-alternating manner.  
-We can define the following dsl4sc models that capture this behavior and
-perform their verification and translation to executable forms.
+Consider 2 sorts of events, _ping_ and _pong_:
+The following two dsl4sc models both track ping and pong events
+emitted in an alternating manner.  
 
-(1) _model1_ includes a single _protocol_ definition in dsl4sc as follows.
+(1) ping\_pong1.rules -- _protocol-only_ model
 
-&ensp; **protocol**
-&ensp; (ping; pong); (ping; pong)*;; // ping followed by pong (1 or more times)
-
-(2) _model2_ introduces _waiting_ to keep track of whether a _pong_ is awaited
+```
+protocol (ping; pong)* ;; // ping followed by pong (repeats 0 or more times)
+```
 
-&ensp; **property**  
-&ensp; &ensp; !waiting; // initially waiting is set to false (pong is not awaited)  
-&ensp; **rule**  
-&ensp; &ensp; **on** ping **when** !waiting **do** { console.log ("You say ping"); } **ensure** waiting;  
-&ensp; &ensp; &ensp; // ping turns waiting from false into true  
-&ensp; &ensp; **on** pong **when** waiting **do** { console.log ("I say pong"); } **ensure** !waiting;  
-&ensp; &ensp; &ensp; // pong turns waiting from true into false
+(2) ping\_pong2.rules -- model that includes _protocol_, _property_, and _rule_ parts
 
-Note that, since no protocol is defined,
-_model2_ assumes that `ping` and `pong` events may arrive in any order.
+```
+protocol  
+  (ping + pong)*;; // ping or pong (repeats 0 or more times)  
+property  
+  !pinged; // not "pinged", initially  
+rule  
+  on ping when !pinged ensure pinged; // pinged after processing ping  
+  on pong when pinged ensure !pinged;  
+```
 
-(3) _model3_ by merging (1) and (2) into one.
+(3) model checking
 
-(4) Requirements for the models.
+ping\_pong1 accepts only ping or pong -- (ping; pong)* |= (ping + pong)*
 
-1. **protocol** (ping + pong)*; pong;;  
-   either ping or pong may repeat any times, though the last event is always pong
-1. **property** [{true}\*][{waiting}] !waiting;  
-   at any point, waiting always changes from true to false
+```
+$ echo 'protocol (ping + pong)*;;' | rulesmc -m ping_pong1.rules /dev/stdin  
+claim holds
+```
 
-The first requirement is met by _model1_ and _model3_, while
-the second one is met by _model2_ and _model3_.
+ping\_pong2 includes ping\_pong1
 
-(5) SCXML generation and execution
+```
+$ rulesmc -m ping_pong2.rules ping_pong1.rules --reachability  
+reachable
+```
 
-Models can be translated into SCXML.
-When `ping` and `pong` are emitted to the SCXML statechart generated from _model3_,
-the following messages appear on the console.
+ping\_pong3, defined as the _conjunction_ of ping\_pong1 and ping\_pong2,
+entails that _!pinged_ and _pinged_ hold in an alternating manner.
+-- ping\_pong3 |= <({!pinged}; {pinged})*> !pinged
 
 ```
-You say ping  
-I say pong
+$ cat ping_pong1.rules ping_pong2.rules > ping_pong3.rules  
+$ echo 'property <({!pinged}; {pinged})*> !pinged;' | rulesmc -m ping_pong3.rules /dev/stdin  
+claim holds
 ```
 
-For more detail,
-please take a look at [these examples](examples/README.md).
+Check out [more examples](examples/README.md) if you are interested.  
 
 # Installation on Docker
 

docs/grammar/core_grammar.html

@@ -1,7 +1,7 @@
 <!DOCTYPE html><html>
 <head>
 <title>Untitled Document</title>
-<!--Generated on Sat Nov 10 10:13:34 2018 by LaTeXML (version 0.8.2) http://dlmf.nist.gov/LaTeXML/.-->
+<!--Generated on Thu Dec 13 09:55:20 2018 by LaTeXML (version 0.8.2) http://dlmf.nist.gov/LaTeXML/.-->
 
 <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
 </head>
@@ -22,8 +22,8 @@
 <tr id="S0.Ex2" class="ltx_equation ltx_eqn_row ltx_align_baseline">
 <td class="ltx_eqn_cell ltx_eqn_center_padleft"></td>
 <td class="ltx_td ltx_align_right ltx_eqn_cell"><span class="ltx_text ltx_markedasmath ltx_font_italic">protocol_decl</span></td>
-<td class="ltx_td ltx_align_left ltx_eqn_cell"><math id="S0.Ex2.m2" class="ltx_Math" alttext="\displaystyle::=\textbf{event}\;\textit{event\_name}\;\left(\texttt{,}\;%
-\textit{event\_name}\right)^{\ast}\;\texttt{;}" display="inline"><mrow><mo>:</mo><mo>:=</mo><mpadded width="+2.8pt"><mtext mathvariant="bold">event</mtext></mpadded><mpadded width="+2.8pt"><mtext mathvariant="italic">event_name</mtext></mpadded><mpadded width="+2.8pt"><msup><mrow><mo>(</mo><mpadded width="+2.8pt"><mtext mathvariant="monospace">,</mtext></mpadded><mtext mathvariant="italic">event_name</mtext><mo>)</mo></mrow><mo>∗</mo></msup></mpadded><mtext mathvariant="monospace">;</mtext></mrow></math></td>
+<td class="ltx_td ltx_align_left ltx_eqn_cell"><math id="S0.Ex2.m2" class="ltx_Math" alttext="\displaystyle::=\textbf{event}\;\left(\textit{event\_name}\;\texttt{;}\right)^%
+{+}" display="inline"><mrow><mo>:</mo><mo>:=</mo><mpadded width="+2.8pt"><mtext mathvariant="bold">event</mtext></mpadded><msup><mrow><mo>(</mo><mpadded width="+2.8pt"><mtext mathvariant="italic">event_name</mtext></mpadded><mtext mathvariant="monospace">;</mtext><mo>)</mo></mrow><mo>+</mo></msup></mrow></math></td>
 <td class="ltx_eqn_cell ltx_eqn_center_padright"></td>
 </tr>
 <tr id="S0.Ex3" class="ltx_equation ltx_eqn_row ltx_align_baseline">
@@ -44,14 +44,15 @@
 <td class="ltx_eqn_cell ltx_eqn_center_padleft"></td>
 <td class="ltx_td ltx_align_right ltx_eqn_cell"></td>
 <td class="ltx_td ltx_align_left ltx_eqn_cell"><math id="S0.Ex5.m2" class="ltx_Math" alttext="\displaystyle\quad\mid\;\textit{protocol}\;\texttt{+}\;\textit{protocol}\;\mid%
-\;\textit{protocol}\;\texttt{*}" display="inline"><mrow><mi mathvariant="normal"> </mi><mo>⁢</mo><mrow><mo rspace="5.3pt">∣</mo><mrow><mpadded width="+2.8pt"><mtext mathvariant="italic">protocol</mtext></mpadded><mo>⁢</mo><mpadded width="+2.8pt"><mtext mathvariant="monospace">+</mtext></mpadded><mo>⁢</mo><mpadded width="+2.8pt"><mtext mathvariant="italic">protocol</mtext></mpadded></mrow><mo rspace="5.3pt">∣</mo></mrow><mo>⁢</mo><mpadded width="+2.8pt"><mtext mathvariant="italic">protocol</mtext></mpadded><mo>⁢</mo><mtext mathvariant="monospace">*</mtext></mrow></math></td>
+\;\textit{protocol}\;\texttt{*}\;\mid\;\texttt{(}\;\textit{protocol}\;\;%
+\texttt{)}" display="inline"><mrow><mi mathvariant="normal"> </mi><mo rspace="5.3pt">∣</mo><mpadded width="+2.8pt"><mtext mathvariant="italic">protocol</mtext></mpadded><mpadded width="+2.8pt"><mtext mathvariant="monospace">+</mtext></mpadded><mpadded width="+2.8pt"><mtext mathvariant="italic">protocol</mtext></mpadded><mo rspace="5.3pt">∣</mo><mpadded width="+2.8pt"><mtext mathvariant="italic">protocol</mtext></mpadded><mpadded width="+2.8pt"><mtext mathvariant="monospace">*</mtext></mpadded><mo rspace="5.3pt">∣</mo><mpadded width="+2.8pt"><mtext mathvariant="monospace">(</mtext></mpadded><mpadded width="+5.6pt"><mtext mathvariant="italic">protocol</mtext></mpadded><mtext mathvariant="monospace">)</mtext></mrow></math></td>
 <td class="ltx_eqn_cell ltx_eqn_center_padright"></td>
 </tr>
 <tr id="S0.Ex6" class="ltx_equation ltx_eqn_row ltx_align_baseline">
 <td class="ltx_eqn_cell ltx_eqn_center_padleft"></td>
 <td class="ltx_td ltx_align_right ltx_eqn_cell"><span class="ltx_text ltx_markedasmath ltx_font_italic">property_decl</span></td>
-<td class="ltx_td ltx_align_left ltx_eqn_cell"><math id="S0.Ex6.m2" class="ltx_Math" alttext="\displaystyle::=\textbf{variable}\;\textit{var\_name}\;\left(\texttt{,}\;%
-\textit{var\_name}\right)^{\ast}\;\texttt{;}" display="inline"><mrow><mo>:</mo><mo>:=</mo><mpadded width="+2.8pt"><mtext mathvariant="bold">variable</mtext></mpadded><mpadded width="+2.8pt"><mtext mathvariant="italic">var_name</mtext></mpadded><mpadded width="+2.8pt"><msup><mrow><mo>(</mo><mpadded width="+2.8pt"><mtext mathvariant="monospace">,</mtext></mpadded><mtext mathvariant="italic">var_name</mtext><mo>)</mo></mrow><mo>∗</mo></msup></mpadded><mtext mathvariant="monospace">;</mtext></mrow></math></td>
+<td class="ltx_td ltx_align_left ltx_eqn_cell"><math id="S0.Ex6.m2" class="ltx_Math" alttext="\displaystyle::=\textbf{variable}\;\left(\textit{var\_name}\;\texttt{;}\right)%
+^{+}" display="inline"><mrow><mo>:</mo><mo>:=</mo><mpadded width="+2.8pt"><mtext mathvariant="bold">variable</mtext></mpadded><msup><mrow><mo>(</mo><mpadded width="+2.8pt"><mtext mathvariant="italic">var_name</mtext></mpadded><mtext mathvariant="monospace">;</mtext><mo>)</mo></mrow><mo>+</mo></msup></mrow></math></td>
 <td class="ltx_eqn_cell ltx_eqn_center_padright"></td>
 </tr>
 <tr id="S0.Ex7" class="ltx_equation ltx_eqn_row ltx_align_baseline">
@@ -120,7 +121,7 @@
 </article>
 </div>
 <footer class="ltx_page_footer">
-<div class="ltx_page_logo">Generated  on Sat Nov 10 10:13:34 2018 by <a href="http://dlmf.nist.gov/LaTeXML/">LaTeXML <img src="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAAsAAAAOCAYAAAD5YeaVAAAAAXNSR0IArs4c6QAAAAZiS0dEAP8A/wD/oL2nkwAAAAlwSFlzAAALEwAACxMBAJqcGAAAAAd0SU1FB9wKExQZLWTEaOUAAAAddEVYdENvbW1lbnQAQ3JlYXRlZCB3aXRoIFRoZSBHSU1Q72QlbgAAAdpJREFUKM9tkL+L2nAARz9fPZNCKFapUn8kyI0e4iRHSR1Kb8ng0lJw6FYHFwv2LwhOpcWxTjeUunYqOmqd6hEoRDhtDWdA8ApRYsSUCDHNt5ul13vz4w0vWCgUnnEc975arX6ORqN3VqtVZbfbTQC4uEHANM3jSqXymFI6yWazP2KxWAXAL9zCUa1Wy2tXVxheKA9YNoR8Pt+aTqe4FVVVvz05O6MBhqUIBGk8Hn8HAOVy+T+XLJfLS4ZhTiRJgqIoVBRFIoric47jPnmeB1mW/9rr9ZpSSn3Lsmir1fJZlqWlUonKsvwWwD8ymc/nXwVBeLjf7xEKhdBut9Hr9WgmkyGEkJwsy5eHG5vN5g0AKIoCAEgkEkin0wQAfN9/cXPdheu6P33fBwB4ngcAcByHJpPJl+fn54mD3Gg0NrquXxeLRQAAwzAYj8cwTZPwPH9/sVg8PXweDAauqqr2cDjEer1GJBLBZDJBs9mE4zjwfZ85lAGg2+06hmGgXq+j3+/DsixYlgVN03a9Xu8jgCNCyIegIAgx13Vfd7vdu+FweG8YRkjXdWy329+dTgeSJD3ieZ7RNO0VAXAPwDEAO5VKndi2fWrb9jWl9Esul6PZbDY9Go1OZ7PZ9z/lyuD3OozU2wAAAABJRU5ErkJggg==" alt="[LOGO]"></a>
+<div class="ltx_page_logo">Generated  on Thu Dec 13 09:55:20 2018 by <a href="http://dlmf.nist.gov/LaTeXML/">LaTeXML <img src="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAAsAAAAOCAYAAAD5YeaVAAAAAXNSR0IArs4c6QAAAAZiS0dEAP8A/wD/oL2nkwAAAAlwSFlzAAALEwAACxMBAJqcGAAAAAd0SU1FB9wKExQZLWTEaOUAAAAddEVYdENvbW1lbnQAQ3JlYXRlZCB3aXRoIFRoZSBHSU1Q72QlbgAAAdpJREFUKM9tkL+L2nAARz9fPZNCKFapUn8kyI0e4iRHSR1Kb8ng0lJw6FYHFwv2LwhOpcWxTjeUunYqOmqd6hEoRDhtDWdA8ApRYsSUCDHNt5ul13vz4w0vWCgUnnEc975arX6ORqN3VqtVZbfbTQC4uEHANM3jSqXymFI6yWazP2KxWAXAL9zCUa1Wy2tXVxheKA9YNoR8Pt+aTqe4FVVVvz05O6MBhqUIBGk8Hn8HAOVy+T+XLJfLS4ZhTiRJgqIoVBRFIoric47jPnmeB1mW/9rr9ZpSSn3Lsmir1fJZlqWlUonKsvwWwD8ymc/nXwVBeLjf7xEKhdBut9Hr9WgmkyGEkJwsy5eHG5vN5g0AKIoCAEgkEkin0wQAfN9/cXPdheu6P33fBwB4ngcAcByHJpPJl+fn54mD3Gg0NrquXxeLRQAAwzAYj8cwTZPwPH9/sVg8PXweDAauqqr2cDjEer1GJBLBZDJBs9mE4zjwfZ85lAGg2+06hmGgXq+j3+/DsixYlgVN03a9Xu8jgCNCyIegIAgx13Vfd7vdu+FweG8YRkjXdWy329+dTgeSJD3ieZ7RNO0VAXAPwDEAO5VKndi2fWrb9jWl9Esul6PZbDY9Go1OZ7PZ9z/lyuD3OozU2wAAAABJRU5ErkJggg==" alt="[LOGO]"></a>
 </div></footer>
 </div>
 </body>