refactored term transformations, added optional display of local anal…

…yses, updated README, various other changes

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "hibou_label"
-version = "0.8.1"
+version = "0.8.2"
 authors = ["Erwan Mahe"]
 edition = "2021"
 

readme/1_interaction.md

@@ -126,5 +126,5 @@ For instance, given "i" an interaction:
 - "loopW(i)" is equivalent to the infinite alternative "alt(∅,i,seq(i,i),...)"
 - "loopP(i)" is equivalent to the infinite alternative "alt(∅,i,par(i,i),...)"
 
-"loopH" is a specific restriction of "loopW" which we documented in
-"[A structural operational semantics for interactions with a look at loops](https://arxiv.org/abs/2105.00208)".
+"loopH" is a specific restriction of "loopW" which is documented in
+"[Equivalence of Denotational and Operational Semantics for Interaction Languages](https://link.springer.com/chapter/10.1007/978-3-031-10363-6_8)".

readme/2_execution.md

@@ -2,9 +2,8 @@
 # The execution and animation of interaction models
 
 The main features of HIBOU revolve around the "execution" or "animation" of interaction models.
-By execution we mean something which consists in executing an atomic action within an initial interaction model, thereby observing its occurrence.
-The execution of such an action yields a new "follow-up" interaction model,
-which specifies all the continuations of the behavior of the original interaction, which start by the occurence of the executed action.
+By execution we mean executing an atomic action within an initial interaction model, thereby observing its occurrence.
+The execution of such an action yields a new "follow-up" interaction model which specifies all the continuations of the behavior of the original interaction following the occurrence of the executed action.
 
 This approach is detailed in
 [this paper](https://link.springer.com/chapter/10.1007%2F978-3-030-45234-6_24) and [this one](https://dl.acm.org/doi/abs/10.1145/3412841.3442054).
@@ -25,85 +24,91 @@ In the following, we will give some insights on the different elements of our la
 
 ## Basic building blocks
 
-| | Initial Encoding | Animation |
-|------------------|-------------------|-----------|
-| atomic emission | <pre>@message{message}<br>@lifeline{lifeline}<br>lifeline -- message ->&#124;</pre> | <img src="./images/2/basic/emission.svg" alt="execution of an emission" width="150"> |
-| atomic reception | <pre>@message{message}<br>@lifeline{lifeline}<br>message -> lifeline</pre> | <img src="./images/2/basic/reception.svg" alt="execution of a reception" width="150"> |
-| asynchronous message passing | <pre>@message{message}<br>@lifeline{l1;l2}<br>l1 -- message -> l2</pre> | <img src="./images/2/basic/asynch_passing.svg" alt="execution of an asynchronous message passing" width="150"> |
-| synchronous message passing | <pre>@message{m}<br>@lifeline{l1;l2}<br>l1 -- <synch>m -> l2</pre> | <img src="./images/2/basic/synch_passing.svg" alt="execution of a synchronous message passing" width="150"> |
-| asynchronous broadcast | <pre>@message{m}<br>@lifeline{lo;lt1;lt2}<br>lo -- m -> (lt1,lt2)</pre> | <img src="./images/2/basic/asynch_broadcast.svg" alt="execution of an asynchronous broadcast" width="275"> |
-| synchronous broadcast | <pre>@message{m}<br>@lifeline{lo;lt1;lt2}<br>lo -- <synch>m -> (lt1,lt2)</pre> | <img src="./images/2/basic/synch_broadcast.svg" alt="execution of a synchronous broadcast" width="260"> |
+The previously introduced basic building blocks can be executed as is represented below.
 
+Each node in grey represents the state of the interaction at a given moment, with, on the left, its syntaxic structure, and, on the right, its representation as a sequence diagram.
 
+Each transition corresponds to the execution/expression of an atomic action.
 
+| | Animation |
+|------------------|-----------|
+| atomic emission | <img src="./examples/2/basic/emission.svg" alt="execution of an emission"> |
+| atomic reception | <img src="./examples/2/basic/reception.svg" alt="execution of a reception"> |
+| asynchronous message passing | <img src="./examples/2/basic/asynch_passing.svg" alt="execution of an asynchronous message passing"> |
+| synchronous message passing | <img src="./examples/2/basic/synch_passing.svg" alt="execution of a synchronous message passing"> |
+| asynchronous broadcast | <img src="./examples/2/basic/asynch_broadcast.svg" alt="execution of an asynchronous broadcast"> |
+| synchronous broadcast | <img src="./examples/2/basic/synch_broadcast.svg" alt="execution of a synchronous broadcast"> |
 
 
-## Alt
-
-Alternatives propose non-deterministic choice between several exclusive alternatives.
 
-<img src="./images/2/alt.svg" alt="execution of actions within an alternative" width="275">
 
 
-## Strict, Seq and Par
+## Alt
 
-### Actions on the same lifeline(s)
+Alternatives propose non-deterministic choice between several exclusive alternatives.
 
-With strict sequencing:
+<img src="./images/2/alt.svg" alt="execution of actions within an alternative">
 
-<img src="./images/2/sched/strict_same.svg" alt="" width="150">
 
-With weak sequencing:
+## Strict, Seq and Par
 
-<img src="./images/2/sched/seq_same.svg" alt="" width="150">
+Three basic scheduling operators enables us to specify successions of behaviors.
 
-With interleaving:
+"strict" corresponds to a strict sequencing operator, specifying a strict succession of behaviors.
 
-<img src="./images/2/sched/par_same.svg" alt="" width="275">
+"seq" corresponds to a weak sequencing operator, specifying that events occurring on
+the same sub-system (lifeline) must occur in a strict order
+even though events occurring on different sub-systems (lifelines) may occur in any order.
 
-### Actions on different lifelines
+"par" corresponds to an interleaving operator, allowing any order between events.
 
-With strict sequencing:
 
-<img src="./images/2/sched/strict_diff.svg" alt="" width="150">
+### Actions on the same lifeline(s)
 
-With weak sequencing:
+| strict | seq | par |
+|-----------------------------------------------------|--------------------------------------------------|--------------------------------------------------|
+| <img src="./images/2/sched/strict_same.svg" alt=""> | <img src="./images/2/sched/seq_same.svg" alt=""> | <img src="./images/2/sched/par_same.svg" alt=""> |
 
-<img src="./images/2/sched/seq_diff.svg" alt="" width="275">
 
-With interleaving:
+### Actions on different lifelines
 
-<img src="./images/2/sched/par_diff.svg" alt="" width="275">
+| strict | seq | par |
+|-----------------------------------------------------|--------------------------------------------------|--------------------------------------------------|
+| <img src="./images/2/sched/strict_diff.svg" alt=""> | <img src="./images/2/sched/seq_diff.svg" alt=""> | <img src="./images/2/sched/par_diff.svg" alt=""> |
 
 
 ## Coreg
 
-As explained previously, a coretion behaves as par on certain lifelines and as seq on the others.
-Here, we can see that:
+A coregion behaves as "par" on certain lifelines and as "seq" on the others.
+In the example, we can see that:
 - l1 must emit m1 before it can emit m2 because the coregion behaves as seq on l1 
 - and l2 can receive m1 and m2 in any order because the coregion behaves as par on l2 
 
-<img src="./images/2/coreg.svg" alt="" width="275">
+<img src="./images/2/coreg.svg" alt="">
 
 ## Pruning
 
-The interplay between alternatives and sequencing makes so that the execution of certain actions
-implicitly imply making certain choices on alternatives. 
+The interplay between alternatives and sequencing makes so that the execution of certain actions implicitly imply making certain choices on alternatives. 
 This must be taken into account when computing the corresponding follow-up interaction.
 
-<img src="./images/2/pruning/pruning_strict.svg" alt="" width="275">
+This is done via a mechanism of pruning which is illustrated with the two examples below.
 
-Another example with a coregion:
+In the first one, we have an alternative in which we have either the passing of message "m1" or nothing, which is followed by the emission of "m2".
+If the first thing that occur is the emission of "m2" then it is impossible to observe "m1" later on.
+Hence, when executing the emission of "m2", this part of the diagram must be pruned out.
 
-<img src="./images/2/pruning/pruning_coreg.svg" alt="" width="350">
+In the second example the pruning of the broadcast of "m1" only occur when it is "l3" which emits "m2" because there is a coregion on "l2" which would allow both orders on the event.
 
+| example 1 | example 2 |
+|-----------|-----------|
+| <img src="./images/2/pruning/pruning_strict.svg" alt=""> | <img src="./images/2/pruning/pruning_coreg.svg" alt=""> |
 
 
 
 ## Loops
 
 Loops specify repetitions of behavior.
-Please refer to "[A structural operational semantics for interactions with a look at loops](https://arxiv.org/abs/2105.00208)" for further details.
+Please refer to "[Equivalence of Denotational and Operational Semantics for Interaction Languages](https://link.springer.com/chapter/10.1007/978-3-031-10363-6_8)" for further details.
 
 Below we demonstrate the difference between loopH and loopW on an example:
 

readme/examples/2/basic/COMMANDS.txt

@@ -0,0 +1,14 @@
+(.\hibou_label.exe explore sig.hsf asynch_broadcast.hif explo.hcf) -and (Rename-Item explo_l1.svg asynch_broadcast.svg)
+(.\hibou_label.exe explore sig.hsf asynch_passing.hif explo.hcf) -and (Rename-Item explo_l1.svg asynch_passing.svg)
+(.\hibou_label.exe explore sig.hsf emission.hif explo.hcf) -and (Rename-Item explo_l1.svg emission.svg)
+(.\hibou_label.exe explore sig.hsf reception.hif explo.hcf) -and (Rename-Item explo_l1.svg reception.svg)
+(.\hibou_label.exe explore sig.hsf synch_broadcast.hif explo.hcf) -and (Rename-Item explo_l1.svg synch_broadcast.svg)
+(.\hibou_label.exe explore sig.hsf synch_passing.hif explo.hcf) -and (Rename-Item explo_l1.svg synch_passing.svg)
+
+
+hibou_label explore sig.hsf asynch_broadcast.hif explo.hcf && mv explo_l1.svg asynch_broadcast.svg
+hibou_label explore sig.hsf asynch_passing.hif explo.hcf && mv explo_l1.svg asynch_passing.svg
+hibou_label explore sig.hsf emission.hif explo.hcf && mv explo_l1.svg emission.svg
+hibou_label explore sig.hsf reception.hif explo.hcf && mv explo_l1.svg reception.svg
+hibou_label explore sig.hsf synch_broadcast.hif explo.hcf && mv explo_l1.svg synch_broadcast.svg
+hibou_label explore sig.hsf synch_passing.hif explo.hcf&& mv explo_l1.svg synch_passing.svg

readme/examples/2/basic/asynch_broadcast.hif

@@ -0,0 +1 @@
+lo -- m -> (lt1,lt2)