Two main problems where targeted during the design: simulating the behavior of Reaction Systems, RS processes and other operations on LTS, and interacting with the user in a intuitive manner. The programming language chosen was Rust\cite{rust_2025}, since it offered good performance and ease of development.
The ReactionSystems project follows a modular architecture and clear design principles to mirror the theoretical model; it implements procedures over RS as pure rust functions and is structured as a library. It also provides a crude Command Line Interface (CLI) for some of the functions provided.
The CLI expects a path to a file with a RS definition and some instructions to execute.
In the second Git repository a native and web application is implemented in Rust and in WebAssembly\cite{WebAssemblyCoreSpecification2} generated from Rust code. The web application consists of only static files and as such may be served by a simple HTTP server.
In the signature of the functions, types will be displayed in teletype font. The decorator \({}^{?}\) will be used for both option types and for result types without distinction.
The design is structured to faithfully implement the reaction system formalism while remaining flexible.
It provides a foundation that matches theoretical definitions (ensuring correctness) and supports further expansion (such as adding optimization, visualization, or integration with other tools) by maintaining a clean separation between the model representation and the execution logic.
Since the language Rust supports object-oriented programming via traits, but lacks generic inheritance, the design of the basic building blocks of RSs are designed around this limitation.
Usually a basic trait is provided for each of them and an extension of the trait is implemented for all structures that implement the basic trait.
Since it is not practical for a user to specify the structures in Rust, a syntax for the basic structures has been specified. This syntax tries to remain compatible, as much as possible, with ones from previous software. To develop the parser, LALRPOP\cite{Burgener2025} was chosen as the parser generator framework. LALRPOP code is transpiled to Rust code via macros and then compiled to machine code.
Entities are the most basic data structure that a RS need to keep track of. They don't have a specified interface and are instead treated only in sets.
Positive elements are also defined and have a state, either \texttt{Positive} or \texttt{Negative}.
Since internally entities are represented as integers, a structure that keeps track of assignment between strings and integer is provided (\(\texttt{Translator}\)). This poses a problem with the default methods for formatting available in Rust, since for the trait \(\texttt{Display}\) and \(\texttt{Debug}\) only the structure itself can be used to generate the string. The trait \(\texttt{PrintableWithTranslator}\) and the structure \(\texttt{Formatter}\) solve this issue by incorporating the \(\texttt{Translator}\) into the struct. \(\texttt{Display}\) is then implemented on the generic structure \(\texttt{Translator}\).
\item\(\texttt{is\_subset}(a, b)\to\texttt{bool}\), which should return true if \(a \subseteq b\);
\item\(\texttt{is\_disjoint}(a, b)\to\texttt{bool}\), which should return true if \(a \cap b =\emptyset\);
\item\(\texttt{union}(a, b)\to\texttt{set}\), which should return \(a \cup b\);
\item\(\texttt{push}(a, b)\), which should replace \(a\) with \(a \cup b\) in place\label{push_set};
\item\(\texttt{intersection}(a, b)\to\texttt{set}\), which should return \(a \cap b\);
\item\(\texttt{subtraction}(a, b)\to\texttt{set}\), which should return \(a \setminus b\);
\item\(\texttt{len}(a)\to\texttt{int}\), which should return the number of elements in \(a\);
\item\(\texttt{is\_empty}(a)\to\texttt{bool}\), which should return true if \(a\) has no elements, false otherwise;
\item\(\texttt{contains}(a, e: \texttt{entity})\to\texttt{bool}\), which should return \(e \in a\);
\item\(\texttt{add}(a, e: \texttt{element})\), which should add the element \(e\) to \(a\) in place.
\end{itemize}
Some other procedures are required for ease of use:
\begin{itemize}
\item\(\texttt{extend}(a, b^?)\), which should extend \(a\) with \(a \cup b\) if \(b\) is a non-null value, and leave \(a\) unchanged otherwise, similar to \(\texttt{push}\) (\ref{push_set}).
\end{itemize}
Two other procedures are implemented for all structs that implement the BasicSet trait:
\begin{itemize}
\item\(\texttt{iter}(a)\to\texttt{iterable}\), which returns an iterator over the elements of the set \(a\);
\item\(\texttt{split}(a, \mathit{trace}: \texttt{[set]})\to{(\texttt{[set]}, \texttt{[set]})}^{?}\), which returns the prefix and the loop part of a trace.
\end{itemize}
Both normal sets and positive sets satisfy this interface, but have additional specific functions for converting between the two.
\item\(\texttt{enabled}(r, \mathit{state}: \texttt{set})\to\texttt{bool}\), which returns true if the reaction is enabled given the entities supplied by \(\mathit{state}\);
\item\(\texttt{compute\_step}(r, \mathit{state}: \texttt{set})\to\texttt{set}^{?}\), which returns the products of the reaction if it is enabled by \(\mathit{state}\).
\end{itemize}
All reactions that satisfy the basic trait automatically implement the following methods:
\begin{itemize}
\item\(\texttt{find\_loop}(\mathit{rs}: \texttt{[reaction]}, \mathit{entities}: \texttt{set}, q: \texttt{set})\to\texttt{([set], [set])}\), which finds a loop and returns the sets that make up the prefix and the loop separately;
\item\(\texttt{find\_only\_loop}(\mathit{rs}: \texttt{[reaction]}, \mathit{entities}: \texttt{set}, q: \texttt{set})\to\texttt{[set]}\), which finds a loop and returns the sets that form it;
\item\(\texttt{find\_prefix\_len\_loop}(\mathit{rs}: \texttt{[reaction]}, \mathit{entities}: \texttt{set}, q: \texttt{set})\)\\\(\to\texttt{(integer, [set])}\), which finds a loop and returns the length of the prefix and the sequence of sets that compose the loop;
Process structures mirror the structure of RS processes as described in Section\ \ref{SOS_rules_section}. Since there is not much behavior that is shared between implementations and since usually they are used with pattern matching, the trait that describe a basic process is very simple.
\begin{itemize}
\item\(\texttt{concat}(a, b)\to\texttt{process}\), which returns a new process \(a \vert b\) flattened with regards to parallel composition;
\item\(\texttt{all\_elements}(a)\to\texttt{set}\), which returns all the entities used in the process;
\item\(\texttt{filter\_delta}(a, \mathit{id}: \texttt{entity})\to\texttt{set}^{?}\), which returns the first rule \(X = Q.X\) for any symbol \(X\) and any set \(Q\).
Since one RS process may have more than one possible next system when evaluating, there is a need to express all possible choices for next states.
The structure choices represents all those possible continuations, associating a set with a process. The set signifies all the entities that are provided by the context by choosing that context.
One particular operation called \texttt{shuffle} is needed: given two choices structures \( c_1\) and \( c_2\) where \(c_i : \texttt{set}\rightharpoonup\texttt{process}, i \in\{1, 2\}\), it generates a new choices structure \(c'\) such that \(\forall s_1\in\mathit{domain}(c_1) . (\forall s_2\in\mathit{domain}(c_2) . \mathit{domain}(c')\ni(s_1\cup s_2)\land c'(s_1\cup s_2)=\texttt{concat}(c_1(s_1), c_2(s_2)))\), where \(\rightharpoonup\) symbolizes a partial function.
Intuitively it is all the possible combinations of two parallel processes.
An environment can be thought as an association between variable names and processes.
The basic interface requires the following methods:
\begin{itemize}
\item\(\texttt{get}(a, k: \texttt{entity})\to\texttt{process}\), which returns the process associated with the variable \(k\);
\item\(\texttt{all\_elements}(a)\to\texttt{set}\), which returns all the entities used in any of the processes;
\item\(\texttt{unfold}(a, \mathit{context}: \texttt{process}, \mathit{s}: \texttt{set})\to\texttt{choices}^{?}\), which returns the list of choices for the context, given the process definitions environment and is used to generate the next systems with the SOS rules.
They all try to find a loop and return some information about the found loop. The \(\texttt{\_named}\) variants require a variable symbol for which in the environment there is an association to a process with the form \( X = Q.\texttt{rec}(X)= Q.X\), where \(Q\) is a set and \(X\) is a variable name. The others instead finds all the symbols that satisfy the constraint and uses them all.
Function \(\texttt{lollipops\_decomposed}\) returns the trace of sets for the prefix and the trace of sets for the loop for each recursive variable.\\
\(\texttt{lollipops\_prefix\_len\_loop\_decomposed}\) returns the length of the prefix and the trace of the loop for each recursive variable.
\(\texttt{lollipops\_only\_loop\_decomposed}\) returns the trace of the loop for each recursive variable.\vspace{1em}
The method \(\texttt{to\_transitions\_iterator}\) should return an iterator over all the possible evaluations of the system. Likewise \(\texttt{to\_slicing\_iterator}\) should return an iterator over the same outgoing edges, but with information that support the creation of a trace to be used for slicing.
The two methods \(\texttt{context\_elements}\) and \(\texttt{products\_elements}\) should return the set of entities that are related to the context and the one related to the reactions. Since it may be a computationally expensive calculation, the result is cached in the structures.
The heuristic that decides which elements belong to the context and which belong to the reactions might give incorrect results, so methods are provided that override the calculated values.
Other methods are implemented for all structures that satisfy the previous interface:
\begin{itemize}
\item\(\texttt{unfold}(\mathit{sys})\to\texttt{choices}^{?}\), which, by calling the same method of the environment, returns the list of choices for the context;
\item\(\texttt{run}(\mathit{sys})\to\texttt{[system]}^{?}\), which computes the sequence of systems for the leftmost execution;
\item\(\texttt{digraph}(\mathit{sys})\to\texttt{graph}^{?}\), which computes the graph generated by the execution of the system;
\item\(\texttt{target}(\mathit{sys})\to\texttt{(integer, set)}^{?}\), which returns the state in one of the terminal states and the number of steps to arrive at the last state;\label{function_target}
\item\(\texttt{slice\_trace}(\mathit{sys})\to\texttt{trace}^{?}\), which generates, similarly to \(\texttt{run}\), a trace appropriate to run slicing calculations over;
\item\(\texttt{lollipops}(\mathit{sys})\to\texttt{[([set], [set])]}\), similar to the method\\\(\texttt{lollipops\_decomposed}\) provided by \(\texttt{environment}\).
\item\(\texttt{lollipops\_only\_loop\_named}(\mathit{sys}, el: \texttt{element})\to\texttt{[[set]]}^{?}\), similar to the me\-thod provided by \(\texttt{environment}\), returns the sequence of entities in the loop individuated by the variable name \(el\) in the environment.
While writing systems, occurs often to forget an element or swap elements names. This type of user error is particularly difficult to spot since most element names are not easily recognizable and the system grammar is particularly dense in information. A useful method to mitigate these problems is provided: \(\texttt{statistics}\). For the structure \(\texttt{System}\) a static analysis of the entities of the system is run and various parameters are checked and reported.
The label structure holds the information about how entities are used in the production of a system and are the labels on the edges of the graphs. Since the only use is to hold data, no meaningful method is required.\vspace{2em}
The project uses petgraph\cite{Borgna2025} as graph data structure library. \textit{petgraph} provides several graph types, but the only one used is \(\texttt{Graph}\), since it provided the best performance during testing. The library has methods for converting the graph structures into {Dot Language}\cite{graphviz_2025} and {GraphML File Format}\cite{graphml_2025}. The Dot methods where found to be not powerful enough and where partially rewritten in the file \href{https://github.com/elvisrossi/ReactionSystems/blob/master/rsprocess/src/dot.rs}{\(\texttt{dot.rs}\)}.
$\texttt{Hide}$ ignores the content of the node and prints the empty string, $\texttt{Entities}$ prints the list of entities currently available in the system, $\texttt{MaskEntities}\ S$ prints the list of entities masked by a specified set \(S\), $\texttt{ExcludeEntities}\ S$ prints the list of entities except for the entities specified by the set \(S\), $\texttt{Context}$ prints the context of the system, $\texttt{UncommonEntities}$ prints only the entities that are not shared between all the nodes in the graph, $\texttt{MaskUncommonEntities}\ S$ prints the entities not shared between all the nodes in the graph and masked by a specified set \(S\).\vspace*{\fill}
Four version of each base option is available: normal, \(\texttt{Mask}\) which masks the normal set of entities with a specified set, \(\texttt{Uncommon}\) which considers only the entities that are not shared between all edges of the graph, and \(\texttt{UncommonMask}\) which combines the two functionalities. The base options return the corresponding entities available in the label.\vspace{1em}
Where \\&\(C\) -> {is a string that specifies the color\\ of the node} : % chktex 26
;; % chktex 26
\(S\) -> is a sets of entities : % chktex 26
;; % chktex 26
\(x\) -> is a variable : % chktex 26
;; % chktex 26
\end{bnf}
\captionsetup{type=table, name=\textbf{Syntax}}
\caption{Syntax for \(\texttt{NodeColor}\)}\label{bnf_node_color}
\end{minipage}\vspace{1em}
The \(\texttt{NodeColor}\) structure assigns the first correct color to the node. The structure can be thought of as a list of pairs; each pair has an entry that evaluated returns true or false, and an entry that holds the desired color of the node.
To find the correct color, the list is scanned until the first pair that returns true and the color is assigned. If no pair returns true, a default value is assigned, specified after \(\texttt{!}\). The possible functions expressible by the grammar are the ones expressed by \(E\) and query either the entities available or the current context.
Where \\&\(C\) -> {is a string that specifies the color\\ of the node} : % chktex 26
;; % chktex 26
\(S\) -> is a sets of entities : % chktex 26
;; % chktex 26
\(x\) -> is a variable : % chktex 26
;; % chktex 26
\end{bnf}
\captionsetup{type=table, name=\textbf{Syntax}}
\caption{Syntax for \(\texttt{EdgeColor}\)}\label{bnf_edge_color}
\end{minipage}\vspace{1em}
\(\texttt{EdgeColor}\) behaves in a similar manner as \(\texttt{NodeColor}\), except the base structure is a \(\texttt{Label}\), so every field is a \(\texttt{Set}\).
Only one structure for slicing trace is provided, but is made to work with both RS and Positive RS with generics. The only method they have is \(\texttt{slice}(\mathit{trace}, \mathit{marking}: \texttt{set})\to\texttt{trace}^{?}\) which returns, if successful, a new sliced trace.
In the workspace \(\texttt{bisimilarity}\) the algorithms by Kanellakis and Smolka, and Paige and Tarjan are implemented over generic graphs. Instead of an implementation over graphs with generic parameters, the input have to implement generic traits from the \(\texttt{petgraph}\) library, making it possible to use with different types of graph, for example spare graphs or matrix graphs.
One key feature was the ability to control via a domain specific language the labels on the edges of the graphs. The developed language is able to also specify values over nodes such that nodes with equal value may be collapsed into one node with outgoing and incoming edges inherited from the original nodes. The code for the typechecking and execution is available in the library \(\texttt{assert}\).
The language has way to define subroutines or functions, has no while loop and limited for loop construction, so that the execution always terminates.\vspace{1em}
\(\texttt{relabel}\) has, in its syntax, the first token equal to \(\texttt{label}\); it also has as special variables \(\texttt{label}\) and \(\texttt{edge}\) that function as input, with \(\texttt{edge.label}==\texttt{label}\). It's used for grouping labels before calculating bisimilarity. \(\texttt{grouping}\) has, in its syntax, the first token equal to \(\texttt{node}\) and has as special variables \(\texttt{entities}\) and \(\texttt{node}\) that function as input, with \(\texttt{node.system.SystemEntities}==\texttt{entities}\). It's used for grouping nodes.
\(\texttt{positive\_relabel}\) and \(\texttt{positive\_grouping}\) have as first token \(\texttt{label}\) and \(\texttt{node}\) respectively and behave in a similar manner compared to their respective functions over RS.%
The template language requires two structures to function relating to the input of the language: a type structure and a value structure. The trait \(\texttt{SpecialVariables}\) holds all the necessary functions that need to be implemented for the special variables to function. Finally the generic language can have the two functions \(\texttt{typecheck}\) and \(\texttt{execute}\) implemented.
The language is very limited and is only designed for simple algorithms since there is no scoping. Typechecking consists in only asserting acceptable types for unary and binary functions, correct type in range declarations and for all return statements to have the same type.
Two workspaces are provided for parsing the structures above. \(\texttt{Grammar}\) creates only one endpoint that parses a system and a list of instructions. Those instructions are then executed via the library \(\texttt{execution}\). A simple CLI has been implemented in the workspace \(\texttt{analysis}\), with proper error formatting for LALRPOP errors.
\begin{subsection}{Experiments and Frequency}\label{experiment}
An experiment is a list of weights and a list of sets of same length. The sets are used as entities given in addition to the context entities when computing the RS.\ The resulting trace is then synthesized into relative frequencies. The methods offered by \(\texttt{Frequency}\) and \(\texttt{PositiveFrequency}\) are:
\item\(\texttt{naive\_frequency}(sys: \texttt{system})\to\texttt{frequency}^{?}\), which computes the relative frequency of each entity in all traversed states, assuming the computation is finite;\label{function_naive_frequency}
\item\(\texttt{loop\_frequency}(sys: \texttt{system}, symbol: \texttt{IdType})\to\texttt{frequency}\), which computes the relative frequency of each entity in each state of the encountered loop, assuming the system stabilizes in a loop;
\item\(\texttt{limit\_frequency}(experiment: \texttt{[set]}, reactions: \texttt{[reaction]}, entities: \texttt{set})\to\texttt{frequency}^{?}\), which computes the relative frequency of each entity in the states of the last loop by providing repeatedly the sets in the experiment until the system stabilizes in a loop;
\item\(\texttt{fast\_frequency}(experiment: \texttt{[set]}, reactions: \texttt{[reaction]}, entities: \texttt{set},\\ weights: \texttt{[int]})\to\texttt{frequency}^{?}\), which computes the weighted relative frequency of each entity in any of the loops.
The command line interface provided by the workspace \(\texttt{analysis}\) expects as input a path to a file with a RS and some instructions, reads the file, executes the instructions and returns the result in the forms specified. The syntax for specifying instructions is as follows:\vspace{1em}
The instruction \(\texttt{Stats}\) returns static information and statistics about the system. \(\texttt{Target}\) and \(\texttt{Run}\) return the results of the function with the same name defined in section\ \ref{function_target}. \(\texttt{Loop}\) returns the result of the function \(\texttt{lollipops\_only\_loop\_named}\) described in the same section. \(\texttt{Frequency}\) returns the results of \(\texttt{naive\_frequency}\) as described in section\ \ref{function_naive_frequency}. \(\texttt{LimitFrequency}\) and \(\texttt{FastFrequency}\) require a path to an experiment, with syntax described in\ \ref{experiment}, and they return the result of \(\texttt{limit\_frequency}\) and \(\texttt{fast\_frequency}\) respectively. \(\texttt{Digraph}\) may take a function \(group\) that groups together nodes that have the same output, described in section\ \ref{bisimilarity_design}. The graphs can be either saved as a Dot or GraphML file or serialized directly. \(\texttt{Bisimilarity}\) takes a path to another instruction file, whose instructions are ignored, and returns if the two systems are bisimilar. The results can be saved to a file or print to screen or both.
During development of ReactionSystems, a need for a more intuitive interaction with the structures presented itself. Since all the operations on the types where already limited and
The library {\(\texttt{egui\_node\_graph2}\)}\cite{egui_node_graph22024} was chosen since it offered customizability, performance and ease of programming. The library unfortunately lacked compatibility with the most recent version of {\(\texttt{egui}\)}\cite{Ernerfeldt2025}, so it is included as a workspace and modified to fit better the need of the project.
This way a couple of visual bugs present in the original code have also been fixed.
\(\texttt{egui\_node\_graph2}\) is based on the library \(\texttt{egui}\), which is an immediate mode GUI. % chktex 13
It differentiate itself from retained mode GUIs by having all the elements specified at every frame; this eases programming at the expense of performance. The trade-off is favorable since most of the computation will be on the algorithms over RS and the number of elements of the UI will remain small in most cases.
All the functions previously described are available as ``nodes'' in the GUI program. Each takes one or more inputs, colored by type, and prevents wrong types from connecting, reducing user error when connecting similarly colored types.
Since at every step all of the GUI is recalculated, a robust cache structure is needed.
The cache developed keeps track of the modified nodes and only recomputes if necessary, exploiting the structure of the graph.
The library \(\texttt{egui\_node\_graph2}\) was also chosen for its ability to create a web application directly from Rust code. The web application is limited; there is no interaction with the file system and no true multi-threading. These limitations are imposed by WebAssembly itself, not by the transpilation from Rust.
The native application executes the expressed instructions in a separate thread and returns the result to the GUI thread to be displayed. Thus the web application may ``freeze'' and become unresponsive with long calculations.
Both native and web applications have the ability to save the current state and resume. The saved state is stored in the browser cache in the web application and in special directories in the native one:
The native application also has the ability to save and load the state from a file. The files have by default the extension ``\(\texttt{.ron}\)''. The web version has no ability to interact with the file system due to a limitation of WebAssembly.
The file structure can be seen in figure\ \ref{save_file_structure}, where ``state'' refers to the state of the GUI, ``translator'' refers to the \(\texttt{Translator}\) structure used to encode entities names into fixed sized integers, and ``cache'' refers to the cache structure for the GUI.\ Version number is a little-endian \(\texttt{u64}\) that encodes the version number of the application; if different from the version of the application, a warning will be issued, but the application will try and load the state anyway. Each ``length'' field is a little-endian \(\texttt{u64}\) and indicates the length in bytes of the corresponding field.
The user can request the result of a computation by interacting with the button ``\textit{Set active}'' under most of the windows. A panel on the right of the screen appears with the computed result. The nodes ``Save string to file'', ``Save SVG'' and ``Save Rasterized SVG'' instead have a button ``\textit{Write}'' that writes to file the result. The node ``Read a file'' has an extra button ``\textit{Update file}'' that reads again the file from disk since a filewatcher has not been implemented.
Since the generated graphs were often times immediately converted to DOT files and rendered to SVG, a native renderer is included that can create PNG images of the supplied graph. They are then rendered to screen. This reduces greatly the time switching between software to achieve the same result.
\fcolorbox{black}{color_Error}{\makebox[4mm][l]{\strut}}&\(\texttt{Error}\)& Structure that holds error messages \\
\fcolorbox{black}{color_String}{\makebox[4mm][l]{\strut}}&\(\texttt{String}\)& A string \\
\fcolorbox{black}{color_Path}{\makebox[4mm][l]{\strut}}&\(\texttt{Path}\)& A path to a file \\
\fcolorbox{black}{color_Svg}{\makebox[4mm][l]{\strut}}&\(\texttt{Svg}\)& A structure for creating and rendering SVG \\
\fcolorbox{black}{color_PositiveInt}{\makebox[4mm][l]{\strut}}&\(\texttt{PositiveInt}\)& Integer in \(\mathbb{N}\)\\
\fcolorbox{black}{color_Symbol}{\makebox[4mm][l]{\strut}}&\(\texttt{Symbol}\)& A single symbol, see section\ \ref{design_entities}\\
\fcolorbox{black}{color_System}{\makebox[4mm][l]{\strut}}&\(\texttt{System}\)& see section\ \ref{design_system}\\
\fcolorbox{black}{color_Environment}{\makebox[4mm][l]{\strut}}&\(\texttt{Environment}\)& see section\ \ref{design_environment}\\
\fcolorbox{black}{color_Set}{\makebox[4mm][l]{\strut}}&\(\texttt{Set}\)& see section\ \ref{design_set}\\
\fcolorbox{black}{color_Context}{\makebox[4mm][l]{\strut}}&\(\texttt{Context}\)& see section\ \ref{design_process}\\
\fcolorbox{black}{color_Reactions}{\makebox[4mm][l]{\strut}}&\(\texttt{Reactions}\)& see section\ \ref{design_reaction}\\
\fcolorbox{black}{color_Experiment}{\makebox[4mm][l]{\strut}}&\(\texttt{Experiment}\)& see section\ \ref{experiment}\\
\fcolorbox{black}{color_PositiveSystem}{\makebox[4mm][l]{\strut}}&\(\texttt{PositiveSystem}\)& see section\ \ref{design_system}\\
\fcolorbox{black}{color_PositiveEnvironment}{\makebox[4mm][l]{\strut}}&\(\texttt{PositiveEnvironment}\)& see section\ \ref{design_environment}\\
\fcolorbox{black}{color_PositiveSet}{\makebox[4mm][l]{\strut}}&\(\texttt{PositiveSet}\)& see section\ \ref{design_set}\\
\fcolorbox{black}{color_PositiveContext}{\makebox[4mm][l]{\strut}}&\(\texttt{PositiveContext}\)& see section\ \ref{design_process}\\
\fcolorbox{black}{color_PositiveReactions}{\makebox[4mm][l]{\strut}}&\(\texttt{PositiveReactions}\)& see section\ \ref{design_reaction}\\
\fcolorbox{black}{color_Trace}{\makebox[4mm][l]{\strut}}&\(\texttt{Trace}\)& see section\ \ref{design_trace}\\
\fcolorbox{black}{color_PositiveTrace}{\makebox[4mm][l]{\strut}}&\(\texttt{PositiveTrace}\)& see section\ \ref{design_trace}\\
\fcolorbox{black}{color_Graph}{\makebox[4mm][l]{\strut}}&\(\texttt{Graph}\)& see section\ \ref{design_graph}\\
\fcolorbox{black}{color_PositiveGraph}{\makebox[4mm][l]{\strut}}&\(\texttt{PositiveGraph}\)& see section\ \ref{design_graph}\\
\fcolorbox{black}{color_DisplayNode}{\makebox[4mm][l]{\strut}}&\(\texttt{DisplayNode}\)& see section\ \ref{design_graph}\\
\fcolorbox{black}{color_DisplayEdge}{\makebox[4mm][l]{\strut}}&\(\texttt{DisplayEdge}\)& see section\ \ref{design_graph}\\
\fcolorbox{black}{color_ColorNode}{\makebox[4mm][l]{\strut}}&\(\texttt{ColorNode}\)& see section\ \ref{design_graph}\\
\fcolorbox{black}{color_ColorEdge}{\makebox[4mm][l]{\strut}}&\(\texttt{ColorEdge}\)& see section\ \ref{design_graph}\\
\fcolorbox{black}{color_AssertFunction}{\makebox[4mm][l]{\strut}}&\(\texttt{AssertFunction}\)& see section\ \ref{bisimilarity_design}\\
\fcolorbox{black}{color_GroupFunction}{\makebox[4mm][l]{\strut}}&\(\texttt{GroupFunction}\)& see section\ \ref{bisimilarity_design}\\
\fcolorbox{black}{color_PositiveAssertFunction}{\makebox[4mm][l]{\strut}}&\(\texttt{PositiveAssertFunction}\)& see section\ \ref{bisimilarity_design}\\
\fcolorbox{black}{color_PositiveGroupFunction}{\makebox[4mm][l]{\strut}}&\(\texttt{PositiveGroupFunction}\)& see section\ \ref{bisimilarity_design}\\
\(\texttt{String}\)&\fcolorbox{black}{color_String}{\makebox[4mm][l]{\strut}}&\fcolorbox{black}{color_String}{\makebox[4mm][l]{\strut}}& Creates a string \\
\(\texttt{Path}\)&\fcolorbox{black}{color_String}{\makebox[4mm][l]{\strut}}&\fcolorbox{black}{color_Path}{\makebox[4mm][l]{\strut}}& Creates a path from a string \\
\(\texttt{Read file}\)&\fcolorbox{black}{color_Path}{\makebox[4mm][l]{\strut}}&\fcolorbox{black}{color_String}{\makebox[4mm][l]{\strut}}& Reads a file into a string \\
\(\texttt{Save string to file}\)&\fcolorbox{black}{color_Path}{\makebox[4mm][l]{\strut}}\fcolorbox{black}{color_String}{\makebox[4mm][l]{\strut}}&& Save a string to a file \\
\(\texttt{Symbol}\)&\fcolorbox{black}{color_String}{\makebox[4mm][l]{\strut}}&\fcolorbox{black}{color_Symbol}{\makebox[4mm][l]{\strut}}& Creates a symbol from a string \\
\(\texttt{Sleep}\)&\fcolorbox{black}{color_PositiveInt}{\makebox[4mm][l]{\strut}}&\fcolorbox{black}{color_PositiveInt}{\makebox[4mm][l]{\strut}}& Waits for selected number of seconds \\
\(\texttt{Dot file to SVG}\)&\fcolorbox{black}{color_String}{\makebox[4mm][l]{\strut}}&\fcolorbox{black}{color_Svg}{\makebox[4mm][l]{\strut}}& Parses a Dot file string into an SVG \\
\(\texttt{Save SVG}\)&\fcolorbox{black}{color_Path}{\makebox[4mm][l]{\strut}}\fcolorbox{black}{color_Svg}{\makebox[4mm][l]{\strut}}&& Saves an SVG \\
\(\texttt{Save Rasterized SVG}\)&\fcolorbox{black}{color_Path}{\makebox[4mm][l]{\strut}}\fcolorbox{black}{color_Svg}{\makebox[4mm][l]{\strut}}&& Saves an SVG as a picture \\
\(\texttt{Create System}\)&\fcolorbox{black}{color_String}{\makebox[4mm][l]{\strut}}&\fcolorbox{black}{color_System}{\makebox[4mm][l]{\strut}}& Creates system from string \\
\(\texttt{Create Positive System}\)&\fcolorbox{black}{color_System}{\makebox[4mm][l]{\strut}}&\fcolorbox{black}{color_PositiveSystem}{\makebox[4mm][l]{\strut}}& Creates positive system from system \\
\(\texttt{Compose System}\)&\fcolorbox{black}{color_Environment}{\makebox[4mm][l]{\strut}}\fcolorbox{black}{color_Set}{\makebox[4mm][l]{\strut}}\fcolorbox{black}{color_Context}{\makebox[4mm][l]{\strut}}\fcolorbox{black}{color_Reactions}{\makebox[4mm][l]{\strut}}&\fcolorbox{black}{color_System}{\makebox[4mm][l]{\strut}}&{Composes system from\\individual structures}\\
\(\texttt{Convert to Positive Set}\)&\fcolorbox{black}{color_Set}{\makebox[4mm][l]{\strut}}&\fcolorbox{black}{color_PositiveSet}{\makebox[4mm][l]{\strut}}&\\
\(\texttt{Target of Positive RS}\)&\fcolorbox{black}{color_PositiveSystem}{\makebox[4mm][l]{\strut}}\fcolorbox{black}{color_PositiveInt}{\makebox[4mm][l]{\strut}}&\fcolorbox{black}{color_String}{\makebox[4mm][l]{\strut}}&\\
\(\texttt{Run of Positive RS}\)&\fcolorbox{black}{color_PositiveSystem}{\makebox[4mm][l]{\strut}}\fcolorbox{black}{color_PositiveInt}{\makebox[4mm][l]{\strut}}&\fcolorbox{black}{color_String}{\makebox[4mm][l]{\strut}}&\\
\(\texttt{Loop}\)&\fcolorbox{black}{color_System}{\makebox[4mm][l]{\strut}}\fcolorbox{black}{color_Symbol}{\makebox[4mm][l]{\strut}}&\fcolorbox{black}{color_String}{\makebox[4mm][l]{\strut}}&{Applies function\\\(\texttt{lollipops\_only\_loop\_named}\) to RS}\\
\(\texttt{Loop of Positive RS}\)&\fcolorbox{black}{color_PositiveSystem}{\makebox[4mm][l]{\strut}}\fcolorbox{black}{color_Symbol}{\makebox[4mm][l]{\strut}}&\fcolorbox{black}{color_String}{\makebox[4mm][l]{\strut}}&\\
\(\texttt{Create Experiment}\)&\fcolorbox{black}{color_String}{\makebox[4mm][l]{\strut}}&\fcolorbox{black}{color_Experiment}{\makebox[4mm][l]{\strut}}& Creates experiment from string \\
\(\texttt{Frequency of Positive RS}\)&\fcolorbox{black}{color_PositiveSystem}{\makebox[4mm][l]{\strut}}&\fcolorbox{black}{color_String}{\makebox[4mm][l]{\strut}}&\\
\(\texttt{Limit Frequency of Positive RS}\)&\fcolorbox{black}{color_PositiveSystem}{\makebox[4mm][l]{\strut}}\fcolorbox{black}{color_Experiment}{\makebox[4mm][l]{\strut}}&\fcolorbox{black}{color_String}{\makebox[4mm][l]{\strut}}&\\
\(\texttt{Fast Frequency of Positive RS}\)&\fcolorbox{black}{color_PositiveSystem}{\makebox[4mm][l]{\strut}}\fcolorbox{black}{color_Experiment}{\makebox[4mm][l]{\strut}}&\fcolorbox{black}{color_String}{\makebox[4mm][l]{\strut}}&\\
\(\texttt{Graph System}\)&\fcolorbox{black}{color_System}{\makebox[4mm][l]{\strut}}&\fcolorbox{black}{color_Graph}{\makebox[4mm][l]{\strut}}& Creates digraph of RS \\
\(\texttt{Create Dot file}\)&\fcolorbox{black}{color_Graph}{\makebox[4mm][l]{\strut}}\fcolorbox{black}{color_DisplayNode}{\makebox[4mm][l]{\strut}}\fcolorbox{black}{color_DisplayEdge}{\makebox[4mm][l]{\strut}}\fcolorbox{black}{color_ColorNode}{\makebox[4mm][l]{\strut}}\fcolorbox{black}{color_ColorEdge}{\makebox[4mm][l]{\strut}}&\fcolorbox{black}{color_String}{\makebox[4mm][l]{\strut}}& Creates Dot file from a graph \\
\(\texttt{Create GraphML file}\)&\fcolorbox{black}{color_Graph}{\makebox[4mm][l]{\strut}}\fcolorbox{black}{color_DisplayNode}{\makebox[4mm][l]{\strut}}\fcolorbox{black}{color_DisplayEdge}{\makebox[4mm][l]{\strut}}&\fcolorbox{black}{color_String}{\makebox[4mm][l]{\strut}}& Creates GraphML file from a graph \\
\(\texttt{Trace to string}\)&\fcolorbox{black}{color_Trace}{\makebox[4mm][l]{\strut}}&\fcolorbox{black}{color_String}{\makebox[4mm][l]{\strut}}&\\
\(\texttt{Positive trace to string}\)&\fcolorbox{black}{color_PositiveTrace}{\makebox[4mm][l]{\strut}}&\fcolorbox{black}{color_String}{\makebox[4mm][l]{\strut}}&\\
\(\texttt{Group Nodes of Positive System}\)&\fcolorbox{black}{color_PositiveGraph}{\makebox[4mm][l]{\strut}}\fcolorbox{black}{color_PositiveGroupFunction}{\makebox[4mm][l]{\strut}}&\fcolorbox{black}{color_PositiveGraph}{\makebox[4mm][l]{\strut}}&\\
All the types can be seen in table\ \ref{types_gui} that are used for the node's input and output. Each type has a distinct color associated that is used to color the connectors between nodes. All nodes can be seen in table\ \ref{node_in_out}. The second column holds the color of the inputs types used; the third column holds the color of the outputs types.
