ReactICS is a toolkit that allows for verification of Reaction Systems. The toolkit consists of two separate modules implementing:
ReactICS GUI offers a graphical user interface allowing for editing the reaction system details and model checking using BDD module.
More on ReactICS can be found at The Reactics Webpage.
Reaction Systems are a formalism inspired by the functioning of living cells. They allow for specifying and analysing computational processes in which reactions operate on sets of molecules.
The behaviour of a reaction system is determined by the interactions of its reactions, which are based on the mechanisms of facilitation and inhibition. The formal treatment of reaction systems is qualitative and there is no direct representation of the number of molecules involved in reactions.
A Distributed Reaction System is a computational model in which multiple autonomous processes (aka. agents) interact locally through rule-based reactions. Each agent operates independently (without any central controller—coordination), processing inputs and producing outputs based on predefined reactions, and their collective behavior leads to complex system dynamics.
More on reaction system can be found at The Reaction System Webpage
ReactICS GUI allows to:
The structure of distributed reaction system can be edited using the following buttons from the distributed reaction system control panel:
The details of a single process can be edited using the following buttons in the process panel:
Verification of formulas against a system specification is done after selecting desired formulas and clicking Evaluate button. The result of the verification (True/False), as well as time and memory used are presented next to each verified formula.
Clicking the Reset button resets the status of the model checking. Note that updating the reaction system specification (the list of processes, details of the reactions or the content automaton structure) the results of model checking, if any, are reset automatically.
To create or edit the context automaton structure a proper edit mode should be set using the edit mode panel.
The type of the newly created object (state or edge) is set by checking the proper toggle button. With no button checked, one can transform the net by moving states around, etc. (see below for more details).
A new state is created by left-clicking the edit area (the main part of the component). As it is customary in automata theory, states are numbered separately starting from 1. The types of states are distinguished by shape and colour: the initial state is depicted as a square, all other states are depicted as circles. Moreover, hovering the mouse above a state allows to see its full description containing both its name and its (distinct) number.
The details of a state can be edited by right-clicking the existing state and choosing the right option from the popup menu:
A directed edge between two states is created by left-clicking both its endpoints in correct order. Each edge may contain several transitions, each of them defined by a context (additional entities provided for active processes/agents) and a guard (a condition required by the transition to execute). The list of transitions may be edited by right-clicking the existing edge and choosing the Nondeterministic transitions popup menu.
Hovering the mouse above an edge allows to see the full list of transitions including context and guards.
Switching the toggle button Delete on allows removing context automaton elements. Each left-clicked element is removed from the automaton grapn. Moreover, the entire context automaton graph may be deleted by clicking the Clear button.
Any state of the automaton may be picked and dragged around the edit area to obtain the desired graph shape. It is also possible to select multiple states and move them together at the same time. After CTRL + left-click on a particular state the entire automaton graph is shifted to be centered on the clicked state. Checking the Lock relative nodes positions checkbox locks the relative positions of the states. In that case, dragging a single state moves the entire automaton graph. Moreover, using mouse scroll the automaton graph view can be zoomed in and out.
The component offers the visualisation of the transition system representing the state space of the reaction systems. The initial state is depicted as a square, all other states are depicted as circles. There is a directed edge connecting the state Si to the state Sj if Sf is reachable from Si by a single computation step of the reaction system.
The component has two separate instances represented by two separate tabs in the application window. The first visualises the complete state space of the reaction system, where each state is represented by sets of entities possessed by each agent and the current context automaton state. The second visualises the compressed state space, where context automaton states are ignored (states are represented only by the sets of entities possessed by each agent).
Computation is done by pressing Update transition system button. The reaction system structure should be loaded from the file or edited manually for the computation to be possible.
Note that no matter in which component the Update transition system button is pressed, the transition system structure will be updated in both.
Hovering the mouse above a state allows to see its full description: entities possessed by each process/agent and the context automaton state (not present in the case of the compressed graph).
Any state of the transition system may be picked and dragged around the edit area to obtain the desired graph shape. It is also possible to select multiple states and move them together at the same time. After CTRL + left-click on a particular state the entire transition system graph is shifted to be centered on the clicked state. Checking the Lock relative nodes positions checkbox locks the relative positions of the states. In that case, dragging a single state moves the entire transition system graph. Moreover, using mouse scroll the transition system graph view can be zoomed in and out.
Model checking is handled by the component at the bottom of the application window. The properties of the analysed system are expressed as formulas following rsCTLK syntax.
The list of formulas may be modified using the following buttons:
Verification of formulas against a system specification is done after selecting desired formulas and clicking Evaluate button. The result of the verification (True/False), as well as time and memory used are presented next to each verified formula.
Clicking the Reset button resets the status of the model checking. Note that updating the reaction system specification (the list of processes, details of the reactions or the content automaton structure) the results of model checking, if any, are reset automatically.