Reactive graphs in action

(extended version)

David Tinoco1 Alexandre Madeira1

Manuel A. Martins1 José Proença2
CIDMA, Dep. Mathematics, Aveiro University, Aveiro, Portugal
CISTER, Faculty of Sciences, University of Porto, Portugal

Reactive graphs are transition structures whereas edges become active and inactive during its evolution, that were introduced by Dov Gabbay from a mathematical's perspective.
This paper presents (https://fm-dcc.github.io/MARGe), a web-based tool to visualise and analyse reactive graphs enriched with labels. animates the operational semantics of reactive graphs and offers different graphical views to provide insights over concrete systems. We motivate the applicability of reactive graphs for adaptive systems and for featured transition systems, using to tighten the gap between the existing theoretical models and their usage to analyse concrete systems.

§ INTRODUCTION AND MOTIVATION

A reactive graph is a transition structure that updates its transitions along its execution. This concept has been introduced by Dov Gabbay in <cit.>. It generalizes the static notion of a graph by incorporating high-order edges that capture updates on the accessibility relations.
The notion of reactivity for these structures is not coined only in the standard sense of Harel and Pnueli <cit.>, as systems that react to their environment and are not meant to terminate, but as systems whose accessibility relation is
a result of the transformations induced by the transitions executed so far.

Let us consider the model of a simple vending machine in <ref> to motivate reactive graphs.
Edges in reactive graphs can be active or inactive, and only transitions involving active edges can be executed.
All edges in our vending machine are active, except one with a dotted line.
Executing a transition triggers an update on the set of active and inactive edges.

A reactive graph of a vending machine offering two different products

The machine VM in <ref> can receive from the user at most 1. The arrows between states represent ground edges, which are labelled with actions; the others arrows represent hyper edges, i.e., edges that can activate ($\arrowOn$) and deactivate ($\arrowOff$) edges.
When the action 1 is performed some edges are deactivated and the machine goes to the Chocolate state. More specifically, both edges labelled by 0.5 and 1 are deactivated. Executing instead the edge labelled by 0.5 would enable a deactivating edge, and executing it a second time would deactivate it.

A solid supporting theory for these models, including proposals of specification logics, has been studied in the last years (e.g. <cit.>) and was summed up in the book <cit.>.
The main advantage of reactive graphs with respect to traditional labelled transition systems (LTS) is the compact representation of dynamic systems.
Gabbay showed the encoded LTS of a given reactive system can have an exponentially larger number of states <cit.>.
For example, our vending machine can be expressed with an LTS with seven states, depicted in <ref>. In a larger example borrowed from Cordy et al. <cit.>, presented in <ref>, the encoded LTS has 7x more states and 4.6x more edges (including hyper edges).
Furthermore, we believe that many examples become easier to understand and to maintain with reactive graphs than with traditional LTSs.

[node distance=15mm, thick, main/.style = draw,rectangle, rounded corners = 2pt, action/.style = rectangle, fill = lightgray!50!white, text = black, rounded corners = 2pt, minimum size = 0.3cm,>=Stealth[length=3mm]]

[main] (inserti)  at (0,0)Insert;
[main] (choco)    at (3, 0.7)Chocolate;
[main] (insertch) at (8, 0.7)Insert;
[main] (cofee1)   at (3,-0.7)Coffee;
[main] (insertc1) at (6,-0.7)Insert;
[main] (cofee2)   at (8.5,-0.7)Coffee;

[main] (insertc2) at (11.5,-0.7)Insert;

[->,bend left=15]  (inserti)  to node[action]$1$ (choco);
[->] (choco)  to node[action]Get chocolate (insertch);

[->,bend right=15]  (inserti)  to node[action]$0.5$ (cofee1);
[->] (cofee1)  to node[action,rotate=45]Get coffee (insertc1);
[->] (insertc1)  to node[action,rotate = 45]$0.5$ (cofee2);
[->] (cofee2)  to node[action,rotate =45]Get coffee (insertc2);

The LTS of the vending machine in <ref>

Reconfigurable systems and variability.
Not all scenarios and application domains can exploit the advantages of modelling by reactive graphs. The benefits of compactness and being more intuitive are more evident when analysing reconfigurable systems. These are systems that operate in different modes of execution, e.g., an operating systems that supports users with different permissions or different performance modes (e.g. an ocean exploring robot that adjusts its behaviour based on the distance of its base, its energy levels, and its environmental conditions).

Work on software product lines (SPL) focuses mainly on configurable systems, i.e., how to develop, maintain, and reason over families of software that share many commonalities. Feature transition systems  <cit.> are structures often used to model such systems, which are enriched with annotations over features, allowing an initial configuration of the variant to select which transitions are active. A branch of SPL focuses on dynamic SPL <cit.>
addressing reconfigurable and self-adaptive systems, in which the configuration can change over time, which relates to our reactive graphs.

This paper introduces :
an open-source web-based prototype tool designed for the visualisation and analysis of labelled reactive graphs. It includes several examples, both from the literature on reactive graphs <cit.> and from work on dynamic SPL <cit.>. The goal of is to help increasing the adoption of reactive graphs,
providing insights over the capabilities and challenges of modelling reconfigurable systems with reactive graphs,
and to expose these to different domains to increase it applicability. Currently does not aim at contributing directly to the community on adaptative SPLs, since it still misses a more user-friendly specification language and mechanisms to support larger systems.
provides support to:
(1) visualise reactive graphs,
(2) animate its operational semantics,
(3) explore the full state-space of its underlying LTS,
(4) verify properties such as deadlocks and conflicts, and
(5) compare reactive graphs using an observational equivalence.

§ MULTI-ACTIONS REACTIVE GRAPHS

A multi-action reactive graph, or simply reactive graph, is a labelled transition system with transitions enriched with a reaction that activates and deactivates transitions, defined formally below.

A Multi-Action Reactive Graph is a tuple
$M = (W, Act, E, \arrowG, \arrowOn, \arrowOff,\overline{\cdot},w_0,\alpha_0)$ where:

* $W\neq \emptyset$ is the set of states;
$Act$ is the set of actions;
$E$ is the set of edges;

* $\arrowG ~\subseteq~ W \times Act \times W$ is the set of ground edges;
$\arrowOn  ~\subseteq~ E\times E$ is the set of activating edges;
$\arrowOff ~\subseteq~ E\times E$ is the set of deactivating edges;
$\overline{\cdot}~:\, E \longrightarrow (\arrowG\cup\arrowOn\cup\arrowOff)$ is an injective function that maps edges in $E$ to their internal details;

* $w_0 \in W$ is the initial state;
$\alpha_0 \in E$ is the set of initially active edges.

Recall the vending machine in <ref>.
When formalising this as a we say that:
(i) Coffee belongs to $W$ (among others),
(ii) lightgray!50!white 0.5  is an action in Act,
$\tpl{\mi{Insert},\text{\action{0.5\euro}},\allowbreak\mi{Coffee}}$ is a ground edge in $\arrowG$,
(iii) $\tpl{e^\dag,e^\dag}$ is a deactivating edge in $\arrowOff$ where $\overline{e^{\dag}} = \tpl{\mi{Insert},\text{\action{0.5\euro}},\allowbreak\mi{Coffee}}$,
(iv) $w_0 = \mi{Insert}$,
(v) $\alpha_0$ is the set of edges in $E$ without the deactivating edge $\tpl{e^\dag,e^\dag}$.

A has an initial state $w_0$ and an initial set of active edges $\alpha_0$. Evolving a means transitioning to a new state, connected by an enabled ground edge from $w_0$, and updating the set of active edges. We start by formalising the set of activate and deactivate edges by another given edge, and then formalise the evolution of .

Given a $M$, an edge $e\in E_M$ and a set of active edges $\alpha \subseteq E_M$, we define the set of edges activated by $e$ (resp. deactivated by $e$), written $\mathsf{on}(e,\alpha)$ (resp. $\mathsf{off}(e,\alpha)$) as follows.

\begin{align*}
\mathsf{from}(e_s) =& \{e ~|~ \exists e_t \cdot \overline{e} = (e_s,e_t)\}
\\% \\[1mm]
\mathsf{from\mkern-2mu}^{*}(e,\alpha) = &
\begin{array}{l}
\bigcup_{r\in (\mathsf{from}(e) \cap \alpha)}
\mathsf{from\mkern-2mu}^{*}(r,\alpha\backslash \{e\})\cup \{r\}
\end{array}
\\%\\[1mm]
\mathsf{on}(e,\alpha)=&
\{e_t ~|~ % all targets such that
e_{\mi{trg}} \in \mathsf{from\mkern-2mu}^{*}(e,\alpha) % e_trg is triggered
\land
\exists e_s \cdot \overline{e_{\mi{trg}}} = (e_s,e_t) \in \arrowOn
\}
\\%\\[1mm]
\mathsf{off}(e,\alpha)=& %\left\{\begin{array}{ll}
\{e_t ~|~ % all targets such that
e_{\mi{trg}} \in \mathsf{from\mkern-2mu}^{*}(e,\alpha) % e_trg is triggered
\land
\exists e_s \cdot \overline{e_{\mi{trg}}} = (e_s,e_t) \in \arrowOff
\}
\end{align*}

Intuitively $\mathsf{from}(e_s)$ returns the hyper edges that start from $e_s$,
$\mathsf{from\mkern-2mu}^{*}$ keeps traversing $\mathsf{from}$ to collect all (active) hyper edges triggered from a single edge,
$ \mathsf{on}(e,\alpha)$ (resp. $ \mathsf{off}(e,\alpha)$) collect all the targets triggered from $e$ by an activating (resp. deactivating) edge.

For example, in the vending machine in <ref> we have that $\mathsf{off}(e_1,E) = \{e_1,e_2\}$, where
$\overline{e_1}=\tpl{\mi{Insert},\text{\action{1\euro}},\mi{Chocolate}}$ and
This means that executing the edge from Insert to Chocolate triggers the deactivating edges $e_1$ and $e_2$.
Using this notion of (de)activation, the evolution of a is formalised below.

The semantics of a $M$ is given by the evolution of a configuration $\tpl{w,\alpha}$ of a state $w\in W$ and active edges $\alpha\subseteq E$, starting from the initial configuration $\tpl{w_0,\alpha_0}$, given by the rule below.

\exists e\in \alpha ~\cdot~
\overline{e} = (w,a,w') ~\land~
\alpha' = \big( \alpha \cup \mathsf{on}(e,\alpha) \big)
\backslash \mathsf{off}(e,\alpha)
\\\hline
\tpl{w,\alpha} \xrightarrow{a}_M  \tpl{w',\alpha'}
\end{array}$

Using the semantics above to our reactive vending machine from <ref> we obtain the LTS depicted in <ref>.
This semantics differs from Gabbay's semantics by atomically collecting all activate edges before applying their (de)activations effects, instead of activating and deactivating edges during the traversal of triggered edges. It also introduces a bias: whenever an edge is both activated and deactivated in a step, deactivation takes precedence. However this may not be intended, which we will address in the next section over contradictory effects.

Relevant properties of reactive graph.
As seen in <ref>, the behaviour of a $M = (W, Act, E, \arrowG,$ $  \arrowOn, \arrowOff,\overline{\cdot},w_0,\alpha_0)$ from a configuration $\tpl{w,\alpha}$ can be represented by the LTS induced by relation $\to_M = \bigcup\{ \xrightarrow{a}_M \mid a\in Act\}$.
Many standard properties of can be defined over the LTS induced by the semantics of ,

A deadlock is a state from which there is no transition (in our case an active transition), often undesirable.
In we can also search for deadlocks
by traversing the induced LTSs from $w_0$ while searching for states without outgoing transitions.

Unreachable states.
An unreachable state, also undesirable in many systems, is a state that cannot be reached from the initial configuration.

Observational equivalence.
As in standard LTS, two configurations are said to be equivalent if they behave in the same way. One way of defining such kind of equivalences is by means of their induced LTS: two configurations are behavioural equivalent if their induced LTS are bisimilar.

Other properties that can be analysed directly over include:

Contradictory effects.
A contradictory effect is when a step triggers both the activation and deactivation of the same edge.
The semantics in <ref> gives priority to disabling, but often these situations are the result of bad design decisions that should be avoided, and can be signalled as warnings.

Unreachable transitions.
Similarly to unreachable states, (hyper) edges that cannot be fired are usually undesirable or a result of a bad understanding of a system. Hence it is a property that can also be investigated directly over .

Products on reactive graphs.
Synchronous and asynchronous products of RG can be defined in the standard way. This section discusses
a new product, called intrusive product. It allows the connections between two RGs, i.e., the execution of an action in a given machine can interfere with the activation/deactivation actions of the other machine, and vice-versa.

Given two multi-action reactive graphs $M_1, M_2$, and $\Gamma^{\oplus},\Gamma^{\ominus} \subseteq E_1 \times E_2 \cup E_2 \times E_1$ is the set of intrusive edges between $M_1$ and $M_2$. The effects produced by $e \in E_{M_i}$ in $M_i$ is given for the set follow:

$\alpha_i(\Gamma^{\oplus},\Gamma^{\ominus},e) =
\big(\alpha_i \cup \mathsf{on}(e,\alpha_i) \cup \Gamma^{\oplus}(e) \big)
\setminus
\big(\mathsf{off}(e,\alpha_i) \cup \Gamma^{\ominus}(e) \big)$

<Ref> illustrates an
intrusive product of $\mi{Usr}\dline[\emptyset,\Gamma^{\ominus}] \mi{VM}$, where Usr is the upper RG and
$\Gamma^{\ominus} = \{
\tpl{\tpl{\mis{Insert},\text{\action{0.5\euro}},\allowbreak\mis{Coffee}},\tpl{\mis{User},\text{\action{Get product}},\allowbreak\mis{Select}}}
\}$.

An example of two reactive graphs and one intrusive edge

Formally the asynchronous product ($\dline$) is defined by the rules below.

\begin{equation*}\label{RO: LRG_PIA1}
\begin{array}{c}
\exists ~ e \cdot s_1 \xrightarrow{a} s_1' \in \alpha_1  ~\land~        \alpha_1' = \big( \alpha_1 \cup \mathsf{on}(e,\alpha_1) \big)
\backslash \mathsf{off}(e,\alpha_2) ~\land~\alpha_2' = \alpha_2(\Gamma^{\oplus},\Gamma^{\ominus},e)
\\\hline
\tpl{s_1,\alpha_1} \dline \tpl{s_2,\alpha_2} ~ \xrightarrow{a}  ~  \tpl{s'_1,\alpha_1'} \dline ,\tpl{s_2,\alpha_2'}
\end{array}
\end{equation*}

\begin{equation*}\label{RO: LRG_PIA2}
\begin{array}{c}
\exists ~ e \cdot s_2 \xrightarrow{a} s_2' \in \alpha_2  ~\land~        \alpha_2' = \big( \alpha_2 \cup \mathsf{on}(e,\alpha_2) \big)
\backslash \mathsf{off}(e,\alpha_2) ~\land~\alpha_1' = \alpha_1(\Gamma^{\oplus},\Gamma^{\ominus},e)
\\\hline
\tpl{s_1,\alpha_1} \dline \tpl{s_2,\alpha_2} ~ \xrightarrow{a}  ~
\tpl{s_1,\alpha_1'} \dline \tpl{s'_2,\alpha_2'}
\end{array}
\end{equation*}

The synchronous product ($\dwavy$) is based on shared actions, defined below.

\begin{equation*}\label{RG PS}\begin{array}{c}
\begin{array}{l}
\exists ~e_1 \cdot s_1 \xrightarrow{a} s_1' \in \alpha_1 \\
\exists ~e_2 \cdot s_2 \xrightarrow{a} s_2' \in \alpha_2
\end{array}
~ \land ~
\begin{array}{l}
\alpha_1' = \big( \alpha_1 \cup \mathsf{on}(e_1,\alpha_1) \cup \Gamma^{\oplus}(e_1) \big)
\backslash
\big( \mathsf{off}(e_1,\alpha_1) \cup \Gamma^{\ominus}(e_1)\big)
\\
\alpha_2' = \big( \alpha_2 \cup \mathsf{on}(e_2,\alpha_2) \cup \Gamma^{\oplus}(e_2) \big)
\backslash
\big( \mathsf{off}(e_2,\alpha_2) \cup \Gamma^{\ominus}(e_2)\big)
\end{array}
\\\hline
\tpl{s_1,\alpha_1} \dwavy \tpl{s_2,\alpha_2} ~ \xrightarrow{a}  ~
\tpl{s'_1,\alpha_1'} \dwavy%_\Gamma
\tpl{s'_2,\alpha_2'}
\end{array}
\end{equation*}

This product supports the modelling, e.g., of self-adaptive systems with a layer that manages a given system and the actual system being adapted <cit.>.

§ THE TOOL

Screenshot of the web interface of the tool

This section briefly presents the tool and its features. A screenshot of its web interface can be found in <ref> with the vending machine example from <ref>.
is open-source and developed in Scala, using the Mermaid library
[Mermaid is  popular markup language for diagrams, cf. https://mermaid.js.org]
to produces graphical representations of the reactive graph and its semantics. The tool is compiled to JavaScript that is used to build an interactive web page, using the CAOS library <cit.> which includes support to animate operational semantics and compare semantics.

Using the tool.
The tool can be used at <https://fm-dcc.github.io/MARGe>, illustrated in <ref> with our vending machine example.
The model is introduced using a textual description in the “” widget (top left). It can also be found in the list of examples (middle left). The remaining widgets provide our analysis and visualisations, and can be either collapsed (as the “”) or expanded (as the “”).

Available widgets. Some of the available widgets are described below.

*  – uses a textual notation, mimicking the mathematical structures, not yet optimised to be compact and maintainable.

*  – shows the graphical representation of a reactive graph. A simplified version without hyper edges and deactivated edges is depicted in the widget “”.

*  – allows the user to simulate the reactive graph by selecting, at each step, an active transition that should be taken. After selecting this transition the graph is updated, including the active edges and the current state.

*  – displays the underlying LTS by expanding all possible actions of the the reactive graph (up to a fixed bound).

*  – presents the number of states and edges of both the reactive graph and its encoded LTS. E.g., Our vending machine as a similar number of states and edges. But a variation (available online) with a limited stock (instead of limited money) uses 4 states, 5 ground edges, and 3 hyper edges, against 19 states and 20 edges in the encoded LTS.

*  – checks if two separated by `$\sim$' in the input program
are equivalent (i.e., bisimilar), providing either a bisimulation or an an explanation for not finding one.

*  – finds conflicts when they exist, i.e. traces until a transition that simultaneously tries to activate and deactivate.

*  – checks the existence of deadlocks in the behaviour of a given .

*  – this a set of widgets, presenting the different types of product introduced in this paper.

§ CONCLUSIONS AND FUTURE WORK

can provide a compact and insightful representation of a variety of reconfigurable scenarios, e.g., in the context of communication protocols <cit.> and in a biological setting <cit.>.
They are also closely related to van Benthem's game models with adversarial agents <cit.>
and to Areces et al.'s logic with reconfiguring modal operators <cit.>.
Extensions to with the paraconsistency paradigm have also been recently proposed <cit.>.
Most work on is theoretical, and a small effort has been done to provide tool support and automatization of results.
This paper presents the tool with basic editor and exploration mechanisms of , including specific analysis such as a search for contradictory effects.
As future work, we intent to improve the usability of (e.g., improving the input language), extend it to support fuzzy extensions (to measure, e.g., costs and rewards from applying reconfigurations <cit.>), and to integrate a model checker according to a suitable logic. The latter would be similar to how we integrated the mCRL2 toolset <cit.> to analyse connectors <cit.> and team automata <cit.>, based on a predecessor of CAOS <cit.>.

§.§.§ Acknowledgments

This work is supported by the FCT, the Portuguese funding agency for Science and Technology, with the projects UIDB/04106/2020 and PTDC/CCI-COM/4280/2021.
It was also supported by the CISTER Research Unit (UIDP/UIDB/04234/2020), financed by National Funds through FCT/MCTES and by project Ibex (ref. PTDC/CCI-COM/4280/2021) financed by national funds through FCT.

§ MODELLING OF A LARGER EXAMPLE IN

This sections presents an example describing a feature transitions system (FTS), borrowed from Cordy et al. <cit.>.
As in the original example, it uses a set of features that can be selected in an initial setup step, triggering the activation and deactivation of edges. Our reactive graph version of this FTS is depicted in <ref>. Variations of this model for reconfigurable FTS can also be made, where the feature selection can be modified outside the setup step.

[node distance=15mm, thick, main/.style = draw,rectangle, rounded corners = 2pt, action/.style = rectangle, fill = lightgray!50!white, text = black, rounded corners = 2pt, minimum size = 0.3cm]

[main] (setup) at (0,0)setup;
[main] (ready) at (4,0)ready;
[main] (received) at (8,0) received;
[main] (routed-safe) at (12,2)routed-safe;
[main] (routed-unsafe) at (12,-2)routed-unsafe;
[main] (sent) at (16,2)sent;
[main] (sent-encrypt) at (16,-2)sent-encrypt;

[-Stealth[length=3mm],out = 70, in = 110, looseness = 15] (setup)  to node[action](safe)safe (setup);
[-Stealth[length=3mm],out = -70, in = -110, looseness = 15] (setup)  to node[action](unsafe)unsafe (setup);
[-Stealth[length=3mm],out = 50, in = 130, looseness = 20] (setup)  to node[action](encrypt)encrypt (setup);
[-Stealth[length=3mm],out = -50, in = -130, looseness = 20] (setup)  to node[action](dencrypt)dencrypt (setup);
[-Stealth[length=3mm],out = 15, in = 165] (setup)  to node[action]- (ready);
[Stealth[length=3mm]-,out = -15, in = -165] (setup)  to node[action]- (ready);
[-Stealth[length=3mm]] (ready)  to node[action]receive (received);
[-Stealth[length=3mm],out=90,in=180] (received)  to node[action](rsafe)route(routed-safe);
[-Stealth[length=3mm],out=-90,in=180] (received)  to node[action](runsafe)route(routed-unsafe);
[-Stealth[length=3mm]] (routed-safe)  to node[action]send(sent);
[-Stealth[length=3mm]] (routed-unsafe)  to node[action](sencrypt)send(sent-encrypt);
[-Stealth[length=3mm],out=90,in=-90] (routed-unsafe)  to node[action](sdencrypt)send (sent);
[-Stealth[length=3mm],out=90,in=90] (sent)  to node[action]ready(ready);
[-Stealth[length=3mm],out=-90,in=-90] (sent-encrypt)  to node[action]ready (ready);

[on background layer]
[color = red,-Stealth[length=3mm],bend left= 1cm] (safe) to (rsafe);
[color = red,-Rays[length=10pt,width=10pt,line width= 1.5pt],bend left= 1cm] (safe) to (runsafe);
[color = red,-Rays[length=10pt,width=10pt,line width= 1.5pt],bend left= 1cm,out = -90, in = -90] (unsafe) to (rsafe);
[color = red,-Stealth[length=3mm],bend left= 1cm,out = -90, in = -90] (unsafe) to (runsafe);
[color = red,-Stealth[length=3mm],bend left= 1cm] (encrypt) to (sencrypt);
[color = red,-Rays[length=10pt,width=10pt,line width= 1.5pt],bend left= 1cm] (encrypt) to (sdencrypt);
[color = red,-Rays[length=10pt,width=10pt,line width= 1.5pt],bend left= 1cm,out = -90, in = -90] (dencrypt) to (sencrypt);
[color = red,-Stealth[length=3mm],bend left= 1cm,out = -90, in = -90] (dencrypt) to (sdencrypt);

Example adapted from <cit.>

A screenshot of analysing this reactive graph is presented in <ref>.

Screenshot of modelling a FTS

In <ref> we can see the explosion of states and the how $\mar$s can compactly represent this systems.
The reactive graph has 7 states, 14 ground edges, and 8 hyper edges, while the encoded LTS has 51 states and 101 edges.
One can confirm that this system has no deadlocks and no contradictory effects, using the widgets depicted in <ref>.
This means that is always possible go to another state, regardless of the current state, and there is no transition that can trigger contradictory effects.

Screenshot of the  widget with the LTS of the FTS example

Screenshot of the widgets that search for deadlocks and contradictory effects