Reactive graphs are directed graphs whose accessibility relation changes when their edges are crossed. I.e., at each point there is a current state and a current set of enabled edges, and non-enabled edges are blocked. The graph can then evolve by transitioning from the current state by an enabled edge, updating the state and the set of enabled edges. These simple structures can be used to directly model and reason about a wide range of phenomena, from computer science (e.g. modelling systems that can reconfigure their behaviour along their execution) to operational research (e.g. resource award or root planning systems). For instance, let us consider the case where we assume that enabled transitions are available resources; the crossing of one of such transitions should block itself since the resource was consumed. A possible transition “refill”, when crossed, would switch it on again.

In view of modelling complex systems in a modular way, we discuss new compositional constructions on reactive graphs. Beyond the formalisation of the standard synchronous and asynchronous products in this setting, we introduce a new product that permits “intrusive” action-interactions within different structures. The latter operator is meaningful to represent scenarios where actions in a model affect the behaviour of another one (e.g. on resource sharing scenarios). All of these operators are implemented in Marge, paving the way for the analysis of concrete examples by animating them and checking the behavioural properties of resultant structures.

To visualise and analyse reactive graphs enriched with labels, we recently developed the web-based tool Marge (available at https://github.com/Dtinas10/MARGe). Marge animates the operational semantics of reactive graphs and provides different graphical views to provide insights into concrete systems. The preservation of behavioural properties along these constructions will also be discussed, as well as, the lines for an effective specification framework for program development based on this semantics.